Limits

In brief: this is what the parser and checker refuse today. It is a description of the language, not a version number and not a list of things to add later.

The checker does not accept

• Type : Type
• A kind as a small type: Π (x : A) → Type : Type, Type × A : Type, a constructor field of type Type
• Cubical primitives
• Tactics
• Implicits
• Unification
• Metavariables / unification (? is an unsolved goal that always fails; it does not unify)
• A quantity other than affine, +, and -. %0 and %1 are marks on the affine quantity
• A multiplicity on a session endpoint other than affine and linear. Affine, written (s : session) →, is used at most once. Linear, written λ¹ and (s : session) ⊸, is used exactly once. +, -, and % on an endpoint binder are refused. A linear binder on ordinary data, on evidence, or on a run term is refused. An unused linear endpoint is refused. A linear endpoint used twice is refused. A meeting that does not consume a linear endpoint exactly once is refused. Neither multiplicity is a quantity. A linear endpoint may be a recursive session, and it may carry a declared data payload. The multiplicity is the endpoint’s, and the payload stays data
• A ν family with no index, one whose uncons takes the family at other arguments than its indices in order, or one whose body is not a product
• + on Stream
• + on Either
• Typing raw Elixir
• Emitting spec or evidence
• Identity on F32 or Tensor F32 S
• An implicit coercion between Nat and U8, U32, U64, or I64. The maps are toU8, toU32, toU64, toI64, and toNat
• A second index language for tensor shapes. A tensor shape stays one I64
• Redeclaring Nat, Unit, Empty, or Stream as data
• A fourth term representation
• Raw HOAS (Tm → Tm) as inductive syntax
• Tags other than run, run internal, spec, evidence
• A session payload other than a nat, a bit, unit, a pair, a record whose keys are names written in the type, a vector whose length is a numeral or a nat received earlier, a nat at most a bound (send (d : Nat) {d ≤ w}), or a non-indexed declared data type applied to payload arguments. Bool, Maybe Nat, List Nat, and Either Nat Bit are payloads. The constructors are that declaration’s, and each field is a payload: a parameter, that data type, or another such data type. An indexed declaration (Fin, Vec), Atom, a field that is a function, a kind, or erased, a parameter that is not Type, and a name that is not a declared data type are refused. Vec in a payload is the vector form, so a data type of that name is not written there. A put may send the value an in-scope run definition computes from its arguments when that value inhabits the payload (put (effective self) done, put (bump 0) done when bump calls an earlier run, and put count when count is a nullary run). The body is a variable, a literal, a constructor, a match on a constructor or a nat, or a call of a definition declared before it. put (suc 0) is refused, and so is put (plus 0 0) when plus is not an in-scope run definition. put (plus 0 0) is also refused when plus calls itself, and so is a call of a run declared later: the body is refused even on an arm that does not take the call. An application of an evidence definition or a spec definition is refused. An application whose argument is not a value is refused. A run application that does not evaluate to an inhabitant of the payload is refused, and so is a term outside that fragment (let, a remaining λ). A later payload may mention a received nat as the length of a vector. A payload argument stops before a token that begins something else: the words def, data, session, conform, meet, place, scheme, move, endpoint, read, talk, choreography, seat, link, relay, import, param, where, nu, ν, end, send, recv, choose, branch, rec, case, on, done, stop, put, get, pick0, pick1, cover, over, say, and offer; the entries temporal <name> : and repr <name> :=; a name followed by ->, →, chooses, or :; and the closers ) and }. A recursion variable in scope is the continuation (send Bool X). Parentheses group a payload ((Reply), (Maybe (List Nat))). Omitting end after the payload is a parse error at that point, and the message says end was expected. The next declaration stays where it is. A token from that list is not a vector length. The argument count is the parameter count. Reply takes 0 arguments, given 2 is the refusal, and one parameter is argument. A matching count that is still not a payload stays ill-formed payload, including Fin with no arguments. Count, which takes a nat, is Count takes 1 argument, given 0 when no argument is written
• An evidence payload other than that one case: the bound is one ≤ whose left side is the sent nat and whose right side is a numeral or a nat bound earlier. A sum, a successor, <, ≡, two bounds on one payload, a bound inside a pair, a record, or a vector, and a bound that names a nat bound later are refused. The name of the sent nat is in scope in its bound only, so a later length may not mention it
• Evidence that the checker does not find: a numeral within a numeral bound, zero within a name, or the bound name itself when the process bound that name once. A numeral against a received window, another received nat, and a name bound twice have no evidence. A received nat that carried a bound is a plain nat to the receiver, so relaying it is not evidence
• A vector length other than a numeral or that nat (a successor, a bit, a pair, a record, a vector, or a name not bound at a nat). A bit bound by an index is a bit, so a vector length may not mention it
• A next action chosen by a value other than a bit written as two arms, a match on the value a get just bound, or a case on the value just exchanged. recv (b : Bit) on S T continues as S when the bit is b0 and as T when it is b1. The sender writes that literal. get (b : Bit) (match b pick0 done pick1 done) matches on the received bit. Each arm conforms to the one continuation. The processes may differ, and the received value chooses which process runs. It does not choose a different protocol. The meeting runs the process of the value that arrived. A declared data type has one process per constructor, in declaration order (get (b : Bool) (match b done done), get (m : Maybe Nat) (match m done done)). recv (b : Bool) on end end is refused: on is a bit, and the sender writes the literal. A case on the name just bound is accepted for a bit or a declared data payload: recv (f : Frame) (case f | bytes => send Ctl end | trailers => send Ctl end | headers => recv Body end). The arms are that declaration’s constructors, in declaration order, one protocol each. The dual is send with the dual of each arm. A receiver covers every constructor, and each process arm conforms to the protocol arm of that constructor. A sender of a literal or a computed value is checked on the arm that value selects. A case on a run of that value is accepted when the run takes the payload, returns a bit or declared data, stays in the computed fragment, and does not call itself or a later run: recv (f : Frame) (case (late f) | true => send Ctl end | false => send Goaway end). The arms are the result’s constructors. Each process arm is checked against what the run returns. A run that only matches the constructor is checked at that constructor. A run that reads a field of a bit or a declared data type is split on the values of the fields it reads, and the process covers that split by a case on the bound field. A field the run binds and does not read is not split. A case on an unbounded nat, a pair, a record, a vector, or unit is refused (a case is on a bit or a declared data type), and so is a case on a name bound earlier than the action just written (a case is on the name just bound). A nat whose bound is a numeral w splits into 0 … w. The arms are those numerals in order, written | 0 => through | w =>, or as positional processes in the same order. | 00 => is not | 0 =>. A run of that nat is evaluated at each numeral, and the process still covers 0 … w. A run of that nat and one declared data payload is the product of the widths, (w + 1) times the constructor count, computed from the declared types. Bit is a payload, not a term, so a file does not give a run the domain Bit. The same product counts a bit when the domain is that payload. The process covers that product. A second bounded nat and a run of three or more finite factors are that same product (erecv-wide). A bound that is a name is not a numeral (recv (w : Nat) (recv (d : Nat) {d ≤ w} (case d …)) stays a case is on a bit or a declared data type). A _ wildcard arm stays case arms do not match the constructors. A nat field of a constructor may carry a numeral bound, (slot : Nat) {slot ≤ 1}, and that field is a factor of width w + 1. A bound that is not a canonical numeral is a field bound is a numeral. A bound on a field that is not a nat is a field bound is on a nat. A bare case, and a case that is not the continuation of that action, are refused (a case follows the value just exchanged). A missing arm, an extra arm, and an arm out of declaration order are refused (case arms do not match the constructors). A run the evaluator does not walk is refused (outside the computed fragment: let), and so is a run that calls itself (run definition calls itself) or a later run (run definition declared later). A run that does not decide a constructor is refused (the run does not decide an arm). A field that is not a finite split, such as a nat, a vector, a pair, or a record, is that refusal, and so is a _ wildcard arm in the run‘s match. A sender whose value is not known at check time is refused unless every protocol arm is the same protocol (the value g does not select an arm). A meeting of a value that is not known is refused, including when the protocol arms agree. A received pair has one arm, | (a, b) =>, binding a at the first component and b at the second. A received record has one arm, | { f1 = a1, ..., fk = ak } =>, naming every field once, in the order the type writes them. A component is payload data, the same way a bound constructor field is. It may be used more than once, it is never linear, including when the endpoint is %1, and the innermost binding wins. put a sends it. put (grant a) is checked by the type grant declares, and both meetings evaluate grant on the component that arrived. A component that is itself a pair or a record is bound whole. A missing field is missing field. An extra field is extra field. A duplicate field is duplicate field. A field out of order is field out of order. A binder count other than two on a pair is wrong arity. A constructor arm on a pair is constructor arm on a pair, and on a record is constructor arm on a record. A nested pattern is a pattern is one level. An unbounded nat, a vector, and unit stay refused as the scrutinee of a session match (match does not cover the received value). A nat received under a numeral bound is covered by one arm per numeral. A case on a pair, a record, or a component stays refused (a case is on a bit or a declared data type; a scrutinee other than the name just received stays a case is on the name just bound). A run that reads a component to choose an arm stays the run does not decide an arm. A component of the wrong type does not conform. A variable bit, a computed bit, and a third arm are refused as the index of on. A short match, a match with an extra arm, a match that is not the continuation of the get just taken, and a match whose scrutinee is not the received name are refused (match does not cover the received value). A named arm on that match binds the constructor’s fields: | nothing => binds none, and | just b => binds b at the field’s type instantiated at the payload’s arguments, so Maybe Bool gives b : Bool. A recursive field binds that same data type, so a List tail is a List. The binder count is the field count (wrong arity). The positional form, one process per constructor and no names, stays, and it is not an arity check. A bound field is payload data. It may be used more than once, and it is never linear, including when the endpoint is %1. The innermost binding wins. put b sends the field. put (grant b) is checked by type: grant is an in-scope run in the computed fragment, not a self-call and not a later run, each argument is a literal, a constructor of literals, or a bound name of the parameter’s type, and the declared codomain is the payload. A put of only literals is still evaluated. The meeting fills the arm from the value that arrived and evaluates that run. The asynchronous meeting does the same. A run that reads a splittable field chooses the protocol for each value of that field. case f still selects an arm by constructor. A run that reads a constructor field whose type is not a finite split, such as an unbounded Nat, a vector, a pair, a record, or a recursive field, is refused (the run does not decide an arm), and so is a _ wildcard arm, a pair or a record as the case payload, an open term, a self-call (run definition calls itself), a later run (run definition declared later), a body outside the computed fragment (outside the computed fragment: let), a case on a name bound earlier (a case is on the name just bound), and a result that is not a bit or a declared data type (a case is on a bit or a declared data type). A process that does not cover the split does not conform. A short or misaligned inner match is match does not cover the received value. An unbound name, including a field that was not bound, is unbound variable. A match whose scrutinee is not the name just received stays match does not cover the received value. A put argument outside the fragment is refused (outside the computed fragment), including a constructor of a bound field (put (just b)). A nested call is argument is not a value (put (grant (just b))). A bound field of the wrong payload type does not conform. A run whose codomain is not the payload is computed value (grant b) does not inhabit Nat. choose stays a label
• Unguarded recursion. rec X. S is that protocol again where X stands. The variable must sit under an action of its own rec: send, recv, a dependent action, an evidence action, an indexed bit, choose, or branch. rec itself does not guard. A case is not a guard. The send or recv that carries the case is the guard, so a call in an arm of that case is guarded. rec X. X, rec X. rec Y. X, and rec X. rec Y. Y are refused. rec X. rec Y. send Nat X is one loop. A guarded action may carry a declared data payload: rec X. send Bool X is that payload again
• A session call that is not an earlier session, applied to the right number of nat arguments, and guarded when it calls itself. session req := send Nat ack is send Nat followed by the body of ack, including in a choose or branch arm, after on, inside a case arm, inside rec, and as an endpoint’s protocol. session frames (k : Nat) := send (Vec Nat k) end is that send at k. frames 3 and frames (bump 0) open it when the argument is a numeral or a run that evaluates, and recv (n : Nat) (rest n) opens rest at the nat just bound. session stream (n : Nat) := send (d : Nat) {d ≤ n} (stream (suc n)) is that send again at the next nat. dual (stream 0) is the dual of the body at 0, and both meeting orders check. A parameter is a nat. An argument is a numeral, a nat in scope, or a run application the same evaluator accepts as a put. session s := s is unguarded session call. A call of a session declared later is session declared later. An unknown name is unknown session. The wrong number of arguments is wrong number of session arguments. An argument that does not evaluate names that argument: argument (plus 0 0): run definition calls itself, argument early: run definition declared later, argument nope is not a nat. A put that misses the instantiated bound names that numeral (d ≤ 0). A self-call may change a vector length; the protocol is still guarded, and a looping put (rep 0 0) against send (Vec Nat n) (grow (suc n)) fails at the next length. The other end of a self-calling session is dual of that call. A second session that calls itself is not that dual. dual ping may still name a session declared later. choose ack (frames 3) is read as an application, so the two arms are written (ack) and (frames 3). A parameter other than Nat is refused
• A free session variable in a process. A bare name in a process is a recursion variable. conform bad : ping := X is refused. A bare name in a protocol is a session call, not a free variable. rec X. X stays unguarded recursion. Y in rec X. send Nat Y is unknown session Y when no session Y was declared earlier
• A recursion variable used as a payload. put X sends the value X. A name not bound by get is unbound. The recursion variable is the continuation, not the value
• A session %1 whose process jumps back to rec. A jump does not finish. rec X. get (n : Nat) (put n X) conforms to rec X. recv Nat (send Nat X) and is still refused at %1. rec X. done does not jump, and %1 accepts it
• An asynchronous meeting of more than two participants, an unbounded buffer, or a transport that reorders messages. meet name : left with right buffer N is two processes and one FIFO in each direction, holding at most N messages. A send waits when its own queue is full; that wait is not an error. A receive takes the head of the other queue. The head has to be the type, the label, or the arm the receiver names. Both processes finish only with both queues empty, and until then some step has to remain possible. A buffer that is not a numeral is buffer bound is a nat. A loop that would enqueue a value built from a received name, such as a successor of that nat under a constructor, is unbounded recursive payload. A constant payload and an echo of a received value stay in the alphabet. rec X. X stays unguarded recursion. The synchronous meeting, written with no buffer, is unchanged. Buffer 0 is not that meeting: every send waits
• An OTP session process talking to more than one peer
• Two calls for one cross
• A call for a stay

