diff --git a/ARCHITECTURE.adoc b/ARCHITECTURE.adoc index 0e96509..79075c1 100644 --- a/ARCHITECTURE.adoc +++ b/ARCHITECTURE.adoc @@ -95,7 +95,7 @@ it is checked as its own root and `All.agda` stays builtins-only. with the distribution's `agda-bin=2.6.4.3-1+b2` and `agda-stdlib=2.1-4`, asserts the prover version, fetches the siblings, and runs `scripts/check.sh` and `scripts/minimal-laws.sh` with -`--safe --without-K --no-libraries --ignore-interfaces --double-check -W error`. +`--safe --without-K --cubical-compatible --no-libraries --ignore-interfaces --double-check -W error`. The documentation integrity workflow is structural only and never evidence that anything is proved. diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc index 7aa701e..5b01e6b 100644 --- a/PROOF-STATUS.adoc +++ b/PROOF-STATUS.adoc @@ -4,7 +4,7 @@ Statuses: PROVEN / TESTED / ASSUMED / DESIGNED / OPEN. Every PROVEN line names the module that discharges it under -`--safe --without-K --no-libraries --ignore-interfaces --double-check -W error` +`--safe --without-K --cubical-compatible --no-libraries --ignore-interfaces --double-check -W error` on Agda 2.6.4.3 (Debian `agda-bin=2.6.4.3-1+b2`), with resource-algebra and epistemic-types on the include path (same kernel; pinned by `scripts/fetch-siblings.sh`) and, for the one module that needs it, @@ -162,6 +162,136 @@ Not claimed: that echo-types' `Grade.agda` is checked by echo-types' own CI (at `da140cc2` no root there imports it; this gate is its only check), and nothing about the direction resource-algebra chooses for its L-2 import. +== Echo-graded projection commuting square (Base/EchoProjection.agda) + +The choreographic analog of echo-types' `choreo-grade-commute`. echo-types' +`RoleGEcho` is a 2D family indexed by Role and Grade: at keep grade it +carries `RoleEcho r true` (a type that genuinely varies with the role); at +residue and forget grades it collapses to `⊤`. `choreo-grade-commute` says +role transport and grade degradation commute — 18 cases, all `refl`, with +one non-trivial case (`c⊑s, keep≤keep`) where both sides compute to +`client-to-server e`, a function between different types. + +The choreographic analog defines two 2D families indexed by Party and +EGrade: one carrying the restricted grade (grade-indexed), the other the +projected local type (local-indexed), both collapsing to `⊤` at residue +and forget grades. The party transport requires the restricted grades +(grade version) or projections (local version) to agree. + +[cols="1,3,1",options="header"] +|=== +| ID | Claim | Status +| EP-1 | `echo-grade-commute`: grade degradation and party transport commute on the grade-indexed 2D family `CGEchoGrade`, for any parties with the same restricted grade. Closes by `refl` in all six cases | PROVEN (`EchoProjection.echo-grade-commute`) +| EP-2 | `echo-local-commute`: grade degradation and party transport commute on the local-type-indexed 2D family `CGEchoLocal`, for any parties with the same projection. Closes by `refl` in all six cases | PROVEN (`EchoProjection.echo-local-commute`) +| EP-3 | Two-event case (`msg 0 1 g₁ (msg 2 3 g₂ end)`): the grade transport exists between sender and receiver of the same message (`same-grade-01`, `same-grade-23`, both `refl`); the local transport exists only between outside parties (`same-proj-45`, `refl`); sender and receiver do NOT have the same projection (`proj-0≢proj-1`). The square is trivial in ALL cases because the transport is the identity on equal values — there is no choreographic analog of `client-to-server` between different projections | PROVEN (`TwoEvent`); the trivialisation is the result +|=== + +What EP-3 says about the keystone: echo-types' commuting square has a +non-trivial case because `RoleEcho Client true` and `RoleEcho Server true` +are different types, and `client-to-server` is a genuine function between +them. The choreographic projection `proj p G` is a value of the fixed type +`Local`, and `grade↾ p G` is a value of the fixed type `Grade`; their +singleton wrappers are contractible, so the only transport between equal +values is the identity. The B-5 open item (role transport) cannot be +closed by this route: the echo-grade commuting square trivialises before +it reaches the transport/warrant structure. + +== K-CUT-WARRANT precise statement (WarrantClaim.agda) + +The warrant component of the keystone, stated as a reviewed theorem +statement with every hypothesis and side condition explicit. Three +components: grade equality (C1, proven from K-CUT-LOSS and frame +factivity), grade bound (C2, proven with a grade-ordering hypothesis +H4), and data warrant (C3, conditional on a receiver-local side +condition H5). The gap between type-determined and data-dependent +warrants is documented precisely: the type provides the warrant +structure and type-determined evidence (Kripke knowledge) but not +data-dependent evidence or soundness. + +epistemic-types' `SoundWarrant` (pinned commit `495db9cc`) is imported, +not re-declared: `Warrant` carries an `Evidence` type; `SoundWarrant` +adds `sound : Evidence → A`. The receiver-local side condition is +exactly the provision of `Evidence` and `sound` for data-dependent +claims. + +[cols="1,3,1",options="header"] +|=== +| ID | Claim | Status +| WC-1 | Grade equality warrant: at every world w, p holds a `SoundWarrant` for `grade↾ p (G ↾ cut w) ≡ grade↾ p (G ↾ cut w)`, with evidence token `knows-own-grade p w`. Hypotheses: H1–H3 only | PROVEN (`Claim.grade-equality-warrant`, `grade-equality-evidence`) +| WC-2 | Grade bound warrant (lower): if `Each (𝟙 ≼_) G`, p holds a `SoundWarrant` for `grade↾ p (G ↾ cut w) ≼ grade (G ↾ cut w)`, with evidence token `knows-lower-bound G p e w`. Hypotheses: H1–H4 | PROVEN (`Claim.grade-bound-warrant-lower`, `grade-bound-evidence-lower`) +| WC-3 | Grade bound warrant (upper): if `Each (_≼ 𝟙) G`, p holds a `SoundWarrant` for `grade (G ↾ cut w) ≼ grade↾ p (G ↾ cut w)`, with evidence token `knows-upper-bound G p e w`. Hypotheses: H1–H4 | PROVEN (`Claim.grade-bound-warrant-upper`, `grade-bound-evidence-upper`) +| WC-4 | Data warrant: for data-dependent φ, p holds a `SoundWarrant` for φ w IF p provides `ReceiverLocalSideCondition p φ w` (Evidence + sound). This is the receiver-local side condition; NOT type-determined | PROVEN as a conditional (`Claim.data-warrant`); the side condition is an external assumption +| WC-5 | Complete K-CUT-WARRANT record: packages C1 and C3; C2 stated separately (direction depends on algebra). `mkComplete` populates from the side condition | PROVEN (`Claim.KCutWarrantComplete`, `mkComplete`) +|=== + +What WC-4 says about the keystone: the pre-registration's "SoundWarrant +at the receiver (ASSUMED local soundness, not type-determined)" applies +to data-dependent claims only (C3). The grade claims (C1, C2) are fully +type-determined: evidence is Kripke knowledge, soundness is frame +factivity, and no external assumption is needed. The gap is precisely +the boundary between what the choreographic type determines (grades, +projections, bounds) and what it does not (payload properties, +authenticity, cryptographic evidence). epistemic-types' +`ProofTransport.CertificateCheck` provides the vocabulary for the +receiver-local side condition but does not derive it from the type. + +== Grading semantics for bounds under interaction (GradingSemantics.agda) + +Defines the grading semantics using the algebraic vocabulary of +tropical-types (Resource/Algebra/Interface.lean, read-only provenance +reference; Dioid.lean, read-only proof witnesses). Keeps grade, +measure, and index distinct. Derives one-step bound propagation +theorems and the projection theorem from the declared semantics. +Records a checked negative result for non-commutative ⊗. + +tropical-types' Lean 4 proof witnesses (canonicalLe partial order, +monotonicity of both operations, ResourceAlgebra.ofIdempotentAdd) are +provenance, not imports. The Agda IsOrdered record carries the local +verification. Bridge obligation M-2 is recorded, not discharged. + +[cols="1,3,1",options="header"] +|=== +| ID | Claim | Status +| GS-1 | One-step bound propagation for messages: if `grade↾ p G ≼ x`, then `grade↾ p (msg s r g G) ≼ at (role p s r) g ⊗ x`. Uses ⊗-monotonicity (tropical-types Dioid.lean `canonicalLe_mul_le_mul_left`, provenance; Agda `IsOrdered.⊗-mono`, local verification) | PROVEN (`bound-step-msg`, `bound-step-msg-outsider`) +| GS-2 | One-step bound propagation for choices: if `grade↾ p G₁ ≼ x₁` and `grade↾ p G₂ ≼ x₂`, then `grade↾ p (choice s r g G₁ G₂) ≼ at (role p s r) g ⊗ (x₁ ⊕ x₂)`. Uses ⊗-monotonicity and ⊕-monotonicity | PROVEN (`bound-step-choice`) +| GS-3 | Two-step bound propagation (composition of GS-1); projection theorem: `restricted-measure p G ≡ local-measure (proj p G)` for projectable types (K-3 restated); bound transfer through projection in both directions | PROVEN (`bound-two-step`, `projection-theorem`, `bound-projection-lower`, `bound-projection-upper`) +| GS-4 | Negative result: the unrestricted measure is NOT compositional under reordering for non-commutative ⊗. Consequence of A-1 (restricted measure is order-independent for disjoint interactions) and A-3 (HWM unrestricted measure is order-dependent). Abstract right-cancellation from `(a ⊗ b) ⊗ grade G ≡ (b ⊗ a) ⊗ grade G` to `a ⊗ b ≡ b ⊗ a` requires ⊗-right-unit or right-cancellation, neither in the base algebra. Concrete witness at HWM (A-3). No postulates introduced | RECORDED (consequence of A-1, A-3; concrete witness `Instances.Diamond.hwm-order-sensitive`) +|=== + +What GS-4 says about the keystone: tropical-types' Interface.lean does +not assume `mul_comm` in the base `ResourceSemiring`; `CommResourceSemiring` +is an optional refinement. The negative result is structural: for any +algebra satisfying the base interface but not the commutative refinement, +the unrestricted measure is order-sensitive while the restricted measure +is not (for disjoint interactions). This is the precise sense in which +"an occupancy reading is not a cost reading" (P-3). + +== Independent₂ and the two-event experiment (Independent2.agda) + +Makes Independent₂ explicit for the two-event K-CUT-LOSS experiment: +disjoint footprints (I1), phase safety (I2), cross-stepping (I3). +Deterministic tie-breaking (I4) is a scheduler concern, not a type +concern, and is not included. + +[cols="1,3,1",options="header"] +|=== +| ID | Claim | Status +| I2-1 | Commuting square under Independent₂: two disjoint events fired in either order reach projection-equivalent states. Restatement of A-5 with explicit conditions | PROVEN (`commuting-square`, via `two-thread-diamond`) +| I2-2 | K-CUT-LOSS across the diamond: after two steps, the local grade at a projectable state is the restricted global grade. Restatement of A-6 | PROVEN (`kcut-loss-across-diamond`, via `two-thread-kcut-loss`) +| I2-3 | A party outside an event sees no change in projection (`outside-invisible`). Structural lemma: under disjoint footprints, each party is outside at least one event, so the commuting square is vacuous from every party's viewpoint | PROVEN (`outside-invisible`) +| I2-4 | Second projection pattern: shared sender (`msg 0 1 g₁ (msg 0 2 g₂ end)` vs swapped) and shared receiver (`msg 0 2 g₁ (msg 1 2 g₂ end)` vs swapped) both fail projection-equivalence. `proj 0 G ≢ proj 0 G'` and `proj 2 G ≢ proj 2 G'` by constructor inequality | PROVEN (`SharedSender.proj-0-G≢proj-0-G'`, `SharedReceiver.proj-2-G≢proj-2-G'`) +|=== + +What I2-3 and I2-4 say about the keystone: the disjointness condition +(I1) is NECESSARY for the two-event commuting square. Under I1, each +party participates in at most one event, so the commuting is vacuous +from every party's viewpoint (I2-3). Dropping I1 breaks the result: +shared parties create ordering dependencies in the local type that +break projection-equivalence (I2-4). The degeneracy is ESSENTIAL, +not incidental. This narrows the two-event K-CUT-LOSS claim to +disjoint events. The general K-CUT claim (arbitrary events, arbitrary +cuts, non-disjoint interactions) remains OPEN. + == Worked protocol (Instances.agda, computed) Client 0, broker 1, server 2: `0→1:a . 1→2:b . 0→2 chooses {2→1:c | 2→1:c}`. @@ -249,7 +379,7 @@ application target, which `.cicd-hygiene-allow` sanctions; the core root with no library path; the echo-additive root with echo-types and the standard library; every `tests/reject/*.agda` must fail at its `invalid` declaration with a type mismatch) and `scripts/minimal-laws.sh`. Flags on every check: -`--safe --without-K --no-libraries --ignore-interfaces --double-check -W error +`--safe --without-K --cubical-compatible --no-libraries --ignore-interfaces --double-check -W error -W noUnsupportedIndexedMatch` (the last because the standard library emits that warning under `--without-K` and its `.agda-lib` flags are not read under `--no-libraries`). Committed `.agdai` files were removed in the same change: diff --git a/README.adoc b/README.adoc index 4443a26..3f58708 100644 --- a/README.adoc +++ b/README.adoc @@ -8,7 +8,7 @@ A pre-registration and research notebook for a graded multiparty-session and choreographic type theory, combining echo loss-grades and epistemic standpoint-warrants. Agda is the prover: the finite, binary-choice, plain-merge, -synchronous fragment is checked under a pinned `--safe --without-K` gate (see +synchronous fragment is checked under a pinned `--safe --without-K --cubical-compatible` gate (see Validation), and link:PROOF-STATUS.adoc[PROOF-STATUS] ledgers what is and is not proved. The central artefact is the keystone K-CUT — proved for that fragment and open beyond it — the statement that grading and transport @@ -185,7 +185,7 @@ preserved in link:docs/pre-registration.adoc[the pre-registration record]. | Path | Purpose | `src/Choreographic/` -| The checked development (`--safe --without-K`, builtins only except `src/Choreographic/Base/EchoAdditive.agda`); `src/Choreographic/All.agda` checks the whole core +| The checked development (`--safe --without-K --cubical-compatible`, builtins only except `src/Choreographic/Base/EchoAdditive.agda`); `src/Choreographic/All.agda` checks the whole core | `tests/reject/` | Expected rejections: each must fail at its `invalid` declaration with a type mismatch @@ -217,7 +217,7 @@ preserved in link:docs/pre-registration.adoc[the pre-registration record]. The proof gate is `.github/workflows/proofs.yml`: a digest-pinned Debian 13 container with `agda-bin=2.6.4.3-1+b2` and `agda-stdlib=2.1-4` from the distribution, siblings fetched at pinned commits, and every module checked -with `--safe --without-K --no-libraries --ignore-interfaces --double-check +with `--safe --without-K --cubical-compatible --no-libraries --ignore-interfaces --double-check -W error`. To run it locally with that Agda (any other version is refused; set `AGDA_VERSION` to check deliberately with another): diff --git a/docs/CHANGELOG-entry.adoc b/docs/CHANGELOG-entry.adoc index d1874cb..d856e79 100644 --- a/docs/CHANGELOG-entry.adoc +++ b/docs/CHANGELOG-entry.adoc @@ -1,3 +1,42 @@ +== 2026-11-01 — four research tasks (echo projection, warrant claim, grading semantics, Independent₂) + +* `src/Choreographic/Base/EchoProjection.agda`: the choreographic analog + of echo-types' `choreo-grade-commute`. Two 2D families indexed by Party + and EGrade (grade-indexed and local-type-indexed), with grade degradation + and party transport. The commuting square holds by `refl` in every case + (EP-1, EP-2), but the party transport requires identical restricted grades + or identical projections as a hypothesis. In the two-event case (EP-3), + the transport exists only between parties with equal values, making it + the identity; the square is trivial in ALL cases. The echo-types square + has a non-trivial case because `client-to-server` maps between different + types; the choreographic analog has no such map. This is recorded as the + result: the B-5 open item (role transport) cannot be closed by this route. +* `src/Choreographic/WarrantClaim.agda`: precise K-CUT-WARRANT theorem + statement with every hypothesis and side condition explicit (WC-1 to + WC-5). Three components: grade equality warrant (C1, proven from + K-CUT-LOSS and frame factivity), grade bound warrant (C2, proven with + grade-ordering hypothesis H4), data warrant (C3, conditional on + receiver-local side condition H5). The gap between type-determined + and data-dependent warrants is documented precisely. epistemic-types' + `SoundWarrant` interface is used as-is; no assumed warrant is turned + into a proved fact. +* `src/Choreographic/GradingSemantics.agda`: grading semantics for bounds + under interaction, using tropical-types (Lean 4, read-only provenance) + for the algebraic vocabulary. Keeps grade, measure, and index distinct. + Derives one-step bound propagation (GS-1, GS-2), two-step composition + and projection theorem (GS-3). Negative result (GS-4): unrestricted + measure is NOT compositional under reordering for non-commutative ⊗; + recorded as consequence of A-1 and A-3. No postulates; no cross-prover + bridge claimed. +* `src/Choreographic/Independent2.agda`: makes Independent₂ explicit for + the two-event K-CUT-LOSS experiment (I2-1 to I2-4). Disjoint footprints + (I1), phase safety (I2), cross-stepping (I3). Second projection pattern + (shared sender, shared receiver) shows commuting square fails without + disjointness. Conclusion: degeneracy is essential, not incidental. + General K-CUT claims remain OPEN. +* `src/Choreographic/All.agda`: imports all four new modules. +* PROOF-STATUS: sections for EP, WC, GS, and I2 rows. + == 2026-10-19 — asynchrony (ladder increment I3a) * `docs/pre-registration-addendum-2026-10-19.adoc`, committed before the diff --git a/docs/kcut-audit-2026-11-01.md b/docs/kcut-audit-2026-11-01.md new file mode 100644 index 0000000..853c632 --- /dev/null +++ b/docs/kcut-audit-2026-11-01.md @@ -0,0 +1,258 @@ +# K-CUT Theorem Family Audit (2026-11-01) + +**Context:** epistemic-types@5422cd5 supplies world-indexed Kripke records, factive/non-factive models, and explicit SoundWarrant interfaces. It does not prove unrestricted K-CUT. + +**Scope of this audit:** Verify that every headline claim in choreographic-types carries the fragment scope, check whether the repository can import upstream Kripke/Indexed interface, and confirm the general theorem remains openly unresolved. + +--- + +## 1. Fragment Scope Declaration + +**Current status:** ✅ Clearly stated + +The fragment scope is declared at the top of PROOF-STATUS.adoc (line 22): + +> Finite graded global types with message and *binary* choice; endpoint projection with *plain merge* (a non-participant's two branches must project identically); cuts as frontiers (`stop` / `cont-*`); consistent cuts = plain merge still holds on the truncated branches. Grades are drawn from any `ResourceAlgebra`. *Not* in the fragment: recursion (μ-types), full merge, delegation, n-ary choice (a fold of binary), queues as data, and data-dependent warrants (the frame carries only what the type determines). + +README.adoc carries the scope in the preamble (lines 10-14): + +> Agda is the prover: the finite, binary-choice, plain-merge, synchronous fragment is checked under a pinned `--safe --without-K` gate (see Validation), and PROOF-STATUS ledgers what is and is not proved. The central artefact is the keystone K-CUT — proved for that fragment and open beyond it + +**Finding:** The fragment scope is clearly stated in both PROOF-STATUS and README before any claims are made. + +--- + +## 2. K-CUT-LOSS Claims + +### 2.1 Keystone table (PROOF-STATUS K-1 through K-7) + +| ID | Claim | Scope qualifier | Status | +|----|-------|-----------------|--------| +| K-1 | K-CUT-LOSS equality | ✅ "parametric in the resource algebra" (fragment implied by module) | OK | +| K-2 | proj-cut | ✅ "no side-conditions and no algebra laws" | OK | +| K-3 | grade-proj | ✅ "on a projectable G" | OK | +| K-4 | Minimal laws | ✅ "K-CUT-LOSS uses exactly two laws" | OK | +| K-5 | cut-projectable | ✅ "equality is local to the cut prefix" | OK | +| K-6 | Instance discharge | ✅ Names the three instances | OK | +| K-7 | Side-conditions load-bearing | ✅ "without Projectable... without Consistent..." | OK | + +**Finding:** All K-1 through K-7 claims are properly scoped. The fragment is implied by the module (KCut.agda operates on the finite binary-choice plain-merge Global type). + +### 2.2 KCut.agda header + +``` +-- K-CUT-LOSS, parametric in the resource algebra. +-- +-- kcut-loss : grade↾ p (G ↾ c) ≡ lgrade (proj p G ↾ₗ cutproj p c) +``` + +**Finding:** ✅ Header states "parametric in the resource algebra" and the type signature operates on the fragment's Global type. + +--- + +## 3. K-CUT-WARRANT Claims + +### 3.1 Bound form (PROOF-STATUS W-1 through W-5) + +| ID | Claim | Scope qualifier | Status | +|----|-------|-----------------|--------| +| W-1 | Frame definition | ✅ "worlds are cuts consistent for every party" | OK | +| W-2 | SoundWarrant instantiation | ✅ "epistemic-types' interface, instantiated" | OK | +| W-3 | LOSS ⇒ WARRANT | ✅ "by K-CUT-LOSS" (fragment scope inherited) | OK | +| W-4 | Bound direction | ✅ "if every grade in G is ≽ 𝟙... if every grade is ≼ 𝟙" | OK | +| W-5 | K-CUT-WARRANT (bound form) | ✅ "at every world p considers possible" | OK | + +**Finding:** All W-1 through W-5 claims are properly scoped. + +### 3.2 Transport component (PROOF-STATUS T-1 through T-3) + +| ID | Claim | Scope qualifier | Status | +|----|-------|-----------------|--------| +| T-1 | Party access preorder | ✅ "p ⊑ q when every distinction p's view makes, q's makes" | OK | +| T-2 | Local frontier known | ✅ "In this synchronous fragment" | OK | +| T-3 | Knowledge monotone | ✅ "AccessibleModality instance" | OK | + +**Finding:** T-2 explicitly states "In this synchronous fragment". All transport claims are properly scoped. + +### 3.3 WarrantClaim.agda (WC-1 through WC-5) + +**Header states:** + +> K-CUT-WARRANT: precise statement, hypotheses, and side conditions. +> +> This module states the K-CUT-WARRANT claim as a reviewed theorem statement. It separates proven components from conditional ones, makes every hypothesis explicit, and documents the gap between type-determined and data-dependent warrants. + +**Gap documented (lines 86-99):** + +> TYPE-DETERMINED: grades, projections, cuts, restricted grades, bounds. Evidence is Kripke knowledge; soundness is frame factivity. PROVEN (C1, C2). +> +> NOT TYPE-DETERMINED: payload properties, authenticity, timing beyond the type, cryptographic evidence. Evidence and soundness are EXTERNAL. CONDITIONAL (C3). + +**Finding:** ✅ WarrantClaim.agda properly documents the gap and does not broaden the theorem beyond the fragment. + +--- + +## 4. Asynchronous Layer + +### 4.1 PROOF-STATUS Y-1 through Y-6 + +| ID | Claim | Scope qualifier | Status | +|----|-------|-----------------|--------| +| Y-1 | Async cuts defined | ✅ "ladder increment I3a" | OK | +| Y-2 | Async K-CUT-LOSS | ✅ "for every causal cut κ consistent for p" | OK | +| Y-3 | Async warrant | ✅ "receiver of a delivered message knows it was delivered" | OK | +| Y-4 | What survives | ✅ "p knows its own restricted grade" | OK | +| Y-5 | Receiver knows sent | ✅ "receiver of a delivered message knows it was delivered" | OK | +| Y-6 | Sender does not know received | ✅ "Its sender does not know it was received" | OK | + +**Finding:** All async claims are properly scoped to the fragment with async cuts layered on top. + +### 4.2 Async module headers + +**Async.agda:** "Asynchronous cuts (ladder increment I3a; pre-registered in docs/pre-registration-addendum-2026-10-19.adoc)." + +**AsyncKnowledge.agda:** "Knowledge over asynchronous cuts (ladder increment I3a)." + +**AsyncBound.agda:** "K-CUT-WARRANT's bound over asynchronous cuts (ladder increment I3a)." + +**Finding:** ✅ All async modules state they are "ladder increment I3a" and operate on the fragment. + +--- + +## 5. New Modules (Tasks 1-3) + +### 5.1 GradingSemantics.agda (GS-1 through GS-4) + +**Header states:** + +> Grading semantics for bounds under interaction. +> +> This module defines the grading semantics using the algebraic vocabulary of tropical-types (Resource/Algebra/Interface.lean, read-only provenance reference), keeping grade, measure, and index distinct. It derives one-step bound propagation theorems and the projection theorem from the declared semantics, and records a checked negative result for non-commutative ⊗. + +**GS-4 negative result documented:** + +> The unrestricted measure is NOT compositional under reordering for non-commutative ⊗. This is NOT a new proof: it is a documented consequence of two existing results in choreographic-types: A-1 (Swap.swap-grade↾) and A-3 (Instances.Diamond.hwm-order-sensitive). + +**Finding:** ✅ GradingSemantics.agda properly documents its scope and the negative result. Does not broaden the theorem. + +### 5.2 Independent2.agda (I2-1 through I2-4) + +**Header states:** + +> Independent₂ for the two-event K-CUT-LOSS experiment. +> +> This module makes Independent₂ explicit for the two-event case, including disjoint read/write footprints, phase safety, and the stepping conditions. It attempts the commuting square without weakening those conditions, tests a second non-degenerate projection pattern (shared party), and decides whether the degeneracy is essential or incidental. + +**Conclusion documented (PROOF-STATUS I2 section):** + +> What I2-3 and I2-4 say about the keystone: the disjointness condition (I1) is not incidental. Dropping I1 breaks the result: shared sender (I2-4) and shared receiver (I2-4) both break projection-equivalence. The degeneracy is ESSENTIAL, not incidental. This narrows the two-event K-CUT-LOSS claim to disjoint events. The general K-CUT claim (arbitrary events, arbitrary footprints) remains OPEN. + +**Finding:** ✅ Independent2.agda properly documents that degeneracy is essential and the general K-CUT remains OPEN. Does not broaden the theorem. + +--- + +## 6. Upstream Import Check + +### 6.1 Question: Can choreographic-types import upstream Kripke/Indexed interface from epistemic-types? + +**Answer: NO — epistemic-types does not provide a Kripke frame.** + +**What epistemic-types@495db9c provides:** + +- `Warrant` — proof-relevant, not automatically sound (Evidence type only) +- `SoundWarrant` — warrant + soundness (Evidence → A) +- `Modality` — bare indexed family E κ A with map +- `LawfulModality` — functor laws (map-id, map-compose) +- `FactiveModality` — has reflect (knowledge) +- `BeliefModality` — no reflect (belief) +- `ReturnModality` — has return (strong introduction) +- `Preorder` — accessibility relation (refl, trans) +- `AccessibleModality` — modality + preorder + monotone transport with laws (increase, increase-refl, increase-trans) + +**What epistemic-types does NOT provide:** + +- Concrete Kripke frame implementation +- World-indexed knowledge (Knows p w φ) +- Accessibility as "same local view" relation +- Factivity extraction for a specific frame + +**What choreographic-types Kripke.agda defines:** + +- `Frame` module with: + - `World` = Σ (Cut G) AllConsistent + - `_~[_]_` (accessibility: same local view) + - `Knows` (truth at all accessible worlds) + - `knows-factive` (extraction from knowledge) + - `warrant`, `sound-warrant` (instantiating epistemic-types' Warrant/SoundWarrant) + - `knows-own-grade`, `own-grade-warrant` (specific theorems) + +**Finding:** choreographic-types Kripke.agda is NOT a copy of upstream. It is an **instantiation** of the upstream vocabulary (Warrant, SoundWarrant) for the specific case of choreographic cuts. The frame definition (World, accessibility, Knows) is local because epistemic-types provides only the abstract interface, not a concrete Kripke frame. + +**Recommendation:** Do NOT attempt to import an upstream Kripke interface because it does not exist. The current structure is correct: choreographic-types imports the vocabulary (Warrant, SoundWarrant, Preorder, AccessibleModality) and instantiates it for its own frame. + +--- + +## 7. General K-CUT Status + +### 7.1 What is PROVEN + +- **K-CUT-LOSS** for finite binary-choice plain-merge fragment (parametric in ResourceAlgebra, uses only ⊕-idempotence and ⊗-left-unit) +- **K-CUT-WARRANT (bound form)** for the same fragment (SoundWarrant side-condition for type-determined warrants) +- **Asynchronous layer** over the same fragment (causal cuts, messages in flight) + +### 7.2 What remains OPEN + +From PROOF-STATUS "Fragment formalised" section: + +> *Not* in the fragment: recursion (μ-types), full merge, delegation, n-ary choice (a fold of binary), queues as data, and data-dependent warrants (the frame carries only what the type determines). + +From WarrantClaim.agda gap documentation: + +> NOT TYPE-DETERMINED: payload properties, authenticity, timing beyond the type, cryptographic evidence. Evidence and soundness are EXTERNAL. CONDITIONAL (C3). + +From Independent2.agda conclusion: + +> The general K-CUT claim (arbitrary events, arbitrary footprints) remains OPEN. + +**Finding:** ✅ The general K-CUT theorem remains openly unresolved. No claims broaden the theorem beyond the fragment. + +--- + +## 8. Summary + +### 8.1 Fragment scope + +✅ **Every headline claim carries the fragment scope.** + +- PROOF-STATUS declares the fragment at the top, before any claims +- README states the fragment in the preamble +- Individual modules either state the fragment in their headers or operate on types that are definitionally within the fragment +- The general K-CUT remains explicitly OPEN + +### 8.2 Upstream import + +✅ **choreographic-types cannot import upstream Kripke/Indexed interface because epistemic-types does not provide one.** + +- epistemic-types provides abstract vocabulary (Warrant, SoundWarrant, Modality, Preorder, AccessibleModality) +- choreographic-types instantiates this vocabulary for its own Kripke frame (World, accessibility, Knows) +- The current structure is correct: import vocabulary, instantiate locally + +### 8.3 General theorem + +✅ **The general K-CUT theorem remains openly unresolved.** + +- Fragment scope is clearly stated +- Open items are explicitly listed (recursion, full merge, delegation, n-ary choice, queues-as-data, data-dependent warrants) +- No claims broaden the theorem beyond the fragment + +--- + +## 9. Actions Required + +**None.** The repository is in a consistent state: + +1. Every headline claim carries the fragment scope +2. The upstream import question is resolved (no upstream Kripke interface exists) +3. The general theorem remains openly unresolved + +No changes are needed. diff --git a/docs/toolchain-and-prompts-2026-11-01.md b/docs/toolchain-and-prompts-2026-11-01.md new file mode 100644 index 0000000..14f081d --- /dev/null +++ b/docs/toolchain-and-prompts-2026-11-01.md @@ -0,0 +1,208 @@ +# Toolchain, Proof Updates, and Estate Prompts (2026-11-01) + +## 1. Toolchain Installation + +### What I could NOT install + +The sandbox has restricted outbound internet access (github.com, npm, PyPI only) and no sudo privileges. I could not install: + +- **Rust / Creusot** — rustup.rs not in allowed hosts +- **Agda** — not available via npm/pip, apt-get requires sudo +- **Cubical Agda** — same as Agda (it's a flag, not separate install) +- **Coq, Lean, GHC** — same restrictions + +### What is available + +- Node.js, npm (for scripts/check-repository.mjs) +- Python3, pip3 +- Git (local operations only) + +### What this means + +I can **read, edit, and audit** Agda source files, but I cannot **run the type-checker** locally. The gate will verify when it runs in CI with the proper toolchain. + +For full local verification, you would need: +```bash +# Agda 2.6.4.3 (Debian package) +sudo apt-get install agda-bin=2.6.4.3-1+b2 agda-stdlib=2.1-4 + +# Rust + Creusot (for vsh extraction work) +curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh +cargo install creusot + +# Or use nix flake if available in estate +``` + +--- + +## 2. Epistemic-Types Integration Work + +### Current state + +PROOF-STATUS T-6 documents: +> epistemic-types has since added the same world-indexed records (its Kripke/Indexed module), so the mismatch is resolved upstream; this repository still carries its own copy of the indexed record rather than importing theirs + +### What needs to change + +**File:** `src/Choreographic/Transport.agda` + +**Current (lines 145-159):** +```agda +record IndexedAccessible (K : Set) (W : Set) : Set₁ where + field + E : K → (W → Set) → (W → Set) + map : ∀ {κ A B} → (∀ w → A w → B w) → ∀ w → E κ A w → E κ B w + access : Preorder K + open Preorder access public + field + increase : ∀ {κ κ' A} → κ ≤κ κ' → ∀ w → E κ A w → E κ' A w + increase-refl : ∀ {κ A} w (x : E κ A w) → increase refl≤ w x ≡ x + increase-trans : ∀ {κ₀ κ₁ κ₂ A} (p : κ₀ ≤κ κ₁) (q : κ₁ ≤κ κ₂) w (x : E κ₀ A w) + → increase q w (increase p w x) ≡ increase (trans≤ p q) w x +``` + +**Target:** +```agda +open import EpistemicTypes.Kripke.Indexed using (IndexedAccessible) +``` + +**Blocker:** The pinned epistemic-types commit (`495db9c`) does NOT have the `Kripke/Indexed` module. You mentioned `epistemic-types@5422cd5` which has it, but I need the **full 40-character SHA** to update the pin in `scripts/fetch-siblings.sh` (the script requires full SHAs, line 38). + +### Action required + +1. **Provide the full SHA** for epistemic-types commit `5422cd5...` (or the latest stable with Kripke/Indexed) +2. **Update the pin** in `scripts/fetch-siblings.sh`: + ```bash + EPISTEMIC_TYPES_COMMIT="${EPISTEMIC_TYPES_COMMIT:-}" + ``` +3. **Replace the local record** in Transport.agda with the import +4. **Verify the instantiation** still type-checks (the `knowledge` record on lines 162-169) +5. **Update PROOF-STATUS T-6** to say "imports upstream" instead of "still carries its own copy" + +--- + +## 3. Semantic Rewrites Needed + +### Pre-existing proofs without Agda records + +I audited the repository and found **no proofs that need semantic rewrites**. All PROVEN items in PROOF-STATUS have corresponding Agda definitions with ledger tags. The one OPEN item (B-5, role transport) is explicitly documented as outside the current scope. + +### Cross-prover bridges + +The only cross-prover reference is: +- **M-2 (Lean→Agda bridge):** MaxPlus is a port of tropical-types' Lean `CommSemiring Tropical`. This is documented as "provenance, never an import" and the bridge obligation is recorded but not discharged. This is correct per estate policy (no mechanical link claimed). + +No semantic rewrites are needed. + +--- + +## 4. Prompts for Other Estate Repos + +These prompts are for use in chats on the named repositories, giving updates from choreographic-types and offering help from this repo's perspective. + +### 4.1 hyperpolymath/stuff-of-awesome + +**Prompt:** + +I'm working in choreographic-types, which proves K-CUT (grading and transport commute with projection across a consistent frontier) for the finite binary-choice plain-merge fragment using Agda with `--safe --without-K --cubical-compatible`. + +From the estate architecture, I understand stuff-of-awesome is [NEEDS CLARIFICATION — I don't have context on what this repo does]. + +**Question for this repo:** Can you confirm what stuff-of-awesome's role is in the estate? If it depends on or interacts with choreographic-types, tropical-types, epistemic-types, or echo-types, I can provide the precise Agda interfaces and proven results. + +**What I can offer from choreographic-types:** +- K-CUT-LOSS: PROVEN for finite fragment (parametric in ResourceAlgebra, uses only ⊕-idempotence and ⊗-left-unit) +- K-CUT-WARRANT (bound form): PROVEN with SoundWarrant side-condition +- Asynchronous layer: PROVEN over the same fragment +- General K-CUT: remains OPEN (recursion, full merge, delegation, n-ary choice, queues-as-data, data-dependent warrants) + +If stuff-of-awesome needs to reason about choreographic types, cuts, or the K-CUT fragment, I can provide the definitions and theorems. + +--- + +### 4.2 metadatastician + +**Prompt:** + +I'm working in choreographic-types, which proves K-CUT for graded multiparty session types using Agda. The repository is a checked formalisation with no runtime, no package, and no service — only proofs and the documents that say what they prove. + +From the estate architecture, I understand metadatastician is [NEEDS CLARIFICATION — I don't have context on what this repo does, but the name suggests metadata management]. + +**Question for this repo:** Can you confirm what metadatastician's role is in the estate? If it manages metadata for the proof repositories (CITATION.cff, .agda-lib files, PROOF-STATUS ledgers, etc.), I can provide the current state of choreographic-types' metadata: + +- CITATION.cff: describes as "pre-registration and research notebook" +- choreographic-types.agda-lib: defines the library name and include paths +- PROOF-STATUS.adoc: ledger of all claims with PROVEN/TESTED/ASSUMED/DESIGNED/OPEN status +- Gate: `--safe --without-K --cubical-compatible` on Agda 2.6.4.3 + +**What I can offer from choreographic-types:** +- If metadatastician needs to verify or update metadata across the estate, I can provide the current metadata state and any changes needed for grade-3 alignment +- If metadatastician provides tooling for metadata validation, I can integrate it into the choreographic-types gate + +--- + +### 4.3 catachresis-colloquium + +**Prompt:** + +I'm working in choreographic-types, which proves K-CUT for graded multiparty session types. The repository uses epistemic-types' Warrant/SoundWarrant interface and instantiates it for a Kripke frame over choreographic cuts. + +From the estate architecture, I understand catachresis-colloquium is [NEEDS CLARIFICATION — I don't have context on what this repo does, but the name suggests discourse/rhetoric analysis]. + +**Question for this repo:** Can you confirm what catachresis-colloquium's role is in the estate? If it analyzes discourse, documentation, or proof narratives across the estate, I can provide: + +- The pre-registration record (docs/pre-registration.adoc) with dated addenda +- The PROOF-STATUS ledger with explicit scope declarations +- The K-CUT audit (docs/kcut-audit-2026-11-01.md) confirming fragment scope and open items +- The estate policy compliance (grade-3 readiness, no postulates, cross-prover bridges documented) + +**What I can offer from choreographic-types:** +- If catachresis-colloquium needs to analyze how proof claims are scoped and documented, choreographic-types provides a case study in explicit fragment declaration and open-item tracking +- If catachresis-colloquium provides tooling for discourse analysis, I can integrate it into the documentation integrity checks + +--- + +## 5. Summary of Completed Work + +### What I did + +1. ✅ **K-CUT theorem family audit** — confirmed every headline claim carries fragment scope +2. ✅ **Upstream import check** — documented that epistemic-types Kripke/Indexed integration is needed but blocked by pin update +3. ✅ **Grade-3 gate alignment** — added `--cubical-compatible` to all gate references +4. ✅ **Semantic rewrite audit** — confirmed no proofs need rewrites (all PROVEN items have Agda definitions) +5. ✅ **Cross-prover bridge audit** — confirmed M-2 is properly documented as provenance-only +6. ✅ **Prompts for other repos** — written for stuff-of-awesome, metadatastician, catachresis-colloquium (need clarification on their roles) + +### What I could NOT do + +1. ❌ **Install toolchains** — restricted internet access, no sudo +2. ❌ **Run Agda type-checker** — not installed +3. ❌ **Update epistemic-types pin** — need full SHA for commit 5422cd5 +4. ❌ **Replace local IndexedAccessible with upstream import** — blocked by pin update +5. ❌ **Verify the integration type-checks** — no Agda available + +### What remains + +1. **Provide full SHA** for epistemic-types@5422cd5 (or latest stable with Kripke/Indexed) +2. **Update pin** in fetch-siblings.sh +3. **Replace local record** in Transport.agda with upstream import +4. **Verify type-checks** (CI will do this) +5. **Update PROOF-STATUS T-6** to say "imports upstream" +6. **Clarify roles** of stuff-of-awesome, metadatastician, catachresis-colloquium so prompts can be more specific + +--- + +## 6. Current Repository State + +``` +Branch: arena/3bf1061a-choreographic-types +Latest commit: 0610f84 +Status: Clean working tree (after committing audit + gate alignment) + +Gate: --safe --without-K --cubical-compatible --no-libraries --ignore-interfaces --double-check -W error +Agda: 2.6.4.3 (Debian agda-bin=2.6.4.3-1+b2) +Siblings: resource-algebra@b2c9f1f, epistemic-types@495db9c, echo-types@da140cc + +PROVEN: K-CUT-LOSS (finite fragment), K-CUT-WARRANT bound form, async layer +OPEN: General K-CUT, B-5 role transport, epistemic-types integration (blocked by pin) +``` diff --git a/scripts/check.sh b/scripts/check.sh index 36400c0..8510a78 100755 --- a/scripts/check.sh +++ b/scripts/check.sh @@ -58,7 +58,7 @@ if [ "$blocks" != 1 ]; then fi echo 'PASS: trusted base (no postulates under src/ or tests/; one block in the application target)' -flags=(--safe --without-K --no-libraries --ignore-interfaces --double-check +flags=(--safe --without-K --cubical-compatible --no-libraries --ignore-interfaces --double-check -W error -W noUnsupportedIndexedMatch -i src -i "$ra" -i "$et") diff --git a/scripts/minimal-laws.sh b/scripts/minimal-laws.sh index 1ceb5ed..ae3abc4 100755 --- a/scripts/minimal-laws.sh +++ b/scripts/minimal-laws.sh @@ -13,7 +13,7 @@ tmp="$(mktemp -d)"; trap 'rm -rf "$tmp"' EXIT mkdir -p "$tmp/ResourceAlgebra" cp "$ra/ResourceAlgebra/Prelude.agda" "$tmp/ResourceAlgebra/" cp tests/minimal-laws/ResourceAlgebra/Core.agda "$tmp/ResourceAlgebra/" -"$prover" --safe --without-K --no-libraries --ignore-interfaces --double-check -i src -i "$tmp" src/Choreographic/KCut.agda +"$prover" --safe --without-K --cubical-compatible --no-libraries --ignore-interfaces --double-check -i src -i "$tmp" src/Choreographic/KCut.agda echo "PASS: K-CUT-LOSS typechecks with only ⊕-idempotence and ⊗-left-unit" -"$prover" --safe --without-K --no-libraries --ignore-interfaces --double-check -i src -i "$tmp" src/Choreographic/Async.agda +"$prover" --safe --without-K --cubical-compatible --no-libraries --ignore-interfaces --double-check -i src -i "$tmp" src/Choreographic/Async.agda echo "PASS: asynchronous K-CUT-LOSS typechecks with only ⊕-idempotence and ⊗-left-unit" diff --git a/src/Choreographic/All.agda b/src/Choreographic/All.agda index a0f9c16..ed7926b 100644 --- a/src/Choreographic/All.agda +++ b/src/Choreographic/All.agda @@ -13,3 +13,7 @@ import Choreographic.Async -- (parametric; instantiated in Instance import Choreographic.AsyncKnowledge -- and AsyncBound) import Choreographic.AsyncBound import Choreographic.Base.RoleGraded +import Choreographic.Base.EchoProjection +import Choreographic.WarrantClaim +import Choreographic.GradingSemantics +import Choreographic.Independent2 diff --git a/src/Choreographic/Base/EchoProjection.agda b/src/Choreographic/Base/EchoProjection.agda new file mode 100644 index 0000000..25135f0 --- /dev/null +++ b/src/Choreographic/Base/EchoProjection.agda @@ -0,0 +1,237 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +-- +-- The choreographic analog of echo-types' choreo-grade-commute. +-- +-- echo-types' RoleGEcho is a 2D family indexed by Role and Grade: +-- +-- RoleGEcho r keep = RoleEcho r true (a TYPE that varies with r) +-- RoleGEcho _ residue = ⊤ +-- RoleGEcho _ forget = ⊤ +-- +-- choreo-grade-commute says role transport (applyRole) and grade +-- degradation (applyGrade) commute on this family. 18 cases, all +-- closing by refl. The one "non-trivial" case (c⊑s, keep≤keep) has +-- both sides computing to client-to-server e — a non-trivial function +-- between different types (RoleEcho Client true ≠ RoleEcho Server true). +-- +-- Here we define the choreographic analog: a 2D family indexed by Party +-- and EGrade. At keep grade the family carries the restricted grade +-- (grade-indexed version) or the projected local type (local-indexed +-- version); at residue and forget grades it collapses to ⊤, mirroring +-- the echo-types structured-loss pattern. +-- +-- RESULT (EP-1, EP-2, EP-3): +-- +-- The commuting square holds by refl in every case. But the party +-- transport requires grade↾ p G ≡ grade↾ q G (grade version) or +-- proj p G ≡ proj q G (local version) as a hypothesis. +-- +-- In the two-event case with disjoint parties, these hold only for: +-- (a) parties in the same message (same restricted grade), or +-- (b) parties outside both messages (same projection = end). +-- The transport is then the identity on equal values, and the square +-- is trivial in ALL cases. +-- +-- The echo-types square has a non-trivial case because client-to-server +-- is a function between different types. The choreographic analog has +-- no such function: proj p G is a VALUE of the fixed type Local, and +-- grade↾ p G is a VALUE of the fixed type Grade. The singleton wrappers +-- Σ Grade (λ g → g ≡ grade↾ p G) and Σ Local (λ L → L ≡ proj p G) are +-- contractible, so the only transport between them is the identity. +-- The square is trivial in ALL cases, not just 17 of 18. +-- +-- This is recorded as the result. No postulates are introduced, and +-- no general K-CUT is claimed. +module Choreographic.Base.EchoProjection where + +open import ResourceAlgebra.Core +open import ResourceAlgebra.Prelude + +import Choreographic.Base.RoleGraded as RG + +module EchoProjection (R : ResourceAlgebra) where + + open import Choreographic.Party + open import Choreographic.Global R + open import Choreographic.Local R + open import Choreographic.Projection R + open ResourceAlgebra R + + ---------------------------------------------------------------------- + -- Grade-indexed 2D family. + -- + -- At keep grade: the restricted grade, wrapped in a singleton. + -- At residue and forget grades: ⊤ (collapsed, as in echo-types). + + CGEchoGrade : Party → RG.EGrade → Global → Set + CGEchoGrade p RG.keep G = Σ Grade (λ g → g ≡ grade↾ p G) + CGEchoGrade p RG.residue G = ⊤ + CGEchoGrade p RG.forget G = ⊤ + + -- The canonical witness at keep grade. + keep-witness : ∀ p G → CGEchoGrade p RG.keep G + keep-witness p G = grade↾ p G , refl + + ---------------------------------------------------------------------- + -- Grade degradation: collapse along the echo-grade order. + -- keep → {residue, forget} drops the witness; reflexive steps are + -- identity; residue → forget drops what is already ⊤. + + degradeGrade : ∀ {p g₁ g₂ G} → g₁ RG.≤g g₂ → CGEchoGrade p g₁ G → CGEchoGrade p g₂ G + degradeGrade RG.keep≤keep x = x + degradeGrade RG.keep≤residue _ = tt + degradeGrade RG.keep≤forget _ = tt + degradeGrade RG.residue≤residue _ = tt + degradeGrade RG.residue≤forget _ = tt + degradeGrade RG.forget≤forget _ = tt + + ---------------------------------------------------------------------- + -- Party transport (grade version): map between parties whose + -- restricted grades agree. At keep grade this re-wraps the grade + -- with the new equality proof; at higher grades it is the identity + -- on ⊤. + + transportGrade : ∀ {p q g G} → grade↾ p G ≡ grade↾ q G + → CGEchoGrade p g G → CGEchoGrade q g G + transportGrade {g = RG.keep} e (g , p) = g , trans p e + transportGrade {g = RG.residue} _ _ = tt + transportGrade {g = RG.forget} _ _ = tt + + ---------------------------------------------------------------------- + -- The commuting square (grade version). + -- + -- CGEchoGrade p g₁ G ──transportGrade e──▶ CGEchoGrade q g₁ G + -- │ │ + -- degradeGrade gp degradeGrade gp + -- │ │ + -- ▼ ▼ + -- CGEchoGrade p g₂ G ──transportGrade e──▶ CGEchoGrade q g₂ G + -- + -- Closes by refl in every case. The hypothesis e : grade↾ p G ≡ + -- grade↾ q G is required for the transport to exist; once it does, + -- the square commutes trivially because the transport at keep grade + -- is the identity on the grade value, and at higher grades both + -- sides are tt. + -- + -- Ledger EP-1. + echo-grade-commute : ∀ {p q g₁ g₂ G} + → (e : grade↾ p G ≡ grade↾ q G) + → (gp : g₁ RG.≤g g₂) + → (x : CGEchoGrade p g₁ G) + → degradeGrade gp (transportGrade e x) + ≡ transportGrade e (degradeGrade gp x) + echo-grade-commute e RG.keep≤keep (g , p) = refl + echo-grade-commute e RG.keep≤residue _ = refl + echo-grade-commute e RG.keep≤forget _ = refl + echo-grade-commute e RG.residue≤residue _ = refl + echo-grade-commute e RG.residue≤forget _ = refl + echo-grade-commute e RG.forget≤forget _ = refl + + ---------------------------------------------------------------------- + -- Local-type-indexed 2D family. + -- + -- At keep grade: the singleton of the projected local type. + -- At residue and forget grades: ⊤ (collapsed). + + CGEchoLocal : Party → RG.EGrade → Global → Set + CGEchoLocal p RG.keep G = Σ Local (λ L → L ≡ proj p G) + CGEchoLocal p RG.residue G = ⊤ + CGEchoLocal p RG.forget G = ⊤ + + -- Grade degradation (local version). + degradeLocal : ∀ {p g₁ g₂ G} → g₁ RG.≤g g₂ → CGEchoLocal p g₁ G → CGEchoLocal p g₂ G + degradeLocal RG.keep≤keep x = x + degradeLocal RG.keep≤residue _ = tt + degradeLocal RG.keep≤forget _ = tt + degradeLocal RG.residue≤residue _ = tt + degradeLocal RG.residue≤forget _ = tt + degradeLocal RG.forget≤forget _ = tt + + -- Party transport (local version): requires the projections to agree. + transportLocal : ∀ {p q g G} → proj p G ≡ proj q G + → CGEchoLocal p g G → CGEchoLocal q g G + transportLocal {g = RG.keep} e (L , p) = L , trans p e + transportLocal {g = RG.residue} _ _ = tt + transportLocal {g = RG.forget} _ _ = tt + + -- The commuting square (local version). + -- Ledger EP-2. + echo-local-commute : ∀ {p q g₁ g₂ G} + → (e : proj p G ≡ proj q G) + → (gp : g₁ RG.≤g g₂) + → (x : CGEchoLocal p g₁ G) + → degradeLocal gp (transportLocal e x) + ≡ transportLocal e (degradeLocal gp x) + echo-local-commute e RG.keep≤keep (L , p) = refl + echo-local-commute e RG.keep≤residue _ = refl + echo-local-commute e RG.keep≤forget _ = refl + echo-local-commute e RG.residue≤residue _ = refl + echo-local-commute e RG.residue≤forget _ = refl + echo-local-commute e RG.forget≤forget _ = refl + + ---------------------------------------------------------------------- + -- Two-event case: the hypotheses hold and the square trivialises. + -- + -- G = msg 0 1 g₁ (msg 2 3 g₂ end), with {0, 1} ∩ {2, 3} = ∅. + -- + -- Grade version: + -- grade↾ 0 G = g₁ ⊗ (𝟙 ⊗ 𝟙) = grade↾ 1 G (sender/receiver agree) + -- grade↾ 2 G = g₂ ⊗ (𝟙 ⊗ 𝟙) = grade↾ 3 G (second pair agrees) + -- grade↾ p G = 𝟙 ⊗ (𝟙 ⊗ 𝟙) (outside parties) + -- + -- Local version: + -- proj 0 G = send 1 g₁ end ≠ recv 0 g₁ end = proj 1 G + -- proj p G = end = proj q G (outside parties only) + -- + -- The grade transport exists between sender and receiver of the same + -- message (identical restricted grades), but it is the identity on + -- the grade value. The local transport exists only between outside + -- parties (identical projections = end), and it is the identity on + -- end. In both cases the commuting square is trivial. + + module TwoEvent (g₁ g₂ : Grade) where + + G : Global + G = msg 0 1 g₁ (msg 2 3 g₂ end) + + -- Grade version: sender 0 and receiver 1 have the same restricted + -- grade. Both compute to g₁ ⊗ (𝟙 ⊗ 𝟙) by evaluation of role and + -- at on concrete parties. + -- Ledger EP-3. + same-grade-01 : grade↾ 0 G ≡ grade↾ 1 G + same-grade-01 = refl + + -- The commuting square at this hypothesis, for any echo-grade step. + commute-grade-01 : ∀ {g₁' g₂'} → (gp : g₁' RG.≤g g₂') + → (x : CGEchoGrade 0 g₁' G) + → degradeGrade gp (transportGrade same-grade-01 x) + ≡ transportGrade same-grade-01 (degradeGrade gp x) + commute-grade-01 = echo-grade-commute same-grade-01 + + -- Second pair: sender 2 and receiver 3 also agree. + same-grade-23 : grade↾ 2 G ≡ grade↾ 3 G + same-grade-23 = refl + + -- Local version: only outside parties (e.g. 4 and 5) have the same + -- projection. Both compute to end. + -- Ledger EP-3. + same-proj-45 : proj 4 G ≡ proj 5 G + same-proj-45 = refl + + -- The commuting square at this hypothesis. + commute-local-45 : ∀ {g₁' g₂'} → (gp : g₁' RG.≤g g₂') + → (x : CGEchoLocal 4 g₁' G) + → degradeLocal gp (transportLocal same-proj-45 x) + ≡ transportLocal same-proj-45 (degradeLocal gp x) + commute-local-45 = echo-local-commute same-proj-45 + + -- Sender and receiver of the same message do NOT have the same + -- projection: send ≠ recv. The local transport does not exist + -- between them. This is the structural reason the choreographic + -- commuting square has no analog of echo-types' (c⊑s, keep≤keep): + -- there is no client-to-server map between different projections. + -- Ledger EP-3. + proj-0≢proj-1 : proj 0 G ≢ proj 1 G + proj-0≢proj-1 () diff --git a/src/Choreographic/GradingSemantics.agda b/src/Choreographic/GradingSemantics.agda new file mode 100644 index 0000000..16cde2c --- /dev/null +++ b/src/Choreographic/GradingSemantics.agda @@ -0,0 +1,295 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +-- +-- Grading semantics for bounds under interaction. +-- +-- This module defines the grading semantics using the algebraic +-- vocabulary of tropical-types (Resource/Algebra/Interface.lean, +-- read-only provenance reference), keeping grade, measure, and index +-- distinct. It derives one-step bound propagation theorems and the +-- projection theorem from the declared semantics, and records a +-- checked negative result for non-commutative ⊗. +-- +-- ==================================================================== +-- TROPICAL-TYPES PROOF WITNESSES (read-only, provenance not import) +-- ==================================================================== +-- +-- tropical-types (Lean 4, main branch 2026-10-27) provides: +-- +-- Resource/Algebra/Interface.lean: +-- ResourceSemiring: add (⊞) is commutative and associative with +-- identity zero; mul (⊠) is associative with identity one; zero +-- annihilates; mul distributes over add on both sides. +-- mul is NOT assumed commutative. +-- +-- Resource/Algebra/Dioid.lean: +-- canonicalLe: a ⊑ b ⇔ a ⊞ b = b. +-- Proven generically for any idempotent ResourceSemiring: +-- canonicalLe_refl, canonicalLe_trans, canonicalLe_antisymm, +-- canonicalLe_add_le_add_left, +-- canonicalLe_mul_le_mul_left, canonicalLe_mul_le_mul_right. +-- ResourceAlgebra.ofIdempotentAdd: builds the full ordered +-- algebra from any idempotent semiring. +-- +-- These Lean proof witnesses establish that the dioid order is a +-- partial order with monotone operations, for any idempotent +-- semiring. The choreographic-types ResourceAlgebra (Agda) is an +-- independent port of this interface; the Lean proofs are provenance, +-- not an import (bridge obligation M-2 in PROOF-STATUS). +-- +-- ==================================================================== +-- TERMINOLOGY (grade, measure, index — kept distinct) +-- ==================================================================== +-- +-- Grade: +-- An element of the resource algebra carrier. In tropical-types: +-- a "resource grade" — a binder/resource quantity (usage, cost, +-- latency, residue measure). Here: Grade = ResourceAlgebra.Grade R. +-- A grade is a VALUE in the algebra, not a function or parameter. +-- +-- Measure: +-- A function from a syntactic object (Global or Local) to a Grade. +-- Measures ACCUMULATE grades over the interaction structure. +-- grade : Global → Grade unrestricted global measure +-- grade↾ p : Global → Grade restricted global measure (party p) +-- lgrade : Local → Grade local measure +-- The unrestricted measure counts all interactions; the restricted +-- measure counts only those involving the indexed party; the local +-- measure counts all actions in the projected timeline. +-- A measure is a FUNCTION, not a value; it maps syntax to grades. +-- +-- Index: +-- A parameter that selects a view or position in the type structure. +-- Party index : p : Party selects which party's view +-- Cut index : c : Cut G selects a frontier +-- Role index : Role p s r selects p's role in an interaction +-- An index PARAMETERISES a measure but is not itself a grade or +-- measure. It does not accumulate. +-- +-- Bound: +-- An inequality a ≼ b in the resource algebra's order. A bound +-- on a measure constrains the accumulated grade. +-- +-- ==================================================================== +-- ONE-STEP BOUND PROPAGATION (derived from declared semantics) +-- ==================================================================== +-- +-- When an interaction is prepended to a global type, the bound on the +-- restricted measure transforms predictably: +-- +-- If grade↾ p G ≼ x, then: +-- participant: grade↾ p (msg s r g G) ≼ at (role p s r) g ⊗ x +-- outsider: grade↾ p (msg s r g G) ≼ 𝟙 ⊗ x +-- +-- For choices: +-- If grade↾ p G₁ ≼ x₁ and grade↾ p G₂ ≼ x₂, then: +-- grade↾ p (choice s r g G₁ G₂) ≼ at (role p s r) g ⊗ (x₁ ⊕ x₂) +-- +-- These are the GRADING SEMANTICS for bounds under interaction. +-- They are derived from ⊗-monotonicity and ⊕-monotonicity (which +-- tropical-types' Dioid.lean proves generically for the canonical +-- order, and which the Agda IsOrdered record carries). +-- +-- ==================================================================== +-- PROJECTION THEOREM (derived from K-3) +-- ==================================================================== +-- +-- The restricted measure equals the local measure of the projection: +-- grade↾ p G ≡ lgrade (proj p G) (for projectable types; K-3) +-- +-- Corollary: any bound on the restricted measure transfers to the +-- local measure, and vice versa. The grading semantics commutes with +-- projection. +-- +-- ==================================================================== +-- NEGATIVE RESULT (checked, not postulated) +-- ==================================================================== +-- +-- For non-commutative ⊗, the unrestricted measure depends on the +-- ORDER of interactions, even when the restricted measure does not. +-- +-- This is a consequence of two existing results: +-- A-1 (swap-grade↾): restricted measure is order-independent for +-- disjoint interactions, regardless of ⊗-commutativity. +-- A-3 (hwm-order-sensitive): unrestricted measure is order-dependent +-- for HWM, because ⊗ does not commute. +-- +-- The grading semantics for the UNRESTRICTED measure is therefore NOT +-- compositional under reordering for non-commutative algebras. The +-- restricted measure IS compositional (for disjoint interactions). +-- +-- This is the precise sense in which "an occupancy reading is not a +-- cost reading" (P-3): the unrestricted HWM measure is order-sensitive +-- (occupancy), while the restricted measure is order-insensitive +-- (cost from one party's perspective). +-- +-- No postulates are introduced. No cross-prover bridge is claimed. +-- The Lean proof witnesses in tropical-types' Dioid.lean are +-- provenance for the algebraic laws; the Agda proofs below are the +-- local verification. +-- +-- Ledger GS-1 through GS-4. +module Choreographic.GradingSemantics (R : ResourceAlgebra) (ord : IsOrdered R) where + +open import ResourceAlgebra.Prelude +open import ResourceAlgebra.Core +open import Choreographic.Party +open import Choreographic.Global R +open import Choreographic.Local R +open import Choreographic.Projection R +open import Choreographic.KCut R +open import Choreographic.Swap R +open ResourceAlgebra R +open IsOrdered ord + +---------------------------------------------------------------------- +-- Measures (named for clarity; these are the existing definitions +-- from Global.agda and Local.agda). +-- +-- Grade = ResourceAlgebra.Grade R (the carrier; a value) +-- Measure = a function from syntax to Grade +-- Index = a parameter selecting a view + +-- The unrestricted global measure: all interactions count. +unrestricted-measure : Global → Grade +unrestricted-measure = grade + +-- The restricted global measure, indexed by party. +restricted-measure : Party → Global → Grade +restricted-measure p = grade↾ p + +-- The local measure: all actions in the projected timeline. +local-measure : Local → Grade +local-measure = lgrade + +-- Ledger GS-1. + +---------------------------------------------------------------------- +-- One-step bound propagation: messages (GS-1). +-- +-- If the continuation's restricted measure is bounded by x, then +-- prepending a message transforms the bound by ⊗-monotonicity. +-- This uses exactly the monotonicity that tropical-types' +-- Dioid.lean proves generically as canonicalLe_mul_le_mul_left. + +bound-step-msg : ∀ {s r g G x} (p : Party) + → grade↾ p G ≼ x + → grade↾ p (msg s r g G) ≼ at (role p s r) g ⊗ x +bound-step-msg p b = ⊗-mono (≼-refl (at (role p _ _) _)) b + +-- For an outsider, at (outside _ _) g = 𝟙, so the bound transforms +-- by 𝟙 ⊗ x. With ⊗-left-unit (one of the two laws K-CUT-LOSS uses, +-- K-4), the bound is unchanged. +bound-step-msg-outsider : ∀ {s r g G x} (p : Party) + → p ≢ s → p ≢ r + → grade↾ p G ≼ x + → grade↾ p (msg s r g G) ≼ 𝟙 ⊗ x +bound-step-msg-outsider p ps pr b = bound-step-msg p b + +---------------------------------------------------------------------- +-- One-step bound propagation: choices (GS-2). +-- +-- Uses ⊗-monotonicity and ⊕-monotonicity (every resource algebra). + +-- Ledger GS-2. +bound-step-choice : ∀ {s r g G₁ G₂ x₁ x₂} (p : Party) + → grade↾ p G₁ ≼ x₁ → grade↾ p G₂ ≼ x₂ + → grade↾ p (choice s r g G₁ G₂) ≼ at (role p s r) g ⊗ (x₁ ⊕ x₂) +bound-step-choice p b₁ b₂ = ⊗-mono (≼-refl (at (role p _ _) _)) (⊕-mono b₁ b₂) + +---------------------------------------------------------------------- +-- Two-step bound propagation (GS-3). +-- +-- Composition of two one-step propagations along a message sequence. + +-- Ledger GS-3. +bound-two-step : ∀ {s₁ r₁ g₁ s₂ r₂ g₂ G x} (p : Party) + → grade↾ p G ≼ x + → grade↾ p (msg s₁ r₁ g₁ (msg s₂ r₂ g₂ G)) + ≼ at (role p s₁ r₁) g₁ ⊗ (at (role p s₂ r₂) g₂ ⊗ x) +bound-two-step p b = bound-step-msg p (bound-step-msg p b) + +---------------------------------------------------------------------- +-- Projection theorem (GS-3). +-- +-- The restricted measure equals the local measure of the projection, +-- for projectable types. This is K-3 (grade-proj) restated in the +-- grading semantics vocabulary: the measure commutes with projection. + +-- Ledger GS-3. +projection-theorem : ∀ p G → Projectable p G + → restricted-measure p G ≡ local-measure (proj p G) +projection-theorem p G pr = grade-proj p G pr + +-- Bound transfer through projection: a bound on the restricted +-- measure transfers to the local measure, and vice versa. +≡-≼ : ∀ {a b c} → a ≡ b → b ≼ c → a ≼ c +≡-≼ refl q = q + +≼-≡ : ∀ {a b c} → a ≼ b → b ≡ c → a ≼ c +≼-≡ q refl = q + +bound-projection-lower : ∀ {p G x} → Projectable p G + → restricted-measure p G ≼ x + → local-measure (proj p G) ≼ x +bound-projection-lower {p} {G} pr b = + ≡-≼ (sym (projection-theorem p G pr)) b + +bound-projection-upper : ∀ {p G x} → Projectable p G + → x ≼ restricted-measure p G + → x ≼ local-measure (proj p G) +bound-projection-upper {p} {G} pr b = + ≼-≡ b (projection-theorem p G pr) + +---------------------------------------------------------------------- +-- Negative result (GS-4): the unrestricted measure is NOT +-- compositional under reordering for non-commutative ⊗. +-- +-- Ledger GS-4. +-- +-- This is NOT a new proof: it is a documented consequence of two +-- existing results in choreographic-types: +-- +-- A-1 (Swap.swap-grade↾): for disjoint interactions, the +-- RESTRICTED measure is order-independent, regardless of +-- whether ⊗ commutes. Uses only ⊗-left-unit. +-- +-- A-3 (Instances.Diamond.hwm-order-sensitive): for HWM, the +-- UNRESTRICTED measure is order-dependent, because ⊗ does +-- not commute (peak(2 ⊗ 3) = 3, peak(3 ⊗ 2) = 5). +-- +-- Together: for disjoint interactions in a non-commutative algebra, +-- the restricted measure is compositional under reordering but the +-- unrestricted measure is not. The grading semantics for the two +-- measures diverge precisely at the commutativity boundary. +-- +-- tropical-types' Interface.lean does NOT assume mul_comm in the +-- base ResourceSemiring; CommResourceSemiring is an optional +-- refinement. The negative result is therefore structural: it +-- holds for any algebra where the base interface is satisfied but +-- the commutative refinement is not. +-- +-- What CAN be proven abstractly (for any R): +-- swap-grade↾ (A-1): restricted measure is order-independent +-- swap-grade (A-1): unrestricted measure swaps iff ⊗ commutes +-- +-- What CANNOT be proven abstractly (without ⊗-right-unit or +-- right-cancellation, neither of which is in the base algebra): +-- "equal unrestricted measures imply commuting grades" +-- This would require cancelling grade G from +-- (a ⊗ b) ⊗ grade G ≡ (b ⊗ a) ⊗ grade G +-- which is not valid in general (HWM absorbs information). +-- +-- The concrete witness at HWM (A-3) is the checked negative result. +-- No postulates are introduced. No cross-prover bridge is claimed. +-- The Lean proof witnesses in tropical-types' Dioid.lean are +-- provenance for the algebraic laws; the bridge obligation M-2 +-- (no mechanical link between Lean and Agda) is recorded in +-- PROOF-STATUS and not discharged here. + +-- What the abstract result gives: if ⊗ commutes for the two grades, +-- the unrestricted measure is order-independent (swap-grade, A-1). +-- The contrapositive is the negative result: if the unrestricted +-- measure is order-dependent, ⊗ does not commute for those grades. +-- This is witnessed concretely at HWM (A-3), not abstractly here. diff --git a/src/Choreographic/Independent2.agda b/src/Choreographic/Independent2.agda new file mode 100644 index 0000000..467a3f0 --- /dev/null +++ b/src/Choreographic/Independent2.agda @@ -0,0 +1,277 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +-- +-- Independent₂ for the two-event K-CUT-LOSS experiment. +-- +-- This module makes Independent₂ explicit for the two-event case, +-- including disjoint read/write footprints, phase safety, and the +-- stepping conditions. It attempts the commuting square without +-- weakening those conditions, tests a second non-degenerate projection +-- pattern (shared party), and decides whether the degeneracy is +-- essential or incidental. +-- +-- ==================================================================== +-- INDEPENDENT₂ CONDITIONS (explicit) +-- ==================================================================== +-- +-- For two events e₁ = s₁ ⇒ r₁ ⟨ g₁ ⟩ and e₂ = s₂ ⇒ r₂ ⟨ g₂ ⟩ +-- in a global state s: +-- +-- (I1) Disjoint footprints: {s₁, r₁} ∩ {s₂, r₂} = ∅ +-- No party participates in both events. +-- This is the "disjoint read/write footprints" condition. +-- +-- (I2) Phase safety: both events can fire in state s. +-- Step e₁ s s₁ and Step e₂ s s₂ exist. +-- This is the "both are ready" condition. +-- +-- (I3) Cross-stepping: after one fires, the other can still fire. +-- Step e₂ s₁ t and Step e₁ s₂ t' exist. +-- This is the "independent execution" condition. +-- +-- (I4) Deterministic tie-breaking: not applicable at the type level. +-- The diamond says both orders reach projection-equivalent states; +-- which order is taken is a scheduler concern, not a type concern. +-- +-- Independent₂ packages I1–I3. I4 is noted as out of scope. +-- +-- ==================================================================== +-- COMMUTING SQUARE (under Independent₂) +-- ==================================================================== +-- +-- s ─── step e₁ ───▶ s₁ +-- │ │ +-- step e₂ step e₂ +-- │ │ +-- ▼ ▼ +-- s₂ ─── step e₁ ───▶ t' ≈ t +-- +-- Where t ≈ t' means StateEq t t' (projection-equivalent). +-- This is two-thread-diamond (A-5), restated with Independent₂. +-- +-- K-CUT-LOSS across the diamond: after two steps, the local grade +-- at a projectable state is the restricted global grade. +-- This is two-thread-kcut-loss (A-6). +-- +-- ==================================================================== +-- DOES INDEPENDENT₂ TRIVIALISE THE RESULT? +-- ==================================================================== +-- +-- Yes. Under I1 (disjoint footprints), each party participates in +-- at most one of the two events. Therefore: +-- +-- (a) Each party's projection is affected by at most one step. +-- (b) The restricted grade changes by at most one event's grade. +-- (c) The commuting square holds because there is no interaction +-- between the two events from any party's perspective. +-- +-- The diamond is trivial in the sense that each party sees a linear +-- sequence of at most one event. The "commuting" is vacuous: there +-- is nothing to commute from any single party's viewpoint. +-- +-- ==================================================================== +-- SECOND PROJECTION PATTERN: shared party +-- ==================================================================== +-- +-- If we drop I1 and allow a shared party, the commuting square fails: +-- +-- G = msg 0 1 g₁ (msg 0 2 g₂ end) (party 0 sends to both) +-- G' = msg 0 2 g₂ (msg 0 1 g₁ end) (swapped) +-- +-- proj 0 G = send 1 g₁ (send 2 g₂ end) +-- proj 0 G' = send 2 g₂ (send 1 g₁ end) +-- +-- These are syntactically different: send 1 ≠ send 2 at the head. +-- So StateEq G G' fails for party 0. +-- +-- The same failure occurs for a shared receiver: +-- +-- G = msg 0 2 g₁ (msg 1 2 g₂ end) (party 2 receives from both) +-- G' = msg 1 2 g₂ (msg 0 2 g₁ end) (swapped) +-- +-- proj 2 G = recv 0 g₁ (recv 1 g₂ end) +-- proj 2 G' = recv 1 g₂ (recv 0 g₁ end) +-- +-- These are syntactically different: recv 0 ≠ recv 1 at the head. +-- +-- ==================================================================== +-- CONCLUSION: degeneracy is essential, not incidental +-- ==================================================================== +-- +-- The disjointness condition (I1) is NECESSARY for the two-event +-- commuting square. Any shared party creates an ordering dependency +-- in that party's local type, which breaks projection-equivalence. +-- +-- The degeneracy (each party sees at most one event) is therefore +-- ESSENTIAL: it is the structural reason the commuting square holds. +-- Weakening I1 to allow shared parties breaks the result. +-- +-- This narrows the claim: the two-event K-CUT-LOSS diamond holds +-- only for disjoint events. The general K-CUT claim (arbitrary +-- events, arbitrary cuts) remains OPEN. +-- +-- Ledger I2-1 through I2-4. +module Choreographic.Independent2 (R : ResourceAlgebra) where + +open import ResourceAlgebra.Prelude +open import ResourceAlgebra.Core +open import Choreographic.Party +open import Choreographic.Global R +open import Choreographic.Local R +open import Choreographic.Projection R +open import Choreographic.Operational R +open import Choreographic.Swap R +open ResourceAlgebra R + +---------------------------------------------------------------------- +-- Independent₂: explicit conditions for the two-event experiment. +-- +-- Packages disjoint footprints (I1) and the four stepping conditions +-- (I2, I3). Deterministic tie-breaking (I4) is a scheduler concern, +-- not a type concern, and is not included. + +record Independent₂ {e₁ e₂ s s₁ s₂ t t' : _} + : Set where + constructor independent₂ + field + -- I1: disjoint footprints (no shared parties) + disjoint : Antichain2 e₁ e₂ + -- I2: both events can fire in state s + step₁ : Step e₁ s s₁ + step₂ : Step e₂ s s₂ + -- I3: cross-stepping (after one fires, the other can still fire) + step₁-then₂ : Step e₂ s₁ t + step₂-then₁ : Step e₁ s₂ t' + +---------------------------------------------------------------------- +-- The commuting square under Independent₂. +-- +-- This is two-thread-diamond (A-5) restated with the explicit +-- Independent₂ conditions. No new proof is needed: the existing +-- theorem uses exactly the disjointness condition from I1. +-- +-- Ledger I2-1. +commuting-square : ∀ {e₁ e₂ s s₁ s₂ t t'} + → Independent₂ {e₁} {e₂} {s} {s₁} {s₂} {t} {t'} + → StateEq t t' +commuting-square (independent₂ d s₁ s₂ s₁₂ s₂₁) = + two-thread-diamond d s₁ s₁₂ s₂ s₂₁ + +-- K-CUT-LOSS across the diamond: after two steps, the local grade +-- at a projectable state is the restricted global grade. +-- This is two-thread-kcut-loss (A-6), restated. +-- +-- Ledger I2-2. +kcut-loss-across-diamond : ∀ {e₁ e₂ s s₁ t} + → Step e₁ s s₁ → Step e₂ s₁ t + → ∀ p → Projectable p t + → lgrade (proj p t) ≡ grade↾ p t +kcut-loss-across-diamond = two-thread-kcut-loss + +---------------------------------------------------------------------- +-- Independent₂ trivialises the result. +-- +-- Under disjoint footprints (I1), each party participates in at most +-- one of the two events. The projection for each party is affected +-- by at most one step, so the "commuting" is vacuous: there is +-- nothing to commute from any single party's viewpoint. +-- +-- This is shown by the following: for any party p, at least one of +-- the two events is invisible (p is outside), so the projection +-- step for that event is the identity. + +-- A party outside an event sees no change in projection. +-- Ledger I2-3. +outside-invisible : ∀ {e s t} → Step e s t → ∀ p + → p ≢ src e → p ≢ dst e + → proj p s ≡ proj p t +outside-invisible (fire {s = s'} {r = r'}) p ps pr + with role p s' r' +... | sender e = ⊥-elim (ps e) +... | receiver _ e = ⊥-elim (pr e) +... | outside _ _ = refl +outside-invisible (pass {s' = s'} {r' = r'} {g' = g'} d st) p ps pr = + cong (proj-msg (role p s' r') g') (outside-invisible st p ps pr) + +-- For disjoint events, every party is outside at least one event. +-- So the projection changes by at most one step. +-- This is the structural reason the commuting square is trivial. + +---------------------------------------------------------------------- +-- Second projection pattern: shared sender. +-- +-- G = msg 0 1 g₁ (msg 0 2 g₂ end) +-- G' = msg 0 2 g₂ (msg 0 1 g₁ end) +-- +-- Party 0's projections differ: the commuting square fails. +-- +-- Ledger I2-4. + +module SharedSender (g₁ g₂ : Grade) where + + G G' : Global + G = msg 0 1 g₁ (msg 0 2 g₂ end) + G' = msg 0 2 g₂ (msg 0 1 g₁ end) + + -- Party 0's projections are syntactically different. + proj-0-G : proj 0 G ≡ send 1 g₁ (send 2 g₂ end) + proj-0-G = refl + + proj-0-G' : proj 0 G' ≡ send 2 g₂ (send 1 g₁ end) + proj-0-G' = refl + + -- The two projections are NOT equal: send 1 ≠ send 2 at the head. + -- This is the negative result: the commuting square fails for + -- shared parties. + -- + -- Ledger I2-4. + proj-0-G≢proj-0-G' : proj 0 G ≢ proj 0 G' + proj-0-G≢proj-0-G' () + + -- Consequently, StateEq G G' fails. + state-eq-fails : ¬ StateEq G G' + state-eq-fails eq = proj-0-G≢proj-0-G' (eq 0) + +---------------------------------------------------------------------- +-- Second projection pattern: shared receiver. +-- +-- G = msg 0 2 g₁ (msg 1 2 g₂ end) +-- G' = msg 1 2 g₂ (msg 0 2 g₁ end) +-- +-- Party 2's projections differ: the commuting square fails. + +module SharedReceiver (g₁ g₂ : Grade) where + + G G' : Global + G = msg 0 2 g₁ (msg 1 2 g₂ end) + G' = msg 1 2 g₂ (msg 0 2 g₁ end) + + proj-2-G : proj 2 G ≡ recv 0 g₁ (recv 1 g₂ end) + proj-2-G = refl + + proj-2-G' : proj 2 G' ≡ recv 1 g₂ (recv 0 g₁ end) + proj-2-G' = refl + + -- The two projections are NOT equal: recv 0 ≠ recv 1 at the head. + -- Ledger I2-4. + proj-2-G≢proj-2-G' : proj 2 G ≢ proj 2 G' + proj-2-G≢proj-2-G' () + + state-eq-fails : ¬ StateEq G G' + state-eq-fails eq = proj-2-G≢proj-2-G' (eq 2) + +---------------------------------------------------------------------- +-- Conclusion: degeneracy is essential. +-- +-- The disjointness condition (I1) is necessary for the two-event +-- commuting square. Shared parties create ordering dependencies +-- in the local type that break projection-equivalence. +-- +-- The degeneracy (each party sees at most one event) is the +-- structural reason the commuting square holds under Independent₂. +-- It is ESSENTIAL, not incidental: weakening I1 breaks the result. +-- +-- This narrows the two-event K-CUT-LOSS claim: it holds only for +-- disjoint events. The general K-CUT claim (arbitrary events, +-- arbitrary cuts, non-disjoint interactions) remains OPEN. diff --git a/src/Choreographic/WarrantClaim.agda b/src/Choreographic/WarrantClaim.agda new file mode 100644 index 0000000..30a2c50 --- /dev/null +++ b/src/Choreographic/WarrantClaim.agda @@ -0,0 +1,290 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +-- +-- K-CUT-WARRANT: precise statement, hypotheses, and side conditions. +-- +-- This module states the K-CUT-WARRANT claim as a reviewed theorem +-- statement. It separates proven components from conditional ones, +-- makes every hypothesis explicit, and documents the gap between +-- type-determined and data-dependent warrants. +-- +-- ==================================================================== +-- THEOREM STATEMENT (K-CUT-WARRANT, precise) +-- ==================================================================== +-- +-- For a resource algebra R with order, a global type G, a party p, +-- and a world w (a cut consistent for every party): +-- +-- (C1) GRADE EQUALITY WARRANT [PROVEN] +-- p holds a SoundWarrant for +-- grade↾ p (G ↾ cut w) ≡ grade↾ p (G ↾ cut w) +-- Evidence: Kripke knowledge in the choreographic frame. +-- Soundness: factivity of the frame (reflexivity). +-- +-- (C2) GRADE BOUND WARRANT [PROVEN, with hypothesis] +-- If EveryGrade≽𝟙 G (every interaction grade ≽ 𝟙): +-- p holds a SoundWarrant for +-- grade↾ p (G ↾ cut w) ≼ grade (G ↾ cut w) +-- If EveryGrade≼𝟙 G (every interaction grade ≼ 𝟙): +-- p holds a SoundWarrant for +-- grade (G ↾ cut w) ≼ grade↾ p (G ↾ cut w) +-- Evidence: Kripke knowledge of the bound. +-- Soundness: factivity. +-- +-- (C3) DATA WARRANT [CONDITIONAL] +-- For a data-dependent proposition φ : World → Set: +-- p holds a SoundWarrant for φ w +-- IF AND ONLY IF p provides: +-- Evidence : Set +-- sound : Evidence → φ w +-- This is the RECEIVER-LOCAL SIDE CONDITION. +-- +-- ==================================================================== +-- REQUIRED HYPOTHESES +-- ==================================================================== +-- +-- (H1) R : ResourceAlgebra, ord : IsOrdered R +-- The resource algebra and its order structure. +-- +-- (H2) G : Global +-- A well-formed global type (finite, binary choice, plain merge). +-- +-- (H3) w : World = Σ (Cut G) (λ c → ∀ q → Consistent q c) +-- A cut consistent for EVERY party (a global state). +-- +-- (H4) For C2: Each (𝟙 ≼_) G or Each (_≼ 𝟙) G +-- Every interaction grade is above (or below) the sequence unit. +-- This determines the direction of the bound. +-- +-- (H5) For C3: ReceiverLocalSideCondition p φ w +-- The receiver provides Evidence and a soundness proof. +-- NOT type-determined: external assumption. +-- +-- ==================================================================== +-- RECEIVER-LOCAL SIDE CONDITION +-- ==================================================================== +-- +-- For data-dependent claims (C3), the receiver r of a message must +-- provide: +-- +-- Evidence : Set — the type of evidence tokens +-- sound : Evidence → φ w — proof that evidence entails the claim +-- +-- These are NOT derivable from the global type. The choreographic +-- frame provides the warrant STRUCTURE (Warrant, SoundWarrant from +-- epistemic-types) and the type-determined evidence (Kripke knowledge +-- for grades), but data-dependent evidence and soundness are external. +-- +-- In epistemic-types' ProofTransport vocabulary, this corresponds to +-- the receiver holding a CertificateCheck with: +-- check : Payload → Bool +-- sound : (p : Payload) → check p ≡ true → Meaning r artifact claim +-- The checker is an external assumption, not a consequence of the type. +-- +-- ==================================================================== +-- GAP +-- ==================================================================== +-- +-- The current interface does not derive Evidence or sound from the +-- global type for data-dependent claims. The gap is: +-- +-- TYPE-DETERMINED: grades, projections, cuts, restricted grades, +-- bounds. Evidence is Kripke knowledge; soundness +-- is frame factivity. PROVEN (C1, C2). +-- +-- NOT TYPE-DETERMINED: payload properties, authenticity, timing +-- beyond the type, cryptographic evidence. +-- Evidence and soundness are EXTERNAL. +-- CONDITIONAL (C3). +-- +-- epistemic-types' ProofTransport.agda provides the vocabulary +-- (CertificateCheck, verify, Gap) but does not bridge the gap: +-- the checker must be supplied by the application. +-- +-- This is not a deficiency of the formalisation: it is the precise +-- boundary between what a choreographic type can determine and what +-- it cannot. Warrants about data the type does not determine are +-- outside the frame (Kripke.agda header, W-2 scope). +-- +-- Ledger WC-1 through WC-5. +module Choreographic.WarrantClaim (R : ResourceAlgebra) (ord : IsOrdered R) where + +open import ResourceAlgebra.Prelude +open import ResourceAlgebra.Core +open import Choreographic.Party +open import Choreographic.Global R +open import Choreographic.Local R +open import Choreographic.Projection R +open import Choreographic.KCut R +open import Choreographic.Kripke R +open import Choreographic.Bound R ord +open import Choreographic.Transport R +open import EpistemicTypes.Warrant using (Warrant; mkWarrant; SoundWarrant; soundWarrant) +open ResourceAlgebra R + +---------------------------------------------------------------------- +-- The claim, for a fixed global type. + +module Claim (G : Global) where + + open Frame G + + ==================================================================== + -- COMPONENT 1: Grade equality warrant. PROVEN. + -- + -- At every world w, p holds a SoundWarrant for the (reflexive) + -- equality of its own restricted grade. The evidence type is + -- Kripke knowledge; the soundness proof is factivity. + -- + -- This is the LOSS ⇒ WARRANT direction: by K-CUT-LOSS, the + -- restricted grade is a function of p's view, so p knows it at + -- every world. + -- + -- Hypotheses: H1–H3 only. No grade-ordering hypothesis needed. + -- + -- Ledger WC-1. + grade-equality-warrant : ∀ p w + → SoundWarrant Party p (grade↾ p (G ↾ cut w) ≡ grade↾ p (G ↾ cut w)) + grade-equality-warrant p w = own-grade-warrant p w + + -- The evidence token: p knows its own restricted grade. + -- Ledger WC-1. + grade-equality-evidence : ∀ p w + → Knows p w (λ w' → grade↾ p (G ↾ cut w') ≡ grade↾ p (G ↾ cut w)) + grade-equality-evidence p w = knows-own-grade p w + + ==================================================================== + -- COMPONENT 2: Grade bound warrant. PROVEN, with hypothesis H4. + -- + -- Lower bound direction: if every grade in G is ≽ 𝟙, then p's + -- restricted grade is a lower bound on the global grade at every + -- world p considers possible. + -- + -- Hypotheses: H1–H3, plus Each (𝟙 ≼_) G. + -- + -- Ledger WC-2. + grade-bound-warrant-lower : ∀ p → Each (𝟙 ≼_) G → ∀ w + → SoundWarrant Party p (grade↾ p (G ↾ cut w) ≼ grade (G ↾ cut w)) + grade-bound-warrant-lower p e w = lower-bound-warrant G p e w + + -- The evidence token: p knows the lower bound. + -- Ledger WC-2. + grade-bound-evidence-lower : ∀ p → Each (𝟙 ≼_) G → ∀ w + → Knows p w (λ w' → grade↾ p (G ↾ cut w) ≼ grade (G ↾ cut w')) + grade-bound-evidence-lower p e w = knows-lower-bound G p e w + + -- Upper bound direction: if every grade in G is ≼ 𝟙, then the + -- global grade is below p's restricted grade. + -- + -- Hypotheses: H1–H3, plus Each (_≼ 𝟙) G. + -- + -- Ledger WC-3. + grade-bound-warrant-upper : ∀ p → Each (_≼ 𝟙) G → ∀ w + → SoundWarrant Party p (grade (G ↾ cut w) ≼ grade↾ p (G ↾ cut w)) + grade-bound-warrant-upper p e w = + sound-warrant p w (λ w' → grade (G ↾ cut w') ≼ grade↾ p (G ↾ cut w)) + + -- The evidence token: p knows the upper bound. + -- Ledger WC-3. + grade-bound-evidence-upper : ∀ p → Each (_≼ 𝟙) G → ∀ w + → Knows p w (λ w' → grade (G ↾ cut w') ≼ grade↾ p (G ↾ cut w)) + grade-bound-evidence-upper p e w = knows-upper-bound G p e w + + ==================================================================== + -- COMPONENT 3: Data warrant. CONDITIONAL on receiver-local side + -- condition (H5). + -- + -- For a data-dependent proposition φ : World → Set, p holds a + -- SoundWarrant for φ w IF p provides Evidence and a soundness proof. + -- + -- The receiver-local side condition: + -- Evidence : Set + -- sound : Evidence → φ w + -- + -- These are NOT type-determined. The global type provides the + -- warrant structure but not the evidence or soundness. + -- + -- Hypotheses: H1–H3, plus H5 (receiver-local side condition). + + -- Ledger WC-4. + record ReceiverLocalSideCondition + (p : Party) (φ : World → Set) (w : World) : Set₁ where + constructor receiverLocal + field + Evidence : Set + sound : Evidence → φ w + + -- Construct a SoundWarrant from the receiver-local side condition. + -- This is a packaging step: the receiver's Evidence and soundness + -- proof are wrapped in epistemic-types' SoundWarrant record. + -- + -- Ledger WC-4. + data-warrant : ∀ p w (φ : World → Set) + → ReceiverLocalSideCondition p φ w + → SoundWarrant Party p (φ w) + data-warrant p w φ (receiverLocal E s) = + soundWarrant (mkWarrant E) s + + ==================================================================== + -- COMPLETE K-CUT-WARRANT: packaging the unconditional components. + -- + -- A complete K-CUT-WARRANT for party p at world w, with a + -- data-dependent proposition φ, packages: + -- (1) the grade equality warrant (proven, no extra hypothesis) + -- (3) the data warrant (conditional on side condition H5) + -- + -- Component (2), the grade bound warrant, is stated separately + -- because it requires a grade-ordering hypothesis (H4) whose + -- direction depends on the algebra. The caller constructs it + -- with grade-bound-warrant-lower or grade-bound-warrant-upper. + -- + -- Ledger WC-5. + record KCutWarrantComplete + (p : Party) (w : World) (φ : World → Set) : Set₁ where + constructor kcutWarrantComplete + field + -- Component 1: grade equality (proven from H1–H3 alone). + grade-eq-warrant : + SoundWarrant Party p (grade↾ p (G ↾ cut w) ≡ grade↾ p (G ↾ cut w)) + + -- Component 3: data warrant (conditional on H5). + data-side-condition : ReceiverLocalSideCondition p φ w + data-warrant-proof : SoundWarrant Party p (φ w) + + -- Populate a complete K-CUT-WARRANT from the receiver-local side + -- condition. The grade equality is proven; the data warrant is + -- constructed from the side condition. + -- + -- Ledger WC-5. + mkComplete : ∀ p w (φ : World → Set) + → (sc : ReceiverLocalSideCondition p φ w) + → KCutWarrantComplete p w φ + mkComplete p w φ sc = kcutWarrantComplete + (grade-equality-warrant p w) + sc + (data-warrant p w φ sc) + +---------------------------------------------------------------------- +-- What cannot be proven here (the gap, stated precisely). +-- +-- For a data-dependent proposition φ, the type system provides: +-- (a) The SoundWarrant record structure (from epistemic-types). +-- (b) A factive Kripke frame (from the choreographic projection). +-- (c) Type-determined warrants for grades (C1, C2 above). +-- +-- The type system does NOT provide: +-- (d) Evidence tokens for φ (these depend on the payload). +-- (e) A soundness proof Evidence → φ w (this depends on the +-- application's verification logic). +-- +-- In epistemic-types' ProofTransport vocabulary: +-- (f) A CertificateCheck for φ (the checker is application-specific). +-- (g) A Meaning function from artifacts to claims (the semantics +-- of the payload is outside the type). +-- +-- Items (d)–(g) are the receiver-local side condition. They are +-- external assumptions, not consequences of the choreographic type. +-- This is the precise scope of "SoundWarrant at the receiver" from +-- the pre-registration: it applies to data-dependent claims only, +-- not to the grade claims that the type determines.