# v5 — D5 rewritten under conservative exclusion; D7 and teardown corrected

hertz 2026-09-12, source-only, NO GRANT, A7 still todlando's. Replaces v4 sections D5/D7 and the
teardown line of D2. Everything else in v4 stands. **NOTHING HERE HAS BEEN EXECUTED.**

## Product selection, recorded as ruled (doyle 06:23Z)

- SERVING BINARY and PREPARATION TOOLS: **921aa68f (FOLD-3)** — `$EXE` is built from it, and
  `xtask debug-keygen / debug-pin / debug-rollout / debug-mark-applied` are run from it.
- RIG SOURCE (role A, the fetching cells): **b6bbaf22**, identified separately, not merged in.
- No assembly mutation and no build during A7.
- **What the evidence will then name:** the PAIR (921aa68f product + b6bbaf22 rig), not either alone,
  and not a landing-candidate verdict. Any later citation that drops one half misstates it.
- This also resolves the v4 D3 blocker (a): `debug-mark-applied` exists at 921aa68f, so preparation
  runs from the same tree as the serving binary, and b6bbaf22 contributes only role A's test file.

## D5 (rewritten) — conservative exclusion, three-valued, not a firewall evaluator

**The polarity is inverted from v4.** v4 asked "does this rule cover the flow?" and answered false
for everything it could not decide — which manufactures a clean zero out of exactly the rules it
failed to model. v5 asks only the question a census may safely answer:

> Does a SUPPORTED predicate PROVE this rule cannot match the tested flow?

Three outcomes per rule: `excluded` (proven non-matching on at least one axis), `admits` (proven
covering on every axis), `unresolved` (neither). **`unresolved` is not a pass — it BLOCKS the
admission review**, exactly as an `admits` row does. No axis ever answers "does not cover" from a
token it does not model; it answers `unknown`, and `unknown` is contagious upward.

Each axis returns one of `covers` / `excludes` / `unknown`. Rule verdict: any `excludes` ⇒ excluded;
else all `covers` ⇒ admits; else unresolved.

### The serving interface is RESOLVED, not unioned (fixes v4 L186-193)

