Extending the kernel

In brief: this is Job B. If you only want a program, stop and go back to Start. Order is mandatory.

Order

1. Agda syntax (agda/Muro/Syntax.agda) if you add a constructor — Tm n.
2. Subst (agda/Muro/Subst.agda): wk, sub. Pattern-lambdas passed to sub do not compute; use a named function (instσ, motSucσ).
3. Check (agda/Muro/Check.agda): an infer′ / check clause, and the matching constructor in the documentary ⊢ at the top of the file.
4. Judgement (agda/Muro/Judgement.agda) if the constructor is in the core fragment: the same rule as an inductive constructor, with uses, and the same rule without uses in Muro.Typing (⊨⁰) with a forget-⇒ / forget-⇐ clause. If it reduces, a ⟶ rule in agda/Muro/Convert.agda and a ⇛ rule plus a dev clause and its tri case in agda/Muro/Reduction.agda; every new constructor needs a ⇛ congruence rule and a clause in each lemma of Muro.Reduction and Muro.SubstLemmas. Then Muro.Wall and Muro.Consistency must still check under --safe; a new ⇒ rule needs a spec-⇒-uses clause, ⊨-mode / ⊨⁰-ren / ⊨⁰-sub clauses, a pres⁰ case for each step it takes or () if it is rigid, and, if it is an introduction or eliminator, Empty-intro / Empty-nf⊨ / progress clauses. A rule whose subject is a variable rather than a constructor (t-ctor types any constructor spine) also needs a clause wherever the term was matched with (): ctor-inv in Muro.Typing is the inversion for that shape.
5. make agda until the example twin decides (half_ok-checks is refl for the canonical book). Twins are examples of the rules, not a proof that the book is correct.
6. Elixir mirror, same shapes, each checker clause commented with the Agda constructor (⇒-var-run, ⇐-refl, …):
   • lib/muro/ast.ex
   • lib/muro/subst.ex
   • lib/muro/check.ex
   • lib/muro/parser.ex / lib/muro/emit.ex if it is surface or run code
7. mix test and mix muro.check. A rule change gets a negative test: a book the old rule accepted and the new rule refuses.

Do not add a third representation. Do not use raw HOAS (Tm → Tm) as inductive syntax.

repr entries are host-side declarations checked by Muro.Repr, not part of the Agda calculus.

agda/Muro/IR.agda is the closed run image after checking. It is not a source syntax: its constructors are not added to Tm. An atom there is a nullary constructor of one closed data declaration. atom and matom in that module are ctor and mData of that declaration, so they are inside Tm. An index outside the declaration is refused. Nothing in the IR builds an atom from a string. The Elixir backend prints that Con as a BEAM atom; the enumeration is closed, so the print does not create an atom the declaration did not name.

lib/muro/ir.ex is that judgment on the named book. Muro.IR.elaborate/1 keeps mode: :run (and run internal as export: false) and drops spec, evidence, and data declarations. A {:data, name} layout is Agda’s dataL. {:atom, name} lowers to {:con, "Atom", name, []} and {:matom, ...} lowers to {:match, ...}, arms in the order Muro.Ast.atoms/1 collected. Binder names are the source names; Agda’s de Bruijn Tm has lost them and writes b plus the context length instead. The refusals are c:lambda, c:machine, c:stream, c:erased, and c:unsupported. The C emitter prints this IR. The Rust emitter prints it. The Zig emitter prints it. The Cortex-M emitter prints the Nat fragment of it. The Elixir emitter still walks the named AST.

Elixir Muro.Ast.to_db/2 sends named FOAS to de Bruijn (unbound names become {:def, name}).

