lane BP merged: C-exact false on a rich turn, residue is one fleet-id transposition; rule 26(c) qualified
This commit is contained in:
parent
371f789ade
commit
10ddf09cb4
3 changed files with 24 additions and 17 deletions
|
|
@ -1,16 +1,16 @@
|
|||
# SotS RE campaign — coverage dashboard
|
||||
|
||||
Generated 2026-09-09 05:36 UTC · `sots-re` @ f14e845,2026-09-09 · `sots-engine` @ 989c692,2026-09-08 (240 commits) · regenerate with `tools/dashboard.py`
|
||||
Generated 2026-09-09 06:02 UTC · `sots-re` @ 371f789,2026-09-09 · `sots-engine` @ 1654785,2026-09-09 (241 commits) · regenerate with `tools/dashboard.py`
|
||||
|
||||
> **North star:** A functional reimplementation of the engine — behavior-equivalent, NOT byte-for-byte
|
||||
|
||||
## 1. Map coverage (campaign/board.md)
|
||||
|
||||
422 targets · mapped-or-better **375/422** `[█████████░] 89%` · verified **333/422** `[████████░░] 79%`
|
||||
425 targets · mapped-or-better **378/425** `[█████████░] 89%` · verified **336/425** `[████████░░] 79%`
|
||||
|
||||
| Status | Count | % |
|
||||
|---|---:|---:|
|
||||
| verified | 333 | 79% |
|
||||
| verified | 336 | 79% |
|
||||
| mapped | 42 | 10% |
|
||||
| in-progress | 4 | 1% |
|
||||
| backlog | 41 | 10% |
|
||||
|
|
@ -19,12 +19,12 @@ Generated 2026-09-09 05:36 UTC · `sots-re` @ f14e845,2026-09-09 · `sots-engine
|
|||
| Type | verified | mapped | in-progress | backlog | blocked | total |
|
||||
|---|---:|---:|---:|---:|---:|---:|
|
||||
| objects | 46 | 6 | 0 | 3 | 1 | 56 |
|
||||
| control-flow | 32 | 2 | 0 | 0 | 0 | 34 |
|
||||
| control-flow | 33 | 2 | 0 | 0 | 0 | 35 |
|
||||
| subsystems | 4 | 8 | 0 | 2 | 1 | 15 |
|
||||
| engine | 30 | 0 | 0 | 0 | 0 | 30 |
|
||||
| engine | 31 | 0 | 0 | 0 | 0 | 31 |
|
||||
| verify | 104 | 15 | 3 | 35 | 0 | 157 |
|
||||
| phase2 | 13 | 3 | 1 | 0 | 0 | 17 |
|
||||
| meta | 85 | 6 | 0 | 1 | 0 | 92 |
|
||||
| meta | 86 | 6 | 0 | 1 | 0 | 93 |
|
||||
| other | 19 | 2 | 0 | 0 | 0 | 21 |
|
||||
|
||||
## 2. Binary understanding
|
||||
|
|
@ -38,7 +38,7 @@ Generated 2026-09-09 05:36 UTC · `sots-re` @ f14e845,2026-09-09 · `sots-engine
|
|||
- Catalogs: **1,595/1,595** files parsed (91 block kinds in `schema_stats.json`), dangling cross-refs **0** (`crosslink.json`)
|
||||
- Oracle `mars-parse`: **1,531/1,531** files agree `[██████████] 100%`
|
||||
- Oracle `mars-text`: **64/64** files agree `[██████████] 100%`
|
||||
- Saves: **38/38** real saves strict-clean — strict exit 0, 0 errors, 0 warnings
|
||||
- Saves: **41/41** real saves strict-clean — strict exit 0, 0 errors, 0 warnings
|
||||
- Design rules: **127/127** stock designs pass `[██████████] 100%`
|
||||
- Value domains: **490/724** typed fields have been seen to vary `[███████░░░] 68%` — the other **234** have only ever held one value across the corpus, so their typing is untested (`value-domain-census.md`)
|
||||
|
||||
|
|
@ -66,7 +66,7 @@ Generated 2026-09-09 05:36 UTC · `sots-re` @ f14e845,2026-09-09 · `sots-engine
|
|||
| `shim/trace` | 2,258 | 9 | 273 | direct (WIN32) | shim-trace.md |
|
||||
| **total** | **58,647** | **122** | **4257** | | |
|
||||
|
||||
Board `engine:` rows: verified **30**, mapped 0, in flight 0 (of 30) — verified & merged `[██████████] 100%`
|
||||
Board `engine:` rows: verified **31**, mapped 0, in flight 0 (of 31) — verified & merged `[██████████] 100%`
|
||||
|
||||
## 5. Phase 2 milestones
|
||||
|
||||
|
|
@ -112,7 +112,7 @@ Detail: `verify/results/standalone/report.txt`.
|
|||
|
||||
## 7. Verification ledger
|
||||
|
||||
- ✅ Saves strict: 38/38 (strict exit 0, 0 errors, 0 warnings)
|
||||
- ✅ Saves strict: 41/41 (strict exit 0, 0 errors, 0 warnings)
|
||||
- ✅ Design rules: 127/127
|
||||
- ✅ oracle mars-parse 1531/1531 · ✅ oracle mars-text 64/64
|
||||
- ✅ Compare harness present (`verify/harness/compare/`)
|
||||
|
|
@ -133,11 +133,11 @@ Most recent open:
|
|||
|
||||
## 9. Delta since previous dashboard
|
||||
|
||||
- verified targets: 330 → 333 (+3) · mapped-or-better: 372 → 375 (+3)
|
||||
- verified targets: 333 → 336 (+3) · mapped-or-better: 375 → 378 (+3)
|
||||
- engine LOC: 58,647 → 58,647 (+0) · test files: 122 → 122 (+0) · checks: 4,257 → 4,257 (+0)
|
||||
- addresses verified: 1,152 → 1,160 (+8) · recovered layouts: 384 → 384 (+0) · open questions: 26 → 26 (+0)
|
||||
- addresses verified: 1,160 → 1,160 (+0) · recovered layouts: 384 → 384 (+0) · open questions: 26 → 26 (+0)
|
||||
- standalone leaves closed: 45 → 45 (+0) · leaves still diverging: 63 → 63 (+0)
|
||||
|
||||
---
|
||||
warnings: board.md: unknown types subsystems; mars-rng.md: no oracle total row parsed; mars-stream.md: no oracle total row parsed; mars-vfs.md: no oracle total row parsed
|
||||
<!-- dashboard-metrics {"verified": 333, "mapped_plus": 375, "targets": 422, "loc": 58647, "tests": 122, "checks": 4257, "addr_verified": 1160, "addr_total": 1291, "layouts": 384, "open_q": 26, "sa_closed": 45, "sa_left": 63} -->
|
||||
<!-- dashboard-metrics {"verified": 336, "mapped_plus": 378, "targets": 425, "loc": 58647, "tests": 122, "checks": 4257, "addr_verified": 1160, "addr_total": 1291, "layouts": 384, "open_q": 26, "sa_closed": 45, "sa_left": 63} -->
|
||||
|
|
|
|||
File diff suppressed because one or more lines are too long
|
|
@ -388,7 +388,11 @@ mechanism.
|
|||
> existing fleets. The per-process seed was present in all three. It reaches the save only through a
|
||||
> decision whose outcome set is not a singleton given the state, and whether such a decision is
|
||||
> reached is a **predicate on the pre-turn save** — rule 28's shape: `ResTNm == ''` names a pick
|
||||
> turn; `NumDes` moving names a design turn; a batch of completions names a fleet-assignment turn;
|
||||
> turn **for a player that has an AI client and something to decide with** (lane BP, 2026-09-09:
|
||||
> four players on `ad-turn27` carry `ResTNm == ''` and contributed nothing, because they have
|
||||
> `NumOwn == 0` and the engine builds **three** AI clients for seven non-human players — the
|
||||
> signature is *necessary, not sufficient*, and a save-field predicate still has to be read
|
||||
> against who actually runs); `NumDes` moving names a design turn; a batch of completions names a fleet-assignment turn;
|
||||
> one consumer (`0x0069dbb0`) has a 3–40-turn fuse and cannot show inside two turns of a load.
|
||||
> So: record the pair as (save, procedure, hashes) and write the exposure facts next to the hashes;
|
||||
> never extend a certified pair by a turn without its own two-process agreement (`ar-oracle-A-post`
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue