Skip to content

docs(proof-needs): reconcile believe_me audit (5 justified axioms) #81

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
hyperpolymath merged 1 commit into from
May 18, 2026
Merged

docs(proof-needs): reconcile believe_me audit (5 justified axioms) #81

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
71 changes: 59 additions & 12 deletions PROOF-NEEDS.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,13 +1,47 @@
# PROOF-NEEDS.md — boj-server

## Current State (Updated 2026-04-25)
## Current State (Updated 2026-05-18)

- **src/abi/Boj/**: 16 Idris2 ABI files
- **Dangerous patterns**: 4 `believe_me` (all documented axioms in SafetyLemmas.idr;
`logSafeBounded` restructured to use them structurally — down from 31)
- **Dangerous patterns**: **5** `believe_me` invocations, **all** in
`src/abi/Boj/SafetyLemmas.idr`, **all** classified `(J)` genuinely
unavoidable (see audit table below). `logSafeBounded` (SafeAPIKey.idr)
consumes these structurally and contains no direct `believe_me` —
down from 31 historically.
- Note: a raw `grep believe_me *.idr` returns **9** hits. 4 of these
are documentation/comment mentions of the word (1 in SafeHTTP.idr
line 15, 1 in SafetyLemmas.idr line 9, 2 in
cartridges/fleet-mcp/abi/FleetMcp/SafeFleet.idr lines 14 & 34) and
are **not** axiom uses. The audited true count is 5.
- **LOC**: ~5,400 (Elixir + Idris2)
- **ABI layer**: Comprehensive dependent-type ABI

## Axiom Audit (2026-05-18)

Every real `believe_me` invocation, with its classification.
Classification key: **(J)** genuinely unavoidable, documented as an axiom;
**(R)** replaceable with a real proof / total definition;
**(S)** stub/laziness to fix.

| # | Site | Function | Type | Class | Rationale |
|---|------|----------|------|-------|-----------|
| 1 | `SafetyLemmas.idr:53` | `charEqSound` | `(c1,c2:Char) -> c1 == c2 = True -> c1 = c2` | **J** | `Char` is an opaque primitive; `==` is `prim__eqChar` (foreign `Bool`). Idris2 0.8.0 has no in-language soundness principle for primitive equality. Standard, well-understood axiom. |
| 2 | `SafetyLemmas.idr:60` | `charEqSym` | `(x,y:Char) -> (x == y) = (y == x)` | **J** | Symmetry of `prim__eqChar`. Same reason as #1 — opaque primitive, no decision procedure to recurse on. |
| 3 | `SafetyLemmas.idr:211` | `unpackLength` | `length (unpack s) = length s` | **J** | `unpack` = `prim__strToCharList` (foreign). `String` is opaque with no induction principle; the relation between primitive `String` length and `List Char` length is not reducible in-language. |
| 4 | `SafetyLemmas.idr:219` | `appendLengthSum` | `length (s ++ t) = length s + length t` | **J** | `++` on `String` = `prim__strAppend` (foreign). Length additivity is a backend-semantics guarantee, not type-level reducible. |
| 5 | `SafetyLemmas.idr:226` | `substrLengthBound` | `LTE (length (substr start len s)) len` | **J** | `substr` = `prim__strSubstr` (foreign). The "result no longer than `len`" bound is a primitive-semantics guarantee with no in-language proof. |

**Verdict: 5/5 are class (J).** All five reduce to the same root cause:
Idris2 treats `Char` and `String` as opaque primitive types whose
operations are foreign functions with no constructors and no induction
principle. There is no constructive in-language proof for any of them; a
`believe_me` (or an equivalent `%foreign` postulate) is the only option
short of changing the trusted computing base. They are correctly marked
`%unsafe`, individually documented, and isolated in one module.

No **(R)** or **(S)** sites were found. The audit's "9" was a raw text
count conflating 5 real axioms with 4 comment mentions.

## Completed Proofs

| File | Covers | REQUIREMENTS-MASTER.md |
Expand All @@ -32,22 +66,35 @@ All P1/P2 proof obligations are now closed.
| BJ2 | Auth/credential handling — full isolation model | ✅ DONE (`CredentialIsolation.idr`) |
| BJ3 | API contract compliance — protocol/domain coverage | ✅ DONE (`APIContractCoverage.idr`) |

### Remaining axiomatic surface (4 believe_me, all in SafetyLemmas.idr)
### Remaining axiomatic surface (5 believe_me, all in SafetyLemmas.idr)

All five are class **(J)** — genuinely unavoidable in Idris2 0.8.0
(opaque `Char`/`String` primitives, foreign-backed operations). See the
**Axiom Audit (2026-05-18)** table above for per-site detail.

| Axiom | Justification |
|-------|---------------|
| `charEqSound` | Soundness of `prim__eqChar` — backend primitive correctness |
| `charEqSym` | Symmetry of `prim__eqChar` — backend primitive correctness |
| `unpackLength` | `prim__strToCharList` preserves length — backend primitive correctness |
| `appendLengthSum` | `prim__strAppend` length semantics — not reducible at type level |
| `substrLengthBound` | `prim__strSubstr` length bound — not reducible at type level |
| Axiom | Site | Justification |
|-------|------|---------------|
| `charEqSound` | `SafetyLemmas.idr:53` | Soundness of `prim__eqChar` — backend primitive correctness |
| `charEqSym` | `SafetyLemmas.idr:60` | Symmetry of `prim__eqChar` — backend primitive correctness |
| `unpackLength` | `SafetyLemmas.idr:211` | `prim__strToCharList` preserves length — backend primitive correctness |
| `appendLengthSum` | `SafetyLemmas.idr:219` | `prim__strAppend` length semantics — not reducible at type level |
| `substrLengthBound` | `SafetyLemmas.idr:226` | `prim__strSubstr` length bound — not reducible at type level |

Note: `logSafeBounded` in SafeAPIKey.idr no longer uses `believe_me` directly;
it calls the documented SafetyLemmas axioms via structural proof.
`charEqSound` is consumed by `Safety.idr` (`shellContra`, `sqlContra`);
`unpackLength` by `SafeAPIKey.idr` (`sufficientEntropyNonEmpty`).

## Priority Going Forward

**LOW** — All named proof obligations closed. Future work:
- Proofs for Dap/Bsp/CodeIntel domains when those cartridges reach Ready status
- Proof that `dispatch` is surjective onto all BJ3-covered (domain, protocol) pairs
- Eliminate string-primitive axioms via a trusted extraction layer
- The 5 string/char-primitive axioms are **irreducible within Idris2**
(opaque primitive types). They cannot be "proved away" in-language;
the only reduction path is to shrink the trusted base by validating
`prim__eqChar` / `prim__strToCharList` / `prim__strAppend` /
`prim__strSubstr` against the chosen backend (Chez/BEAM) via an
external trusted-extraction or property-test harness, then citing
that evidence here. This is a backend-assurance task, not a proof
obligation — keep it tracked but do not expect a constructive proof.
Loading