docs: honest framing of remaining ABI axioms (epic #87 Tier C item 11) by hyperpolymath · Pull Request #108 · hyperpolymath/boj-server

hyperpolymath · 2026-05-20T08:09:09Z

Summary

Module docstring on src/abi/Boj/SafetyLemmas.idr claimed "Three axiomatic believe_me primitives" while five live in the file. Corrected to enumerate all five and tag each to its underlying prim__* primitive.
appendLengthSum and substrLengthBound declarations used (x y : T) multi-binder syntax which Idris2 0.8.0 rejects at parse time ("Expected a type declaration" at the colon). Adding the comma — (x, y : T) — restores parsability. Types and proof terms are unchanged.
New == Formal verification section in README.adoc summarising posture so external readers don't have to dig through PROOF-NEEDS.md: all P1/P2 obligations closed; the 5 remaining axioms are principled assumptions over Idris2 primitives, not unproven debt.

Why this is a docs PR, not a discharge campaign

The 2026-05-18 audit in PROOF-NEEDS.md already classified every remaining believe_me as class (J) — genuinely unavoidable in Idris2 0.8.0 because Char / String are opaque primitives with no in-language induction principle. The reduction path is external backend-assurance (Chez/BEAM extraction), not constructive proof. Item 11 was therefore already done as research — just not surfaced honestly. This PR closes the documentation gap.

d2622566 proof(abi): reduce believe_me from 31 to 4 is where the "4 axioms canonical" framing originated; 4f729e7e and 0de09a47 later added appendLengthSum and substrLengthBound. Honest current count: 5.

Out of scope (deliberately)

src/abi/Boj/SafeAPIKey.idr has independent baseline rot: plusLteMonotone not found (likely stdlib rename — "did you mean transitive?") + a constraint-solver failure on logSafeBounded. Pre-existing, not introduced here. Worth a separate fix-up PR.
idris2 --build src/abi/boj.ipkg does not complete in 9 min on my dev box (gets SIGTERMed). Per-module idris2 --check is fast and was used for verification.
No CI workflow exercises the src/abi/boj.ipkg build today (.github/workflows/ only mentions idris2 in abi-drift.yml which uses a different tool). Wiring an idris2 build into CI is a separate concern.

Test plan

idris2 --check src/abi/Boj/SafetyLemmas.idr — green with my changes; previously red on origin/main due to the multi-binder parse error.
idris2 --check src/abi/Boj/Safety.idr — green (downstream consumer of charEqSound).
CI Hypatia neurosymbolic analysis + dogfood gate (will run on PR open).
Reviewer sanity-check on PROOF-NEEDS.md vs the new README posture.

Related branches / overlap to resolve

fix/proof-needs-reconcile-believe-me exists on remote (single commit 3d6b881c dated 2026-05-18, title says "reconcile believe_me audit — 5 justified axioms, not zero/4") but its diff does not touch PROOF-NEEDS.md, SafetyLemmas.idr, or README.adoc — looks abandoned. Worth a quick owner confirmation that this PR isn't displacing intentional work.

Refs epic #87 Tier C item 11. Item 12 (cross-cartridge composition proof) is a separate draft PR (ADR-0014 RFC).

🤖 Generated with Claude Code

The 2026-05-18 audit recorded in PROOF-NEEDS.md classified every remaining `believe_me` in the ABI safety layer as class (J) — a principled, irreducible assumption over Idris2 0.8.0's opaque `Char`/`String` primitives. The audit, however, left two stale artefacts behind: 1. `src/abi/Boj/SafetyLemmas.idr`'s module docstring still claimed "Three axiomatic believe_me primitives" while listing only 3 of the 5 that actually live in the file. The docstring now matches reality: 5 axioms, each enumerated, each tagged to its underlying `prim__*` primitive, with a one-line statement of why none of them can be discharged in-language. 2. The file did not actually type-check on Idris2 0.8.0. The `appendLengthSum` and `substrLengthBound` declarations used `(x y : T)` multi-binder syntax which this Idris2 build rejects ("Expected a type declaration." at the colon). Adding the comma — `(x, y : T)` — restores parsability; the types and proof terms are unchanged. Verified locally via `idris2 --check Boj/SafetyLemmas.idr` (green) and `Boj/Safety.idr` (green, downstream consumer of `charEqSound`). A new "Formal verification" section in README.adoc summarises the posture so external readers don't have to dig through PROOF-NEEDS to learn the framing: all P1/P2 obligations are closed with constructive proofs; the 5 remaining `believe_me` sites are principled assumptions over backend primitives, not unproven debt. Out of scope (independent baseline rot, deliberately not fixed in this PR): - `src/abi/Boj/SafeAPIKey.idr` fails `idris2 --check` on `plusLteMonotone` (renamed/moved in stdlib?) and a constraint-solver failure in `logSafeBounded`. Pre-existing, not introduced here. - `src/abi/boj.ipkg --build` doesn't complete in 9 min on this machine; the per-module `--check` of the modules I touched and their direct consumers does pass. Refs epic #87 Tier C item 11. Item 12 (cross-cartridge composition proof) is being drafted as a separate RFC ADR-0014. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

github-actions · 2026-05-20T08:10:06Z

🔍 Hypatia Security Scan

Findings: 31 issues detected

Severity	Count
🔴 Critical	19
🟠 High	5
🟡 Medium	7

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Stale AI session file -- delete",
    "type": "stale",
    "file": "GEMINI.md",
    "action": "delete",
    "rule_module": "root_hygiene",
    "severity": "medium"
  },
  {
    "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": "Python file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/boj-server/boj-server/.github/scripts/validate-eclexiaiser.py",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/boj-server/boj-server/cartridges/sanctify-mcp/adapter/mod.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/boj-server/boj-server/cartridges/academic-workflow-mcp/adapter/mod.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/boj-server/boj-server/cartridges/fireflag-mcp/adapter/mod.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/boj-server/boj-server/cartridges/ephapax-mcp/adapter/mod.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/boj-server/boj-server/cartridges/bofig-mcp/adapter/mod.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

github-actions · 2026-05-20T08:14:01Z

🔍 Hypatia Security Scan

Findings: 31 issues detected

Severity	Count
🔴 Critical	19
🟠 High	5
🟡 Medium	7

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Stale AI session file -- delete",
    "type": "stale",
    "file": "GEMINI.md",
    "action": "delete",
    "rule_module": "root_hygiene",
    "severity": "medium"
  },
  {
    "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": "Python file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/boj-server/boj-server/.github/scripts/validate-eclexiaiser.py",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/boj-server/boj-server/cartridges/sanctify-mcp/adapter/mod.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/boj-server/boj-server/cartridges/academic-workflow-mcp/adapter/mod.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/boj-server/boj-server/cartridges/fireflag-mcp/adapter/mod.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/boj-server/boj-server/cartridges/ephapax-mcp/adapter/mod.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/boj-server/boj-server/cartridges/bofig-mcp/adapter/mod.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

The pre-existing `logSafeBounded` proof in SafeAPIKey.idr did not type-check on the bundled Idris2 0.8.0. Audit-by-build (not by reading PROOF-NEEDS.md) was the only way to spot this. Three concrete defects, each fixed independently here: 1. **Removed local `plusLteMonotone` helper** which wrapped `lteTransitive (plusLteMonotoneRight _ lmn) (plusLteMonotoneLeft _ lpq)`. Idris2 0.8.0's `Data.Nat.plusLteMonotone` is exactly the shape we want (`LTE m n -> LTE p q -> LTE (m + p) (n + q)`), so the local wrapper is redundant. The wrapper called `lteTransitive` (no longer in stdlib — it's now `Control.Relation.transitive` and ambiguous in this import context) and passed wildcard arguments that didn't match the current `plusLteMonotoneRight` / `plusLteMonotoneLeft` signatures (`(p,q,r : Nat) -> LTE q r -> LTE (q+p) (r+p)`). Using stdlib directly sidesteps all of it. 2. **Lifted both branches out of the `with`-block.** Inside the with-block, the elaborator does not reduce `length "***"` (or `length "..."`) at type level — the goal is exposed as `LTE (integerToNat (prim__cast_IntInteger (prim__strLength (if ...)))) 11` with the `if`-arm unreduced. Outside the with-block the same lemmas type-check via `Refl`-equivalent computation. The fix: extract `logSafeBoundedShort` and `logSafeBoundedLong` as private helpers and let the with-block just dispatch. 3. **Right-associated the long-path proof.** `(++)` is right- associative in Idris (`a ++ b ++ c = a ++ (b ++ c)`), but the original proof bound `(p1 ++ "...") ++ p3` (left-associative) while the with-block's `False`-branch rewrites the goal to `substr 0 4 s ++ ("..." ++ substr (...) 4 s)`. The new proof composes `step23 (length "..." + length (substr ...) ≤ 3 + 4)` then `step123 (length (substr 0 4 s) + length (...) ≤ 4 + 7)`, producing exactly the right-associated form. Also fixed two bound-name typos in `toLogSafeShortEq` and `toLogSafeLongEq` where the outer pattern discarded the `prf` argument that the `False`/`True` branch then referenced (`absurd prf` against an undefined `prf`). Build verification (per-module `--check`, full ipkg --build hangs on this machine — see PR #108 notes): Boj.SafetyLemmas green Boj.SafeAPIKey green (this PR) Boj.Safety green Boj.APIContractCoverage green Boj.CartridgeDispatch green Boj.Catalogue green Boj.CredentialIsolation green Boj.Federation green Boj.SafeCORS green Boj.SafeHTTP green Boj.SafePromptInjection green Boj.SafeWebSocket green Stacked on PR #108 (`feat/item11-proof-debt-honest-framing`) because this proof depends on SafetyLemmas's comma-fix; when #108 merges, this auto-rebases to main. No new axioms introduced. The 5-class-(J) framing from PR #108 is preserved. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

… baseline rot) (#116) ## Summary Restores `Boj.SafeAPIKey` to a green Idris2 0.8.0 build. The pre-existing `logSafeBounded` proof on `main` does not type-check; this PR rebuilds it against the current stdlib + elaborator behaviour. **No new axioms.** The 5-class-(J) framing established in #108 is preserved. Discovered while verifying #108 (item 11). Was originally stacked on #108; rebased onto `main` after #108 merged at 2026-05-20T08:13Z. ## Three independent defects, each fixed 1. **Removed the redundant local `plusLteMonotone` helper.** It wrapped `lteTransitive (plusLteMonotoneRight _ lmn) (plusLteMonotoneLeft _ lpq)`: - `lteTransitive` is no longer in stdlib — Idris2 0.8.0 uses `Control.Relation.transitive`, but that's ambiguous in this import context. - `plusLteMonotoneRight` / `plusLteMonotoneLeft` have signature `(p, q, r : Nat) -> LTE q r -> LTE (q+p) (r+p)` in this stdlib — the wrapper passed wildcards expecting a different shape. The stdlib already ships `Data.Nat.plusLteMonotone : LTE m n -> LTE p q -> LTE (m + p) (n + q)` — exactly what the wrapper was trying to be. Use it directly. 2. **Lifted both branches out of the `with`-block.** Inside `logSafeBounded s with (length s <= 8) proof cond`, Idris2 0.8.0 does not reduce `length "***"` (or `length "..."`) at type level — the goal is exposed as `LTE (integerToNat (prim__cast_IntInteger (prim__strLength (if True then ... else ...)))) 11` with the `if`-arm unreduced. Outside the with-block, the same lemmas type-check via Refl-equivalent computation. Extracted `logSafeBoundedShort` / `logSafeBoundedLong` as private helpers; the with-block now just dispatches. 3. **Right-associated the long-path proof.** `(++)` is right-associative in Idris (`a ++ b ++ c = a ++ (b ++ c)`), but the original composed `(p1 ++ "...") ++ p3` (left-associative) — its conclusion didn't match the with-block's False-branch goal. New proof: `step23 (length "..." + length (substr ...) ≤ 3 + 4)` then `step123 (length (substr 0 4 s) + length (...) ≤ 4 + 7)`. Plus two bound-name typos in `toLogSafeShortEq` / `toLogSafeLongEq` where the outer `_` discarded the `prf` argument that the inner branch then referenced. ## Test plan Per-module `idris2 --check` on every safety module — **all 12 green**: ``` Boj.SafetyLemmas green Boj.SafeAPIKey green (this PR) Boj.Safety green Boj.APIContractCoverage green Boj.CartridgeDispatch green Boj.Catalogue green Boj.CredentialIsolation green Boj.Federation green Boj.SafeCORS green Boj.SafeHTTP green Boj.SafePromptInjection green Boj.SafeWebSocket green ``` `idris2 --build src/abi/boj.ipkg` does not complete in 9 min on my dev box (gets SIGTERMed) — same note as #108. Per-module `--check` is the verification surface. ## Why this matters `PROOF-NEEDS.md`'s 2026-05-18 audit claims `SafeAPIKey` carries constructive proofs that close BJ2-partial. Pre-this-PR the proof did not compile. The audit was, like the SafetyLemmas axiom count noted in #108, evidently a desk-read of the source rather than a build. With this PR merged, the audited safety surface is buildable from scratch. Refs epic #87 Tier C (companion to #108 / #109). 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…eep (#126) ## Summary Human + machine documentation close-out for the 2026-05-20 epic #87 Tier C session and follow-on baseline-rot sweep. No code, no behavioural change. ## Files - **`CHANGELOG.md`** `[Unreleased]`: - *Added* — ADR-0014 RFC (#109); README "Formal verification" section (#108). - *Fixed* — SafeAPIKey `logSafeBounded` proof rebuild for Idris2 0.8.0 (#116); `tests/aspect_tests.sh` grep-count bash bug (#118); honest framing of the ABI axiom count + `(s t : T)` → `(s, t : T)` parser-comma fix to `SafetyLemmas.idr` (#108). - **`.machine_readable/6a2/STATE.a2ml`**: - `last-updated` bumped `2026-04-25` → `2026-05-20`. - `believe-me-count` corrected `4` → `5`, with citation back to `PROOF-NEEDS.md` 2026-05-18 audit + #108. - `[session-history]` entry appended summarising items 11 + 12 + the SafeAPIKey baseline-rot follow-up + the CI baseline-rot sweep + operational notes (parallel-session branch drift, workflow OAuth scope dance). ## Companion PRs from this thread | PR | Status | What | |---|---|---| | #108 | MERGED 2026-05-20T08:13Z | item 11 honest framing (docstring + README + parser-comma) | | #109 | MERGED 2026-05-20T08:12Z | item 12 ADR-0014 RFC (cross-cartridge composition safety) | | #116 | MERGED 2026-05-20T08:46Z | SafeAPIKey `logSafeBounded` rebuild for Idris2 0.8.0 | | #118 | MERGED 2026-05-20T09:02Z | `tests/aspect_tests.sh` grep-count bash bug | | #123 | OPEN | `.github/workflows/e2e.yml` Zig + Deno pin refresh | | **#126 (this)** | OPEN | session-close docs | ## Out of scope (intentionally) - `governance / Language / package anti-pattern policy` baseline rot stays untouched per the parallel-session-branch-drift guardrail (parent campaign standards#66 owns it). 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Merge branch 'main' into feat/item11-proof-debt-honest-framing

b855892

hyperpolymath marked this pull request as ready for review May 20, 2026 08:13

hyperpolymath merged commit d307b6c into main May 20, 2026
13 of 20 checks passed

hyperpolymath deleted the feat/item11-proof-debt-honest-framing branch May 20, 2026 08:13

hyperpolymath mentioned this pull request May 20, 2026

fix(idris): rebuild logSafeBounded proof for Idris2 0.8.0 (SafeAPIKey baseline rot) #116

Merged

hyperpolymath mentioned this pull request May 20, 2026

docs(state): close-out 2026-05-20 — epic #87 Tier C + baseline-rot sweep #126

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

docs: honest framing of remaining ABI axioms (epic #87 Tier C item 11) - #108

docs: honest framing of remaining ABI axioms (epic #87 Tier C item 11)#108
hyperpolymath merged 2 commits into
mainfrom
feat/item11-proof-debt-honest-framing

hyperpolymath commented May 20, 2026

Uh oh!

github-actions Bot commented May 20, 2026

Uh oh!

Uh oh!

github-actions Bot commented May 20, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Uh oh!

Conversation

hyperpolymath commented May 20, 2026

Summary

Why this is a docs PR, not a discharge campaign

Out of scope (deliberately)

Test plan

Related branches / overlap to resolve

Uh oh!

github-actions Bot commented May 20, 2026

🔍 Hypatia Security Scan

Uh oh!

Uh oh!

github-actions Bot commented May 20, 2026

🔍 Hypatia Security Scan

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant