certified-pairs: record pairs as (save, procedure, route, hashes, processes, masks)
This commit is contained in:
alex
parent
f1306713d1
commit
77b5dd0d13
2 changed files with 90 additions and 0 deletions
78
verify/results/saves/certified-pairs.md
Normal file
78
verify/results/saves/certified-pairs.md
Normal file
|
|
@ -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.
|
||||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue