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

@@ -388,6 +388,63 @@ parse or carries no list passes 3.2.2 with no profile present
 (`+residualDivergence+`) |OPEN
 |===
 
+==== 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+`.
+|===
+
+
 === Properties Proven
 
 ==== 1. Confidence Bounds (`+ConfidenceBounds.idr+`)
@@ -540,9 +597,13 @@ inventory row above. These are properties of the model, not of the Elixir.
 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)