proof(idris2): tighten Ephapax.IR.SExpr to %default total via fueled mutual parser by hyperpolymath · Pull Request #89 · hyperpolymath/ephapax

hyperpolymath · 2026-05-20T16:32:33Z

Summary

First step of the hyperpolymath/standards#134 totality tightening campaign. Ephapax.IR.SExpr was one of 9 ephapax Idris2 source files declared %default partial. This PR converts it to %default total without any proof escapes.

Root cause of the partiality

The mutual parseExpr / parseList (plus its where-bound go) thread List Char through dropWhile and parser-returned remainders. Idris2 0.8.0's structural termination checker cannot prove these recursive arguments smaller.

Resolution (no `assert_total`, no `assert_smaller`)

Introduced explicit Nat fuel parameters: parseExprFuel, parseListFuel, listGo. Each recursive call decrements S k → k, giving Idris2 a structural decreasing measure.
Lifted the original inner go to a top-level listGo in the same mutual block, so its fuel can participate in mutual termination (an inner where cannot).
Public parse wrapper seeds fuel from length (unpack input). Sound: every successful primitive parser (parseAtom, parseString, '(' / ')' tokens) consumes at least one character, so the input-length bound cannot be exceeded by any valid parse.

Verification

idris2 --check Ephapax/IR/SExpr.idr from idris2/src/ → exit 0 (Idris2 0.8.0).
No remaining partial annotations, no assert_smaller, no assert_total.
Show SExpr retains its original covering annotation — that's a coverage-only relaxation that was already in place under %default partial, unaffected by this change.

What this does NOT close

8 other ephapax source files under idris2/src/Ephapax/ still carry %default partial (IR/AST.idr, IR/Decode.idr, Parse/Lexer.idr, Parse/Util.idr, Parse/Stream.idr, Parse/Parser.idr, Affine/Typecheck.idr, Affine/Emit.idr). They can be tackled one chain at a time using the same fueled-mutual-recursion pattern this PR establishes.

Refs hyperpolymath/standards#124
Refs hyperpolymath/standards#134

🤖 Generated with Claude Code

