diff --git a/ARCHITECTURE.adoc b/ARCHITECTURE.adoc new file mode 100644 index 0000000..1c0a7a6 --- /dev/null +++ b/ARCHITECTURE.adoc @@ -0,0 +1,48 @@ +== Architecture + +=== Overview + +This repository follows a modular, maintainable architecture designed +for clarity, scalability, and long-term sustainability. + +=== Directory Structure + +.... +. +├── src/ # Source code +├── tests/ # Test suites +├── docs/ # Documentation +├── scripts/ # Utility scripts +├── config/ # Configuration files +├── LICENSE # License file +├── LICENSES/ # Full license texts +└── README.adoc # Project documentation +.... + +=== Design Principles + +* *Separation of Concerns*: Each module has a single responsibility +* *Testability*: Code is written to be easily testable +* *Documentation*: All public APIs are documented +* *Configuration*: Environment-specific settings are externalized + +=== Dependencies + +* External dependencies are minimized and clearly declared +* Version pinning is used for reproducibility + +=== Security Considerations + +* Sensitive data is never committed to the repository +* Secrets are managed through environment variables or secure vaults +* Regular dependency audits are performed + +=== Maintainability + +* Code follows consistent style guidelines +* Pull requests require review and CI checks +* Issues and discussions are tracked transparently + +''''' + +_Last updated: 2026-07-18_ diff --git a/ARCHITECTURE.md b/ARCHITECTURE.md deleted file mode 100644 index 607e3d8..0000000 --- a/ARCHITECTURE.md +++ /dev/null @@ -1,47 +0,0 @@ -# Architecture - -## Overview - -This repository follows a modular, maintainable architecture designed for clarity, scalability, and long-term sustainability. - -## Directory Structure - -``` -. -├── src/ # Source code -├── tests/ # Test suites -├── docs/ # Documentation -├── scripts/ # Utility scripts -├── config/ # Configuration files -├── LICENSE # License file -├── LICENSES/ # Full license texts -└── README.adoc # Project documentation -``` - -## Design Principles - -- **Separation of Concerns**: Each module has a single responsibility -- **Testability**: Code is written to be easily testable -- **Documentation**: All public APIs are documented -- **Configuration**: Environment-specific settings are externalized - -## Dependencies - -- External dependencies are minimized and clearly declared -- Version pinning is used for reproducibility - -## Security Considerations - -- Sensitive data is never committed to the repository -- Secrets are managed through environment variables or secure vaults -- Regular dependency audits are performed - -## Maintainability - -- Code follows consistent style guidelines -- Pull requests require review and CI checks -- Issues and discussions are tracked transparently - ---- - -*Last updated: 2026-07-18* diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc new file mode 100644 index 0000000..2bdadc6 --- /dev/null +++ b/CHANGELOG.adoc @@ -0,0 +1,70 @@ +== Changelog + +All notable changes to this project will be documented in this file. + +The format is based on https://keepachangelog.com/en/1.1.0/[Keep a +Changelog], and this project adheres to +https://semver.org/spec/v2.0.0.html[Semantic Versioning]. + +=== [Unreleased] + +==== Fixed + +* *Formal proofs now actually machine-check.* The 7 Idris2/Lean4 proofs +were marked "`100% proven`" since 2026-04-16, but +`+Foreign+`/`+Platform+`/`+Compliance+` never compiled (Idris2 +unbound-implicit auto-binding; unary-`+Nat+` blow-up on 65536-scale +arithmetic) and no CI job ever ran a prover. All 6 Idris2 modules + the +Lean4 module now pass. +* *Justfile was unparseable by `+just+`* (line 2 used `+//+` instead of +`+#+`), which broke every recipe including `+build-wasm+` used by the +e2e gate. Fixed. +* *Proof gate was decorative.* `+just proof-check-*+` used a broken +`+idris2 --check+` invocation (no `+--source-dir+`, never resolved the +`+ABI.*+` graph) and silently passed when the prover was absent (SKIP = +exit 0). Now uses the correct invocation and fails-on-skip. +* *`+checked_add+` made genuinely checked.* The export was a wrapping +`+a +% b+` despite its name (the GAP-1b metamorphic gate surfaced the +misnomer). It is now a real checked add: overflow TRAPS +(`+@addWithOverflow+` + `+unreachable+` → WASM trap → `+{:error, _}+`, +BEAM survives) in all build modes, and a non-overflowing add returns the +exact sum. Signature unchanged (the ABI gate stays green); the +metamorphic oracle now asserts trap-on-overflow. + +==== Changed + +* Project gloss *"`Safe NIFs`" → "`Safer NIFs`"* (acronym SNIF +unchanged): WASM sandboxing makes NIFs _safer_, not provably _safe_. +Living docs + paper/citation titles updated. NOTE: the paper carries +Zenodo DOI 10.5281/zenodo.19520245 under the old title — the rename +should be reflected on the next Zenodo version/deposit. +* Re-modeled `+Platform.idr+` WASM memory-size facts over `+Integer+` +(was unary `+Nat+`). + +==== Added + +* `+.github/workflows/proofs.yml+` — real CI proof gate (Idris2 + Lean4 +via Nix). +* *SNIFs 2 — sharpened verification.* SEC-1 (`+SnifIsolation.agda+`) now +wires confidentiality into the operational theorem (deniability +re-derived over the actual run via `+run-deniable+` / +`+fault-via-observe+` + a two-distinct-secret `+SecretWitness+`), models +the real 6-origin error taxonomy (`+TrapOrigin+` guestFault / hostBudget +/ preExec + a `+call+` front-end + `+PreExecWitness+`), and adds a +non-trivial-`+Alive+` recovery witness (`+PartialAlive+`) — all +mutation-confirmed load-bearing by a 4-skeptic adversarial re-audit +(`+--safe --without-K+`, every targeted mutation rejected). +* *ABI-7 buffer-guest coverage.* +`+verification/proofs/idris2/ABI/BufferAbi.idr+` models all 7 +`+buffer_abi+` exports (multi-value/void-faithful `+WasmSig+`), raising +gated ABI coverage to 15 of 20 Zig export sites; +`+verification/tools/abi_conformance.py+` is now guest-aware (per-guest +model manifest, multi-value/void parsing). The conformance gate now runs +in CI (`+proofs.yml+`, CI-1). +* *GAP-1b behaviour gate.* `+demo/test/snif_metamorphic_test.exs+` — +dependency-free metamorphic relations over the scalar kernels (fibonacci +recurrence + base cases; `+checked_add+` non-overflow = exact-sum / +overflow = trap oracle). +* `+AFFIRMATION.adoc+` — point-in-time, ground-truthed honesty snapshot +(the README/EXPLAINME/AFFIRMATION trio); SPDX header parked for the +owner to add + sign. diff --git a/CHANGELOG.md b/CHANGELOG.md deleted file mode 100644 index 5ff729e..0000000 --- a/CHANGELOG.md +++ /dev/null @@ -1,58 +0,0 @@ - -# Changelog - -All notable changes to this project will be documented in this file. - -The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/), -and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html). - - - - -## [Unreleased] - -### Fixed -- **Formal proofs now actually machine-check.** The 7 Idris2/Lean4 proofs were marked - "100% proven" since 2026-04-16, but `Foreign`/`Platform`/`Compliance` never compiled - (Idris2 unbound-implicit auto-binding; unary-`Nat` blow-up on 65536-scale arithmetic) - and no CI job ever ran a prover. All 6 Idris2 modules + the Lean4 module now pass. -- **Justfile was unparseable by `just`** (line 2 used `//` instead of `#`), which broke - every recipe including `build-wasm` used by the e2e gate. Fixed. -- **Proof gate was decorative.** `just proof-check-*` used a broken `idris2 --check` - invocation (no `--source-dir`, never resolved the `ABI.*` graph) and silently passed - when the prover was absent (SKIP = exit 0). Now uses the correct invocation and - fails-on-skip. -- **`checked_add` made genuinely checked.** The export was a wrapping `a +% b` despite its name - (the GAP-1b metamorphic gate surfaced the misnomer). It is now a real checked add: overflow - TRAPS (`@addWithOverflow` + `unreachable` → WASM trap → `{:error, _}`, BEAM survives) in all - build modes, and a non-overflowing add returns the exact sum. Signature unchanged (the ABI gate - stays green); the metamorphic oracle now asserts trap-on-overflow. - -### Changed -- Project gloss **"Safe NIFs" → "Safer NIFs"** (acronym SNIF unchanged): WASM sandboxing - makes NIFs *safer*, not provably *safe*. Living docs + paper/citation titles updated. - NOTE: the paper carries Zenodo DOI 10.5281/zenodo.19520245 under the old title — the - rename should be reflected on the next Zenodo version/deposit. -- Re-modeled `Platform.idr` WASM memory-size facts over `Integer` (was unary `Nat`). - -### Added -- `.github/workflows/proofs.yml` — real CI proof gate (Idris2 + Lean4 via Nix). -- **SNIFs 2 — sharpened verification.** SEC-1 (`SnifIsolation.agda`) now wires confidentiality into - the operational theorem (deniability re-derived over the actual run via `run-deniable` / - `fault-via-observe` + a two-distinct-secret `SecretWitness`), models the real 6-origin error - taxonomy (`TrapOrigin` guestFault / hostBudget / preExec + a `call` front-end + `PreExecWitness`), - and adds a non-trivial-`Alive` recovery witness (`PartialAlive`) — all mutation-confirmed - load-bearing by a 4-skeptic adversarial re-audit (`--safe --without-K`, every targeted mutation - rejected). -- **ABI-7 buffer-guest coverage.** `verification/proofs/idris2/ABI/BufferAbi.idr` models all 7 - `buffer_abi` exports (multi-value/void-faithful `WasmSig`), raising gated ABI coverage to 15 of 20 - Zig export sites; `verification/tools/abi_conformance.py` is now guest-aware (per-guest model - manifest, multi-value/void parsing). The conformance gate now runs in CI (`proofs.yml`, CI-1). -- **GAP-1b behaviour gate.** `demo/test/snif_metamorphic_test.exs` — dependency-free metamorphic - relations over the scalar kernels (fibonacci recurrence + base cases; `checked_add` - non-overflow = exact-sum / overflow = trap oracle). -- `AFFIRMATION.adoc` — point-in-time, ground-truthed honesty snapshot (the README/EXPLAINME/AFFIRMATION - trio); SPDX header parked for the owner to add + sign. diff --git a/CODE_OF_CONDUCT.adoc b/CODE_OF_CONDUCT.adoc new file mode 100644 index 0000000..bd2a83c --- /dev/null +++ b/CODE_OF_CONDUCT.adoc @@ -0,0 +1,24 @@ +== Contributor Covenant Code of Conduct + +=== Our Pledge + +We pledge to make participation a harassment-free experience for +everyone. + +=== Our Standards + +*Positive behavior:* * Using welcoming language * Being respectful of +differing viewpoints * Accepting constructive criticism * Focusing on +what is best for the community + +*Unacceptable behavior:* * Harassment, trolling, or personal attacks * +Publishing private information without permission + +=== Enforcement + +Report issues to the maintainers. All complaints will be reviewed. + +=== Attribution + +Adapted from https://www.contributor-covenant.org/[Contributor Covenant] +v2.1. diff --git a/CODE_OF_CONDUCT.md b/CODE_OF_CONDUCT.md deleted file mode 100644 index bbe9219..0000000 --- a/CODE_OF_CONDUCT.md +++ /dev/null @@ -1,30 +0,0 @@ - -# Contributor Covenant Code of Conduct - -## Our Pledge - -We pledge to make participation a harassment-free experience for everyone. - -## Our Standards - -**Positive behavior:** -* Using welcoming language -* Being respectful of differing viewpoints -* Accepting constructive criticism -* Focusing on what is best for the community - -**Unacceptable behavior:** -* Harassment, trolling, or personal attacks -* Publishing private information without permission - -## Enforcement - -Report issues to the maintainers. All complaints will be reviewed. - -## Attribution - -Adapted from [Contributor Covenant](https://www.contributor-covenant.org/) v2.1. - diff --git a/CONTRIBUTING.adoc b/CONTRIBUTING.adoc new file mode 100644 index 0000000..5949bf0 --- /dev/null +++ b/CONTRIBUTING.adoc @@ -0,0 +1,9 @@ +== Contributing + +[arabic] +. Fork the repository +. Create a feature branch +. Ensure SPDX headers on all files +. Submit a pull request + +*Author:* Jonathan D.A. Jewell j.d.a.jewell@open.ac.uk diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md deleted file mode 100644 index b7e3340..0000000 --- a/CONTRIBUTING.md +++ /dev/null @@ -1,12 +0,0 @@ - -# Contributing - -1. Fork the repository -2. Create a feature branch -3. Ensure SPDX headers on all files -4. Submit a pull request - -**Author:** Jonathan D.A. Jewell diff --git a/GOVERNANCE.adoc b/GOVERNANCE.adoc new file mode 100644 index 0000000..9b836fb --- /dev/null +++ b/GOVERNANCE.adoc @@ -0,0 +1,60 @@ +== Governance + +=== Overview + +This project is governed by the following principles and structures to +ensure transparent, inclusive, and effective decision-making. + +=== Roles and Responsibilities + +==== Maintainers + +Maintainers are responsible for: - Reviewing and merging pull requests - +Managing releases and versioning - Ensuring code quality and standards - +Triaging issues and bug reports - Community engagement and support + +==== Contributors + +Contributors are expected to: - Follow the code of conduct - Submit +well-documented pull requests - Write tests for new functionality - +Maintain existing tests - Update documentation as needed + +=== Decision Making + +==== Minor Changes + +* Can be made by any maintainer +* Include bug fixes, documentation updates, dependency updates + +==== Major Changes + +* Require discussion in issues or pull requests +* Include new features, architectural changes, API changes +* Need approval from at least 2 maintainers + +==== Breaking Changes + +* Require RFC (Request for Comments) process +* Need approval from majority of maintainers +* Must include migration guide + +=== Code of Conduct + +All participants are expected to follow our Code of Conduct. Violations +can be reported to the maintainers. + +=== Communication + +* *Issues*: For bug reports and feature requests +* *Discussions*: For questions and general discussion +* *Pull Requests*: For code contributions + +=== Licensing + +All contributions are made under the terms of the repository’s LICENSE +file. By submitting a pull request, you agree to license your +contributions accordingly. + +''''' + +_Last updated: 2026-07-18_ diff --git a/GOVERNANCE.md b/GOVERNANCE.md deleted file mode 100644 index e27364c..0000000 --- a/GOVERNANCE.md +++ /dev/null @@ -1,60 +0,0 @@ -# Governance - -## Overview - -This project is governed by the following principles and structures to ensure transparent, inclusive, and effective decision-making. - -## Roles and Responsibilities - -### Maintainers - -Maintainers are responsible for: -- Reviewing and merging pull requests -- Managing releases and versioning -- Ensuring code quality and standards -- Triaging issues and bug reports -- Community engagement and support - -### Contributors - -Contributors are expected to: -- Follow the code of conduct -- Submit well-documented pull requests -- Write tests for new functionality -- Maintain existing tests -- Update documentation as needed - -## Decision Making - -### Minor Changes -- Can be made by any maintainer -- Include bug fixes, documentation updates, dependency updates - -### Major Changes -- Require discussion in issues or pull requests -- Include new features, architectural changes, API changes -- Need approval from at least 2 maintainers - -### Breaking Changes -- Require RFC (Request for Comments) process -- Need approval from majority of maintainers -- Must include migration guide - -## Code of Conduct - -All participants are expected to follow our Code of Conduct. Violations can be reported to the maintainers. - -## Communication - -- **Issues**: For bug reports and feature requests -- **Discussions**: For questions and general discussion -- **Pull Requests**: For code contributions - -## Licensing - -All contributions are made under the terms of the repository's LICENSE file. -By submitting a pull request, you agree to license your contributions accordingly. - ---- - -*Last updated: 2026-07-18* diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc new file mode 100644 index 0000000..a87d050 --- /dev/null +++ b/PROOF-NEEDS.adoc @@ -0,0 +1,199 @@ +== Proof Requirements — SNIFs (Safer NIFs) + +____ +*Standing requirements catalogue.* This file lists the proof obligations +this repo _commits to carrying_. For the *live status* of each (proven / +tested / trusted, with the adversarial-audit caveats), see +link:PROOF-STATUS.md[`+PROOF-STATUS.md+`] — that is the authoritative +tracker; this file is the more stable "`what must exist and why`". +____ + +=== Proof Tier + +*Tier*: *T2 — High.* SNIF’s entire value proposition is a _safety_ claim +(a guest fault becomes `+{:error,_}+` and the BEAM survives), so the +operational isolation theorem (SEC-1) and the ABI boundary are +load-bearing. It is not T1 only because the residual +runtime-faithfulness assumption (`+wasmtime ⊨ FaithfulRuntime+`) is +explicitly _trusted_, not yet machine-verified — which is exactly why +the product is "`Safer`", not "`Safe`". + +=== Proof Categories + +[width="100%",cols="24%,36%,40%",options="header",] +|=== +|Code |Meaning |Applies? +|*TP* |Typing Proofs (type soundness, type safety) |*Yes* — result-type +algebra, verdict model + +|*INV* |Invariant Proofs (state machines, monotonicity, bounds) |Partial +— fuel/liveness bound in SEC-1 + +|*SEC* |Security Proofs (crypto, injection freedom, access control) +|*Yes* — SEC-1 crash isolation + deniability + +|*CONC* |Concurrency Proofs (linearizability, deadlock freedom) |No +(pool isolation is tested, not proven) + +|*ALG* |Algorithm Proofs (termination, correctness, bounds) |Partial — +run termination via fuel + +|*ABI* |ABI/FFI Proofs (memory layout, pointer safety, platform compat) +|*Yes* — the guest export boundary + +|*DOM* |Domain-Specific Proofs (bespoke to this project) |*Yes* — +echo×epistemic verdict bridge +|=== + +=== Mandatory Proofs (All RSR Repos) + +ABI/FFI boundary (Idris2) and core typing — all present and CI-gated by +`+just proof-check-all+`: + +[width="100%",cols="13%,29%,33%,25%",options="header",] +|=== +|# |Proof |Status |File +|ABI-1 |Non-null pointer proofs (`+So (ptr /= 0)+`) |✅ Gated +|`+verification/proofs/idris2/ABI/Pointers.idr+` + +|ABI-2 |Memory layout correctness (`+HasSize+`, `+HasAlignment+`) |✅ +Gated |`+verification/proofs/idris2/ABI/Layout.idr+` + +|ABI-3 |Platform type size proofs |✅ Gated +|`+verification/proofs/idris2/ABI/Platform.idr+` + +|ABI-4 |FFI function return-type proofs (safe_nif, 8 exports) |✅ Gated +|`+verification/proofs/idris2/ABI/Foreign.idr+` + +|ABI-5 |C ABI compliance (`+CABICompliant+`, `+FieldsAligned+`) |✅ +Gated |`+verification/proofs/idris2/ABI/Compliance.idr+` + +|TP-1 |Core data-type well-formedness |✅ Gated +|`+verification/proofs/idris2/Types.idr+` + +|TP-2 |Public API type safety (exported functions) |✅ Gated +|`+verification/proofs/lean4/ApiTypes.lean+` +|=== + +=== Project-Specific Proofs + +[width="100%",cols="9%,25%,19%,15%,15%,17%",options="header",] +|=== +|# |Proof Needed |Category |Prover |Status |File(s) +|SEC-1 |Operational crash-isolation: guest fault ⇒ `+{:error,_}+` ∧ host +survives, over a fuelled host↔guest run, _modulo_ the explicit +`+FaithfulRuntime+` TCB |SEC |Agda |✅ Proven-modulo-TCB +|`+verification/proofs/agda/SnifIsolation.agda+` + +|SEC-1-F1 |*Deniability wired into the operational run*: trap residue = +redacted secret (`+fault-via-observe+`), two equal-redaction faults +host-indistinguishable (`+run-deniable+`) |SEC |Agda |✅ Done (SNIFs 2) +|`+SnifIsolation.agda+` + +|SEC-1-F2 |*Outcome taxonomy*: `+TrapOrigin+` (guestFault / hostBudget / +preExec) + `+call+` front-end covering all 6 `+error_reason+` origins +|TP/SEC |Agda |✅ Done (SNIFs 2) |`+SnifIsolation.agda+` + +|SEC-1-TCB |Discharge *`+wasmtime ⊨ FaithfulRuntime+`* in-prover (WASM +trap-soundness; trap→`+{:error,_}+`; scheduler resumed) |SEC |Coq +(WasmCert-Coq) |⏳ Open (the "`Safer ≠ Safe`" residue) +|`+verification/proofs/coq/+` (slot) + +|DOM-1 |Verdict bridge: crash-isolation dichotomy + non-forgery + +restricted deniability (echo×epistemic, tropical-free) |DOM |Agda |✅ +Gated |`+verification/proofs/agda/SnifVerdict.agda+` + +|ABI-6 |Buffer/array marshalling round-trip + in-bounds (the +`+(ptr,len)+` _semantics_, unblocks FFT-class guests) |ABI |Idris2 |⏳ +Framework only |`+Compliance.WasmArray*+` + +|ABI-7 |Coverage: model + gate every real guest export |ABI |Idris2 + +Python |◐ buffer_abi done (15/20 Zig sites); burble_fft + Rust guests +ledgered |`+verification/proofs/idris2/ABI/BufferAbi.idr+`, +`+verification/tools/abi_conformance.py+` + +|GAP-1b |Behaviour faithfulness: metamorphic relations prove kernels +_behave_ as modelled, not just match signatures |TP |metamorphic tests +|◐ scalar kernels done (fibonacci, checked_add); buffer kernels next +|`+demo/test/snif_metamorphic_test.exs+` + +|CI-1 |`+abi-conformance+` runs in CI (not just local `+just+`) |ABI |CI +|✅ Done (job added); _required-check_ = owner branch-protection +|`+.github/workflows/proofs.yml+` +|=== + +*Ledgered out of current scope (named, not silently dropped):* - +`+zig/src/burble_fft.zig+` +(`+fft+`/`+ifft+`/`+crash_oob_fft+`/`+test_constant+`): not built into +any artifact dir, and its slice params are `+(ptr,len)+` marshalling = +*ABI-6* territory. Model once ABI-6 lands and the guest is built. - Rust +guests: `+rust/crates/demo-guest+` (canonical, loaded by the demo) and +the standalone `+rust-guest/+` experiment share the buffer ABI; their +conformance is pending the buffer-ABI multi-language gate (and the +`+rust/+` vs `+rust-guest/+` relationship is documented, not merged — +see PROOF-STATUS). + +=== Dangerous Patterns (BANNED — scanned by `+just proof-scan-dangerous+`, part of the gate) + +[width="100%",cols="33%,35%,32%",options="header",] +|=== +|Pattern |Language |Meaning +|`+believe_me+` |Idris2 |Unsafe cast / trust-me + +|`+assert_total+` |Idris2 |Skip totality check + +|`+postulate+` |Idris2/Agda |Unproven axiom (SEC-1’s TCB is a _record +hypothesis_, NOT a postulate — by design) + +|`+sorry+` |Lean4 |Incomplete proof + +|`+Admitted+` |Coq |Incomplete proof + +|`+unsafeCoerce+` |Haskell |Unsafe type cast + +|`+Obj.magic+` |OCaml/ReScript |Unsafe type cast + +|`+unsafe+` (unaudited) |Rust |Unsafe block without safety comment +|=== + +=== Prover Selection Guide + +[width="99%",cols="45%,34%,21%",options="header",] +|=== +|Use Case |Prover |Why +|ABI/FFI boundaries |*Idris2* |Dependent types model layouts + +signatures precisely + +|Public API type safety |*Lean4* |Algebraic/type metatheory + +|Operational isolation, (co)induction, the verdict bridge |*Agda* +(`+--safe --without-K+`) |Self-contained small-step model; native +induction + +|WASM operational semantics (the TCB discharge) |*Coq* (WasmCert-Coq) +|Existing mechanised WASM semantics +|=== + +=== Proof File Locations + +.... +verification/proofs/ +├── idris2/ABI/ # ABI-1..5 + ABI-7 (Foreign.idr safe_nif, BufferAbi.idr buffer guest) +├── idris2/Types.idr # TP-1 +├── lean4/ # TP-2 (ApiTypes.lean) +├── agda/ # SEC-1 (SnifIsolation.agda) + DOM-1 (SnifVerdict.agda) [GATED] +│ # Properties.agda is unrendered rsr-template SCAFFOLD (NOT gated) +├── coq/ # SEC-1-TCB slot (WasmCert-Coq); current file is SCAFFOLD +└── tlaplus/ # unused scaffold +verification/tools/abi_conformance.py # the gap-1 interface drift gate +demo/test/snif_metamorphic_test.exs # GAP-1b behaviour gate +.... + +=== References + +* Live proof status (authoritative): +link:PROOF-STATUS.md[`+PROOF-STATUS.md+`] +* Honesty boundary (what "`Safer`" may claim): `+AUDIT.adoc+`, README +`+Honesty+` section +* Proven library (Idris2 verified foundations): `+proven+` repo +* Template origin: `+rsr-template-repo/PROOF-NEEDS.md+` diff --git a/PROOF-NEEDS.md b/PROOF-NEEDS.md deleted file mode 100644 index accd2c5..0000000 --- a/PROOF-NEEDS.md +++ /dev/null @@ -1,107 +0,0 @@ - -# Proof Requirements — SNIFs (Safer NIFs) - -> **Standing requirements catalogue.** This file lists the proof obligations this repo -> *commits to carrying*. For the **live status** of each (proven / tested / trusted, with -> the adversarial-audit caveats), see [`PROOF-STATUS.md`](PROOF-STATUS.md) — that is the -> authoritative tracker; this file is the more stable "what must exist and why". - -## Proof Tier - - -**Tier**: **T2 — High.** SNIF's entire value proposition is a *safety* claim (a guest fault -becomes `{:error,_}` and the BEAM survives), so the operational isolation theorem (SEC-1) and -the ABI boundary are load-bearing. It is not T1 only because the residual runtime-faithfulness -assumption (`wasmtime ⊨ FaithfulRuntime`) is explicitly *trusted*, not yet machine-verified — -which is exactly why the product is "Safer", not "Safe". - -## Proof Categories - -| Code | Meaning | Applies? | -|------|---------|----------| -| **TP** | Typing Proofs (type soundness, type safety) | **Yes** — result-type algebra, verdict model | -| **INV** | Invariant Proofs (state machines, monotonicity, bounds) | Partial — fuel/liveness bound in SEC-1 | -| **SEC** | Security Proofs (crypto, injection freedom, access control) | **Yes** — SEC-1 crash isolation + deniability | -| **CONC** | Concurrency Proofs (linearizability, deadlock freedom) | No (pool isolation is tested, not proven) | -| **ALG** | Algorithm Proofs (termination, correctness, bounds) | Partial — run termination via fuel | -| **ABI** | ABI/FFI Proofs (memory layout, pointer safety, platform compat) | **Yes** — the guest export boundary | -| **DOM** | Domain-Specific Proofs (bespoke to this project) | **Yes** — echo×epistemic verdict bridge | - -## Mandatory Proofs (All RSR Repos) - -ABI/FFI boundary (Idris2) and core typing — all present and CI-gated by `just proof-check-all`: - -| # | Proof | Status | File | -|---|-------|--------|------| -| ABI-1 | Non-null pointer proofs (`So (ptr /= 0)`) | ✅ Gated | `verification/proofs/idris2/ABI/Pointers.idr` | -| ABI-2 | Memory layout correctness (`HasSize`, `HasAlignment`) | ✅ Gated | `verification/proofs/idris2/ABI/Layout.idr` | -| ABI-3 | Platform type size proofs | ✅ Gated | `verification/proofs/idris2/ABI/Platform.idr` | -| ABI-4 | FFI function return-type proofs (safe_nif, 8 exports) | ✅ Gated | `verification/proofs/idris2/ABI/Foreign.idr` | -| ABI-5 | C ABI compliance (`CABICompliant`, `FieldsAligned`) | ✅ Gated | `verification/proofs/idris2/ABI/Compliance.idr` | -| TP-1 | Core data-type well-formedness | ✅ Gated | `verification/proofs/idris2/Types.idr` | -| TP-2 | Public API type safety (exported functions) | ✅ Gated | `verification/proofs/lean4/ApiTypes.lean` | - -## Project-Specific Proofs - -| # | Proof Needed | Category | Prover | Status | File(s) | -|---|-------------|----------|--------|--------|---------| -| SEC-1 | Operational crash-isolation: guest fault ⇒ `{:error,_}` ∧ host survives, over a fuelled host↔guest run, *modulo* the explicit `FaithfulRuntime` TCB | SEC | Agda | ✅ Proven-modulo-TCB | `verification/proofs/agda/SnifIsolation.agda` | -| SEC-1-F1 | **Deniability wired into the operational run**: trap residue = redacted secret (`fault-via-observe`), two equal-redaction faults host-indistinguishable (`run-deniable`) | SEC | Agda | ✅ Done (SNIFs 2) | `SnifIsolation.agda` | -| SEC-1-F2 | **Outcome taxonomy**: `TrapOrigin` (guestFault / hostBudget / preExec) + `call` front-end covering all 6 `error_reason` origins | TP/SEC | Agda | ✅ Done (SNIFs 2) | `SnifIsolation.agda` | -| SEC-1-TCB | Discharge **`wasmtime ⊨ FaithfulRuntime`** in-prover (WASM trap-soundness; trap→`{:error,_}`; scheduler resumed) | SEC | Coq (WasmCert-Coq) | ⏳ Open (the "Safer ≠ Safe" residue) | `verification/proofs/coq/` (slot) | -| DOM-1 | Verdict bridge: crash-isolation dichotomy + non-forgery + restricted deniability (echo×epistemic, tropical-free) | DOM | Agda | ✅ Gated | `verification/proofs/agda/SnifVerdict.agda` | -| ABI-6 | Buffer/array marshalling round-trip + in-bounds (the `(ptr,len)` *semantics*, unblocks FFT-class guests) | ABI | Idris2 | ⏳ Framework only | `Compliance.WasmArray*` | -| ABI-7 | Coverage: model + gate every real guest export | ABI | Idris2 + Python | ◐ buffer_abi done (15/20 Zig sites); burble_fft + Rust guests ledgered | `verification/proofs/idris2/ABI/BufferAbi.idr`, `verification/tools/abi_conformance.py` | -| GAP-1b | Behaviour faithfulness: metamorphic relations prove kernels *behave* as modelled, not just match signatures | TP | metamorphic tests | ◐ scalar kernels done (fibonacci, checked_add); buffer kernels next | `demo/test/snif_metamorphic_test.exs` | -| CI-1 | `abi-conformance` runs in CI (not just local `just`) | ABI | CI | ✅ Done (job added); *required-check* = owner branch-protection | `.github/workflows/proofs.yml` | - -**Ledgered out of current scope (named, not silently dropped):** -- `zig/src/burble_fft.zig` (`fft`/`ifft`/`crash_oob_fft`/`test_constant`): not built into any artifact dir, and its slice params are `(ptr,len)` marshalling = **ABI-6** territory. Model once ABI-6 lands and the guest is built. -- Rust guests: `rust/crates/demo-guest` (canonical, loaded by the demo) and the standalone `rust-guest/` experiment share the buffer ABI; their conformance is pending the buffer-ABI multi-language gate (and the `rust/` vs `rust-guest/` relationship is documented, not merged — see PROOF-STATUS). - -## Dangerous Patterns (BANNED — scanned by `just proof-scan-dangerous`, part of the gate) - -| Pattern | Language | Meaning | -|---------|----------|---------| -| `believe_me` | Idris2 | Unsafe cast / trust-me | -| `assert_total` | Idris2 | Skip totality check | -| `postulate` | Idris2/Agda | Unproven axiom (SEC-1's TCB is a *record hypothesis*, NOT a postulate — by design) | -| `sorry` | Lean4 | Incomplete proof | -| `Admitted` | Coq | Incomplete proof | -| `unsafeCoerce` | Haskell | Unsafe type cast | -| `Obj.magic` | OCaml/ReScript | Unsafe type cast | -| `unsafe` (unaudited) | Rust | Unsafe block without safety comment | - -## Prover Selection Guide - -| Use Case | Prover | Why | -|----------|--------|-----| -| ABI/FFI boundaries | **Idris2** | Dependent types model layouts + signatures precisely | -| Public API type safety | **Lean4** | Algebraic/type metatheory | -| Operational isolation, (co)induction, the verdict bridge | **Agda** (`--safe --without-K`) | Self-contained small-step model; native induction | -| WASM operational semantics (the TCB discharge) | **Coq** (WasmCert-Coq) | Existing mechanised WASM semantics | - -## Proof File Locations - -``` -verification/proofs/ -├── idris2/ABI/ # ABI-1..5 + ABI-7 (Foreign.idr safe_nif, BufferAbi.idr buffer guest) -├── idris2/Types.idr # TP-1 -├── lean4/ # TP-2 (ApiTypes.lean) -├── agda/ # SEC-1 (SnifIsolation.agda) + DOM-1 (SnifVerdict.agda) [GATED] -│ # Properties.agda is unrendered rsr-template SCAFFOLD (NOT gated) -├── coq/ # SEC-1-TCB slot (WasmCert-Coq); current file is SCAFFOLD -└── tlaplus/ # unused scaffold -verification/tools/abi_conformance.py # the gap-1 interface drift gate -demo/test/snif_metamorphic_test.exs # GAP-1b behaviour gate -``` - -## References - -- Live proof status (authoritative): [`PROOF-STATUS.md`](PROOF-STATUS.md) -- Honesty boundary (what "Safer" may claim): `AUDIT.adoc`, README `Honesty` section -- Proven library (Idris2 verified foundations): `proven` repo -- Template origin: `rsr-template-repo/PROOF-NEEDS.md` diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc new file mode 100644 index 0000000..322dbb9 --- /dev/null +++ b/PROOF-STATUS.adoc @@ -0,0 +1,393 @@ +== Proof Status — SNIF + +=== Summary + +[cols=",,,,,",options="header",] +|=== +|Category |Total |Done |In Progress |Blocked |Remaining +|ABI/FFI (ABI) |6 |6 |0 |0 |0 +|Typing (TP) |2 |2 |0 |0 |0 +|Security / bridge (SEC, DOM) |2 |2 |0 |0 |0 +|*Total* |*10* |*10* |*0* |*0* |*0* +|=== + +*Overall*: 10/10 gated proof artifacts machine-check via +`+just proof-check-all+` — 7 Idris2 (ABI-1..5 + ABI-7 buffer guest + +TP-1 core types), 1 Lean4 (TP-2), 2 Agda (DOM-1 `+SnifVerdict+` bridge + +SEC-1 `+SnifIsolation+`). *SEC-1 is proven-modulo-the-explicit +`+FaithfulRuntime+` TCB* (the Safer-not-Safe gap); the other nine are +unconditional. + +____ +*Scope honesty.* These 7 proofs verify the *interface model* — ABI +layout/pointer safety and the result-type algebra — _not_ the +operational crash-isolation theorem. The operational theorem *SEC-1* +("`a guest trap becomes `+{:error, _}+`, the BEAM survives, and the +error carries no guest value`") is now *PROVEN-MODULO-EXPLICIT-TCB* in +Agda (`+SnifIsolation.agda+`, `+agda --safe --without-K+`, gated) — see +the SEC-1 section below. It is proven over a small-step host↔guest model +_modulo_ an explicit, type-visible trust boundary (`+FaithfulRuntime+`); +the boundary’s faithfulness to wasmtime/wasmex (the WASM-opsem TCB) is +*assumed, not yet discharged in-prover*. This residual assumption is +exactly why the project is *Safer* NIFs, not Safe NIFs. +____ + +____ +*Scope ceiling (by design).* SNIF proofs cover the _safer-NIF_ +obligation *only*: the ABI/type model, crash-isolation (SEC-1), and the +boundary residue being deniable/non-forging (`+SnifVerdict+`). SNIF does +*not* extend past the NIF goal — it adapts and perfects the existing NIF +for safety. Obligations belonging to _graduated integration beyond a +NIF_ (the transmutable *cleave* surface, its well-founded "`staircase`" +teardown, transaction-gating, mode-indexed permissions) are *not SNIF’s* +and are tracked in the cleave proof-needs +(`+~/developer/dev-notes/2026-06-16-cleave-proof-needs.adoc+`), not +here. A SNIF _realizes one residue-clean cleave instance_ at the +BEAM↔native boundary; it is *not* the cleave. +____ + +=== Verification (ground-truthed 2026-06-16) + +All seven typecheck from a clean build cache under the pinned toolchain +(`+idris2 0.8.0+`, `+lean 4.13.0+`). Run the gate with: + +[source,bash] +---- +just proof-check-all # idris2 (--source-dir) + lean4 + dangerous-pattern scan; fails-on-skip +---- + +CI enforces this via `+.github/workflows/proofs.yml+` (Idris2 + Lean4 +via Nix). To make it *blocking*, add the check "`Formal proofs — Idris2 ++ Lean4`" to branch-protection required status checks (owner-only). + +____ +*History correction.* Entries dated 2026-04-16 below claimed "`100% +proven`", but `+ABI/Foreign+`, `+ABI/Platform+`, and `+ABI/Compliance+` +never actually compiled (Idris2 unbound-implicit auto-binding shadowing +the global specs; unary-`+Nat+` blow-up on the 65536-scale page-size +arithmetic), and no CI job ever ran a prover (the `+just proof-check-*+` +targets used a broken invocation and exited 0 when the tool was absent). +Repaired and genuinely verified on 2026-06-16. +____ + +=== Proofs Done + +[width="100%",cols="11%,17%,20%,15%,25%,12%",options="header",] +|=== +|ID |Proof |Prover |File |Verified |By +|ABI-1 |Non-null pointer proofs (WasmAddr, SafePtr, MemRegion) |Idris2 +|`+verification/proofs/idris2/ABI/Pointers.idr+` |2026-06-16 +|`+idris2 --check+` + +|ABI-2 |Memory layout correctness (WasmValType sizes, alignment) |Idris2 +|`+verification/proofs/idris2/ABI/Layout.idr+` |2026-06-16 +|`+idris2 --check+` + +|ABI-3 |Platform type size proofs (WASM32 Zig-WASM correspondence) +|Idris2 |`+verification/proofs/idris2/ABI/Platform.idr+` |2026-06-16 +|`+idris2 --check+` + +|ABI-4 |FFI function return type proofs (8 SNIF exports) |Idris2 +|`+verification/proofs/idris2/ABI/Foreign.idr+` |2026-06-16 +|`+idris2 --check+` + +|ABI-5 |C ABI compliance (scalar exports, array layout framework) +|Idris2 |`+verification/proofs/idris2/ABI/Compliance.idr+` |2026-06-16 +|`+idris2 --check+` + +|TP-1 |Core data type well-formedness (WasmTrapKind, SNIFCallResult, +CompilationMode) |Idris2 |`+verification/proofs/idris2/Types.idr+` +|2026-06-16 |`+idris2 --check+` + +|TP-2 |Public API type safety (SNIFResult functor/monad laws, BEAM +survival model) |Lean4 |`+verification/proofs/lean4/ApiTypes.lean+` +|2026-06-16 |`+lean+` +|=== + +==== Repairs applied 2026-06-16 (no theorem weakened; no `+believe_me+`/`+postulate+`/`+sorry+`) + +* *Foreign / Compliance* — global spec names (`+specFibonacci+`, …) in +proof signatures were being auto-bound as fresh implicits (Idris2 +unbound-implicits), making `+Refl+` unprovable; qualified them +(`+Foreign.specX+`) to force resolution to the globals. +* *Platform* — WASM memory-size facts re-modeled `+Nat → Integer+` +(faithful: WASM is 32-bit addressed) so `+65536²+` and `+mod 65536+` +evaluate in O(1) instead of hanging the typechecker. 5 signatures in the +linear-memory section changed (comment-tagged). +* *Compliance* — `+CABICompliant+` / `+WasmArrayValid+` gained an +explicit `+NonZero alignment+` witness (the originals used +`+SIsNonZero+`, which cannot solve `+NonZero (abstract divisor)+`); a +faithful strengthening, not a weakening. +* *Types / Lean* — supplied the missing `+LTE max max+` / +`+{max : Nat}+` witnesses. + +=== Safety/security bridge (Agda, gated 2026-06-16) + +`+verification/proofs/agda/SnifVerdict.agda+` +(`+agda --safe --without-K+`, gated via `+just proof-check-agda-snif+`, +included in `+proof-check-all+`) is a *real* proof (not scaffold): it +models the host verdict as `+ok ⊕ trap+` and proves, *tropical-free* — +`+dichotomy+` (crash isolation), `+no-reflect+` (non-forgery: no +extractor exists; epistemic non-factivity) and +`+deniable-upto-redaction+` / `+perfect-deniable+` (confidentiality: +echo deniability up to a `+redact : S→R+` channel). It bridges +echo-types (loss/deniability) × epistemic-types (factive/belief). *Scope +honesty:* this is the _verdict-type_ result; it does NOT replace SEC-1 +(the operational theorem that the boundary actually _produces_ such +verdicts). Model-level here — but as of *SNIFs 2* the +deniability/redaction machinery is also re-derived *operationally* over +the actual fuelled run in `+SnifIsolation.agda+` (`+fault-via-observe+`, +`+run-deniable+`); see the SEC-1 audit section (F1 resolved). + +=== SEC-1 — operational crash-isolation (Agda, PROVEN-MODULO-EXPLICIT-TCB, gated 2026-06-16) + +`+verification/proofs/agda/SnifIsolation.agda+` (module +`+SnifIsolation+`, +`+agda --safe --without-K --no-libraries -i verification/proofs/agda+`, +exit 0 from a clean cache) mechanically proves *SEC-1*, the operational +crash-isolation theorem, over a small-step host↔guest model. The theorem +is + +.... +Model.isolation : (rt : FaithfulRuntime) (n : Nat) (g : G) (h : H) + → Alive h → Isolated rt n g h +.... + +inside the parameterised `+module Model (G H A R : Set)+` (G = opaque +guest config / the secret: linear memory/pc/locals; H = host/BEAM state; +A = success value; R = public `+{:error,reason}+`). Callers +`+open Model G H A R+`; the witnesses use `+open Model ⊤ ⊤ ⊤ ⊤+` and +`+open Model Nat ⊤ ⊤ ⊤+`. So SEC-1’s externally-qualified name is +*`+Model.isolation+`*. `+FaithfulRuntime+` and `+Isolated+` live in +*Set₁* (because `+Alive : H → Set+` and `+noForgery+` quantifies over +`+Set+`) — benign under `+--safe --without-K+`. + +`+Isolated+` bundles exactly the three SEC-1 conjuncts about the fuelled +run `+run rt n g h+`: + +[width="100%",cols="27%,17%,56%",options="header",] +|=== +|Conjunct |Field |How it is established +|*crash isolation* (verdict ∈ ok ⊕ trap) |`+okOrTrap+` +|`+SnifVerdict.dichotomy+` applied to the `+Verdict A R+` that `+run+` +builds *by construction* (returned↦ok, trapped↦trap, fuel-0↦trap). Not a +`+FaithfulRuntime+` field. + +|*preservation* (host survives the call) |`+hostSafe+` |*DERIVED* by +`+survives+`, an induction on the `+Nat+` fuel: zero→`+timeout-host+`; +`+suc+` dispatches on `+step rt g h+` via with-inversion to continue→F3, +returned→F4, trapped→F5 (each equation-guarded). Not a field. + +|*non-forgery* (error carries no guest value) |`+noForgery+` +|`+SnifVerdict.no-reflect+` reused *verbatim* (no total +`+Verdict A R → A+` extractor). Independent of every runtime field. +|=== + +*The TCB is an explicit hypothesis, never a postulate.* +`+FaithfulRuntime : Set₁+` bundles only PRIMITIVE single-step facts: +`+step : G → H → Step+` (F1; the exhaustive continue/returned/trapped +trichotomy IS "`no stuck / no host-observable UB`"); the opaque +`+Alive : H → Set+` (F2; the predicate the conclusion is ABOUT, only +transported); and equation-guarded per-step preservation F3 +`+step-continue-host+` (host-transparent internal step), F4 +`+step-return-host+` (survives across `+onReturn+`), *F5 +`+step-trap-host+`* (the crash-isolation primitive: survives across +`+recover+`), F6 `+timeout-host+` (fuel/epoch exhaustion surfaced as a +trap, survives across `+onTimeout+`). *No field mentions a whole run, +"`the call survives`", or "`ok-or-trap`".* + +*Non-circularity — verified by mutation, not by reading.* Replacing the +trap-branch discharge `+trapOk r refl alive+` in `+survives+` with the +bare hypothesis `+alive+` makes the file FAIL with +`+h != FaithfulRuntime.recover rt h of type H+`: the run MUTATES the +host to `+recover h+` on a fault, so `+Alive (recover h)+` is +unobtainable from `+Alive h+` and can come only from F5. Deleting the +`+trapped+` clause of `+survives+` fails with a `+CoverageIssue+`, so +the trap branch is coverage-mandatory for *every* `+rt+`. F5 is +load-bearing. + +*Non-vacuity — the model admits faulting runs, witnessed by `+refl+`.* +`+UnitWitness.trapping-runtime+` (step = `+λ _ _ → trapped tt+`) gives +`+actually-traps : verdict (run … 1 …) ≡ trap tt+` by `+refl+`; +`+Countdown.skipRT+` reaches a trap only AFTER two `+continue+` +recursions (4→2→0→trap) with `+multistep-traps = refl+`, so the +*inductive* trap path is exercised (holing that `+refl+` breaks the +build with `+UnsolvedInteractionMetas+`); +`+multistep-isolated = isolation skipRT 3 4 tt tt+` instantiates SEC-1 +on a real faulting trace; `+timeout-traps+` shows fuel-0 surfaces as a +trap, not a stuck state. Dual `+returning-runtime+` / `+ok-case-live+` +make the dichotomy a genuine two-sided ⊕, not an always-ok degenerate. + +*What is ASSUMED (the WASM-opsem TCB, NOT discharged here).* The prose +claim *"`wasmtime ⊨ FaithfulRuntime`"* — that wasmtime + the wasmex +embedding actually realise these primitive facts (WASM trap-soundness, +signal-caught trap → `+{:error,reason}+`, host scheduler resumed +unchanged) — is the stated trust boundary. It sits in the theorem’s TYPE +as the `+(rt : FaithfulRuntime)+` binder (gate-legal: a record, not a +`+postulate+`), and is *explicitly out of scope* for in-Agda discharge. +Discharging it via WasmCert-Coq trap-soundness + a wasmtime +signal-handling model is the remaining obligation (see "`Not yet +proven`"). *SEC-1 is therefore proven-modulo-this-explicit-TCB, and the +TCB itself is not yet machine-verified — the honest Safer-not-Safe gap.* + +Banned-token scan clean (the only `+postulate+` string is a design-rule +comment); zero `+?+` holes; `+run+`/`+survives+` are structurally +recursive on the `+Nat+` fuel (native termination, no `+TERMINATING+` +pragma). Gated via `+just proof-check-agda-snif+` (included in +`+proof-check-all+`; orchestrator wires the Justfile target — not edited +here). + +=== SEC-1 — audit caveats (2026-06-16): F1/F2 RESOLVED in SNIFs 2; F3/F4/F5 standing precision notes + +An adversarial proof-skeptic pass (`+agda --safe --without-K+`, exit 0 — +the proofs are *sound*) originally found the prose over-claiming in five +ways (F1–F5). *F1 and F2 have since been fixed, and the fixes +mutation-confirmed load-bearing* by a 4-skeptic re-audit (2026-06-16); +*F3/F4/F5* remain as accurate _precision_ caveats (they bound what the +prose may claim, not soundness). + +* *F1 — RESOLVED (SNIFs 2): confidentiality is now wired into the +operational theorem.* `+SnifIsolation.agda+` imports +`+observe+`/`+faulted+` from `+SnifVerdict+`; its +`+Step.trapped : S → Step+` carries the guest *secret*; +`+FaithfulRuntime.redact : S → R+` is the sole secret→public channel; +and the run’s fault verdict is `+trap (guestFault (redact s))+`, shown +to factor through `+observe+` (`+fault-via-observe+`). Operational +deniability is re-derived over the actual run (`+run-deniable+`): two +faults whose secrets redact equally are host-indistinguishable. +*Mutation-confirmed non-vacuous:* making `+redact+` injective (lossless) +makes `+SecretWitness.secrets-indistinguishable+` fail to typecheck +(`+one ≠ two+`) — the lossy redaction is genuinely load-bearing. +* *F2 / MODEL-1 — RESOLVED (SNIFs 2): the verdict models the real +outcome taxonomy.* The host reason is now `+TrapOrigin+` = +`+guestFault+` (`+:trap+`) ⊕ `+hostBudget+` (`+:fuel_exhausted+` / +`+:timeout+`) ⊕ `+preExec+` (`+:load+` / `+:no_such_export+` / +`+:pool+`), and a `+call+` front-end models the three pre-execution +origins the old run-only model could not express — covering all six +`+SnifDemo.Snif+` `+error_reason+` origins; `+PreExecWitness+` exercises +the pre-exec path. *Mutation-confirmed:* deleting the `+preFail+` branch +of `+survives+` is rejected (`+[CoverageIssue]+`); retagging the trapped +clause `+guestFault+`→`+hostBudget+` is rejected. +* *F3 — `+dichotomy+`/`+noForgery+` are structural, not runtime +(standing, accurate).* `+okOrTrap+` and `+noForgery+` typecheck with +_no_ `+FaithfulRuntime+` in scope (re-confirmed: standalone lemmas +taking no `+rt+` argument accept); only `+hostSafe+`/`+survives+` +consumes the TCB. The load-bearing operational content of SEC-1 is *host +preservation*, not the ok|trap split (true for any 2-constructor type). +* *F4 — `+noForgery+` is parametric, not instance-level (standing, +accurate).* It proves no total `+∀{A R}. Verdict A R → A+` exists; the +instance-level discharge is rejected (`+A !=< ⊥+`). Sound, labelled +precisely. +* *F5 — `+Alive+` faithfulness remains TCB; vacuity now rebutted by a +witness (SNIFs 2).* `+PartialAlive+` exhibits a _non-trivial_ liveness +(`+Alive? dead = ⊥+`; mutation-confirmed — making it `+⊤+` breaks +`+dead-not-alive+`) whose `+recover+` maps a dying host to a live one. +This rebuts the _vacuity_ worry, but `+Alive+`’s faithfulness to +wasmtime/wasmex is still part of the TCB: `+survives+` _transports_ a +liveness, it does not _establish_ the real one. + +*Positive control (F6):* `+step-trap-host+` _is_ load-bearing (mutating +`+survives+`’ trap branch to bare `+alive+` is rejected: +`+h != recover rt h+`); `+perfect-deniable+`’s constant redaction _is_ +load-bearing. SEC-1 is *not vacuous* — +host-preservation-across-`+recover+` + the structural ok|trap split + +operational deniability + the origin taxonomy, all _modulo_ the +`+Alive+`/`+FaithfulRuntime+` TCB. A 2026-06-16 mutation re-audit (4 +independent skeptics, every targeted mutation rejected as expected) +confirmed all of the above; the only weakness found was stale prose, now +corrected here. + +=== Scaffold (NOT counted, NOT gated) + +`+verification/proofs/{agda,coq,tlaplus}/+` contain *unmodified +rsr-template stubs* (a toy list/Nat Agda lemma, a toy Nat/Bool Coq +soundness proof, a generic TLA+ pipeline) — they have nothing to do with +SNIF and are excluded from `+proof-check-all+`. Each now carries a +`+SCAFFOLD — NOT A SNIF PROOF+` banner. They are kept as homes for real +future obligations (e.g. the Coq slot → the WasmCert-Coq isolation +theorem). + +=== Not yet proven (the real gap / next obligations) + +[width="100%",cols="11%,32%,23%,18%,16%",options="header",] +|=== +|ID |Proof needed |Category |Prover |Notes +|SEC-1-TCB |Discharge *"`wasmtime ⊨ FaithfulRuntime`"* in-prover: prove +that wasmtime + the wasmex embedding actually realise the primitive +single-step facts (WASM trap-soundness; trap → `+{:error,_}+`; host +scheduler resumed unchanged) that `+SnifIsolation.agda+` assumes as its +TCB record |SEC |Coq (WasmCert-Coq) |SEC-1’s *operational* layer is now +PROVEN-MODULO-EXPLICIT-TCB in Agda (`+Model.isolation+`). This row is +the REMAINING half: machine-verifying the runtime-faithfulness +assumption that is currently in the theorem’s _type_ but not proven. + +|ABI-6 |Buffer/array marshalling round-trip + in-bounds (unblocks +"`powerful`" NIFs; FFT) |ABI |Idris2 |`+Compliance.WasmArray*+` is only +a framework today + +|ABI-7 |◐ *Coverage 15 of 20 — buffer_abi DONE 2026-06-16.* `+safe_nif+` +(8, `+Foreign.idr+`) + `+buffer_abi+` (7, `+BufferAbi.idr+`, incl. 3 +void returns) are modelled+gated, both in the `+abi_conformance.py+` +guest manifest. *Remaining (ledgered):* `+zig/src/burble_fft.zig+` (5 — +`+fft+`/`+ifft+`/… use `+(ptr,len)+` slice marshalling = ABI-6, and it +is not built into any artifact) + the Rust buffer guest |ABI |Idris2 + +Python |Buffer guest closed; FFT + Rust pending the multi-language +buffer-ABI gate + +|GAP-1b |◐ *Behaviour faithfulness — scalar kernels DONE 2026-06-16.* +`+demo/test/snif_metamorphic_test.exs+` (dep-free, 9 metamorphic tests, +green on OTP 25). *Load-bearing relations (do not delete):* the +`+fibonacci+` recurrence n=2..40 + base cases (uniquely determines fib), +and the `+checked_add+` oracle over a 100-case boundary-spanning family +(non-overflow = exact sum; overflow = `+{:error,_}+`) + the +boundary-trap test. Buffer kernels (`+sum_f32+` permutation/additivity) +are next |TP |metamorphic tests (extraction long-term) |The gate first +surfaced that `+checked_add+` was a *misnomer* (wrapping `+a +% b+`); +*resolved 2026-06-16 by making it genuinely checked* — overflow traps +(`+@addWithOverflow+` + `+unreachable+`, all modes) + +|CI-1 |✅ *DONE 2026-06-16*: `+abi-conformance+` now runs as a CI job in +`+.github/workflows/proofs.yml+` (builds both guests, fails on signature +drift) |ABI |CI wiring |Making it a _required_ status check is the +owner-only branch-protection step + +|MODEL-1 |◐ *Largely RESOLVED by F2 (SNIFs 2).* The 6 `+error_reason+` +origins are now modelled via `+TrapOrigin+` +(guestFault/hostBudget/preExec) + the `+call+` front-end in +`+SnifIsolation+`. *Residual:* the `+snif_alloc+`-returns-0 OOM "`third +outcome`" is not yet modelled as a distinct verdict |TP |Agda |Taxonomy +half done; only the OOM-sentinel nuance remains +|=== + +=== Changelog + +[width="100%",cols="32%,42%,26%",options="header",] +|=== +|Date |Change |By +|2026-04-04 |Initial proof status tracking |Template + +|2026-04-16 |(Claimed) all 7 proofs complete — see History correction; +not actually compiling |Claude Code + +|2026-06-16 |All 7 proofs *genuinely* machine-checked (clean-cache); +real gate wired; scaffold de-counted; scope honesty added |Claude Opus +4.8 + +|2026-06-16 |*SEC-1 (`+Model.isolation+`) PROVEN-MODULO-EXPLICIT-TCB* in +Agda (`+SnifIsolation.agda+`, `+--safe --without-K+`, clean-cache exit +0); TCB = `+FaithfulRuntime+` record hypothesis (primitive single-step +facts), non-circularity + non-vacuity confirmed by mutation; WASM-opsem +discharge ("`wasmtime ⊨ FaithfulRuntime`") remains as SEC-1-TCB |Claude +Opus 4.8 (1M context) + +|2026-06-16 |*SNIFs 2.* SEC-1 sharpened: F1 deniability wired +operationally (`+run-deniable+`/`+fault-via-observe+` + +`+SecretWitness+`), F2 6-origin `+TrapOrigin+` taxonomy + `+call+` +front-end (`+PreExecWitness+`), F5 non-trivial-`+Alive+` recovery +witness (`+PartialAlive+`) — all mutation-confirmed load-bearing by a +4-skeptic re-audit. ABI-7: `+buffer_abi+` modelled+gated +(`+BufferAbi.idr+`, 15/20 sites); guest-aware `+abi_conformance.py+`; +CI-1 conformance job added; GAP-1b scalar metamorphic gate (found the +`+checked_add+` misnomer, then made it genuinely checked — overflow +traps). |Claude Opus 4.8 (1M context) +|=== diff --git a/PROOF-STATUS.md b/PROOF-STATUS.md deleted file mode 100644 index 979cc7a..0000000 --- a/PROOF-STATUS.md +++ /dev/null @@ -1,238 +0,0 @@ - -# Proof Status — SNIF - - - -## Summary - -| Category | Total | Done | In Progress | Blocked | Remaining | -|----------|-------|------|-------------|---------|-----------| -| ABI/FFI (ABI) | 6 | 6 | 0 | 0 | 0 | -| Typing (TP) | 2 | 2 | 0 | 0 | 0 | -| Security / bridge (SEC, DOM) | 2 | 2 | 0 | 0 | 0 | -| **Total** | **10** | **10** | **0** | **0** | **0** | - -**Overall**: 10/10 gated proof artifacts machine-check via `just proof-check-all` — 7 Idris2 -(ABI-1..5 + ABI-7 buffer guest + TP-1 core types), 1 Lean4 (TP-2), 2 Agda (DOM-1 `SnifVerdict` -bridge + SEC-1 `SnifIsolation`). **SEC-1 is proven-modulo-the-explicit `FaithfulRuntime` TCB** -(the Safer-not-Safe gap); the other nine are unconditional. - -> **Scope honesty.** These 7 proofs verify the **interface model** — ABI layout/pointer -> safety and the result-type algebra — *not* the operational crash-isolation theorem. -> The operational theorem **SEC-1** ("a guest trap becomes `{:error, _}`, the BEAM -> survives, and the error carries no guest value") is now **PROVEN-MODULO-EXPLICIT-TCB** -> in Agda (`SnifIsolation.agda`, `agda --safe --without-K`, gated) — see the SEC-1 -> section below. It is proven over a small-step host↔guest model *modulo* an explicit, -> type-visible trust boundary (`FaithfulRuntime`); the boundary's faithfulness to -> wasmtime/wasmex (the WASM-opsem TCB) is **assumed, not yet discharged in-prover**. -> This residual assumption is exactly why the project is **Safer** NIFs, not Safe NIFs. - -> **Scope ceiling (by design).** SNIF proofs cover the *safer-NIF* obligation **only**: the -> ABI/type model, crash-isolation (SEC-1), and the boundary residue being deniable/non-forging -> (`SnifVerdict`). SNIF does **not** extend past the NIF goal — it adapts and perfects the -> existing NIF for safety. Obligations belonging to *graduated integration beyond a NIF* (the -> transmutable **cleave** surface, its well-founded "staircase" teardown, transaction-gating, -> mode-indexed permissions) are **not SNIF's** and are tracked in the cleave proof-needs -> (`~/developer/dev-notes/2026-06-16-cleave-proof-needs.adoc`), not here. A SNIF *realizes one -> residue-clean cleave instance* at the BEAM↔native boundary; it is **not** the cleave. - -## Verification (ground-truthed 2026-06-16) - -All seven typecheck from a clean build cache under the pinned toolchain -(`idris2 0.8.0`, `lean 4.13.0`). Run the gate with: - -```bash -just proof-check-all # idris2 (--source-dir) + lean4 + dangerous-pattern scan; fails-on-skip -``` - -CI enforces this via `.github/workflows/proofs.yml` (Idris2 + Lean4 via Nix). To make it -**blocking**, add the check "Formal proofs — Idris2 + Lean4" to branch-protection required -status checks (owner-only). - -> **History correction.** Entries dated 2026-04-16 below claimed "100% proven", but -> `ABI/Foreign`, `ABI/Platform`, and `ABI/Compliance` never actually compiled (Idris2 -> unbound-implicit auto-binding shadowing the global specs; unary-`Nat` blow-up on the -> 65536-scale page-size arithmetic), and no CI job ever ran a prover (the `just -> proof-check-*` targets used a broken invocation and exited 0 when the tool was absent). -> Repaired and genuinely verified on 2026-06-16. - -## Proofs Done - -| ID | Proof | Prover | File | Verified | By | -|----|-------|--------|------|----------|-----| -| ABI-1 | Non-null pointer proofs (WasmAddr, SafePtr, MemRegion) | Idris2 | `verification/proofs/idris2/ABI/Pointers.idr` | 2026-06-16 | `idris2 --check` | -| ABI-2 | Memory layout correctness (WasmValType sizes, alignment) | Idris2 | `verification/proofs/idris2/ABI/Layout.idr` | 2026-06-16 | `idris2 --check` | -| ABI-3 | Platform type size proofs (WASM32 Zig-WASM correspondence) | Idris2 | `verification/proofs/idris2/ABI/Platform.idr` | 2026-06-16 | `idris2 --check` | -| ABI-4 | FFI function return type proofs (8 SNIF exports) | Idris2 | `verification/proofs/idris2/ABI/Foreign.idr` | 2026-06-16 | `idris2 --check` | -| ABI-5 | C ABI compliance (scalar exports, array layout framework) | Idris2 | `verification/proofs/idris2/ABI/Compliance.idr` | 2026-06-16 | `idris2 --check` | -| TP-1 | Core data type well-formedness (WasmTrapKind, SNIFCallResult, CompilationMode) | Idris2 | `verification/proofs/idris2/Types.idr` | 2026-06-16 | `idris2 --check` | -| TP-2 | Public API type safety (SNIFResult functor/monad laws, BEAM survival model) | Lean4 | `verification/proofs/lean4/ApiTypes.lean` | 2026-06-16 | `lean` | - -### Repairs applied 2026-06-16 (no theorem weakened; no `believe_me`/`postulate`/`sorry`) -- **Foreign / Compliance** — global spec names (`specFibonacci`, …) in proof signatures - were being auto-bound as fresh implicits (Idris2 unbound-implicits), making `Refl` - unprovable; qualified them (`Foreign.specX`) to force resolution to the globals. -- **Platform** — WASM memory-size facts re-modeled `Nat → Integer` (faithful: WASM is - 32-bit addressed) so `65536²` and `mod 65536` evaluate in O(1) instead of hanging the - typechecker. 5 signatures in the linear-memory section changed (comment-tagged). -- **Compliance** — `CABICompliant` / `WasmArrayValid` gained an explicit - `NonZero alignment` witness (the originals used `SIsNonZero`, which cannot solve - `NonZero (abstract divisor)`); a faithful strengthening, not a weakening. -- **Types / Lean** — supplied the missing `LTE max max` / `{max : Nat}` witnesses. - -## Safety/security bridge (Agda, gated 2026-06-16) - -`verification/proofs/agda/SnifVerdict.agda` (`agda --safe --without-K`, gated via -`just proof-check-agda-snif`, included in `proof-check-all`) is a **real** proof (not -scaffold): it models the host verdict as `ok ⊕ trap` and proves, **tropical-free** — -`dichotomy` (crash isolation), `no-reflect` (non-forgery: no extractor exists; epistemic -non-factivity) and `deniable-upto-redaction` / `perfect-deniable` (confidentiality: echo -deniability up to a `redact : S→R` channel). It bridges echo-types (loss/deniability) × -epistemic-types (factive/belief). **Scope honesty:** this is the *verdict-type* result; it -does NOT replace SEC-1 (the operational theorem that the boundary actually *produces* such -verdicts). Model-level here — but as of **SNIFs 2** the deniability/redaction machinery is also -re-derived **operationally** over the actual fuelled run in `SnifIsolation.agda` -(`fault-via-observe`, `run-deniable`); see the SEC-1 audit section (F1 resolved). - -## SEC-1 — operational crash-isolation (Agda, PROVEN-MODULO-EXPLICIT-TCB, gated 2026-06-16) - -`verification/proofs/agda/SnifIsolation.agda` (module `SnifIsolation`, -`agda --safe --without-K --no-libraries -i verification/proofs/agda`, exit 0 from a clean -cache) mechanically proves **SEC-1**, the operational crash-isolation theorem, over a -small-step host↔guest model. The theorem is - -``` -Model.isolation : (rt : FaithfulRuntime) (n : Nat) (g : G) (h : H) - → Alive h → Isolated rt n g h -``` - -inside the parameterised `module Model (G H A R : Set)` (G = opaque guest config / the -secret: linear memory/pc/locals; H = host/BEAM state; A = success value; R = public -`{:error,reason}`). Callers `open Model G H A R`; the witnesses use `open Model ⊤ ⊤ ⊤ ⊤` -and `open Model Nat ⊤ ⊤ ⊤`. So SEC-1's externally-qualified name is **`Model.isolation`**. -`FaithfulRuntime` and `Isolated` live in **Set₁** (because `Alive : H → Set` and -`noForgery` quantifies over `Set`) — benign under `--safe --without-K`. - -`Isolated` bundles exactly the three SEC-1 conjuncts about the fuelled run `run rt n g h`: - -| Conjunct | Field | How it is established | -|----------|-------|----------------------| -| **crash isolation** (verdict ∈ ok ⊕ trap) | `okOrTrap` | `SnifVerdict.dichotomy` applied to the `Verdict A R` that `run` builds **by construction** (returned↦ok, trapped↦trap, fuel-0↦trap). Not a `FaithfulRuntime` field. | -| **preservation** (host survives the call) | `hostSafe` | **DERIVED** by `survives`, an induction on the `Nat` fuel: zero→`timeout-host`; `suc` dispatches on `step rt g h` via with-inversion to continue→F3, returned→F4, trapped→F5 (each equation-guarded). Not a field. | -| **non-forgery** (error carries no guest value) | `noForgery` | `SnifVerdict.no-reflect` reused **verbatim** (no total `Verdict A R → A` extractor). Independent of every runtime field. | - -**The TCB is an explicit hypothesis, never a postulate.** `FaithfulRuntime : Set₁` bundles -only PRIMITIVE single-step facts: `step : G → H → Step` (F1; the exhaustive -continue/returned/trapped trichotomy IS "no stuck / no host-observable UB"); the opaque -`Alive : H → Set` (F2; the predicate the conclusion is ABOUT, only transported); and -equation-guarded per-step preservation F3 `step-continue-host` (host-transparent internal -step), F4 `step-return-host` (survives across `onReturn`), **F5 `step-trap-host`** (the -crash-isolation primitive: survives across `recover`), F6 `timeout-host` (fuel/epoch -exhaustion surfaced as a trap, survives across `onTimeout`). **No field mentions a whole -run, "the call survives", or "ok-or-trap".** - -**Non-circularity — verified by mutation, not by reading.** Replacing the trap-branch -discharge `trapOk r refl alive` in `survives` with the bare hypothesis `alive` makes the -file FAIL with `h != FaithfulRuntime.recover rt h of type H`: the run MUTATES the host to -`recover h` on a fault, so `Alive (recover h)` is unobtainable from `Alive h` and can come -only from F5. Deleting the `trapped` clause of `survives` fails with a `CoverageIssue`, so -the trap branch is coverage-mandatory for **every** `rt`. F5 is load-bearing. - -**Non-vacuity — the model admits faulting runs, witnessed by `refl`.** -`UnitWitness.trapping-runtime` (step = `λ _ _ → trapped tt`) gives -`actually-traps : verdict (run … 1 …) ≡ trap tt` by `refl`; `Countdown.skipRT` reaches a -trap only AFTER two `continue` recursions (4→2→0→trap) with `multistep-traps = refl`, so -the **inductive** trap path is exercised (holing that `refl` breaks the build with -`UnsolvedInteractionMetas`); `multistep-isolated = isolation skipRT 3 4 tt tt` instantiates -SEC-1 on a real faulting trace; `timeout-traps` shows fuel-0 surfaces as a trap, not a -stuck state. Dual `returning-runtime` / `ok-case-live` make the dichotomy a genuine -two-sided ⊕, not an always-ok degenerate. - -**What is ASSUMED (the WASM-opsem TCB, NOT discharged here).** The prose claim -**"wasmtime ⊨ FaithfulRuntime"** — that wasmtime + the wasmex embedding actually realise -these primitive facts (WASM trap-soundness, signal-caught trap → `{:error,reason}`, host -scheduler resumed unchanged) — is the stated trust boundary. It sits in the theorem's -TYPE as the `(rt : FaithfulRuntime)` binder (gate-legal: a record, not a `postulate`), and -is **explicitly out of scope** for in-Agda discharge. Discharging it via WasmCert-Coq -trap-soundness + a wasmtime signal-handling model is the remaining obligation (see "Not -yet proven"). **SEC-1 is therefore proven-modulo-this-explicit-TCB, and the TCB itself is -not yet machine-verified — the honest Safer-not-Safe gap.** - -Banned-token scan clean (the only `postulate` string is a design-rule comment); zero `?` -holes; `run`/`survives` are structurally recursive on the `Nat` fuel (native termination, -no `TERMINATING` pragma). Gated via `just proof-check-agda-snif` (included in -`proof-check-all`; orchestrator wires the Justfile target — not edited here). - -## SEC-1 — audit caveats (2026-06-16): F1/F2 RESOLVED in SNIFs 2; F3/F4/F5 standing precision notes - -An adversarial proof-skeptic pass (`agda --safe --without-K`, exit 0 — the proofs are **sound**) -originally found the prose over-claiming in five ways (F1–F5). **F1 and F2 have since been fixed, -and the fixes mutation-confirmed load-bearing** by a 4-skeptic re-audit (2026-06-16); **F3/F4/F5** -remain as accurate *precision* caveats (they bound what the prose may claim, not soundness). - -- **F1 — RESOLVED (SNIFs 2): confidentiality is now wired into the operational theorem.** - `SnifIsolation.agda` imports `observe`/`faulted` from `SnifVerdict`; its `Step.trapped : S → Step` - carries the guest **secret**; `FaithfulRuntime.redact : S → R` is the sole secret→public channel; and - the run's fault verdict is `trap (guestFault (redact s))`, shown to factor through `observe` - (`fault-via-observe`). Operational deniability is re-derived over the actual run (`run-deniable`): - two faults whose secrets redact equally are host-indistinguishable. **Mutation-confirmed non-vacuous:** - making `redact` injective (lossless) makes `SecretWitness.secrets-indistinguishable` fail to typecheck - (`one ≠ two`) — the lossy redaction is genuinely load-bearing. -- **F2 / MODEL-1 — RESOLVED (SNIFs 2): the verdict models the real outcome taxonomy.** The host reason - is now `TrapOrigin` = `guestFault` (`:trap`) ⊕ `hostBudget` (`:fuel_exhausted` / `:timeout`) ⊕ - `preExec` (`:load` / `:no_such_export` / `:pool`), and a `call` front-end models the three - pre-execution origins the old run-only model could not express — covering all six `SnifDemo.Snif` - `error_reason` origins; `PreExecWitness` exercises the pre-exec path. **Mutation-confirmed:** deleting - the `preFail` branch of `survives` is rejected (`[CoverageIssue]`); retagging the trapped clause - `guestFault`→`hostBudget` is rejected. -- **F3 — `dichotomy`/`noForgery` are structural, not runtime (standing, accurate).** `okOrTrap` and - `noForgery` typecheck with *no* `FaithfulRuntime` in scope (re-confirmed: standalone lemmas taking no - `rt` argument accept); only `hostSafe`/`survives` consumes the TCB. The load-bearing operational - content of SEC-1 is **host preservation**, not the ok|trap split (true for any 2-constructor type). -- **F4 — `noForgery` is parametric, not instance-level (standing, accurate).** It proves no total - `∀{A R}. Verdict A R → A` exists; the instance-level discharge is rejected (`A !=< ⊥`). Sound, - labelled precisely. -- **F5 — `Alive` faithfulness remains TCB; vacuity now rebutted by a witness (SNIFs 2).** `PartialAlive` - exhibits a *non-trivial* liveness (`Alive? dead = ⊥`; mutation-confirmed — making it `⊤` breaks - `dead-not-alive`) whose `recover` maps a dying host to a live one. This rebuts the *vacuity* worry, but - `Alive`'s faithfulness to wasmtime/wasmex is still part of the TCB: `survives` *transports* a liveness, - it does not *establish* the real one. - -**Positive control (F6):** `step-trap-host` *is* load-bearing (mutating `survives`' trap branch to bare -`alive` is rejected: `h != recover rt h`); `perfect-deniable`'s constant redaction *is* load-bearing. -SEC-1 is **not vacuous** — host-preservation-across-`recover` + the structural ok|trap split + -operational deniability + the origin taxonomy, all *modulo* the `Alive`/`FaithfulRuntime` TCB. A -2026-06-16 mutation re-audit (4 independent skeptics, every targeted mutation rejected as expected) -confirmed all of the above; the only weakness found was stale prose, now corrected here. - -## Scaffold (NOT counted, NOT gated) - -`verification/proofs/{agda,coq,tlaplus}/` contain **unmodified rsr-template stubs** (a -toy list/Nat Agda lemma, a toy Nat/Bool Coq soundness proof, a generic TLA+ pipeline) — -they have nothing to do with SNIF and are excluded from `proof-check-all`. Each now -carries a `SCAFFOLD — NOT A SNIF PROOF` banner. They are kept as homes for real future -obligations (e.g. the Coq slot → the WasmCert-Coq isolation theorem). - -## Not yet proven (the real gap / next obligations) - -| ID | Proof needed | Category | Prover | Notes | -|----|--------------|----------|--------|-------| -| SEC-1-TCB | Discharge **"wasmtime ⊨ FaithfulRuntime"** in-prover: prove that wasmtime + the wasmex embedding actually realise the primitive single-step facts (WASM trap-soundness; trap → `{:error,_}`; host scheduler resumed unchanged) that `SnifIsolation.agda` assumes as its TCB record | SEC | Coq (WasmCert-Coq) | SEC-1's **operational** layer is now PROVEN-MODULO-EXPLICIT-TCB in Agda (`Model.isolation`). This row is the REMAINING half: machine-verifying the runtime-faithfulness assumption that is currently in the theorem's *type* but not proven. | -| ABI-6 | Buffer/array marshalling round-trip + in-bounds (unblocks "powerful" NIFs; FFT) | ABI | Idris2 | `Compliance.WasmArray*` is only a framework today | -| ABI-7 | ◐ **Coverage 15 of 20 — buffer_abi DONE 2026-06-16.** `safe_nif` (8, `Foreign.idr`) + `buffer_abi` (7, `BufferAbi.idr`, incl. 3 void returns) are modelled+gated, both in the `abi_conformance.py` guest manifest. **Remaining (ledgered):** `zig/src/burble_fft.zig` (5 — `fft`/`ifft`/… use `(ptr,len)` slice marshalling = ABI-6, and it is not built into any artifact) + the Rust buffer guest | ABI | Idris2 + Python | Buffer guest closed; FFT + Rust pending the multi-language buffer-ABI gate | -| GAP-1b | ◐ **Behaviour faithfulness — scalar kernels DONE 2026-06-16.** `demo/test/snif_metamorphic_test.exs` (dep-free, 9 metamorphic tests, green on OTP 25). **Load-bearing relations (do not delete):** the `fibonacci` recurrence n=2..40 + base cases (uniquely determines fib), and the `checked_add` oracle over a 100-case boundary-spanning family (non-overflow = exact sum; overflow = `{:error,_}`) + the boundary-trap test. Buffer kernels (`sum_f32` permutation/additivity) are next | TP | metamorphic tests (extraction long-term) | The gate first surfaced that `checked_add` was a **misnomer** (wrapping `a +% b`); **resolved 2026-06-16 by making it genuinely checked** — overflow traps (`@addWithOverflow` + `unreachable`, all modes) | -| CI-1 | ✅ **DONE 2026-06-16**: `abi-conformance` now runs as a CI job in `.github/workflows/proofs.yml` (builds both guests, fails on signature drift) | ABI | CI wiring | Making it a *required* status check is the owner-only branch-protection step | -| MODEL-1 | ◐ **Largely RESOLVED by F2 (SNIFs 2).** The 6 `error_reason` origins are now modelled via `TrapOrigin` (guestFault/hostBudget/preExec) + the `call` front-end in `SnifIsolation`. **Residual:** the `snif_alloc`-returns-0 OOM "third outcome" is not yet modelled as a distinct verdict | TP | Agda | Taxonomy half done; only the OOM-sentinel nuance remains | - -## Changelog - -| Date | Change | By | -|------|--------|-----| -| 2026-04-04 | Initial proof status tracking | Template | -| 2026-04-16 | (Claimed) all 7 proofs complete — see History correction; not actually compiling | Claude Code | -| 2026-06-16 | All 7 proofs **genuinely** machine-checked (clean-cache); real gate wired; scaffold de-counted; scope honesty added | Claude Opus 4.8 | -| 2026-06-16 | **SEC-1 (`Model.isolation`) PROVEN-MODULO-EXPLICIT-TCB** in Agda (`SnifIsolation.agda`, `--safe --without-K`, clean-cache exit 0); TCB = `FaithfulRuntime` record hypothesis (primitive single-step facts), non-circularity + non-vacuity confirmed by mutation; WASM-opsem discharge ("wasmtime ⊨ FaithfulRuntime") remains as SEC-1-TCB | Claude Opus 4.8 (1M context) | -| 2026-06-16 | **SNIFs 2.** SEC-1 sharpened: F1 deniability wired operationally (`run-deniable`/`fault-via-observe` + `SecretWitness`), F2 6-origin `TrapOrigin` taxonomy + `call` front-end (`PreExecWitness`), F5 non-trivial-`Alive` recovery witness (`PartialAlive`) — all mutation-confirmed load-bearing by a 4-skeptic re-audit. ABI-7: `buffer_abi` modelled+gated (`BufferAbi.idr`, 15/20 sites); guest-aware `abi_conformance.py`; CI-1 conformance job added; GAP-1b scalar metamorphic gate (found the `checked_add` misnomer, then made it genuinely checked — overflow traps). | Claude Opus 4.8 (1M context) | diff --git a/SECURITY.adoc b/SECURITY.adoc new file mode 100644 index 0000000..e47fdd9 --- /dev/null +++ b/SECURITY.adoc @@ -0,0 +1,16 @@ +== Security Policy + +=== Reporting a Vulnerability + +If you discover a security vulnerability, please report it responsibly. + +*Email:* j.d.a.jewell@open.ac.uk + +*Please include:* - Description of the vulnerability - Steps to +reproduce - Potential impact + +*Response timeline:* - Acknowledgement within 48 hours - Initial +assessment within 7 days - Fix or mitigation within 90 days + +*Safe harbour:* We will not pursue legal action against security +researchers who follow responsible disclosure. diff --git a/SECURITY.md b/SECURITY.md deleted file mode 100644 index c7c239f..0000000 --- a/SECURITY.md +++ /dev/null @@ -1,23 +0,0 @@ - -# Security Policy - -## Reporting a Vulnerability - -If you discover a security vulnerability, please report it responsibly. - -**Email:** j.d.a.jewell@open.ac.uk - -**Please include:** -- Description of the vulnerability -- Steps to reproduce -- Potential impact - -**Response timeline:** -- Acknowledgement within 48 hours -- Initial assessment within 7 days -- Fix or mitigation within 90 days - -**Safe harbour:** We will not pursue legal action against security researchers who follow responsible disclosure. diff --git a/TEST-NEEDS.adoc b/TEST-NEEDS.adoc new file mode 100644 index 0000000..405db65 --- /dev/null +++ b/TEST-NEEDS.adoc @@ -0,0 +1,138 @@ +== TEST-NEEDS: snifs + +=== CRG Grade: C — ACHIEVED 2026-04-04 + +=== Current State (Updated 2026-04-04) + +[width="100%",cols="40%,26%,34%",options="header",] +|=== +|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 \{\{project}} 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 + +* [line-through]#*Template repo used by ALL new repos has 0 validation +tests*# → FIXED: 4 test suites + validation script +* [line-through]#*fuzz/placeholder.txt*# → FIXED: replaced with +README.adoc containing real harness instructions +* [line-through]#*No E2E tests for template instantiation*# → FIXED: +full E2E test suite +* [line-through]#*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) ✅ diff --git a/TEST-NEEDS.md b/TEST-NEEDS.md deleted file mode 100644 index 017ddc4..0000000 --- a/TEST-NEEDS.md +++ /dev/null @@ -1,111 +0,0 @@ - -# TEST-NEEDS: snifs - -## 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 {{project}} 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) ✅ diff --git a/TOPOLOGY.adoc b/TOPOLOGY.adoc new file mode 100644 index 0000000..a975f58 --- /dev/null +++ b/TOPOLOGY.adoc @@ -0,0 +1,36 @@ +== Architecture Topology + +=== System Overview + +RSR (Rhodium Standard Repository) template provides the canonical +scaffold for all hyperpolymath projects, with integrated CI/CD, +documentation, and service discovery patterns. + +=== Component Overview + +[width="100%",cols="37%,33%,30%",options="header",] +|=== +|Component |Language |Purpose +|dogfood-gate workflow |YAML |Quality checks (CRG, security, linting) +|eclexiaiser-validate job |YAML |Resource cost awareness scoring +|Groove discovery |JSON |Service endpoint registration +|=== + +=== Data Flow + +.... +[Code Push] → [GitHub Actions] → [hypatia scan] → [eclexiaiser validate] → [Results] +.... + +=== Integration Points + +* *Upstream*: Hypatia (neurosymbolic CI/CD), eclexiaiser (resource +scoring) +* *Downstream*: All RSR-based repositories (500+ instances) + +=== Deployment + +* Container: Stapeln Six ecosystem +* CI/CD: GitHub Actions → Hypatia scan → eclexiaiser-validate (6 +scorecard dimensions) → Mirror +* Service Discovery: Groove protocol (.well-known/groove/manifest.json) diff --git a/TOPOLOGY.md b/TOPOLOGY.md deleted file mode 100644 index 4ad8569..0000000 --- a/TOPOLOGY.md +++ /dev/null @@ -1,36 +0,0 @@ - - - -# Architecture Topology - -## System Overview - -RSR (Rhodium Standard Repository) template provides the canonical scaffold for all hyperpolymath projects, with integrated CI/CD, documentation, and service discovery patterns. - -## Component Overview - -| Component | Language | Purpose | -|-----------|----------|---------| -| dogfood-gate workflow | YAML | Quality checks (CRG, security, linting) | -| eclexiaiser-validate job | YAML | Resource cost awareness scoring | -| Groove discovery | JSON | Service endpoint registration | - -## Data Flow - -``` -[Code Push] → [GitHub Actions] → [hypatia scan] → [eclexiaiser validate] → [Results] -``` - -## Integration Points - -- **Upstream**: Hypatia (neurosymbolic CI/CD), eclexiaiser (resource scoring) -- **Downstream**: All RSR-based repositories (500+ instances) - -## Deployment - -- Container: Stapeln Six ecosystem -- CI/CD: GitHub Actions → Hypatia scan → eclexiaiser-validate (6 scorecard dimensions) → Mirror -- Service Discovery: Groove protocol (.well-known/groove/manifest.json) diff --git a/demo/deps/jason/CHANGELOG.md b/demo/deps/jason/CHANGELOG.md deleted file mode 100644 index c37dd2a..0000000 --- a/demo/deps/jason/CHANGELOG.md +++ /dev/null @@ -1,132 +0,0 @@ -# Changelog - -## 1.4.4 (26.07.2024) - -* Fix warnings on Elixir 1.17 by conditionally compiling Decimal support - -## 1.4.3 (29.06.2024) - -* Fix derive with _ struct key - -## 1.4.2 (29.06.2024) - -* Fix compiler warnings for Elixir 1.17 - -## 1.4.1 (06.07.2023) - -* Add limit to decoded integer sizes of 1024 digits. This can be changed - with the `decoding_integer_digit_limit` app env config. - -## 1.4.0 (12.09.2022) - -### Enhancements - -* Use the `:erlang.float_to_binary(_, [:short])` function, instead of `io_lib_format.fwrite_g/1` - where available (OTP 24.1+). This provides equivalent output with much less memory used - and significantly improved performance. - -## 1.3.0 (21.12.2021) - -### Enhancements - -* Add the `Jason.OrderedObject` struct -* Support decoding objects preserving all the keys with `objects: :ordered_objects` option -* Support decoding floats to `Decimal` with `floats: :decimals` option -* Add `~j` and `~J` sigils in module `Jason.Sigil` to support writing JSON literals in code - -### Fixes -* Fix error reporting when decoding strings (it was possible to mis-attribute the offending byte) -* Verify fields given to `@derive` - -## 1.2.2 (08.09.2020) - -### Enhancements - -* Support Decimal 2.0 - -## 1.2.1 (04.05.2020) - -### Security - -* Fix `html_safe` escaping in `Jason.encode` - - The ` -# LLM Warmup — snifs (Developer) - -## What is snifs? -See README.adoc for overview. - -## Key Commands -- `just setup` — set up development environment -- `just build` — build the project -- `just test` — run tests -- `just doctor` — diagnose issues -- `just heal` — attempt auto-repair - -## Quick Context -- License: MPL-2.0 -- Part of hyperpolymath ecosystem -- See EXPLAINME.adoc for architecture diff --git a/llm-warmup-user.adoc b/llm-warmup-user.adoc new file mode 100644 index 0000000..0a9fe7f --- /dev/null +++ b/llm-warmup-user.adoc @@ -0,0 +1,19 @@ +== LLM Warmup — snifs (User) + +=== What is snifs? + +See README.adoc for overview. + +=== Key Commands + +* `+just setup+` — set up development environment +* `+just build+` — build the project +* `+just test+` — run tests +* `+just doctor+` — diagnose issues +* `+just heal+` — attempt auto-repair + +=== Quick Context + +* License: MPL-2.0 +* Part of hyperpolymath ecosystem +* See EXPLAINME.adoc for architecture diff --git a/llm-warmup-user.md b/llm-warmup-user.md deleted file mode 100644 index 60a7d7e..0000000 --- a/llm-warmup-user.md +++ /dev/null @@ -1,20 +0,0 @@ - -# LLM Warmup — snifs (User) - -## What is snifs? -See README.adoc for overview. - -## Key Commands -- `just setup` — set up development environment -- `just build` — build the project -- `just test` — run tests -- `just doctor` — diagnose issues -- `just heal` — attempt auto-repair - -## Quick Context -- License: MPL-2.0 -- Part of hyperpolymath ecosystem -- See EXPLAINME.adoc for architecture diff --git a/verification/README.adoc.invariants.adoc b/verification/README.adoc.invariants.adoc new file mode 100644 index 0000000..bd74777 --- /dev/null +++ b/verification/README.adoc.invariants.adoc @@ -0,0 +1,15 @@ +== Invariant Path Scan: README.adoc + +=== Invariant: ip-ae105f4e3bfdc1d9 + +⚠️ *ISSUE DETECTED / 🔍 REVIEW REQUIRED* + +*Source Text:* This project + +*Target Text:* that compiling native code (Zig) to WebAssembly + +*Invariant Type:* provenance + +*Notes:* auto-generated heuristic suggestion; editable + +''''' diff --git a/verification/README.adoc.invariants.md b/verification/README.adoc.invariants.md deleted file mode 100644 index b3d0de4..0000000 --- a/verification/README.adoc.invariants.md +++ /dev/null @@ -1,19 +0,0 @@ - -# Invariant Path Scan: README.adoc - -## Invariant: ip-ae105f4e3bfdc1d9 - -⚠️ **ISSUE DETECTED / 🔍 REVIEW REQUIRED** - -**Source Text:** This project - -**Target Text:** that compiling native code (Zig) to WebAssembly - -**Invariant Type:** provenance - -**Notes:** auto-generated heuristic suggestion; editable - ----