This file is the single authoritative source for the state of
my-lang's proofs. Where any other document (a proof file's own
prose, proofs/verification/README.md, .machine_readable/STATE)
disagrees, this registry wins. Modelled on AffineScript's
CAPABILITY-MATRIX.adoc discipline.
Last verified: 2026-06-14.
| Term | Meaning |
|---|---|
| machine-checked | A proof assistant accepts it today (Qed / no holes) and it is run in CI. |
| locally-checked | Accepts under the proof assistant locally; not yet in CI. |
| conformance-checked | An implementation is shown to refine a verified spec by differential testing against the artifact extracted from that spec (not a full refinement proof). Used for impl ⇄ spec couplings. |
| proved-on-paper | A written proof exists in proofs/**.md; not mechanised. |
| statement-only | The theorem is stated mechanically (typed hole / Admitted); the proof is a tracked obligation, not done. |
| definitions-only | Syntax/rules/operations defined; no theorems yet. |
| absent | Does not exist, regardless of prose elsewhere. |
No proof hole is ever described as "proved". A statement-only theorem is an obligation, not a result. On the Coq track the obligations are recorded as named
Props (noAdmitted/Axiomin the trusted base); on the Idris2 track as typed holes (?todo_*).
| Artefact | Track | Status | Notes |
|---|---|---|---|
| QTT semiring + laws | Idris2 idris/solo-core/Quantity.idr |
machine-checked | Semiring + ordering laws by exhaustive Refl, %default total. CI: proofs.yml Idris job (idris2 --build). |
| QTT semiring + laws | Coq coq/solo-core/Quantity.v |
machine-checked | Laws by destruct; reflexivity, real Qed. CI: proofs.yml Coq job (coqc). |
| Resource-algebra boundary + parametric soundness | Coq solo-core/{ResourceAlgebra,SoloCore}.v |
machine-checked | R2 (2026-06-13). Module Type SEMIRING (10 laws). The whole Coq solo core (syntax/usage/typing/soundness) is one functor SoloCoreF (M : SEMIRING); Include SoloCoreF Linear3 recovers progress/preservation/affine_pres axiom-free (Print Assumptions closed, CI-guarded). Tropical/affine instances reuse the functor unchanged (R4). The four former chain files (Syntax/Usage/Typing/Soundness.v) are merged into SoloCore.v. |
Affine layer (aff_type, affine_pres) |
Coq solo-core/SoloCore.v |
machine-checked | R3 (2026-06-13). ORDERED_SEMIRING is now live and the functor is SoloCoreF (M : ORDERED_SEMIRING). ule = pointwise qle; aff_type G D t a := ∃ D0, has_type G D0 t a ∧ ule D0 D ("uses at most budget D"); has_type_aff (linear ⊆ affine), aff_weaken (discard surplus), and affine_pres (budget-preservation) are real Qed, axiom-free. Makes affine_pres DISTINCT from preservation (no longer := Preservation). The linear proofs use only SEMIRING. |
| Tropical (min-plus) instance | Coq solo-core/Tropical.v |
machine-checked | R4 (2026-06-13). Module Tropical <: ORDERED_SEMIRING (carrier ℕ∪{∞}, ⊕=min, ⊗=+, 0=∞, 1=Fin 0); Module SoloTropical := SoloCoreF Tropical yields progress/preservation/affine_pres axiom-free at an INFINITE carrier with no new soundness proof — the R2 functor's acceptance test (it provably does not rely on the finite carrier). |
Usage-walk checker (check) + adequacy |
Coq solo-core/SoloCore.v |
machine-checked | R5 (2026-06-13). Executable one-pass synthesiser check : tctx → tm → option (ty × uvec) proved equivalent to the declarative has_type: check_sound (only well-typed terms accepted), check_complete (every derivation recovered with exactly its usage), and check_correct : has_type G D t a ↔ check G t = Some (a, D) are real Qed, axiom-free (Print Assumptions closed, CI-guarded). Internalises usage/type determinacy (corollary typing_unique). SoloTropical inherits the verified checker at the infinite carrier for free. Needs Q_eq_dec (added to ORDERED_SEMIRING); the soundness proofs do not. The F1.4 tail; overtakes AffineScript (which states the same static-split≡usage-walk equivalence only as prose — "an explicit equivalence lemma is future work"). Several Compute-backed examples pin non-vacuity. |
Affine judgement decidability (aff_type_dec) |
Coq solo-core/SoloCore.v |
machine-checked | R5b (2026-06-13). check decides the strictly-linear has_type; the affine judgement aff_type (R3, the affine discard) is decided by aff_type_dec, via aff_type_iff : aff_type G D t a ↔ ∃ D0, check G t = Some (a, D0) ∧ ule D0 D (the affine analogue of check_correct) and ule_dec (the budget order is decidable as qle is bool). All axiom-free, CI-guarded, inherited free at the tropical carrier. The discard is the exact separator: the same UnitT at budget One is aff_type-accepted but has_type-rejected. |
me → solo elaboration (elab) + concrete adequacy |
Coq solo-core/SoloCore.v |
machine-checked | M1.0 (2026-06-14). The visual/block me surface (no settled AST in code — only the paper block grammar in proofs/me/visual-semantics/formal-model.md) is pinned as me_tm (the affine/token fragment) with elab : me_tm → tm landing in the de Bruijn solo core (the mechanised translate). Examples EXECUTE elab + the R5 check on the concrete carrier: a linear token create-and-consume is accepted; the dropped token is rejected linearly but accepted via sequencing and via the R3 aff_type layer; the echo linear→affine bridge end-to-end. Real Qed/reflexivity. |
me → solo universal adequacy (elab_data_check) |
Coq solo-core/SoloCore.v |
machine-checked | M1.1 (2026-06-14). elab_data_check : ∀ e G, me_data e = true → ∃ a, check G (elab e) = Some (a, uzero G) — formal-model.md Theorem 1 (Visual Soundness) for the no-linear-use fragment (data + discard-sequencing + sum injections), real Qed, axiom-free (Print Assumptions closed, CI-guarded). Corollaries elab_data_typed (has_type via check_correct — the cleanest Visual-Soundness statement) and elab_data_aff_budget (fits any affine budget ≥ uzero G, the R3 discard). The first mechanised surface→core elaboration-correctness result in either sibling; overtakes AffineScript (solo-only, no me-like dialect). The linear-USE constructs are M1.0 Examples here; their UNIVERSAL adequacy is M1.1b (below). |
me → solo universal linear-use adequacy (me_wt / me_wt_sound) |
Coq solo-core/SoloCore.v |
machine-checked | M1.1b (2026-06-14). A me-level typing/usage judgement me_wt : tctx → uvec → me_tm → ty → Prop (the visual linear token discipline, colours/ports abstracted) with me_wt_sound : me_wt G D e a → has_type G D (elab e) a — elaboration is type- AND usage-preserving — real Qed, axiom-free (Print Assumptions closed, CI-guarded). Covers the resource-INTERESTING constructs UNIVERSALLY: token consumption (MeVar), MeLet (consumed once), MeUsePair, and the new faithful conditional MeIf → Case (the paper IfBlock = sum ELIM; MeInl/MeInr are sum INTRO). Corollaries me_wt_check (accepted by the verified check) and me_wt_aff (any affine budget ≥ realised usage). It spans the WHOLE me_tm: MeSeq (sequencing/discard) is closed too via MW_Seq, reusing the existing F1.4 ht_shift0 weakening lemma (e1 erased at multiplicity Zero, e2 weakened under the discarded binder) — so the elaboration is universally type- and usage-preserving over the entire pinned surface. M1 (axis-4 SURFACE) is complete. |
Ensemble session-π core (SessionPi.v) |
Coq solo-core/SessionPi.v |
definitions-only (+ machine-checked witnesses) | S1.0 (axis-2 STRUCTURE, 2026-06-14). A NEW standalone Coq development (NOT an extension of SoloCore.v — processes are a different term language; nothing carrier-bearing imported) for the ensemble session-typed π-calculus, after proofs/duet/session-types/ + proofs/ensemble/agent-calculus/. Defines: base-value payloads (vty/val/vtype), session types sty (send/recv/end) with a computed duality and dual_involutive (Qed), polarised endpoints (Pos/Neg, co_involutive), processes proc (nil/send/recv/par/νrestriction), capture-safe payload substitution, a linear channel-typing judgement wt with context splitting csplit, and small-step step for the communication redex under par/ν contexts. Executable witnesses are real Qed: a well-typed ping-pong (wt_pingpong) that reduces (step_pingpong/step_sys), plus duality Compute examples — all axiom-free (Print Assumptions closed), CI-built by proofs.yml. Subject reduction is NOT claimed here — it is the S1.1 obligation. Honest OUT (deferred): name-passing/mobility (payloads are base values ⇒ capture-safe, no scope extrusion), structural congruence (S1.2), choice select/branch (S1.2), replication, mismatch, μ-recursion, bisimulation, the AI primitives, and multiparty G/projection (the S2 hook). |
Session-π communication-redex subject reduction (sr_comm) + value substitution (wt_subst) |
Coq solo-core/SessionPi.v |
machine-checked (Coq) | S1.1a (2026-06-14). The load-bearing core of subject reduction, isolated as two axiom-free Qed lemmas (Print Assumptions closed, CI-guarded). wt_subst (with corollary wt_subst0) is the first-order value-substitution lemma — strictly easier than the solo core's ht_subst because payloads are base values (no channel-context splitting inside the substitution). sr_comm is subject reduction for R-Comm: given a sender continuing at k and a receiver that — by DUALITY (exactly what a ν-bound channel guarantees) — expects the sent type t and continues at dual k, the reduct P ∣ Q[v] is well-typed at the session-advanced context. These are architecture-invariant (they act at the payload / PPar level, never touching the ν binder). |
Session-π full closed-system subject reduction (config_subject_reduction) |
Coq solo-core/SessionPi.v |
machine-checked (Coq) | S1.1b (2026-06-14). config_subject_reduction : wf_config c → cstep c c' → wf_config c' — real Qed, axiom-free (Print Assumptions closed, CI-guarded). Done via the fused two-party (νc)(P∣Q) form (config/party/cstep, the duet T-Session primitive — owner-chosen): the shared protocol lives on the configuration and advances locally on each communication, so the free context never changes and ν re-typing is automatic (the protocol s is existential in wf_config). Reuses the S1.1a value-substitution machinery verbatim via the party analogue pty_subst/pty_subst0. Faithfulness fence: the TWO-PARTY, SINGLE-SESSION, straight-line fragment (each party sequential send/recv/end on its one endpoint; no intra-party parallelism, sub-session nesting, free channels, or choice — richer structure stays with the open proc calculus, whose R-Comm case is sr_comm). Witness wf_preserved_pingpong instantiates it end-to-end. |
Session-π session fidelity + progress / deadlock-freedom (session_fidelity, config_progress) |
Coq solo-core/SessionPi.v |
machine-checked (Coq) | S1.2 (2026-06-14). The duet paper's headline SAFETY and LIVENESS theorems for the binary send/recv/end fragment, both real Qed, axiom-free (Print Assumptions closed, CI-guarded). session_fidelity: a communication advances the shared protocol by EXACTLY one sty_step (head action consumed) and the reduct is well-formed at that successor — the reduction follows the session type (refines subject reduction by pinning which protocol the reduct follows). config_progress: a well-formed config is either fully ended (Conf QEnd QEnd) or can step — no stuck/deadlocked state, since duality matches each party's pending action with the other's dual. Still OUT (S1.3+): internal/external choice (select/branch), μ-recursion, structural congruence over the open proc calculus, and multiparty G/projection (the S2 hook). |
Session-π choice (select/branch ⊕/&) — config_subject_reduction / session_fidelity / config_progress extended |
Coq solo-core/SessionPi.v |
machine-checked (Coq) | S1.3a (axis-2 STRUCTURE, 2026-06-14). n-ary, labelled internal/external choice (the paper's ⊕/&{lᵢ:Sᵢ}, formal-system.md:81-88/182), all real Qed, axiom-free (Print Assumptions closed, CI-gated). sty/party gain SSelect/SBranch/QSel/QBra over dedicated mutual inductives sbranch/pbranch (NOT list (nat*_), so dual and psubst_party are well-guarded mutual fixpoints — Coq's guard checker rejects the List.map form). Duality dualises pointwise over the label list preserving labels; pty carries label-coverage premises (via the functional lookups bget/pget), so label-mismatch safety is expressible — a select on an unoffered label is ill-typed. The three S1.1b/S1.2 theorems are extended with the choice cases (sty_step gains SS_Sel+SS_Bra and is now non-deterministic — the chosen label is threaded through fidelity); pty_subst is reproved over the mutual party_mut scheme so its QBra case recurses structurally into branches. Witnesses: a 2-branch {0:end,1:end} choice that is well-formed, steps (CSel), and is deadlock-free. Fence: still TWO-PARTY fused form. Faithfulness note: the panel-flagged binary alternative was rejected — n-ary is required so S2.2's merge (over label sets) is statable. Echo-types audit: NOT-RELEVANT (axis-2 STRUCTURE). |
Session-π structural congruence preserves typing (wt_congr) |
Coq solo-core/SessionPi.v |
machine-checked (Coq) | S1.3c (axis-2 STRUCTURE, 2026-06-14). On the OPEN proc calculus, wt_congr : wt G D P → cong P Q → wt G D Q — structural congruence preserves the linear channel-typing, real Qed, axiom-free (CI-gated). Proved as an iff (wt_congr_iff) so the symmetric closure goes through in one induction. cong = the three par laws P|0≡P, P|Q≡Q|P, (P|Q)|R≡P|(Q|R) (full equivalence). New context-splitting algebra: csplit_comm, csplit_assoc (reassociation — load-bearing), csplit_ended, and wt_absorb_ended (the par-nil engine: ended endpoints thread through the typing derivation to the PNil leaves; by induction on wt). Honest fence: this is typing-PRESERVATION under ≡, NOT subject-reduction-up-to-≡ (no reduction in the statement — the open form lacks closed SR for the S1.1b ν reason). OUT (named, with reasons): ν-extrusion (needs a free-name function fn that does not exist → side-condition unstatable), ν-swap (needs an absent context-permutation lemma), replication *P≡P|*P (no !P constructor → vacuous). Echo-types audit: NOT-RELEVANT (axis-2 STRUCTURE). |
Session-π μ-recursion — type layer (unfold_mu, dual_unfold, guarded) |
Coq solo-core/SessionPi.v |
machine-checked (Coq), PARTIAL | S1.3b-core (axis-2 STRUCTURE, 2026-06-14). The equi-recursive type-layer infrastructure (the S2.2 projection target), all real Qed, axiom-free (CI-gated). sty gains SMu/SVar (de Bruijn); tlift/tsubst (mutual over sty/sbranch) and unfold_mu (μa.s) := s[μa.s/a] — a plain Definition, ONE structural tsubst pass, so it terminates with no fuel/measure even on μa.a. dual passes through SMu/SVar untouched (correct ONLY because recursion variables are unpolarised — fenced). dual_unfold : dual (unfold_mu s) = unfold_mu (dual s) — the projection-duality-of-recursion lemma S2.2 consumes (via dual_tlift/dual_tsubst). guarded — a depth-indexed contractiveness predicate (every SVar referring to an inner μ-binder occurs under a message/choice prefix; carried in WELL-FORMEDNESS, never in typing); witnessed: μa.!Nat.a is guarded, μa.a is not. Equi-recursive (no fold/unfold terms → party/proc/S2 inherit unchanged). DEFERRED — S1.3b-meta: the equi-recursive typing / subject-reduction layer (typing up to unfolding) is NOT mechanised — naive inversion is unprovable under a PT_Unfold rule and needs every inversion lemma rewritten to an up-to-unfolding relation + a PT_Unfold-soundness theorem. No "μ supported / recursive sessions done" claim until S1.3b-meta lands. S2.2 is NOT blocked — it consumes only this type layer. Echo-types audit: NOT-RELEVANT (axis-2 STRUCTURE). |
Session-π duet by projection (projection_duality, projected_config_wf, projected_config_subject_reduction, projected_session_fidelity, projected_config_progress, global_projects_to_dual_channel) |
Coq solo-core/SessionPi.v |
machine-checked (Coq) | S2.0/S2.1 (axis-2 STRUCTURE, 2026-06-14). The duet thesis "duet = ensemble │ 2-party" as a theorem — all real Qed, axiom-free (Print Assumptions closed, dedicated proofs.yml gate). S2.0 adds the multiparty-SHAPED global-type layer gty (message-passing + end), the three-case projection proj G r (sender ! / receiver ? / uninvolved passthrough — faithful to formal-system.md:250-252; role := nat so the uninvolved branch is syntactically reachable), and the two-party restriction two_party p q G; witnesses gpingpong/g3 project by reflexivity (the 3-party g3 fires all three projection branches on one term and is provably not two_party 0 1). S2.1 is the collapse + bridge: projection_duality — for a two-party choreography proj G p = dual (proj G q), i.e. projection yields DUAL binary local types (the p≠q side-condition is load-bearing: at p=q the theorem is FALSE, a self-send projects to SSend whose dual is SRecv); projected_config_wf + the corollaries projected_config_subject_reduction / projected_session_fidelity / projected_config_progress (and the round-trip global_projects_to_dual_channel) transport the WHOLE S1.1b/S1.2 guarantee across projection — a config built from the two role-projections is well-formed BY CONSTRUCTION and inherits subject reduction, session fidelity, and progress/deadlock-freedom; projected_pingpong_deadlock_free is a one-line instance. Honest fence: message-passing + end ONLY — the syntax is multiparty-shaped but every theorem's two_party hypothesis collapses to a single fixed pair, so this INSTANTIATES the duet thesis on two-party choreographies; it does NOT prove a general n-party → 2-party result, and proj is total only because there is no choice (no merge / no coherence / no projectability predicate exists or is needed). OUT (deferred): choice global types p→q:{lᵢ:Gᵢ} (S2.2), μ-recursion (S2.2), n≥3 coherence / merge / projection-existence (S3 — the boundary where "duet" stops and "ensemble" begins). Echo-types audit: NOT-RELEVANT (axis-2 STRUCTURE — projection emits no obligation/residue/attestation; re-checked for the multiparty-syntax layer). |
Session-π choice + recursion by projection (merge/merge_idem, partial proj, option-form projection_duality, proj_q_dual_p_some) |
Coq solo-core/SessionPi.v |
machine-checked (Coq), PARTIAL | S2.2 (axis-2 STRUCTURE, 2026-06-14). Global types gain labelled choice GBra p→q:{lᵢ:Gᵢ} (over a dedicated mutual gbranch, NOT list — the S1.3a guard-checker lesson) and equi-recursive GMu/GVar (de Bruijn aligned with the S1.3b local SMu/SVar); projection becomes PARTIAL — proj : gty → role → option sty, three-way mutual proj/proj_br/proj_uninv — sender→SSelect, receiver→SBranch, uninvolved→merge of the branches. merge (+ keystone merge_idem : merge s s = Some s, via the mutual sty_mut scheme) is the combinator that makes an uninvolved role's projection DEFINED exactly when the branches AGREE. projection_duality is reproved in option-map form proj G p = option_map dual (proj G q) over the two-party fragment via the mutual two_party_mut scheme (the GBra case needs the per-branch motive proj_br p = option_map dual_br (proj_br q)); the S2.0/S2.1 bridge + all four corollaries are rethreaded through proj … = Some _ (single helper proj_q_dual_p_some). All real Qed, axiom-free (dedicated proofs.yml S2.2 gate). Witnesses: choice (gchoice2) and recursive (grec = μX.0→1:Nat.X) choreographies project to dual select/branch and dual μ-types (gchoice2_dual/grec_dual via projection_duality); partial projection is witnessed in BOTH directions (uninvolved AGREE→Some, DISAGREE→None), incl. the tail-conflict regression proj_tail_conflict_none that locks the design-panel-found None-erasure bug (a tail merge-conflict must be None, not silently Some SEnd), an unprojectable-body→None, and merge's two failure modes (payload / constructor mismatch). Honest fences: (1) merge is the plain / identity-MEET merge (= equality on the message fragment; only branch continuations meet pointwise under identical labels) — NOT the full label-set-UNION merge of Honda-Yoshida-Carbone, deferred to S3; (2) GMu projection is UNPRUNED — a non-participating role yields the non-contractive μX.X (rejected by guarded/not_guarded_muvar), arising only OUTSIDE the two_party {p,q} collapse (non-theorematic), never displayed as a role's type; (3) NO global-level metatheory — subject reduction / fidelity / progress are NOT re-proved for GBra/GMu; the duet-collapse bridge transports the BINARY metatheory only where both projections are Some; (4) dual_unfold is NOT consumed (the GMu duality case uses only structural dual(SMu x)=SMu(dual x)). DEFERRED → S3: n≥3 coherence / full-UNION merge / projection-EXISTENCE. Echo-types audit: NOT-RELEVANT (axis-2 STRUCTURE — projection/merge emit no obligation/residue/attestation; re-checked for the choice+recursion layer). |
Session-π n-party projection totality (projectable_wf, projection_total) |
Coq solo-core/SessionPi.v |
machine-checked (Coq), PARTIAL | S3a (axis-2 STRUCTURE, 2026-06-14). The FIRST theorem quantifying over a genuine n≥3 role space, breaking the standing fence that no prior theorem quantified over a real n-party system — all real Qed, axiom-free (Print Assumptions closed, dedicated proofs.yml S3a gate). Keystone projection_total : projectable_wf G → ∀ r:role, ∃ s, proj G r = Some s — every role of a well-branched global type projects (the foundational MPST projectability result, restricted to plain-merge), proved over the mutual projectable_wf_mut scheme. projectable_wf (mutual projectable_wf_br) = the restricted projectability predicate: at every GBra it requires p≠q, a non-empty choice (bs≠GBnil), inductive body coherence, and the merge-existence clause (∀ r∉{p,q}, ∃ s, proj_uninv bs r = Some s — every uninvolved role's branches merge under plain merge); μ is permitted (PW_Mu) and handled by the keystone. Design-panel-validated (4 lenses, empirically compiled on Coq 8.18): the panel forced the honest rename (projectable_wf, NOT coherent — it asserts projection EXISTENCE, not safety), the non-empty-choice fix, inductive body coherence, and dropping circular μ-guardedness. Witnesses pin non-vacuity at n=3: a 3-party ring (g_ring = 0→1.1→2.2→0) is projectable_wf, projects on all three roles (g_ring_projects_all via the keystone), and is provably not two_party; an agreeing 3-party choice (g_choice3, uninvolved role 2 active in both branches) projects role 2 via a non-trivial merge (merge_idem); and the plain-merge boundary is witnessed — a same-direction different-payload choice (g_excluded) is a SAFE protocol that full-union merge admits but plain merge rejects (proj … = None, ~ projectable_wf). Honest fences: (1) projectable_wf = every-role-projects, NOT session safety — no n-party subject-reduction / progress / fidelity is proved or implied; (2) the uninvolved merge is plain / identity-meet — choices where an uninvolved role behaves differently across branches are EXCLUDED (the safe MPST pattern admitted by full label-UNION merge — S3c); (3) μ projection stays UNPRUNED (S2.2 fence b) — guardedness-of-projection not imposed; (4) the general two_party p q G → projectable_wf G is NOT proved — and is in fact FALSE (two_party is strictly more permissive: it admits empty choices and μ-divergent branches on which an absent role's unpruned projections fail to merge) — so the n=2 collapse is witnessed BY EXAMPLE (projectable_gpingpong); (5) no n-party config / no operational semantics — static role-assignment tuple = S3b, full-union merge + n-party SR/progress = S3c, both deferred. Echo-types audit: NOT-RELEVANT (axis-2 STRUCTURE). |
Session-π static n-party config (role_assignment, wf_assignment, conf_is_role_assignment2) |
Coq solo-core/SessionPi.v |
machine-checked (Coq) | S3b (axis-2 STRUCTURE, 2026-06-14). The FIRST n-party CONFIGURATION form — a STATIC role→endpoint assignment, NO operational semantics, all real Qed, axiom-free (Print Assumptions closed, dedicated proofs.yml S3b gate). S3a gave projection TOTALITY (the type side is defined on every role); S3b gives the CONTAINER (an assembly of endpoint processes). role_assignment := list (role * party); wf_assignment G ra (a plain Definition over a Prop, In-based — NOT nth/length, NOT a Fixpoint/Inductive, so the S1.3a guard/positivity wall is sidestepped) asserts ONLY that every listed (r,P) is typed at G's projection on r (∀ r P, In (r,P) ra → ∃ s, proj G r = Some s ∧ pty [] P s). The binary Conf/wf_config is recovered as the n=2 INSTANCE by the keystone conf_is_role_assignment2 (from two_party p q G + p≠q + the two entries, build wf_config (Conf P Q) reusing projected_config_wf verbatim — the two destructs yield the SAME sp/sq, duality re-derived internally, no mismatch), with the converse embed role_assignment2_of_conf (binary data → 2-element assignment) and the lookup bridge ra_get/ra_get_in/wf_assignment_get. Non-vacuity at n=3: wf_ra_ring exhibits a genuine 3-party static config over g_ring with concrete closed endpoints (ring_P0/1/2); it is NOT a single Conf — length ra_ring = 3 paired with the existing g_ring_not_two_party (BY EXAMPLE, no over-conditioned theorem). Honesty witnesses lock the soundness boundary: wf_assignment_admits_duplicate_keys (In is duplicate-tolerant → no functionality/config-determined-by-G theorem), and projectable_but_uncoverable (GVar 3 is projectable_wf yet proj (GVar 3) 0 = Some (SVar 3) is uninhabited by any closed party via svar_uninhabited → no general "projectable ⇒ coverable"). Honest fences: (1) wf_assignment = each endpoint typed at its projection, NOT n-party safety — no n-party SR/progress/fidelity/deadlock-freedom, no global coherence; (2) the n=2 recovery is a SLICE (two_party+p≠q required), NOT an n→2 collapse; (3) STATIC — no cstep/no n-party operational metatheory (= S3c); (4) plain (not label-union) merge inherited from S3a — g_excluded-class roles project to None and are silently excluded; (5) μ unpruned (S2.2 fence b); (6) role_assignment is an association LIST (pointwise In-typing, duplicate-tolerant, empty = vacuous, NOT a verified map; no coverage claim). Deferred → S3c: n-party operational semantics, n-party SR/progress/fidelity, full-union merge + coherence. Echo-types audit: NOT-RELEVANT (axis-2 STRUCTURE). |
Session-π full label-union merge (umerge/umerge_br, umerge_idem) |
Coq solo-core/SessionPi.v |
machine-checked (Coq) | S3c.0 (axis-2 STRUCTURE, 2026-06-14). The FIRST S3c sub-rung — the Honda-Yoshida-Carbone label-UNION merge umerge, ADDED ALONGSIDE the plain identity-meet merge (touches nothing S2/S3a/S3b depend on — design-panel-validated, empirically compiled on Coq 8.18, baseline rebuild byte-identical), all real Qed, axiom-free (Print Assumptions closed, dedicated proofs.yml S3c.0 gate). At an external choice (SBranch &) a merged uninvolved role may offer the UNION of the branches' labels (shared labels' continuations recursively umerged via bget/bremove, unshared carried over); the message fragment + the internal choice (SSelect ⊕) require EQUALITY (sty_eqb/sbranch_eqb + sty_eqb_refl) — unioning a sender's own choice is HYC-unsound. Keystone umerge_idem : ∀ s, umerge s s = Some s (unconditional, via the mutual sty_mut scheme; the bremove-threaded encoding makes it hold even on duplicate-divergent label lists — no branch_free fence needed). The WIN is witnessed: a different-label external choice (&{0:end} vs &{1:end}) that plain merge rejects (merge_rejects_disjoint = None) umerge unions to &{0:end,1:end} (umerge_accepts_disjoint, umerge_widens_strictly, umerge_overlap). Honest fences: (1) TYPE-ALGEBRA ONLY — umerge : sty → sty → option sty; it is NOT wired into proj/projectable_wf/cstep (union-projection + coherence = S3c.1); no theorem here quantifies over a gty/role/config. (2) NO coherence/safety — the name umerge claims a defined widening only (deliberately not coherent_merge/safe_merge); n-party safety is earned no earlier than S3c.3. (3) SSelect ⊕ is NOT unioned (equality required — umerge_select_disjoint_rejected); the ⊕/& asymmetry is load-bearing. (4) Does NOT unlock the g_excluded class — that is same-direction different-PAYLOAD message divergence (SRecv VTNat vs SRecv VTBool), which umerge still rejects (umerge_still_rejects_payload_divergence); umerge unions labels, it does not reconcile payloads. (5) only idempotence proved — umerge is not syntactically commutative (label order is argument-order dependent) nor associative; later rungs must reason up to branch-set equality. (6) μ unioned structurally (unpruned, S2.2 fence b inherited). (7) not NoDup-required; non-idempotent uses on duplicate keys need a NoDup side-condition. Remaining S3c sub-rungs (solo): S3c.1 union-projection + coherence predicate, S3c.2 n-ary located config + nstep, S3c.3 message-fragment n-party subject reduction (the first earned n-party safety half), S3c.4 n-party progress (research-hard — fence). Echo-types audit: NOT-RELEVANT (axis-2 STRUCTURE). |
Session-π union-projection (proj_u, projectable_u_wf, projection_total_u, projectable_wf_implies_u) |
Coq solo-core/SessionPi.v |
machine-checked (Coq) | S3c.1 (axis-2 STRUCTURE, 2026-06-14). The SECOND S3c sub-rung — wires the S3c.0 label-union merge into a SEPARATE projection, all real Qed, axiom-free (Print Assumptions closed, dedicated proofs.yml S3c.1 gate; design-panel-validated, 4 lenses empirically compiled on Coq 8.18 — the panel found the keystone and corrected the agreement-lemma structure before any code landed). proj_u/proj_br_u/proj_uninv_u is the plain proj with EXACTLY ONE token changed (the uninvolved fold's merge → umerge), ADDED ALONGSIDE proj — proj/merge/projectable_wf/projection_total and all binary metatheory stay byte-identical (proj is NOT re-pointed at umerge — S3c.0 fence 5; the first 2377 lines verified unchanged). projectable_u_wf (mutual projectable_u_wf_br) is the union analogue of projectable_wf (its PWu_Bra merge-existence clause refers to proj_uninv_u). Keystone existence theorem projection_total_u : projectable_u_wf G → ∀ r:role, ∃ s, proj_u G r = Some s — proved over the mutual projectable_u_wf_mut scheme, the SAME proof as projection_total with _u renames; umerge's partiality is never inspected because the merge-existence is supplied by the PWu_Bra hypothesis. The monotonicity bridge projectable_wf_implies_u : projectable_wf G → projectable_u_wf G (every plain-projectable global type is union-projectable) rides on the keystone lemma merge_forces_eq : merge s₁ s₂ = Some s → s₁ = s₂ (plain merge is the identity-meet — exactly the invariant already asserted in the merge fence comment, here proved via sty_mut) through the agreement lemmas proj_agrees_u (gty_mut, single-output — gbranch transfers carried in the P0 motive) and proj_uninv_agrees_u; the two projections coincide on the plain-projectable subset. Non-vacuity g_union3 (uninvolved role 2 sees &{3:end} in outer-branch 0 vs &{4:end} in outer-branch 1 — DIFFERENT labels, same external-choice direction) is genuinely in union-projectable minus plain-projectable: proj g_union3 2 = None ∧ ~projectable_wf g_union3 (plain merge rejects) but proj_u g_union3 2 = Some &{3:end,4:end} ∧ projectable_u_wf g_union3 (umerge unions). Honest fences: (1) EXISTENCE not SAFETY — projection_total_u asserts only that every role projects; no n-party subject-reduction / progress / fidelity / deadlock-freedom / coherence (identical fence to projection_total; safety earned no earlier than S3c.3); (2) TYPE-ALGEBRA / PROJECTION ONLY — strictly ADDITIVE, no operational metatheory, proj NOT re-pointed; (3) umerge unions LABELS not PAYLOADS — the different-payload class is STILL rejected (proj_u g_excluded 2 = None, proj_u g_excluded_u 2 = None, ~projectable_u_wf g_excluded_u); (4) SSelect ⊕ asymmetry inherited (internal choice NOT unioned); (5) proj_u order-dependent, idempotent only (no canonicity claim); (6) monotonicity is DOMAIN-INCLUSION, not behavioural refinement — one-directional (converse FALSE via g_union3), provable-cheap ONLY because this merge is positional-same-label (regression pin on merge_forces_eq: a future reordering/widening merge breaks the bridge — the existence theorems survive); (7) μ unpruned, p≠q a hypothesis (inherited). Remaining S3c (solo): S3c.2 n-ary located config + nstep, S3c.3 message-fragment n-party subject reduction, S3c.4 n-party progress (research-hard — fence). Echo-types audit: NOT-RELEVANT (axis-2 STRUCTURE). |
Session-π n-ary located operational semantics (nstep/gstep, ra_set, wf_assignment_f, nstep_breaks_wf_at_fixed_G) |
Coq solo-core/SessionPi.v |
machine-checked (Coq) | S3c.2 (axis-2 STRUCTURE, 2026-06-14). The THIRD S3c sub-rung and the FIRST operational metatheory over an n-party config (S3a/S3b/S3c.1 were all type-side / static), all real Qed, axiom-free (Print Assumptions closed, dedicated proofs.yml S3c.2 gate; built solo — empirically compiled on Coq 8.18 on a scratch copy, all 11 names verified). A located reduction nstep : role_assignment → role_assignment → Prop = the located mirror of the fused binary cstep: one synchronous communication between two distinct roles ra_set-updates exactly those two endpoints (NStep_Comm message + NStep_Sel select), every other role untouched. Because p is universally quantified, cstep's fixed-left/right CStepR/CSelR are subsumed (no mirror rules needed). Supporting machinery: the functional pointwise update ra_set (first-match, with ra_set_get_eq/ra_set_get_neq/ra_set_length), a global-type reduction gstep (message fragment) + closures nstar/gstar, and the functional well-formedness wf_assignment_f (the ra_get-based form S3c.3's SR will be stated against; wf_assignment_to_f : wf_assignment G ra → wf_assignment_f G ra — one direction, the converse needs NoDup — so S3b's wf_ra_ring transfers as wf_ra_ring_f). Adequacy witnessed on BOTH sides: the 3-party ring runs 0→1→2→0 to all-QEnd — ring_runs_to_end : nstar ra_ring ra_ring3 (three NStep_Comm) and g_ring_gsteps : gstar g_ring GEnd; nstep_length/nstar_length give the structural-adequacy fact that communication preserves the role count (no role created/destroyed). The load-bearing honesty witness nstep_breaks_wf_at_fixed_G PROVES nstep does NOT preserve wf_assignment_f at a fixed G (after one step role 0 is a receiver QRecv QEnd, while proj g_ring 0 is a send type — the endpoint is typed at proj of the STEPPED g, not of g_ring) — this is exactly why n-party subject reduction (S3c.3) must be stated against a stepping G, and why wf_assignment ra → deadlock-free is false. Honest fences: (1) OPERATIONAL ADEQUACY ONLY — nstep/gstep defined + the ring run witnessed; NO subject reduction (the refutation above is proved), NO progress / deadlock-freedom (the ring run is by example, = S3c.4); (2) nstep/gstep not yet coupled — no gstep↔nstep simulation / fidelity (= S3c.3); (3) message + select fragments only (gstep = message only; choice-gstep = S3c.3-choice); (4) ra_set first-match (duplicate-tolerant like ra_get; only the first entry updates); (5) wf_assignment_f STATIC typed-at-projection, NOT n-party safety; (6) uses plain proj (NOT proj_u) — the located semantics is independent of the S3c.1 widening; plain merge + unpruned μ + p≠q-as-hypothesis inherited. Remaining S3c (solo): S3c.3 message-fragment n-party SR (coupled gstep/nstep vs a stepping G — first earned n-party safety half), S3c.3-choice, S3c.4 n-party progress (research-hard — fence). Echo-types audit: NOT-RELEVANT (axis-2 STRUCTURE). |
Session-π head-coupled message subject reduction (nstep_sr_msg_head, nstep_gstep_sr_msg_head, sr_earns_safety_across_step, runahead_breaks_head_coupling) |
Coq solo-core/SessionPi.v |
machine-checked (Coq) | S3c.3-msg (axis-2 STRUCTURE, 2026-06-14). The FOURTH S3c sub-rung and the first EARNED n-party safety half, all real Qed, axiom-free (Print Assumptions closed, dedicated proofs.yml S3c.3-msg gate). Design-panel-validated + independently adversary-verified (4 design lenses empirically compiled on Coq 8.18 → coq-mechanic build → a SEPARATE adversary that re-instantiated the premises at the ring, re-derived the payload coupling, and compiled its own run-ahead refutation; verdict sound-and-honest, land as-is). S3c.2 proved nstep does not preserve wf_assignment_f at a fixed G (nstep_breaks_wf_at_fixed_G); S3c.3-msg proves the TRUE statement — the head communication sanctioned by a head GMsg p q t G' carries wf from G to its continuation G': nstep_sr_msg_head : p≠q → wf_assignment_f (GMsg p q t G') ra → ra_get ra p = Some (QSend v P) → ra_get ra q = Some (QRecv Q) → wf_assignment_f G' (ra_set (ra_set ra p P) q (open_party v Q)). Proved by a 3-way located role case-split (sender p via ra_set_get_eq + pty_send_inv; receiver q via pty_recv_inv + pty_subst0; uninvolved r via the definitional proj (GMsg p q t G') r = proj G' r). The coupling: the SAME value v at the SAME payload type t the sender ships (vtype [] v t from pty_send_inv, forced equal to the head GMsg's t) is what the receiver substitutes — payload soundness is genuine, not assumed. The firing pair is structurally pinned to G's head by stating wf at GMsg p q t G' (no separate is-head hypothesis). The coupled corollary nstep_gstep_sr_msg_head packages gstep+nstep+wf' in one conclusion for the head step. Earned-safety headline: the SAME ra_ring1 that S3c.2's nstep_breaks_wf_at_fixed_G refuted at the fixed g_ring is wf at the stepped g_ring (g_ring_stepped := GMsg 1 2 VTNat (GMsg 2 0 VTNat GEnd)) — ra_ring1_wf_at_stepped_g (proved through the core SR, not re-derived), sealed by sr_earns_safety_across_step (¬ wf g_ring ra_ring1 ∧ wf g_ring_stepped ra_ring1 ∧ gstep g_ring g_ring_stepped); proj_stepped_0 shows role 0 flips SEND→RECV across the step, exactly why the previously-ill-typed QRecv becomes well-typed. The run-ahead fence is SELF-WITNESSED (runahead_breaks_head_coupling, boundary-by-example like g_excluded): on g_runahead := GMsg 0 1 VTNat (GMsg 2 3 VTNat GEnd) a non-head (2→3) nstep fires from a wf config yet its post-state is not wf at the head continuation — so head-coupled SR genuinely cannot cover run-ahead. Honest fences: (1) HEAD communication only — run-ahead / permutation needs a gstep-with-swap relation (S3c.3-perm), a strictly bigger asynchronous theory; (2) MESSAGE fragment only — select/branch SR = S3c.3-choice; (3) the coupled corollary is a head wrapper, NOT general/unrestricted SR (FALSE for run-ahead), NOT a bisimulation / multi-step fidelity; (4) functional wf_assignment_f (first-match ra_get); (5) plain proj (not proj_u), unpruned μ, p≠q-as-hypothesis inherited; (6) PRESERVATION only — NO progress / deadlock-freedom / fidelity (S3c.4+). Naming deliberately avoids the M1/S3a overclaim trap (_msg_head, not n_party_safety). Remaining S3c (solo): S3c.3-choice (select/branch SR), S3c.3-perm (run-ahead), S3c.4 n-party progress (research-hard — fence). Echo-types audit: NOT-RELEVANT (axis-2 STRUCTURE). |
Session-π head-coupled select/branch subject reduction (nstep_sr_choice_head, nstep_gstep_sr_choice_head, gbget/GStep_Bra, proj_br_selected, proj_uninv_selected) |
Coq solo-core/SessionPi.v |
machine-checked (Coq) | S3c.3-choice (axis-2 STRUCTURE, 2026-06-15). The FIFTH S3c sub-rung — the CHOICE analogue of S3c.3-msg, all real Qed, axiom-free (Print Assumptions closed, dedicated proofs.yml S3c.3-choice gate). Design-panel-validated + independently adversary-verified (3 design lenses → coq-mechanic clean from-scratch rebuild on Coq 8.18 → a SEPARATE adversary that recompiled all 11 modules, re-instantiated at a fresh 4-role label-1 choreography exercising the recursive arms, and ran run-ahead + disagreeing-branch break attempts; verdict sound-and-honest, land as-is). The head select/branch sanctioned by a head GBra p q {lᵢ:Gᵢ} carries wf from G to its selected branch continuation Gl = gbget l bs: nstep_sr_choice_head : p≠q → gbget l bs = Some Gl → wf_assignment_f (GBra p q bs) ra → ra_get ra p = Some (QSel l P) → ra_get ra q = Some (QBra bsP) → pget l bsP = Some Q → wf_assignment_f Gl (ra_set (ra_set ra p P) q Q). Proved by the SAME 3-way located role case-split as the message head (selector p via ra_set_get_eq + pty_sel_inv; offerer q via pty_bra_inv + the per-label coverage Hcov; uninvolved r). The label l drives BOTH the new global step (GStep_Bra on the new functional gbranch lookup gbget — no such lookup pre-existed; only proj_br/proj_uninv consumed gbranch) and the located NStep_Sel onto the SAME Gl. The genuinely-new part vs the message head: the uninvolved arm is no longer definitional — it rides proj_uninv (the plain-merge fold over all branches) and is discharged by the new proj_uninv_selected via merge_forces_eq (plain merge is the IDENTITY-MEET, so every branch projects an uninvolved r to the SAME type, hence so does the selected Gl; the ≥2-branch case uses an explicit one-level unfold to avoid cbn [proj_uninv] over-unfolding). The coupled corollary nstep_gstep_sr_choice_head packages gstep+nstep+wf' for the head step. Non-vacuity: choice3_head_fires_end_to_end fires the rung end-to-end on the agreeing 3-party choice g_choice3 (+ wf_ra_choice3). Honest fences: (1) HEAD choice only — run-ahead/non-head selection = S3c.3-perm (a non-head has no matching head GStep_Bra); (2) PLAIN proj (not proj_u) — the uninvolved arm leans on merge_forces_eq=identity-meet; the label-UNION merge is S3 (regression pin: widening merge breaks proj_uninv_selected and this theorem becomes false-as-stated — that IS the S3 fence); (3) coupled corollary is a head wrapper for ONE step, NOT general SR/bisimulation; (4) p≠q-as-hypothesis + functional wf_assignment_f inherited; (5) PRESERVATION only — NO progress (S3c.4). Naming avoids the overclaim trap (_choice_head, not n_party_safety). Strictly ADDITIVE (bytes 1-2868 SHA-identical to baseline; sole prior-region edit = the gbget fixpoint + the GStep_Bra constructor on the gstep Inductive). Remaining S3c (solo): S3c.3-perm (run-ahead), S3c.4 n-party progress (research-hard — fence). Echo-types audit: NOT-RELEVANT (axis-2 STRUCTURE). |
| Solo syntax / contexts / typing | Idris2 + Coq solo-core/ |
definitions-only | de Bruijn terms, QTT context split/scale/zero, context-splitting typing judgement. |
progress |
Coq solo-core/SoloCore |
machine-checked | Theorem progress : Progress. real Qed, axiom-free. Phase F1.3. CI: proofs.yml compiles it + asserts Print Assumptions closed. |
progress |
Idris2 solo-core/Soundness |
locally-checked | Hole-free total function (no ?todo_progress); accepted by idris2, package built in CI (proofs.yml). Phase F1.3. Re-proven over the SEPARATED context (Tctx/Uvec) + both products (TWith/TTensor, LetPair) in the 2026-06-15 F1.4 design migration — closed-term inversions now massage only the usage vector (uaddEmpty/uscaleEmpty), since the shared type context stays TEmpty automatically; :total progress confirms totality. |
preservation |
Coq solo-core/SoloCore |
machine-checked | Theorem preservation : Preservation., real Qed, axiom-free, via the open-context QTT substitution lemma ht_subst. Phase F1.4. CI: proofs.yml compiles it + asserts Print Assumptions closed (and likewise affine_pres). |
preservation |
Idris2 solo-core/Soundness |
locally-checked | DISCHARGED 2026-06-21 (#108). preservation : (t : Tm) -> Has g d t a -> Step t t' -> Has g d t' a is a total, hole-free function by induction on Step — :total preservation confirms; %default total, no postulate/believe_me/assert_total/?hole. Mirrors the Coq twin preservation: the β/projection/elimination cases consume the QTT substitution lemmas from Substitution.idr — substLemma0 (App/Case/Let single-variable) and subst2Lemma (LetPair two-variable) — realigning the residual usage with d via uadd commutativity/associativity (uaddAssoc) and uscale One; congruence cases recurse structurally. Stated over the CORRECT design (separated context + genuine products) that made the same-usage statement sound (issue #93). The reduct term t is taken explicitly (relevant), exactly as progress does, because Idris erases the derivation's term/type indices while the substitution lemmas compute on the bound body + substituted value. affinePreservation follows as the Solo-kernel corollary (:total too). Supporting chain in Substitution.idr (all total, hole-free): append-context algebra, shape invariant (shapeVar/shapeType), hvShift/htShift, the accounting algebra (qReassoc/vecReassoc/substReassocAdd/substReassocMult/usplit3/uaddSplitBoundary2/uaddAssoc), hvSubst, the FULL htSubst (all 15 cases), substLemma0, subst2Lemma. The b-index-erasure obstruction (ADR-003) is resolved by carrying b erased. idris2 --build solo-core.ipkg exits 0; the solo core is now HOLE-FREE. CI: proofs.yml Idris job. |
Small-step step |
Coq solo-core/SoloCore |
definitions-only | CBV left-to-right relation, all redex + congruence constructors. Committed in F1.1. |
Functional evaluator step1 (sound+complete vs step) |
Coq solo-core/Eval |
machine-checked | 2026-06-21. Eval.v: step1 : tm -> option tm with step1_sound/step1_complete (step1 t = Some t' ↔ step t t'), real Qed, axiom-free, in _CoqProject (CI-gated). The executable mirror of the step relation; extracted (Extract.v) to couple the Rust evaluator my_qtt::step1 (interpreter coupling #2). |
Functional session stepper cstep1 (sound+complete vs cstep) |
Coq solo-core/SessionEval |
machine-checked | 2026-06-21. SessionEval.v: cstep1 : config -> option config (binary fused config) with cstep1_sound/cstep1_complete (cstep1 c = Some c' ↔ cstep c c'), real Qed, axiom-free, in _CoqProject (CI-gated). The executable mirror of the cstep relation; extracted to couple the Rust session runtime my_qtt::session::cstep1 (session coupling #4). |
Functional global stepper gstep1 (sound+progress vs gstep) |
Coq solo-core/SessionEval |
machine-checked | 2026-06-21. gstep1 : gty -> option gty with gstep1_sound + gstep1_complete (progress: gstep G G' -> ∃ G'', gstep1 G = Some G''), real Qed, axiom-free. Progress not determinism — gstep is nondeterministic at GBra. Extracted to couple my_qtt::session::gstep1. |
Functional n-ary stepper nstep1 (sound+progress vs nstep) |
Coq solo-core/SessionEval |
machine-checked | 2026-06-21. nstep1 : role_assignment -> option role_assignment (first communicating pair) with nstep1_sound + nstep1_complete (progress), real Qed, axiom-free. The pairing search (find_recv/find_bra) re-fetches parties through ra_get, so duplicate role entries never act on a stale party; soundness via per-search inversion lemmas, progress via the dual membership lemmas. Extracted to couple my_qtt::session::nstep1. |
Small-step Step |
Idris2 solo-core/Soundness |
definitions-only | CBV left-to-right relation, both products: additive SFst/SSnd fire on With values, multiplicative SLetPair fires on a Tensor value via subst2; plus the echo residue rules (SWeaken). Consumed by the verified progress. Migrated 2026-06-15. |
| General core typing + substitution | Coq coq/Typing.v |
locally-checked | Pre-existing: 9 Qed, 0 Admitted. Non-quantitative; substitution lemma proved. |
Echo residue-measure SEAM (RESIDUE_MEASURE, EchoTraceTropical, echo_measure_not_injective) |
Coq solo-core/ResourceAlgebra.v + EchoMeasure.v |
machine-checked (Coq) | E4 SEAM — Coq mirror (axis-3 ECHO, 2026-06-14). The my-lang half of the joint seam capstone ("interaction, not identification, is a theorem"), all real Qed, axiom-free (Print Assumptions closed, dedicated proofs.yml E4 gate). The former PENDING prose sketch in ResourceAlgebra.v is now the real Module Type RESIDUE_MEASURE (S : SEMIRING) — measure : Residue → S.Q with measure_empty/measure_combine (a monoid homomorphism (Residue,combine,empty) → (S.Q,qmul,one), needing only the DONE R2 SEMIRING) — a faithful mirror of the upstream tropical-resource-typing Resource/EchoBridge.lean structure ResidueMeasure. EchoMeasure.v inhabits it at the DONE R4 Tropical cost carrier (EchoTraceTropical: a residue is an echo reindexing trace, measure = accumulated Affine-collapse cost = tropical Fin), and witnesses measure-independence on the Coq side via echo_measure_not_injective ([Affine] and [Linear;Affine] both cost Fin 1 → the measure cannot reconstruct the residue). Echo-types audit: RELEVANT (axis-3 ECHO) — the audit confirmed the seam is already mechanised upstream on both foundations (echo-types Echo/Measure/Interface.agda ResidueMeasure + Separation/NotResourceInstance.agda equal-measure-does-not-imply-equal-echo, --safe --without-K); per the audit directive the Coq side reuses rather than re-derives. Honest fences: (1) the Coq mirror carries the measure HOMOMORPHISM + residue-level non-injectivity; the full measure-independence over the degrade-compose modality (the ECHO_MODALITY act transport, sketch (b)) is upstream-CITED, not re-derived — hence the ladder marks E4 ◑ (Coq mirror ✓, full seam upstream); (2) hard IS-NOT invariant kept — Echo is NOT a resource/SEMIRING instance, measure is a one-directional E→R lossy decoration, and EchoMode.v/EchoResidue.v stay Quantity-independent; (3) the trace carrier is the free residue monoid (the minimal composition skeleton), not a claim to BE the full echo residue object. |
| Area | Status | Location |
|---|---|---|
| Type-system soundness | proved-on-paper | proofs/shared/type-system/soundness.md |
| Type-system metatheory / inference / subtyping | proved-on-paper | proofs/shared/type-system/ |
| Effect-system soundness | proved-on-paper | proofs/shared/effect-system/soundness.md |
| Memory model / ownership | proved-on-paper | proofs/shared/memory-model/ownership.md |
| Operational & denotational semantics | proved-on-paper | proofs/shared/{operational,denotational}-semantics/ |
| Solo affine types | proved-on-paper | proofs/solo/affine-types/formal-system.md |
| Duet session types | proved-on-paper | proofs/duet/session-types/formal-system.md |
| Ensemble agent calculus | proved-on-paper | proofs/ensemble/agent-calculus/ |
| AI semantics | proved-on-paper | proofs/shared/ai-semantics/ |
| Topic AS has | my-lang status | Plan phase |
|---|---|---|
| Mechanised QTT solo-core | commenced (this PR) | F1 |
| Mechanised progress/preservation | Coq machine-checked (axiom-free Qed, CI-guarded); Idris twin locally-checked (both total + hole-free; preservation #108 discharged 2026-06-21) |
F1.3 / F1.4 |
| Algorithmic typing / decidable typecheck (static-split ≡ usage-walk) | Coq machine-checked (check_correct, axiom-free) — overtakes AS (states it as prose "future work" only) |
F1.4 |
Surface→core elaboration correctness (me → solo) |
Coq machine-checked (me_wt_sound over the WHOLE me_tm + elab_data_check, axiom-free, M1.1/M1.1b — M1 complete) — overtakes AS (solo-only; no me-like dialect, nothing analogous as surveyed (AS@main 2026-06-02)) |
M1 |
| Quantitative-types (dedicated doc) | folded into solo affine doc | F4 |
| Row-polymorphism proof | absent | F4 |
| Dependent/refinement types proof | absent | F4 |
| Axiomatic (Hoare) semantics | absent | F4 |
| Categorical semantics | absent | F4 |
| Complexity analysis | absent | F4 |
| Proof CI leg | present — proofs.yml machine-checks both tracks (coqc + idris2 --build); overtakes AS |
F5 |
The mechanised cores above are the spec; the Rust toolchain
(crates/my-lang) is a separate, conventional AI-first implementation. The
coupling method adopted here is differential conformance against the
Coq-extracted verified artifact (extract the verified function to OCaml,
then assert the Rust implementation agrees on a random corpus) — the honest,
reproducible alternative to an infeasible full Rust-in-Coq refinement proof.
Couplings #1 (checker), #2 (evaluator vs step), #3 (echo
modality), and #4 (session runtime vs cstep) are closed by this
method (below). Where the spec is a relation (step, cstep), a functional
mirror (step1, cstep1) is first proved sound+complete vs the relation
(Eval.v, SessionEval.v — machine-checked, axiom-free), then the Rust port
is conformance-tested against the extracted mirror. One harness
(conformance/run.sh) drives all of them: 60 000 results across 5 seeds
agree (3000 cases × {check, one-step, normal-form, session-step}). #5 is
deliberately by-design (Me is a runtime projector, not a static dialect —
see the top-level pedagogy note), so it is not a gap. (Audit: 2026-06-21,
verified against the crate sources + the conformance harness.)
| Obligation | Status | Note |
|---|---|---|
Rust affine checker refines Coq check / aff_type_dec (R5/R5b) |
conformance-checked | CLOSED by differential conformance 2026-06-21. The verified Coq check (R5) is extracted to OCaml (proofs/verification/coq/solo-core/Extract.v, Separate Extraction check) and used as an independent ORACLE; the Rust port crates/my-qtt is the implementation under test. conformance/run.sh generates a random corpus of (ctx, tm) queries (crates/my-qtt/src/bin/conformance_gen.rs), runs BOTH the extracted verified check (conformance/oracle.ml) and my_qtt::check, and asserts byte-identical results — same accept/reject, same synthesized type, same usage vector — including echo (MkEcho/Weaken/TEcho) terms. 25 000 random terms across 5 seeds agree (≈13% accept / 87% reject, so both branches are exercised). my_qtt::aff_check mirrors the Coq aff_type_iff (check … = Some(a,D0) ∧ ule D0 budget) and carries the R5/R5b reflexivity oracle tests. SCOPE/honesty: this is differential refinement-by-conformance against the extracted verified algorithm, NOT a full Rust-in-Coq refinement proof; and the main crates/my-lang/src/checker.rs (Hindley) now CALLS the verified core by default for #[safe] functions (Checker::check_qtt_safe_fn → qtt_bridge → my_qtt::check; a dropped/duplicated binder in the resource fragment is a CheckError::ResourceViolation, out-of-fragment bodies skip). So the resource axis is enforced-by-default where opted in via #[safe] (the docs/STATUS.adoc "make the resource axis the default" item — DONE); whole-program linear-by-default is intentionally NOT the design (my-lang is not a linear language). |
Evaluator refines Coq step (solo core) |
conformance-checked | CLOSED 2026-06-21. The reference semantics is the step RELATION (not extractable), so Eval.v adds a FUNCTIONAL step1 : tm -> option tm and proves it both ways vs the relation — step1_sound : step1 t = Some t' -> step t t' and step1_complete : step t t' -> step1 t = Some t' — real Qed, axiom-free (Print Assumptions closed), machine-checked in CI (Eval.v is in _CoqProject). step1 is extracted alongside check (Extract.v) and the Rust port my_qtt::step1 (faithful shift/subst_at/subst0/subst2/is_value/step1) is differentially conformance-tested against it: conformance/run.sh compares one-step results AND iterated normal forms (cap 64) over a random + closed-redex corpus. 45 000 results across 5 seeds agree (3000 terms × {check, one-step, normal-form}); the normal-form pass cross-checks the Rust substitution against Coq's extracted subst. SCOPE/honesty: this couples an evaluator over the SHARED solo tm (the same approach as the checker), exactly mirroring step; the separate AI-surface interpreter.rs (richer term language, runtime no-ops for Restrict/Ref/RefMut) is NOT what is coupled here and remains an independent, unverified frontend. |
| Echo modality wired into surface + checker | conformance-checked (verified-core surface) | 2026-06-21. Echo is wired end-to-end through the VERIFIED core: the my_qtt::surface fragment has echo intro (SExpr::Echo / STy::Echo) and the weaken elimination (SExpr::Weaken), elaborate lowers them to Tm::MkEcho/Tm::Weaken, and the machine-checked check consumes them — so the linear ⊑ affine discipline (EchoLinear) is enforced from a surface term by the proof. Pinned by surface.rs tests: intro types correctly, a LINEAR echo weakens to AFFINE, weakening an AFFINE echo is REJECTED (the one-way no-section fact), and witness linearity is threaded (an echo whose witness drops a linear binder is rejected). Echo terms are also in the random differential-conformance corpus (#1/#2), so my_qtt's echo handling matches the extracted Coq check/step1. SCOPE/honesty: this closes echo on the verified-core-facing surface; the conventional compiler (crates/my-lang ast::Expr/parser) still has no echo SYNTAX (so qtt_bridge cannot yet lower a compiler-AST echo — that needs a type-annotated echo grammar, a frontend follow-on like the Param quantity syntax). types.rs EchoMode is no longer inert at the verified boundary; it is in the conventional frontend. |
Session runtime refining cstep / nstep / gstep (all three layers) |
conformance-checked | 2026-06-21. SessionEval.v adds a functional stepper for each layer of the session metatheory and proves it adequate vs the reference RELATION, all real Qed, axiom-free, in _CoqProject (CI-gated): (1) binary cstep1 : config -> option config — SOUND + COMPLETE vs cstep; (2) global gstep1 : gty -> option gty — SOUND + PROGRESS vs gstep (gstep1_sound + gstep1_complete, the progress form because gstep is nondeterministic at GBra); (3) n-ary located nstep1 : role_assignment -> option role_assignment — SOUND + PROGRESS vs nstep (nstep1_sound + nstep1_complete; nstep1 scans for the first communicating pair via find_recv/find_bra, parties always re-fetched through ra_get). All three are extracted (Extract.v) and the Rust runtime my_qtt::session (faithful val/party/config/gty/role_assignment + the substitution/lookup chain + cstep1/gstep1/nstep1) is differentially conformance-tested against them (conformance/run.sh, (cstep …)/(gstep …)/(nstep …) queries) — 90 000 results across 5 seeds agree (6 query classes × 3000 cases × 5 seeds). SCOPE/honesty: for the two NONDETERMINISTIC relations the functional stepper commits to a deterministic strategy (first branch / first pair), so adequacy is soundness + progress (step1 = None iff the relation is stuck), NOT functional determinism — the honest statement for a nondeterministic reduction. The AI-surface interpreter.rs (Go/Await collapse to sequential) is a separate unverified frontend. |
Concrete me surface exercising the M1 elaboration |
by-design — not a gap | Affirmed 2026-06-21. This is a deliberate architectural decision, NOT an omission: Me is an on-the-fly agent-generated runtime projection over the Solo ⊂ Duet ⊂ Ensemble dialect hierarchy, not a static fourth dialect — two attempts to build it as a static compiler were retired (hyperpolymath/me-dialect archived; in-tree dialects/me/ sidelined to _exploratory/me-scaffolding/SIDELINED.adoc). The elaboration coupling that DOES matter is already machine-checked: M1 (me_wt_sound) proves me -> solo adequacy over the abstract Coq me_tm, axiom-free. Building a concrete static me grammar to "close" this row would CONTRADICT the architecture, so it is intentionally not built. No further action. |
These do not diminish the mechanised results — they fence the boundary between proved (the four-axis core) and implemented (the AI-first Rust frontend), which today are two disconnected universes.
Change this registry in the same PR as any proof change. When an
Admitted/?todo becomes a real proof, move the row from
statement-only to locally-checked, and to machine-checked once
the F5 CI leg verifies it.