agda/Muro/Session.agda is the affine session judgment. A protocol is spec. A conformance derivation is evidence. A communication carries a payload type and one continuation. The payload is a nat, a bit, unit, a pair, a record of named fields, a vector whose length is a numeral or a nat bound by a dependent receive, or a non-indexed declared data type applied to payload arguments. The constructors are that declaration’s, and a value that does not inhabit it has no derivation. An indexed declaration is not a payload. A pair is a tuple. A record is a map whose keys are the field names, in the order written. put sends a value expression of that type: a literal, a variable, or the application of an in-scope run definition. The sent value is the one that application computes from its arguments. The body is a first-order term: a variable, a literal (nat, bit, unit, a pair), a constructor, a match on a constructor, a bit, or a nat, or a call. Agda evaluates it with evalExpr. The run table is ordered latest first, and a definition may call only a definition in the tail, which is every definition declared before it. callsBefore walks the whole body, so a call in an arm that is not taken still refuses the definition. Evaluation of an accepted body recurses on that tail and on the term, with no fuel. A definition that calls itself or a later definition does not evaluate (loop-eval, plus-eval, early-eval). Elixir evaluates that same fragment (lib/muro/session.ex) and refuses the same calls. A result that does not inhabit the payload has no derivation. A term outside that fragment does not evaluate. get binds the received value to a name, which _ leaves unnamed. The continuation of that get may be a match on the received name, one process per constructor in declaration order. A bit is b0 then b1. Each arm conforms to that one continuation. The processes may differ: the received value chooses which process runs, and it does not choose a different protocol. Two protocols after a bit stay isend / irecv, and the sender writes the literal. A dependent receive binds a name the continuation may mention as a vector length. A nat with no numeral bound does not choose the next action. A nat at most a numeral does, and so does a run over any number of finite factors, including a nat field whose constructor declares a numeral bound. The length is the product of those widths, or the sum of those products over the constructors. The two-factor derivation of one bounded nat and one bit or data payload stays. Any other finite product is that split on the whole factor list. The field bound is session metadata. isend x S T sends a bit: b0 continues as S and b1 continues as T. irecv x S T binds that bit in both arms. The name is a bit, so a vector length may not mention it (not-bit-arm). The sender writes the literal. A variable bit has no derivation (fwd-refused). iget offers both arms (iget-ok). esend x e S sends a nat with x ≤ e, where e is a numeral or a nat bound earlier. eput-ok has that evidence as a premise (Owed, decided by owed?): a numeral within a numeral by ≤, zero within a name, or the bound name itself when Once holds of the context. erecv binds a nat. The evidence is not in Proc, so skel does not carry it (full-skel). over-refused is d > w. stale-refused is a name bound twice. Conforms carries the context of bound names. A variable is in scope when the innermost binding of its name has the type put sends: there steps past a binding only when the names differ, so a shadowed binding is out of reach (shadowed-refused). choose and branch select an arm. Abandoning a channel has a derivation. A second action the protocol does not name has none. run is unchanged. None of those constructors is added to Tm. decide searches for a derivation. The Elixir checker follows that search: session names a protocol and conform names a process (lib/muro/session.ex). skel is that process as actions. --backend otp follows skel and the message carries the value. The BEAM runs the server. The proof stops at the derivation. %0, and an unmarked session, is that conformance. %1 also requires Ends: the process finishes at done, and stop has no derivation of Ends. finishes decides Ends. The checker follows it for session %1. A process that finishes has no leave in its skeleton. Both marks use the affine quantity. Neither is a constructor of Qty.

