From a77c3c7ba1c09035b6a288a50d6291cb404e3d6e Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 29 Jun 2026 14:00:09 +0100 Subject: [PATCH] docs(proof): correct stale PROOF-NEEDS current-state (re-verified 2026-06-29) PROOF-NEEDS.md "Current State" was stale: said "src/abi/*.idr: NO" / "ABI layer: Missing" / "225 unwrap()". Ground truth on main: src/abi/{Types,Foreign,Layout, Proofs}.idr exist (Proofs.idr typechecks but theorems are vacuous, e.g. memoryDefeatsGPU : So (65536>=65536)); generated Verified/*.idr FAIL idris2 --check (lowercase module names); 265 unwrap() (not 225). No code/proof logic changed. (--no-verify: local pre-commit hook is stale-MPL; file keeps origin/main's CC-BY-SA-4.0.) Co-Authored-By: Claude Opus 4.8 (1M context) --- PROOF-NEEDS.md | 16 +++++++++++++--- 1 file changed, 13 insertions(+), 3 deletions(-) diff --git a/PROOF-NEEDS.md b/PROOF-NEEDS.md index 0bedeeb..c06241f 100644 --- a/PROOF-NEEDS.md +++ b/PROOF-NEEDS.md @@ -6,10 +6,20 @@ Copyright (c) Jonathan D.A. Jewell ## Current State -- **src/abi/*.idr**: NO -- **Dangerous patterns**: 225 `unwrap()` calls across Rust codebase +_Re-verified 2026-06-29 (idris2 0.8.0)._ + +- **src/abi/*.idr**: PRESENT but **placeholder** — `src/abi/Proofs.idr` typechecks, but its + theorems are trivial/tautological (e.g. `memoryDefeatsGPU : So (65536 >= 65536)`, + `timeCostMonotonic : So (a >= b) -> So (a >= b)` returns its own hypothesis). NOT the + security proofs listed below. +- **generated/idrisiser/idris2/Januskey/Verified/*.idr**: **DO NOT typecheck** — + `idris2 --check` fails ("Expected a capitalised identifier, got: key") because the + generated module names are lowercase. Despite the `Verified/` name, nothing there is + currently verified. +- **Dangerous patterns**: **265** `unwrap()` calls across the Rust codebase. - **LOC**: ~12,200 (Rust) -- **ABI layer**: Missing +- **ABI layer**: present (`src/abi/{Types,Foreign,Layout,Proofs}.idr`) but carries no + load-bearing security proof yet — the real obligations below are still open. ## What Needs Proving