diff --git a/test/rules/actions_lock_closure_corpus_test.exs b/test/rules/actions_lock_closure_corpus_test.exs index 9f5bf0e6..0ff7f1ea 100644 --- a/test/rules/actions_lock_closure_corpus_test.exs +++ b/test/rules/actions_lock_closure_corpus_test.exs @@ -53,6 +53,112 @@ defmodule Hypatia.Rules.ActionsLockClosureCorpusTest do end end + # verification/proofs/idris2/ActionsLockClosure.idr transcribes this corpus + # into its model, numbering each ref, and proves each row's verdict as an + # equation. The type checker cannot read the fixtures, so these tests bind + # the transcription to them: every fixture's edges, and every expected.tsv + # row, must match the model row its `-- corpus:` line names. + @model "verification/proofs/idris2/ActionsLockClosure.idr" + @external_resource @model + + test "the Idris2 model names exactly the corpus locks" do + corpus = model_corpus(File.read!(@model)) + assert corpus |> Map.keys() |> Enum.sort() == @rows |> Enum.map(&elem(&1, 0)) |> Enum.sort() + end + + for {file, _verdict, _refs} <- @rows do + test "the Idris2 model transcribes the edges of #{file}" do + src = File.read!(@model) + numbering = model_numbering(src) + row = Map.fetch!(model_corpus(src), unquote(file)) + {workflow_refs, records} = model_lock(src, row) + + {fixture_refs, fixture_records} = + lock_edges(File.read!(Path.join(@dir, unquote(file))), numbering) + + assert Enum.sort(fixture_refs) == Enum.sort(workflow_refs) + assert fixture_records == records + end + end + + for {file, _verdict, refs} <- @rows do + test "the Idris2 equation for #{file} states its expected.tsv row" do + src = File.read!(@model) + numbering = model_numbering(src) + row = Map.fetch!(model_corpus(src), unquote(file)) + expected = Enum.map(unquote(refs), &Map.fetch!(numbering, ActionsLock.normalise_ref(&1))) + assert model_equation(src, row) == expected + end + end + + # `-- N owner/repo@ref`: the model's ref numbering, keyed after the fold. + defp model_numbering(src) do + Regex.scan(~r/^--\s+(\d+)\s+(\S+@\S+)\s*$/m, src) + |> Map.new(fn [_, n, ref] -> {ActionsLock.normalise_ref(ref), String.to_integer(n)} end) + end + + # `-- corpus: ` + defp model_corpus(src) do + Regex.scan(~r/^-- corpus: (\S+) (\w+)\s*$/m, src) + |> Map.new(fn [_, file, row] -> {file, row} end) + end + + # ` = MkLock [w, ...] [(k, [u, ...]), ...]` + defp model_lock(src, row) do + [_, wf, recs] = Regex.run(~r/^#{row} = MkLock \[([\d, ]*)\] \[(.*)\]\s*$/m, src) + + records = + Regex.scan(~r/\((\d+), \[([\d, ]*)\]\)/, recs) + |> Map.new(fn [_, k, uses] -> {String.to_integer(k), uses |> nats() |> Enum.sort()} end) + + {nats(wf), records} + end + + # `row : danglingOf ActionsLockClosure. = [n, ...]` + defp model_equation(src, row) do + [_, refs] = Regex.run(~r/: danglingOf ActionsLockClosure\.#{row} = \[([\d, ]*)\]/, src) + nats(refs) + end + + defp nats(list), + do: list |> String.split(",", trim: true) |> Enum.map(&String.to_integer(String.trim(&1))) + + # The edges a fixture names: every quoted ref under workflows:, and each + # dependency record with its nested uses:, mapped through the numbering. + defp lock_edges(content, numbering) do + id = &Map.fetch!(numbering, ActionsLock.normalise_ref(&1)) + + {_section, _key, refs, records} = + content + |> String.split("\n") + |> Enum.reduce({nil, nil, [], %{}}, fn line, {section, key, refs, records} -> + cond do + line == "workflows:" -> + {:workflows, nil, refs, records} + + line == "dependencies:" -> + {:dependencies, nil, refs, records} + + section == :workflows and Regex.match?(~r/^\s+- '/, line) -> + [_, ref] = Regex.run(~r/^\s+- '([^']+)'$/, line) + {section, key, [id.(ref) | refs], records} + + section == :dependencies and Regex.match?(~r/^ '[^']+':$/, line) -> + [_, ref] = Regex.run(~r/^ '([^']+)':$/, line) + {section, id.(ref), refs, Map.put(records, id.(ref), [])} + + section == :dependencies and Regex.match?(~r/^\s{12}- '/, line) -> + [_, ref] = Regex.run(~r/^\s+- '([^']+)'$/, line) + {section, key, refs, Map.update!(records, key, &Enum.sort([id.(ref) | &1]))} + + true -> + {section, key, refs, records} + end + end) + + {refs, records} + end + defp assert_verdict(result, "closed", []) do assert {:ok, %ActionsLock{}} = result end diff --git a/verification/PROOF-STATUS.adoc b/verification/PROOF-STATUS.adoc index ea95851c..4bdf07d6 100644 --- a/verification/PROOF-STATUS.adoc +++ b/verification/PROOF-STATUS.adoc @@ -27,15 +27,19 @@ neurosymbolic CI/CD platform. * Canonical estate policy: https://github.com/metadatastician/standards/blob/main/3-practice/PROOF-POLICY.adoc[Proof and Verification Policy]. This file is a proof inventory, not an independent alternative policy. -* Proof *grades* follow hyperpolymath/mathesis, - `+estate-mathematical-architecture+` §§5–6: *Grade 3* is an Agda proof - formulated and type-checking under the strict profile; *Grade 2* - requires translation(s) into independent foundational system(s); - *Grade 1* additionally requires those translated witnesses to compile - in headless, isolated CI via verified checker APIs. A target grade is - not a status. This inventory records exact statuses (Open / Claimed / - `+AGDA-PENDING+` / `+AGDA-VERIFIED+` / Grade 3 …) and never flattens - them into a confidence percentage. +* Proof grades are *Proof Witness Grades*, defined normatively in the + estate policy above, §8 (owner ruling 2026-11-04). The Mathesis brief + `+estate-mathematical-architecture+` §§5–6, which first proposed the + ladder, is provenance only. `+PWG-3+`: the Agda proof checks under the + §2.1 profile, with its import cone recorded. `+PWG-2i+` / `+PWG-2ii+`: + one or both Rocq/Lean recheck legs count, meaning kernel-checked and + `+RECONCILED+`. `+PWG-1+`: every counted witness has a current + per-commit receipt. Lower is stronger, and the `+PWG-+` prefix is always + written. PWG applies to theory theorems only; engineering proofs carry + the §5 tokens alone. A grade is derived from receipts and is not a + status. This inventory records statuses (`+AGDA-PENDING+` / + `+AGDA-VERIFIED+` …) and grades separately, and never flattens them + into a confidence percentage. * A checked model proves its stated proposition only. In particular it does not prove runtime refinement of Elixir/BEAM code; such claims need their own correspondence evidence and tests. @@ -170,7 +174,7 @@ JSONL for violations. See commit history. Finite, implementation-independent table correspondence for the retired ECHIDNA `+security_learning.lgt+` alert semantics versus `+Hypatia.Rules.SecurityErrors+`. Per the estate verifier mapping this -is Agda territory; per Mathesis this is now *Grade 3* on the +is Agda territory; under PROOF-POLICY §8 this is now `+PWG-3+` on the strict-profile receipt recorded in the row below (checker version, library discipline, exact invocation, result, source digest, and verification commit). Fix *strings* and Elixir @@ -190,13 +194,69 @@ entries; the two ledgered non-equalities stated exactly former severity catch-all members explicit (`+catchAllSastLow+`, `+catchAllCiTestsLow+`, `+catchAllUnmaintainedLow+`). Source SHA-256 (at authoring): bbd18e2747c84e2eda7ff5a778a2df7f8960a1ef47b1c253f316b9d97b9902a0. -|Grade 3 — AGDA-VERIFIED. Receipt: official pinned Agda 2.8.0.2 Linux +|`+PWG-3+` — AGDA-VERIFIED. Receipt: official pinned Agda 2.8.0.2 Linux release, builtins only/no stdlib; invocation `agda --safe --without-K --cubical-compatible LogtalkMigration.agda`; success in Verify Proofs -run 41328302925, job 124912804344, at commit 4018290eaa3265b82209e2a45b6917a4bb0a0331. No Grade 2/1, +run 41328302925, job 124912804344, at commit 4018290eaa3265b82209e2a45b6917a4bb0a0331. Import cone: Agda builtins only, zero postulates (`+--safe+`). No `+PWG-2i+`/`+PWG-2ii+`/`+PWG-1+`, reconciliation, or runtime-refinement claim. |=== +==== actions.lock closure (2026-11-09, standards#963 criterion 5) + +An engineering property of one wire format (`+actions.lock+`), so Idris2 +under PROOF-POLICY §1. Hypatia is the authority for closure (owner decision on +standards#963). `+scripts/close-lock.sh --check+` in hyperpolymath/standards +is a second implementation. The two share a five-row corpus, +`+test/fixtures/actions_lock/closure/+`, which is byte-identical to standards' +`+scripts/tests/fixtures/actions-lock-closure/+`. This is an engineering +proof, so it carries §5 tokens only and no PWG. + +[width="100%",cols="28%,14%,42%,16%",options="header",] +|=== +|File |Language |Properties stated |Status +|`+verification/proofs/idris2/ActionsLockClosure.idr+` |Idris2 +|The model is generic over refs with decidable equality, and its +statements are proved for that model: + +* `+closedIffNoDangling+`: closure holds exactly when the dangling list is +empty. +* `+danglingSound+`: every reported ref is named and has no record. +* `+danglingComplete+`: every named ref without a record is reported. +* `+decClosed+`: closure is decidable. + +The five corpus rows are evaluated as equations +(`+rowClosedV00x+`, `+rowClosedCaseVariant+`, `+rowDanglingNested+`, +`+rowDanglingWorkflowRef+`). The transcription is bound to its sources by +`+test/rules/actions_lock_closure_corpus_test.exs+`, which checks every +fixture's edges and every `+expected.tsv+` row against the model's +`+-- corpus:+` rows and ref table. A drift on either side turns that test or +this file's type check red. +|PROVEN (model only; runtime refinement not claimed). Receipt: Idris 2 +0.7.0 built from source on Chez Scheme 10.0.0+dfsg-5build1; +invocation `+idris2 --check+` on this file, under +`+%default total+`, with no `+believe_me+`, `+assert_total+` or +`+postulate+`; success in Verify Proofs run 42623006244, job +129179628830. The source was commit +71d116024954a0ef314c1e1910cbd11102fb1646, checked as the PR merge commit +8db0f43fbe8bd0b4a195b5d40736012c4f8d2a4b on main +c639c465e9bbbd01522f1eae12ac98a071afac13. + +|Elixir `+ActionsLock.parse/1+` and Bash `+close-lock.sh --check+` +against the model |ExUnit, Bash |Each implementation reproduces +`+expected.tsv+`: the verdict and the exact dangling refs. The tests are +`+test/rules/actions_lock_closure_corpus_test.exs+` and standards' +`+scripts/tests/close-lock-test.sh+`. +|TESTED. Bounds: 5 locks, 6 distinct refs, lockfile versions v0.0.2 and +v0.0.3. Each suite has a mutant that fails exactly one row. Runtime +refinement is not claimed. + +|Parse boundary: owner/repo folded to lowercase, ref kept exact +(`+ActionsLock.normalise_ref/1+`) |- |The model takes refs after the +fold. Its corpus rows are transcribed with the fold applied. +|ASSUMED in the model. TESTED in both implementations by +`+closed-case-variant.lock+`. +|=== + ==== Verdict support (2026-10-14, HYP-01) A gate verdict names its support: a pattern match, an observation count, or @@ -378,7 +438,7 @@ rejected ==== 8. Logtalk Migration Correspondence (`+LogtalkMigration.agda+`) -Status for all of P8: *Grade 3 — AGDA-VERIFIED* on the strict-profile +Status for all of P8: `+PWG-3+` — AGDA-VERIFIED, on the strict-profile receipt in the inventory row above (Agda 2.8.0.2, Verify Proofs run 41328302925, job 124912804344, commit 4018290eaa3265b82209e2a45b6917a4bb0a0331). This grades the finite model only. @@ -448,9 +508,13 @@ model only. superseded 2026-11-01) |Logtalk → Elixir alert-table correspondence -|`+LogtalkMigration.agda+` |Finite model only — Grade 3 / +|`+LogtalkMigration.agda+` |Finite model only — `+PWG-3+` / AGDA-VERIFIED (receipt above); fix text and runtime refinement excluded +|actions.lock closure |`+ActionsLockClosure.idr+` |Model only: decision +procedure and the five corpus verdicts; the implementations are TESTED +against the corpus, and runtime refinement is excluded + |Neural ensemble aggregation |`+NeuralConsensus.idr+` |Full (bounds + min-lower-bound) diff --git a/verification/proofs/idris2/ActionsLockClosure.idr b/verification/proofs/idris2/ActionsLockClosure.idr new file mode 100644 index 00000000..7b84a950 --- /dev/null +++ b/verification/proofs/idris2/ActionsLockClosure.idr @@ -0,0 +1,241 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- Hypatia — actions.lock closure model (standards#963, criterion 5) +-- +-- An actions.lock is CLOSED when every ref it names, under `workflows:` or in +-- a record's nested `uses:`, has a top-level record of its own. This module +-- states that property and proves a decision procedure for it: +-- +-- 1. `danglingNilOfAll` / `allOfDanglingNil`: the dangling list is empty +-- exactly when the lock is closed (`closedIffNoDangling`). +-- 2. `danglingSound`: every ref the dangling list reports is named by the +-- lock and has no record. +-- 3. `danglingComplete`: every named ref without a record is reported. +-- 4. `decClosed`: closure is decidable, by the dangling list. +-- 5. The five rows of the shared closure corpus are transcribed here, and +-- the verdict and exact dangling refs of each are equations the type +-- checker reduces. The transcription is bound to its sources by +-- test/rules/actions_lock_closure_corpus_test.exs. That test reads the +-- ref table and the `-- corpus:` lines below and checks every fixture's +-- edges and every expected.tsv row against them. So if the fixtures, +-- the table and this model ever disagree, one of the two checks fails. +-- +-- Corresponds to: lib/rules/actions_lock.ex (validate_workflow_dependencies, +-- validate_transitive_dependencies) and, in hyperpolymath/standards, +-- scripts/close-lock.sh --check. Both are tested against the same corpus. +-- +-- What this does NOT prove (recorded in verification/PROOF-STATUS.adoc): +-- * Runtime refinement. The Elixir and Bash implementations agree with this +-- model on the five corpus rows only (TESTED), not in general. +-- * The parse boundary. Refs are abstract values with decidable equality. +-- Folding owner/repo to lowercase while keeping the ref exact +-- (ActionsLock.normalise_ref/1) happens before this model, so the corpus +-- rows below are transcribed with the fold already applied (ASSUMED). + +module ActionsLockClosure + +import Data.List +import Data.List.Elem +import Data.List.Quantifiers +import Decidable.Equality + +%default total + +------------------------------------------------------------------------ +-- Section 1: The lock and its closure predicate +------------------------------------------------------------------------ + +||| A lock after parsing: the refs listed under `workflows:` (all workflows +||| flattened together) and the top-level records, each a key paired with +||| the refs in its nested `uses:`. +public export +record Lock a where + constructor MkLock + workflowRefs : List a + records : List (a, List a) + +||| The refs that have a top-level record. +public export +keys : Lock a -> List a +keys l = map fst (records l) + +||| Every ref the lock names: the workflow refs, then every nested `uses:`. +public export +edges : Lock a -> List a +edges l = workflowRefs l ++ concatMap snd (records l) + +||| A lock is closed when every ref it names has a record. +public export +Closed : Lock a -> Type +Closed l = All (\r => Elem r (keys l)) (edges l) + +------------------------------------------------------------------------ +-- Section 2: The dangling list +------------------------------------------------------------------------ + +||| The refs in `rs` that are not in `ks`, in order: the set that +||| `close-lock.sh --check` prints. Hypatia checks in two phases, workflow +||| refs first and then nested `uses:`, and reports `(source, ref)` pairs from +||| the first phase that fails. For a lock missing refs of both kinds it +||| therefore reports only the workflow ones, a subset of this list. +public export +dangling : DecEq a => List a -> List a -> List a +dangling ks [] = [] +dangling ks (r :: rs) with (isElem r ks) + _ | Yes _ = dangling ks rs + _ | No _ = r :: dangling ks rs + +||| If every ref has a record, nothing dangles. +export +danglingNilOfAll : DecEq a => (ks, rs : List a) -> + All (\r => Elem r ks) rs -> dangling ks rs = [] +danglingNilOfAll ks [] [] = Refl +danglingNilOfAll ks (r :: rs) (p :: ps) with (isElem r ks) + _ | Yes _ = danglingNilOfAll ks rs ps + _ | No np = void (np p) + +||| If nothing dangles, every ref has a record. +export +allOfDanglingNil : DecEq a => (ks, rs : List a) -> + dangling ks rs = [] -> All (\r => Elem r ks) rs +allOfDanglingNil ks [] _ = [] +allOfDanglingNil ks (r :: rs) prf with (isElem r ks) + _ | Yes p = p :: allOfDanglingNil ks rs prf + _ | No _ = absurd prf + +||| Every reported ref is named and has no record. +export +danglingSound : DecEq a => (ks, rs : List a) -> + Elem d (dangling ks rs) -> (Elem d rs, Not (Elem d ks)) +danglingSound ks [] e = absurd e +danglingSound ks (r :: rs) e with (isElem r ks) + danglingSound ks (r :: rs) e | Yes _ = + let (inRs, notKs) = danglingSound ks rs e in (There inRs, notKs) + danglingSound ks (r :: rs) Here | No np = (Here, np) + danglingSound ks (r :: rs) (There e') | No np = + let (inRs, notKs) = danglingSound ks rs e' in (There inRs, notKs) + +||| Every named ref without a record is reported. +export +danglingComplete : DecEq a => (ks, rs : List a) -> + Elem d rs -> Not (Elem d ks) -> Elem d (dangling ks rs) +danglingComplete ks [] e _ = absurd e +danglingComplete ks (r :: rs) Here nk with (isElem r ks) + _ | Yes p = void (nk p) + _ | No _ = Here +danglingComplete ks (r :: rs) (There e) nk with (isElem r ks) + _ | Yes _ = danglingComplete ks rs e nk + _ | No _ = There (danglingComplete ks rs e nk) + +------------------------------------------------------------------------ +-- Section 3: Closure is decided by the dangling list +------------------------------------------------------------------------ + +||| The dangling list of a lock: its edges without a record. +public export +danglingOf : DecEq a => Lock a -> List a +danglingOf l = dangling (keys l) (edges l) + +||| A lock is closed if and only if its dangling list is empty. +export +closedIffNoDangling : DecEq a => (l : Lock a) -> + (Closed l -> danglingOf l = [], danglingOf l = [] -> Closed l) +closedIffNoDangling l = + (danglingNilOfAll (keys l) (edges l), allOfDanglingNil (keys l) (edges l)) + +||| Closure is decidable. +export +decClosed : DecEq a => (l : Lock a) -> Dec (Closed l) +decClosed l = case decEq (danglingOf l) [] of + Yes nil => Yes (allOfDanglingNil (keys l) (edges l) nil) + No notNil => No (\c => notNil (danglingNilOfAll (keys l) (edges l) c)) + +------------------------------------------------------------------------ +-- Section 4: The shared closure corpus, row by row +------------------------------------------------------------------------ +-- +-- Each distinct ref of test/fixtures/actions_lock/closure/ is numbered, after +-- the owner/repo fold (ASSUMED, see the header): +-- +-- 1 example/build@1111111111111111111111111111111111111111 +-- 2 example/setup@2222222222222222222222222222222222222222 +-- 3 example/push-signed@3333333333333333333333333333333333333333 +-- 4 example/setup-python@v2 +-- 5 example/generator@4444444444444444444444444444444444444444 +-- 6 example/rust-cache@5555555555555555555555555555555555555555 +-- (closed-case-variant.lock spells the workflow ref Example/Rust-Cache; +-- the fold maps it to the record's key) +-- +-- A record's ref:, commit:, owner_id:, repo_id: and hostname: fields carry no +-- edges, so they are not modelled. An empty workflow (`empty.yml: []`) +-- contributes no edge. + +-- corpus: closed-v0.0.2.lock closedV00x +-- corpus: closed-v0.0.3.lock closedV00x +||| closed-v0.0.2.lock and closed-v0.0.3.lock (the same edges; v0.0.3 adds a +||| hostname, which carries no edge). +public export +closedV00x : Lock Nat +closedV00x = MkLock [1] [(1, [2]), (2, [])] + +-- corpus: closed-case-variant.lock closedCaseVariant +||| closed-case-variant.lock, after the fold. +public export +closedCaseVariant : Lock Nat +closedCaseVariant = MkLock [6] [(6, [])] + +-- corpus: dangling-nested.lock danglingNested +||| dangling-nested.lock: the standards#963 shape. +public export +danglingNested : Lock Nat +danglingNested = MkLock [3] [(3, [4])] + +-- corpus: dangling-workflow-ref.lock danglingWorkflowRef +||| dangling-workflow-ref.lock. +public export +danglingWorkflowRef : Lock Nat +danglingWorkflowRef = MkLock [1, 5] [(1, [])] + +||| expected.tsv rows `closed-v0.0.2.lock closed -` and +||| `closed-v0.0.3.lock closed -`. +export +rowClosedV00x : danglingOf ActionsLockClosure.closedV00x = [] +rowClosedV00x = Refl + +||| expected.tsv row `closed-case-variant.lock closed -`. +export +rowClosedCaseVariant : danglingOf ActionsLockClosure.closedCaseVariant = [] +rowClosedCaseVariant = Refl + +||| expected.tsv row `dangling-nested.lock dangling example/setup-python@v2`. +export +rowDanglingNested : danglingOf ActionsLockClosure.danglingNested = [4] +rowDanglingNested = Refl + +||| expected.tsv row +||| `dangling-workflow-ref.lock dangling example/generator@4444…`. +export +rowDanglingWorkflowRef : danglingOf ActionsLockClosure.danglingWorkflowRef = [5] +rowDanglingWorkflowRef = Refl + +||| The closed rows are closed, as proofs of the predicate itself. +export +closedRowsAreClosed : (Closed ActionsLockClosure.closedV00x, + Closed ActionsLockClosure.closedCaseVariant) +closedRowsAreClosed = + ( allOfDanglingNil (keys closedV00x) (edges closedV00x) rowClosedV00x + , allOfDanglingNil (keys closedCaseVariant) (edges closedCaseVariant) + rowClosedCaseVariant ) + +||| The dangling rows are not closed. +export +danglingRowsAreNotClosed : (Not (Closed ActionsLockClosure.danglingNested), + Not (Closed ActionsLockClosure.danglingWorkflowRef)) +danglingRowsAreNotClosed = + ( \c => absurd (trans (sym rowDanglingNested) + (danglingNilOfAll (keys danglingNested) + (edges danglingNested) c)) + , \c => absurd (trans (sym rowDanglingWorkflowRef) + (danglingNilOfAll (keys danglingWorkflowRef) + (edges danglingWorkflowRef) c)) )