Skip to content

Commit f6717f5

Browse files
hyperpolymathhyperpolymath
committed
feat(L8): EffectSubsumes preorder + subsumeCompose (A5)
Closes PROOF-NEEDS §P0.4. The file already had reflexivity (`effectSubsumesRefl`), single-element weakening (`effectWeaken`), and single-declared-set composition (`combineSub`). This change adds the missing transitivity, append-preservation for membership, two-list weakening, and the flagship two-declared-set composition theorem. Lemmas: hasEffectTrans : HasEffect e ys -> EffectSubsumes xs ys -> HasEffect e xs — lift a membership proof through a subsumption. hasEffectCombineL, hasEffectCombineR : HasEffect e xs (resp. ys) -> HasEffect e (combineEffects xs ys) — membership survives appending. subsumePrepend, subsumeAppend : EffectSubsumes d2 a -> EffectSubsumes (d1 ++ d2) a (and dually for d1) — prepending/appending declared effects preserves subsumption of the actual set. Theorems: subsumeRefl : (xs : EffectSet) -> EffectSubsumes xs xs — PROOF-NEEDS §P0.4 naming alias for the existing `effectSubsumesRefl`. subsumeTrans : EffectSubsumes xs ys -> EffectSubsumes ys zs -> EffectSubsumes xs zs — transitivity; together with subsumeRefl makes `EffectSubsumes` a preorder on EffectSet. subsumeCompose : EffectSubsumes d1 a1 -> EffectSubsumes d2 a2 -> EffectSubsumes (d1 ++ d2) (a1 ++ a2) — the composition theorem: sequencing two operations is witnessed by the union of their declared and actual effects; attestations now compose rather than needing re-verification against the monolith. Existing `SubNil`, `SubCons`, `combineSub`, `effectWeaken` untouched. idris2 --check clean. panic-attack assail: 0 weak points. Zero dangerous patterns. %default total.
1 parent 81b191b commit f6717f5

2 files changed

Lines changed: 110 additions & 1 deletion

File tree

‎LEVEL-STATUS.md‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -49,7 +49,7 @@ the remaining v1.1 work.**
4949
| 5 | Bounds-proof | TypedAccess.idr + Levels.idr | Bounds check | ECHIDNA 10^5 | **E2E complete** |
5050
| 6 | Result-type | TypedAccess.idr | Type flow | ECHIDNA 10^5 | **E2E complete** |
5151
| 7 | Aliasing safety | Pointer.idr (Unique) | Erased (QTT) | ECHIDNA 10^4 | **Proven [sfap], erased** |
52-
| 8 | Effect-tracking | Effects.idr | Erased (QTT) | ECHIDNA 10^4 | **Proven [sfap], erased** |
52+
| 8 | Effect-tracking | Effects.idr | Erased (QTT) | ECHIDNA 10^4 | **Proven [sfap], erased. Preorder + composition theorems added A5 (2026-04-18): `subsumeRefl` (alias of `effectSubsumesRefl`), `hasEffectTrans`, `subsumeTrans`, `hasEffectCombineL`/`CombineR`, `subsumePrepend`/`Append`, and the flagship `subsumeCompose` giving `EffectSubsumes d1 a1 -> EffectSubsumes d2 a2 -> EffectSubsumes (d1++d2) (a1++a2)` so L8 attestations compose.** |
5353
| 9 | Lifetime safety | Lifetime.idr | Erased (QTT) | ECHIDNA 10^4 | **Proven [sfap], erased. Preorder + load-safety theorems added A4 (2026-04-18): `outlivesRefl`, `outlivesTrans` (alias of pre-existing `outlivesTransitive` with 7-constructor case analysis), `loadSafe` proof-term, behavioural lemmas `loadSafeOffset` and `loadSafeIrrelevant` (proof irrelevance at the value level).** |
5454
| 10 | Linearity | Linear.idr (QTT q=1) | Erased (QTT) | ECHIDNA 10^4 | **Proven [sfap], erased. Propositional state-machine theorems added A3 (2026-04-18): distinctUsage, consumePreservesData, noReuse, noReuseEcho — usage-indexed handle `LinHandleU Fresh/Consumed tok` with `consume` state transition, alongside the QTT structural layer.** |
5555
| 11 | Tropical cost-tracking | Tropical.idr | Not yet | None | **In package (A1, 2026-04-18). Commutative-semiring closure PROVEN (A2, 2026-04-18): all 12 axioms — tropAddLeftId/RightId/Comm/Assoc, tropMulLeftId/RightId/Comm/Assoc, tropMulLeftAnn/RightAnn, tropMulDistrib/DistribR. Uses structural `tropMin` (007-lang template). Zero dangerous patterns.** |

‎src/abi/TypedWasm/ABI/Effects.idr‎

Lines changed: 109 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -204,6 +204,115 @@ effectSubsumesRefl [] = SubNil
204204
effectSubsumesRefl (x :: rest) =
205205
SubCons EffHere (effectWeaken (effectSubsumesRefl rest))
206206

