<#
.SYNOPSIS
  wal-recovery-test.ps1 - rerunnable regression TEST for FIX #3-bis (WAL fold branch rule).

.DESCRIPTION
  Turns the hand-run W0.3 fault-injection (S120, run-folder W0-evidence 4.1/4.2) into a
  test that can be re-run. This is a TEST, not a detector: it EXITS NON-ZERO on failure
  (governance-detectors.ps1 is exit-0-always by mandate; this one is a gate for itself).

  RULE UNDER TEST (FIX #3-bis, spec v3-PATCH):
    K      = git rev-list --count origin/main..HEAD
    BOTTOM = git log --format=%s origin/main..HEAD | LAST line   (= OLDEST commit in range)
      K == 0             -> 'noop'          empty range: no reset, no rebase, commit straight
      BOTTOM starts wal: -> 'reset-soft'    ca1 (NONWAL=0) AND ca2 (NONWAL=1) - SAME handling
      else               -> 'rebase-fixup'  ca3 (bottom = ordinary commit)

    NONWAL IS NOT A BRANCH VARIABLE. Select-WalFoldBranch does not even ACCEPT it as a
    parameter - a structural anchor (asserted at runtime through Get-Command reflection,
    NOT through a grep over source text: a grep would self-match this comment block).

  WHY ca2 KILLS THE OLD RULE (spec v2 :92 branched on NONWAL==0):
    shape base|wal:|[CLAUDE] has NONWAL=1 -> old rule picks REBASE -> todo head = pick wal:
    -> fixup melts the top commit INTO the bottom one and INHERITS THE BOTTOM MESSAGE
    -> range still contains a 'wal:' commit -> push-guard blocks -> re-squash -> same result
    -> permanent STOP. The hazard is that it SUCCEEDS INCORRECTLY: exit 0, no rebase-merge
    residue, no trace. So a test asserting only 'exit code == 0' would PASS on the bug.

  ANTI-TAUTOLOGY ORACLE:
    The expected branch is NOT a restatement of the rule. For every case BOTH candidate
    branches are EXECUTED on independent throwaway trees and the post-state is MEASURED
    (count of 'wal:' commits left in origin/main..HEAD after the fold + re-commit):
      exactly one candidate CLEAN -> expectation is EMPIRICAL (measured, not asserted)
      both candidates CLEAN       -> oracle INCONCLUSIVE -> falls back to the spec-stated
                                     expectation, and the table SAYS SO (honest label)
    ca1/ca2 are EMPIRICAL. ca0/ca3 are DEFINITIONAL - declared, not hidden.

  REGRESSION-GUARD (the real value): at ca2 the test asserts the SUT picks the branch this
  very run MEASURED to be clean, and that the legacy rule picks the branch this very run
  MEASURED to deadlock. Flip Select-WalFoldBranch back to NONWAL-branching and ca2 FAILS.
  Verify the teeth with -InjectLegacyRule (must exit non-zero).

.PARAMETER RepoRoot
  Repo root. Used as a CONTAINMENT ORACLE only: this test must never touch the real .git.
  Containment is proven STRUCTURALLY - every path this script writes derives from -WorkDir,
  and -WorkDir is asserted to sit outside RepoRoot. The RepoRoot HEAD + porcelain snapshot is
  printed as corroboration but deliberately NOT asserted: in a concurrent multi-agent wave a
  sibling lane or the WAL Stop-hook can legitimately move both mid-run, so asserting on them
  would fail for exogenous reasons (a flaky gate is worse than no gate). No repo file is read
  as test material - the trees are synthesized from scratch.

.PARAMETER WorkDir
  Parent dir for the throwaway git trees. Default = $env:TEMP.

.PARAMETER KeepTemp
  Keep the throwaway trees for inspection instead of deleting them.

.PARAMETER InjectLegacyRule
  FAULT-INJECTION SELF-TEST. Swaps the SUT for the legacy NONWAL rule. Expected result:
  ca2 FAILS and the script exits non-zero. Proves this test is not vacuously green.

.EXAMPLE
  powershell.exe -ExecutionPolicy Bypass -File scripts/wal-recovery-test.ps1
  powershell.exe -ExecutionPolicy Bypass -File scripts/wal-recovery-test.ps1 -InjectLegacyRule
#>
param(
    [string]$RepoRoot = (Resolve-Path (Join-Path $PSScriptRoot '..')).Path,
    [string]$WorkDir = $env:TEMP,
    [switch]$KeepTemp,
    [switch]$InjectLegacyRule
)

$ErrorActionPreference = 'Continue'

# ---------------------------------------------------------------------------
# Result plumbing
# ---------------------------------------------------------------------------
$script:AssertCount = 0
$script:FailCount = 0
$script:CaseFail = @{}
# PRE-fold measurement per case, captured from real git BEFORE any surgery. The guard
# below must reuse THIS, never re-measure a main tree that has already been folded.
$script:CaseMeasure = @{}
$script:Rows = New-Object System.Collections.Generic.List[object]

function Write-Section($title) {
    Write-Host ''
    Write-Host ("===== $title =====") -ForegroundColor Cyan
}

function Assert-That {
    param([string]$CaseId, [string]$Name, [bool]$Ok, [string]$Detail)
    $script:AssertCount++
    if ($Ok) {
        Write-Host ("  [PASS] {0,-4} | {1,-26} | {2}" -f $CaseId, $Name, $Detail) -ForegroundColor Green
    }
    else {
        Write-Host ("  [FAIL] {0,-4} | {1,-26} | {2}" -f $CaseId, $Name, $Detail) -ForegroundColor Red
        $script:FailCount++
        $script:CaseFail[$CaseId] = $true
    }
}

# ---------------------------------------------------------------------------
# RULE UNDER TEST (SUT) - FIX #3-bis
# Branch variable = BOTTOM of range (+ K for the empty case). NONWAL absent BY DESIGN:
# once the bottom is 'wal:', reset --soft is correct for NONWAL=0 and NONWAL>0 alike,
# so NONWAL cannot change the handling and must not select the branch.
# ---------------------------------------------------------------------------
function Select-WalFoldBranch {
    param([int]$K, [string]$Bottom)
    if ($K -eq 0) { return 'noop' }
    if ($Bottom -match '^wal:') { return 'reset-soft' }
    return 'rebase-fixup'
}

# LEGACY rule (spec v2 :92). Kept ONLY as the regression oracle - never as the SUT
# unless -InjectLegacyRule is passed to prove this test has teeth.
function Select-WalFoldBranchLegacy {
    param([int]$Nonwal)
    if ($Nonwal -eq 0) { return 'reset-soft' }
    return 'rebase-fixup'
}

function Get-FoldBranch {
    param([int]$K, [string]$Bottom, [int]$Nonwal)
    if ($InjectLegacyRule) { return (Select-WalFoldBranchLegacy -Nonwal $Nonwal) }
    return (Select-WalFoldBranch -K $K -Bottom $Bottom)
}

# ---------------------------------------------------------------------------
# git helpers - every path derives from $WorkDir / $RepoRoot, none hardcoded.
# ---------------------------------------------------------------------------
$script:SeqEditor = $null

function New-SeqEditor {
    param([string]$Dir)
    # Sequence editor: keep the FIRST pick, turn every later pick into fixup.
    # Written with LF + no BOM so the git todo parser sees clean lines.
    $p = Join-Path $Dir 'wal-test-seq-editor.ps1'
    $body = @(
        'param($TodoPath)',
        '$lines = Get-Content -LiteralPath $TodoPath',
        '$seen = $false',
        '$out = New-Object System.Collections.Generic.List[string]',
        'foreach ($l in $lines) {',
        '    if ($l -match "^pick ") {',
        '        if ($seen) { $out.Add(($l -replace "^pick ", "fixup ")) }',
        '        else { $seen = $true; $out.Add($l) }',
        '    } else { $out.Add($l) }',
        '}',
        '[System.IO.File]::WriteAllText($TodoPath, (($out -join "`n") + "`n"))',
        'exit 0'
    ) -join "`n"
    [System.IO.File]::WriteAllText($p, $body)
    return $p
}

function New-CaseTree {
    param([string]$Path, [string[]]$Shape)
    if (Test-Path $Path) { Remove-Item -Recurse -Force -LiteralPath $Path }
    New-Item -ItemType Directory -Path $Path -Force | Out-Null
    Push-Location $Path
    git init -q .
    git config user.email 'wal-test@local'
    git config user.name 'wal-test'
    git config commit.gpgsign false
    git config core.autocrlf false
    # Isolate from any inherited hook path: a stray hook must not edit these trees.
    git config core.hooksPath (Join-Path $Path '.git/no-such-hooks')
    [System.IO.File]::WriteAllText((Join-Path $Path 'base.txt'), "base`n")
    git add -- base.txt
    git commit -q -m '[CLAUDE] Infra: base'
    # Fake origin/main as a LOCAL ref - no network, no real remote.
    git update-ref refs/remotes/origin/main HEAD
    $n = 0
    foreach ($subject in $Shape) {
        $n++
        [System.IO.File]::WriteAllText((Join-Path $Path "f$n.txt"), "content $n`n")
        git add -- "f$n.txt"
        git commit -q -m $subject
    }
    Pop-Location
}

function Measure-Range {
    param([string]$Path)
    Push-Location $Path
    $k = [int](git rev-list --count origin/main..HEAD)
    $log = @(git log --format=%s origin/main..HEAD)
    Pop-Location
    $bottom = ''
    if ($log.Count -gt 0) { $bottom = $log[-1] }
    return [pscustomobject]@{
        K      = $k
        Bottom = $bottom
        Nonwal = @($log | Where-Object { -not ($_ -match '^wal:') }).Count
        Nwal   = @($log | Where-Object { $_ -match '^wal:' }).Count
        Log    = $log
    }
}

function Get-RefSnapshot {
    param([string]$Path)
    Push-Location $Path
    $s = @(git for-each-ref --format='%(refname) %(objectname)') -join '|'
    $h = (git rev-parse HEAD)
    Pop-Location
    return ("HEAD=$h REFS=$s")
}

# Executes one fold branch on $Path. Returns what was MEASURED, asserts nothing.
function Invoke-FoldBranch {
    param([string]$Path, [string]$Branch, [int]$K)

    $r = [pscustomobject]@{
        Branch        = $Branch
        RebaseInvoked = $false
        RebaseExit    = $null
        ResetInvoked  = $false
        HeadKEqOrigin = $null
        StateLeft     = $false
        Error         = ''
    }
    Push-Location $Path

    if ($Branch -eq 'noop') {
        # ca0: deliberately do NOTHING. No reset, no rebase.
    }
    elseif ($Branch -eq 'reset-soft') {
        # Safety assert BEFORE touching anything (v2 W0.3 gate).
        $a = (git rev-parse "HEAD~$K")
        $b = (git rev-parse origin/main)
        $r.HeadKEqOrigin = ($a -eq $b)
        if ($r.HeadKEqOrigin) {
            $r.ResetInvoked = $true
            git reset --soft "HEAD~$K" | Out-Null
            git diff --cached --quiet
            if ($LASTEXITCODE -ne 0) { git commit -q -m '[CLAUDE] Infra: fold re-commit' }
        }
        else {
            $r.Error = 'ABORT: HEAD~K != origin/main'
        }
    }
    elseif ($Branch -eq 'rebase-fixup') {
        $env:GIT_SEQUENCE_EDITOR = ('powershell.exe -NoProfile -ExecutionPolicy Bypass -File "' + $script:SeqEditor + '"')
        # Hang-guard: never let git open an interactive message editor.
        $env:GIT_EDITOR = 'powershell.exe -NoProfile -Command exit 0'
        $r.RebaseInvoked = $true
        git rebase -i origin/main 2>$null | Out-Null
        $r.RebaseExit = $LASTEXITCODE
        if ($r.RebaseExit -ne 0) { git rebase --abort 2>$null | Out-Null }
        $env:GIT_SEQUENCE_EDITOR = $null
        $env:GIT_EDITOR = $null
    }

    # Rebase-state residue check after EVERY step, on every branch.
    $r.StateLeft = ((Test-Path '.git/rebase-merge') -or (Test-Path '.git/rebase-apply'))
    Pop-Location
    return $r
}

# Runs a candidate branch on a FRESH tree and reports the measured outcome.
function Test-Candidate {
    param([string]$Root, [string]$Id, [string[]]$Shape, [string]$Branch)
    $p = Join-Path $Root $Id
    New-CaseTree -Path $p -Shape $Shape
    $pre = Measure-Range -Path $p
    $exec = Invoke-FoldBranch -Path $p -Branch $Branch -K $pre.K
    $post = Measure-Range -Path $p
    $outcome = 'CLEAN'
    if ($post.Nwal -gt 0) { $outcome = 'DEADLOCK' }
    return [pscustomobject]@{
        Branch = $Branch; Exec = $exec; Post = $post; Outcome = $outcome; Path = $p
    }
}

# ---------------------------------------------------------------------------
# Bootstrap + containment
# ---------------------------------------------------------------------------
Write-Section 'setup + containment (RepoRoot must stay untouched)'

$stamp = (Get-Date -Format 'yyyyMMddTHHmmss')
$root = Join-Path $WorkDir ("wal-recovery-test-" + $stamp)
New-Item -ItemType Directory -Path $root -Force | Out-Null
$script:SeqEditor = New-SeqEditor -Dir $root

Write-Host ("  RepoRoot = {0}" -f $RepoRoot)
Write-Host ("  WorkDir  = {0}" -f $root)
if ($InjectLegacyRule) {
    Write-Host '  MODE     = FAULT-INJECT (-InjectLegacyRule): SUT swapped to legacy NONWAL rule.' -ForegroundColor Magenta
    Write-Host '             EXPECTED RESULT = ca2 FAIL + non-zero exit.' -ForegroundColor Magenta
}

# Containment (a) HARD ASSERT: every tree this script builds hangs off $root, so proving
# $root is outside RepoRoot proves the real .git is unreachable. Structural, not flaky.
$rrFull = ($RepoRoot -replace '/', '\').TrimEnd('\')
$wdFull = ($root -replace '/', '\')
Assert-That 'env' 'workdir-outside-repo' (-not $wdFull.StartsWith(($rrFull + '\'), [StringComparison]::OrdinalIgnoreCase)) `
    ("WorkDir not under RepoRoot -> real .git cannot be reached")

# Containment (b) INFO ONLY: snapshot the real repo, re-printed at the end. NOT asserted -
# see .PARAMETER RepoRoot: concurrent lanes / the WAL Stop-hook move these legitimately.
$repoIsGit = Test-Path (Join-Path $RepoRoot '.git')
$repoHeadBefore = 'n/a'
$repoDirtyBefore = -1
if ($repoIsGit) {
    $repoHeadBefore = (git -C $RepoRoot rev-parse HEAD)
    $repoDirtyBefore = @(git -C $RepoRoot status --porcelain).Count
    Write-Host ("  RepoRoot HEAD before = {0} ; porcelain entries = {1}" -f $repoHeadBefore, $repoDirtyBefore)
}
else {
    Write-Host '  [note] RepoRoot is not a git repo - containment (b) reduced to path check only' -ForegroundColor DarkGray
}

# Structural anchor: the SUT must not be ABLE to branch on NONWAL.
$sutParams = @((Get-Command Select-WalFoldBranch).Parameters.Keys)
$hasNonwal = $false
foreach ($pn in $sutParams) { if ($pn -match '(?i)nonwal') { $hasNonwal = $true } }
Assert-That 'env' 'sut-has-no-NONWAL-param' (-not $hasNonwal) `
    ("Select-WalFoldBranch params = [{0}] (structural, via Get-Command - not a source grep)" -f ($sutParams -join ', '))

# ---------------------------------------------------------------------------
# The 4 cases. Shape = commits laid on top of base, BOTTOM-FIRST.
# ---------------------------------------------------------------------------
$WAL1 = 'wal: flush 1'
$WAL2 = 'wal: flush 2'
$REAL = '[CLAUDE] Infra: real work'

$cases = @(
    [pscustomobject]@{ Id = 'ca0'; Shape = @();                Label = 'base';                SpecBranch = 'noop' },
    [pscustomobject]@{ Id = 'ca1'; Shape = @($WAL1, $WAL2);    Label = 'base|wal:|wal:';      SpecBranch = 'reset-soft' },
    [pscustomobject]@{ Id = 'ca2'; Shape = @($WAL1, $REAL);    Label = 'base|wal:|[CLAUDE]';  SpecBranch = 'reset-soft' },
    [pscustomobject]@{ Id = 'ca3'; Shape = @($REAL, $WAL1);    Label = 'base|[CLAUDE]|wal:';  SpecBranch = 'rebase-fixup' }
)

foreach ($c in $cases) {
    $script:CaseFail[$c.Id] = $false
    Write-Section ("{0} : {1}" -f $c.Id, $c.Label)

    # --- 1. build the tree and MEASURE the branch inputs from real git ---
    $main = Join-Path $root ($c.Id + '-main')
    New-CaseTree -Path $main -Shape $c.Shape
    $m = Measure-Range -Path $main
    $script:CaseMeasure[$c.Id] = $m
    Write-Host ("  measured: K={0} NONWAL={1} BOTTOM=[{2}]" -f $m.K, $m.Nonwal, $m.Bottom)
    foreach ($l in $m.Log) { Write-Host ("    range: {0}" -f $l) -ForegroundColor DarkGray }

    $sut = Get-FoldBranch -K $m.K -Bottom $m.Bottom -Nonwal $m.Nonwal
    $legacy = Select-WalFoldBranchLegacy -Nonwal $m.Nonwal
    Write-Host ("  SUT picks   = {0}" -f $sut)
    Write-Host ("  legacy rule = {0}   (branches on NONWAL - spec v2 :92)" -f $legacy)

    # --- 2. ORACLE: execute BOTH candidates on independent trees, measure outcome ---
    $cfReset = Test-Candidate -Root $root -Id ($c.Id + '-cf-reset') -Shape $c.Shape -Branch 'reset-soft'
    $cfRebase = Test-Candidate -Root $root -Id ($c.Id + '-cf-rebase') -Shape $c.Shape -Branch 'rebase-fixup'
    Write-Host ("  counterfactual reset-soft   -> n(wal: in range)={0} -> {1}" -f $cfReset.Post.Nwal, $cfReset.Outcome)
    Write-Host ("  counterfactual rebase-fixup -> n(wal: in range)={0} -> {1}  [rebase-exit={2}]" -f `
            $cfRebase.Post.Nwal, $cfRebase.Outcome, $cfRebase.Exec.RebaseExit)

    $clean = @()
    if ($cfReset.Outcome -eq 'CLEAN') { $clean += 'reset-soft' }
    if ($cfRebase.Outcome -eq 'CLEAN') { $clean += 'rebase-fixup' }

    $oracleKind = 'DEFINITIONAL'
    $expected = $c.SpecBranch
    if ($c.Id -ne 'ca0' -and $clean.Count -eq 1) {
        $oracleKind = 'EMPIRICAL'
        $expected = $clean[0]
    }
    if ($oracleKind -eq 'EMPIRICAL') {
        Write-Host ("  ORACLE = EMPIRICAL: exactly one candidate survives the push-guard -> expected={0}" -f $expected) -ForegroundColor Yellow
    }
    else {
        Write-Host ("  ORACLE = DEFINITIONAL: both candidates outcome-equivalent on the n(wal:) metric") -ForegroundColor DarkGray
        Write-Host ("           -> expected={0} taken from spec v3-PATCH, NOT measured. Declared, not hidden." -f $expected) -ForegroundColor DarkGray
    }

    # --- 3. execute the SUT-chosen branch on the main tree ---
    $snapBefore = Get-RefSnapshot -Path $main
    $exec = Invoke-FoldBranch -Path $main -Branch $sut -K $m.K
    $snapAfter = Get-RefSnapshot -Path $main
    $post = Measure-Range -Path $main

    # --- 4. asserts ---
    Assert-That $c.Id 'branch-selection' ($sut -eq $expected) `
        ("SUT={0} expected={1} ({2} oracle)" -f $sut, $expected, $oracleKind)

    Assert-That $c.Id 'no-rebase-state-left' (-not $exec.StateLeft) `
        ('.git/rebase-merge + .git/rebase-apply ABSENT after the step')
    Assert-That $c.Id 'cf-no-rebase-state' ((-not $cfReset.Exec.StateLeft) -and (-not $cfRebase.Exec.StateLeft)) `
        ('.git/rebase-merge ABSENT on BOTH counterfactual trees too')

    # REBASE-EXIT is never non-zero - on the main tree AND on the counterfactual that rebased.
    $rebaseExits = @()
    if ($null -ne $exec.RebaseExit) { $rebaseExits += $exec.RebaseExit }
    if ($null -ne $cfRebase.Exec.RebaseExit) { $rebaseExits += $cfRebase.Exec.RebaseExit }
    $badExit = @($rebaseExits | Where-Object { $_ -ne 0 }).Count
    Assert-That $c.Id 'rebase-exit-never-nonzero' ($badExit -eq 0) `
        ("rebase exits observed = [{0}] ; non-zero count = {1}" -f (($rebaseExits | ForEach-Object { "$_" }) -join ','), $badExit)

    if ($sut -eq 'reset-soft') {
        Assert-That $c.Id 'headK-eq-origin-pre-reset' ($exec.HeadKEqOrigin -eq $true) `
            ("HEAD~K == origin/main asserted BEFORE reset (K={0})" -f $m.K)
    }

    if ($c.Id -eq 'ca0') {
        Assert-That $c.Id 'noop-touched-nothing' ((-not $exec.ResetInvoked) -and (-not $exec.RebaseInvoked)) `
            ('no reset, no rebase issued on an empty range')
        Assert-That $c.Id 'git-tree-identical' ($snapBefore -eq $snapAfter) `
            ('.git ref-state byte-identical before/after')
    }

    if ($c.Id -eq 'ca2') {
        # v3-PATCH acceptance: ca2 must not touch git rebase AT ALL.
        Assert-That $c.Id 'ca2-never-rebases' (-not $exec.RebaseInvoked) `
            ('git rebase NOT invoked on ca2')
    }

    if ($oracleKind -eq 'EMPIRICAL') {
        Assert-That $c.Id 'post-state-clean' ($post.Nwal -eq 0) `
            ("n(wal: in origin/main..HEAD) after SUT branch = {0}" -f $post.Nwal)
    }

    $verdict = 'PASS'
    if ($script:CaseFail[$c.Id]) { $verdict = 'FAIL' }
    $script:Rows.Add([pscustomobject]@{
            Case = $c.Id; Shape = $c.Label; K = $m.K; Nonwal = $m.Nonwal
            Sut = $sut; Legacy = $legacy; Expected = $expected; Oracle = $oracleKind; Verdict = $verdict
        })
}

# ---------------------------------------------------------------------------
# REGRESSION-GUARD - the actual value of this script.
# Not a restatement of the rule: both claims below are MEASURED this run.
# ---------------------------------------------------------------------------
Write-Section 'REGRESSION-GUARD (ca2) - legacy NONWAL rule must stay rejected'

$c2 = $cases | Where-Object { $_.Id -eq 'ca2' }
$g1 = Test-Candidate -Root $root -Id 'guard-ca2-legacy' -Shape $c2.Shape -Branch 'rebase-fixup'
# PRE-fold inputs of ca2, captured from real git in the loop above. Re-measuring
# ca2-main here would read the ALREADY-FOLDED tree (K=1, bottom = the re-commit) and
# silently ask the rule a different question than the one under test.
$m2 = $script:CaseMeasure['ca2']

Write-Host '  Replay of W0.3 4.2 - legacy branch (rebase+fixup) executed on a ca2 tree:'
Write-Host ("    rebase-exit           = {0}   (0 = it SUCCEEDS, which is exactly the hazard)" -f $g1.Exec.RebaseExit)
Write-Host ("    rebase-state left     = {0}" -f $g1.Exec.StateLeft)
foreach ($l in $g1.Post.Log) { Write-Host ("    after: {0}" -f $l) -ForegroundColor DarkGray }
Write-Host ("    n(wal: in range)      = {0}" -f $g1.Post.Nwal)

# Fixed-point probe: re-folding the deadlocked range never escapes it.
$g2 = $null
if ($g1.Post.Nwal -gt 0) {
    $g2 = Invoke-FoldBranch -Path $g1.Path -Branch 'rebase-fixup' -K $g1.Post.K
    $after2 = Measure-Range -Path $g1.Path
    Write-Host ("    re-squash (2nd fold)  -> n(wal:)={0}  [rebase-exit={1}] -> fixed point = PERMANENT STOP" -f `
            $after2.Nwal, $g2.RebaseExit)
    Assert-That 'grd' 'deadlock-is-fixed-point' ($after2.Nwal -gt 0) `
        ('re-squashing the legacy result still leaves a wal: commit -> push-guard blocks forever')
}

Assert-That 'grd' 'legacy-branch-deadlocks' (($g1.Exec.RebaseExit -eq 0) -and ($g1.Post.Nwal -gt 0)) `
    ("MEASURED: legacy branch exits 0 yet leaves n(wal:)={0} -> succeeds INCORRECTLY" -f $g1.Post.Nwal)

$legacyCa2 = Select-WalFoldBranchLegacy -Nonwal $m2.Nonwal
$sutCa2 = Get-FoldBranch -K $m2.K -Bottom $m2.Bottom -Nonwal $m2.Nonwal

Assert-That 'grd' 'legacy-picks-the-bad-one' ($legacyCa2 -eq 'rebase-fixup') `
    ("legacy(NONWAL={0}) = {1} = the branch measured to deadlock" -f $m2.Nonwal, $legacyCa2)
Assert-That 'grd' 'sut-rejects-legacy-branch' ($sutCa2 -ne 'rebase-fixup') `
    ("SUT = {0} != the measured-deadlock branch. Revert the rule to NONWAL and THIS assert fails." -f $sutCa2)
Assert-That 'grd' 'rules-diverge-at-ca2' ($sutCa2 -ne $legacyCa2) `
    ("SUT={0} vs legacy={1} - divergence is what makes this guard non-vacuous" -f $sutCa2, $legacyCa2)

# ---------------------------------------------------------------------------
# Result table
# ---------------------------------------------------------------------------
Write-Section 'RESULT'

Write-Host ('{0,-5} {1,-22} {2,-3} {3,-7} {4,-13} {5,-13} {6,-13} {7,-13} {8}' -f `
        'CASE', 'SHAPE', 'K', 'NONWAL', 'SUT', 'LEGACY', 'EXPECTED', 'ORACLE', 'VERDICT')
Write-Host ('-' * 118)
foreach ($r in $script:Rows) {
    $col = 'Green'
    if ($r.Verdict -eq 'FAIL') { $col = 'Red' }
    Write-Host ('{0,-5} {1,-22} {2,-3} {3,-7} {4,-13} {5,-13} {6,-13} {7,-13} {8}' -f `
            $r.Case, $r.Shape, $r.K, $r.Nonwal, $r.Sut, $r.Legacy, $r.Expected, $r.Oracle, $r.Verdict) -ForegroundColor $col
}

$passCases = @($script:Rows | Where-Object { $_.Verdict -eq 'PASS' }).Count
$totalCases = $script:Rows.Count

# Containment (b) re-check - INFO, never a verdict input (concurrency-exogenous).
Write-Host ''
if ($repoIsGit) {
    $repoHeadAfter = (git -C $RepoRoot rev-parse HEAD)
    $repoDirtyAfter = @(git -C $RepoRoot status --porcelain).Count
    $same = (($repoHeadAfter -eq $repoHeadBefore) -and ($repoDirtyAfter -eq $repoDirtyBefore))
    Write-Host ("  [info] RepoRoot HEAD {0} -> {1} ; porcelain {2} -> {3} ; unchanged={4}" -f `
            $repoHeadBefore.Substring(0, 7), $repoHeadAfter.Substring(0, 7), $repoDirtyBefore, $repoDirtyAfter, $same)
    if (-not $same) {
        Write-Host '  [info] delta above is NOT a failure: containment is proven by workdir-outside-repo.' -ForegroundColor DarkGray
        Write-Host '         A concurrent lane or the WAL Stop-hook can move HEAD/porcelain mid-run.' -ForegroundColor DarkGray
    }
}

# ---------------------------------------------------------------------------
# Cleanup + exit. pass/fail COMPUTED from the counters - never a pasted label.
# ---------------------------------------------------------------------------
if ($KeepTemp) {
    Write-Host ("temp trees KEPT at: {0}" -f $root) -ForegroundColor Yellow
}
else {
    Set-Location $WorkDir
    Remove-Item -Recurse -Force -LiteralPath $root -ErrorAction SilentlyContinue
    Write-Host ("temp trees removed ({0}) - pass -KeepTemp to inspect" -f $root) -ForegroundColor DarkGray
}

Write-Host ''
Write-Host ("cases {0}/{1} PASS | asserts {2} run, {3} failed" -f $passCases, $totalCases, $script:AssertCount, $script:FailCount) -ForegroundColor Cyan

$exitCode = 0
if ($script:FailCount -gt 0) { $exitCode = 1 }
if ($passCases -ne $totalCases) { $exitCode = 1 }

if ($exitCode -eq 0) {
    Write-Host 'VERDICT: PASS' -ForegroundColor Green
}
else {
    Write-Host 'VERDICT: FAIL' -ForegroundColor Red
    if ($InjectLegacyRule) {
        Write-Host 'NOTE: -InjectLegacyRule was set. A FAIL here is the EXPECTED result: it proves the test has teeth.' -ForegroundColor Magenta
    }
}
exit $exitCode