The meeting is checked. The OTP image is the only runtime that can produce the event of two processes exchanging the payload and stopping :normal when the parties sit at different places. Other emitters are unchanged because they do not implement the meeting.

Former names (history, not syntax)

The language was once described as nothing dead runs and a proof never becomes a run. Those words are not tags. The tags are spec, evidence, and run.

What is proved, and what is not

• The mode wall is proved for the core fragment in agda/Muro/Wall.agda.
• In agda/Muro/Consistency.agda: no closed normal evidence term has type Empty, closed evidence terms make progress, and a reduction step keeps the type of closed evidence (preservation, from agda/Muro/Typing.agda). Conversion is a congruent relation generated by a confluent parallel reduction (agda/Muro/Reduction.agda, agda/Muro/Convert.agda), and the modules are checked under --safe.
• The fragment these are proved for is Π, λ, application, Nat, Unit, Empty, identity, rewrite, def, annotation, pairs (A × B, (a, b), let (a, b) = e in t), and data with constructor applications and match, on indexed data types too (⇒-mData: the motive is a telescope over the indices and the scrutinee, a branch is typed at its constructor’s own indices, a constructor whose numeral index clashes with the scrutinee’s is skipped), and ν (Stream, Always, ~, and declared families). An unfold of a stream is the λ (⇐-unf); uncons of that λ wraps and stays a stream. An unfold of a declared family is the pair instantiated at the seed (⇐-unfR); uncons of that pair reads the head obligation and the proof at the tail. uncons of the source λ wraps, and that wrap is not the family read. The checker refuses a self-call in the head of an unfold, and refuses a tail that uses the block other than as a guarded tail: a block member applied to arguments that do not mention the block, a pair of guarded tails, or a nested unfold whose seed, binder type and head are free of the block and whose tail is guarded. Outside spec, a seed that mentions the block is refused when the head or the tail reads the seed binder; the refusal is <name> productivity: unguarded recursive call. A bare stream unfold is refused when its head reads the seed and its tail mentions the block, at every such unfold in the body (under a pair, an application, a match, a λ, or another unfold). The head reads the seed when the binder occurs in it, including under a match, an annotation, a unit match, a rewrite, or an empty motive. accepted-productive‘s Seen observes those nested unfolds. A declared family stays accepted. A seed neither component reads stays accepted, including a descending call discarded before the step. A block-free seed may occur in either component. guardedTail-reflects says that boolean reflects the inductive relation GuardedTail. checkUnfold-guarded says that an unfold checkUnfold accepts outside spec has, after whnf, lambdas over a pair with a block-free head and a guarded tail. ⊢ records the pair and does not recheck that guard. accepted-productive in agda/Muro/Productive.agda says that if checkSig accepts the signature, every run or evidence definition is observable at every finite depth: each head is block-free and the observation does not re-enter the block. The only hypothesis is that acceptance. Normalisation of a block-free head (Empty-evid) and termination of an accepted block by the descent check are not this theorem. Tensor and Atom remain outside. ⊢ does not check data declarations (positivity, small fields); Check.checkData does. A field is strictly positive after unfolding: D is absent, or D heads a spine whose arguments do not contain D, or D occurs only to the right of a Π whose domain does not contain D. D inside an argument of D is refused. Another data type is not opaque: its fields are held to the same test, so D stored there and placed in a domain is refused. Run, evidence, and spec definitions that reach each other descend each on an argument of its own: every call passes a smaller variable at the callee’s position, or the caller’s argument unchanged to a definition earlier in the signature, so (size, index) decreases at every call. The checker decides this; termination of an accepted block is argued from that measure and is not an Agda theorem.
• Preservation is proved for derivations in every mode (Typing.pres), given a signature whose bodies have their declared types (WfSig). That hypothesis is not the checker’s acceptance of the signature. The proof covers the wrap of a stream λ and the read of a family pair. fam-def-uncons in Soundness.agda opens a definition whose body is a family λ onto that λ, and derives uncons of the pair instantiated at the seed at the family goal, in any context. The opened definition and that pair are two subjects.
• The executable checker is sound for ⊢ on the fragment (agda/Muro/Soundness.agda, with Soundness/Conv.agda and Soundness/Views.agda): if Check.infer, check, or checkTy answers yes on a fragment term over a fragment signature whose constructor types are telescopes ending in the data type at its parameters and indices (GoodSig), and every premise is at the type its rule requires, ⊢ has a derivation with the same uses. For a stream unfold the subject is the term checked, and the type infer returns is convertible to the one ⊢ infers. For a declared-family unfold the subject is the pair instantiated at the seed, not the source λ, and that derivation is not claimed convertible to a type computed from the λ. A premise that is not at the type its rule requires is not a derivation. checkSig-sound lifts acceptance of a signature to that statement for each definition. This is one direction only (no completeness), for the ⊢ fragment only. Muro.Check and the soundness modules are checked under --safe: no postulates, no TERMINATING pragmas. The theorem holds for every value of the fuel.
• The checker is fuelled, and running out is not a verdict. Fuel bounds reduction (whnf, conversion, isData, the index-clash test); everything else is structural recursion on the term. A definition applied to arguments unfolds only when that unfolding makes progress: the match it reduces to fires on a constructor. The arguments are compared first. If they convert, the applications convert. If that comparison runs out of fuel, conversion stops. A definite mismatch unfolds once. While that unfolding is already in progress and the match does not fire, the application is neutral and the argument mismatch stands, so two stuck calls that differ in an argument the unfolding does not erase fail at every fuel. Fuel is one budget shared by the argument comparison and that unfolding. When the budget is spent the answer is the error out of fuel (the checker gave up reducing; raise the fuel), never a silently unreduced term and never a type error. Raise it with mix muro.check --fuel N path.muro (default 2000) and check again; there is no resumption. A term that needs more fuel than any you give it is refused, not accepted: fuel caps what the checker tries to prove, not what it proves. Removing the cap waits on normalisation, the same open hypothesis as Empty-evid. A fixed-width word operation, and a closed numeral, does not spend fuel in proportion to the magnitude. toNat of a residue is that numeral. Two closed numerals convert by integer equality. A match peels one successor off a closed numeral and does not expand it.
• Spec descends, and it is still not the logic. A spec definition that names itself unapplied (def T : spec Type := T, def X : spec Type := Π (+ x : X) → Empty) is refused, and so is a call that does not pass a smaller variable (def bogus : spec Π (n : Nat) → {n ≡ suc(n) : Nat} := λ (n : Nat) → bogus n). IsEven stays: it recurses on a match-bound predecessor. Evidence is the logic: a rewrite in a run or evidence term reads an evidence equation. Fuel still bounds a spec computation inside a type. This descent check removes the negation that built a closed evidence term of Empty; it is not a proof that every accepted spec term normalises.
• The full consistency statement (Empty-evid) is not proved. Normalisation of closed evidence is its one open hypothesis (Empty-evid-from). Do not cite Empty-evid.
• Type is impredicative and kinds are not small types. Before the kind/small-type distinction was enforced, the checker accepted Π (x : A) → Type : Type, which retracts Type into a small type; that was a bug in the calculus, not in a program, and it is fixed in both Agda and Elixir.
• A nat at most a numeral is a finite split, and so is a nat field of a constructor whose bound is a numeral. in-split and split-bound in agda/Muro/Session.agda say every value in 0 … w is in the split and every member is within the bound. in-product and member-admitted say every tuple the factors admit occurs in the product, and every member of the product is such a tuple. enum-size says the split of a run has the product of the factor widths, for any factor list, with no fuel and no budget. prod-card is that product for one bounded nat and one constructor list. data-size is the sum of those products over the constructors. val-sound and rows-at say a process that covers the split conforms on every value the bound admits. bound-recv-decides is the decision for bound 1. meet-agrees in agda/Muro/Meet.agda says the meeting of a literal numeral takes the arm that numeral selects. The derivation that is checked is one bounded nat, that nat with one bit or declared data payload, or any other finite product of those factors (erecv-wide, mget-wide, eget-wide, eput-wide, dput-wide). The modules are checked under --safe.
• A synchronous meeting is an asynchronous meeting at buffer 1. meets-async in agda/Muro/AsyncSync.agda says that every Meetsρ derivation is a safe configuration at bound 1, for every value environment, with both queues empty at the start. A larger bound is not proved. The checker in agda/Muro/Async.agda accepts a finite meeting only when every reachable configuration has no reception error, every configuration that is not finished can step, and a finished configuration has both queues empty. The search recurses on the size of the two processes. agda/Muro/AsyncRec.agda decides a recursive meeting by the same statement over a finite universe of configurations; the search recurses on a budget computed from that universe. A shape whose payloads would leave the universe is refused (unbounded recursive payload), not approximated. The three modules are checked under --safe.
• A temporal declaration is decided on the reachable configurations of one buffered meeting (agda/Muro/Temporal.agda, Temporal/Graph.agda, Temporal/Safety.agda, Temporal/Live.agda, Temporal/Decide.agda, Temporal/Fair.agda). Satisfies g φ is every infinite run from init g satisfying φ. Holds of leadsTo p q is Globally of p implying Eventually of q. TemporalOk g m φ is Satisfies g φ, and m : NoStuck g is the meeting: every configuration reachable from the start has Shape (view g c). Decide.check accepts if and only if Satisfies holds (check-sound, check-complete). Decide.cex-sound returns Valid × ¬ Satisfies for every form. For always, v-fin is the breadth-first parent path to a configuration where the proposition is false, and run-exists extends it to an IsRun. For eventually and leads_to, v-ev and v-to record that parent path, the stem, and a nonempty cycle. The cycle unrolled from init g is an IsRun that misses the formula. The reachable set is reachable. It takes no meeting derivation. The recursion is well-founded on length (Unvisited (Universe g) seen). universe-complete, wf-init, and wf-step say the universe contains the start and is closed under a step. reachable-sound, reachable-complete, and reachable-nodup say the list is exactly the distinct reachable configurations. decide-nostuck decides NoStuck from that list. ex-fin is one reachable configuration on a finished graph. ex-loop-len is four on the loop graph. The liveness region drops a configuration whose successors in the region are empty, by well-founded recursion on the length of the region (prune). A finished configuration stutters, so it stays. solo-bounded says a stretch of consecutive lside steps from c has length at most phiL g c, and the same for rside and phiR. phiL g c is (cap g ∸ length (l2rOf c)) + length (r2lOf c). phiL-bound and phiR-bound take reachability from the start, and that reachability supplies the queue bound. every-run-fair takes IsRun and NotFinal, and says a run that never reaches a finished configuration takes lside infinitely often and rside infinitely often. fair-sum is that disjunction with “the run finishes”, under double negation. I1 says the prune count is the length of the recomputed successor list. I2-miss and I2-hit are the cases of firstZero. The modules are checked under --safe. --guardedness is infective from Muro.Temporal, the same way it is from Muro.Rec, so Graph, Safety, Live, Fair, Decide, Source, Bridge, and Finite carry it too. Source is the source configuration and its step. Bridge.frag? decides the fragment (nat literals, bits, nullary constructors, an echo of a received name). init-sim says the start of that source configuration is init of graphOf. elab of the loop, the crossing pair, the echo, and the spin is the process the compiled graph already uses, by refl. The block lookB reads for those processes is the block of that action, by refl, and the echo put block is not the echo get block. Ordinal.block-of reads the block of an arbitrary ordinal action, and that block has the verb. The echo meeting has 8 reachable states, the spin meeting 4, and the inflight meeting 9, each by refl. The echo and inflight verdicts are Decide.check ≡ yes, and the two spin refusals are Decide.check ≡ no, through yes-check, live-check, and no-check. A source step is a graph step (sim-fwd in Temporal/Expose.agda): a cursor Hold sends every source step to a graph Step of abs whose target is the abs of the successor. A graph step on a left put whose place is already that put, with nothing pending, is that source put (bwd-put in Temporal/Back.agda). A smu peels to the unfold of its body (spine in Temporal/Reveal.agda). A jump is followed to the mu it names (Temporal/Chase.agda), and that unfold agrees with abs (readL, readR in Temporal/Follow.agda). Under Hold, a graph step other than the stutter is the source step (sim-bwd), and the source configuration is final exactly when abs of it is (final-iff in Temporal/Carry.agda). SourceSafe says each reachable source configuration is final or takes a step. That is weaker than NoStuck: one side can step while the other is a fault, and merge returns VBad. SourceShape in Temporal/Span.agda says every source-reachable view is Shape. Under graphOf ≡ gok, echoOk, and muOk, source-safe-iff equates SourceShape with NoStuck, and transfer equates Satisfies g φ with SourceSatisfies g c φ for always, eventually, and leads_to. check-yes and check-no say Decide.check accepts exactly when the source meeting satisfies the formula. cex-source maps a cex-sound refusal to a source run that misses it. inj-fwd and inj-bwd in Temporal/Finite.agda relate one Async.Conf step to one source step of inj. Embed carries the typed messages, the value environments, and the index contexts. inj-fwd sends the async step to a graph Step. inj-bwd reads a graph step other than the stutter back as the async step, and it takes Safe, because a payload received as another declaration is a graph step and a bad reception. init-embed is that embedding at the start. safe→nostuck says that under graphOf ≡ gok, initS ≡ just, and echoOk on both sides, Safe of Async.init is NoStuck. muOk of inj holds whenever Frag does (mu-inj). inj is sout or pOut for a bare arm, an arm list other than the declaration’s constructors in order, a constructor the declaration does not inhabit, an echo whose type is not the binder’s type, a payload type that contains an index variable, a second binding of a name already in scope, and a name that occurs twice anywhere in the process. SourceSatisfies is Holds of the path of projected configurations. Nothing in these modules calls the recursive-meeting search.
• A choreography projects to a binary session for each ordered pair of roles (agda/Muro/Choreo.agda). g ↾ r / s ≡ b is that session on the fragment end, send, recv, choose, branch, and ⌊_⌋ erases it to Proto. project returns that session exactly when the judgment derives it (project-sound, project-complete). pairwise-dual says that when project g r s is just S, project g s r is just (dual S), including a pair that never interacts, where both sides are end. A self-interaction, a choice with fewer than two branches, and a plain merge whose arms differ return nothing. More than two branches nest to the right. A chooser on the channel has choose even when the arms agree. The module is checked under --safe. It does not import Muro.Rec or Muro.Temporal. Global progress beyond a tree of binary sessions, full merge, recursion in the global type, multiparty execution, and multi-place placement are not this theorem.
• Example twins are not a proof that a .muro file is correct.
• import and param are resolved by Muro.Load before anything is checked, and they are not in Agda. std: is that resolution too: the library books are ordinary files, joined before the checker runs. What is checked is the resulting book: the importer’s entries, each imported file’s entries, and the supplying definitions in the params’ place. A library with params is checked once per program that supplies them, not once for every environment: a statement in it is proved for the supplied State, step, and so on, the way an Agda module is checked at its parameters.