207+
||| PROOF-NEEDS §P0.4 alias for `effectSubsumesRefl`.
208+
public export
209+
subsumeRefl : (xs : EffectSet) -> EffectSubsumes xs xs
210+
subsumeRefl = effectSubsumesRefl
211+
212+
-- ============================================================================
213+
-- Transitivity + Composition (PROOF-NEEDS §P0.4)
214+
-- ============================================================================
215+
--
216+
-- The reflexivity and weakening lemmas above together with `combineSub`
217+
-- give a partial story. This block adds the remaining two preorder /
218+
-- composition theorems requested by PROOF-NEEDS §P0.4:
219+
--
220+
-- subsumeTrans — transitivity of subsumption.
221+
-- subsumeCompose — when two operations are sequenced, their combined
222+
-- actual effects are subsumed by the combined
223+
-- declared effects.
224+
--
225+
-- Both are used by the attestation layer in Proofs.idr so that an L8
226+
-- attestation can be built compositionally from per-operation proofs
227+
-- rather than re-verifying the monolithic set each time.
228+
229+
||| Membership-lifting lemma: if `e` is in `ys` and `ys` is subsumed by
230+
||| `xs`, then `e` is in `xs`. This is the step that makes subsumption
231+
||| transitive: a membership proof in the middle set gets lifted by the
232+
||| per-element witnesses stored in the subsumption chain.
233+
public export
234+
hasEffectTrans : {ys : EffectSet} ->
235+
HasEffect e ys ->
236+
EffectSubsumes xs ys ->
237+
HasEffect e xs
238+
hasEffectTrans EffHere (SubCons h _) = h
239+
hasEffectTrans (EffThere p) (SubCons _ s) = hasEffectTrans p s
240+
241+
||| Subsumption is transitive: if zs ⊆ ys and ys ⊆ xs, then zs ⊆ xs.
242+
|||
243+
||| Together with `subsumeRefl`, this makes `EffectSubsumes` a preorder
244+
||| on `EffectSet`.
245+
public export
246+
subsumeTrans : {ys : EffectSet} ->
247+
EffectSubsumes xs ys ->
248+
EffectSubsumes ys zs ->
249+
EffectSubsumes xs zs
250+
subsumeTrans _ SubNil = SubNil
251+
subsumeTrans sxy (SubCons hez syz) =
252+
SubCons (hasEffectTrans hez sxy) (subsumeTrans sxy syz)
253+
254+
-- ---- Append-preservation for HasEffect ----
255+
256+
||| Membership on the left: if `e` is in `xs`, then `e` is in
257+
||| `combineEffects xs ys`.
258+
public export
259+
hasEffectCombineL : {xs : EffectSet} ->
260+
HasEffect e xs ->
261+
HasEffect e (combineEffects xs ys)
262+
hasEffectCombineL {xs = (_ :: _)} EffHere = EffHere
263+
hasEffectCombineL {xs = (_ :: _)} (EffThere p) = EffThere (hasEffectCombineL p)
264+
265+
||| Membership on the right: if `e` is in `ys`, then `e` is in
266+
||| `combineEffects xs ys`.
267+
public export
268+
hasEffectCombineR : {xs : EffectSet} ->
269+
HasEffect e ys ->
270+
HasEffect e (combineEffects xs ys)
271+
hasEffectCombineR {xs = []} p = p
272+
hasEffectCombineR {xs = (_ :: _)} p = EffThere (hasEffectCombineR p)
273+
274+
-- ---- Compositional weakening ----
275+
276+
||| Prepending declared effects preserves subsumption of the actual set.
277+
||| If `actual ⊆ d2`, then `actual ⊆ (d1 ++ d2)`.
278+
public export
279+
subsumePrepend : {d1 : EffectSet} ->
280+
EffectSubsumes d2 actual ->
281+
EffectSubsumes (combineEffects d1 d2) actual
282+
subsumePrepend SubNil = SubNil
283+
subsumePrepend (SubCons h rest) =
284+
SubCons (hasEffectCombineR h) (subsumePrepend rest)
285+
286+
||| Appending declared effects preserves subsumption of the actual set.
287+
||| If `actual ⊆ d1`, then `actual ⊆ (d1 ++ d2)`.
288+
public export
289+
subsumeAppend : {d1 : EffectSet} ->
290+
EffectSubsumes d1 actual ->
291+
EffectSubsumes (combineEffects d1 d2) actual
292+
subsumeAppend SubNil = SubNil
293+
subsumeAppend (SubCons h rest) =
294+
SubCons (hasEffectCombineL h) (subsumeAppend rest)
295+
296+
||| The composition theorem: when two operations are sequenced, the
297+
||| combined actual effects are subsumed by the combined declared
298+
||| effects.
299+
|||
300+
||| PROOF-NEEDS §P0.4 stated as:
301+
||| EffectSubsumes d1 a1 -> EffectSubsumes d2 a2 ->
302+
||| EffectSubsumes (d1 ++ d2) (a1 ++ a2)
303+
|||
304+
||| Without this the L8 attestation would have to re-verify the whole
305+
||| effect set for every compound operation. With it, attestations
306+
||| compose.
307+
public export
308+
subsumeCompose : {d1 : EffectSet} ->
309+
EffectSubsumes d1 a1 ->
310+
EffectSubsumes d2 a2 ->
311+
EffectSubsumes (combineEffects d1 d2) (combineEffects a1 a2)
312+
subsumeCompose SubNil s2 = subsumePrepend s2
313+
subsumeCompose (SubCons h r) s2 =
314+
SubCons (hasEffectCombineL h) (subsumeCompose r s2)
315+
207316
-- ============================================================================
208317
-- Effectful Operation Type
209318
-- ============================================================================

0 commit comments

Comments
 (0)