proof(idris2): tighten Ephapax.IR.Decode to %default total#96
Merged
Conversation
Flip %default partial -> total. Net upgrade: about 22 atomic
encode/decode helpers (baseToAtom, atomToBase, linearityToAtom,
binopToAtom, unaryToAtom, encodeLit, decodeLit, encodeTy, decodeTy,
escape/escape.go, unescape/unescape.decode, encodeParam, decodeParam,
and reverse maps) are now provably total under the file default.
7 functions retain `covering` (an explicit "exhaustive but termination
deferred" marker, strictly stronger than the previous file default of
partial -- no new escape) for two distinct Idris2 0.8.0 limits:
- encodeExpr / decodeExpr: structural recursion through
`map encodeExpr` and `traverse decodeExpr` on List Expr (the Block
case). The recursion IS structural by induction on the Expr tree
via list head/tail, but Idris2 SCT cannot trace the size decrease
across the Functor/Traversable dictionary. Same root cause as the
AST.idr Show/Eq covering markers (PR #94).
- encodeDecl, decodeDecl, fromSExpr, toSExpr: transitively call the
above; inherit covering.
- encode: encode = show . toSExpr -- depends on Ephapax.IR.SExpr.show
totality, which lands separately in PR #89 (SExpr.idr partial->total).
Will become provably total once #89 merges.
No assert_total / believe_me. Downstream Parse/Parser and Affine/Emit
both still build clean.
Refs #124 (proof-debt epic), #134 (ephapax totality)
Part of ephapax %default partial -> total campaign: 6/9 files done
(SExpr PR #89; Stream PR #90; Util PR #91; Lexer PR #93; AST PR #94;
Decode here).
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This was referenced May 20, 2026
hyperpolymath
added a commit
that referenced
this pull request
May 20, 2026
## Summary Seventh file in the `%default partial` → `%default total` chain. Companions: SExpr (#89), Stream (#90), Util (#91), Lexer (#93), AST (#94), Decode (#96). Two changes, atomically: ### 1. Fix pre-existing baseline rot Lines 184–186 had a 3-line layout for `if-then-else` that Idris2 0.8.0 rejects with `Expected 'else'`: ```idris if not (isLinear tv) then Left (LetLinNonLinear name tv) else do ... ``` Reformatted to single-line `if X then Y else do` — matching the same-pattern usage at line 246–255 in the same file (the `If c t f` branch). The file now compiles for the first time on the current Idris2 toolchain. **This is independent of the totality work but cannot be separated** — without the layout fix the file does not parse and no totality check can run. ### 2. Flip `%default partial → %default total` No further changes needed. The `check` function's structural recursion through pattern destructuring (sub-Exprs of compound forms like `StringConcat a b → check ... a; check ... b`) and the mutual `check`/`checkBlock`/`numeric`/`litTy` forward-declaration block are all accepted by Idris2 0.8.0 SCT as terminating. No `assert_total` / `believe_me` / `covering` escapes anywhere. **Every definition in the file is now provably total** — including `check` (Expr typechecker), `checkBlock`, `mergeAffine`, `mergeLinear` (and inner `findMismatch`), `checkModule` (and inner `addFn` / `checkDecls`). ## Verification ``` $ IDRIS2_PREFIX=…/idris2/0.8.0 idris2 --check Ephapax/Affine/Typecheck.idr 2/2: Building Ephapax.Affine.Typecheck (Ephapax/Affine/Typecheck.idr) $ idris2 --check Ephapax/Affine/Emit.idr # downstream 4/4: Building Ephapax.Affine.Emit ``` ## Refs - `#124` (proof-debt audit epic) - `#134` (ephapax totality sub-issue) - Companions: PR `#89` (SExpr), `#90` (Stream), `#91` (Util), `#93` (Lexer), `#94` (AST), `#96` (Decode) ## Test plan - [x] `idris2 --check Ephapax/Affine/Typecheck.idr` builds green under `%default total` - [x] Downstream `Ephapax.Affine.Emit` still builds - [ ] CI green - [x] No `assert_*` / `believe_me` / `covering` — every definition is provably total 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
hyperpolymath
added a commit
that referenced
this pull request
May 20, 2026
## Summary Eighth file in the `%default partial` → totality-tightening chain. Companions: SExpr (#89), Stream (#90), Util (#91), Lexer (#93), AST (#94), Decode (#96), Typecheck (#97). **Distinct outcome for this file**: lands as `%default covering` rather than `%default total`. ## Why covering, not total `Parser.idr` is a hand-written recursive-descent parser with ~30 mutually-recursive `Parser X = Stream → Either ParseError (X, Stream)` combinators. Every parser function consumes ≥1 token from the input stream on success, but the recursion is on a `Stream` record (Int-indexed token buffer), not on a structural recursor. Idris2 0.8.0 SCT cannot trace termination through Int-indexed records. The errors form one large mutual cycle: ``` parseModule → parseDecls → parseDecl → parseFnDecl → parseFnAfterParams → parseType → parseSumType → sepBy1 (Util) → sepTail → ... → parseExpr → parseLambda → parseType (back to top) ``` Fuel-converting every combinator (the pattern used in SExpr / Stream / Util / Lexer) would require: - adding a `Nat` fuel parameter to ~30 function signatures - updating ~150 call sites - threading fuel through `where`-bound mutual blocks (`parsePostfix.{parseCall, parseFst, parseSnd, parsePostfixTail}`, `parseBlock.{parseBlockExpr, parseBlockTail}`, `parseExpr.{parseLetKw, ...}`, etc.) - introducing a top-level fuel computed from `bufLen` at every `parseModuleTokens` entry Substantially larger than the other 7 files combined. Chose the pragmatic intermediate annotation. `covering` is **strictly stronger** than the previous `partial`: it asserts exhaustive pattern matching has been verified (it has); only termination is deferred. No `assert_total` / `believe_me`. This is the truthful annotation for an LL(k) recursive-descent parser whose recursive structure is the *input grammar*, not the *input data*. ## Verification ``` $ IDRIS2_PREFIX=…/idris2/0.8.0 idris2 --check Ephapax/Parse/Parser.idr 6/6: Building Ephapax.Parse.Parser (Ephapax/Parse/Parser.idr) ``` ## Cross-PR dependency note Downstream `Main.idr` does not yet compile on `origin/main` due to a **pre-existing** baseline-rot parse error in `Ephapax.Affine.Typecheck.idr` (lines 184–186, 3-line `if-then-else` layout Idris2 0.8.0 rejects). That bug is fixed independently in PR #97. **Unrelated to this PR's scope** — `Parser.idr` itself builds clean in isolation; the merge ordering issue clears once #97 lands. ## Refs - `#124` (proof-debt audit epic) - `#134` (ephapax totality sub-issue) - Companions: PR `#89` (SExpr), `#90` (Stream), `#91` (Util), `#93` (Lexer), `#94` (AST), `#96` (Decode), `#97` (Typecheck) ## Test plan - [x] `idris2 --check Ephapax/Parse/Parser.idr` builds green under `%default covering` - [ ] CI green - [x] No `assert_*` / `believe_me`; `covering` annotation is justified above 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
hyperpolymath
added a commit
that referenced
this pull request
May 20, 2026
## Summary **Ninth and final file** in the ephapax `%default partial` → totality-tightening campaign. After this lands together with the rest, no `%default partial` remains anywhere in `ephapax/idris2/src/Ephapax/`. The file is a one-line wrapper: ```idris emitModule : Module -> String emitModule = encode ``` Its totality is exactly `Ephapax.IR.Decode.encode`'s. On the chain's exit state (with PR #96 merged), `encode` is `covering` — the `show . toSExpr` pipeline inherits `covering` from Decode's recursive `encode`/`decode` functions (justified in #96's body). Mark `emitModule` `covering` to match. Flip file default `%default partial → %default total`. The `covering` modifier on the one defined function is the entirety of the "escape" footprint — explicit, narrow, justified. No `assert_total` / `believe_me`. ## Verification ``` $ IDRIS2_PREFIX=…/idris2/0.8.0 idris2 --check Ephapax/Affine/Emit.idr 1/4: Building Ephapax.IR.SExpr 2/4: Building Ephapax.IR.AST 3/4: Building Ephapax.IR.Decode 4/4: Building Ephapax.Affine.Emit ``` ## Refs — the full campaign - `#124` (proof-debt audit epic) - `#134` (ephapax totality sub-issue) | # | File | PR | Annotation outcome | |---|---|---|---| | 1 | `IR/SExpr.idr` | #89 | `%default total`, fueled mutual parser | | 2 | `Parse/Stream.idr` | #90 | `%default total`, fueled `remaining/build` | | 3 | `Parse/Util.idr` | #91 | `%default total`, fueled `many` + `sepBy.sepTail` | | 4 | `Parse/Lexer.idr` | #93 | `%default total`, fueled `lex.go` (57 call sites) | | 5 | `IR/AST.idr` | #94 | `%default total` + 6 retained `covering` (showPrec/(/=) loop) | | 6 | `IR/Decode.idr` | #96 | `%default total` + 7 `covering` (map/traverse SCT limit) | | 7 | `Affine/Typecheck.idr` | #97 | `%default total` + pre-existing baseline-rot layout fix | | 8 | `Parse/Parser.idr` | #99 | `%default covering` (LL(k) Stream-recursion, ~30 fns, large refactor deferred) | | 9 | `Affine/Emit.idr` | **this** | `%default total` + 1 `covering` (inherits from Decode.encode) | ## Test plan - [x] `idris2 --check Ephapax/Affine/Emit.idr` builds green under `%default total` - [ ] CI green - [x] No `assert_*` / `believe_me`; only `covering` on `emitModule` (matches dependency) 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
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.
Summary
Sixth file in the
%default partial→%default totalchain. Companions: SExpr (#89), Stream (#90), Util (#91), Lexer (#93), AST (#94).Flip
%default partial → %default total. Roughly 22 atomic encode/decode helpers (thebaseToAtom/atomToBasestyle maps,encodeLit/decodeLit,encodeTy/decodeTy,escape/unescape,encodeParam/decodeParam, etc.) are now provably total under the file default.7
coveringmarkers retainedTwo distinct Idris2 0.8.0 limits force this:
encodeExpr/decodeExpr— structural recursion runs throughmap encodeExpr esandtraverse decodeExpr restfor theBlockcase. The recursion is structural via list head/tail induction on aList Expr, but Idris2 SCT cannot trace the size decrease across theFunctor/Traversabledictionary call. Same root cause as the existingShow Expr/Eq Exprcoveringmarkers in AST.idr (proof(idris2): tighten Ephapax.IR.AST to %default total #94).encodeDecl/decodeDecl/fromSExpr/toSExpr— transitively call the two above; inheritcovering.encode—encode = show . toSExprdepends onEphapax.IR.SExpr.showtotality, which lands in PR proof(idris2): tighten Ephapax.IR.SExpr to %default total via fueled mutual parser #89. After proof(idris2): tighten Ephapax.IR.SExpr to %default total via fueled mutual parser #89 merges,encodewould still becoveringfromtoSExpr.coveringis strictly stronger than the previous file default ofpartial— no new escape. Noassert_total/believe_me.Verification
Refs
#124(proof-debt audit epic)#134(ephapax totality sub-issue)#89(SExpr),#90(Stream),#91(Util),#93(Lexer),#94(AST)Test plan
idris2 --check Ephapax/IR/Decode.idrbuilds green under%default totalassert_*/believe_me; only 7 deliberatecoveringmarkers (justified above)🤖 Generated with Claude Code