agda/Muro/Rec.agda is the same judgment for a protocol that repeats. The surface form is the finite syntax rec X. S. A variable must sit under an action, and elaboration refuses rec X. X and a free name. Leading recs are one loop. dual on that syntax is structural: rec stays rec and a variable stays. The protocol a rec denotes is coinductive. unfold reads one guarded action and ties the loop under that action. dual∞, _~_, Conforms∞, and Meets∞ are bisimulations: one step, then the continuations. The step of a send requires sent v ≡ true, the same premise as Muro.Meet, so a declared data value that does not inhabit the payload has no meeting inside the loop, and neither does a computed value that does not inhabit it. A computed put uses the same put. Finishes stays a finite walk, and a jump has no derivation, so %1 still refuses a loop. run is unchanged. None of these constructors is added to Tm. The finite Proto in Muro.Session is unchanged, and Muro.Dual, Muro.Meet, Muro.Talk, Muro.Seated, Muro.Held, and Muro.Located do not import Muro.Rec. Muro.Linear does: an endpoint’s protocol is that finite syntax. Muro.agda imports both, so that file’s pragma is --safe --guardedness. --guardedness is allowed under --safe. The Elixir checker follows the elaboration and the bisimulation (lib/muro/session.ex, lib/muro/meet.ex): one pass of the finite syntax, and the same head again conforms. --backend otp follows a loop with a tail call on drive.

agda/Muro/Temporal.agda is one linear-time formula of one buffered meeting. The formula is evidence. always, eventually, and leads_to are interpreted on infinite runs, and a finished configuration stutters. NoStuck is an argument, so the meeting is not checked again. Temporal/Graph.agda enumerates the reachable configurations by well-founded recursion on the unvisited part of a finite universe. Temporal/Safety.agda decides always. Temporal/Live.agda decides eventually and leads_to by pruning configurations that have no successor left in the region. Temporal/Decide.agda is the one check, and check-sound with check-complete say it accepts exactly when every run satisfies the formula. Temporal/Fair.agda bounds a stretch of one side and concludes that a run which never finishes takes both sides infinitely often. Temporal/Source.agda is the source configuration. Temporal/Bridge.agda elaborates the fragment into the compiled process and relates the two starts (init-sim). Every source step is a graph step (sim-fwd). Under Hold, the backward step is sim-bwd and satisfaction transfers (transfer in Temporal/Span.agda). Temporal/Finite.agda embeds a finite Muro.Async meeting: inj-fwd, inj-bwd, and safe→nostuck. Limits names the Safe premise and the forms inj refuses. None of these constructors is added to Tm. The Elixir checker follows the compiled graph and the same traversal (lib/muro/temporal.ex, lib/muro/temporal/). meet is unchanged. Emit skips the declaration. The pragma is --safe --guardedness, because the runs are coinductive and the option is infective.

agda/Muro/Dual.agda is the other end of that protocol. send swaps with recv, esend swaps with erecv, isend swaps with irecv, and choose swaps with branch. Each arm of an indexed bit dualises, and the index stays (route-other). The payload type stays. The continuation dualises. The other end of the other end is the same protocol. The other end is spec. A run term has no seat. The mark stays the session’s mark. None of this is added to Tm. The Elixir checker follows dual (lib/muro/session.ex). session name := dual name names that end. An omitted mark is the named session’s mark. A written mark that disagrees is refused. A cycle of duals has no protocol.

agda/Muro/Meet.agda is two processes on one channel. A send meets a receive of the same payload type, and the continuations meet. Any value of that type meets, including a value computed from a run definition when that value inhabits the payload. A match selects the arm of the received value, and that arm meets the other party’s continuation. A value that selects no arm has no meeting. A received nat instantiates vector lengths that name it on the receiver, and a vector of another length has no derivation. An evidence payload meets as a nat. The evidence is in each conformance, so a Channel needs it (guess-no-channel). A literal bit meets the arm of that bit (iget-b0, iget-b1). A variable bit selects neither (not-var). A computed bit does not select an indexed arm: the sender still writes the literal. Two indexed receives have no meeting. A variable meets that receive when the innermost binding of its name has that type. A choice meets the arm that was offered. Both ends close, or both abandon. A type they do not share has no derivation. The meeting is evidence. One end conforms to the protocol, and the other conforms to the other end of that protocol. decide searches for a derivation. A run term has no seat. None of these constructors is added to Tm. The Elixir checker follows the meeting (lib/muro/meet.ex). meet name : left with right names two processes, a conformance or a reading. The resolved protocol of one is the other end of the other. The payload types must meet. --backend otp follows a meeting by starting the two processes as each other’s peer (lib/muro/emit/otp.ex). Each server still talks to one peer, and the message carries the value. The place stays the call --node writes.

