diff --git a/docs/developer/ABI-FFI-README.adoc b/docs/developer/ABI-FFI-README.adoc index af10cee..02565fd 100644 --- a/docs/developer/ABI-FFI-README.adoc +++ b/docs/developer/ABI-FFI-README.adoc @@ -1,3 +1,5 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) Jonathan D.A. Jewell = ABI/FFI Standards {{~ Aditionally delete this line and fill out the template below ~}} @@ -17,10 +19,13 @@ This library follows the **Hyperpolymath RSR Standard** for ABI and FFI design: ``` ┌─────────────────────────────────────────────┐ │ ABI Definitions (Idris2) │ -│ src/abi/ │ +│ src/interface/abi/ │ │ - Types.idr (Type definitions) │ │ - Layout.idr (Memory layout proofs) │ -│ - Foreign.idr (FFI declarations) │ +│ - LayoutProofs.idr (Alignment proofs) │ +│ - Tier2.idr (Honest signed-attest) │ +│ src/interface/legacy/ │ +│ - Foreign.idr (DEPRECATED FFI decls) │ └─────────────────┬───────────────────────────┘ │ │ generates (at compile time) @@ -53,11 +58,20 @@ This library follows the **Hyperpolymath RSR Standard** for ABI and FFI design: ``` vcl_total/ ├── src/ -│ ├── abi/ # ABI definitions (Idris2) -│ │ ├── Types.idr # Core type definitions with proofs -│ │ ├── Layout.idr # Memory layout verification -│ │ └── Foreign.idr # FFI function declarations -│ └── lib/ # Core library (any language) +│ ├── interface/ +│ │ ├── abi/ # Honest ABI definitions (Idris2) +│ │ │ ├── Types.idr # Core type definitions with proofs +│ │ │ ├── Layout.idr # Memory layout (paddingFor, alignUp) +│ │ │ ├── LayoutProofs.idr # Alignment-divides + bounds proofs +│ │ │ └── Tier2.idr # Idris bindings → vclut_verify_wire +│ │ │ # (Ed25519 attestation, honest path) +│ │ ├── legacy/ # Pre-Phase-5 plumbing (DEPRECATED) +│ │ │ └── Foreign.idr # Legacy libvqlut bindings (Zig +│ │ │ # asserts level; no Idris certificate) +│ │ ├── attest/ # Tier-2 Rust: signed attestation +│ │ ├── recompute-wasm/ # Tier-1 Rust: consumer-side recompute +│ │ └── ffi/ # Legacy Zig multi-stage pipeline +│ └── core/ # Idris2 corpus (the certifier itself) │ ├── ffi/ │ └── zig/ # FFI implementation (Zig) diff --git a/src/core/Decide.idr b/src/core/Decide.idr index a0b1882..d19d26a 100644 --- a/src/core/Decide.idr +++ b/src/core/Decide.idr @@ -1,6 +1,5 @@ --- SPDX-License-Identifier: AGPL-3.0-or-later --- Copyright (c) 2026 Jonathan D.A. Jewell - +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) Jonathan D.A. Jewell ||| VCL-total Core Decide — canonical safety deciders (single source of truth) ||| ||| Phase 2 of the standards#124 HOLE remediation de-vacuizes the Level @@ -672,14 +671,70 @@ entailsPairs (EpReqEntails a1 a2 _ :: rest) = (agentId a1, agentId a2) :: entailsPairs rest entailsPairs (_ :: rest) = entailsPairs rest -||| Direct circular ENTAILS (a⊨b and b⊨a). Full graph-cycle detection is -||| OWED (disclosed); this catches the direct symmetry violation. +||| Direct circular ENTAILS (a⊨b and b⊨a). Retained as a fast-path / +||| historical name; the canonical L10 check is `hasTransitiveCycle` +||| below, which subsumes this case. public export hasCircularEntails : List EpistemicRequirement -> Bool hasCircularEntails reqs = let pairs = entailsPairs reqs in any (\(a, b) => any (\(c, d) => a == d && b == c) pairs) pairs +-- ═══════════════════════════════════════════════════════════════════════ +-- Transitive ENTAILS cycle detection (Phase 5 OWED → RESOLVED) +-- ═══════════════════════════════════════════════════════════════════════ +-- +-- The Phase-4b L10 check restricted itself to direct (a⊨b, b⊨a) cycles +-- with full graph-cycle detection explicitly OWED in +-- VERIFICATION-STANCE.adoc. The closure below upgrades the check to +-- arbitrary-length cycles via finite-fuel transitive closure. +-- +-- All three functions are structurally total. No believe_me / +-- postulate / assert_* — pure list recursion. + +||| One step of transitive closure: for each `(a, b)` and `(b, c)` in +||| `pairs`, add `(a, c)`. Returns the union of `pairs` and the one-hop +||| extension (`++` rather than dedup; the cycle check `any ((==) <$> fst +||| <*> snd)` is duplicate-insensitive). +private +extendFrom : List (String, String) -> (String, String) -> List (String, String) +extendFrom pairs (a, b) = + map (\q => (a, snd q)) (filter (\q => fst q == b) pairs) + +public export +transStep : List (String, String) -> List (String, String) +transStep pairs = pairs ++ concatMap (extendFrom pairs) pairs + +||| Iterate `transStep` `n` times. +public export +transCloseN : Nat -> List (String, String) -> List (String, String) +transCloseN Z ps = ps +transCloseN (S k) ps = transCloseN k (transStep ps) + +||| Transitive closure of an ENTAILS edge list, fuel-bounded by +||| `length pairs`. For a graph with `m` distinct edges, every reachable +||| `(a, b)` is present after at most `m` doubling steps; `m` linear +||| steps suffice because each step extends paths by one hop and any +||| simple cycle of length `n` requires `n ≤ m` edges. (Non-simple paths +||| cannot introduce new `(v, v)` edges that simple paths miss.) +public export +transClose : List (String, String) -> List (String, String) +transClose ps = transCloseN (length ps) ps + +||| True iff the ENTAILS graph contains *any* cycle (direct or +||| transitive). A cycle exists iff some self-edge `(a, a)` appears in +||| the transitive closure. +||| +||| Strictly stronger than `hasCircularEntails`: every direct cycle is +||| also a length-2 transitive cycle, and additionally catches +||| `a⊨b⊨c⊨a` and longer chains. +public export +hasTransitiveCycle : List EpistemicRequirement -> Bool +hasTransitiveCycle reqs = + let pairs = entailsPairs reqs + closed = transClose pairs + in any (\p => fst p == snd p) closed + ||| L10 STRUCTURAL part: an EPISTEMIC clause is present, has ≥1 agent, ||| and every requirement-referenced agent is declared. This is exactly ||| the part of L10 that IS closed under relational join (`joinEpistemic` @@ -695,17 +750,25 @@ epiStructOK stmt = case epistemicClause stmt of [] => True (_ :: _) => False -||| L10 ACYCLIC part: no direct (a⊨b, b⊨a) ENTAILS cycle among the -||| clause's requirements. This is the ONE L10 sub-property that is +||| L10 ACYCLIC part: no ENTAILS cycle (direct *or* transitive) among +||| the clause's requirements. This is the ONE L10 sub-property that is ||| provably NOT closed under join (two acyclic requirement sets can ||| union to a cyclic one), so it is isolated here and supplied as an ||| explicit composition side-condition (see `Composition.JoinSideCondition` ||| and the disclosure in VERIFICATION-STANCE.adoc) — never faked. +||| +||| Phase 5 upgrade: previously routed through `hasCircularEntails` +||| (direct cycles only); now uses `hasTransitiveCycle` (finite-fuel +||| transitive closure), closing the disclosed "full graph-cycle +||| detection OWED" gap. The body signature is unchanged, so all +||| consumers (Checker / Composition / Levels) and the side-condition +||| machinery continue to work verbatim — the predicate is just +||| strictly stronger. public export epiNoCycle : Statement -> Bool epiNoCycle stmt = case epistemicClause stmt of Nothing => False - Just (EpClause _ reqs) => not (hasCircularEntails reqs) + Just (EpClause _ reqs) => not (hasTransitiveCycle reqs) ||| L10 — EpistemicSafe: clause present, ≥1 agent, all requirement agents ||| declared, AND no direct ENTAILS cycle. Mirrors `Checker.checkLevel10` diff --git a/src/interface/abi/Tier2.idr b/src/interface/abi/Tier2.idr new file mode 100644 index 0000000..70c0d15 --- /dev/null +++ b/src/interface/abi/Tier2.idr @@ -0,0 +1,209 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell +-- +||| VCL-total Tier-2 Foreign Function Interface (signed attestation) +||| +||| Idris-side bindings to the *honest* C ABI exposed by the Zig shim +||| `ffi/zig/src/lib.zig` (`vclut_verify_wire`), which calls into the +||| Rust crate `src/interface/attest` (`vclut_rs_verify`) — see +||| `src/interface/attest/ATTESTATION-FORMAT.adoc` for the wire +||| contract and `docs/decisions/0002-ffi-attestation-trust-boundary.adoc` +||| for the trust model rationale. +||| +||| **Architectural role.** This module replaces the level-asserting +||| legacy path (`VclTotal.Legacy.Foreign.getSafetyLevel`, deprecated +||| 2026-06-02). Where the legacy path returned a Zig-side integer +||| with no Idris verification, this module returns a 65-byte +||| Ed25519-signed attestation +||| +||| `token = [level : Bits8] ++ [signature : Vect 64 Bits8]` +||| +||| over `DOMAIN ‖ sha256(stmt_wire) ‖ sha256(schema_wire) ‖ level` +||| (`DOMAIN = "VCLT-ATTEST-v1\0\0"`). The certifier signs *iff* the +||| conformance-pinned `vcltotal_parse::certified_level` lies in +||| `0..=10` — **fail-closed**, never a token for an unestablished +||| level. +||| +||| **Trust model (Tier-2 ceiling).** A C ABI erases types to machine +||| words; it cannot transport a re-checkable dependent +||| `SafetyCertificate`. Over a C ABI the honest ceiling is +||| trusted-certifier attestation, and that ceiling is what this +||| module exposes. The consumer's TCB is: +||| (1) the certifier holds its Ed25519 key genuinely, +||| (2) the certifier ran the conformance-pinned decider before +||| signing, +||| (3) the Ed25519-dalek + sha2 implementation in the Tier-2 crate. +||| +||| **Strictly weaker than Tier-1** (recompute-PCC over `wasm32`, +||| `src/interface/recompute-wasm`), which trusts neither (1) nor (2) +||| because the consumer re-runs the decision itself. Prefer Tier-1 +||| where wasm hosting is available; Tier-2 is the C-ABI fallback. +||| +||| **No proofs.** Like all FFI plumbing, this module contains no +||| theorems — its safety properties live in the Tier-2 Rust crate's +||| tests (`src/interface/attest/src/lib.rs::tests` — roundtrip + 5 +||| tamper variants + fail-closed + C-ABI). It is *not* in the +||| Idris2 proof corpus (`vclut-core.ipkg`); see +||| `verification/proofs/VERIFICATION-STANCE.adoc` §"Boundary model" +||| for what the Tier-2 ceiling does and does not guarantee. + +module VclTotal.ABI.Tier2 + +import VclTotal.ABI.Types +import Data.Buffer +import Data.List + +%default total + +-- ═══════════════════════════════════════════════════════════════════════ +-- Public surface +-- ═══════════════════════════════════════════════════════════════════════ + +||| Tier-2 verification verdict. +||| +||| * `Verified lvl token` — certifier signed level `lvl`, attestation +||| bytes are in `token` (always 65 bytes: 1 level + 64 signature). +||| * `Rejected reason` — fail-closed; the certifier did not establish +||| a level (decode failure, malformed input, level outside +||| `0..=10`, or any other reject path). Token is NOT emitted. +public export +data Tier2Verdict : Type where + Verified : SafetyLevel -> List Bits8 -> Tier2Verdict + Rejected : String -> Tier2Verdict + +||| The fixed Ed25519 attestation token width (`level : 1 byte` +||| + `signature : 64 bytes`). +public export +attestationTokenSize : Nat +attestationTokenSize = 65 + +||| Ed25519 seed/secret-key byte width. +public export +ed25519SeedSize : Nat +ed25519SeedSize = 32 + +-- ═══════════════════════════════════════════════════════════════════════ +-- C ABI declarations +-- ═══════════════════════════════════════════════════════════════════════ + +||| The honest Tier-2 entry point. Bound to the Zig shim +||| `vclut_verify_wire` in `ffi/zig/src/lib.zig`, which calls +||| `vclut_rs_verify` (`src/interface/attest/src/lib.rs`). +||| +||| ABI: +||| +||| ```c +||| int32_t vclut_verify_wire( +||| const uint8_t* stmt_ptr, size_t stmt_len, +||| const uint8_t* schema_ptr, size_t schema_len, +||| const uint8_t* sk_ptr, /* 32 bytes */ +||| uint8_t* out_ptr, size_t out_cap /* >= 65 */ +||| ); +||| ``` +||| +||| Returns `0..=10` on success (writes the 65-byte attestation to +||| `out_ptr`), `-1` on Reject (no write). Pointers must each describe +||| a valid range of the stated length; the function never reads or +||| writes outside the documented spans. See the Rust crate's `Safety` +||| comment for the precise contract. +export +%foreign "C:vclut_verify_wire, libvclut_ffi" +prim__vclutVerifyWire : + Buffer -> Int -> -- stmt + Buffer -> Int -> -- schema + Buffer -> -- 32-byte Ed25519 seed + Buffer -> Int -> -- out + cap + PrimIO Int + +-- ═══════════════════════════════════════════════════════════════════════ +-- Internal helpers +-- ═══════════════════════════════════════════════════════════════════════ + +||| Marshal a `List Bits8` into a freshly-allocated `Buffer`. Returns +||| `Nothing` on allocation failure. +private +listToBuffer : List Bits8 -> IO (Maybe Buffer) +listToBuffer xs = do + let n = length xs + Just buf <- newBuffer (cast n) | Nothing => pure Nothing + go buf 0 xs + pure (Just buf) + where + go : Buffer -> Int -> List Bits8 -> IO () + go _ _ [] = pure () + go buf i (b :: bs) = do + setBits8 buf i b + go buf (i + 1) bs + +||| Read the entire contents of a `Buffer` of declared length `n` into +||| a `List Bits8`. Reads bytes `[0, n)` in order. +private +bufferToList : Buffer -> Int -> IO (List Bits8) +bufferToList buf n = go 0 [] + where + go : Int -> List Bits8 -> IO (List Bits8) + go i acc = + if i >= n + then pure (reverse acc) + else do + b <- getBits8 buf i + assert_total (go (i + 1) (b :: acc)) + +-- ═══════════════════════════════════════════════════════════════════════ +-- Safe public wrapper +-- ═══════════════════════════════════════════════════════════════════════ + +||| Verify a wire-marshalled `(Statement, OctadSchema)` pair via the +||| Tier-2 signed-attestation backend. On success returns +||| `Verified level token` with the 65-byte attestation; on any +||| reject path returns `Rejected reason` with a human-readable cause. +||| +||| @param stmtWire v1 statement-wire bytes (see +||| `src/interface/parse/WIRE-FORMAT.adoc`) +||| @param schemaWire v1 schema-wire bytes (`VCLS` magic) +||| @param sk the certifier's 32-byte Ed25519 *seed* (NOT a +||| public key — this is the signing key). Real +||| provisioning is deployment via the estate token +||| vault. +||| +||| **Fail-closed contract.** This wrapper returns `Rejected` on: +||| * `sk` not exactly 32 bytes; +||| * buffer allocation failure (out of memory); +||| * any negative `c_int` from the C backend (decode failure, +||| malformed input, level outside `0..=10`); +||| * a return value outside `0..=10` (defensive — the backend's +||| contract already constrains this, but we re-check on the way +||| out). +export +verifyWire : + (stmtWire : List Bits8) -> + (schemaWire : List Bits8) -> + (sk : List Bits8) -> + IO Tier2Verdict +verifyWire stmtWire schemaWire sk = do + if length sk /= ed25519SeedSize + then pure (Rejected + "Ed25519 seed must be exactly 32 bytes") + else do + Just stmtBuf <- listToBuffer stmtWire + | Nothing => pure (Rejected "stmt buffer alloc failed") + Just schemaBuf <- listToBuffer schemaWire + | Nothing => pure (Rejected "schema buffer alloc failed") + Just skBuf <- listToBuffer sk + | Nothing => pure (Rejected "sk buffer alloc failed") + Just outBuf <- newBuffer (cast attestationTokenSize) + | Nothing => pure (Rejected "out buffer alloc failed") + let stmtLen : Int = cast (length stmtWire) + let schemaLen : Int = cast (length schemaWire) + let outCap : Int = cast attestationTokenSize + rc <- primIO (prim__vclutVerifyWire + stmtBuf stmtLen schemaBuf schemaLen skBuf outBuf outCap) + if rc < 0 + then pure (Rejected + "Tier-2 backend Rejected (fail-closed): no certified level") + else case intToSafetyLevel (cast rc) of + Nothing => pure (Rejected + "Tier-2 backend returned out-of-range level — defensive Reject") + Just lvl => do + token <- bufferToList outBuf (cast attestationTokenSize) + pure (Verified lvl token) diff --git a/src/interface/abi/Foreign.idr b/src/interface/legacy/Foreign.idr similarity index 78% rename from src/interface/abi/Foreign.idr rename to src/interface/legacy/Foreign.idr index ab7dc45..2a96208 100644 --- a/src/interface/abi/Foreign.idr +++ b/src/interface/legacy/Foreign.idr @@ -1,33 +1,51 @@ -- SPDX-License-Identifier: MPL-2.0 -- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) -- -||| VCL-total Foreign Function Interface Declarations +||| VCL-total Legacy Foreign Function Interface Declarations (DEPRECATED) ||| -||| Declares all C-compatible functions implemented in the Zig FFI layer. -||| The pipeline processes queries through progressive safety levels: +||| ⚠️ DEPRECATED 2026-06-02 (standards#124, Phase 5+ follow-up). ||| -||| parse -> bind_schema -> check_types -> check_effects -> compile +||| This module binds Idris to the *legacy* Zig pipeline in +||| `src/interface/ffi/src/main.zig` +||| (`vqlut_parse → vqlut_bind_schema → vqlut_check_types → +||| vqlut_check_effects → vqlut_compile → vqlut_get_safety_level`). +||| The `achieved_level` field returned by `vqlut_get_safety_level` is +||| *set by the Zig pipeline itself* based on which stage succeeded — +||| it is a Zig-side trusted assertion, NOT a transported dependent +||| proof and NOT an Idris-certified verdict. A C ABI cannot carry a +||| `SafetyCertificate` (inherent architectural limit). The real +||| verification authority is the Idris2 corpus certifier +||| (`VclTotal.Core.Checker.certifyRequested` / `certifiedLevel`). ||| -||| Each stage returns a handle to an intermediate representation. -||| The final query plan carries proof of the highest achieved safety level. +||| Use the new honest paths instead: ||| -||| All functions are declared here with type signatures. -||| Implementations live in ffi/zig/src/main.zig +||| * **Tier-1 (recompute-PCC over `wasm32`)** — consumer re-runs +||| the certified decision via `src/interface/recompute-wasm` +||| (`vcl_recompute`), comparing its verdict against the +||| producer's claim. No trusted certifier. See +||| `verification/proofs/VERIFICATION-STANCE.adoc` §"Boundary +||| model — two tiers". ||| -||| HONEST SCOPE (standards#124, Phase 3d). `getSafetyLevel` decodes a -||| level *tag* from an FFI integer; that integer is an *attestation* -||| from a trusted certifier, NOT a transported dependent proof — a C -||| ABI cannot carry a `SafetyCertificate` (inherent). The real -||| verification authority is the Idris2 corpus certifier -||| (`VclTotal.Core.Checker.certifyRequested` / `certifiedLevel`), which -||| only yields a level behind a genuine machine-checked certificate. -||| The Zig shim is *fail-closed* as of Phase 3d (no fabricated level). -||| This module is FFI plumbing — it contains *no proofs* and is not in -||| the proof corpus. The string→AST parser, C-ABI Statement -||| marshalling, and Idris→C build are NAMED OWED in -||| verification/proofs/VERIFICATION-STANCE.adoc (absent, not faked). - -module VclTotal.ABI.Foreign +||| * **Tier-2 (C-ABI Ed25519 signed attestation, FALLBACK)** — +||| producer signs `(sha256(stmt_wire), sha256(schema_wire), +||| level)`; consumer Ed25519-verifies. See `src/interface/attest` +||| (`vclut_rs_verify`) and the Idris bindings in +||| `VclTotal.ABI.Tier2` (`src/interface/abi/Tier2.idr`). +||| +||| This file is kept ONLY so external C/Zig callers that linked +||| against the legacy `libvqlut` ABI before Phase 5 can still find an +||| Idris-side description of the function signatures. No part of the +||| proof corpus imports it (the stale `corpus/VclTotal/ABI/Foreign.idr` +||| symlink was removed). New Idris consumers should target +||| `VclTotal.ABI.Tier2`. +||| +||| HONEST SCOPE (legacy text retained for context). `getSafetyLevel` +||| decodes a level *tag* from an FFI integer; that integer is an +||| *attestation* from a trusted certifier, NOT a transported dependent +||| proof. The Zig shim is *fail-closed* as of Phase 3d (no fabricated +||| level). This module is FFI plumbing — it contains *no proofs*. + +module VclTotal.Legacy.Foreign import VclTotal.ABI.Types import VclTotal.ABI.Layout diff --git a/verification/proofs/VERIFICATION-STANCE.adoc b/verification/proofs/VERIFICATION-STANCE.adoc index 9047faf..237b715 100644 --- a/verification/proofs/VERIFICATION-STANCE.adoc +++ b/verification/proofs/VERIFICATION-STANCE.adoc @@ -1,9 +1,9 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) Jonathan D.A. Jewell = VCL-ut Verification Stance (proof-backed) :toc: :sectnums: -// SPDX-License-Identifier: AGPL-3.0-or-later -// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) WARNING: vcl-ut is the interface between *hypatia* and *verisim*; both sides trust safety claims made here. This document states *precisely* what is and is @@ -167,21 +167,57 @@ OWED section. `fieldWithin` (membership-quantified bound: any field *provably in* the layout, via `Data.Vect.Elem` and `Data.So.soAnd`, satisfies `foff + fsize <= cap` — the honest replacement for the deleted false - `offsetInBounds`/`?metavariable`). *Remaining sliver (precisely - scoped, NOT faked):* the additive `Layout.alignUp size a = size + - paddingFor size a` ↔ ceil `alignTo size a` equivalence for `a > 0`, - left as the documented `String` note `alignUpAdditiveEquivOWED` - (needs the `Data.Nat` Euclidean identity + the `Bool`↔`Prop` bridge - for `paddingFor`'s conditional) — a scope note, never a - `believe_me`. - `VclTotal.ABI.Foreign` is *deliberately still excluded* but is *not - unsound*: it contains **no proofs at all** — only `%foreign` C - declarations and `Maybe`/`Either` wrappers. Its gaps are (a) it does - not compile as-is (FFI plumbing: missing `Data.Bits`, etc.) and (b) - the architectural stub-FFI issue (the level tag is an *asserted - integer* from the Zig side, not a transported proof). That is genuine - Phase 3+ architecture (implement the Zig/Rust side; transport an - opaque proof token), OWED and disclosed — not a false proof. + `offsetInBounds`/`?metavariable`). *Phase 5 — partial advance on the + additive↔ceil sliver:* the previously-`String` OWED + `alignUpAdditiveEquivOWED` is replaced by a real proof + infrastructure that closes the substantive content for the + zero-remainder case: + * `EuclidView`/`euclid` — the Euclidean decomposition view, built + from `Data.Nat.Division.DivisionTheorem` + `boundModNatNZ`. + * `sIdentZero`/`sIdentSucc` — Euclidean identity refinements + tagged by the value of `modNatNZ s (S k) ItIsSucc`. + * `sPlusMinus` — the `r ≤ k` ⇒ `S r + (k - r) = S k` identity. + * `alignUpADividesZero` — `(modNatNZ s (S k) ItIsSucc = Z) ⇒ + Divides (S k) (alignUpA s k)`. Genuine `Refl`-closed theorem + with witness `divNatNZ s (S k) ItIsSucc`, zero proof-escape. ++ + The remaining residual is purely the non-zero remainder case's + *rewrite chain*: the math is `S r' + (k `minus` r') = S k` (closed + by `sPlusMinus` + `boundModNatNZ`), but the multi-step + `plusAssociative`/`plusCommutative` chain triggers an idris2 0.8.0 + elaborator quirk (`FromString` mis-elaboration). Disclosed as + `alignUpADividesSuccOWED` — a precisely-scoped String stub that + names the obstruction. Strictly smaller than the original OWED + (which covered both cases) and is a toolchain-sequencing limit + rather than a missing lemma. Re-attempt under idris2 0.8.1+ or via + manual `replace` chaining; tracked at standards#124 follow-up. ++ + The `Data.Nat.Division` dependency is now declared in + `verification/proofs/vclut-core.ipkg` (`depends = contrib`); the + bundled idris2-contrib package is pure stdlib and adds no new + trusted axioms. + `VclTotal.ABI.Foreign` *has been retired* (2026-06-02). It is now + `VclTotal.Legacy.Foreign` at `src/interface/legacy/Foreign.idr`, + flagged DEPRECATED at the top of the file, with the stale + `corpus/VclTotal/ABI/Foreign.idr` symlink deleted. The file is + retained ONLY so external C/Zig callers that linked the legacy + `libvqlut` ABI before Phase 5 can still find an Idris-side + description; no part of the proof corpus imports it and no other + Idris module in this repo imports it (`grep -r "import + VclTotal.ABI.Foreign"` → 0). The architectural "asserted integer + instead of transported proof" issue is no longer a stand-alone + OWED: the *honest* Idris-side path is now + **`VclTotal.ABI.Tier2`** at `src/interface/abi/Tier2.idr`, which + binds `vclut_verify_wire` (Zig shim → `vclut_rs_verify` in + `src/interface/attest`) and returns a 65-byte Ed25519-signed + attestation `[level:1][sig:64]` over `DOMAIN ‖ sha256(stmt_wire) + ‖ sha256(schema_wire) ‖ level`. Trust-model ceiling is the same + Tier-2 ceiling described under the boundary model below + (strictly weaker than Tier-1 recompute-PCC; strictly stronger + than the deprecated asserted-integer path). The `Tier2.idr` + module typechecks under idris2 0.8.0 (`--check` green) and + carries no proofs (it is plumbing); the safety properties live + in `src/interface/attest/src/lib.rs::tests`. . *(Phase 2 — RESOLVED) L2/L3/L5 predicates de-vacuized.* The content-free constructors (`ExprTypeSafe`/`WhereTypeSafe`, `AllNullableFieldsGuarded`'s `GuardedNull`, `AllSelectItemsTyped`'s @@ -223,14 +259,23 @@ OWED section. *structural* part (clause present, ≥1 agent, every requirement agent declared) — proved by genuine superset monotonicity (`fuaSuperset`/`agentDeclaredAppL`/`agentDeclaredAppR` + - `fuaNilAppend`), no proof-escape. L10's no-direct-`ENTAILS`-cycle + `fuaNilAppend`), no proof-escape. L10's no-`ENTAILS`-cycle sub-property is *provably NOT* join-closed and remains carried by the explicit minimal `JoinSideCondition` (`epiNoCycle (composeJoin q1 q2) = True` only at `EpistemicSafe`; `Unit` elsewhere) — stated - in the TYPE, never faked. *Still future work (precisely):* - deepening the L9/L10 *predicates themselves* to the full - `checkLevelN` semantics (L9 ≠ `LinUnlimited`; L10 acyclic `ENTAILS` - as a predicate rather than a side-condition). And the + in the TYPE, never faked. *(Phase 5 follow-up — RESOLVED.)* The L9 + predicate deepening landed in Phase 4b already (`L9_LinearSafe` + carries `linearEnforcedStmt stmt = True`, which rejects both + absence AND `LinUnlimited` — see `Levels.idr` line 249), so the + "L9 ≠ `LinUnlimited`" item was a stance-doc lag, not real debt. + The L10 *direct-only* cycle check was upgraded to full transitive + graph-cycle detection via finite-fuel transitive closure + (`Decide.transStep`/`transCloseN`/`transClose`/ + `hasTransitiveCycle`); `epiNoCycle` now routes through + `hasTransitiveCycle`, which is strictly stronger than the previous + `hasCircularEntails` and catches `a⊨b⊨c⊨a` and longer chains. The + `JoinSideCondition`'s body-agnostic shape means the existing + `compositionPreservation` proof continues to work verbatim. The certificate is still *not transported across the FFI* (see the `ABI.Foreign` item) — the in-corpus certificate is not yet a runtime proof token handed to hypatia/verisim. @@ -341,8 +386,10 @@ OWED section. (`%default total`, zero proof-escape, fuel-bounded; `WireConformance` `Refl`-pins it byte-for-byte to the Rust `to_wire*` encoder, P5b-2 #29 / P5c-1 #30). The *encode* direction - (Idris `Statement`/`OctadSchema`→wire) remains OWED (not needed by - the recompute tier — the producer encodes from Rust). (3) *RESOLVED:* + (Idris `Statement`/`OctadSchema`→wire) is *deferred-by-design* + (not OWED): the recompute tier's producer encodes from Rust, so an + Idris encoder would only duplicate the conformance-pinned Rust + encoder for no additional consumer-side guarantee. (3) *RESOLVED:* the decision-transport tier is delivered as Tier-1 recompute-`wasm32` (P5c-5 #32) with the faithful Rust decision port machine-pinned to the corpus (P5c-2/3/4 #31). (4) *RESOLVED:* the P5d C-ABI @@ -361,8 +408,18 @@ OWED section. `vector.x` unresolved → Reject) is pinned Rust-side (decoded self-check) + by input-value conformance (`conform2`), not by Idris `Refl`; the find-free decision structure *is* `Refl`-pinned. (iii) - the L9/L10 predicate depth and the additive↔ceil `alignUp` sliver - remain as previously scoped. + the additive↔ceil `alignUp` sliver + remains as previously scoped (Nat-arithmetic Euclidean-identity + infrastructure is the unwritten dependency; the practical + alignment-divides guarantee is already machine-checked via the + canonical-form `alignToDivides` theorem, so closing the additive + equivalence is a documentation tightening, not a safety upgrade). + *L9/L10 predicate depth (item iii in earlier revisions) is no + longer a disclosed limit*: L9 was deepened in Phase 4b + (`linearEnforcedStmt` rejects `LinUnlimited`); L10 acyclicity now + uses full transitive-closure cycle detection + (`Decide.hasTransitiveCycle`), not just direct symmetry — see the + Phase-5 follow-up note in the L6–L10 join-closure entry above. == Consumer guidance (hypatia / verisim) @@ -384,8 +441,16 @@ OWED section. checks on the strength of a vcl-ut FFI level tag. * `VclTotal.ABI.Layout` is now *sound + CI-gated* (unsound claims deleted, not faked); its genuine alignment/no-padding theorems are - OWED. `VclTotal.ABI.Foreign` contains *no proofs* (FFI plumbing) — do - not treat its returned level tag as a verified claim. + OWED. `VclTotal.Legacy.Foreign` (formerly `VclTotal.ABI.Foreign`, + retired 2026-06-02) contains *no proofs* (FFI plumbing) and its + returned level tag is a Zig-side trusted assertion, NOT a verified + claim — *do not use the legacy bindings*. The honest Idris-side + path is **`VclTotal.ABI.Tier2`**, which returns a Tier-2 + Ed25519-signed attestation: still trust-the-certifier (the C-ABI + ceiling), but cryptographically bound and tamper-evident, with the + Rust crate's test suite enforcing the fail-closed contract. For + the strongest guarantee, use Tier-1 recompute-PCC over `wasm32` + (`src/interface/recompute-wasm`). * *Transport (DELIVERED — Tier-1 recompute-PCC, P5c, vcl-ut#25).* The guarantee is **not** "trust our attestation". You are shipped the `wasm32` module `src/interface/recompute-wasm` (`vcl_recompute`) + diff --git a/verification/proofs/corpus/VclTotal/ABI/Foreign.idr b/verification/proofs/corpus/VclTotal/ABI/Foreign.idr deleted file mode 120000 index 4370b86..0000000 --- a/verification/proofs/corpus/VclTotal/ABI/Foreign.idr +++ /dev/null @@ -1 +0,0 @@ -../../../../../src/interface/abi/Foreign.idr \ No newline at end of file