Merge pull request #360 from PhysShell/claude/p037-a1-guarded-transfer

P-037 A1.0 (bootstrap): port the formal kernel and controls onto post-cutover main; re-measure the pre-A1 record

Author: PhysShell

.github/workflows/ci.yml

@@ -72,6 +72,64 @@ jobs:
       - name: cargo test
         run: cargo test
 
+  # The P-037 formal kernel (formal/p037-kernel, docs/notes/p037-formal-kernel.md):
+  # its own workspace root, a member of nothing, wired to nothing — the pure
+  # guarded-transfer algebra checked twice over the same functions, by plain
+  # test twins and by Kani proof harnesses. The PR gate is fmt + clippy + the
+  # twins + the FAST harnesses (value-level laws, the G-A2 floor, the one-step
+  # lemmas; well under a minute of CBMC in total). The whole-solver harnesses
+  # take minutes each and run in formal-p037-gate.yml on a schedule / on
+  # demand — the owner's split after the A0 spike, so the inner loop never
+  # pays for a proof it does not need on every push.
+  #
+  # `toolchain: stable` here is deliberate and matches `rust-core` directly
+  # above. The pinned rustc that #262 Stage 3 requires is a property of
+  # action.yml — the CONSUMER-facing distribution surface, where a moving
+  # toolchain would move what users get — not of this repository's own CI,
+  # which is where a moving toolchain is supposed to break us first.
+  formal-p037:
+    name: formal kernel (fmt + clippy + twins + fast Kani)
+    runs-on: ubuntu-latest
+    defaults:
+      run:
+        working-directory: formal/p037-kernel
+    steps:
+      - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4
+      - uses: dtolnay/rust-toolchain@fa04a1451ff1842e2626ccb99004d0195b455a88 # master, 2026-07-10
+        with:
+          toolchain: stable
+          components: rustfmt, clippy
+      - name: cargo fmt --check
+        run: cargo fmt --check
+      - name: cargo clippy (the rust/ workspace lints, copied verbatim)
+        run: cargo clippy --all-targets
+      - name: cargo test (the exhaustive / randomized twins)
+        run: cargo test
+      - name: install Kani (pinned) and its toolchain bundle
+        run: |
+          cargo install --locked kani-verifier --version 0.68.0
+          cargo kani setup
+      - name: fast Kani harnesses (value-level laws, floor, one-step lemmas)
+        run: |
+          set -e
+          for h in \
+            k1_transfer_join_laws k1_transfer_order_is_a_partial_order k1_cells_join_laws \
+            k2_election_join_laws \
+            k3_reads_and_contributions_are_monotone \
+            k4_import_is_monotone_and_conflict_propagates \
+            k5_collapse_monotone_and_join_morphism \
+            k6_consume_only_through_a_selected_or_unanimous_must \
+            k7_no_fabricated_consume \
+            k8_involutions \
+            k9_residual_bottom_lemma_all_three_groundings \
+            k10a_step_is_monotone_in_the_state \
+            k10e_election_step_is_monotone_in_the_state \
+            k11_one_step_lax_simulation \
+            k12a_step_keeps_uncond_coordinates_diagonal; do
+            echo "== $h"
+            cargo kani --harness "$h"
+          done
+
   # P-022 step 7b (#261) — the production OwnIR executable's parity replay, on
   # BOTH platforms. The Python half of this contract is gated by the `tests`
   # matrix above (`tests/test_cli_ownir_fixtures.py` is auto-discovered like

.github/workflows/formal-p037-gate.yml

@@ -0,0 +1,51 @@
+name: formal-p037-gate
+
+# The heavy half of the P-037 formal kernel's proof harnesses
+# (formal/p037-kernel): the whole-solver statements — least fixpoint at the
+# full 3-coordinate bound, chaotic = Jacobi, the G-T2a lfp form, G-T2b, and
+# Uncond-stays-diagonal at the lfp. Minutes of CBMC each, ~15 minutes in all;
+# the owner's ruling after the A0 spike keeps them off the PR gate (ci.yml's
+# formal-p037 job runs the fast half on every push) and here, nightly and on
+# demand. A red run here is a real finding about the kernel or the contract,
+# never a flake to re-run: every harness is deterministic.
+
+permissions:
+  contents: read
+
+on:
+  schedule:
+    - cron: "17 3 * * *"
+  workflow_dispatch:
+
+jobs:
+  heavy-kani:
+    name: formal kernel (whole-solver Kani harnesses)
+    runs-on: ubuntu-latest
+    timeout-minutes: 90
+    defaults:
+      run:
+        working-directory: formal/p037-kernel
+    steps:
+      - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4
+      - uses: dtolnay/rust-toolchain@fa04a1451ff1842e2626ccb99004d0195b455a88 # master, 2026-07-10
+        with:
+          toolchain: stable
+      - name: install Kani (pinned) and its toolchain bundle
+        run: |
+          cargo install --locked kani-verifier --version 0.68.0
+          cargo kani setup
+      - name: whole-solver harnesses
+        run: |
+          set -e
+          for h in \
+            k10b_solve_is_a_fixpoint_below_every_fixpoint \
+            k10c_chaotic_equals_jacobi_on_small_sccs \
+            k10e_elect_is_a_fixpoint_below_every_fixpoint \
+            k10e_chaotic_equals_jacobi_on_small_sccs \
+            k11_lfp_lax_simulation_against_the_collapsed_system_on_small_sccs \
+            k11b_legacy_observational_compatibility_on_small_sccs \
+            k11_lfp_lax_simulation_against_today_post_finalization_on_small_sccs \
+            k12b_lfp_keeps_uncond_coordinates_diagonal_on_small_sccs; do
+            echo "== $h"
+            cargo kani --harness "$h"
+          done