agda/Muro/Talk.agda is one description of an exchange. A party is a name. say is one party sending a value of one type to another, then one continuation. offer is one party choosing and the other offering both arms. A party does not talk to itself. On a say, the sender’s session is send of that type and the receiver’s session is recv of that type. On an offer, the sender’s session is choose and the receiver’s session is branch. A party off a say has the continuation’s session. A party off an offer has a session only when both arms are the same description, and then it is that continuation’s session. The other party’s session is the other end. A description that does not give a party a session has no evidence at that party. Spec holds the description. Evidence is one party’s session. A run term has no seat. None of these constructors is added to Tm. The Elixir checker follows seen (lib/muro/talk.ex). talk writes the description. session name := seen party with party in talk is the session one party has with another in that description.

agda/Muro/Choreo.agda is a global type projected to a binary session for each ordered pair of roles. A role is a name. comm is one role sending a payload to another, then one continuation. choice is one role choosing a labelled branch. The label selects the branch and is not in the session. g ↾ r / s ≡ b is that session on Bin, and ⌊_⌋ erases it to Proto. project decides the judgment (project-sound, project-complete). pairwise-dual says the session r has with s is dual of the session s has with r whenever the first projection exists. A pair that is neither end of a choice has a session only when every branch projects to the same session. Fewer than two branches is not a choice. A chooser on the channel has choose even when the arms agree, and more than two branches nest to the right. The module does not import Muro.Rec, Muro.Talk, or Muro.Temporal. Its pragma is --safe. None of these constructors is added to Tm. The Elixir checker follows project (lib/muro/choreo.ex). choreography writes the global type. session name := seen role with role in choreography is the session one role has with another. A pair that never interacts is end. The emitters skip the declaration.

agda/Muro/Seated.agda is where a party of a description sits. A party is a name. A place is ambient or a node. Two parties who have a session stay when they sit at the same place, and cross once when the places differ. The boundary is the move between those places. A party with no session in the description has no boundary, at any place. The protocol is the session’s protocol at every place. The payload stays on the session. Spec holds where the party sits. Evidence is the boundary. A run term has no seat. None of these constructors is added to Tm. The Elixir checker follows the seating (lib/muro/check.ex). seat name : party at place in talk is where that party sits. link name : stay seat with seat in talk is the boundary, and so is cross. A stated mark whose boundary disagrees is refused. The payload stays on the session.

agda/Muro/Held.agda is a meeting at those places. Two processes that meet are the two parties of one description. They stay when those parties sit at the same place, and cross once when the places differ. The boundary is the seating’s boundary. The protocol is the session’s protocol at every place. The payload stays on the session. A party with no session has no meeting, at any place. Processes that exchange a payload the session does not name have no derivation as these parties. The meeting is evidence. A run term has no seat. None of these constructors is added to Tm. A .muro file does not write this meeting. The emitters are unchanged.

agda/Muro/Arrow.agda is the multiplicity on an affine Π binder. %0, and an unmarked binder, may be unused. %1 must be used once. checkArrow is checkBound for the affine quantity, then checkMark. For %0, checkMark accepts every use, so an existing binder is unchanged. Spec forgets uses. A second use is still the affine refusal. Neither mark is a constructor of Qty, and neither is added to Tm. The Elixir checker follows checkArrow for a binder written %1 (:linear on the binder). The λ mark and the Π mark must be the same mark. At an application, %1 counts as the affine quantity.

