proof(actions-lock): Idris2 closure model with the corpus verdicts as equations

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: <fixture> <model row>`
+  defp model_corpus(src) do
+    Regex.scan(~r/^-- corpus: (\S+) (\w+)\s*$/m, src)
+    |> Map.new(fn [_, file, row] -> {file, row} end)
+  end
+
+  # `<row> = 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<Name> : danglingOf ActionsLockClosure.<row> = [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

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)