diff --git a/verify/results/saves/certified-pairs.md b/verify/results/saves/certified-pairs.md new file mode 100644 index 0000000..f6d452e --- /dev/null +++ b/verify/results/saves/certified-pairs.md @@ -0,0 +1,78 @@ +# Certified pairs — what has actually been shown to reproduce, and under what procedure + +`determinism-hashes.txt` next to this file is a **file-hash inventory**: it says what a byte string +hashed to. It cannot say what was *done* to produce it, and after 2026-09-09 that distinction is +load-bearing. Two findings made it so: + +- **A pair certifies a procedure, not a state** (rule 26(c)). A control that agrees means "no exposed + decision was reached on these turns", never "this state is deterministic". +- **The route is part of the procedure.** The same turn runs one way by *continuation* and another way + after a *load*, **both reproducibly** — because a `Colonize` task alive in the AI agent by + continuation is simply absent after a load (lane BS). A hash without its route is not a claim. + +So a pair is `(input save, procedure, route, outputs, process count, masks)`. Anything missing one of +those columns is an observation, not a certification. + +## Certified + +| input | procedure | route | `(Autosave EndTurn)` | `(Autosave)` | processes | evidence | +|---|---|---|---|---|---:|---| +| `ref-turn2.sav` `ab4ac2d7…` | one End Turn | load | `bb4fd9ac…` | `978041ac…` | 5 + 1 | runs A–E; reproduced by lane H after everything changed | +| `ar-turn37-816raiders.sav` `b6f4e05f…` | End Turn, **auto-resolve peacefully**, End Turn | load | `15b99255…` | `7a8b3d5e…` | **4** | lane AR ×3 `hooks=off`, lane BS ×1 instrumented | +| `ar-oracle-A-pre.sav` `15b99255…` | one End Turn | **load** | `33e30092…` | `4c356f59…` | **3** | lane BQ ×2 `hooks=off`, lane BS ×1 instrumented | + +**The second and third rows are the same lineage and they do not agree with each other.** Row 2's +second turn reached by continuation gives `7a8b3d5e…`; the identical turn reached by *loading* row 2's +own intermediate save gives `4c356f59…`. Both are certified; neither is wrong. This is the load +boundary, and it is why the route column exists. + +**Row 3 is the standalone's first trade-raid pair** — one End Turn, no encounter, four raid rolls at +one word each. + +### Masks that must be on the line + +- `Player.Status` (4 → 0 on load) and the derived `Summary.Checksum`. +- **`/CD[1]/NPrvVa`, which advances by exactly +5.00 across a load** and falls on a combat turn. The + documented `--mask resave` rule said "nothing else varies"; that was true of early-game saves with + an empty `CD[1]` diplomacy block and **false on these**. Lane BQ's probe was unsatisfiable on that + leaf alone, before any AI behaviour entered the question. +- Row 3's `(Autosave EndTurn)` is a **resave** of `ar-oracle-A-pre.sav` and differs from it on that + one leaf. + +## Explicitly NOT certified + +| input | procedure | route | outcome set | why | +|---|---|---|---|---| +| `ad-turn27-two-raiders.sav` `1c8baa27…` | one End Turn | load | **2**: `e913ff41…` ×3, `724528ff…` ×2 | the fleet-visit-order residue | + +Five processes across three instrument configurations, **no third file**, both members reproduced at +least twice. The two outputs are `bp-pinA-turn28.sav` and `bp-pinB-turn28.sav`, and lane BU showed +the difference **is** the two orderings of two heap pointers: the assignment pass walks a container +keyed on `fleet->Location`, and under LFH randomisation two same-size allocations land in either +relative order. + +That is not a defect to fix and not a pair to keep hunting for. It is a **two-member outcome set**, +which is what C-set's shape needs, and `state_checksum --relabel-new-ids` compares across it: +`IDENTICAL modulo π = {1970↔1986}`. **The unpinned pair on the same save is refused by that tool and +still reports 94 leaves**, so the relabelling cannot launder a real divergence. + +Do not add a row here on the strength of one agreeing run. Three processes on `as-turn15` produced +the same bytes on a turn the predicate says is *exposed*, and a fourth produced different ones — +agreement on a single pair proves nothing (lane AP). + +## Standing rules for adding a row + +1. **Two fresh processes minimum**, and say how many. +2. **Run the control before reading anything from an instrumented run**, so that if it is a single + outcome the 1/k coincidence caveat does not apply (lane AR). +3. **Never extend a certified pair by a turn** without its own agreement. Row 2's state enters the + following turn with `ResTNm == ''` and is *predicted* to vary. +4. **Record the exposure facts next to the hashes**: each AI player's pre-turn `ResTNm`, `NumDes`, + `NumOwn`, whether ships completed, **and which players actually have an AI client** — a save with + seven non-human players builds three clients, and the other four carry the signature inertly. +5. **When the instrument cannot be removed**, pin to a natural run's observed values and require + byte-identity with it first (rule 26(d)). That agreement is both the pin's control and a noise + mask. + +Hashes here are recorded to 8 bytes for readability; the full values are in `determinism-hashes.txt` +and in each lane's findings file. diff --git a/verify/results/saves/determinism-hashes.txt b/verify/results/saves/determinism-hashes.txt index c4f326d..ec2e9a5 100644 --- a/verify/results/saves/determinism-hashes.txt +++ b/verify/results/saves/determinism-hashes.txt @@ -25,3 +25,15 @@ bb4fd9ac89f41e3bc0db2af08b18ce83417521ac4bcee695fc9fa6ce16e30948 runs/runE/MyGa bb4fd9ac89f41e3bc0db2af08b18ce83417521ac4bcee695fc9fa6ce16e30948 runs/runE/MyGameverify1rtE.sav bb4fd9ac89f41e3bc0db2af08b18ce83417521ac4bcee695fc9fa6ce16e30948 runs/runE/MyGameverify1verify1.sav ab4ac2d7e2977260a4de916f65c7ecc6dd5b0094dac4bb51241317232ea17ab4 runs/runE/ref-turn2.sav + +# 2026-09-09: this file is a FILE-HASH INVENTORY, not a certification record. +# It cannot express the procedure or the route, and after the load-boundary finding +# both are load-bearing: the same turn reached by continuation and by load gives +# different, individually reproducible results. Certified pairs live in +# certified-pairs.md next to this file, with route, process count and masks. +b6f4e05ff226eabd1695003b36293553642553cea96ef417364393e2332a7094 verify/results/saves/ar-turn37-816raiders.sav +15b99255e1f03dab3e35ab8c1ac64f221cb5aa9321f113c7a6e3d1263c3f34ca verify/results/saves/ar-oracle-A-pre.sav +7a8b3d5eb3a60ebac9f40646d3e4b15768a24a0af047a439ce090c7cf38e8b38 verify/results/saves/ar-oracle-A-post.sav +1c8baa27680809d585ab1728391e82729642d32aaedffd5bf95b616f0a11a436 verify/results/saves/ad-turn27-two-raiders.sav +e913ff41188211c02d536da616337544e64133996cd7cc7a6521a8df1960226f verify/results/saves/bp-pinA-turn28.sav +724528ffde9a7514b69ab9e82ed3b8c8ade63d622c0720de30503a73a92df11e verify/results/saves/bp-pinB-turn28.sav