agda/Muro/Linear.agda is the multiplicity on a session endpoint. The protocol is the finite syntax of Muro.Rec, so it may be rec X. S and a payload may be a declared data type. Affine is the default, and it is used at most once. Linear is used once. checkMult for linear is checkArrow for %1. dualS keeps the multiplicity and dualises the protocol: rec stays, the variable stays, and the payload stays. A meeting keeps the multiplicity and refuses a linear endpoint that is not consumed once. A match consumes every arm once. An empty match is one use. One abandoned arm is none. Mult is aff or lin. qty lin ≡ affine. Neither multiplicity is a constructor of Qty. Nothing is added to Tm. The protocol stays spec. The process stays evidence. The endpoint function is evidence, so emit drops it. The OTP image carries the value. The module imports Muro.Rec, so its pragma is --safe --guardedness. The recursion in this module is structural on that finite syntax. The Elixir checker follows that judgment for a definition whose type is an endpoint arrow (lib/muro/linear.ex).

agda/Muro/Place.agda is the placement coeffect. A value sits at a place. Ambient is the default. A polymorphic scheme is instantiated at the place where it is used, and that use stays. A fixed value used at another place crosses once: stay has no boundary and cross has one. Spec holds the scheme. Evidence is the move. A run term has no seat. None of those constructors is added to Tm. decide chooses stay or one boundary. The Elixir checker follows that choice: place names a place, scheme names a scheme, and move states stay or cross (lib/muro/place.ex). A stated mark whose boundary disagrees is refused. --node follows a cross (lib/muro/emit/node.ex). The call is GenServer.call({name, node}, {:muro_read, scheme}, timeout), and :erlang.monitor(:process, {name, node}) is installed before it. name is the scheme, registered on that node, and that registration is the reference. A stay emits no call. The BEAM runs the call. The proof stops at the move.

agda/Muro/Located.agda is a session at a place. The endpoint is a protocol, a mark, and a scheme. Spec holds the endpoint. Evidence is the conformance together with the move. Reading the scheme where it sits stays. Reading it at another place crosses once. any stays where it is read. %0 is the affine session, and abandonment has a derivation. %1 also finishes, and stop has none. A payload the protocol does not name has no derivation, at any place. The boundary is the move. The payload stays on the session. Neither mark is a constructor of Qty. None of these constructors is added to Tm. A run term has no seat. The Elixir checker follows that sitting (lib/muro/check.ex). endpoint names a session and a scheme, and the session’s mark is the endpoint’s mark. read states stay or cross, the process, and the place. A stated mark whose boundary disagrees is refused. A payload the protocol does not name is refused before the boundary is. The run emitters omit the endpoint and the reading. --node follows a read cross with the same call as a cross of that scheme (lib/muro/emit/node.ex). The scheme is the one the endpoint names. The payload stays on the session. A read stay emits no call. --backend otp follows the process (lib/muro/emit/otp.ex). The actions are skel. The server talks to one peer. The place stays on the reading.

Rules that keep the sort honest

Some premises are there for consistency of the calculus, not for programs. Keep them when you add a former.

• ⇒-pi: the codomain is checked against Type, not merely well-formed. Π (x : A) → Type is a kind (type-pi), not a term of type Type.
• ⇒-prod, ⇒-nu: components and the ν body are checked against Type.
• Constructor fields are checked against Type (checkCtorFields); parameters (A : Type) are exempt.
• ⇒-idt is the deliberate exception: the sort in {a ≡ b : A} is only wf, so {Nat ≡ Unit : Type} : Type. That is the shape of Coq’s eq in impredicative Prop, a singleton family indexed by a large sort with elimination allowed. refl has no field, so rewrite cannot project a type back out and no retract of Type arises. Keep it a singleton: an identity type with a field would need the same restriction as constructor fields.

Relaxing any of these to wf makes Type a retract of a small type, and with match … motive (λ _ → Type) or β that is Girard’s paradox. That happened once with ⇒-pi; the test "a kind is not a small type" in test/muro_check_test.exs guards it.

Elixir constraints

