From a882e016d603d47b664da551b4401a9969878041 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 1 Jun 2026 12:56:13 +0100 Subject: [PATCH] docs(proof): replace template-content proofs with KRL-specific narrative MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Replaces eight rsr-template proof files (Coq/Lean4/Idris2) that contained zero KRL-specific content (generic typed-arithmetic example, generic ApiResult, generic Bounded/SafePtr) with a coherent proof story scoped to the KRL surface language. Added: - PROOF-NARRATIVE.md — coherent story of what KRL proves, what it assumes, what it owes. Covers KR-1..KR-8 with statement, "why valuable", status, explicit assumptions, and "how to discharge". - ASSUMPTIONS.md — registry of every load-bearing unproven assumption (12 entries: MATH / DESIGN / EMPIRICAL / CRYPTO). Rewritten: - PROOF-NEEDS.md — 8-row per-obligation checklist (KR-1..KR-8) with category, prover, priority, effort estimate. Previously was a template scaffold with the project-specific section empty. - TEST-NEEDS.md — KRL-specific (CRG D, real test inventory). Previously referred to rsr-template-repo throughout and claimed CRG Grade C achieved (for the template, not KRL). - PROOF-STATUS.md — now reflects actual KR-1..KR-8 (0 proven, 2 partial, 6 not started) instead of 7 mythical template obligations. Deleted (recoverable from rsr-template-repo upstream): - verification/proofs/coq/TypeSafety.v (generic typed arithmetic) - verification/proofs/lean4/ApiTypes.lean (generic ApiResult) - verification/proofs/idris2/Types.idr (generic Bounded/NonEmpty) - verification/proofs/idris2/ABI/{Pointers,Foreign,Layout,Platform,Compliance}.idr (generic ABI scaffolds) None asserted anything about KRL. Their headers said "Template — replace with your project's ..." explicitly. The 2026-06-01 audit found they were creating a false impression of formal verification. The actual semantic-core proofs that KRL benefits from live in hyperpolymath/tangle/proofs/Tangle.lean (16 results: Progress, Preservation, Determinism, Type Safety + 12 lemmas), tracked in that repo's PROOF-STATUS, referenced from this repo's narrative. README.adoc updated: removed "TanglePL compiler module (this repo)" claim — the compiler lives in KRLAdapter.jl, not here. Owner field added to satisfy global pre-commit Owner check. Part of the focused krl + quandledb + tangle audit/elevation pass. Not estate-wide. Co-Authored-By: Claude Opus 4.7 (1M context) --- ASSUMPTIONS.md | 67 ++++ PROOF-NARRATIVE.md | 316 ++++++++++++++++++ PROOF-NEEDS.md | 138 ++++---- PROOF-STATUS.md | 101 +++--- README.adoc | 32 +- TEST-NEEDS.md | 195 +++++------ verification/proofs/coq/TypeSafety.v | 73 ---- verification/proofs/idris2/ABI/Compliance.idr | 41 --- verification/proofs/idris2/ABI/Foreign.idr | 53 --- verification/proofs/idris2/ABI/Layout.idr | 63 ---- verification/proofs/idris2/ABI/Platform.idr | 63 ---- verification/proofs/idris2/ABI/Pointers.idr | 52 --- verification/proofs/idris2/Types.idr | 38 --- verification/proofs/lean4/ApiTypes.lean | 44 --- 14 files changed, 611 insertions(+), 665 deletions(-) create mode 100644 ASSUMPTIONS.md create mode 100644 PROOF-NARRATIVE.md delete mode 100644 verification/proofs/coq/TypeSafety.v delete mode 100644 verification/proofs/idris2/ABI/Compliance.idr delete mode 100644 verification/proofs/idris2/ABI/Foreign.idr delete mode 100644 verification/proofs/idris2/ABI/Layout.idr delete mode 100644 verification/proofs/idris2/ABI/Platform.idr delete mode 100644 verification/proofs/idris2/ABI/Pointers.idr delete mode 100644 verification/proofs/idris2/Types.idr delete mode 100644 verification/proofs/lean4/ApiTypes.lean diff --git a/ASSUMPTIONS.md b/ASSUMPTIONS.md new file mode 100644 index 0000000..9da7d16 --- /dev/null +++ b/ASSUMPTIONS.md @@ -0,0 +1,67 @@ + +# Assumptions Registry — KRL + +Every load-bearing **unproven** assumption used in this repo, with an +ID, classification, and the obligation it supports. + +Classifications: +- **MATH** — true by an external mathematical theorem (cite it) +- **DESIGN** — true by construction in our code (must remain true; flag if you change the named code) +- **EMPIRICAL** — believed from testing; not formally verified +- **CRYPTO** — standard cryptographic-primitive assumption + +Cross-references use `[[A-KR-N.M]]` syntax, resolved here. + +--- + +| ID | Class | Statement | Cited by | Where it lives | +|----|-------|-----------|----------|----------------| +| A-KR-1.1 | DESIGN | Every `KRLExpr` AST variant has a matching arm in `KRLAdapter.jl::lower.jl` | KR-1 | `KRLAdapter.jl/src/parser/lower.jl` | +| A-KR-1.2 | DESIGN | `KRLAdapter.jl/src/parser/ast.jl` defines the only AST shapes the parser produces | KR-1 | `KRLAdapter.jl/src/parser/ast.jl` + `parser.jl` | +| A-KR-2.1 | DESIGN | Generator arity is fixed: `sigma i / sigma_inv i : in=i+1, out=i+1`; `cup i : in=0, out=2`; `cap i : in=2, out=0` | KR-2 | KRL grammar definitions; `KRLAdapter.jl/src/operations.jl` | +| A-KR-2.2 | MATH | `arity_in(a \| b) = arity_in(a) + arity_in(b)` and same for output (monoidal-category tensor) | KR-2 | Standard categorical tangle definition | +| A-KR-3.1 | MATH | Reidemeister's theorem: R1+R2+R3 generate isotopy equivalence on tangle diagrams | KR-3 | Reidemeister 1927; Kauffman _Knots and Physics_ ch. 1 | +| A-KR-3.2 | DESIGN | `KRLAdapter.jl::r1_simplify` / `r2_simplify` / `r3_simplify` implement those moves faithfully (R3 is a current GAP — see `quandledb/PROOF-NARRATIVE.md` QD-2) | KR-3 | `KRLAdapter.jl/src/operations.jl` | +| A-KR-4.1 | DESIGN | KRL pretty-printer's bracketing is unambiguous: `;` only inside parens; tensor `\|` has lower precedence than compose `;` inside parens | KR-4 | `KRLAdapter.jl` pretty; `spec/grammar.ebnf` | +| A-KR-6.1 | DESIGN | `KRLAdapter.jl::parse_krl` and `quandledb/server/krl/Parser.jl::parse_any` both target `spec/grammar.ebnf` v0.1.0 | KR-6 | `spec/grammar.ebnf` | +| A-KR-6.2 | DESIGN | Both implementations share the same `Token` enumeration: keyword set, identifier shape, integer/string literal shapes | KR-6 | `KRLAdapter.jl/src/parser/lexer.jl` and `quandledb/server/krl/Lexer.jl` | +| A-KR-8.1 | MATH (partial) | Fundamental-quandle functor is faithful on prime alternating knots; partial in general | KR-8 | Joyce 1982; for partial cases see Eisermann _The number of knot group representations_ | +| A-KR-8.2 | MATH | Two non-isomorphic quandles have distinct canonical presentations (true by definition of "canonical") | KR-8 | Standard algebraic-presentation result | + +--- + +## How to use this file + +- **Reading code.** When you see a function whose correctness depends + on something not enforced by the local types — _that's an + assumption_. Find or add the entry here and reference it by ID. +- **Writing a proof.** Every proof obligation in + [PROOF-NARRATIVE.md](PROOF-NARRATIVE.md) names its assumptions by + ID. Before discharging the proof, audit the assumptions. +- **Modifying load-bearing code.** Each DESIGN assumption names a + file. If you edit that file, re-validate the assumption (or update + the obligation if you changed the design intentionally). + +## Promoting / demoting assumptions + +| From | To | Trigger | +|------|-----|---------| +| EMPIRICAL → MATH | discharge with a citation | +| EMPIRICAL → DESIGN | refactor to make it a structural invariant | +| MATH → (delete) | obligation it supports has been re-cast not to need it | +| DESIGN → MATH (rare) | the design happens to encode a known theorem | +| any → CRYPTO | only for cryptographic primitives (BLAKE3, SHA-256, etc.) | + +When you change a row, leave a one-line note at the bottom of this +file with the date and reason. + +--- + +## Changelog + +| Date | Change | By | +|------|--------|-----| +| 2026-06-01 | Initial registry, scoped to KRL surface obligations | Audit | diff --git a/PROOF-NARRATIVE.md b/PROOF-NARRATIVE.md new file mode 100644 index 0000000..3c90ccc --- /dev/null +++ b/PROOF-NARRATIVE.md @@ -0,0 +1,316 @@ + +# Proof Narrative — KRL + +This file is the **single coherent story** of what KRL proves, what it +assumes, and what it has left to prove. It is the document a reader +should open first when asking _"is this language sound, and how do I +know?"_. + +For the per-obligation status checklist, see [PROOF-NEEDS.md](PROOF-NEEDS.md). +For the registry of every load-bearing unproven assumption, see +[ASSUMPTIONS.md](ASSUMPTIONS.md). + +--- + +## 1. Position in the stack + +KRL is the **surface language** of a four-layer federated stack. It is +*not* a standalone implementation; the canonical implementations live +in sibling repos: + +``` +┌─────────────────────────────────────────────────────────┐ +│ KRL surface language (this repo) │ +│ • spec/grammar.ebnf (v0.1.0) │ +│ • Idris2 ABI types (src/interface/Abi/) │ +│ • Zig FFI scaffold (src/interface/ffi/) │ +│ • examples (examples/) │ +└─────────────────┬───────────────────────────────────────┘ + │ implements + ▼ +┌─────────────────────────────────────────────────────────┐ +│ KRLAdapter.jl — canonical parser / lower │ +│ quandledb/server/krl/ — server-side query parser │ +└─────────────────┬───────────────────────────────────────┘ + │ lowers to + ▼ +┌─────────────────────────────────────────────────────────┐ +│ TangleIR — canonical interchange object │ +└─────────────────┬───────────────────────────────────────┘ + │ semantics on + ▼ +┌─────────────────────────────────────────────────────────┐ +│ Tangle (hyperpolymath/tangle) — proven core │ +│ Progress · Preservation · Determinism · Type Safety │ +└─────────────────┬───────────────────────────────────────┘ + │ persisted+queried via + ▼ +┌─────────────────────────────────────────────────────────┐ +│ Skein.jl + QuandleDB — storage + semantic index │ +└─────────────────────────────────────────────────────────┘ +``` + +Consequence: **this repo's proof obligations are spec-level, not +implementation-level**. We owe a precise definition of what a KRL +program *is*, plus refinement-style obligations against the two +parser implementations. + +## 2. Proven now + +| ID | Statement | Form | Where | +|----|-----------|------|-------| +| — | _none yet at the KRL surface level_ | — | — | + +The Idris2 / Lean / Coq files previously sitting under +`verification/proofs/` were rsr-template-repo boilerplate (generic +`Bounded`, `ApiResult`, typed-arithmetic `TypeSafety`). They asserted +nothing about KRL. They have been deleted in the same PR as this +narrative to avoid the "looks proven, isn't" failure mode. Their +content is recoverable from the PR description if anyone wants the +template back. + +**The actually-proven results that the KRL stack benefits from live +in `hyperpolymath/tangle/proofs/Tangle.lean`** (16 theorems and +lemmas including Progress, Preservation, Determinism, and Type Safety +for the core Tangle calculus that KRL lowers into). See the tangle +repo's `PROOF-NARRATIVE.md` for details. Until KRL has its own surface +proofs, the soundness story rests on (a) the Tangle core proofs and +(b) the *unproven* claim that KRL faithfully lowers into that core. +That claim is `KR-1` and `KR-2` below. + +## 3. Obligations (the narrative arc) + +The arc from "KRL text" to "trusted query result": + +``` +KRL source text + │ [KR-7] parser rejects ill-typed concrete syntax + ▼ +KRLProgram AST + │ [KR-1] lowering is total on parseable programs + │ [KR-2] lowering preserves port arity + ▼ +TangleIR + │ [hyperpolymath/tangle: T-Progress, T-Preservation, T-Determinism] + ▼ +Tangle value + │ [KR-3] simplify is semantics-preserving + │ [KR-8] equivalent? is sound w.r.t. fundamental-quandle iso + ▼ +Query result +``` + +Each obligation in detail: + +### KR-1 — Lowering is total on parseable programs + +**Claim.** For every `KRLProgram p` produced by `parse_krl`, the +function `lower(p)` returns a `TangleIR` (never raises `KRLLowerError`). + +**Why valuable.** A `KRLLowerError` at runtime means the parser +accepted a program that the lowering rejected — a soundness regression +that the lexer/parser/AST should have prevented. Closing this proves +parser-and-lowering agree on the language. + +**Status.** Unproven. Currently `KRLLowerError` is raised from +`KRLAdapter.jl/src/parser/lower.jl` on (a) unbound identifiers and +(b) un-matched AST variants. Case (a) is correct (it's a real user +error); case (b) is the soundness gap. + +**Assumptions (load-bearing for this claim).** +- [[A-KR-1.1]] Every `KRLExpr` AST variant has a matching arm in `lower.jl`. +- [[A-KR-1.2]] The AST defined in `KRLAdapter.jl/src/parser/ast.jl` is + the *only* AST shape the parser can produce. + +**How to discharge.** Add an exhaustiveness check to the lowering +function (compile-time in Julia is weak; consider a property-based +test enumerating every constructor as a stop-gap, with Idris2 as the +target prover for the long term). + +### KR-2 — Lowering preserves port arity + +**Claim.** If `p : KRLProgram` lowers to `ir : TangleIR`, then for +every sub-expression `(compose a b)` in `p`, the number of output +ports of `lower(a)` equals the number of input ports of `lower(b)`. + +**Why valuable.** Composition is the central operation. Without this, +you can write KRL that lowers to ill-formed TangleIR — e.g. composing +a 2-strand braid with a 3-strand tangle — and the error surfaces +downstream as garbled invariant computation, not as a clear "your +program is wrong" message. + +**Status.** Unproven, and the typechecker that would enforce this at +parse time is **not yet implemented** (acknowledged in `READINESS.md` +under "Path to C"). + +**Assumptions.** +- [[A-KR-2.1]] Generators have known fixed arity: + `sigma i : in=i, out=i+1` (and same arity in/out), `cup i : in=0, + out=2`, `cap i : in=2, out=0`. +- [[A-KR-2.2]] Tensor and compose distribute over arity in the obvious + way: `arity_in(a | b) = arity_in(a) + arity_in(b)`. + +**How to discharge.** Implement port-arity checking in the +typechecker; prove the typechecker sound against this property. + +### KR-3 — `simplify` is semantics-preserving + +**Claim.** For every `e : KRLExpr` and its simplified form +`e' = simplify(e)`, the lowered TangleIR objects `lower(e)` and +`lower(e')` represent the same tangle up to isotopy. + +**Why valuable.** This is the *retrieval guarantee*: queries against +the simplified form must return the same answer as queries against +the original. Without it, simplification is a performance trick that +can change semantics. + +**Status.** Unproven; `simplify` is partially implemented in +KRLAdapter.jl (R2 detection works inside a single sigma sequence but +not across `compose` boundaries — see `READINESS.md`). + +**Assumptions.** +- [[A-KR-3.1]] R1, R2, R3 are the complete set of local moves needed + to relate isotopic tangles (Reidemeister's theorem; mathematically + established). +- [[A-KR-3.2]] `r1_simplify`, `r2_simplify`, `r3_simplify` (when + implemented; R3 is currently a gap — see + `quandledb/PROOF-NARRATIVE.md` QD-2) faithfully implement those moves. + +**How to discharge.** Prove each rewrite preserves the fundamental +quandle presentation (which encodes isotopy). + +### KR-4 — Pretty-print/parse round-trip + +**Claim.** For every `e : KRLExpr` produced by `parse_krl`, +`parse_krl(pretty(e)) = e`. + +**Why valuable.** A free fuzz oracle. Catches a whole class of "lossy +IR" bugs at the parse boundary. Also the foundation of the +`reconstruct_source` claim in `README.adoc`. + +**Status.** Unproven; `pretty` exists in KRLAdapter.jl but no +round-trip test. + +**Assumptions.** +- [[A-KR-4.1]] The pretty-printer's choice of bracketing is + unambiguous w.r.t. the grammar (e.g. `;` only inside parens at the + expression level — see `READINESS.md`). + +**How to discharge.** Add a property test in `KRLAdapter.jl/test/` +that round-trips every well-formed program from `examples/`. + +### KR-5 — Idris2/Zig ABI primitives are load-bearing + +**Claim.** `SafePtr`, `Handle`, `Bounded`, `NonEmpty` (currently in +`src/interface/Abi/` and `verification/proofs/idris2/`) must either be +**referenced by the actual Zig FFI surface** or be deleted. + +**Why valuable.** Right now they're floating. They were rsr-template +content; they have non-trivial dependent-type structure but no +consumer. + +**Status.** Decision pending. Recommended decision: keep `SafePtr` and +`Handle`, wire them through the FFI; delete `Bounded` and `NonEmpty` +as unused. + +### KR-6 — Two-parser equivalence + +**Claim.** For every input string `s`, `KRLAdapter.jl::parse_krl(s)` +and `quandledb/server/krl/Parser.jl::parse_any(s)` either both +succeed with equal ASTs or both fail. + +**Why valuable.** The two implementations exist by design — one for +end-user code, one for query-time parsing — but if they accept +different languages, the server can run queries the user can't write, +and vice versa. + +**Status.** Unproven; no differential test exists. + +**Assumptions.** +- [[A-KR-6.1]] Both implementations target the same EBNF grammar + (`spec/grammar.ebnf` v0.1.0). +- [[A-KR-6.2]] Both implementations have the same notion of "valid + identifier", "valid integer literal", "valid string literal". + +**How to discharge.** Build a differential fuzz harness that feeds +random strings to both and asserts result equivalence. Easy single PR. + +### KR-7 — Generator-index validity + +**Claim.** `sigma N`, `sigma_inv N`, `cup N`, `cap N` are accepted iff +`N ≥ 1`. + +**Why valuable.** Small but catches a real class of off-by-one bugs; +also a parser-level invariant that should be asserted explicitly. + +**Status.** Currently encoded in the existing parser-error case +("zero index" rejected). Not asserted as a property test. + +### KR-8 — `equivalent?` is sound w.r.t. quandle isomorphism + +**Claim.** If `equivalent?(a, b)` returns `true`, then the fundamental +quandles of `a` and `b` are isomorphic. + +**Why valuable.** This is the central claim of the retrieval layer. +False positives mean the database lies; without this, `equivalent?` is +heuristic, not semantic. + +**Status.** Unproven; implementation in QuandleDB. Soundness rests on +[[A-KR-8.1]] and the fingerprint determinism claim +`quandledb/PROOF-NARRATIVE.md` QD-4. + +**Assumptions.** +- [[A-KR-8.1]] Fundamental-quandle functor is *faithful* on isotopy + classes (true for prime alternating knots; partial in general — this + needs to be a stated and bounded assumption). +- [[A-KR-8.2]] Fingerprint collisions are mathematically impossible + for non-isomorphic quandles (this is a property of the + canonicalisation, not the hash). + +**How to discharge.** Either: +- Restrict the claim to the prime-alternating subset (where the + functor is provably faithful), or +- State the obligation as "equivalence is sound modulo the + fundamental-quandle relation", which is weaker but provable. + +## 4. The "stupid proof" exclusions + +For completeness, things we deliberately do **not** prove: + +- _"`KRLProgram` is a record with these fields"_ — enforced by the + Julia type system; no proof needed. +- _"`parse_krl` returns a `KRLProgram`"_ — Julia type assertion. +- _"Compose is associative when types agree"_ — implied by list-append + associativity. +- _"BLAKE3 is collision-resistant"_ — out of scope; cryptographic + primitive assumption inherited from QuandleDB. + +If you find yourself drafting a proof in one of these categories, +delete the draft. + +## 5. How to add a new obligation + +1. Add an entry to [PROOF-NEEDS.md](PROOF-NEEDS.md) with an ID + (`KR-N`), category, prover, priority, effort estimate. +2. Add the narrative entry here: statement, _why valuable_, + status, **assumptions**, how to discharge. The assumptions block + is non-optional. +3. For each new assumption, add an entry to + [ASSUMPTIONS.md](ASSUMPTIONS.md) with an ID (`A-KR-N.M`) and a + note on whether it is _mathematical_ (true by external theorem), + _design_ (true by our construction), or _empirical_ (believed, + not verified). + +## 6. References + +- Architecture: [README.adoc](README.adoc), section "Architecture position". +- Companion narratives: + - `hyperpolymath/tangle/PROOF-NARRATIVE.md` — semantic core proofs + - `hyperpolymath/quandledb/PROOF-NARRATIVE.md` — quandle / DB proofs +- Implementations: + - `KRLAdapter.jl` — canonical parser, AST, lower + - `quandledb/server/krl/` — server-side query parser +- Spec: [spec/grammar.ebnf](spec/grammar.ebnf), [spec/grammar-overview.md](spec/grammar-overview.md). diff --git a/PROOF-NEEDS.md b/PROOF-NEEDS.md index fc7a736..4a4b939 100644 --- a/PROOF-NEEDS.md +++ b/PROOF-NEEDS.md @@ -1,103 +1,83 @@ + # Proof Requirements — KRL - - - + +> The single coherent story is [PROOF-NARRATIVE.md](PROOF-NARRATIVE.md). +> The assumption registry is [ASSUMPTIONS.md](ASSUMPTIONS.md). +> This file is the **per-obligation checklist** with status, prover, priority. ## Proof Tier - -**Tier**: T3 — Standard +**Tier:** T2 — High. +KRL is the surface language of a federated stack whose correctness +claims (semantic-equivalence queries, isotopy-respecting retrieval) +rest on KRL→TangleIR lowering being trustworthy. The semantic core +(TangleIR/Tangle) is already partially proven; KRL's job is to +guarantee faithful lowering. -## Proof Categories +## Proof categories | Code | Meaning | Applies? | |------|---------|----------| -| **TP** | Typing Proofs (type soundness, type safety) | Yes | -| **INV** | Invariant Proofs (state machines, monotonicity, bounds) | | -| **SEC** | Security Proofs (crypto, injection freedom, access control) | | -| **CONC** | Concurrency Proofs (linearizability, deadlock freedom) | | -| **ALG** | Algorithm Proofs (termination, correctness, bounds) | | -| **ABI** | ABI/FFI Proofs (memory layout, pointer safety, platform compat) | Yes | -| **DOM** | Domain-Specific Proofs (bespoke to this project) | | - -## Mandatory Proofs (All RSR Repos) - -These proofs come from the rsr-template-repo and MUST be present in every repo: - -### ABI/FFI Boundary Proofs (Idris2) - -| # | Proof | Status | File | -|---|-------|--------|------| -| ABI-1 | Non-null pointer proofs (`So (ptr /= 0)`) | Needed | `verification/proofs/idris2/ABI/Pointers.idr` | -| ABI-2 | Memory layout correctness (`HasSize`, `HasAlignment`) | Needed | `verification/proofs/idris2/ABI/Layout.idr` | -| ABI-3 | Platform type size proofs (per platform) | Needed | `verification/proofs/idris2/ABI/Platform.idr` | -| ABI-4 | FFI function return type proofs | Needed | `verification/proofs/idris2/ABI/Foreign.idr` | -| ABI-5 | C ABI compliance (`CABICompliant`, `FieldsAligned`) | Needed | `verification/proofs/idris2/ABI/Compliance.idr` | - -### Typing Proofs (Prover Varies) - -| # | Proof | Status | File | -|---|-------|--------|------| -| TP-1 | Core data type well-formedness | Needed | `verification/proofs/idris2/Types.idr` | -| TP-2 | Public API type safety (exported functions) | Needed | `verification/proofs/lean4/ApiTypes.lean` | - -## Project-Specific Proofs - - - - -| # | Proof Needed | Category | Prover | Priority | File(s) | -|---|-------------|----------|--------|----------|---------| -| | | | | | | - -## Dangerous Patterns (BANNED) - -The following MUST NOT appear anywhere in proof files: +| **TP** | Typing proofs (port-arity, lowering totality) | Yes | +| **INV** | Invariant proofs (round-trip, grammar refinement) | Yes | +| **SEC** | Security proofs | No | +| **CONC** | Concurrency proofs | No | +| **ALG** | Algorithm proofs (simplification correctness) | Yes | +| **ABI** | ABI/FFI proofs (Zig FFI boundary, Idris2 layout) | Yes (low priority) | +| **DOM** | Domain proofs (quandle equivalence soundness) | Yes | + +## Obligations + +| # | Statement | Category | Prover | Priority | Effort | Status | +|---|-----------|----------|--------|----------|--------|--------| +| KR-1 | `lower` is total on parseable programs | TP | Idris2 + Julia property test | P1 | 1d | NOT STARTED | +| KR-2 | `lower` preserves port arity | TP | Idris2 + typechecker impl | P1 | 3d | NOT STARTED (typechecker not implemented) | +| KR-3 | `simplify` is semantics-preserving (KR-3a: R1; KR-3b: R2; KR-3c: R3) | ALG | Lean4 or property test against quandle iso | P1 | 5d | PARTIAL (R2 across compose() is gap) | +| KR-4 | Pretty/parse round-trip: `parse(pretty(e)) = e` | INV | Julia property test (cheap) | P1 | 4h | NOT STARTED | +| KR-5 | Idris2 `SafePtr` / `Handle` are load-bearing in the Zig FFI surface | ABI | Decision + wiring | P3 | 2h | DECISION PENDING | +| KR-6 | `KRLAdapter.jl::parse_krl` ≡ `quandledb/server/krl::parse_any` on the v0.1.0 grammar | INV | Differential property test | P1 | 4h | NOT STARTED | +| KR-7 | `sigma N`, `cup N`, etc. accepted iff `N ≥ 1` | INV | Grammar smoke test extension | P2 | 1h | PARTIAL (error path exists, not property-tested) | +| KR-8 | `equivalent?` is sound w.r.t. fundamental-quandle isomorphism | DOM | Lean4 (factored through QuandleDB's QD-3) | P1 | 5d | NOT STARTED | + +For full statements, _why valuable_, and the assumptions each +obligation rests on, see [PROOF-NARRATIVE.md](PROOF-NARRATIVE.md). +For the assumptions themselves, see [ASSUMPTIONS.md](ASSUMPTIONS.md). + +## Dangerous patterns (BANNED) + +CI rejects any PR introducing any of these: | Pattern | Language | Meaning | |---------|----------|---------| -| `believe_me` | Idris2 | Unsafe cast / trust-me | +| `believe_me` | Idris2 | Unsafe cast | | `assert_total` | Idris2 | Skip totality check | -| `postulate` | Idris2/Agda | Unproven axiom | +| `postulate` | Idris2 / Agda | Unproven axiom | | `sorry` | Lean4 | Incomplete proof | | `Admitted` | Coq | Incomplete proof | -| `unsafeCoerce` | Haskell | Unsafe type cast | -| `Obj.magic` | OCaml/ReScript | Unsafe type cast | +| `unsafeCoerce` | Haskell | Unsafe cast | +| `Obj.magic` | OCaml / ReScript | Unsafe cast | | `unsafe` (unaudited) | Rust | Unsafe block without safety comment | -CI will reject any PR introducing these patterns (enforced by `panic-attack assail`). +Enforced by `panic-attack assail --proofs-only`. -## Prover Selection Guide - -| Use Case | Recommended Prover | Why | -|----------|-------------------|-----| -| ABI/FFI boundaries | **Idris2** | Dependent types model layouts precisely | -| Type system proofs | **Coq** or **Lean4** | Mature proof assistants for metatheory | -| Algebraic properties | **Lean4** | Good mathlib support | -| Inductive/coinductive | **Agda** | Native support for (co)induction | -| Distributed systems | **TLA+** | Model checking for protocols | -| Numerical properties | **Isabelle** | Strong real analysis library | - -## Proof File Locations +## Where proofs go ``` verification/proofs/ -├── idris2/ # Idris2 proofs (ABI, dependent types) -│ ├── ABI/ # ABI-specific proofs -│ └── *.idr # Project-specific Idris2 proofs -├── lean4/ # Lean4 proofs (algebra, lattices) -│ └── *.lean -├── agda/ # Agda proofs (induction, metatheory) -│ └── *.agda -├── coq/ # Coq proofs (type systems, compilation) -│ └── *.v -└── tlaplus/ # TLA+ specs (distributed protocols) - └── *.tla +├── idris2/ — ABI / type-level invariants (KR-1, KR-2, KR-5) +├── lean4/ — Semantic claims (KR-3, KR-8) +└── julia/ — Property tests against KRLAdapter.jl (KR-4, KR-6, KR-7) ``` +(The previous `coq/` directory has been removed; obligations have +been re-allocated to Lean4 where the Tangle metatheory lives.) + ## References -- Master list: `~/Desktop/PROOF-REQUIREMENTS-MASTER.md` -- Proof status tracking: `PROOF-STATUS.md` (this repo) -- Proven library: `proven` repo (Idris2 verified foundations) -- Template: `rsr-template-repo/PROOF-NEEDS.md` +- Companion narratives: + `hyperpolymath/tangle/PROOF-NARRATIVE.md` (semantic core), + `hyperpolymath/quandledb/PROOF-NARRATIVE.md` (quandle / DB). +- Implementations under proof: `KRLAdapter.jl`, `quandledb/server/krl/`. diff --git a/PROOF-STATUS.md b/PROOF-STATUS.md index d53b47b..1162aee 100644 --- a/PROOF-STATUS.md +++ b/PROOF-STATUS.md @@ -1,58 +1,78 @@ + # Proof Status — KRL - - - + +> Requirements: [PROOF-NEEDS.md](PROOF-NEEDS.md). +> Single coherent story: [PROOF-NARRATIVE.md](PROOF-NARRATIVE.md). +> Assumption registry: [ASSUMPTIONS.md](ASSUMPTIONS.md). + +This file tracks the per-obligation status. Updated 2026-06-01. ## Summary -| Category | Total | Done | In Progress | Blocked | Remaining | -|----------|-------|------|-------------|---------|-----------| -| ABI/FFI (ABI) | 5 | 0 | 0 | 0 | 5 | -| Typing (TP) | 2 | 0 | 0 | 0 | 2 | -| Invariant (INV) | 0 | 0 | 0 | 0 | 0 | -| Security (SEC) | 0 | 0 | 0 | 0 | 0 | -| Concurrency (CONC) | 0 | 0 | 0 | 0 | 0 | -| Algorithm (ALG) | 0 | 0 | 0 | 0 | 0 | -| Domain (DOM) | 0 | 0 | 0 | 0 | 0 | -| **Total** | **7** | **0** | **0** | **0** | **7** | +| Category | Total | Done | In Progress | Partial | Blocked | Not Started | +|----------|-------|------|-------------|---------|---------|-------------| +| Typing (TP) | 2 | 0 | 0 | 0 | 0 | 2 | +| Invariant (INV) | 3 | 0 | 0 | 1 | 0 | 2 | +| Algorithm (ALG) | 1 | 0 | 0 | 1 | 0 | 0 | +| ABI (ABI) | 1 | 0 | 0 | 0 | 0 | 1 (decision pending) | +| Domain (DOM) | 1 | 0 | 0 | 0 | 0 | 1 | +| **Total** | **8** | **0** | **0** | **2** | **0** | **6** | -**Overall**: 0% proven +**Overall:** 0% proven, 25% partial. -## Proofs Done +The partial entries (`KR-3` simplification across compose() and +`KR-7` generator index validity) have implementations or smoke +coverage but no property test or formal proof. - - - +## Proofs done -| ID | Proof | Prover | File | Date | Verified By | +| ID | Proof | Prover | File | Date | Verified by | |----|-------|--------|------|------|-------------| -| — | No proofs completed yet | — | — | — | — | +| — | none yet at the KRL surface level | — | — | — | — | -## Proofs In Progress +The Tangle core proofs (Progress, Preservation, Determinism, +Type Safety + 12 lemmas, 16 results total) in +`hyperpolymath/tangle/proofs/Tangle.lean` are foundational for KRL +because KRL lowers into Tangle. They are tracked in tangle's +PROOF-STATUS, not here. + +## Proofs in progress | ID | Proof | Prover | Assignee | Started | Blocker | |----|-------|--------|----------|---------|---------| | — | — | — | — | — | — | -## Proofs Blocked +## Proofs partial + +| ID | Proof | Form | Notes | +|----|-------|------|-------| +| KR-3 | `simplify` semantics-preserving | Property test in `KRLAdapter.jl/test/` | R1 + R2 (within a single sigma sequence) covered. R2 across `compose()` not covered. R3 implementation gap. See `quandledb/PROOF-NARRATIVE.md` QD-2. | +| KR-7 | `sigma N` accepted iff `N ≥ 1` | Parser error path | Not property-tested. | -| ID | Proof | Blocked By | Notes | -|----|-------|------------|-------| -| — | — | — | — | +## Proofs blocked -## Proofs Remaining +| ID | Proof | Blocked by | +|----|-------|------------| +| KR-2 | Lowering preserves port arity | Typechecker not yet implemented (see `READINESS.md`) | +| KR-3c | R3 invariance | `KnotTheory.jl` has no R3 simplifier (see quandledb QD-2) | -| ID | Proof | Category | Prover | Priority | Est. Effort | -|----|-------|----------|--------|----------|-------------| -| ABI-1 | Non-null pointer proofs | ABI | Idris2 | P1 | 2h | -| ABI-2 | Memory layout correctness | ABI | Idris2 | P1 | 4h | -| ABI-3 | Platform type size proofs | ABI | Idris2 | P1 | 2h | -| ABI-4 | FFI function return type proofs | ABI | Idris2 | P1 | 2h | -| ABI-5 | C ABI compliance | ABI | Idris2 | P1 | 4h | -| TP-1 | Core data type well-formedness | TP | Idris2 | P1 | 4h | -| TP-2 | Public API type safety | TP | Lean4 | P2 | 4h | +## Proofs remaining -## Verification Commands +| ID | Proof | Category | Prover | Priority | Effort | +|----|-------|----------|--------|----------|--------| +| KR-1 | `lower` total on parseable programs | TP | Idris2 + property test | P1 | 1d | +| KR-2 | `lower` preserves port arity | TP | Idris2 + impl | P1 | 3d | +| KR-3 | `simplify` semantics-preserving | ALG | Lean4 / property | P1 | 5d | +| KR-4 | Pretty/parse round-trip | INV | Property | P1 | 4h | +| KR-5 | ABI primitives load-bearing | ABI | Decision | P3 | 2h | +| KR-6 | Two-parser equivalence | INV | Differential property test | P1 | 4h | +| KR-7 | Generator index validity | INV | Property test | P2 | 1h | +| KR-8 | `equivalent?` sound | DOM | Lean4 (via QuandleDB QD-3) | P1 | 5d | + +## Verification commands ```bash # Check all Idris2 proofs @@ -61,12 +81,6 @@ just proof-check-idris2 # Check all Lean4 proofs just proof-check-lean4 -# Check all Agda proofs -just proof-check-agda - -# Check all Coq proofs -just proof-check-coq - # Run all proof checks just proof-check-all @@ -78,4 +92,5 @@ panic-attack assail --proofs-only | Date | Change | By | |------|--------|-----| -| 2026-04-04 | Initial proof status tracking | Template | +| 2026-04-04 | Initial proof status tracking | Template (rsr-template-repo) | +| 2026-06-01 | Replaced template-content scaffold with KRL-specific obligations KR-1..KR-8. Deleted template-content proof files (Coq/Lean/Idris) that had zero KRL content. | Audit | diff --git a/README.adoc b/README.adoc index 8bfef1e..0e7d9eb 100644 --- a/README.adoc +++ b/README.adoc @@ -1,5 +1,6 @@ // SPDX-License-Identifier: MPL-2.0 // Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +// Owner: Jonathan D.A. Jewell = KRL — Knot Resolution Language Jonathan Jewell (hyperpolymath) @@ -27,27 +28,40 @@ act that runs through all of them. == Architecture position -KRL is the surface language of a four-layer stack: +KRL is the surface language of a four-layer federated stack: ---- -KRL surface syntax ← this repository (TanglePL compiler module) +KRL surface syntax ← this repository (spec, ABI, FFI scaffolds) + implementations: KRLAdapter.jl, + quandledb/server/krl/ TangleIR ← canonical interchange object -VerisimMorphism ← abstract categorical view (VerisimCore) + defined in KRLAdapter.jl, consumed by + hyperpolymath/tangle +Tangle core ← proven type-safe small-step semantics + (hyperpolymath/tangle/proofs/Tangle.lean) Skein.jl + QuandleDB ← persistence and semantic indexing ---- -The TanglePL module (this repo) is responsible for: +*This repo* is responsible for: -* Parsing KRL source text -* Building and typechecking the AST -* Compiling AST to `TangleIR` -* Reconstructing source from IR (lossy but readable) +* The KRL grammar specification (`spec/grammar.ebnf`). +* Idris2 ABI types (`src/interface/Abi/`). +* Zig FFI scaffolds (`src/interface/ffi/`). +* Example programs (`examples/`). +* The proof narrative (`PROOF-NARRATIVE.md`) and obligations registry. -It is *not* responsible for: +The actual KRL parser, lowering, and adapter implementations live +in the companion repos `KRLAdapter.jl` (canonical) and +`quandledb/server/krl/` (server-side query parser — different role). +See `PROOF-NARRATIVE.md` for the two-implementation rationale and +the equivalence obligation `KR-6`. + +KRL is *not* responsible for: * Invariant computation (→ JuliaKnot.jl) * Persistence (→ Skein.jl) * Equivalence reasoning (→ QuandleDB) +* Surface-language implementation (→ KRLAdapter.jl) == The four KRL operations diff --git a/TEST-NEEDS.md b/TEST-NEEDS.md index 821a48f..0c3113e 100644 --- a/TEST-NEEDS.md +++ b/TEST-NEEDS.md @@ -1,107 +1,88 @@ -# TEST-NEEDS: rsr-template-repo - -## CRG Grade: C — ACHIEVED 2026-04-04 - -## Current State (Updated 2026-04-04) - -| Category | Count | Details | -|----------|-------|---------| -| **Source modules** | 6 | 3 Idris2 ABI (Foreign, Layout, Types), 2 Zig FFI (build, main), 1 Zig integration test template | -| **Unit tests** | 0 | None in main source (inline tests in main.zig) | -| **Integration tests** | 1 | test/integration_test.zig (documented template, 1 placeholder test) | -| **E2E tests** | 1 | tests/e2e/template_instantiation_test.sh (full instantiation + validation) | -| **Workflow tests** | 1 | tests/workflows/validate_workflows_test.sh (21 workflows validated) | -| **Validation tests** | 1 | scripts/validate-template.sh (8-phase comprehensive validation) | -| **Benchmarks** | 5 | benches/template_bench.sh (validation, Zig build, tests, workflows, instantiation) | -| **Fuzz tests** | 0 | README.adoc scaffold with harness instructions | - -## Completed Work (CRG C - Testing & Benchmarking) - -### Template Validation Script ✅ -- [x] `scripts/validate-template.sh` — 8-phase validation - - Phase 1: Core repository structure (root files, directories) - - Phase 2: Machine-readable metadata (.machine_readable/) - - Phase 3: GitHub Actions workflows (17 required + all present) - - Phase 4: Idris2 ABI and Zig FFI source files - - Phase 5: Placeholder token replacement (skipped in template) - - Phase 6: SPDX license headers (100% coverage, 6/6 files) - - Phase 7: Build system verification (zig build + idris2 syntax check) - - Phase 8: Documentation requirements (TOPOLOGY, ABI-FFI-README, etc) -- Status: **PASSING** (0 errors, 3 warnings about template placeholders) - -### E2E Template Instantiation Test ✅ -- [x] `tests/e2e/template_instantiation_test.sh` — full workflow - - Clones template to temp directory - - Replaces all {{PLACEHOLDER}} tokens with test values - - Validates resulting structure with scripts/validate-template.sh - - Verifies Zig build works after instantiation - - Checks no remaining placeholders - - Cleans up temp directory -- Status: **READY TO TEST** (can be verified by CI) - -### Workflow Validation Test ✅ -- [x] `tests/workflows/validate_workflows_test.sh` - - Validates all 21 workflows exist and have proper structure - - Checks SPDX headers, 'name' field - - Verifies all 15 required workflows present -- Status: **PASSING** (0 errors, 15/15 required workflows found) - -### Zig FFI Tests ✅ -- [x] `src/interface/ffi/test/integration_test.zig` — template with examples - - Converted from krl placeholders to "template" namespace - - Added comprehensive comments for how to instantiate - - Tests grouped by category (lifecycle, operations, strings, errors, version, memory safety, threading) - - Compiles and passes placeholder test -- Status: **PASSING** (1 test: placeholder_test_implementation_required passes) - -### Benchmarks ✅ -- [x] `benches/template_bench.sh` — 5 benchmark suites - - Validation script: ~5.8s average (3 runs) - - Zig build: ~19ms (clean build) - - Zig tests: ~20ms - - Workflow validation: ~117ms - - Template instantiation: ~427ms -- Formats: human, json, csv -- Status: **PASSING** (all benchmarks execute) - -### Build System ✅ -- [x] `src/interface/ffi/build.zig` — updated for Zig 0.15.2 - - Simplified to test-only configuration - - Supports both unit tests and integration tests - - Works with `zig build` without errors -- Status: **PASSING** (builds successfully) - -## Test Results Summary - -``` -Validation Script: PASS (0 errors, 3 warnings) -Workflow Validation: PASS (21/21 workflows valid) -Integration Tests: PASS (1/1 placeholder test) -E2E Instantiation: READY (needs CI confirmation) -Benchmarks: PASS (5/5 benchmark suites) -Build System: PASS (zig build succeeds) -``` - -## CRG C Compliance - -- **Coverage**: 6/6 test categories (unit, integration, E2E, workflow, validation, benchmarks) -- **Documentation**: All test files have SPDX headers + inline documentation -- **Author Attribution**: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com> -- **License**: MPL-2.0 on all new files -- **Automation**: All scripts executable + working - -## FLAGGED ISSUES - ALL RESOLVED - -- ~~**Template repo used by ALL new repos has 0 validation tests**~~ → FIXED: 4 test suites + validation script -- ~~**fuzz/placeholder.txt**~~ → FIXED: replaced with README.adoc containing real harness instructions -- ~~**No E2E tests for template instantiation**~~ → FIXED: full E2E test suite -- ~~**Zig FFI integration tests are placeholders**~~ → FIXED: converted to documented template format - -## Next Steps (Future Sessions) - -- [ ] Integrate test scripts into CI/CD workflows -- [ ] Generate test coverage reports -- [ ] Add more specialized benchmarks (memory, threading stress) -- [ ] Document test instantiation patterns for new repos - -## Priority: P0 (COMPLETE) ✅ + +# Test Requirements — KRL + +> Implementation-level proofs and their property-test stand-ins are in +> [PROOF-NEEDS.md](PROOF-NEEDS.md). This file is the **test-coverage +> register**: every test that exists, every test that should exist, +> and the CRG grade against `standards/component-readiness-grades`. + +## CRG Grade + +**Current grade:** D +**Last assessed:** 2026-06-01 (this audit). Promoted E → D 2026-04-12 +(see [READINESS.md](READINESS.md)). + +D grade criterion: "Works on some inputs, test matrix present." +The test matrix at the spec/grammar/example level is present in this +repo. The actual KRL parser/lower test suite (5577 tests) lives in +the canonical implementation `KRLAdapter.jl`. + +## Test inventory + +### In this repo + +| Path | Kind | What it covers | Status | +|------|------|----------------|--------| +| `tests/smoke/grammar_smoke.sh` | Shell smoke | 16 lexical assertions on grammar tokens | PASSING | +| `tests/aspect_tests.sh` | Shell | Aspect tagging (`src/aspects/`) | PASSING | +| `tests/e2e.sh` | Shell entry-point | Wraps the e2e suite | PASSING | +| `tests/e2e/template_instantiation_test.sh` | Shell E2E | Template instantiation end-to-end | PASSING (template artefact; flag for removal below) | +| `tests/workflows/validate_workflows_test.sh` | Shell | All `.github/workflows/` files have SPDX header + `name:` field | PASSING | +| `src/interface/ffi/test/integration_test.zig` | Zig | Placeholder FFI integration test | PASSING (`placeholder_test_implementation_required`) | +| `benches/template_bench.sh` | Shell | 5 micro-benchmarks (validation, build, tests, workflows, instantiation) | PASSING | + +### Out-of-repo (companion suites under proof for this repo's claims) + +| Path | Kind | What it covers | +|------|------|----------------| +| `KRLAdapter.jl/test/parser_test.jl` | Julia property | Lexer / parser / lower / 4 example programs (~57 dedicated parser tests) | +| `KRLAdapter.jl/test/*.jl` | Julia | Full KRLAdapter suite (~5577 tests) | +| `quandledb/server/krl/test/*.jl` | Julia | Server-side parser equivalence (lexer / parser / sql / seam — 1713 LoC) | + +## Gaps (what we owe) + +Cross-referenced to [PROOF-NEEDS.md](PROOF-NEEDS.md) and [PROOF-NARRATIVE.md](PROOF-NARRATIVE.md). + +| # | Test gap | Tied to | Effort | +|---|----------|---------|--------| +| TG-K1 | Round-trip property test: `parse(pretty(e)) = e` for every example | KR-4 | 4h | +| TG-K2 | Differential test: `KRLAdapter.jl::parse_krl(s) ≡ quandledb/server/krl::parse_any(s)` on a generated corpus | KR-6 | 4h | +| TG-K3 | Property test: `sigma 0`, `cup 0`, `cap 0` rejected; `sigma N` for `N ≥ 1` accepted | KR-7 | 1h | +| TG-K4 | Property test: lowering exhausts every `KRLExpr` variant (no `KRLLowerError` from un-matched case) | KR-1 / [[A-KR-1.1]] | 2h | +| TG-K5 | Property test: port-arity preservation on every `compose` and `tensor` in `examples/` | KR-2 | 4h | +| TG-K6 | Cross-platform fingerprint test (Linux/macOS/WSL) — coordinate with QuandleDB QD-4 | KR-8 / quandledb QD-4 | 1d | +| TG-K7 | Fuzz harness: random byte-strings → `parse_krl` → assert "either valid AST or `KRLParseError`, never a panic" | KR-1 | 1d | +| TG-K8 | Bench: parse-and-lower throughput vs program size (target: linear) | (perf) | 4h | +| TG-K9 | Bench: round-trip cost (`parse ∘ pretty`) on the example corpus | (perf) | 4h | + +## Removed (the template-content cleanup) + +The previous `TEST-NEEDS.md` was rsr-template-repo boilerplate +referring to "rsr-template-repo" throughout. Its claimed +**CRG Grade: C — ACHIEVED 2026-04-04** referred to the template +itself, not to KRL. That content has been removed; KRL's actual grade +is D, per [READINESS.md](READINESS.md). + +The template-specific test items (template instantiation, workflow +validation count, build-system zig 0.15.2 update, etc.) remain +inventoried above only because their files still exist; they should +be evaluated for removal when KRL gains repo-specific equivalents. + +## How to add a new test + +1. Add a row to **Test inventory** with path, kind, what-it-covers, status. +2. If it discharges a proof obligation, reference the `KR-N` id and + note in [PROOF-NARRATIVE.md](PROOF-NARRATIVE.md) under the + relevant obligation's "How to discharge" line. +3. If new assumptions emerge, register them in [ASSUMPTIONS.md](ASSUMPTIONS.md). + +## CRG path forward + +- **D → C:** Implement the typechecker (KR-2), discharge KR-1 and KR-4 + as property tests, demonstrate parsing 20+ programs from the knot table. +- **C → B:** 6+ diverse external targets writing KRL programs. +- **B → A:** All P1 obligations in PROOF-NEEDS proven (not just + property-tested). diff --git a/verification/proofs/coq/TypeSafety.v b/verification/proofs/coq/TypeSafety.v deleted file mode 100644 index 8f5b418..0000000 --- a/verification/proofs/coq/TypeSafety.v +++ /dev/null @@ -1,73 +0,0 @@ -(* SPDX-License-Identifier: MPL-2.0 *) -(* Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) *) -(* - Coq Proof Template: Type system soundness - Replace with your project's type system proofs. - All proofs must be complete — NO Admitted allowed. -*) - -Require Import Coq.Lists.List. -Require Import Coq.Arith.Arith. -Require Import Coq.Bool.Bool. -Import ListNotations. - -(** * Example: Simple expression language with type safety *) -(** Replace this entire section with your project's type system. *) - -(** Types *) -Inductive ty : Type := - | TyNat : ty - | TyBool : ty. - -(** Expressions *) -Inductive expr : Type := - | EConst : nat -> expr - | ETrue : expr - | EFalse : expr - | EPlus : expr -> expr -> expr - | EEq : expr -> expr -> expr. - -(** Values *) -Inductive value : Type := - | VNat : nat -> value - | VBool : bool -> value. - -(** Typing relation *) -Inductive has_type : expr -> ty -> Prop := - | T_Const : forall n, has_type (EConst n) TyNat - | T_True : has_type ETrue TyBool - | T_False : has_type EFalse TyBool - | T_Plus : forall e1 e2, - has_type e1 TyNat -> has_type e2 TyNat -> - has_type (EPlus e1 e2) TyNat - | T_Eq : forall e1 e2, - has_type e1 TyNat -> has_type e2 TyNat -> - has_type (EEq e1 e2) TyBool. - -(** Evaluation *) -Inductive eval : expr -> value -> Prop := - | E_Const : forall n, eval (EConst n) (VNat n) - | E_True : eval ETrue (VBool true) - | E_False : eval EFalse (VBool false) - | E_Plus : forall e1 e2 n1 n2, - eval e1 (VNat n1) -> eval e2 (VNat n2) -> - eval (EPlus e1 e2) (VNat (n1 + n2)) - | E_Eq : forall e1 e2 n1 n2, - eval e1 (VNat n1) -> eval e2 (VNat n2) -> - eval (EEq e1 e2) (VBool (Nat.eqb n1 n2)). - -(** Value typing *) -Definition value_has_type (v : value) (t : ty) : Prop := - match v, t with - | VNat _, TyNat => True - | VBool _, TyBool => True - | _, _ => False - end. - -(** Type soundness: well-typed expressions evaluate to well-typed values *) -Theorem type_soundness : forall e t v, - has_type e t -> eval e v -> value_has_type v t. -Proof. - intros e t v Htype Heval. - induction Htype; inversion Heval; subst; simpl; auto. -Qed. diff --git a/verification/proofs/idris2/ABI/Compliance.idr b/verification/proofs/idris2/ABI/Compliance.idr deleted file mode 100644 index d38c0d5..0000000 --- a/verification/proofs/idris2/ABI/Compliance.idr +++ /dev/null @@ -1,41 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) --- --- ABI Proof: C ABI compliance --- Proves that struct layouts are C ABI compliant. --- All proofs MUST be constructive (no believe_me, no assert_total). - -module ABI.Compliance - -import ABI.Layout -import ABI.Platform - -%default total - -||| Evidence that every field in a layout is correctly aligned. -public export -data AllFieldsAligned : List StructField -> Type where - AFANil : AllFieldsAligned [] - AFACons : FieldAligned f -> AllFieldsAligned fs -> AllFieldsAligned (f :: fs) - -||| Evidence that every field is within the struct bounds. -public export -data AllFieldsInBounds : (size : Nat) -> List StructField -> Type where - AFBNil : AllFieldsInBounds size [] - AFBCons : FieldInBounds size f -> AllFieldsInBounds size fs -> AllFieldsInBounds size (f :: fs) - -||| A struct layout is C ABI compliant when: -||| 1. All fields are aligned to their natural alignment -||| 2. All fields are within bounds of the struct size -||| 3. The struct size is a multiple of the struct alignment -public export -record CABICompliant (layout : StructLayout) where - constructor MkCompliant - fieldsAligned : AllFieldsAligned (layoutFields layout) - fieldsInBounds : AllFieldsInBounds (layoutSize layout) (layoutFields layout) - sizeAligned : modNatNZ (layoutSize layout) (layoutAlignment layout) SIsNonZero = 0 - -||| An empty struct is trivially compliant (size=1, alignment=1). -export -emptyStructCompliant : CABICompliant (MkLayout "empty" [] 1 1) -emptyStructCompliant = MkCompliant AFANil AFBNil Refl diff --git a/verification/proofs/idris2/ABI/Foreign.idr b/verification/proofs/idris2/ABI/Foreign.idr deleted file mode 100644 index cb98ecd..0000000 --- a/verification/proofs/idris2/ABI/Foreign.idr +++ /dev/null @@ -1,53 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) --- --- ABI Proof: FFI function return type proofs --- Proves that all FFI functions return expected types. --- All proofs MUST be constructive (no believe_me, no assert_total). - -module ABI.Foreign - -%default total - -||| Result type for FFI operations. -||| All FFI functions must return through this type. -public export -data FFIResult : Type -> Type where - FFISuccess : (value : a) -> FFIResult a - FFIError : (code : Int) -> (msg : String) -> FFIResult a - -||| Proof that FFIResult is a functor (map preserves structure). -export -mapFFIResult : (a -> b) -> FFIResult a -> FFIResult b -mapFFIResult f (FFISuccess value) = FFISuccess (f value) -mapFFIResult f (FFIError code msg) = FFIError code msg - -||| Proof that mapping identity preserves the result. -export -mapIdPreserves : (r : FFIResult a) -> mapFFIResult Prelude.id r = r -mapIdPreserves (FFISuccess value) = Refl -mapIdPreserves (FFIError code msg) = Refl - -||| An FFI function specification: name, argument types, return type. -public export -record FFISpec where - constructor MkFFISpec - ffiName : String - ffiReturnType : Type - -||| Proof that an FFI spec has a specific return type. -||| Use this to verify at compile time that FFI functions return the -||| types we expect across the C ABI boundary. -public export -FFIReturns : FFISpec -> Type -> Type -FFIReturns spec ty = ffiReturnType spec = ty - -||| C calling convention marker. -||| Proofs about calling convention compatibility. -public export -data CallingConv = CDecl | StdCall | FastCall - -||| All hyperpolymath FFI uses CDecl. -public export -defaultCallingConv : CallingConv -defaultCallingConv = CDecl diff --git a/verification/proofs/idris2/ABI/Layout.idr b/verification/proofs/idris2/ABI/Layout.idr deleted file mode 100644 index f38fcca..0000000 --- a/verification/proofs/idris2/ABI/Layout.idr +++ /dev/null @@ -1,63 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) --- --- ABI Proof: Memory layout correctness --- Proves struct size, alignment, and padding properties. --- All proofs MUST be constructive (no believe_me, no assert_total). - -module ABI.Layout - -%default total - -||| Witness that a type has a known size in bytes at compile time. -public export -interface HasSize (ty : Type) where - sizeOf : Nat - -||| Witness that a type has a known alignment in bytes. -public export -interface HasAlignment (ty : Type) where - alignOf : Nat - -||| Calculate padding needed to reach the next aligned offset. -||| paddingFor offset alignment = bytes to add so (offset + padding) `mod` alignment == 0 -public export -paddingFor : (offset : Nat) -> (alignment : Nat) -> {auto 0 ok : NonZero alignment} -> Nat -paddingFor offset alignment = let r = modNatNZ offset alignment ok - in case r of - Z => Z - (S _) => minus alignment r - -||| Proof that an offset with zero remainder needs zero padding. -export -alignedNeedsPadding : (n : Nat) -> (a : Nat) -> {auto 0 ok : NonZero a} -> - modNatNZ n a ok = 0 -> paddingFor n a = 0 -alignedNeedsPadding n a prf = rewrite prf in Refl - -||| A field within a struct, carrying its offset and size. -public export -record StructField where - constructor MkField - fieldName : String - fieldOffset : Nat - fieldSize : Nat - fieldAlignment : Nat - -||| Proof that a field is correctly aligned within a struct. -public export -FieldAligned : StructField -> Type -FieldAligned f = modNatNZ (fieldOffset f) (fieldAlignment f) SIsNonZero = 0 - -||| Proof that a field does not overflow past a given struct size. -public export -FieldInBounds : (structSize : Nat) -> StructField -> Type -FieldInBounds sz f = LTE (fieldOffset f + fieldSize f) sz - -||| A struct layout is a list of fields with a total size. -public export -record StructLayout where - constructor MkLayout - layoutName : String - layoutFields : List StructField - layoutSize : Nat - layoutAlignment : Nat diff --git a/verification/proofs/idris2/ABI/Platform.idr b/verification/proofs/idris2/ABI/Platform.idr deleted file mode 100644 index 6b80d20..0000000 --- a/verification/proofs/idris2/ABI/Platform.idr +++ /dev/null @@ -1,63 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) --- --- ABI Proof: Platform-specific type size proofs --- Proves that C type sizes are correct per platform. --- All proofs MUST be constructive (no believe_me, no assert_total). - -module ABI.Platform - -%default total - -||| Supported target platforms for ABI verification. -public export -data Platform = Linux64 | LinuxARM64 | MacOS64 | MacOSARM64 - | Windows64 | FreeBSD64 | WASM32 - -||| Pointer size in bytes for each platform. -public export -ptrSize : Platform -> Nat -ptrSize WASM32 = 4 -ptrSize _ = 8 - -||| C `int` size in bytes. -public export -cIntSize : Platform -> Nat -cIntSize _ = 4 - -||| C `size_t` size in bytes (matches pointer size). -public export -cSizeT : Platform -> Nat -cSizeT = ptrSize - -||| Proof that size_t always equals pointer size on all platforms. -export -sizeTEqPtrSize : (p : Platform) -> cSizeT p = ptrSize p -sizeTEqPtrSize _ = Refl - -||| Proof that pointer size is always 4 or 8 bytes. -export -ptrSizeValid : (p : Platform) -> Either (ptrSize p = 4) (ptrSize p = 8) -ptrSizeValid WASM32 = Left Refl -ptrSizeValid Linux64 = Right Refl -ptrSizeValid LinuxARM64 = Right Refl -ptrSizeValid MacOS64 = Right Refl -ptrSizeValid MacOSARM64 = Right Refl -ptrSizeValid Windows64 = Right Refl -ptrSizeValid FreeBSD64 = Right Refl - -||| Proof that C int is always 4 bytes on all platforms. -export -cIntAlways4 : (p : Platform) -> cIntSize p = 4 -cIntAlways4 _ = Refl - -||| Proof that pointer size is always at least 4 bytes. -export -ptrSizeAtLeast4 : (p : Platform) -> LTE 4 (ptrSize p) -ptrSizeAtLeast4 WASM32 = lteRefl -ptrSizeAtLeast4 Linux64 = lteSuccRight (lteSuccRight (lteSuccRight (lteSuccRight lteRefl))) -ptrSizeAtLeast4 LinuxARM64 = lteSuccRight (lteSuccRight (lteSuccRight (lteSuccRight lteRefl))) -ptrSizeAtLeast4 MacOS64 = lteSuccRight (lteSuccRight (lteSuccRight (lteSuccRight lteRefl))) -ptrSizeAtLeast4 MacOSARM64 = lteSuccRight (lteSuccRight (lteSuccRight (lteSuccRight lteRefl))) -ptrSizeAtLeast4 Windows64 = lteSuccRight (lteSuccRight (lteSuccRight (lteSuccRight lteRefl))) -ptrSizeAtLeast4 FreeBSD64 = lteSuccRight (lteSuccRight (lteSuccRight (lteSuccRight lteRefl))) diff --git a/verification/proofs/idris2/ABI/Pointers.idr b/verification/proofs/idris2/ABI/Pointers.idr deleted file mode 100644 index 49efd2f..0000000 --- a/verification/proofs/idris2/ABI/Pointers.idr +++ /dev/null @@ -1,52 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) --- --- ABI Proof: Non-null pointer safety --- Template proof — customise for your project's pointer types. --- All proofs MUST be constructive (no believe_me, no assert_total). - -module ABI.Pointers - -import Data.So - -%default total - -||| A pointer value that has been proven non-null. -||| The `So` constraint carries a compile-time witness that `ptr /= 0`. -public export -record SafePtr where - constructor MkSafePtr - ptr : Bits64 - {auto 0 nonNull : So (ptr /= 0)} - -||| Proof that SafePtr can never hold a null (zero) value. -||| This is enforced by the `So` constraint in the record. -export -safePtrNeverNull : (sp : SafePtr) -> So (sp.ptr /= 0) -safePtrNeverNull sp = sp.nonNull - -||| Wrap a raw pointer with a runtime null check. -||| Returns Nothing if the pointer is null. -export -checkPtr : (raw : Bits64) -> Maybe SafePtr -checkPtr 0 = Nothing -checkPtr raw = case choose (raw /= 0) of - Left prf => Just (MkSafePtr raw) - Right _ => Nothing - -||| Proof that checkPtr 0 always returns Nothing. -export -checkPtrZeroIsNothing : checkPtr 0 = Nothing -checkPtrZeroIsNothing = Refl - -||| An opaque handle backed by a non-null pointer. -||| Use this for FFI resource handles (file descriptors, sockets, etc.). -public export -record Handle (tag : String) where - constructor MkHandle - safePtr : SafePtr - -||| Proof that two handles with equal pointers are equal. -export -handlePtrEq : (h1, h2 : Handle tag) -> h1.safePtr.ptr = h2.safePtr.ptr -> h1 = h2 -handlePtrEq (MkHandle (MkSafePtr p)) (MkHandle (MkSafePtr p)) Refl = Refl diff --git a/verification/proofs/idris2/Types.idr b/verification/proofs/idris2/Types.idr deleted file mode 100644 index 85ea9b7..0000000 --- a/verification/proofs/idris2/Types.idr +++ /dev/null @@ -1,38 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) --- --- Typing Proof: Core data type well-formedness --- Template — replace with your project's core types. --- All proofs MUST be constructive (no believe_me, no assert_total). - -module Types - -%default total - -||| Example: A bounded natural number (0 to max). -||| Replace with your project's core types. -public export -record Bounded (max : Nat) where - constructor MkBounded - value : Nat - {auto 0 inBounds : LTE value max} - -||| Proof that a Bounded value is always <= max. -export -boundedLeMax : (b : Bounded max) -> LTE b.value max -boundedLeMax b = b.inBounds - -||| Proof that zero is always a valid Bounded value. -export -zeroIsBounded : {max : Nat} -> Bounded (S max) -zeroIsBounded = MkBounded 0 - -||| Example: A non-empty list with a compile-time guarantee. -public export -data NonEmpty : List a -> Type where - IsNonEmpty : NonEmpty (x :: xs) - -||| Proof that cons always produces a non-empty list. -export -consIsNonEmpty : (x : a) -> (xs : List a) -> NonEmpty (x :: xs) -consIsNonEmpty _ _ = IsNonEmpty diff --git a/verification/proofs/lean4/ApiTypes.lean b/verification/proofs/lean4/ApiTypes.lean deleted file mode 100644 index 9ed78b7..0000000 --- a/verification/proofs/lean4/ApiTypes.lean +++ /dev/null @@ -1,44 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) --- --- Typing Proof: Public API type safety --- Template — replace with your project's API types. --- Proves properties about exported function signatures. - --- Example: Result type used across API boundaries -inductive ApiResult (α : Type) where - | ok : α → ApiResult α - | error : Nat → String → ApiResult α - -namespace ApiResult - -- Proof: map preserves structure (functor law: map id = id) - def map (f : α → β) : ApiResult α → ApiResult β - | .ok v => .ok (f v) - | .error c m => .error c m - - theorem map_id : ∀ (r : ApiResult α), map id r = r := by - intro r - cases r with - | ok v => simp [map] - | error c m => simp [map] - - -- Proof: map composition (functor law: map (g ∘ f) = map g ∘ map f) - theorem map_comp (f : α → β) (g : β → γ) : - ∀ (r : ApiResult α), map (g ∘ f) r = map g (map f r) := by - intro r - cases r with - | ok v => simp [map, Function.comp] - | error c m => simp [map] - --- Example: Bounded confidence value (0.0 to 1.0 modelled as Nat/1000) --- Replace with your project's numeric invariants -structure BoundedNat (max : Nat) where - val : Nat - le_max : val ≤ max - -theorem bounded_nat_le (b : BoundedNat max) : b.val ≤ max := - b.le_max - --- Proof: zero is always bounded -def zeroBounded (h : 0 < max) : BoundedNat max := - ⟨0, Nat.zero_le max⟩