proof(idris2): tighten Ephapax.Parse.Lexer to %default total by hyperpolymath · Pull Request #93 · hyperpolymath/ephapax

hyperpolymath · 2026-05-20T17:19:49Z

Summary

Fourth file in the %default partial → %default total chain. Companions: PR #89 (SExpr), #90 (Stream), #91 (Util).

Ephapax.Parse.Lexer.lex.go : Pos -> List Char -> List Token -> ... is a hand-written tokeniser that slices the input via span / pattern destructuring and recurses on the tail. Idris2 can't track that each branch's tail / more / rest3 is structurally smaller than the original list, so the totality checker rejects go (and lex transitively).

Fix: add a Nat fuel parameter to go. Fuel = length (unpack input) at entry (set in lex). Every recursive call decrements fuel by 1 and consumes ≥ 1 character of input — the well-formed assumption every Lexer branch already satisfies. All 57 recursive go-call sites updated mechanically (bulk sed within the where-block, then spot-fixed two pattern-declaration over-applications).

readString.goStr is already structurally total (recurses on the tail of a pattern-match list) and required no fuel. advanceN likewise.

Soundness

On every well-formed input, fuel exhausts at or after the input list does — so behaviour is identical to the partial original. A degenerate non-consuming branch (which Lexer does not contain) would loop forever in the partial form and return truncated output in the fueled form — strictly safer.

No assert_total / assert_smaller / believe_me escapes.

Verification

$ IDRIS2_PREFIX=…/idris2/0.8.0 idris2 --check Ephapax/Parse/Lexer.idr
1/1: Building Ephapax.Parse.Lexer (Ephapax/Parse/Lexer.idr)
$ idris2 --check Ephapax/Parse/Parser.idr   # downstream
6/6: Building Ephapax.Parse.Parser (Ephapax/Parse/Parser.idr)

Refs

#124 (proof-debt audit epic)
#134 (ephapax totality sub-issue)
Companions: PR #89 (SExpr), #90 (Stream), #91 (Util)

Test plan

idris2 --check Ephapax/Parse/Lexer.idr builds green under %default total
Downstream Ephapax.Parse.Parser (transitive Stream / Util) still builds
CI green
No assert_* / believe_me introduced (verified — inspect the diff)

🤖 Generated with Claude Code

The where-bound lex.go : Pos -> List Char -> List Token -> ... ran a hand-written tokeniser by recursing on a List Char that was sliced piecewise via `span` / pattern destructuring. Idris2 cannot track that each branch's "tail" is structurally smaller than the input, so the totality checker rejected go (and lex transitively). Add a Nat fuel parameter to go. Fuel = `length (unpack input)` at entry (set in lex). Every recursive call decrements fuel by one and consumes >=1 char of input (well-formed assumption: every Lexer branch advances past at least one character). All 57 recursive go-call sites updated mechanically (bulk sed within the where-block). readString.goStr was already structurally total (recurses on the tail of a pattern-match list) and required no fuel. advanceN likewise. Soundness: on every well-formed input, fuel exhausts at-or-after the input list does, so behaviour is identical to the partial original. A degenerate non-consuming branch (which the original Lexer does not contain) would loop forever in the partial form and return truncated output in the fueled form -- strictly safer. No assert_total / assert_smaller / believe_me escapes. Downstream Ephapax.Parse.Parser, Stream, Util all still build clean. Refs #124 (proof-debt epic), #134 (ephapax totality) Part of ephapax %default partial -> total campaign: 4/9 files done (SExpr.idr PR #89; Stream.idr PR #90; Util.idr PR #91; Lexer.idr here). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

## Summary Fifth file in the `%default partial` → `%default total` chain. Single-line change: `%default partial` → `%default total`. The 6 `covering` markers already in the file (Eq Expr, Show Expr, Eq Decl, Show Decl, Eq Module, Show Module) cover the interface-dispatch totality blind spot Idris2 0.8.0 has around the `showPrec` / `(/=)` defaults across nested data instances — those markers stay, nothing new is added. I verified empirically: removing the existing `covering` markers, even one at a time, makes the build fail with `showPrec -> show -> showPrec -> show` (Show side) and `(/=) -> (==) -> (/=) -> (==)` (Eq side) loops. These are *not* unsoundness; the recursion is genuinely structural. Idris2 just can't trace the decrease through the interface defaults. `covering` is the project's existing escape and stays. ## What gets stricter About ten previously-implicitly-partial definitions are now provably total under the file default: `Eq Linearity`, `Eq BaseTy`, `Eq Ty`, `Eq Literal`, `Eq BinOp`, `Eq UnaryOp`, the matching `Show` instances, and `isLinear`. The data-only declarations are unaffected. No `assert_total` / `believe_me` escapes. ## Verification ``` $ IDRIS2_PREFIX=…/idris2/0.8.0 idris2 --check Ephapax/IR/AST.idr 1/1: Building Ephapax.IR.AST (Ephapax/IR/AST.idr) $ idris2 --check Ephapax/Parse/Parser.idr # downstream 6/6: Building Ephapax.Parse.Parser (Ephapax/Parse/Parser.idr) ``` ## Refs - `#124` (proof-debt audit epic) - `#134` (ephapax totality sub-issue) - Companions: PR `#89` (SExpr), `#90` (Stream), `#91` (Util), `#93` (Lexer) ## Test plan - [x] `idris2 --check Ephapax/IR/AST.idr` builds green under `%default total` - [x] Downstream `Ephapax.Parse.Parser` still builds - [ ] CI green - [x] No new `covering` markers; no `assert_*` / `believe_me` 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