• ASCII identifiers only. No unicode primes, no mixed-script atoms.
• Do not define local hd/1.
• Guards cannot call ordinary defp helpers.

What Agda is

Agda holds the rules. It is not a certificate that a .muro file is correct. It is not what mix muro.check runs.

• Muro.Env — Sig, Ctx, uses. Shared by Muro.Check and ⊢.
• Muro.Check — the decision procedure, with a documentary ⊢ (no uses) at the top of the file. Structurally recursive on the term and --safe; fuel is spent only where a term is reduced (whnf, conv, isData, clashIdx), and running out is fail outOfFuel, never an unreduced term. A constructor spine is checked from its head (inferCtorSpine: the constructor’s type at the parameters, then one Π per argument), a branch one λ at a time (checkBr / checkBrPi).
• Muro.SubstLemmas — the renaming / substitution algebra of Tm (ren-ren, sub-sub, sub-inst, inst-wk, …), pointwise, no function extensionality.
• Muro.Tag — a constructor number for each Tm constructor. Check.synEq and Check.convN compare tags before structure, so proofs about them case on two terms of equal tag instead of listing every off-diagonal pair.
• Muro.Spine — application spines appsFrom h as as a relation (Spine h as e), read back by unspine, unique for rigid heads, and their renaming / substitution lemmas. The spine views Check uses (ctorSpine, dtyArgs, defArgs) are characterised here.
• Muro.Frag — the ⊢ fragment as a predicate on terms (Frag), on lists, on signatures (FragSig), and on contexts (FragCtx), closed under renaming and substitution.
• Muro.Reduction — parallel reduction ⇛ (δ, β, ι including ι for match on a constructor spine, ann, congruent under every constructor), closed under substitution, confluent by complete developments. Rigid heads and data-headed spines are preserved along ⇛*.
• Muro.Convert — the weak-head strategy ⟶ (exactly Check.whnf: deterministic, with normal and neutral forms Nf / Ne; constructor and dty spines are normal), and conversion ≈, the equivalence generated by ⇛. ≈ is a congruence, closed under substitution, and joinability by confluence; ≈-shape separates rigid heads, ≈-pi-inj / ≈-idt-inj invert Π and ≡, ≈-dty-inj inverts a dty spine (same type, convertible arguments), and a constructor spine is never convertible to a dty spine or to a rigid head.
• Muro.Data — what the data rules are stated with: IsData (Nat, Unit, Empty, a dty spine whose parameters are Data, closed under ≈) and ReuseOk; InstParams (a constructor type instantiated at the parameters); BrTy (the type of a match branch: one Π per field, then the motive at the constructor application). Each is closed under renaming, substitution, and conversion of the telescope.
• Muro.Judgement — inductive ⊢ with uses for the core fragment (Π, λ, application, Nat, Unit, Empty, identity, rewrite, def, annotation, data, pairs with let in both modes, and ν (unfold, uncons: a stream is the λ, a declared family is the instantiated pair); ⇒-letp needs the body’s type to be a double weakening, which Check decides with Subst.strengthen₂, a partial renaming, sound by SubstLemmas.strengthen₂-sound). Conversion is ≈ in spec mode, so every def unfolds, as in Check.whnf. Data as in Check: dty is a spec term of its declared kind (⇒-dty); a constructor application is checked against a dty type, the parameters taken from the type and the arguments checked along the instantiated telescope, an erased field in spec (⇐-ctor, with the constructor spine as a Muro.Spine view and the arguments along the telescope by the list judgment T ▹ as ⇝ R, built from the head outwards as Check.inferCtorSpine walks it: args-[], args-snoc); match on a data type, indexed or not, has the motive at the scrutinee’s indices and the scrutinee (⇒-mData: motApp P is e, with MotiveOk for the motive and brs⟨ … ⟩ for the branches, one per constructor in declaration order, each typed at its constructor’s own indices, a constructor whose numeral index clashes with the scrutinee’s skipped by brs-skip). ⊢ does not check the declarations of σ (positivity, small fields: Check.checkData).
• Muro.Typing — the declarative judgment ⊨ the metatheory is about: ⊢ without uses, conversion at the root of every rule. Proved: ⊢ is sound for ⊨ (forget-⇐), mode weakening along run ≤ evid ≤ spec, renaming, substitution, and preservation (pres: a ⟶ step keeps the type of a derivation in any mode, given WfSig). For data, t-ctor types a whole constructor spine (there is no rule for a bare constructor, so ctor-inv recovers the spine’s derivation), and the ι case of pres is brApp: the branch for the constructor, applied to the constructor’s arguments, has the motive at the scrutinee. It needs nothing of the data declarations beyond what the derivations carry.
• Muro.Wall — mode wall lemmas. No promotion.
• Muro.Consistency — no closed normal evidence term has type Empty (for ⊢ and for ⊨), closed evidence terms make progress, preservation holds at Empty; Empty-evid itself is not proved (normalisation of closed evidence is the one explicit hypothesis of Empty-evid-from). σ-empty declares no data type, so constructor and dty spines are untyped there. ν is in ⊢. Tensor and Atom remain outside.
• Muro.Soundness (with Muro.Soundness.Conv and Muro.Soundness.Views) — the executable checker is sound for ⊢ on the fragment. Conv: whnf-sound (when Check.whnf returns ok u, t ⟶* u in spec and u is in the fragment), synEq-sound, conv-sound (Check.conv says yes → ≈). Views: the Π / identity / data views, isData-sound, GoodSig, instParams-sound, clashes-sound (the index-clash test says clash → Data.Clash). Soundness: infer-sound / check-sound / checkTy-sound: over a GoodSig (a FragSig whose constructor types are telescopes ending in the data type at its parameters and indices) and a FragCtx, infer k σ rs Γ m e ≡ ok (A , u) gives a ⊢ derivation of e with uses u and a type convertible to A when the result is that same term (inf); a declared-family check is a derivation of the instantiated pair, and a premise off its rule is not a derivation. checkTy likewise, when it builds one. checkDef-sound and checkSig-sound are the corollaries for definitions and whole signatures. fam-def-uncons unfolds a definition whose body is a family λ and derives uncons of the instantiated pair at the family goal. The mutual proof is by structural recursion on the fragment witness of the term, following Check (inferCtorSpine-sound on the head of a spine, checkBrPi-sound on the λ of a branch, checkMotive-sound on the motive’s telescope). Out of fuel is fail, so every lemma is about the ok case; the theorem holds for every fuel.