A temporal declaration

The surface is Temporal. These are the refusals.

• A meeting written with no buffer: temporal needs a buffered meeting. A temporal declaration on a rendezvous meeting is future work. meets-async relates the rendezvous to buffer 1 for safety. It does not transfer a liveness verdict.
• A pair, a record, a vector, a constructor with a field, or a computed put: payload outside the temporal fragment. A wider explored state needs a wider alphabet first. A loop that grows a value is already unbounded recursive payload at the meeting.
• A formula or a proposition that mentions a run definition: temporal formulas do not mention run definitions.
• A temporal operator inside a proposition, other than the one sugar always (P implies eventually Q): nested temporal operator. That sugar is leads_to.
• forall over Nat, a pair, a record, a vector, or a data type with a field: forall over Nat ranges over an open type, forall over a pair ranges over an open type, forall over a record ranges over an open type, forall over Vec ranges over an open type, or forall over <name> ranges over an open type.
• An unknown meeting, role, binder, step, or constructor: unknown meeting <name>, unknown role <name>, unknown binder <name> in <role>, unknown step, unknown constructor <name>. Two binders of one name: ambiguous binder <name> in <role>. A literal of the wrong type: ill-typed literal. A meeting that does not check: skipped because <meeting> does not check.
• under fair is not in the grammar, so it is a parse error. Internal choice between two enabled actions of one process would be the point at which a fairness clause is added. solo-bounded and every-run-fair are the lemmas that clause would have to replace.

