From 843ab0f8dff3fc5f493704e08f991b385bc51adf Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:01:56 +0000 Subject: [PATCH 1/5] proof(actions-lock): Idris2 closure model with the corpus verdicts as equations MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit standards#963 criterion 5 left closure with Hypatia as the authority and a shared five-row corpus binding it to standards' close-lock.sh --check. That corpus is test evidence. This adds the formal half that PROOF-POLICY §1 assigns to an engineering property of one wire format: Idris2. verification/proofs/idris2/ActionsLockClosure.idr models a lock as its workflow refs plus its records (key, nested uses) over any type with decidable equality, and proves: - closedIffNoDangling: closed exactly when the dangling list is empty; - danglingSound / danglingComplete: the reported list is exactly the named refs without a record; - decClosed: closure is decidable. The five corpus rows are transcribed into the model and their verdicts are Refl equations (rowClosedV00x, rowClosedCaseVariant, rowDanglingNested, rowDanglingWorkflowRef). If expected.tsv and the model ever disagree, this file stops type-checking. PROOF-STATUS records three rows with honest tokens: - the model is OPEN until Verify Proofs' idris2 --check receipt is recorded (no idris2 in this session; the CI lane is the checker); - the Elixir and Bash implementations are TESTED against the corpus, with bounds (5 locks, 6 refs); - the owner/repo fold at the parse boundary is ASSUMED in the model and TESTED by closed-case-variant.lock. Runtime refinement is not claimed. Engineering proofs carry no PWG. scripts/check-proof-status.sh: 42 files, 77 identifiers, 0 mismatches. No believe_me / assert_total / postulate in the new file. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01TbbnKqskQA5mj5gfMniPzi --- verification/PROOF-STATUS.adoc | 50 ++++ .../proofs/idris2/ActionsLockClosure.idr | 230 ++++++++++++++++++ 2 files changed, 280 insertions(+) create mode 100644 verification/proofs/idris2/ActionsLockClosure.idr diff --git a/verification/PROOF-STATUS.adoc b/verification/PROOF-STATUS.adoc index ea95851c..1fc68f54 100644 --- a/verification/PROOF-STATUS.adoc +++ b/verification/PROOF-STATUS.adoc @@ -197,6 +197,52 @@ run 41328302925, job 124912804344, at commit 4018290eaa3265b82209e2a45b6917a4bb0 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+`). So the file stops type-checking if the model +and `+expected.tsv+` disagree. +|OPEN until the first `+idris2 --check+` receipt from Verify Proofs is +recorded here. + +|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 @@ -451,6 +497,10 @@ superseded 2026-11-01) |`+LogtalkMigration.agda+` |Finite model only — Grade 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..13503e76 --- /dev/null +++ b/verification/proofs/idris2/ActionsLockClosure.idr @@ -0,0 +1,230 @@ +-- 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 evaluated here: the +-- verdict and the exact dangling refs of each row are equations the type +-- checker reduces, so this file fails to check if the model and +-- test/fixtures/actions_lock/closure/expected.tsv ever disagree. +-- +-- 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. This is what +||| `close-lock.sh --check` prints and what Hypatia's error payload carries. +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. + +||| 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, [])] + +||| closed-case-variant.lock, after the fold. +public export +closedCaseVariant : Lock Nat +closedCaseVariant = MkLock [6] [(6, [])] + +||| dangling-nested.lock: the standards#963 shape. +public export +danglingNested : Lock Nat +danglingNested = MkLock [3] [(3, [4])] + +||| 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)) ) From 83c2334ea68a30a8ce8d8e74337b5632262349c1 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:02:26 +0000 Subject: [PATCH 2/5] =?UTF-8?q?docs(proofs):=20write=20grades=20as=20PWG?= =?UTF-8?q?=20per=20standards=20PROOF-POLICY=20=C2=A78?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The owner ruling of 2026-11-04 adopted the Mathesis grade ladder as standards' PROOF-POLICY §8, the normative source. That ruling forbids a bare "Grade 3" or "Grade 2" in a status line, because it collides with the CRG/TRG/ARG/FRG letter grades and with ECHIDNA's TrustLevel, which counts the other way. This file still cited the Mathesis brief as the definition and wrote "Grade 3" five times. - The policy bullet now cites §8 as normative and the brief as provenance. It states PWG-3, PWG-2i, PWG-2ii and PWG-1, says lower is stronger, and says engineering proofs carry §5 tokens only. - LogtalkMigration.agda is relabelled PWG-3 in its row, in P8 and in the coverage map. Its recorded receipt already met PWG-3: pinned Agda 2.8.0.2, the §2.1 flags, builtins only, success at a recorded commit. The import cone, builtins only with zero postulates under --safe, is now stated explicitly. No grade moved. scripts/check-proof-status.sh agrees with the tree. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01TbbnKqskQA5mj5gfMniPzi --- verification/PROOF-STATUS.adoc | 32 ++++++++++++++++++-------------- 1 file changed, 18 insertions(+), 14 deletions(-) diff --git a/verification/PROOF-STATUS.adoc b/verification/PROOF-STATUS.adoc index 1fc68f54..43b7bea1 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,10 +194,10 @@ 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. |=== @@ -424,7 +428,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. @@ -494,7 +498,7 @@ 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 From 71d116024954a0ef314c1e1910cbd11102fb1646 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:09:25 +0000 Subject: [PATCH 3/5] test(actions-lock): bind the Idris2 corpus transcription to the fixtures Codex review on #1026 raised two P2 findings: 1. The closure file claimed it would stop checking if the model and expected.tsv disagreed. Nothing tied its hand-transcribed rows to the fixtures or the table, so changing both together could leave every Refl green. The corpus test now reads the model file's ref table and its new `-- corpus: ` lines, and checks three things: - the model names exactly the corpus locks; - each fixture's workflow refs and records (with nested uses), after the owner/repo fold, equal its MkLock row; - each expected.tsv row equals the model's equation for that row. The type checker binds the equations to the model, so drift on either side now fails one of the two checks. 2. The doc comment on `dangling` said it is what Hypatia's error payload carries. That is false in general: ActionsLock checks workflow refs before nested uses, stops at the first failing phase, and reports (source, ref) pairs. The comment now says so. The model's list is the set close-lock.sh --check prints, and Hypatia reports a subset of it when a lock is missing refs of both kinds. PROOF-STATUS says the same. Verification, run standalone because hex.pm is unreachable: - the corpus test passes 17/17; - a mutant transcription (danglingNested's nested uses changed) fails exactly that row's edge test; - a mutant equation (danglingNested = [5]) fails exactly that row's equation test; - the formatter leaves the test unchanged; - check-proof-status.sh agrees with the tree. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01TbbnKqskQA5mj5gfMniPzi --- .../actions_lock_closure_corpus_test.exs | 106 ++++++++++++++++++ verification/PROOF-STATUS.adoc | 7 +- .../proofs/idris2/ActionsLockClosure.idr | 23 +++- 3 files changed, 128 insertions(+), 8 deletions(-) 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 43b7bea1..fbcca8f9 100644 --- a/verification/PROOF-STATUS.adoc +++ b/verification/PROOF-STATUS.adoc @@ -226,8 +226,11 @@ empty. The five corpus rows are evaluated as equations (`+rowClosedV00x+`, `+rowClosedCaseVariant+`, `+rowDanglingNested+`, -`+rowDanglingWorkflowRef+`). So the file stops type-checking if the model -and `+expected.tsv+` disagree. +`+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. |OPEN until the first `+idris2 --check+` receipt from Verify Proofs is recorded here. diff --git a/verification/proofs/idris2/ActionsLockClosure.idr b/verification/proofs/idris2/ActionsLockClosure.idr index 13503e76..7b84a950 100644 --- a/verification/proofs/idris2/ActionsLockClosure.idr +++ b/verification/proofs/idris2/ActionsLockClosure.idr @@ -13,10 +13,13 @@ -- 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 evaluated here: the --- verdict and the exact dangling refs of each row are equations the type --- checker reduces, so this file fails to check if the model and --- test/fixtures/actions_lock/closure/expected.tsv ever disagree. +-- 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, @@ -71,8 +74,11 @@ 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. This is what -||| `close-lock.sh --check` prints and what Hypatia's error payload carries. +||| 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 [] = [] @@ -165,22 +171,27 @@ decClosed l = case decEq (danglingOf l) [] of -- 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 From 693333a54649c206460ded8d12a5f8f3d7f84f3d Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:30:58 +0000 Subject: [PATCH 4/5] docs(proofs): record the idris2 --check receipt for ActionsLockClosure Verify Proofs run 42623006244, job 129179628830: Idris 2 0.7.0 (from source, Chez Scheme 10.0.0+dfsg-5build1) type-checked verification/proofs/idris2/ActionsLockClosure.idr under %default total, at source commit 71d1160, as the PR merge commit 8db0f43 on main c639c46. The model row moves from OPEN to PROVEN, model only; runtime refinement is still not claimed. The implementation rows stay TESTED and the parse-boundary row stays ASSUMED. Only this document changes. The .idr is byte-identical to the checked commit. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01TbbnKqskQA5mj5gfMniPzi --- verification/PROOF-STATUS.adoc | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/verification/PROOF-STATUS.adoc b/verification/PROOF-STATUS.adoc index fbcca8f9..54b92c2f 100644 --- a/verification/PROOF-STATUS.adoc +++ b/verification/PROOF-STATUS.adoc @@ -231,8 +231,15 @@ The five corpus rows are evaluated as equations 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. -|OPEN until the first `+idris2 --check+` receipt from Verify Proofs is -recorded here. +|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 ActionsLockClosure.idr+` 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 From cfe423d08b2588162af66b658a63eae18c7b925d Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:31:16 +0000 Subject: [PATCH 5/5] docs(proofs): keep the receipt's invocation out of the path checker check-proof-status.sh reads `+...+` spans that name a file as paths. The receipt wrote `+idris2 --check ActionsLockClosure.idr+`, which no tree path matches, so the currency check went red. The receipt now writes `+idris2 --check+` on this file. The check passes again: 42 files, 77 identifiers, 0 mismatches. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01TbbnKqskQA5mj5gfMniPzi --- verification/PROOF-STATUS.adoc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/verification/PROOF-STATUS.adoc b/verification/PROOF-STATUS.adoc index 54b92c2f..4bdf07d6 100644 --- a/verification/PROOF-STATUS.adoc +++ b/verification/PROOF-STATUS.adoc @@ -233,7 +233,7 @@ fixture's edges and every `+expected.tsv+` row against the model's 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 ActionsLockClosure.idr+` under +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