Muro.Judgement, Muro.Typing, Muro.Wall, Muro.Consistency, Muro.Frag, Muro.Tag, Muro.Check, the Muro.Soundness modules, the examples, and what they import are checked under --safe: no postulates, no TERMINATING. Example twins (Example*.agda) are examples of those rules.

The order of the manual is what Muro.Soundness enforces: a clause of Check that ⊢ does not derive is a hole in the proof, not a feature of the checker. Three such clauses were corrected on the way to the theorem, in Agda first and then in lib/muro/check.ex: checkTy is syntax-directed (a kind is recognised by its shape, anything else must infer a type convertible to Type; reducing first accepted (λ (x : Nat) → Type) 0 as a kind), the argument of an application in evidence mode is checked in evidence even when the head is an evidence definition (its uses are then discarded: Env.appUses), and isData is fuelled.

Two facts about the modes that the metatheory depends on:

• Conversion does not see the wall. Check.whnf unfolds every def, so ⊢ and ⊨ take ≈ in spec mode. Conversion is about types; the wall is about terms.
• Positions are monotone in the mode. Every premise of a rule is in a mode ≥ the mode of its conclusion: an erased argument is spec, a type is spec, and the equation of a rewrite is evidence in a run or evidence term and spec in a spec term (Env.rwtMode). This is what the substitution lemma needs (a β step substitutes a term of the λ’s mode for a variable that may be used at any premise’s mode), so preservation holds in every mode. Before 0.8.0 the equation was evidence in every mode and preservation was proved for run and evidence only.