…mutual parser (#134) First step of the #134 totality tightening campaign. The S-expression parser previously used a `%default partial` directive because the mutual recursion between [parseExpr] and [parseList] (plus its inner `where`-bound `go`) had no structural termination measure visible to Idris2 0.8.0 — the recursive calls thread a `List Char` through [dropWhile] and parser-returned remainders, neither of which Idris2 can statically prove smaller. Resolution (no proof escapes, no [assert_total]): - Introduce explicit `Nat` fuel parameters on the mutual functions [parseExprFuel] / [parseListFuel] / [listGo]. Each recursive call decrements fuel from `S k → k`, giving Idris2 a structural decreasing measure. - Lift the original inner `go` to a top-level [listGo] in the same mutual block so its fuel can participate in the termination measure (an inner `where` cannot drive mutual termination). - Public [parse] wrapper seeds fuel from `length (unpack input)`. Sound because every successful primitive parser ([parseAtom], [parseString], the '(' / ')' tokens) consumes at least one character, so the input-length bound cannot be exceeded. File now compiles with `%default total` in effect; no remaining `partial` annotations and no `assert_smaller`/`assert_total`. Only [Show SExpr] retains the original `covering` (its `show` recurses on a list of `SExpr`, requiring a coverage-only check — that was already the case under `%default partial` and is unaffected). Verification: `idris2 --check Ephapax/IR/SExpr.idr` exit 0 from [idris2/src] under Idris2 0.8.0. Refs hyperpolymath/standards#124 Refs hyperpolymath/standards#134 🤖 Generated with [Claude Code](https://claude.com/claude-code) 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 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 - [x] `idris2 --check Ephapax/Parse/Lexer.idr` builds green under `%default total` - [x] Downstream `Ephapax.Parse.Parser` (transitive Stream / Util) still builds - [ ] CI green - [ ] No `assert_*` / `believe_me` introduced (verified — inspect the diff) 🤖 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 Second file in the `%default partial` → `%default total` chain for `ephapax/idris2/src/Ephapax/`. SExpr.idr (#89) was first; Stream.idr is this one. Only one definition in `Stream.idr` actually recurses: the `where`-bound `build` inside `remaining`. It walks an `Int` index up to `s.len` — Idris2 can't detect this as terminating because Int is not a structural recursor. Fix: replace `build` with a Nat-fueled helper `buildFuel`, with fuel `= integerToNat (s.len - s.index)`. Each recursive call decrements fuel by 1 and increments the index by 1 in lockstep, so the fuel can never run out before the `i >= s.len` guard fires. When `s.index >= s.len` the cast/truncation produces fuel 0 — matching the partial original's empty-return. No `assert_total` / `assert_smaller` / `believe_me` escapes anywhere. ## Verification ``` $ IDRIS2_PREFIX=…/idris2/0.8.0 idris2 --check Ephapax/Parse/Stream.idr 1/3: Building Ephapax.Parse.Lexer 2/3: Building Ephapax.Parse.ZigBuffer 3/3: Building Ephapax.Parse.Stream ``` Downstream `Ephapax.Parse.Parser` (which `import Ephapax.Parse.Stream`) also still builds clean — checked locally. ## Refs - `#124` (proof-debt audit epic) - `#134` (ephapax totality sub-issue) - Companion: PR `#89` (Ephapax.IR.SExpr — same campaign, file 1 of 9) ## Test plan - [x] `idris2 --check Ephapax/Parse/Stream.idr` builds green under `%default total` - [x] Downstream `Ephapax.Parse.Parser` still builds - [ ] CI green - [ ] No `assert_*` / `believe_me` introduced (verified by inspection — see diff) 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

## Summary Third file in the `%default partial` → `%default total` chain for `ephapax/idris2/src/Ephapax/`. SExpr.idr (#89) was first; Stream.idr (#90) second. Two combinators in `Util.idr` recurse unboundedly on a `Stream` rather than on a structural recursor: - `many : Parser a -> Parser (List a)` — repeated application until first failure - `sepBy.sepTail` — alternating separator + element Replace both with Nat-fueled siblings (`manyFuel` / `sepTailFuel`) where fuel `= integerToNat (cast (s.len - s.index))` — the count of remaining tokens in the input stream at entry. Each recursive call decrements fuel by 1, and the inner parser is assumed to consume ≥1 token per success (the only well-formed usage). `sepBy1` already delegates to `sepBy` and inherits totality for free. ## Soundness On a *consuming* inner parser (every real combinator client), the fueled form is observationally identical to the partial original: the stream is monotonically advancing, so the parser exhausts the stream before the fuel exhausts (in the common case it's tight equality — fuel = tokens-remaining). On a degenerate non-consuming inner parser, the partial original loops forever; the fueled form returns a truncated list. Strictly safer. No `assert_total` / `assert_smaller` / `believe_me` escapes. ## Verification ``` $ IDRIS2_PREFIX=…/idris2/0.8.0 idris2 --check Ephapax/Parse/Util.idr 4/4: Building Ephapax.Parse.Util (Ephapax/Parse/Util.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) - Companion: PR `#89` (SExpr — file 1), PR `#90` (Stream — file 2) ## Test plan - [x] `idris2 --check Ephapax/Parse/Util.idr` builds green under `%default total` - [x] Downstream `Ephapax.Parse.Parser` still builds - [ ] CI green - [ ] No `assert_*` / `believe_me` introduced (verified by inspection — see diff) 🤖 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-21T03:51:48Z

🔍 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

…122) Closure sweep after PR #116 took preservation from 22 → 12 open goals and PR #121 landed Phase 1 scaffold. Updates the preservation-count claims across docs to reflect 12, and adds a CHANGELOG entry summarising the full 2026-05-20 → 2026-05-21 reduction campaign. ## Files updated | File | What changed | |---|---| | `README.adoc` | Coq formal-foundations paragraph; reduction chain now lists all 8 PRs through #121; clear pointer to ROADMAP closure plan | | `ROADMAP.adoc` | Formal-proof status table row (`12 open goals`); v0.1 blocker entry; v1.0 status; 97.6% → 98.7% reduction figure | | `EXPLAINME.adoc` | Coq theorem table; reduction-story bullets extended through #114, #116, #121 | | `CHANGELOG.md` | New "Proof state" + "Documentation" sections under `[Unreleased]` tracking the full PR chain (#92, #102, #104, #106, #114, #115, #116, #117, #121) + the Idris2 totality campaign (#89–#100) + doc/wiki refresh (#113 + wiki) | ## Companion wiki update `Home.md`, `Proof-status.md`, `What-can-go-wrong.md` updated in the wiki repo with the same 22 → 12 figures + extended reduction story. Pushed separately to wiki master. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

This was referenced May 20, 2026

proof(idris2): tighten Ephapax.Parse.Stream to %default total #90

Merged

proof(idris2): tighten Ephapax.Parse.Util to %default total #91

Merged

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

Merged

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 marked this pull request as ready for review May 20, 2026 17:59

hyperpolymath merged commit 94a8d71 into main May 20, 2026
8 checks passed

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

hyperpolymath mentioned this pull request May 20, 2026

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

Open

hyperpolymath mentioned this pull request May 21, 2026

docs: refresh stale "22 open" → "12 open" + CHANGELOG closure entry #122

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

proof(idris2): tighten Ephapax.IR.SExpr to %default total via fueled mutual parser#89

proof(idris2): tighten Ephapax.IR.SExpr to %default total via fueled mutual parser#89
hyperpolymath merged 1 commit into
mainfrom
proof-debt/ephapax-sexpr-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

Root cause of the partiality

Resolution (no assert_total, no assert_smaller)

Verification

What this does NOT close

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

Resolution (no `assert_total`, no `assert_smaller`)