The search has no fuel and no budget. --fuel does not change the verdict. Termination is the measure in the theorem above.

A choreography

The surface is Choreography. These are the refusals.

• A role written twice: duplicate role <name>.
• A name in the global type that is not a role: unknown role <name>.
• A message from a role to itself, or a projection of a role with itself: self-interaction <name>.
• A branch label written twice in one choice: duplicate branch <label>.
• A choice with fewer than two branches: a choice has two branches.
• Plain merge fails: <role>: branches <label> and <label> disagree. Three or more labels are joined with commas. Both ends of the pair are named. An inner choice that fails is that inner refusal, not the choice wrapped around it.
• A payload that is not a session payload is refused with that session error. The wrong number of arguments is <name> takes <n> arguments, given <k>. One parameter is argument.

test/fixtures/choreo_untold.muro is the plain-merge refusal: the arms are alice -> bob : go and bob -> alice : stop, and nobody told alice or bob which arm was taken. The coordinator’s own pairs stay choose end end.

--fuel does not change the verdict. The projection recurses on the global type.

If you need a hole

Write ?. The checker answers with the expected type and the context, then refuses the book. Fill the hole. ? is not a metavariable and it is not in ⊢: a derivation never contains one.

If conversion fails, the error is in surface syntax (Fin n, {n ≡ 0 : Nat}). Write a rewrite or a match until refl checks.

That is the language.