## Summary Sixth file in the `%default partial` → `%default total` chain. Companions: SExpr (#89), Stream (#90), Util (#91), Lexer (#93), AST (#94). Flip `%default partial → %default total`. Roughly 22 atomic encode/decode helpers (the `baseToAtom`/`atomToBase` style maps, `encodeLit`/`decodeLit`, `encodeTy`/`decodeTy`, `escape`/`unescape`, `encodeParam`/`decodeParam`, etc.) are now provably total under the file default. ## 7 `covering` markers retained Two distinct Idris2 0.8.0 limits force this: 1. **`encodeExpr` / `decodeExpr`** — structural recursion runs through `map encodeExpr es` and `traverse decodeExpr rest` for the `Block` case. The recursion *is* structural via list head/tail induction on a `List Expr`, but Idris2 SCT cannot trace the size decrease across the `Functor` / `Traversable` dictionary call. Same root cause as the existing `Show Expr` / `Eq Expr` `covering` markers in AST.idr (#94). 2. **`encodeDecl` / `decodeDecl` / `fromSExpr` / `toSExpr`** — transitively call the two above; inherit `covering`. 3. **`encode`** — `encode = show . toSExpr` depends on `Ephapax.IR.SExpr.show` totality, which lands in PR #89. After #89 merges, `encode` would still be `covering` from `toSExpr`. `covering` is strictly stronger than the previous file default of `partial` — no new escape. No `assert_total` / `believe_me`. ## Verification ``` $ IDRIS2_PREFIX=…/idris2/0.8.0 idris2 --check Ephapax/IR/Decode.idr 3/3: Building Ephapax.IR.Decode (Ephapax/IR/Decode.idr) $ idris2 --check Ephapax/Parse/Parser.idr # downstream 6/6: Building Ephapax.Parse.Parser $ 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) ## Test plan - [x] `idris2 --check Ephapax/IR/Decode.idr` builds green under `%default total` - [x] Downstream Parse/Parser + Affine/Emit still build - [ ] CI green - [x] No `assert_*` / `believe_me`; only 7 deliberate `covering` markers (justified above) 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

## 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>

## 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>

## 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>

github-actions · 2026-05-21T11:48:59Z

🔍 Hypatia Security Scan

Findings: 29 issues detected

Severity	Count
🔴 Critical	7
🟠 High	6
🟡 Medium	16

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Issue in quality.yml",
    "type": "missing_workflow",
    "file": "quality.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in security-policy.yml",
    "type": "missing_workflow",
    "file": "security-policy.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action hyperpolymath/standards/.github/workflows/governance-reusable.yml@main needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Admitted leaves proof hole (1 occurrences, CWE-704)",
    "type": "admitted",
    "file": "/home/runner/work/ephapax/ephapax/formal/Semantics.v",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "reason": "Coq admit tactic leaves goal unproven (2 occurrences, CWE-704)",
    "type": "coq_admit_tactic",
    "file": "/home/runner/work/ephapax/ephapax/formal/Semantics.v",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "reason": "believe_me undermines formal verification (1 occurrences, CWE-704)",
    "type": "believe_me",
    "file": "/home/runner/work/ephapax/ephapax/src/formal/Ephapax/Formal/RegionLinear.idr",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "reason": "assert_total bypasses totality checker (1 occurrences, CWE-704)",
    "type": "assert_total",
    "file": "/home/runner/work/ephapax/ephapax/src/formal/Ephapax/Formal/RegionLinear.idr",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  },
  {
    "reason": "expect() in hot path (1 occurrences, CWE-754)",
    "type": "expect_in_hot_path",
    "file": "/home/runner/work/ephapax/ephapax/src/ephapax-repl/src/lib.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "from_raw constructs types from raw pointers without safety checks (1 occurrences, CWE-676)",
    "type": "from_raw",
    "file": "/home/runner/work/ephapax/ephapax/src/ephapax-vram-cache/src/lib.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  },
  {
    "reason": "unwrap() without prior check -- DoS via panic (8 occurrences, CWE-754)",
    "type": "unwrap_without_check",
    "file": "/home/runner/work/ephapax/ephapax/src/ephapax-vram-cache/benches/cache_bench.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

Merge branch 'main' into proof-debt/ephapax-lexer-totality

86cc108

hyperpolymath marked this pull request as ready for review May 20, 2026 17:29

hyperpolymath merged commit 52079a7 into main May 20, 2026
2 of 8 checks passed

hyperpolymath deleted the proof-debt/ephapax-lexer-totality branch May 20, 2026 17:29

hyperpolymath mentioned this pull request May 20, 2026

proof(idris2): tighten Ephapax.IR.Decode to %default total #96

Merged

4 tasks

This was referenced May 20, 2026

proof(idris2): tighten Ephapax.Affine.Typecheck to %default total #97

Merged

proof(idris2): tighten Ephapax.Parse.Parser to %default covering #99

Merged

proof(idris2): tighten Ephapax.Affine.Emit to %default total #100

Merged

hyperpolymath mentioned this pull request May 20, 2026

[P2] ephapax: 11 partial + add ABI seam (Rust/SPARK NON-COMPLIANT) hyperpolymath/standards#134

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

proof(idris2): tighten Ephapax.Parse.Lexer to %default total#93

proof(idris2): tighten Ephapax.Parse.Lexer to %default total#93
hyperpolymath merged 2 commits into
mainfrom
proof-debt/ephapax-lexer-totality

hyperpolymath commented May 20, 2026

Uh oh!

Uh oh!

github-actions Bot commented May 21, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

hyperpolymath commented May 20, 2026

Summary

Soundness

Verification

Refs

Test plan

Uh oh!

Uh oh!

github-actions Bot commented May 21, 2026

🔍 Hypatia Security Scan

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant