Typecheck-shortcut-laws
On this page
fx.experimental.desc-interp.effects.typecheck-shortcut-laws: kernel-checked one-shot lemmas certifying each typecheck handler on the canonical report op reduces to its shortcut residual (pair newState tt for the resume strategies; a Sum inl/inr for strict). Each discharges by H.refl — ι on EffTypeCheck.elim fires the single report branch, β binds the four fields + state, and the step's boolElim at a concrete passed selects the arm. RHSes match the extract.PairRaw/Resume/Abort emitter outputs, anchoring per-strategy shortcut soundness at the kernel layer. firstN-fail splits on the stuck down-counter (suc/zero); summarize/summarize-assoc fail keep the reason symbolic (one lemma per variant covers all tokens).
collectingFail
Proof of collecting-fail: 5 lams + H.refl. A fail conses the residue (RHS via consAtExplicit).
collectingFailTy
Π-type of collecting-fail: … (report … false) s ≡ H.pair (cons carrier s) tt.
collectingPass
Proof of collecting-pass: 5 lams + H.refl. A pass keeps the accumulator.
collectingPassTy
Π-type of collecting-pass: Π R reason path carrier. Π s:List R. handle_collecting R (report reason path carrier true) s ≡ H.pair s tt.
firstNFailSuc
Proof of firstN-fail-suc: 6 lams + H.refl. The recorded list is annotated (the ind step body is synthesized, so a bare cons carries no element type).
firstNFailSucTy
Π-type of firstN-fail at remaining = suc rp: … (report … false) (pair coll (suc rp)) ≡ H.pair (pair (cons carrier coll) rp) tt — record and decrement.
firstNFailZero
Proof of firstN-fail-zero: 5 lams + H.refl.
firstNFailZeroTy
Π-type of firstN-fail at remaining = zero: … (report … false) (pair coll zero) ≡ H.pair (pair coll zero) tt — drop and hold (the abort state).
firstNPass
Proof of firstN-pass: 5 lams + H.refl.
firstNPassTy
Π-type of firstN-pass: … handle_firstN R (report … true) s ≡ H.pair s tt (no ind; the state is returned).
loggingFail
Proof of logging-fail: 5 lams + H.refl.
loggingFailTy
Π-type of logging-fail: … (report … false) s ≡ H.pair (cons (pair false carrier) s) tt.
loggingPass
Proof of logging-pass: 5 lams + H.refl. Every decision is recorded; the outcome rides in the record.
loggingPassTy
Π-type of logging-pass: … handle_logging R (report … true) s ≡ H.pair (cons (pair true carrier) s) tt.
prettyFail
Proof of pretty-fail: 5 lams + H.refl.
prettyFailTy
Π-type of pretty-fail: … (report … false) s ≡ H.pair (cons carrier s) tt (the host-rendered line rides in carrier).
prettyPass
Proof of pretty-pass: 5 lams + H.refl.
prettyPassTy
Π-type of pretty-pass: same shape as collecting-pass (H.pair s tt).
strictFail
Proof of strict-fail: 5 lams + H.refl.
strictFailTy
Π-type of strict-fail: … (report … false) s ≡ inr strictLeft (strictRight R) (pair carrier s) — surrender the residue down the right summand (the throw channel).
strictPass
Proof of strict-pass: 5 lams + H.refl.
strictPassTy
Π-type of strict-pass: … handle_strict R (report … true) s ≡ inl strictLeft (strictRight R) (pair tt s) — resume down the left summand.
summarizeAssocFail
Proof of summarize-assoc-fail: 7 lams + H.refl.
summarizeAssocFailTy
Π-type of summarize-assoc-fail (reason symbolic): … (report reason … false) (pair br (pair pt ft)) ≡ H.pair (pair (insertOrIncrement (reasonName reason) br) (pair pt (suc ft))) tt.
summarizeAssocPass
Proof of summarize-assoc-pass: 7 lams + H.refl.
summarizeAssocPassTy
Π-type of summarize-assoc-pass: … handle_summarizeAssoc R (report … true) (pair br (pair pt ft)) ≡ H.pair (pair br (pair (suc pt) ft)) tt.
summarizeFail
Proof of summarize-fail: 7 lams + H.refl.
summarizeFailTy
Π-type of summarize-fail (reason symbolic): … (report reason … false) (pair br (pair pt ft)) ≡ H.pair (pair (bumpReason reason br) (pair pt (suc ft))) tt. bumpReason reason br stays neutral on both sides, so one lemma covers every reason.
summarizePass
Proof of summarize-pass: 7 lams + H.refl.
summarizePassTy
Π-type of summarize-pass: … handle_summarize R (report … true) (pair br (pair pt ft)) ≡ H.pair (pair br (pair (suc pt) ft)) tt — bump the passed total.