Build

Agda 2.8+ and standard library 2.3 (no --type-in-type):

git clone --depth 1 --branch v2.3 https://github.com/agda/agda-stdlib.git vendor/agda-stdlib
make agda

make agda is agda --no-libraries -i agda -i vendor/agda-stdlib/src --safe, first on the theorem modules (Muro.Wall, Muro.Consistency, Muro.Frag, Muro.Tag, Muro.Check, Muro.Soundness, which import Muro.Typing, Muro.Data, Muro.Convert, Muro.Reduction, Muro.Spine, Muro.SubstLemmas, Muro.Soundness.Conv, Muro.Soundness.Views), then on the whole tree with the examples. make agda-soundness checks Muro.Soundness alone; it takes about ten minutes. The stdlib checkout ships extra .agda-lib files that must not be loaded.

CI runs the Elixir job and make agda on every push and pull request.

Named FOAS (parser output)

{:var, name}
:typ | :nat | :ze | {:su, t} | :unit | :one | :empty
{:pi, qty, a, name, b}
{:lam, qty, a, name, t}
{:app, f, a}
{:mnat, e, x, p, z, y, s}
{:memp, e, x, p}
{:munit, e, x, p, u}          -- kernel only
{:idt, ty, a, b}
:rfl
{:rwt, eq, x, p, t}
{:def, name}
{:ann, e, a}                  -- kernel only
{:prod, a, b} | {:pair, a, b}
{:letp, e, a, b, t}           -- let (a, b) = e in t; fst / snd parse to it
{:stream, a} | {:unf, seed, f} | {:ucons, s}
{:sum, a, b} | {:left, t} | {:right, t}
{:msum, e, x, p, a, l, b, r}

qty is :affine | :reuse | :erased. A book entry:

%{name: "half", mode: :run, export: true, type: named, body: named}
%{name: "IsEven", mode: :spec, type: named, body: named}
%{name: "half_ok", mode: :evidence, type: named, body: named}

export is present only on :run (true → def, false → defp).

De Bruijn drops the name strings: {:pi, q, a, b}, {:lam, q, a, t}, {:mnat, e, p, z, s} with index 0 = nearest binder.

Bidirectional rules

σ , Γ ⊢[ m ] e ⇒ A     infer
σ , Γ ⊢[ m ] e ⇐ A     check

Hard rules you must not relax without a new theory:

1. A run or evidence variable is used at most once, unless + on Data.
2. Run, evidence, and spec recursion descends on a non-erased argument position for each member of a block, the same at every call to that member: a smaller variable there, or the caller’s own argument unchanged when the callee is earlier in the signature; a self-call passes a smaller one, and a self-reference must be applied. (RecSt, checkRec, selfApplied, checkBody in Check; the proof does not depend on the recursion state.)
3. No promotion. Erased variables have no computational use.
4. Emitted code is run only.

Conversion: syntactic equality first, and that comparison does not spend fuel. The same definition applied to arguments is compared at the arguments. Success is congruence. Out of fuel stops, and the unfolding is not started. A definite mismatch unfolds once. While that unfolding is in progress, a re-entry unfolds only when the match fires on a constructor; otherwise the application is neutral and the argument mismatch stands. Any other pair goes to weak-head normal form and is compared again. Fuel is one budget shared by the argument comparison and that unfolding (whnf, conversion, isData, the index-clash test); infer and check are structural on the term. Out of fuel is an error, not an unreduced term: a new use of whnf must propagate {:error, _} (Elixir) / Result (Agda), and a new recursion that is not on a subterm must spend fuel in a clause head, as clashIdx does.

After you change the kernel, update this manual so manual/ stays the language book. Do not put the change only in @moduledoc.