v4 collected every connected prefix and every connection profile and treated the union as "the
serving interface". The route to the peer names one interface; that one is the subject.

    $route  = Find-NetRoute -RemoteIPAddress $PEER -ErrorAction Stop | Select-Object -First 1
    $srcIp  = [string]$route.IPAddress
    $ifIdx  = [int]$route.InterfaceIndex
    $srcLen = [int](Get-NetIPAddress -InterfaceIndex $ifIdx -IPAddress $srcIp -AddressFamily IPv4 `
                      -ErrorAction Stop).PrefixLength
    # The profile category MAY be unavailable; that is an 'unknown' input, never a default.
    $cat = try { [string](Get-NetConnectionProfile -InterfaceIndex $ifIdx -ErrorAction Stop).NetworkCategory }
           catch { $null }
    # If Find-NetRoute throws, the census is UNRESOLVED as a whole and no arm runs.

### One numeric helper, no prefix strings (fixes v4 L182-185)

v4 formatted a network back into a dotted string via `BitConverter` + a reversed slice — a second
byte reversal on top of `Ip2I`'s. v5 never formats a network at all; membership is compared
numerically, so the round-trip that carried the bug does not exist.

    function Ip2I($s){ $b = [System.Net.IPAddress]::Parse($s).GetAddressBytes()
                       ([uint32]$b[0] -shl 24) -bor ([uint32]$b[1] -shl 16) -bor
                       ([uint32]$b[2] -shl 8)  -bor  [uint32]$b[3] }
    function MaskOf([int]$len){ if($len -le 0){ [uint32]0 } else { [uint32]::MaxValue -shl (32-$len) } }
    function SameNet($aIp,$bIp,[int]$len){ ((Ip2I $aIp) -band (MaskOf $len)) -eq ((Ip2I $bIp) -band (MaskOf $len)) }

### The axes

    # Enabled ------------------------------------------------------------------
    function Ax-Enabled($v){ switch($v){ 'True'{'covers'} 'False'{'excludes'} default{'unknown'} } }

    # Protocol: TCP admits; a DIFFERENT known protocol proves non-match; anything
    # else is unknown (never 'excludes' from an unmodelled token).
    function Ax-Proto($v){
      if($v -in @('TCP','6','Any')){ 'covers' }
      elseif($v -in @('UDP','17','ICMPv4','1','ICMPv6','58','IPv6','41','GRE','47','ESP','50','AH','51')){ 'excludes' }
      else { 'unknown' } }

    # LocalPort: per-entry supported/unsupported, then combined. UNSUPPORTED
    # TOKENS ('RPC','RPCEPMap','IPHTTPSIn','PlayToDiscovery', ...) make the rule
    # unknown -- v4 mapped them to false. (doyle: PortCovers mapped unsupported
    # tokens to false, not undecided.)
    function Ax-Port($entries,[int]$p){
      $sawUnknown = $false
      foreach($e in @($entries)){
        if($e -eq 'Any'){ return 'covers' }
        elseif($e -match '^\d+$'){ if([int]$e -eq $p){ return 'covers' } }
        elseif($e -match '^(\d+)-(\d+)$'){ if($p -ge [int]$Matches[1] -and $p -le [int]$Matches[2]){ return 'covers' } }
        else { $sawUnknown = $true } }
      if($sawUnknown){ 'unknown' } else { 'excludes' } }

    # Program: 'Any' and an ABSENT filter both mean no program restriction --
    # v4 excluded 'Any' (doyle, line 194). An env-var or store-app spelling is
    # unknown, because comparing it to a literal path proves nothing.
    function Ax-Program($prog,$exe){
      if([string]::IsNullOrEmpty($prog) -or $prog -eq 'Any'){ 'covers' }
      elseif($prog -match '%|^\{|^S-1-|\|'){ 'unknown' }          # env var, package/app id, policy id
      elseif($prog -ieq $exe){ 'covers' }
      elseif($prog -match '^[A-Za-z]:\\' -and $exe -match '^[A-Za-z]:\\'){ 'excludes' }
      else { 'unknown' } }

    # Profile: no category resolved => every non-Any rule is unknown.
    function Ax-Profile($profile,$cat){
      if($profile -eq 'Any'){ 'covers' }
      elseif($null -eq $cat){ 'unknown' }
      elseif(($profile -split ',') -contains $cat){ 'covers' }
      elseif(($profile -split ',') | Where-Object { $_ -notin @('Domain','Private','Public') }){ 'unknown' }
      else { 'excludes' } }

    # Address axis, shared by LocalAddress (vs $srcIp) and RemoteAddress (vs $PEER).
    # v4's local axis accepted ONLY 'Any' and so excluded a rule scoped to the
    # server's own address (doyle, line 195). LocalSubnet may only ever return
    # 'covers' or 'unknown': the serving interface's prefix is checked, and BOTH a
    # miss and an unresolved interface are unknown, because that one prefix does
    # not exhaust the keyword's applicable scope -- v4 tested it against a union of
    # every interface and let a miss read as an exclusion (doyle, lines 182-185 and
    # 06:26Z).
    function Ax-Addr($entries,$target,$srcIp,[int]$srcLen){
      $sawUnknown = $false
      foreach($e in @($entries)){
        if($e -eq 'Any'){ return 'covers' }
        elseif($e -match '^\d+\.\d+\.\d+\.\d+$'){ if($e -eq $target){ return 'covers' } }
        elseif($e -match '^(\d+\.\d+\.\d+\.\d+)/(\d+)$'){
          if(SameNet $Matches[1] $target ([int]$Matches[2])){ return 'covers' } }
        elseif($e -match '^(\d+\.\d+\.\d+\.\d+)-(\d+\.\d+\.\d+\.\d+)$'){
          $i = Ip2I $target; if($i -ge (Ip2I $Matches[1]) -and $i -le (Ip2I $Matches[2])){ return 'covers' } }
        elseif($e -eq 'LocalSubnet'){
          # A MISS IS UNKNOWN, NOT AN EXCLUSION (doyle 06:26Z). The route-selected
          # interface's prefix does not exhaust the keyword's applicable scope, so
          # "not in THIS prefix" does not prove "matches no local subnet".
          if($null -eq $srcIp){ $sawUnknown = $true }
          elseif(SameNet $srcIp $target $srcLen){ return 'covers' }
          else { $sawUnknown = $true } }
        else { $sawUnknown = $true } }      # Internet, Intranet, DNS, DHCP, dynamic keywords, IPv6
      if($sawUnknown){ 'unknown' } else { 'excludes' } }

    # EnforcementStatus: 'Full' covers. ANYTHING ELSE IS UNKNOWN, NOT EXCLUDED --
    # the value set is not one I have modelled, and "this rule is not enforced"
    # is exactly the kind of exclusion this section refuses to infer.
    function Ax-Enforce($v){ if($v -eq 'Full'){ 'covers' } else { 'unknown' } }

### The pass

    $ax = @('Ax-Enabled','Ax-Proto','Ax-Port','Ax-Program','Ax-Profile','Ax-Local','Ax-Remote','Ax-Enforce')
    $rows = $D | ForEach-Object {
      $v = @( (Ax-Enabled $_.enabled), (Ax-Proto $_.proto), (Ax-Port $_.ports $PORT),
              (Ax-Program $_.program $EXE), (Ax-Profile $_.profile $cat),
              (Ax-Addr $_.local  $srcIp $srcIp $srcLen), (Ax-Addr $_.remotes $PEER $srcIp $srcLen),
              (Ax-Enforce $_.enforce) )
      $verdict = if($v -contains 'excludes'){ 'excluded' }
                 elseif($v -contains 'unknown'){ 'unresolved' } else { 'admits' }
      [pscustomobject]@{ name=$_.name; verdict=$verdict; axes=($ax -join ',' ); values=($v -join ',') } }
    $admits     = @($rows | ? verdict -eq 'admits')
    $unresolved = @($rows | ? verdict -eq 'unresolved')
    $excluded   = @($rows | ? verdict -eq 'excluded')
    # Every unresolved row is PRINTED with its per-axis values, so the reason it
    # could not be decided is on the record rather than summarised into a count.

**BLOCKED PRECONDITION** = `$admits` empty **AND** `$unresolved` empty **AND** the serving profile's
`DefaultInboundAction` recorded **AND** the enabled Block rules enumerated and reported (same
three-valued treatment; reported, never judged). A non-empty `$unresolved` does not weaken the
verdict — it withholds it.

### Controls

Dump-level, over the captured `$D`, creating nothing (unchanged from v4):
positive port column = a row whose ports cover 5470 (the live listener's rule); positive program
column = a row with a non-empty program; negative = a sentinel name minted this run and never
created must return 0 rows. Plus both rule counts, with and without the `-Direction Inbound` query
filter, so that filter's effect is a measured number rather than an assumption.

Predicate-level, per doyle: **each axis function is exercised against a MATCHING, a NONMATCHING and
an UNSUPPORTED input, and must answer `covers` / `excludes` / `unknown` respectively.** These are
pure and need no host state, but they are scheduled AFTER the window with everything else. Examples:
`Ax-Port @('29470') 29470`→covers, `Ax-Port @('80') 29470`→excludes, `Ax-Port @('RPC') 29470`→unknown;
`Ax-Program 'C:\hz-rig\spt-twohost.exe' $EXE`→covers, `Ax-Program 'C:\windows\other.exe' $EXE`→excludes,
`Ax-Program '%SystemRoot%\x.exe' $EXE`→unknown; `Ax-Addr @('LocalSubnet') $PEER $null 0`→unknown, and `Ax-Addr @('LocalSubnet') '10.9.9.9'
'192.168.1.81' 24`→unknown as well (a MISS on the serving prefix is not an exclusion).
A suite in which no case returns `excludes` is a dead instrument and voids the census.

## D7 (corrected) — the exe path DOES matter

v4 said the pinned path is irrelevant to matching because the product's own pair carries no program
filter. **That is false as written and doyle rejected it:** it is true only of the OWNED pair. An
UNRELATED enabled Allow rule that is program-scoped may name that path and admit the flow — which is
precisely what `Ax-Program` is in the census for. So:

- `$EXE` is pinned once, at a path the census's program axis reports as named by NO enabled Allow
  rule — and "not named" here means **proven** `excludes` on the program axis for every such rule,
  with any `unknown` blocking the choice rather than permitting it.
- If no candidate path clears that bar, the arm is UNRUNNABLE and is reported so.
- `$EXE` remains the gate's sha subject and the binder the product prints (v4 D3.1), unchanged.

## Teardown (corrected) — nothing unconditional

The v4 line `Remove-Item -Recurse $HOME_DIR` is REMOVED. Sequence instead:

1. `serve lan --stop` (T4) and its `LAN_FIREWALL_CLEAN` line.
2. Re-run every census of D4/D5 and diff against the initial dump.
3. COPY the evidence out of the isolated home — the product's stdout/stderr per transition, the
   home's `logs/`, both rule dumps, the route/interface resolution — into
   `.spt/preserved/hertz-304-w2-traceability/`, and verify the copies by content (not by exit code).
4. Only after cleanup is VERIFIED and the evidence is copied and checked does the home get removed,
   and that removal is a separate decision, not a line in the rig script.

## One instrument note (not part of the plan)

Auditing this file's line endings through MSYS `grep -c $'\r'` returned 0 and `sed -n | xxd` showed
bare `0a`: both text-mode paths STRIP the CR. `xxd` on the file directly shows `0d0a`. A CRLF audit
run through either would read clean-LF and license a naive LF rewrite of all 1215 lines. Same family
as the zero-match filter that reads as absence. Yours if it belongs in the register.
