diff --git a/.github/workflows/proof-corpus.yml b/.github/workflows/proof-corpus.yml index 71ffd85..65e0963 100644 --- a/.github/workflows/proof-corpus.yml +++ b/.github/workflows/proof-corpus.yml @@ -37,12 +37,24 @@ jobs: - name: Checkout repository uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 - # NOTE: pin to a commit SHA per repo security posture once a stable - # release SHA is recorded (TODO(SHA-pin); tags used here interim). - - name: Set up Idris2 0.8.0 - uses: idris-community/setup-idris@v1 - with: - idris-version: 0.8.0 + # Idris2 0.8.0 is built from PINNED official source. The former + # `idris-community/setup-idris` action's repository no longer + # resolves (404), and no maintained equivalent exists; a + # SHA-pinned source build is deterministic, version-exact, and + # depends on no third-party action (matches the repo's pin + # posture). `idris-lang/Idris2` tag v0.8.0 == commit + # 15a3e4e70843f7a34100f6470c04b791330788df. + - name: Build & install Idris2 0.8.0 from pinned source + run: | + set -euo pipefail + sudo apt-get update -qq + sudo apt-get install -y --no-install-recommends chezscheme make gcc + git clone --no-checkout https://github.com/idris-lang/Idris2.git /tmp/Idris2 + git -C /tmp/Idris2 checkout 15a3e4e70843f7a34100f6470c04b791330788df + make -C /tmp/Idris2 bootstrap SCHEME=chezscheme + make -C /tmp/Idris2 install PREFIX="$HOME/.idris2" + echo "$HOME/.idris2/bin" >> "$GITHUB_PATH" + echo "IDRIS2_PREFIX=$HOME/.idris2" >> "$GITHUB_ENV" - name: Proof-escape audit (no believe_me / postulate / assert_* / sorry) run: | @@ -51,7 +63,8 @@ jobs: files="src/core/Grammar.idr src/core/Schema.idr src/core/Decide.idr \ src/core/Levels.idr src/core/Checker.idr \ src/core/Composition.idr src/core/Epistemic.idr \ - src/interface/abi/Types.idr src/interface/abi/Layout.idr" + src/interface/abi/Types.idr src/interface/abi/Layout.idr \ + src/interface/abi/LayoutProofs.idr" if grep -nE '\b(believe_me|really_believe_me|assert_total|assert_smaller|idris_crash|postulate|sorry)\b' \ $files | grep -vE ':\s*(--|\|\|\|)' ; then echo "::error::proof-escape symbol found in the Phase-1 corpus" diff --git a/CHANGELOG.md b/CHANGELOG.md index 55dbc9b..967e7cb 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -10,6 +10,33 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ## [Unreleased] +### Verified + +**VclTotal proof corpus — Phase 0→4 remediation** (2026-05-18/19, +hyperpolymath/standards#124). The `src/core/**` Idris2 corpus, which at +Phase 0 did not compile and had never been machine-checked, is now +CI-gated and green: + +- `verification/proofs/vclut-core.ipkg` builds clean under idris2 0.8.0 + (`idris2 --build`, exit 0, `%default total`) as **10 modules**, with + **zero proof-escape symbols** (no `believe_me`/`postulate`/`assert_*`/ + `idris_crash`/`sorry`), enforced by `.github/workflows/proof-corpus.yml`. +- Phase 1 (#21): corpus resurrection — `ABI.Types`/`Grammar` repaired, + `.ipkg`/CI added, L4 verified in situ. +- Phase 2 (#22): L2/L3/L5 de-vacuized over the shared `Core.Decide` + deciders + `checkLevel2/3/5Sound` + genuine `composeJoin` closure. +- Phase 3 (#23): L1 + L6–L10 soundness; `Checker.certifyAt`/ + `certifyRequested` assemble a genuine dependent `SafetyCertificate`; + `ABI.Layout` made sound; Phase 3d removed the fabricating Zig FFI + (now fail-closed) and added the proof-gated `Checker.certifiedLevel`. +- Phase 4 (PR #24): `ABI.LayoutProofs` (genuine alignment/no-padding/ + bounds) + L6–L10 `composeJoin` closure (`l6..l9Compose`, + `epiStructJoin`); L10 acyclicity carried by the explicit + `JoinSideCondition` (provably non-closed, not faked). + +`verification/proofs/VERIFICATION-STANCE.adoc` is the authoritative, +precisely-scoped catalogue (residual OWED items disclosed, not masked). + ### Renamed **V{Q→C}L-{UT→total}** (2026-04-05). Full repo-wide migration of the project diff --git a/CLAUDE-CROSS-SESSION-NOTE.md b/CLAUDE-CROSS-SESSION-NOTE.md deleted file mode 100644 index 02abdaa..0000000 --- a/CLAUDE-CROSS-SESSION-NOTE.md +++ /dev/null @@ -1,56 +0,0 @@ - - -# vcl-ut PR #21 — cross-session note (2026-05-19) - -**To: the Claude actively working `_wt-vclut-phase1` (Phase 2 de-vacuization).** -**From: the session that rebased #21 onto post-#20 main and gated it.** - -## What I did (and why your worktree looked the way it did) -- `#20` is **MERGED** to `main` (`89c64a1`). -- I rebased #21 onto post-#20 main: `git rebase --onto origin/main 81f8e33` - → tip `25a3296`. This is the foundation **you built Phase 2 on top of** - (`25a3296` ← `51831b5` L5 ← `79d1ef3` L2 + your current WIP). Your adoption - of it is correct; nothing of yours was lost. -- I proved via a local **real-file** idris2-0.8.0 corpus build (reconstructs - the symlink tree as real files, bypassing this WSL clone's - `core.symlinks=false` confound — naive local builds here are unreliable; - use this technique) that `25a3296` does **not** compile: the old - `Composition.joinWhereTypeSafe` referenced `NoWhere`/`WhereTypeSafe`, - which #20 removed when it redefined L2 `AllComparisonsTypeSafe` to - `MkAllCompat : whereComparisonsCompatible m schema = True -> …`. - You have since fixed exactly this (`whereCompatJoin`/`MkAllCompat`). Good. -- I converted PR #21 to **DRAFT** and posted two close-out comments - (latest: issue-comment-4483359972) so it cannot be admin-merged broken. - The remote PR head is still the stale, non-compiling `25a3296`. - -## The decision is YOURS to make -The user wants you to decide #21's disposition. Key facts for that call: - -1. **Remote `25a3296` is stale & broken.** Your Phase-2 fixes (`51831b5`, - `79d1ef3`, + uncommitted `Checker/Composition/Decide/Levels.idr`) are - **local-only, unpushed**. Until you push, the PR cannot be made ready. -2. **Merge oracle = the idris2 build, never GitHub-MERGEABLE.** Before - un-drafting/merging, get the real-file local build (or the - `idris2 0.8.0 --build vclut-core` CI job) green. Do not admin-merge a - proof corpus past a non-green build — that is the antipattern this whole - PR exists to kill. -3. **No proof escapes** (`believe_me`/`assert_*`/`postulate`/`sorry`/ - `idris_crash`/`Obj.magic`) — rhodibot CI greps & bans them. -4. **Backup** of the original pre-rebase #21 tip: local ref - `backup/vclut-21-prerebase-3a4ec43` (compiled green, but pre-#20, - 7-module). Don't resurrect it; it's a safety net only. - -## Suggested path (you decide) -Finish Phase 2 → run the **real-file local idris2 build** to green → -commit → push the branch → mark PR #21 **ready** → let CI confirm → -then it can land. Refs standards#124 (does **not** Close — the user -closes the epic). Update the shared memory -(`project_vclut_hole_deeper_than_documented.md`) when state changes; -its top "📌 CLOSE-OUT CONSOLIDATED STATE" block is the current handoff. - -— Delete this file once you've read it. diff --git a/PROOF-NEEDS.md b/PROOF-NEEDS.md index 20ff595..f197968 100644 --- a/PROOF-NEEDS.md +++ b/PROOF-NEEDS.md @@ -6,8 +6,8 @@ - **LOC**: ~8,000 - **Languages**: Rust, ReScript, Idris2, Zig - **Existing ABI proofs**: `src/interface/abi/*.idr` + domain-specific Idris2: `src/core/Checker.idr`, `Grammar.idr`, `Levels.idr`, `Schema.idr`, `Composition.idr` -- **Machine-verified**: `verification/proofs/SafetyL4Model.idr` only (idris2 0.8.0 `--check`, exit 0, zero proof escapes) — the Level-4 SQL-injection remediation -- **Dangerous patterns**: ⚠️ The `src/core/**` Idris2 corpus **does not compile** on `origin/main` and has **never been machine-checked** (no `.ipkg`/CI). `ABI.Types` has ≥4 type errors; `Grammar.idr` forward-references types with no `mutual` block. L2/L3/L5 safety predicates are **vacuous** (inhabited for any input, incl. injection); `SafetyCertificate` is never constructed by `checkQuery`; the Zig FFI is a `SELECT`-substring stub. See `verification/proofs/VERIFICATION-STANCE.adoc` for the authoritative, proof-backed catalogue. The earlier "None detected" line was wrong. +- **Machine-verified**: the full `VclTotal` proof corpus — `verification/proofs/vclut-core.ipkg` builds clean under idris2 0.8.0 (`idris2 --build`, exit 0, `%default total`, **zero proof-escape symbols**, CI-gated by `.github/workflows/proof-corpus.yml`) as **10 modules** (`ABI.{Types,Layout,LayoutProofs}` + `Core.{Grammar,Schema,Decide,Levels,Checker,Composition,Epistemic}`), plus the self-contained `verification/proofs/SafetyL4Model.idr` (`--check`, exit 0). Phases 1–3 are on `origin/main` (PRs #21/#22/#23); Phase 4 (`LayoutProofs` + L6–L10 `composeJoin` closure) is **PR #24**, pending merge. +- **Status (Phase 0 → 4 RESOLVED, honestly)**: the Phase-0 blockers are fixed, not faked — the corpus compiles and is machine-checked; `ABI.Types`/`Grammar` errors repaired; **L2/L3/L5 de-vacuized** (Phase 2, evidence-carrying predicates over `Core.Decide`); all ten levels carry `checkLevelNSound` and `Checker.certifyAt`/`certifyRequested` assemble a genuine dependent `SafetyCertificate` (Phase 3); the Zig FFI is no longer a fabricating stub — it is **fail-closed** with a proof-gated `Checker.certifiedLevel` mint (Phase 3d). Remaining honest gaps are precisely scoped (FFI proof-transport, string→`Statement` parser, L3 subquery/heuristic scoping, L9/L10 predicate depth, the additive↔ceil `alignUp` sliver). `verification/proofs/VERIFICATION-STANCE.adoc` is the authoritative, proof-backed catalogue and takes precedence over this file. ## What Needs Proving @@ -20,8 +20,9 @@ - Prove: parser (ReScript side) accepts exactly the Idris2-specified grammar ### Level System (src/core/Levels.idr) -- ✅ L4 `NoRawUserInput` de-vacuized + `checkLevel4Sound` + `noRawUserInputCompose` (verified in `verification/proofs/SafetyL4Model.idr`) -- ⚠️ L2/L3/L5 predicates still vacuous — de-vacuize with evidence-carrying constructors and prove each `checkLevelN` sound (as done for L4) +- ✅ L4 `NoRawUserInput` de-vacuized + `checkLevel4Sound` + `noRawUserInputCompose` (verified in `verification/proofs/SafetyL4Model.idr` and in situ in the corpus) +- ✅ L2/L3/L5 de-vacuized (Phase 2) — evidence-carrying predicates over `Core.Decide`, with `checkLevel2/3/5Sound` and genuine `composeJoin` closure +- ✅ L1 + L6–L10 sound (Phase 3) + genuine L6–L10 `composeJoin` closure (Phase 4: `l6..l9Compose`, `epiStructJoin`); L10 acyclicity carried by the explicit `JoinSideCondition` (provably non-closed, not faked) - 10-level type safety hierarchy — prove level ordering is a lattice - Prove: level promotion/demotion preserves query safety diff --git a/src/core/Checker.idr b/src/core/Checker.idr index 7b5ce6b..7a9e72a 100644 --- a/src/core/Checker.idr +++ b/src/core/Checker.idr @@ -455,12 +455,17 @@ checkLevel5Sound stmt schema m prf ||| ||| @stmt The statement to check. ||| @return (True, _) if LIMIT is present; (False, diagnostic) otherwise. +||| Defined THROUGH `Decide.cardinalityBoundedStmt` (Phase 4b), so the +||| L6 predicate and this decision share one definition. public export checkLevel6 : Statement -> (Bool, String) -checkLevel6 stmt = - case limit stmt of - Just n => (True, "L6:CardinalitySafe — LIMIT " ++ show n ++ " present") - Nothing => (False, "L6:CardinalitySafe FAILED — no LIMIT clause on query") +checkLevel6 stmt = l6Verdict (cardinalityBoundedStmt stmt) + where + l6Verdict : Bool -> (Bool, String) + l6Verdict True = + (True, "L6:CardinalitySafe — result cardinality is LIMIT-bounded") + l6Verdict False = + (False, "L6:CardinalitySafe FAILED — no LIMIT clause on query") ||| Level 7 — EffectTracked: the statement includes an EFFECTS declaration. ||| Side-effectful operations (INSERT/UPDATE/DELETE) must declare their @@ -468,12 +473,16 @@ checkLevel6 stmt = ||| ||| @stmt The statement to check. ||| @return (True, _) if effectDecl is present; (False, diagnostic) otherwise. +||| Defined THROUGH `Decide.effectTrackedStmt` (Phase 4b). public export checkLevel7 : Statement -> (Bool, String) -checkLevel7 stmt = - case effectDecl stmt of - Just _ => (True, "L7:EffectTracked — effect declaration present") - Nothing => (False, "L7:EffectTracked FAILED — no EFFECTS declaration") +checkLevel7 stmt = l7Verdict (effectTrackedStmt stmt) + where + l7Verdict : Bool -> (Bool, String) + l7Verdict True = + (True, "L7:EffectTracked — effect declaration present") + l7Verdict False = + (False, "L7:EffectTracked FAILED — no EFFECTS declaration") ||| Level 8 — TemporalSafe: the statement includes a version constraint. ||| Queries against VeriSimDB's time-travel engine must specify temporal @@ -481,12 +490,16 @@ checkLevel7 stmt = ||| ||| @stmt The statement to check. ||| @return (True, _) if versionConst is present; (False, diagnostic) otherwise. +||| Defined THROUGH `Decide.temporalBoundedStmt` (Phase 4b). public export checkLevel8 : Statement -> (Bool, String) -checkLevel8 stmt = - case versionConst stmt of - Just _ => (True, "L8:TemporalSafe — version constraint present") - Nothing => (False, "L8:TemporalSafe FAILED — no version constraint") +checkLevel8 stmt = l8Verdict (temporalBoundedStmt stmt) + where + l8Verdict : Bool -> (Bool, String) + l8Verdict True = + (True, "L8:TemporalSafe — version constraint present") + l8Verdict False = + (False, "L8:TemporalSafe FAILED — no version constraint") ||| Level 9 — LinearSafe: the statement includes a linearity annotation ||| with an actual consumption constraint (LinUseOnce or LinBounded). @@ -494,14 +507,17 @@ checkLevel8 stmt = ||| ||| @stmt The statement to check. ||| @return (True, _) if a consume constraint is present; (False, diagnostic) otherwise. +||| Defined THROUGH `Decide.linearEnforcedStmt` (Phase 4b): rejects both +||| absence AND the no-op `LinUnlimited`, matching the predicate exactly. public export checkLevel9 : Statement -> (Bool, String) -checkLevel9 stmt = - case linearAnnot stmt of - Nothing => (False, "L9:LinearSafe FAILED — no linearity annotation") - Just LinUnlimited => (False, "L9:LinearSafe FAILED — LinUnlimited is not a consume constraint") - Just LinUseOnce => (True, "L9:LinearSafe — consume-after-1-use constraint present") - Just (LinBounded _) => (True, "L9:LinearSafe — bounded usage constraint present") +checkLevel9 stmt = l9Verdict (linearEnforcedStmt stmt) + where + l9Verdict : Bool -> (Bool, String) + l9Verdict True = + (True, "L9:LinearSafe — enforced consumption bound (LinUseOnce/LinBounded)") + l9Verdict False = + (False, "L9:LinearSafe FAILED — no enforced linearity (absent or LinUnlimited)") ||| Level 10 — EpistemicSafe: the statement includes an EPISTEMIC clause ||| with well-formed agent declarations and consistent requirements. @@ -516,139 +532,84 @@ checkLevel9 stmt = ||| @stmt The statement to check. ||| @return (True, _) if epistemic clause is present and consistent; ||| (False, diagnostic) otherwise. +||| Defined THROUGH `Decide.epistemicConsistentStmt` (Phase 4b). The +||| agent-declaration / direct-ENTAILS-cycle helper logic was hoisted +||| verbatim into `Decide` so the L10 predicate and this decision share +||| ONE definition (single source of truth, no drift). The richer +||| diagnostic (which agent, etc.) is derived separately for the message +||| but the verdict bit is exactly the decider. public export checkLevel10 : Statement -> (Bool, String) -checkLevel10 stmt = - case epistemicClause stmt of - Nothing => (False, "L10:EpistemicSafe FAILED — no EPISTEMIC clause") - Just (EpClause agents reqs) => - case agents of - [] => (False, "L10:EpistemicSafe FAILED — EPISTEMIC clause has no agents") - _ => - let undeclared = findUndeclaredAgents agents reqs - in case undeclared of - [] => - if hasCircularEntails reqs - then (False, "L10:EpistemicSafe FAILED — circular ENTAILS dependency") - else (True, "L10:EpistemicSafe — " - ++ show (length agents) ++ " agent(s), " - ++ show (length reqs) ++ " requirement(s) verified") - (name :: _) => - (False, "L10:EpistemicSafe FAILED — agent '" - ++ name ++ "' used in REQUIRES but not declared in AGENTS") +checkLevel10 stmt = l10Verdict (epistemicConsistentStmt stmt) where - ||| Get a string identifier for an agent (for comparison purposes). - agentId : Agent -> String - agentId AgEngine = "ENGINE" - agentId (AgProver name) = "PROVER:" ++ name - agentId AgValidator = "VALIDATOR" - agentId (AgUser name) = "USER:" ++ name - agentId AgFederation = "FEDERATION" - - ||| Check if an agent is in the declared agents list. - agentDeclared : Agent -> List Agent -> Bool - agentDeclared a declared = any (\d => agentId a == agentId d) declared - - ||| Find agents referenced in requirements but not declared. - ||| Returns list of undeclared agent name strings. - findUndeclaredAgents : List Agent -> List EpistemicRequirement -> List String - findUndeclaredAgents declared [] = [] - findUndeclaredAgents declared (EpReqKnows a _ :: rest) = - if agentDeclared a declared - then findUndeclaredAgents declared rest - else agentId a :: findUndeclaredAgents declared rest - findUndeclaredAgents declared (EpReqBelieves a _ :: rest) = - if agentDeclared a declared - then findUndeclaredAgents declared rest - else agentId a :: findUndeclaredAgents declared rest - findUndeclaredAgents declared (EpReqCommon _ :: rest) = - findUndeclaredAgents declared rest - findUndeclaredAgents declared (EpReqEntails a1 a2 _ :: rest) = - let u1 = if agentDeclared a1 declared then [] else [agentId a1] - u2 = if agentDeclared a2 declared then [] else [agentId a2] - in u1 ++ u2 ++ findUndeclaredAgents declared rest - - ||| Collect all (source, target) pairs from ENTAILS requirements. - entailsPairs : List EpistemicRequirement -> List (String, String) - entailsPairs [] = [] - entailsPairs (EpReqEntails a1 a2 _ :: rest) = - (agentId a1, agentId a2) :: entailsPairs rest - entailsPairs (_ :: rest) = entailsPairs rest - - ||| Check for direct circular ENTAILS (a->b and b->a). - ||| Full cycle detection would require a graph algorithm; - ||| for now we check the direct symmetry violation. - hasCircularEntails : List EpistemicRequirement -> Bool - hasCircularEntails reqs = - let pairs = entailsPairs reqs - in any (\(a, b) => any (\(c, d) => a == d && b == c) pairs) pairs + l10Verdict : Bool -> (Bool, String) + l10Verdict True = + (True, "L10:EpistemicSafe — clause present, agents declared, no direct ENTAILS cycle") + l10Verdict False = + (False, "L10:EpistemicSafe FAILED — missing clause / no agents / undeclared agent / direct ENTAILS cycle") -- ═══════════════════════════════════════════════════════════════════════ --- Soundness of the L6–L10 decision procedures (Phase 3a, standards#124) +-- Soundness of the L6–L10 decision procedures (Phase 4b, standards#124) -- ═══════════════════════════════════════════════════════════════════════ -- -- Each `checkLevelNSound` proves: if `checkLevelN` accepts, the statement -- genuinely carries the corresponding `LN_*` witness. Same `with … proof --- p` shape as `checkLevel4Sound`; no proof-escape. +-- p` shape as `checkLevel2Sound`; no proof-escape. -- --- SCOPE (honest): the L6–L10 *predicates* assert exactly "the relevant --- clause/annotation is present" (`limit/effectDecl/versionConst/ --- linearAnnot/epistemicClause stmt = Just _`). That is a real, --- non-vacuous property (a query lacking the clause cannot inhabit it), --- but it is *shallower* than what `checkLevelN` additionally enforces --- (L9 rejects `LinUnlimited`; L10 also requires declared agents and no --- direct ENTAILS cycle). These soundness lemmas are genuine for the --- predicates as stated; the predicate↔checker shallowness gap is --- disclosed in VERIFICATION-STANCE.adoc (Phase 3 residual), not masked. - -||| L6 soundness: acceptance ⇒ a LIMIT is present. +-- PHASE 4b: the L6–L10 predicates now carry the SHARED `Decide` decider +-- (`cardinalityBoundedStmt`/`effectTrackedStmt`/`temporalBoundedStmt`/ +-- `linearEnforcedStmt`/`epistemicConsistentStmt`), and `checkLevelN` is +-- defined THROUGH that same decider, so each soundness lemma is a direct +-- equality extraction — not a check against a parallel re-implementation +-- that could drift. The Phase-3 disclosed predicate↔checker shallowness +-- gap (L9 `LinUnlimited`; L10 declared-agents / direct ENTAILS cycle) is +-- hereby CLOSED at the level of these predicates. Remaining disclosed L10 +-- residual (full transitive cycle detection, proposition well-typedness) +-- is in VERIFICATION-STANCE.adoc — scoped, not masked. + +||| L6 soundness: acceptance ⇒ the cardinality decider holds. export checkLevel6Sound : (stmt : Statement) -> (m : String) -> checkLevel6 stmt = (True, m) -> L6_CardinalitySafe stmt -checkLevel6Sound stmt m prf with (limit stmt) proof p - checkLevel6Sound stmt m prf | Just n = MkL6 stmt n p - checkLevel6Sound stmt m prf | Nothing = void (falseNotTrue (cong fst prf)) +checkLevel6Sound stmt m prf with (cardinalityBoundedStmt stmt) proof p + checkLevel6Sound stmt m prf | True = MkL6 p + checkLevel6Sound stmt m prf | False = void (falseNotTrue (cong fst prf)) -||| L7 soundness: acceptance ⇒ an EFFECTS declaration is present. +||| L7 soundness: acceptance ⇒ the effect-tracked decider holds. export checkLevel7Sound : (stmt : Statement) -> (m : String) -> checkLevel7 stmt = (True, m) -> L7_EffectTracked stmt -checkLevel7Sound stmt m prf with (effectDecl stmt) proof p - checkLevel7Sound stmt m prf | Just e = MkL7 stmt e p - checkLevel7Sound stmt m prf | Nothing = void (falseNotTrue (cong fst prf)) +checkLevel7Sound stmt m prf with (effectTrackedStmt stmt) proof p + checkLevel7Sound stmt m prf | True = MkL7 p + checkLevel7Sound stmt m prf | False = void (falseNotTrue (cong fst prf)) -||| L8 soundness: acceptance ⇒ a version constraint is present. +||| L8 soundness: acceptance ⇒ the temporal-bound decider holds. export checkLevel8Sound : (stmt : Statement) -> (m : String) -> checkLevel8 stmt = (True, m) -> L8_TemporalSafe stmt -checkLevel8Sound stmt m prf with (versionConst stmt) proof p - checkLevel8Sound stmt m prf | Just v = MkL8 stmt v p - checkLevel8Sound stmt m prf | Nothing = void (falseNotTrue (cong fst prf)) +checkLevel8Sound stmt m prf with (temporalBoundedStmt stmt) proof p + checkLevel8Sound stmt m prf | True = MkL8 p + checkLevel8Sound stmt m prf | False = void (falseNotTrue (cong fst prf)) -||| L9 soundness: acceptance ⇒ a linearity annotation is present. -||| (The accepting cases are exactly `LinUseOnce` / `LinBounded`; the -||| witness `MkL9` records `linearAnnot stmt = Just la`.) +||| L9 soundness: acceptance ⇒ linearity is genuinely ENFORCED +||| (`LinUseOnce`/`LinBounded`; absence and `LinUnlimited` are rejected +||| by the shared decider — the Phase-3 L9 gap is closed). export checkLevel9Sound : (stmt : Statement) -> (m : String) -> checkLevel9 stmt = (True, m) -> L9_LinearSafe stmt -checkLevel9Sound stmt m prf with (linearAnnot stmt) proof p - checkLevel9Sound stmt m prf | Nothing = - void (falseNotTrue (cong fst prf)) - checkLevel9Sound stmt m prf | Just LinUnlimited = - void (falseNotTrue (cong fst prf)) - checkLevel9Sound stmt m prf | Just LinUseOnce = - MkL9 stmt LinUseOnce p - checkLevel9Sound stmt m prf | Just (LinBounded n) = - MkL9 stmt (LinBounded n) p +checkLevel9Sound stmt m prf with (linearEnforcedStmt stmt) proof p + checkLevel9Sound stmt m prf | True = MkL9 p + checkLevel9Sound stmt m prf | False = void (falseNotTrue (cong fst prf)) -||| L10 soundness: acceptance ⇒ an EPISTEMIC clause is present. +||| L10 soundness: acceptance ⇒ the epistemic-consistency decider holds +||| (clause present, ≥1 agent, all requirement agents declared, no direct +||| ENTAILS cycle — the Phase-3 L10 gap is closed at this predicate). export checkLevel10Sound : (stmt : Statement) -> (m : String) -> checkLevel10 stmt = (True, m) -> L10_EpistemicSafe stmt -checkLevel10Sound stmt m prf with (epistemicClause stmt) proof p - checkLevel10Sound stmt m prf | Just ec = MkL10 stmt ec p - checkLevel10Sound stmt m prf | Nothing = - void (falseNotTrue (cong fst prf)) +checkLevel10Sound stmt m prf with (epistemicConsistentStmt stmt) proof p + checkLevel10Sound stmt m prf | True = MkL10 p + checkLevel10Sound stmt m prf | False = void (falseNotTrue (cong fst prf)) -- ═══════════════════════════════════════════════════════════════════════ -- Pipeline Runner diff --git a/src/core/Composition.idr b/src/core/Composition.idr index ef8fb75..7e086d0 100644 --- a/src/core/Composition.idr +++ b/src/core/Composition.idr @@ -523,11 +523,26 @@ l5Compose (MkL5 s1 sch t1) (MkL5 s2 _ t2) = -- SECTION 6: L6..L10 — GENUINE equational proofs about join* combiners -- ══════════════════════════════════════════════════════════════════════ -||| `joinLimit (Just a) (Just b)` is `Just (min a b)` — definitional. -l6Compose : L6_CardinalitySafe q1 -> L6_CardinalitySafe q2 -> - L6_CardinalitySafe (composeJoin q1 q2) -l6Compose (MkL6 s1 n1 p1) (MkL6 s2 n2 p2) = - MkL6 (composeJoin s1 s2) (min n1 n2) (rewrite p1 in rewrite p2 in Refl) +-- PHASE 4b (standards#124). The L6–L10 predicates now carry the shared +-- `Decide` deciders. L6–L9 are GENUINELY closed under `composeJoin` +-- (`joinLimit`/`joinEffects`/`joinVersion` of two present clauses is +-- present; all four ENFORCED×ENFORCED `joinLinear` cases stay enforced). +-- L10's structural part (clause present, ≥1 agent, all requirement +-- agents declared) is ALSO genuinely join-closed and proven below +-- (`epiStructJoin`); its no-direct-ENTAILS-cycle part is provably NOT +-- join-closed (two acyclic requirement sets can union to a cyclic one), +-- so it is supplied as an explicit, minimal `JoinSideCondition`, never +-- faked. No believe_me / postulate / assert_* / idris_crash / sorry. + +-- ── Maybe-level join-closure (L6–L9) ────────────────────────────────── + +||| `joinLimit` of two present LIMITs is present (`Just (min a b)`). +presentJoinLimit : (la, lb : Maybe Nat) -> + isPresentM la = True -> isPresentM lb = True -> + isPresentM (joinLimit la lb) = True +presentJoinLimit (Just _) (Just _) _ _ = Refl +presentJoinLimit Nothing _ p _ = void (notFalseTrue p) +presentJoinLimit (Just _) Nothing _ q = void (notFalseTrue q) ||| For any two `EffectDecl`s, `joinEffects (Just a) (Just b)` is `Just _`. joinEffectsJust : (a, b : EffectDecl) @@ -549,11 +564,14 @@ joinEffectsJust EffConsume EffWrite = (_ ** Refl) joinEffectsJust EffConsume EffReadWrite = (_ ** Refl) joinEffectsJust EffConsume EffConsume = (_ ** Refl) -l7Compose : L7_EffectTracked q1 -> L7_EffectTracked q2 -> - L7_EffectTracked (composeJoin q1 q2) -l7Compose (MkL7 s1 e1 p1) (MkL7 s2 e2 p2) = - let (c ** q) = joinEffectsJust e1 e2 - in MkL7 (composeJoin s1 s2) c (rewrite p1 in rewrite p2 in q) +||| `joinEffects` of two present effect decls is present. +presentJoinEffects : (ea, eb : Maybe EffectDecl) -> + isPresentM ea = True -> isPresentM eb = True -> + isPresentM (joinEffects ea eb) = True +presentJoinEffects (Just a) (Just b) _ _ = + let (_ ** q) = joinEffectsJust a b in rewrite q in Refl +presentJoinEffects Nothing _ p _ = void (notFalseTrue p) +presentJoinEffects (Just _) Nothing _ r = void (notFalseTrue r) ||| For any two `VersionConstraint`s, `joinVersion (Just a) (Just b)` is ||| `Just _` (case split on the four constructor shapes; Nat payloads @@ -574,11 +592,49 @@ joinVersionJust (VerRange _ _) (VerAtLeast _) = (_ ** Refl) joinVersionJust (VerRange _ _) (VerExact _) = (_ ** Refl) joinVersionJust (VerRange _ _) (VerRange _ _) = (_ ** Refl) -l8Compose : L8_TemporalSafe q1 -> L8_TemporalSafe q2 -> +||| `joinVersion` of two present version constraints is present. +presentJoinVersion : (va, vb : Maybe VersionConstraint) -> + isPresentM va = True -> isPresentM vb = True -> + isPresentM (joinVersion va vb) = True +presentJoinVersion (Just a) (Just b) _ _ = + let (_ ** q) = joinVersionJust a b in rewrite q in Refl +presentJoinVersion Nothing _ p _ = void (notFalseTrue p) +presentJoinVersion (Just _) Nothing _ r = void (notFalseTrue r) + +||| `joinLinear` of two ENFORCED annotations stays enforced. All four +||| `{LinUseOnce,LinBounded} × {LinUseOnce,LinBounded}` combinations +||| yield `LinUseOnce` or `LinBounded` — genuinely join-closed. +enforcedJoinLinear : (la, lb : Maybe LinearAnnotation) -> + linEnforcedM la = True -> linEnforcedM lb = True -> + linEnforcedM (joinLinear la lb) = True +enforcedJoinLinear (Just LinUseOnce) (Just LinUseOnce) _ _ = Refl +enforcedJoinLinear (Just LinUseOnce) (Just (LinBounded _)) _ _ = Refl +enforcedJoinLinear (Just (LinBounded _)) (Just LinUseOnce) _ _ = Refl +enforcedJoinLinear (Just (LinBounded _)) (Just (LinBounded _)) _ _ = Refl +enforcedJoinLinear Nothing _ p _ = void (notFalseTrue p) +enforcedJoinLinear (Just LinUnlimited) _ p _ = void (notFalseTrue p) +enforcedJoinLinear (Just LinUseOnce) Nothing _ q = void (notFalseTrue q) +enforcedJoinLinear (Just LinUseOnce) (Just LinUnlimited) _ q = void (notFalseTrue q) +enforcedJoinLinear (Just (LinBounded _)) Nothing _ q = void (notFalseTrue q) +enforcedJoinLinear (Just (LinBounded _)) (Just LinUnlimited) _ q = void (notFalseTrue q) + +l6Compose : {q1, q2 : Statement} -> + L6_CardinalitySafe q1 -> L6_CardinalitySafe q2 -> + L6_CardinalitySafe (composeJoin q1 q2) +l6Compose {q1} {q2} (MkL6 p1) (MkL6 p2) = + MkL6 (presentJoinLimit (limit q1) (limit q2) p1 p2) + +l7Compose : {q1, q2 : Statement} -> + L7_EffectTracked q1 -> L7_EffectTracked q2 -> + L7_EffectTracked (composeJoin q1 q2) +l7Compose {q1} {q2} (MkL7 p1) (MkL7 p2) = + MkL7 (presentJoinEffects (effectDecl q1) (effectDecl q2) p1 p2) + +l8Compose : {q1, q2 : Statement} -> + L8_TemporalSafe q1 -> L8_TemporalSafe q2 -> L8_TemporalSafe (composeJoin q1 q2) -l8Compose (MkL8 s1 v1 p1) (MkL8 s2 v2 p2) = - let (c ** q) = joinVersionJust v1 v2 - in MkL8 (composeJoin s1 s2) c (rewrite p1 in rewrite p2 in q) +l8Compose {q1} {q2} (MkL8 p1) (MkL8 p2) = + MkL8 (presentJoinVersion (versionConst q1) (versionConst q2) p1 p2) ||| For any two `LinearAnnotation`s, `joinLinear (Just a) (Just b)` is ||| `Just _`. @@ -594,22 +650,196 @@ joinLinearJust (LinBounded _) LinUnlimited = (_ ** Refl) joinLinearJust (LinBounded _) LinUseOnce = (_ ** Refl) joinLinearJust (LinBounded _) (LinBounded _) = (_ ** Refl) -l9Compose : L9_LinearSafe q1 -> L9_LinearSafe q2 -> +l9Compose : {q1, q2 : Statement} -> + L9_LinearSafe q1 -> L9_LinearSafe q2 -> L9_LinearSafe (composeJoin q1 q2) -l9Compose (MkL9 s1 a1 p1) (MkL9 s2 a2 p2) = - let (c ** q) = joinLinearJust a1 a2 - in MkL9 (composeJoin s1 s2) c (rewrite p1 in rewrite p2 in q) - -||| `joinEpistemic (Just (EpClause ..)) (Just (EpClause ..))` is `Just _`. -joinEpistemicJust : (a, b : EpistemicClause) - -> (c : EpistemicClause ** joinEpistemic (Just a) (Just b) = Just c) -joinEpistemicJust (EpClause _ _) (EpClause _ _) = (_ ** Refl) - -l10Compose : L10_EpistemicSafe q1 -> L10_EpistemicSafe q2 -> +l9Compose {q1} {q2} (MkL9 p1) (MkL9 p2) = + MkL9 (enforcedJoinLinear (linearAnnot q1) (linearAnnot q2) p1 p2) + +-- ── L10: structural part is join-closed; acyclicity is NOT ──────────── + +||| An append is `[]` only if both sides are. +appendNilSplit : (xs, ys : List a) -> xs ++ ys = [] -> (xs = [], ys = []) +appendNilSplit [] ys prf = (Refl, prf) +appendNilSplit (_ :: _) _ Refl impossible + +||| `(if b then [] else [x]) = []` forces `b = True`. +ifNilForcesTrue : {0 a : Type} -> (b : Bool) -> (x : a) -> + (if b then [] else [x]) = (the (List a) []) -> b = True +ifNilForcesTrue True _ _ = Refl +ifNilForcesTrue False _ Refl impossible + +||| `agentDeclared` is monotone under appending declared agents (left). +||| Clean structural induction because `Decide.agentDeclared` is explicit +||| `||` recursion (not Prelude `any`). +agentDeclaredAppL : (a : Agent) -> (xs, ys : List Agent) -> + agentDeclared a xs = True -> agentDeclared a (xs ++ ys) = True +agentDeclaredAppL a (d :: ds) ys prf with (agentId a == agentId d) + _ | True = Refl + _ | False = agentDeclaredAppL a ds ys prf + +||| `agentDeclared` is monotone under appending declared agents (right). +agentDeclaredAppR : (a : Agent) -> (xs, ys : List Agent) -> + agentDeclared a ys = True -> agentDeclared a (xs ++ ys) = True +agentDeclaredAppR a [] ys prf = prf +agentDeclaredAppR a (d :: ds) ys prf with (agentId a == agentId d) + _ | True = Refl + _ | False = agentDeclaredAppR a ds ys prf + +||| If no requirement agent is undeclared wrt `d`, the same holds wrt any +||| superset `d'` (`sub` witnesses `d ⊆ d'` by `agentDeclared`). The only +||| reachable requirement shapes are those whose contribution is `[]` +||| (otherwise the `findUndeclaredAgents d r = []` hypothesis is absurd), +||| so each agent involved is declared in `d`, hence in `d'` via `sub`. +fuaSuperset : + (d, d' : List Agent) -> + (sub : (a : Agent) -> agentDeclared a d = True -> agentDeclared a d' = True) -> + (r : List EpistemicRequirement) -> + findUndeclaredAgents d r = [] -> findUndeclaredAgents d' r = [] +fuaSuperset d d' sub [] _ = Refl +fuaSuperset d d' sub (EpReqKnows a _ :: rest) pr with (agentDeclared a d) proof adp + _ | True = rewrite sub a (rewrite adp in Refl) in fuaSuperset d d' sub rest pr + _ | False = absurd pr +fuaSuperset d d' sub (EpReqBelieves a _ :: rest) pr with (agentDeclared a d) proof adp + _ | True = rewrite sub a (rewrite adp in Refl) in fuaSuperset d d' sub rest pr + _ | False = absurd pr +fuaSuperset d d' sub (EpReqCommon _ :: rest) pr = + fuaSuperset d d' sub rest pr +fuaSuperset d d' sub (EpReqEntails a1 a2 _ :: rest) pr + with (agentDeclared a1 d) proof adp1 + fuaSuperset d d' sub (EpReqEntails a1 a2 _ :: rest) pr | False = absurd pr + fuaSuperset d d' sub (EpReqEntails a1 a2 _ :: rest) pr | True + with (agentDeclared a2 d) proof adp2 + fuaSuperset d d' sub (EpReqEntails a1 a2 _ :: rest) pr | True | False = + absurd pr + fuaSuperset d d' sub (EpReqEntails a1 a2 _ :: rest) pr | True | True = + rewrite sub a1 (rewrite adp1 in Refl) in + rewrite sub a2 (rewrite adp2 in Refl) in + fuaSuperset d d' sub rest pr + +||| `findUndeclaredAgents` over a requirements append is `[]` when each +||| side is (the head contributions split off cleanly via +||| `appendNilSplit`; no list-associativity gymnastics needed). +fuaNilAppend : + (d : List Agent) -> (r, s : List EpistemicRequirement) -> + findUndeclaredAgents d r = [] -> findUndeclaredAgents d s = [] -> + findUndeclaredAgents d (r ++ s) = [] +fuaNilAppend d [] s _ ps = ps +fuaNilAppend d (EpReqKnows a _ :: rest) s pr ps with (agentDeclared a d) + _ | True = fuaNilAppend d rest s pr ps + _ | False = absurd pr +fuaNilAppend d (EpReqBelieves a _ :: rest) s pr ps with (agentDeclared a d) + _ | True = fuaNilAppend d rest s pr ps + _ | False = absurd pr +fuaNilAppend d (EpReqCommon _ :: rest) s pr ps = + fuaNilAppend d rest s pr ps +fuaNilAppend d (EpReqEntails a1 a2 _ :: rest) s pr ps + with (agentDeclared a1 d) + fuaNilAppend d (EpReqEntails a1 a2 _ :: rest) s pr ps | False = absurd pr + fuaNilAppend d (EpReqEntails a1 a2 _ :: rest) s pr ps | True + with (agentDeclared a2 d) + fuaNilAppend d (EpReqEntails a1 a2 _ :: rest) s pr ps | True | False = + absurd pr + fuaNilAppend d (EpReqEntails a1 a2 _ :: rest) s pr ps | True | True = + fuaNilAppend d rest s pr ps + +||| `epiStructOK`'s inner decision is `case findUndeclaredAgents .. of +||| [] => True; (_::_) => False`. From that fold being `True`, recover the +||| underlying `findUndeclaredAgents .. = []` equality (the `(_::_)` branch +||| yields `False = True`, absurd). Genuine, no escape. +undeclaredCaseNil : (us : List String) -> + (case us of { [] => True; (_ :: _) => False }) = True -> us = [] +undeclaredCaseNil [] _ = Refl +undeclaredCaseNil (_ :: _) Refl impossible + +||| Conversely, if `findUndeclaredAgents .. = []` then the `epiStructOK` +||| inner fold is `True` (rewrite collapses the `case`). +nilUndeclaredCase : (us : List String) -> + us = [] -> (case us of { [] => True; (_ :: _) => False }) = True +nilUndeclaredCase _ prf = rewrite prf in Refl + +||| Top-level superset lift of `e1` to the joined agent list, factored out +||| so the ascribed-`let` parse ambiguity (a `let x : T` whose `T` ends in +||| `= []`) never arises. Left-append monotonicity. +epiStructDecl1 : + (x1 : Agent) -> (xs1 : List Agent) -> + (x2 : Agent) -> (xs2 : List Agent) -> + (rs1 : List EpistemicRequirement) -> + findUndeclaredAgents (x1 :: xs1) rs1 = [] -> + findUndeclaredAgents ((x1 :: xs1) ++ (x2 :: xs2)) rs1 = [] +epiStructDecl1 x1 xs1 x2 xs2 rs1 d1 = + fuaSuperset (x1 :: xs1) ((x1 :: xs1) ++ (x2 :: xs2)) + (\a => agentDeclaredAppL a (x1 :: xs1) (x2 :: xs2)) rs1 d1 + +||| Right-append monotonicity counterpart of `epiStructDecl1`. +epiStructDecl2 : + (x1 : Agent) -> (xs1 : List Agent) -> + (x2 : Agent) -> (xs2 : List Agent) -> + (rs2 : List EpistemicRequirement) -> + findUndeclaredAgents (x2 :: xs2) rs2 = [] -> + findUndeclaredAgents ((x1 :: xs1) ++ (x2 :: xs2)) rs2 = [] +epiStructDecl2 x1 xs1 x2 xs2 rs2 d2 = + fuaSuperset (x2 :: xs2) ((x1 :: xs1) ++ (x2 :: xs2)) + (\a => agentDeclaredAppR a (x1 :: xs1) (x2 :: xs2)) rs2 d2 + +||| The STRUCTURAL part of L10 (clause present, ≥1 agent, all requirement +||| agents declared) IS closed under `composeJoin`: `joinEpistemic` unions +||| agents and requirements; a nonempty agent list stays nonempty under +||| append, and declaring MORE agents never makes a declared agent +||| undeclared (`fuaSuperset` via `agentDeclaredAppL/R`). +epiStructJoin : (q1, q2 : Statement) -> + epiStructOK q1 = True -> epiStructOK q2 = True -> + epiStructOK (composeJoin q1 q2) = True +epiStructJoin q1 q2 e1 e2 with (epistemicClause q1) + epiStructJoin q1 q2 e1 e2 | Nothing = absurd e1 + epiStructJoin q1 q2 e1 e2 | Just (EpClause as1 rs1) with (as1) + epiStructJoin q1 q2 e1 e2 | Just (EpClause as1 rs1) | [] = absurd e1 + epiStructJoin q1 q2 e1 e2 | Just (EpClause as1 rs1) | (x1 :: xs1) + with (epistemicClause q2) + epiStructJoin q1 q2 e1 e2 | Just (EpClause as1 rs1) | (x1 :: xs1) + | Nothing = absurd e2 + epiStructJoin q1 q2 e1 e2 | Just (EpClause as1 rs1) | (x1 :: xs1) + | Just (EpClause as2 rs2) with (as2) + epiStructJoin q1 q2 e1 e2 | Just (EpClause as1 rs1) | (x1 :: xs1) + | Just (EpClause as2 rs2) | [] = absurd e2 + epiStructJoin q1 q2 e1 e2 | Just (EpClause as1 rs1) | (x1 :: xs1) + | Just (EpClause as2 rs2) | (x2 :: xs2) = + -- e1 collapses to: (case findUndeclaredAgents (x1::xs1) rs1 of + -- [] => True; (_::_) => False) = True ; likewise e2. Recover + -- the `= []` equalities, lift each to the joined agent list + -- (superset monotone), then fuaNilAppend over rs1 ++ rs2. + let d1 = undeclaredCaseNil (findUndeclaredAgents (x1 :: xs1) rs1) e1 + d2 = undeclaredCaseNil (findUndeclaredAgents (x2 :: xs2) rs2) e2 + decl1 = epiStructDecl1 x1 xs1 x2 xs2 rs1 d1 + decl2 = epiStructDecl2 x1 xs1 x2 xs2 rs2 d2 + in nilUndeclaredCase + (findUndeclaredAgents ((x1 :: xs1) ++ (x2 :: xs2)) (rs1 ++ rs2)) + (fuaNilAppend ((x1 :: xs1) ++ (x2 :: xs2)) rs1 rs2 decl1 decl2) + +||| Extra evidence needed ONLY to compose at `EpistemicSafe`: the JOINED +||| query is still free of a direct ENTAILS cycle. This is the single L10 +||| sub-property provably NOT closed under relational join (two acyclic +||| requirement sets can union to a cyclic one). Trivial (`Unit`) at every +||| other level, so `compositionPreservation` stays uniform while the +||| non-closure is explicit in the TYPE — not hidden behind a vacuous +||| predicate or a proof escape. Disclosed in VERIFICATION-STANCE.adoc. +public export +JoinSideCondition : Statement -> Statement -> SafetyLevel -> Type +JoinSideCondition q1 q2 EpistemicSafe = epiNoCycle (composeJoin q1 q2) = True +JoinSideCondition _ _ _ = Unit + +||| L10 composition: the structural part is genuinely join-closed +||| (`epiStructJoin`); the acyclic part is supplied as the minimal +||| `epiNoCycle (composeJoin q1 q2) = True` side-condition. Together they +||| are exactly `epistemicConsistentStmt (composeJoin q1 q2) = True`. +l10Compose : (q1, q2 : Statement) -> + epiNoCycle (composeJoin q1 q2) = True -> + L10_EpistemicSafe q1 -> L10_EpistemicSafe q2 -> L10_EpistemicSafe (composeJoin q1 q2) -l10Compose (MkL10 s1 c1 p1) (MkL10 s2 c2 p2) = - let (c ** q) = joinEpistemicJust c1 c2 - in MkL10 (composeJoin s1 s2) c (rewrite p1 in rewrite p2 in q) +l10Compose q1 q2 ncyc (MkL10 p1) (MkL10 p2) = + let (s1, _) = andTrueSplit (epiStructOK q1) (epiNoCycle q1) p1 + (s2, _) = andTrueSplit (epiStructOK q2) (epiNoCycle q2) p2 + in MkL10 (andTrueIntro (epiStructJoin q1 q2 s1 s2) ncyc) -- ══════════════════════════════════════════════════════════════════════ -- SECTION 7: the main theorem @@ -619,73 +849,79 @@ l10Compose (MkL10 s1 c1 p1) (MkL10 s2 c2 p2) = ||| closed under relational join: a level-k certificate for q1 and q2 ||| yields a level-k certificate for `composeJoin q1 q2`. ||| -||| L0/L1/L4/L6..L10 are genuine. L2/L3/L5 are produced at the correct -||| indexed type by `lN Compose`, but the L2/L3/L5 predicates are still -||| vacuous (Phase 2 work) — disclosed OWED in VERIFICATION-STANCE.adoc. +||| PHASE 4b: L0/L1/L4 and now L2/L3/L5 (de-vacuized in Phase 2) and +||| L6/L7/L8/L9 are ALL genuine and UNCONDITIONALLY join-closed. L10's +||| structural content is genuine and join-closed (`epiStructJoin`); its +||| direct-ENTAILS-acyclicity is provably NOT join-closed, so the theorem +||| now takes an explicit `JoinSideCondition` — `Unit` at every level +||| except `EpistemicSafe`, where it is the minimal +||| `epiNoCycle (composeJoin q1 q2) = True`. The non-closure is therefore +||| visible in the TYPE, not faked. See VERIFICATION-STANCE.adoc. export compositionPreservation : (q1, q2 : Statement) -> (schema : OctadSchema) -> (k : SafetyLevel) -> Composable q1 q2 -> + JoinSideCondition q1 q2 k -> SafetyCertificate q1 schema k -> SafetyCertificate q2 schema k -> SafetyCertificate (composeJoin q1 q2) schema k -compositionPreservation q1 q2 _ ParseSafe _ _ _ = +compositionPreservation q1 q2 _ ParseSafe _ _ _ _ = CertL0 (MkL0 (composeJoin q1 q2)) -compositionPreservation q1 q2 _ SchemaBound _ +compositionPreservation q1 q2 _ SchemaBound _ _ (CertL1 _ l1a) (CertL1 _ l1b) = CertL1 (MkL0 (composeJoin q1 q2)) (l1Compose l1a l1b) -compositionPreservation q1 q2 _ TypeCompat _ +compositionPreservation q1 q2 _ TypeCompat _ _ (CertL2 _ l1a l2a) (CertL2 _ l1b l2b) = CertL2 (MkL0 (composeJoin q1 q2)) (l1Compose l1a l1b) (l2Compose l2a l2b) -compositionPreservation q1 q2 _ NullSafe _ +compositionPreservation q1 q2 _ NullSafe _ _ (CertL3 _ l1a l2a l3a) (CertL3 _ l1b l2b l3b) = CertL3 (MkL0 (composeJoin q1 q2)) (l1Compose l1a l1b) (l2Compose l2a l2b) (l3Compose l3a l3b) -compositionPreservation q1 q2 _ InjectionProof _ +compositionPreservation q1 q2 _ InjectionProof _ _ (CertL4 _ l1a l2a l3a l4a) (CertL4 _ l1b l2b l3b l4b) = CertL4 (MkL0 (composeJoin q1 q2)) (l1Compose l1a l1b) (l2Compose l2a l2b) (l3Compose l3a l3b) (l4Compose l4a l4b) -compositionPreservation q1 q2 _ ResultTyped _ +compositionPreservation q1 q2 _ ResultTyped _ _ (CertL5 _ l1a l2a l3a l4a l5a) (CertL5 _ l1b l2b l3b l4b l5b) = CertL5 (MkL0 (composeJoin q1 q2)) (l1Compose l1a l1b) (l2Compose l2a l2b) (l3Compose l3a l3b) (l4Compose l4a l4b) (l5Compose l5a l5b) -compositionPreservation q1 q2 _ CardinalitySafe _ +compositionPreservation q1 q2 _ CardinalitySafe _ _ (CertL6 _ l1a l2a l3a l4a l5a l6a) (CertL6 _ l1b l2b l3b l4b l5b l6b) = CertL6 (MkL0 (composeJoin q1 q2)) (l1Compose l1a l1b) (l2Compose l2a l2b) (l3Compose l3a l3b) (l4Compose l4a l4b) (l5Compose l5a l5b) (l6Compose l6a l6b) -compositionPreservation q1 q2 _ EffectTracked _ +compositionPreservation q1 q2 _ EffectTracked _ _ (CertL7 _ l1a l2a l3a l4a l5a l6a l7a) (CertL7 _ l1b l2b l3b l4b l5b l6b l7b) = CertL7 (MkL0 (composeJoin q1 q2)) (l1Compose l1a l1b) (l2Compose l2a l2b) (l3Compose l3a l3b) (l4Compose l4a l4b) (l5Compose l5a l5b) (l6Compose l6a l6b) (l7Compose l7a l7b) -compositionPreservation q1 q2 _ TemporalSafe _ +compositionPreservation q1 q2 _ TemporalSafe _ _ (CertL8 _ l1a l2a l3a l4a l5a l6a l7a l8a) (CertL8 _ l1b l2b l3b l4b l5b l6b l7b l8b) = CertL8 (MkL0 (composeJoin q1 q2)) (l1Compose l1a l1b) (l2Compose l2a l2b) (l3Compose l3a l3b) (l4Compose l4a l4b) (l5Compose l5a l5b) (l6Compose l6a l6b) (l7Compose l7a l7b) (l8Compose l8a l8b) -compositionPreservation q1 q2 _ LinearSafe _ +compositionPreservation q1 q2 _ LinearSafe _ _ (CertL9 _ l1a l2a l3a l4a l5a l6a l7a l8a l9a) (CertL9 _ l1b l2b l3b l4b l5b l6b l7b l8b l9b) = CertL9 (MkL0 (composeJoin q1 q2)) (l1Compose l1a l1b) (l2Compose l2a l2b) (l3Compose l3a l3b) (l4Compose l4a l4b) (l5Compose l5a l5b) (l6Compose l6a l6b) (l7Compose l7a l7b) (l8Compose l8a l8b) (l9Compose l9a l9b) -compositionPreservation q1 q2 _ EpistemicSafe _ +compositionPreservation q1 q2 _ EpistemicSafe _ ncyc (CertL10 _ l1a l2a l3a l4a l5a l6a l7a l8a l9a l10a) (CertL10 _ l1b l2b l3b l4b l5b l6b l7b l8b l9b l10b) = CertL10 (MkL0 (composeJoin q1 q2)) (l1Compose l1a l1b) (l2Compose l2a l2b) (l3Compose l3a l3b) (l4Compose l4a l4b) (l5Compose l5a l5b) (l6Compose l6a l6b) (l7Compose l7a l7b) (l8Compose l8a l8b) (l9Compose l9a l9b) - (l10Compose l10a l10b) + (l10Compose q1 q2 ncyc l10a l10b) diff --git a/src/core/Decide.idr b/src/core/Decide.idr index 5a02eac..361b753 100644 --- a/src/core/Decide.idr +++ b/src/core/Decide.idr @@ -555,3 +555,163 @@ allFieldsBoundFromResolve (r :: rs) schema prf = (allFieldRefsResolve rs schema) prf in ConsBound (fieldBoundFromResolve r schema h) (allFieldsBoundFromResolve rs schema t) + +-- ═══════════════════════════════════════════════════════════════════════ +-- Levels 6–10 deciders — Phase 4b (standards#124) +-- +-- Phase 3 left L6–L10 as *presence-only* predicates ("the clause is +-- present"), and disclosed in VERIFICATION-STANCE.adoc that this is +-- shallower than what `Checker.checkLevelN` actually enforces (L9 also +-- rejects `LinUnlimited`; L10 also requires declared agents and no direct +-- ENTAILS cycle). Phase 4b closes that gap: the L6–L10 predicates now +-- carry ` stmt = True` exactly as L2/L3/L5 do, and +-- `Checker.checkLevelN` is defined THROUGH the same decider, so +-- `checkLevelNSound` is a genuine equality, not a parallel +-- re-implementation that could silently drift. +-- +-- Nothing here uses believe_me / postulate / assert_* / idris_crash / +-- sorry: the deciders are ordinary case analysis over the AST. +-- ═══════════════════════════════════════════════════════════════════════ + +-- The L6–L8 deciders factor through a tiny `Maybe`-level presence test +-- and L9 through a `Maybe LinearAnnotation` enforcement test. Naming the +-- helpers (rather than inlining `case`) keeps the Composition closure +-- lemmas a single structural step, matching the `notAnyTy`/`selectItemTyped` +-- house style. + +||| A `Maybe` clause is present. +public export +isPresentM : Maybe a -> Bool +isPresentM (Just _) = True +isPresentM Nothing = False + +||| L6 — CardinalitySafe: the query bounds its result cardinality with a +||| LIMIT. The AST carries no finer cardinality information, and a query +||| with no LIMIT genuinely fails this (not vacuous). +public export +cardinalityBoundedStmt : Statement -> Bool +cardinalityBoundedStmt stmt = isPresentM (limit stmt) + +||| L7 — EffectTracked: the query declares its effects. +public export +effectTrackedStmt : Statement -> Bool +effectTrackedStmt stmt = isPresentM (effectDecl stmt) + +||| L8 — TemporalSafe: the query pins a version constraint. +public export +temporalBoundedStmt : Statement -> Bool +temporalBoundedStmt stmt = isPresentM (versionConst stmt) + +||| A linearity annotation that actually ENFORCES a consumption bound: +||| `LinUseOnce` or `LinBounded`. Absence and the no-op `LinUnlimited` +||| are NOT enforced. +public export +linEnforcedM : Maybe LinearAnnotation -> Bool +linEnforcedM (Just LinUseOnce) = True +linEnforcedM (Just (LinBounded _)) = True +linEnforcedM (Just LinUnlimited) = False +linEnforcedM Nothing = False + +||| L9 — LinearSafe: the query carries a linearity annotation that +||| actually enforces a consumption bound. This is the genuine Phase-4b +||| strengthening that closes the Phase-3 disclosed L9 predicate↔checker +||| gap (`LinUnlimited`/absence are now rejected by the predicate too). +public export +linearEnforcedStmt : Statement -> Bool +linearEnforcedStmt stmt = linEnforcedM (linearAnnot stmt) + +-- L10 epistemic-consistency helpers, hoisted verbatim from the +-- `Checker.checkLevel10` where-block so the predicate and the checker +-- share ONE definition (single source of truth, no drift). + +||| String identity of an agent (declaration / cycle comparison key). +public export +agentId : Agent -> String +agentId AgEngine = "ENGINE" +agentId (AgProver name) = "PROVER:" ++ name +agentId AgValidator = "VALIDATOR" +agentId (AgUser name) = "USER:" ++ name +agentId AgFederation = "FEDERATION" + +||| Whether an agent is in the declared-agents list (by `agentId`). +||| Defined by explicit `||` spine recursion rather than Prelude `any` +||| (which is `foldr`/`Delay`-based and does NOT reduce structurally on +||| `_::_`, so monotonicity inductions stall — the same reason `Decide` +||| uses `refElem` instead of `elemBy`). Extensionally identical to +||| `any (\d => agentId a == agentId d)`. +public export +agentDeclared : Agent -> List Agent -> Bool +agentDeclared _ [] = False +agentDeclared a (d :: ds) = (agentId a == agentId d) || agentDeclared a ds + +||| Agents referenced in requirements but not declared (as `agentId`s). +public export +findUndeclaredAgents : + List Agent -> List EpistemicRequirement -> List String +findUndeclaredAgents declared [] = [] +findUndeclaredAgents declared (EpReqKnows a _ :: rest) = + if agentDeclared a declared + then findUndeclaredAgents declared rest + else agentId a :: findUndeclaredAgents declared rest +findUndeclaredAgents declared (EpReqBelieves a _ :: rest) = + if agentDeclared a declared + then findUndeclaredAgents declared rest + else agentId a :: findUndeclaredAgents declared rest +findUndeclaredAgents declared (EpReqCommon _ :: rest) = + findUndeclaredAgents declared rest +findUndeclaredAgents declared (EpReqEntails a1 a2 _ :: rest) = + (if agentDeclared a1 declared then [] else [agentId a1]) + ++ (if agentDeclared a2 declared then [] else [agentId a2]) + ++ findUndeclaredAgents declared rest + +||| All (source, target) pairs from ENTAILS requirements. +public export +entailsPairs : List EpistemicRequirement -> List (String, String) +entailsPairs [] = [] +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. +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 + +||| 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` +||| unions agents and requirements; declaring MORE agents never makes a +||| declared agent undeclared — see `Composition.epiStructJoin`). +public export +epiStructOK : Statement -> Bool +epiStructOK stmt = case epistemicClause stmt of + Nothing => False + Just (EpClause agents reqs) => case agents of + [] => False + (_ :: _) => case findUndeclaredAgents agents reqs 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 +||| 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. +public export +epiNoCycle : Statement -> Bool +epiNoCycle stmt = case epistemicClause stmt of + Nothing => False + Just (EpClause _ reqs) => not (hasCircularEntails reqs) + +||| L10 — EpistemicSafe: clause present, ≥1 agent, all requirement agents +||| declared, AND no direct ENTAILS cycle. Mirrors `Checker.checkLevel10` +||| exactly. Split as `epiStructOK && epiNoCycle` so the join-closed +||| structural content and the (non-join-closed) acyclicity are separable +||| in the composition proof. +public export +epistemicConsistentStmt : Statement -> Bool +epistemicConsistentStmt stmt = epiStructOK stmt && epiNoCycle stmt diff --git a/src/core/Levels.idr b/src/core/Levels.idr index 7f7fbaa..060f577 100644 --- a/src/core/Levels.idr +++ b/src/core/Levels.idr @@ -205,51 +205,68 @@ data L5_ResultTyped : Statement -> OctadSchema -> Type where AllSelectItemsTyped (selectItems stmt) schema -> L5_ResultTyped stmt schema -||| Level 6: Cardinality Safe — query has a LIMIT clause. +||| Level 6: Cardinality Safe — the query bounds its result set. +||| +||| HISTORY (standards#124, Phase 4b): this used to be the presence-only +||| `MkL6 : (n : Nat) -> limit stmt = Just n -> ...`. It now carries the +||| shared decider `Decide.cardinalityBoundedStmt stmt = True` (which +||| `Checker.checkLevel6` is defined through), so `checkLevel6Sound` is a +||| direct equality, not a parallel re-implementation. Genuinely +||| non-vacuous: a query with no LIMIT cannot inhabit it. public export data L6_CardinalitySafe : Statement -> Type where - MkL6 : (stmt : Statement) -> - (n : Nat) -> - (limit stmt = Just n) -> - L6_CardinalitySafe stmt + MkL6 : cardinalityBoundedStmt stmt = True -> L6_CardinalitySafe stmt ||| Level 7: Effect Tracked — side effects are declared. +||| +||| HISTORY (standards#124, Phase 4b): presence-only → shared decider +||| `Decide.effectTrackedStmt stmt = True` (Checker.checkLevel7 defined +||| through it). Soundness: `Checker.checkLevel7Sound`. public export data L7_EffectTracked : Statement -> Type where - MkL7 : (stmt : Statement) -> - (eff : EffectDecl) -> - (effectDecl stmt = Just eff) -> - L7_EffectTracked stmt + MkL7 : effectTrackedStmt stmt = True -> L7_EffectTracked stmt ||| Level 8: Temporal Safe — version constraint is present. +||| +||| HISTORY (standards#124, Phase 4b): presence-only → shared decider +||| `Decide.temporalBoundedStmt stmt = True` (Checker.checkLevel8 defined +||| through it). Soundness: `Checker.checkLevel8Sound`. public export data L8_TemporalSafe : Statement -> Type where - MkL8 : (stmt : Statement) -> - (vc : VersionConstraint) -> - (versionConst stmt = Just vc) -> - L8_TemporalSafe stmt + MkL8 : temporalBoundedStmt stmt = True -> L8_TemporalSafe stmt -||| Level 9: Linear Safe — linearity annotation is present and respected. +||| Level 9: Linear Safe — linearity is actually ENFORCED. +||| +||| HISTORY (standards#124, Phase 4b): this used to be presence-only +||| (`linearAnnot stmt = Just la` for ANY `la`, including the no-op +||| `LinUnlimited`) — strictly weaker than what `checkLevel9` enforces, +||| a gap explicitly disclosed as a Phase-3 residual. It now carries the +||| shared decider `Decide.linearEnforcedStmt stmt = True`, which (like +||| the checker) rejects both absence AND `LinUnlimited`, requiring a +||| genuine `LinUseOnce`/`LinBounded` consumption bound. The Phase-3 L9 +||| predicate↔checker shallowness gap is hereby CLOSED. Soundness: +||| `Checker.checkLevel9Sound`. public export data L9_LinearSafe : Statement -> Type where - MkL9 : (stmt : Statement) -> - (la : LinearAnnotation) -> - (linearAnnot stmt = Just la) -> - L9_LinearSafe stmt - -||| Level 10: Epistemic Safe — epistemic clause is present and consistent. -||| The epistemic clause specifies agents, their knowledge/belief requirements, -||| and the S5 modal properties that must hold. The checker verifies: -||| 1. All referenced agents are declared in the clause's agent list -||| 2. Each REQUIRES KNOWS/BELIEVES/COMMON references valid propositions -||| 3. ENTAILS requirements respect the S5 knowledge transfer axiom -||| 4. No circular knowledge dependencies exist + MkL9 : linearEnforcedStmt stmt = True -> L9_LinearSafe stmt + +||| Level 10: Epistemic Safe — epistemic clause present AND consistent. +||| +||| HISTORY (standards#124, Phase 4b): this used to be presence-only +||| (`epistemicClause stmt = Just ec`), strictly weaker than the +||| consistency `checkLevel10` enforces (a disclosed Phase-3 residual). +||| It now carries the shared decider `Decide.epistemicConsistentStmt +||| stmt = True` — clause present, ≥1 agent, every requirement-referenced +||| agent declared, and no direct (a⊨b, b⊨a) ENTAILS cycle — exactly the +||| `checkLevel10` semantics (its helper logic was hoisted into `Decide` +||| as the single source of truth). Soundness: `Checker.checkLevel10Sound`. +||| Disclosed residual (NOT faked): full transitive ENTAILS-cycle +||| detection and proposition well-typedness remain OWED in +||| VERIFICATION-STANCE.adoc; the decider checks the *direct* symmetry +||| violation, matching the checker. public export data L10_EpistemicSafe : Statement -> Type where - MkL10 : (stmt : Statement) -> - (ec : EpistemicClause) -> - (epistemicClause stmt = Just ec) -> - L10_EpistemicSafe stmt + MkL10 : epistemicConsistentStmt stmt = True -> L10_EpistemicSafe stmt -- ═══════════════════════════════════════════════════════════════════════ diff --git a/src/interface/abi/LayoutProofs.idr b/src/interface/abi/LayoutProofs.idr new file mode 100644 index 0000000..18565a8 --- /dev/null +++ b/src/interface/abi/LayoutProofs.idr @@ -0,0 +1,168 @@ +-- SPDX-License-Identifier: PMPL-1.0-or-later +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + +||| VCL-cap ABI Layout — genuine alignment / no-padding / bounds proofs +||| +||| Phase 4a of the standards#124 remediation. The Phase-3c surgery +||| *deleted* three unsound `Layout` items rather than fake them +||| (`alignUpCorrect` used a `Bool` as a type + a bogus `Refl`; +||| `offsetInBounds` was an open hole; `queryPlanHeaderNoPadding` +||| over-claimed and would not reduce). This module discharges the +||| genuine theorems honestly. +||| +||| SELF-CONTAINED BY DESIGN: it does NOT `import VclTotal.ABI.Layout`. +||| That import pulls `Layout`'s record-field *projections* into scope +||| (`StructLayout.n`, `Field.size/offset/...`); idris2 0.8.0 then +||| mis-parses later declarations whose implicits/pattern-variables +||| collide with those names, reporting the failure on an unrelated +||| downstream line (a genuine, reproduced toolchain quirk — not faked). +||| Decoupling removes it entirely. The field model below +||| (`PField`/`qphFields`) is *byte-identical* to the field list inside +||| `Layout.queryPlanHeaderLayout` (magic/version/mode/level @ 4B, +||| plan_size @ 8B; cap 24B, 8B-aligned); these theorems therefore +||| establish exactly the intended QueryPlanHeader properties. +||| +||| Decision (user-approved, option A): prove divisibility for the +||| *canonical* round-up-to-multiple alignment `alignTo size a = +||| ceil(size/a) * a` — genuine *by construction* (witness = quotient, +||| no `div`/`mod` lemma debt, no escape). `Layout.alignUp` is the +||| additive form `size + paddingFor size a`; for `a > 0` the two agree. +||| That additive↔ceil equivalence is the ONLY remaining sliver, stated +||| precisely as `alignUpAdditiveEquivOWED` (a documented scope note, +||| NOT a `believe_me`). +||| +||| Nothing here uses believe_me / postulate / assert_* / idris_crash / +||| sorry. Verified by the CI `--build` of `vclut-core.ipkg`. + +module VclTotal.ABI.LayoutProofs + +import Data.Vect +import Data.Vect.Elem +import Data.So + +%default total + +-- ═══════════════════════════════════════════════════════════════════════ +-- 1. Genuine alignment divisibility (canonical ceil-multiple form) +-- ═══════════════════════════════════════════════════════════════════════ + +||| `Divides d m` ≜ ∃q. m = q * d — a genuine divisibility witness +||| (local; the `Layout.Divides` analogue, without the poisoning import). +public export +data Divides : Nat -> Nat -> Type where + DivideBy : (q : Nat) -> {0 d : Nat} -> {0 m : Nat} -> + (m = q * d) -> Divides d m + +||| Ceiling division `⌈s / a⌉` (saturating; `a = 0` yields `0`, cap +||| but meaningless — alignment is only sensible for `a > 0`). +public export +ceilDivNat : Nat -> Nat -> Nat +ceilDivNat s a = (s + (a `minus` 1)) `div` a + +||| Canonical round-up-to-multiple alignment = `⌈size/a⌉ * a`. +public export +alignTo : (size : Nat) -> (a : Nat) -> Nat +alignTo size a = ceilDivNat size a * a + +||| **Genuine** alignment divisibility, by construction: `alignTo size a` +||| is literally `q * a` with `q = ⌈size/a⌉`, so `a` divides it and the +||| witness is `q` itself. No `div`/`mod` lemma, no proof-escape. +public export +alignToDivides : (size : Nat) -> (a : Nat) -> Divides a (alignTo size a) +alignToDivides size a = DivideBy (ceilDivNat size a) Refl + +||| SCOPE NOTE (Phase 4a — precise, NOT faked). `Layout.alignUp size a = +||| size + Layout.paddingFor size a` (additive). For `a > 0` it equals +||| `alignTo size a`; that additive↔ceil equality needs the `Data.Nat` +||| Euclidean identity + the `Bool`↔`Prop` bridge for `paddingFor`'s +||| conditional. That single equivalence is the only remaining sliver, +||| deliberately left as this documented note (no proof-escape). The +||| substantive OWED — a genuine machine-checked alignment-divides +||| theorem, CI-gated — is resolved by `alignToDivides`. +public export +alignUpAdditiveEquivOWED : String +alignUpAdditiveEquivOWED = + "Layout.alignUp (additive) = alignTo (ceil) for a>0: scoped, " + ++ "not faked — see VERIFICATION-STANCE.adoc Phase 4a." + +-- ═══════════════════════════════════════════════════════════════════════ +-- 2. Genuine no-internal-padding proof for QueryPlanHeader +-- ═══════════════════════════════════════════════════════════════════════ + +||| A struct field model (offset, size). Distinct local record with +||| non-colliding accessor names (`foff`/`fsize`) — see the module note +||| on why `Layout.Field` is deliberately not imported. +public export +record PField where + constructor MkPField + foff : Nat + fsize : Nat + +||| QueryPlanHeader fields — byte-identical to the list inside +||| `Layout.queryPlanHeaderLayout`. +public export +qphFields : Vect 5 PField +qphFields = + [ MkPField 0 4 + , MkPField 4 4 + , MkPField 8 4 + , MkPField 12 4 + , MkPField 16 8 + ] + +||| Declared cap size of QueryPlanHeader (= Layout.queryPlanHeaderTotalSize). +public export +qphTotalSize : Nat +qphTotalSize = 24 + +||| Sum of declared field sizes. +public export +sumFieldSizes : Vect len PField -> Nat +sumFieldSizes [] = 0 +sumFieldSizes (x :: xs) = fsize x + sumFieldSizes xs + +||| **Genuine** no-internal-padding: field sizes (4+4+4+4+8) sum to +||| exactly the declared cap (24) — the header packs with no wasted +||| padding. Reduces under `Refl` (concrete `Vect` + plain constant). +public export +-- NB: `qphFields`/`qphTotalSize` are FULLY QUALIFIED here. A bare +-- lowercase global in a TYPE signature is silently auto-bound by idris2 +-- 0.8.0 as a fresh implicit (warning "shadowing …"), which decouples +-- the proof from the real definition ⇒ `Refl` then cannot reduce +-- (the documented standards#124 footgun; qualification pins it). +queryPlanHeaderNoPadding : + sumFieldSizes VclTotal.ABI.LayoutProofs.qphFields + = VclTotal.ABI.LayoutProofs.qphTotalSize +queryPlanHeaderNoPadding = Refl + +-- ═══════════════════════════════════════════════════════════════════════ +-- 3. Genuine, membership-quantified field-bounds proof +-- ═══════════════════════════════════════════════════════════════════════ + +||| Decider: every field's `foff + fsize` fits within `cap`. +public export +allWithin : Vect len PField -> Nat -> Bool +allWithin [] _ = True +allWithin (x :: xs) cap = (foff x + fsize x <= cap) && allWithin xs cap + +||| **Genuine** bounds proof: every QueryPlanHeader field's +||| `foff + fsize` is ≤ the declared cap. `allWithin qphFields 24` +||| *computes* to `True`, so the witness is `Oh`. Replaces the deleted +||| Phase-3c `?offsetInBoundsProof` hole. +public export +queryPlanHeaderWithin : + So (allWithin VclTotal.ABI.LayoutProofs.qphFields + VclTotal.ABI.LayoutProofs.qphTotalSize) +queryPlanHeaderWithin = Oh + +||| Membership-quantified bound: any field *provably in* the vector +||| satisfies `foff + fsize <= cap`. Honest replacement for the +||| deleted `offsetInBounds` (which quantified over an arbitrary field +||| not necessarily in the layout — false in general). Proved by +||| `Data.So.soAnd` over the `&&`-fold. +public export +fieldWithin : {0 len : Nat} -> {xs : Vect len PField} -> {x : PField} -> + (cap : Nat) -> So (allWithin xs cap) -> + Elem x xs -> So (foff x + fsize x <= cap) +fieldWithin cap prf Here = fst (soAnd prf) +fieldWithin cap prf (There e) = fieldWithin cap (snd (soAnd prf)) e diff --git a/verification/proofs/README.adoc b/verification/proofs/README.adoc index e95b6b6..7430697 100644 --- a/verification/proofs/README.adoc +++ b/verification/proofs/README.adoc @@ -6,6 +6,19 @@ This directory holds the *machine-verified* proof artefacts for vcl-ut. == Contents +`vclut-core.ipkg`:: + The machine-check package for the full `VclTotal` proof corpus. + `idris2 --build verification/proofs/vclut-core.ipkg` exits 0 over + **10 modules** (`ABI.{Types,Layout,LayoutProofs}` + + `Core.{Grammar,Schema,Decide,Levels,Checker,Composition,Epistemic}`) + under `%default total` with **zero proof-escape symbols**. The + `corpus/` subtree is a module→path symlink tree into `src/` (edits to + `src/**` are checked here verbatim). CI-gated by + `.github/workflows/proof-corpus.yml` (which also runs the + proof-escape audit and rebuilds `SafetyL4Model.idr`). Always + `rm -rf verification/proofs/build` before a local build (stale + `build/ttc` can yield a false green). + `SafetyL4Model.idr`:: Self-contained, idris2 0.8.0 `--check`-clean (exit 0, `%default total`, zero proof-escape symbols) model of the Level-4 SQL-injection safety @@ -16,16 +29,20 @@ This directory holds the *machine-verified* proof artefacts for vcl-ut. `VERIFICATION-STANCE.adoc`:: The authoritative, proof-backed statement of what is and is not verified. *Read this before trusting any "verified"/"type-safe" - phrasing elsewhere in the repo.* It documents that the shipped - `src/core/**` corpus does not compile on `origin/main` and has never - been machine-checked, and gives the phased remediation roadmap. + phrasing elsewhere in the repo.* It records the full Phase 0→4 + history (the Phase-0 corpus did not compile and was never + machine-checked; Phases 1–4 fixed that *honestly* — corpus compiles, + CI-gated, L1–L10 sound + dependent `SafetyCertificate`, FFI + fail-closed) and the precisely-scoped residual OWED items. == Verifying [source,sh] ---- export IDRIS2_PREFIX= -idris2 --check verification/proofs/SafetyL4Model.idr # expect exit 0 +rm -rf verification/proofs/build # avoid stale-ttc false green +idris2 --build verification/proofs/vclut-core.ipkg # expect exit 0 (10 modules) +cd verification/proofs && idris2 --check SafetyL4Model.idr # expect exit 0 ---- Tracked under hyperpolymath/standards#124. diff --git a/verification/proofs/VERIFICATION-STANCE.adoc b/verification/proofs/VERIFICATION-STANCE.adoc index e839ad2..b9ea21b 100644 --- a/verification/proofs/VERIFICATION-STANCE.adoc +++ b/verification/proofs/VERIFICATION-STANCE.adoc @@ -40,8 +40,9 @@ typecheck. The concrete blockers were: `Composition` (forward refs, deleted `AllParameterised` still referenced, wrong `CertL6+` arities, non-reducing `rewrite`s). -*Phase 1 + 2 + 3 status (RESOLVED):* every blocker above is fixed -*honestly* and the corpus compiles. **Phase 2** de-vacuized L2/L3/L5 +*Phase 1–4 status (RESOLVED):* every blocker above is fixed +*honestly* and the corpus compiles (10 modules; Phase 4 = `LayoutProofs` ++ L6–L10 `composeJoin` closure, PR #24). **Phase 2** de-vacuized L2/L3/L5 (new shared decider module `VclTotal.Core.Decide`, evidence-carrying predicates, `checkLevel2/3/5Sound`, genuine `composeJoin` closure). **Phase 3** added soundness for L1 and L6–L10 @@ -144,10 +145,26 @@ OWED section. Nat`) was *fixed* to `minus`. The sound content (the `safetyLevel`/`queryMode`/`vqlUtError` round-trip `Refl` proofs, the layout data, `Divides`/`alignUp`/`paddingFor`) remains and is now - machine-checked. *Carried OWED (Phase 3, precisely):* the genuine - alignment/no-padding theorems (`alignUp` divisibility via real - `div`/`mod` lemmas; fold field sizes = `totalSize`) and a - membership-quantified `offsetInBounds`. + machine-checked. *(Phase 4a — RESOLVED.)* The genuine + alignment/no-padding/bounds theorems are discharged in the new, + self-contained, CI-gated module `VclTotal.ABI.LayoutProofs` + (10th `vclut-core.ipkg` module; byte-identical `PField`/`qphFields` + model of `Layout.queryPlanHeaderLayout`): `alignToDivides` + (alignment divisibility *by construction* for the canonical + round-up-to-multiple form `alignTo size a = ⌈size/a⌉ * a` — witness + is the quotient, no `div`/`mod` lemma, no escape); + `queryPlanHeaderNoPadding` (fold of field sizes 4+4+4+4+8 = declared + cap 24, reduces under `Refl`); `queryPlanHeaderWithin` + + `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 @@ -189,11 +206,22 @@ OWED section. assemble them: a `Just` result *is* a machine-checked `SafetyCertificate stmt schema (requestedLevel stmt)`. `checkQuery` (the `Bool`/`CheckResult` C-ABI path) is retained unchanged. - *Carried OWED (Phase 3, precisely):* the L6–L10 *predicates* assert - only "the relevant clause/annotation is present" — real and - non-vacuous, but shallower than what `checkLevelN` additionally - enforces (L9 ≠ `LinUnlimited`; L10 declared agents + acyclic - `ENTAILS`); strengthening those predicates is future work. And the + *(Phase 4b — RESOLVED for join-closure.)* The L6–L10 predicates now + carry the shared `VclTotal.Core.Decide` deciders and are *genuinely + closed under `composeJoin`*, machine-checked: `l6/l7/l8/l9Compose` + (present-LIMIT / present-EFFECTS / present-VERSION join + all four + ENFORCED×ENFORCED `joinLinear` cases) and `epiStructJoin` for L10's + *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 + 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 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. @@ -304,6 +332,31 @@ OWED section. scoping. (A C ABI carrying a re-checkable dependent proof is *not* on this list — it is impossible by construction; the honest target is trusted-certifier attestation.) +. *Phase 4 (DONE in-corpus, this PR — discharges the Phase-3 "owed" + layout + join-closure debt):* + *(4a)* the genuine `ABI.Layout` alignment / no-padding / bounds + theorems, in the new self-contained CI-gated module + `VclTotal.ABI.LayoutProofs` (10th ipkg module): `alignToDivides` + (divisibility by construction for canonical ceil-multiple + alignment), `queryPlanHeaderNoPadding` (Σ field sizes = cap, reduces + under `Refl`), `fieldWithin` (membership-quantified bound via + `Vect.Elem` + `So.soAnd`). *Residual sliver:* additive↔ceil + `alignUp` equivalence for `a>0`, the documented `String` note + `alignUpAdditiveEquivOWED` — scoped, never faked. + *(4b)* L6–L10 genuinely closed under `composeJoin` + (`l6/l7/l8/l9Compose`, `epiStructJoin` via real superset + monotonicity); L10 acyclicity remains the explicit + `JoinSideCondition` (provably non-closed, in the type). No + `believe_me`/`postulate`/`assert_*`/`idris_crash`/`sorry`. + *Residual (carried):* deepen the L9/L10 *predicates* to full + `checkLevelN` semantics; FFI transport; the additive↔ceil sliver; + the unchanged Phase-3 string→`Statement`/marshalling/Idris→C items. + This residual is *tracked, not forgotten*: the boundary-reinforcement + workstream (FFI proof-attestation transport + the missing + `String -> Statement` parser, priority 1; the secondary items above) + is hyperpolymath/vcl-ut#25. A C ABI carrying a *re-checkable* + dependent proof is impossible by construction — the honest target + there is trusted-certifier attestation, stated not hidden. == Provenance @@ -314,7 +367,11 @@ L2/L3/L5 de-vacuized (new `VclTotal.Core.Decide`). Phase 3 2026-05-19: L1/L6–L10 soundness + `certifyAt`/`certifyRequested` dependent certificate + `ABI.Layout` made sound & gated; Phase 3d 2026-05-19: FFI fabricated-level lie deleted (fail-closed, `zig build test` green) + -proof-gated `Checker.certifiedLevel` mint. The corpus builds clean as +proof-gated `Checker.certifiedLevel` mint. Phase 4 2026-05-19: +`ABI.LayoutProofs` (genuine alignment/no-padding/bounds, 10th ipkg +module) + L6–L10 `composeJoin` closure (`l6..l9Compose`, +`epiStructJoin`); corpus rebuilt clean, 10 modules, zero proof-escape. +The corpus builds clean as *9 modules* (`idris2 0.8.0 --build verification/proofs/vclut-core.ipkg`, exit 0, `%default total`, zero proof-escape symbols — CI-enforced), the added diff --git a/verification/proofs/corpus/VclTotal/ABI/LayoutProofs.idr b/verification/proofs/corpus/VclTotal/ABI/LayoutProofs.idr new file mode 120000 index 0000000..30d3195 --- /dev/null +++ b/verification/proofs/corpus/VclTotal/ABI/LayoutProofs.idr @@ -0,0 +1 @@ +../../../../../src/interface/abi/LayoutProofs.idr \ No newline at end of file diff --git a/verification/proofs/vclut-core.ipkg b/verification/proofs/vclut-core.ipkg index 24c0f55..abd9cc0 100644 --- a/verification/proofs/vclut-core.ipkg +++ b/verification/proofs/vclut-core.ipkg @@ -29,6 +29,7 @@ sourcedir = "corpus" modules = VclTotal.ABI.Types , VclTotal.ABI.Layout + , VclTotal.ABI.LayoutProofs , VclTotal.Core.Grammar , VclTotal.Core.Schema , VclTotal.Core.Decide