Repository navigation
K-CUT theorem family audit, grade-3 gate alignment, and epistemic-types integration plan #38
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -4,7 +4,7 @@ | |
|
|
||
| Statuses: PROVEN / TESTED / ASSUMED / DESIGNED / OPEN. Every PROVEN line | ||
| names the module that discharges it under | ||
| `--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 | ||
|
Comment on lines
+285
to
+289
Contributor
There was a problem hiding this comment. Limit the disjointness conclusion to the proved guarantee. The shared-sender and shared-receiver examples show that dropping I1 can break projection-equivalence. They do not show that disjointness is necessary in every case. For example, swapping two identical
 |
||
| 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 --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: | ||
|
|
||
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Make the repository checker recognize the new ledger IDs.
scripts/check-repository.mjsaccepts only IDs shaped likeK-1. It therefore skips EP-1 through EP-3, along with the new WC, GS, and I2 rows. Their cited definitions can lose their ledger bindings without a repository-check failure. Extend both its row-ID parser and stale-reference scan to recognize the new prefixes. (raw.githubusercontent.com)