corpus/p036-bakeoff/guarded-consume-early-return/after.cs

@@ -0,0 +1,22 @@
+// FIXED (synthetic conformance, P-037 §8 row 2). `keep: false` reaches the
+// Dispose on the only path -> clean.
+using System;
+using System.IO;
+
+static class GuardedEarlyReturn
+{
+    static void Close(Stream s, bool keep)
+    {
+        if (keep)
+            return;
+        s.Dispose();
+    }
+
+    static long Fine(string path)
+    {
+        var s = File.OpenRead(path);
+        long len = s.Length;
+        Close(s, keep: false);
+        return len;
+    }
+}

corpus/p036-bakeoff/guarded-consume-early-return/before.cs

@@ -0,0 +1,22 @@
+// BUGGY (synthetic conformance, P-037 §8 row 2 — the same guard spelled as an
+// early return; the two spellings must converge in a guarded summary).
+using System;
+using System.IO;
+
+static class GuardedEarlyReturn
+{
+    static void Close(Stream s, bool keep)
+    {
+        if (keep)
+            return;
+        s.Dispose();
+    }
+
+    static long Leak(string path)
+    {
+        var s = File.OpenRead(path);
+        long len = s.Length;
+        Close(s, keep: true);              // returns before the Dispose -> leak
+        return len;
+    }
+}

corpus/p036-bakeoff/guarded-consume-early-return/expected-diagnostics.txt

@@ -0,0 +1 @@
+OWN001

corpus/p036-bakeoff/guarded-consume-flag-branch/after.cs

@@ -0,0 +1,24 @@
+// FIXED (synthetic conformance, P-037 §8 row 1). The caller passes
+// `keep: false`, so `Close` disposes the stream on its only path: the
+// obligation moves into the helper and the caller must stay silent.
+using System;
+using System.IO;
+
+static class Guarded
+{
+    static void Close(Stream s, bool keep)
+    {
+        if (!keep)
+        {
+            s.Dispose();
+        }
+    }
+
+    static long Fine(string path)
+    {
+        var s = File.OpenRead(path);
+        long len = s.Length;
+        Close(s, keep: false);             // provably disposes -> clean
+        return len;
+    }
+}

corpus/p036-bakeoff/guarded-consume-flag-branch/before.cs

@@ -0,0 +1,29 @@
+// BUGGY (synthetic conformance, P-037 §8 row 1 — the SectorTS `Teardown(bool)`
+// shape on an IDisposable parameter).
+//
+// `Close(s, keep)` disposes its parameter ONLY when `keep == false`. The caller
+// passes `keep: true`, so the stream is never disposed on any path -> leak.
+// A context-insensitive summary can only say "may consume"; the guarded
+// summary of P-037 selects the `no` cell at this call site and keeps the
+// obligation with the caller.
+using System;
+using System.IO;
+
+static class Guarded
+{
+    static void Close(Stream s, bool keep)
+    {
+        if (!keep)
+        {
+            s.Dispose();
+        }
+    }
+
+    static long Leak(string path)
+    {
+        var s = File.OpenRead(path);
+        long len = s.Length;
+        Close(s, keep: true);              // provably does NOT dispose -> leak
+        return len;
+    }
+}

corpus/p036-bakeoff/guarded-consume-flag-branch/expected-diagnostics.txt

@@ -0,0 +1 @@
+OWN001

corpus/p036-bakeoff/guarded-consume-negation-wrapper/after.cs

@@ -0,0 +1,28 @@
+// FIXED (synthetic conformance, P-037 §8 row 8). `Outer(s, stop: true)` becomes
+// `Inner(s, keep: false)` -> disposed -> clean.
+using System;
+using System.IO;
+
+static class GuardedNegation
+{
+    static void Inner(Stream s, bool keep)
+    {
+        if (!keep)
+        {
+            s.Dispose();
+        }
+    }
+
+    static void Outer(Stream s, bool stop)
+    {
+        Inner(s, !stop);
+    }
+
+    static long Fine(string path)
+    {
+        var s = File.OpenRead(path);
+        long len = s.Length;
+        Outer(s, stop: true);
+        return len;
+    }
+}

corpus/p036-bakeoff/guarded-consume-negation-wrapper/before.cs

@@ -0,0 +1,28 @@
+// BUGGY (synthetic conformance, P-037 §8 row 8 — the wrapper NEGATES the flag
+// on the edge: `Inner(s, !stop)`; the cells swap).
+using System;
+using System.IO;
+
+static class GuardedNegation
+{
+    static void Inner(Stream s, bool keep)
+    {
+        if (!keep)
+        {
+            s.Dispose();
+        }
+    }
+
+    static void Outer(Stream s, bool stop)
+    {
+        Inner(s, !stop);                   // stop == false  =>  keep == true
+    }
+
+    static long Leak(string path)
+    {
+        var s = File.OpenRead(path);
+        long len = s.Length;
+        Outer(s, stop: false);             // Inner(s, keep: true) never disposes -> leak
+        return len;
+    }
+}