Skip to content

feat(abi): add Tier-2 Idris bindings + retire legacy Foreign + close L10 transitive cycle #47

New issue

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

Sign up for GitHub

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

Already on GitHub? Sign in to your account

Closed
hyperpolymath wants to merge 1 commit into from
Closed

feat(abi): add Tier-2 Idris bindings + retire legacy Foreign + close L10 transitive cycle #47

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

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
28 changes: 21 additions & 7 deletions docs/developer/ABI-FFI-README.adoc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
// SPDX-License-Identifier: MPL-2.0
// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
= ABI/FFI Standards
{{~ Aditionally delete this line and fill out the template below ~}}

Expand All @@ -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)
Expand Down Expand Up @@ -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)
Expand Down
79 changes: 71 additions & 8 deletions src/core/Decide.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,5 @@
-- SPDX-License-Identifier: AGPL-3.0-or-later
-- Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>

-- SPDX-License-Identifier: MPL-2.0
-- Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
||| VCL-total Core Decide — canonical safety deciders (single source of truth)
|||
||| Phase 2 of the standards#124 HOLE remediation de-vacuizes the Level
Expand Down Expand Up @@ -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`
Expand All @@ -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`
Expand Down
209 changes: 209 additions & 0 deletions src/interface/abi/Tier2.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,209 @@
-- SPDX-License-Identifier: MPL-2.0
-- Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
--
||| 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)
Loading
Loading