-
Notifications
You must be signed in to change notification settings - Fork 1
Expand file tree
/
Copy pathverify.c
More file actions
6798 lines (6546 loc) · 349 KB
/
Copy pathverify.c
File metadata and controls
6798 lines (6546 loc) · 349 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
/* https://github.com/petersm3/roae
* Developed with AI assistance (Claude, Anthropic)
*
* verify.c — independent per-layer mass verifier for the f1c5 run (TR-11 §10vi, gate (c)).
*
* WHAT THIS IS. A second opinion on the symmetry-quotient DP, computed a different way and
* sharing NO code with solve.c. solve.c reports, for each layer k, a per-layer *plain*
* (orbit-expanded) mass in its run.out:
*
* [f1c5] layer k= 3/31: canonical_masks=378 ... mass=158364 ...
*
* That number is produced by the orbit-quotient DP and then expanded through orbit weights.
* This program recomputes the same quantity with a PLAIN, NON-QUOTIENT layered DP — no
* canonicalization, no orbit weights, no stabilizer bookkeeping — and compares. Agreement
* therefore exercises exactly the machinery TR-11 §2 flags as delicate (the mask action is
* NOT free, so prefix stabilizers exist and must be weighted correctly), and it does so on
* the TRUE full-31 instance rather than a reduced rung.
*
* WHY THIS FORM. At the time this verifier was written (2026-07-21), solve.c's on-disk layer
* format was not published in any public document, so verifying the binary layer FILES would
* have required consulting solve.c — reintroducing precisely the shared-misreading failure
* class that verify.py's F-3 finding proved is real. (Since then the formats HAVE been
* published — documentation/F1C5_LAYER_FORMAT.md — so a spec-driven independent layer reader
* is now possible; per the verifier discipline it belongs in this file.) The per-layer
* masses in run.out, by contrast, are plain numbers whose MEANING is published (TR-11 §3's
* gate identity), so they can be checked independently with no format dependency at all.
*
* SCOPE — what agreement does and does not establish.
* DOES: the quotient DP's orbit expansion and stabilizer weighting reproduce the plain
* mass exactly, at full-31, for every layer this program reaches.
* DOES NOT: verify layers beyond its memory reach (the plain state space grows ~16x per
* layer, so it exhausts long before k=31), and therefore does NOT constitute the
* independent full-scale recomputation §10(vi) asks for. That remains open.
*
* INDEPENDENCE — OF ALGORITHM, NOT OF INPUT. Everything is rebuilt from the published
* definitions — SPECIFICATION.md's C1-C5, partner() = rev unless palindromic else comp, and
* TR-11 §5's first-completion DFS for the budget B0. No solve.c header, no shared traversal,
* no copied table of RESULTS. The KING WEN INPUT is deliberately shared: KW[64] below is the
* same 64-entry literal solve.c and verify.py carry — it is the object of study, and every
* instrument reads it, so it is an acknowledged DATA-level closure, not an independence
* (Codex V2-12 #1, 2026-09-02: a line-position permutation applied to all 64 entries changes
* 48 of them and still satisfies partner-pairing, C4, the C5 histogram and C3 = 776 — every
* shared-input verifier would agree on a wrong convention; the datum is anchored EXTERNALLY,
* by a re-derivation from source texts, not by anything in this file). What this file does
* with that input is derived, not trusted: the KW pair table and B0 are DERIVED here, C3's
* ceiling is recomputed and asserted, and B0 is cross-checked against the value solve.c
* records in its manifest (a disagreement is itself a finding).
*
* BUILD: cc -O2 -o verify verify.c -lz -lpthread -lm
* (zlib: the v2 layer codec is per-block zlib; pthreads: the --ie-* modes;
* libm: sqrtl in the Knuth prober's kn_ci — WITHOUT -lm THE LINK FAILS on the
* stock toolchain, "undefined reference to `sqrtl'". This header omitted -lm
* until 2026-09-03 (Codex V2-F59 #8) while the compile gate silently supplied it.)
* USAGE: ./verify <run.out> [max_layer] (default max_layer = 6)
* Increase max_layer while memory allows; the program reports what it reached and
* stops cleanly rather than being killed.
* ./verify --check-layers DIR [max_k] [run.out] spec-driven layer-file reader
* (all layers, entry-streaming; with run.out also compares the independently
* re-derived orbit-weighted mass per layer); --check-layers-selftest.
* ./verify --scan-layers DIR [max_k] [run.out] the SAME checks + masses via
* the multi-observable parallel scan driver (N O_DIRECT read lanes, riders:
* T7/BL-7 orbit census + T6-slot stub; env LC_SCAN_LANES/CHUNK_KB/ODIRECT/
* T6STUB). Identity contract: minus "[scan] " lines, stdout and rc are
* byte-identical to --check-layers; --scan-selftest proves it on fixtures.
* ./verify --check-g-ladder FDIR GDIR [max_k] g-ladder verifier (structural +
* the f·g cut identity at every layer), against GT_LADDER_FORMAT.md.
* ./verify --check-t-ladder FDIR TDIR [max_k] t-ladder verifier (f-geometry
* mirror + the f·t node identity at every layer); --check-gt-selftest.
* ./verify --ie-count [opts] Route B: the INDEPENDENT inclusion–exclusion
* transfer-walk recount of |C1∩C2∩C4∩C5| (TR-11 §10vi) — see the ROUTE B
* section header below for the algorithm, options and validation ladder.
* --ie-no-budget = the C1∩C2∩C4 (F4) variant; --ie-pin/--ie-pin-c6c7 =
* the pinned-step (T3) variant for |C1∩C2∩C4∩C5∩C6∩C7|.
* ./verify --ie-probe NSAMP [--ie-threads N] full-31 throughput probe.
* ./verify --dp-count [opts] Route D: the SECOND instrument for the
* pinned (C6/C7) exact count — a direct layered exact-cover mask DP
* (NO inclusion–exclusion; different algorithm class from --ie-count).
* See the ROUTE D section header below.
* ./verify --knuth-anchors clean-room Knuth prober validation gate:
* exact KW-prefix subtree anchors (443/4, 62,256/2,232,
* 9,422,793/16,504, 8 with C6/C7) + a fixed-seed probe-vs-exact
* machinery check. Run before any probe run.
* ./verify --knuth-probe N [--knuth-seed S] [--knuth-threads T]
* [--knuth-no-c67] [--knuth-free F] the #194 CLEAN-ROOM Knuth
* random-probe estimator of |C1..C7| (default; own C3 predicate and
* own C6/C7 pin logic) or |C1..C5| (--knuth-no-c67). See the
* CLEAN-ROOM KNUTH PROBER section header below.
*/
#define _GNU_SOURCE /* O_DIRECT for the --scan-layers parallel read lanes */
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <stdint.h>
#include <zlib.h>
#include <pthread.h> /* --ie-count / --ie-probe worker threads (Route B); --scan-layers lanes */
#include <time.h>
#include <unistd.h>
#include <fcntl.h> /* --scan-layers: open(O_DIRECT), pread */
#include <errno.h>
#include <math.h> /* --knuth-probe: sqrtl/fabsl for the Wald CI */
#include <stdatomic.h> /* --knuth-probe: racy-free progress counters */
/* ---------- published constraint definitions, rebuilt from scratch ---------- */
static int popcount6(int n) { int c = 0; while (n) { c += n & 1; n >>= 1; } return c; }
static int hamming(int a, int b) { return popcount6(a ^ b); }
static int rev6(int n) { /* bit reversal of a 6-bit value */
int r = 0;
for (int i = 0; i < 6; i++) if ((n >> i) & 1) r |= 1 << (5 - i);
return r;
}
static int comp6(int n) { return n ^ 63; } /* complement */
static int partner(int h) { int r = rev6(h); return (r != h) ? r : comp6(h); }
/* The published King Wen sequence (the object of study; 6-bit hexagram values in KW order).
* Needed because TR-11 §5 states plainly that "the pair ORDER is part of the instance
* definition" — enumerating pairs by hexagram value instead builds a DIFFERENT instance and
* yields the wrong B0. (Learned the hard way: value-order gave B0=(7,6,10,8,0) against the
* published (2,8,13,7,1).) */
static const int KW[64] = {
63, 0,17,34,23,58, 2,16,55,59, 7,56,61,47, 4, 8,25,38, 3,48,41,37,32, 1,
57,39,33,30,18,45,28,14,60,15,40, 5,53,43,20,10,35,49,31,62,24, 6,26,22,
29,46, 9,36,52,11,13,44,54,27,50,19,51,12,21,42
};
/* The 32 canonical pairs IN KING WEN ORDER: pair i = (KW[2i], KW[2i+1]).
* partner() is re-derived independently and used to CHECK each pair (a disagreement would
* mean the published sequence violates C1 — itself a finding), not to build the ordering. */
static int PA[32], PB[32], NPAIR = 0;
static int build_pairs(void) {
if (NPAIR == 32) return 1; /* idempotent: both modes call it */
for (int i = 0; i < 32; i++) {
int a = KW[2 * i], b = KW[2 * i + 1];
if (partner(a) != b || partner(b) != a) {
fprintf(stderr, "*** C1 VIOLATION at KW pair %d: (%d,%d) partner=%d\n",
i, a, b, partner(a));
return 0;
}
PA[i] = a; PB[i] = b; NPAIR++;
}
return 1;
}
/* ---------- C3, re-derived HERE from this file's own KW table --------------
*
* SPECIFICATION.md C3: sum over all v in 0..63 of |pos(v) - pos(v ^ 63)|, where
* ^63 is the 6-bit complement. Every complement pair contributes its positional
* distance twice, once from each end. King Wen's value is the ceiling.
*
* DERIVED, NOT COPIED. The ceiling is computed from the KW table above rather
* than written as the literal 776, and then ASSERTED against 776 -- the same
* shape verify.py uses. A corrupted table must fail loudly rather than silently
* redefine the constraint. Note the identity C3 = 16 + 8*G is deliberately NOT
* used: it is an algebraic result this file exists to check independently, so
* importing it here would close the loop it is supposed to open.
*
* WHY THIS ARRIVED LATE (2026-09-02, Codex V2-F20 #1 / V2-F58 #1). Neither
* --check-artifact nor the repr oracle computed C3 at all. Both certified a
* record whose complement distance is 1080 against this 776 ceiling. The
* enumerator enforces C3 in-walk, and inheriting an enumerator-enforced
* invariant is precisely what an independent verifier may not do. */
static int vc_comp_dist(const int *seq) {
int pos[64];
for (int i = 0; i < 64; i++) pos[seq[i]] = i;
int total = 0;
for (int v = 0; v < 64; v++) {
int d = pos[v] - pos[v ^ 63];
total += (d < 0) ? -d : d;
}
return total;
}
/* Lazily derived and asserted. Lazy rather than folded into vc_build_budget()
* so that any future caller of vc_repr_of_key() gets a built ceiling; a zero
* ceiling would silently reject every key, which is the failure direction that
* looks like success. */
static int vc_c3_ceiling(void) {
static int c3max = 0;
if (c3max == 0) {
c3max = vc_comp_dist(KW);
if (c3max != 776) {
fprintf(stderr, "*** verify.c: KW complement distance is %d, expected 776 "
"(C3) -- KW table corrupt\n", c3max);
exit(2);
}
}
return c3max;
}
/* The 64-value hexagram sequence a record encodes, from its key and orientation
* bits. Slot s contributes its pair in stored order. */
static void vc_seq_of(const int *key, const int *orient, int *seq) {
for (int slot = 0; slot < 32; slot++) {
int P = key[slot], a = PA[P], b = PB[P];
seq[2 * slot] = orient[slot] ? b : a;
seq[2 * slot + 1] = orient[slot] ? a : b;
}
}
/* C5 boundary classes; distance 5 is forbidden by C2, distance 0 cannot occur. */
static const int CLS[5] = {1, 2, 3, 4, 6};
static int cls_ix(int d) { for (int i = 0; i < 5; i++) if (CLS[i] == d) return i; return -1; }
/* ---------- independent repr(k) oracle (--check-repr) ----------------------
*
* WHY IT EXISTS. AVAILABILITY FIRST (2026-09-03, Codex V2-L21 #3 / V2-F59 #7):
* `--kc-repr-normalize` and the SOLVE_REPR_FC A/B are NOT in main's solve.c and
* are on NO published ref AT ALL (zero occurrences on main, v4-compiler,
* v4-canonical AND orbit-port-188-candidate; they exist only on an unpushed
* local branch). The orb_* functions they wrap are published only on the
* unlanded orbit-port-188-candidate branch, which BRANCH_REGISTRY marks
* snapshot-do-not-cite (VERIFY.md §"NOT AVAILABLE IN THIS TREE"). They are
* quoted below as the design rationale this oracle answers, not as commands a
* reader of this tree can run. That unpublished --kc-repr-normalize said outright
* that "there is NO separate repr oracle in this tree": its only built-in
* check was IDEMPOTENCE (re-run on the output, expect byte-identical), which
* is self-consistent and so cannot catch a normalization that is stable but
* WRONG. The SOLVE_REPR_FC A/B was weaker than it looked for the same reason
* at one remove -- both arms
* share solve.c's DFS, child order and code, so a defect in the shared
* traversal is invisible to it at any sample size. This is the second
* instrument, of a different algorithm class, per the TR-11 v1.11 pattern.
*
* INDEPENDENCE IS THE DELIVERABLE. Written from the DEFINITION in
* lean/RecordConvention.lean --
*
* repr(k) = the lexicographically least orientation completion of the
* pair-order key k satisfying the constraint set (slot 0 forced)
*
* -- on THIS file's own KW table, its own partner()-derived pairs and its own
* hamming(). Not a transcription of orb_recanon_dfs. A faster reimplementation
* that borrowed solve.c's helpers or search shape would not be a second opinion.
* verify.py carries the same oracle; C exists because Python cannot cover 1.78e9
* records.
*
* WHY GREEDY 0-BEFORE-1 IS EXACTLY LEX-LEAST. Record byte i is
* (pair_index << 2) | (orientation << 1). The key fixes pair_index at every
* slot, so at each slot the orient=0 byte is strictly below the orient=1 byte,
* and records compare left to right. The first complete valid assignment found
* by a DFS trying 0 before 1, in slot order, IS the minimum. No search-order
* cleverness is involved, and none is permitted -- that equivalence is the
* entire point. */
static int vc_budget0[7];
/* Re-derive the C5 budget HERE from this file's KW table. Asserted against the
* published multiset so a corrupted table fails loudly instead of silently
* redefining the constraint. */
static int vc_build_budget(void) {
static const int WANT[7] = {0, 2, 20, 13, 19, 0, 9};
for (int d = 0; d < 7; d++) vc_budget0[d] = 0;
for (int i = 0; i < 63; i++) vc_budget0[hamming(KW[i], KW[i + 1])]++;
for (int d = 0; d < 7; d++)
if (vc_budget0[d] != WANT[d]) {
fprintf(stderr, "*** KW budget mismatch at d=%d: %d != %d\n",
d, vc_budget0[d], WANT[d]);
return 0;
}
return 1;
}
typedef struct { const int *key; int budget[7]; int orient[32]; } VcRepr;
static int vc_rec(VcRepr *st, int slot, int last) {
if (slot == 32) { /* exact consumption, not merely "fits" */
for (int d = 0; d < 7; d++) if (st->budget[d] != 0) return 0;
return 1;
}
int P = st->key[slot], a = PA[P], b = PB[P];
for (int o = 0; o < 2; o++) { /* 0 BEFORE 1 == lex-least */
int f = o ? b : a, s = o ? a : b;
int bd = hamming(last, f);
if (bd == 5 || st->budget[bd] <= 0) continue;
int wd = hamming(f, s);
st->budget[bd]--;
if (st->budget[wd] <= 0) { st->budget[bd]++; continue; }
st->budget[wd]--;
st->orient[slot] = o;
if (vc_rec(st, slot + 1, s)) return 1;
st->budget[wd]++; st->budget[bd]++;
}
return 0;
}
/* out must hold 32 bytes. Returns 1 and fills out, or 0 if the key admits no
* valid completion (which is itself a finding if the artifact stores one). */
static int vc_repr_of_key(const int *pair_order, unsigned char *out) {
VcRepr st;
/* C3 PRE-FILTER (added 2026-09-02). lean/RecordConvention.lean defines
* repr(k) as the lex-least completion satisfying C2/C3/C5; this function
* implemented C4/C2/C5 and omitted C3, so for a key whose C3 exceeds the
* ceiling it RETURNED A RECORD where the definition says none exists.
*
* Because C3 is ORIENTATION-INVARIANT -- swapping a pair moves a hexagram
* and its complement together -- the omission could never change WHICH
* completion is lex-least, so no AGREE/DISAGREE verdict was ever wrong. What
* it corrupted is the INCOMPUTABLE leg, the one VERIFY.md advertises as
* fail-closed: measured on a C3 = 1080 key in both languages, CHECK_REPR=PASS
* with INCOMPUTABLE=0 and rc 0.
*
* That same invariance is what makes this a legitimate PRE-DFS filter rather
* than a leaf test: C3 is a function of the key alone, so it is decided once,
* here, instead of at every completion -- it PRUNES rather than costing. Any
* orientation gives the same value, so the all-zero assignment is used. */
int seq0[64], orient0[32];
for (int i = 0; i < 32; i++) orient0[i] = 0;
vc_seq_of(pair_order, orient0, seq0);
if (vc_comp_dist(seq0) > vc_c3_ceiling()) return 0;
st.key = pair_order;
memcpy(st.budget, vc_budget0, sizeof(st.budget));
int P0 = pair_order[0], a0 = PA[P0], b0 = PB[P0], o0;
if (a0 == 63 && b0 == 0) o0 = 0; /* C4 forces the (63,0) opening */
else if (b0 == 63 && a0 == 0) o0 = 1;
else return 0;
int wd0 = hamming(63, 0);
if (st.budget[wd0] <= 0) return 0;
st.budget[wd0]--;
st.orient[0] = o0;
if (!vc_rec(&st, 1, 0)) return 0;
for (int i = 0; i < 32; i++)
out[i] = (unsigned char)(((pair_order[i] & 0x3F) << 2) | ((st.orient[i] & 1) << 1));
return 1;
}
/* ---------- --check-artifact: what solutions.bin ACTUALLY claims ----------
*
* WHY THIS EXISTS, AND WHEN --check-repr DOES NOT APPLY.
*
* --check-repr asks "is the stored orientation the global lex-least valid
* completion of this key?". That IS the record convention -- forced by
* partition-invariance, and settled against the cell-scoped alternative -- but it
* is established by a POST-PASS, not by the merge. orb_normalize_rec_op ->
* orb_repr_global, exposed as `solve --kc-repr-normalize IN.bin OUT.bin` — the
* orb_* functions published only on the UNLANDED orbit-port-188-candidate branch,
* the flag itself on NO published ref at all (NOT in main's solve.c — VERIFY.md
* §"NOT AVAILABLE IN THIS TREE"; in this tree the
* convention is an acceptance-test CONTRACT, with no shipped tool that applies
* it), is what applies it. Against a raw merge output that pass has not run, so --check-repr
* disagrees on exactly the records the post-pass would rewrite: measured
* 2026-08-15 over 1,776,347,935 records, a regionally varying 1.06%-42.2% with
* INCOMPUTABLE=0 throughout. Expected, not a defect. --check-repr is the right
* ACCEPTANCE TEST for the post-pass output and the wrong instrument for its input.
*
* Do not mistake orb_recanon for the convention (a misreading made and retracted
* on 2026-08-15): it pins slots 0..3 from a member CELL's prefix and its only
* caller is orb_expand_record, for cell-faithful expansion shards. Cell-scoped
* visited-min was PROVEN INSUFFICIENT as a record representative -- the merged
* cross-cell min moves with budget, breaking partition-invariance and
* record-level nesting.
*
* A second limitation survives normalization: --check-repr is STRUCTURALLY BLIND
* TO A WRONG PAIR SEQUENCE. vc_repr_of_key builds its output from the same key
* array it just decoded out of the stored record, so the pair-order bits are
* identical by construction and a disagreement can only ever be an orientation
* bit. This check is not blind to it.
*
* WHAT THIS CHECKS INSTEAD -- the four properties the file does claim:
* (1) VALIDITY every stored record satisfies the constraint set: the forced
* (63,0) opening (C4), no HD-5 transition (C2), the C5 budget
* consumed EXACTLY (not merely "fits"), and the C3
* complement-distance ceiling.
* (2) SORTEDNESS pair-order keys strictly increase, matching compare_solutions.
* (3) DEDUP strictness in (2) is exactly the one-record-per-class claim.
* (4) HEADER format version, the zero reserved field, and the declared
* count against the stream.
*
* (1) READ "every stored record's OWN ORIENTATIONS satisfy the constraint set"
* until 2026-09-02. That was an overclaim in two directions at once: it promised
* the whole constraint set while C3 was absent, and the word "orientations"
* scoped the promise to a property C3 does not have. Both are now true as
* written -- C3 landed with this revision -- but the wording is what made the
* gap invisible, so it is corrected here rather than merely satisfied.
*
* SCOPE TOKEN, DELIBERATELY UNCHANGED. This mode still prints
* SCOPE=validity_sortedness_dedup_only_NOT_completeness. C3 and the header legs
* make the "validity" term MORE complete; they do not move the boundary the
* token actually draws, which is completeness. Changing the string would break
* every `grep -qx` consumer to signal nothing.
*
* This is a linear walk per record, not a backtracking search, so the whole
* artifact streams in minutes rather than the ~47 h a repr sweep costs -- and
* unlike the repr sweep it can actually fail on real corruption.
*
* SCOPE: this does NOT check that the artifact is COMPLETE (that no valid
* solution is missing). Completeness is the enumeration's claim, attested by
* the canonical sha, not something a single-pass reader can establish. */
static int vc_check_artifact_main(int argc, char **argv) {
if (argc < 3) { fprintf(stderr, "usage: %s --check-artifact FILE [N] [OFFSET]\n", argv[0]); return 2; }
const char *path = argv[2];
long long want = (argc >= 4) ? atoll(argv[3]) : -1; /* -1 == to EOF */
long long off = (argc >= 5) ? atoll(argv[4]) : 0;
if (!build_pairs() || !vc_build_budget()) { printf("ARTIFACT=FAIL_tables\n"); return 2; }
gzFile fh = gzopen(path, "rb");
if (!fh) { printf("ARTIFACT=FAIL_open\n"); return 2; }
unsigned char hdr[32];
if (gzread(fh, hdr, 32) != 32) { printf("ARTIFACT=FAIL_short_header\n"); gzclose(fh); return 2; }
/* VALIDATE THE MAGIC. Without this a HEADERLESS file (a raw sub_*.bin shard)
* has its FIRST RECORD silently eaten as "header", and the checker can then
* report ARTIFACT=PASS on a file it never fully read. That is the same
* failure mode as the recon off-by-one this repo already carries a fix for:
* applying solutions.bin's header convention to headerless shards. Fail
* closed rather than auto-detect -- this tool validates the merged artifact,
* and a shard should be an explicit refusal, not a silent reinterpretation. */
if (memcmp(hdr, "ROAE", 4) != 0) {
printf("ARTIFACT=FAIL_no_ROAE_header\n");
printf(" refusing: first 4 bytes are not 'ROAE'. A headerless shard would\n");
printf(" otherwise have its first record consumed as a header.\n");
gzclose(fh); return 2;
}
/* HEADER CONFORMANCE (added 2026-09-02; Codex V2-F48 #3 / V2-F58 #2).
* Before this, the magic was the ONLY header field checked: the version and
* the declared count were never read and the reserved field was never
* inspected, so a v2 header, a nonzero reserved byte and a count that
* disagreed with the body each returned ARTIFACT=PASS. SOLUTIONS_FORMAT.md
* makes version==1, a zero reserved field and an accurate count normative,
* and REBUILD_FROM_SPEC.md requires a conformant reader to REJECT an unknown
* version. Counters rather than hard exits, matching verify.py: a
* nonconformant header does not make the records unreadable, and an operator
* is better served by both facts than by the first one alone. */
long long bad_hdr_version = 0, bad_hdr_reserved = 0, bad_geometry = 0;
unsigned int hdr_version = (unsigned int)hdr[4] | ((unsigned int)hdr[5] << 8)
| ((unsigned int)hdr[6] << 16) | ((unsigned int)hdr[7] << 24);
if (hdr_version != 1u) {
bad_hdr_version = 1;
printf(" header: unsupported format version %u (this reader knows version 1)\n", hdr_version);
}
for (int i = 16; i < 32; i++) if (hdr[i]) { bad_hdr_reserved = 1; break; }
if (bad_hdr_reserved) {
printf(" header: reserved bytes [16:32] are NONZERO (");
for (int i = 16; i < 32; i++) printf("%02x", hdr[i]);
printf(")\n");
}
unsigned long long hdr_declared = 0;
for (int i = 15; i >= 8; i--) hdr_declared = (hdr_declared << 8) | (unsigned long long)hdr[i];
unsigned char rec[32], prev[32];
for (long long i = 0; i < off; i++)
if (gzread(fh, rec, 32) != 32) { printf("ARTIFACT=FAIL_offset_past_eof\n"); gzclose(fh); return 2; }
long long n = 0, bad_key = 0, bad_spare = 0, bad_open = 0,
bad_hd5 = 0, bad_budget = 0, bad_residue = 0, bad_order = 0, bad_c3 = 0, shown = 0;
int have_prev = 0;
while (want < 0 || n < want) {
int got = gzread(fh, rec, 32);
if (got == 0) break;
if (got != 32) { printf("ARTIFACT=FAIL_partial_record\n"); gzclose(fh); return 2; }
long long idx = off + n;
n++;
int key[32], orient[32]; uint32_t seen = 0; int bad = 0;
/* Count spare bits over ALL 32 bytes BEFORE the key check. Previously this
* sat inside the decode loop and stopped at the bad-key break, so on a
* record with both a bad key and later spare bits the C and Python
* implementations disagreed (Python counts all 32 first). Two independent
* instruments that diverge on compound defects are not two instruments. */
for (int i = 0; i < 32; i++) if (rec[i] & 1) bad_spare++;
for (int i = 0; i < 32; i++) {
key[i] = (rec[i] >> 2) & 0x3F;
orient[i] = (rec[i] >> 1) & 1;
if (key[i] >= 32 || ((seen >> key[i]) & 1u)) { bad = 1; break; }
seen |= 1u << key[i];
}
if (bad) { bad_key++; if (shown < 5) { printf(" record %lld: key is not a permutation of 0..31\n", idx); shown++; } continue; }
/* C3 (added 2026-09-02). SPECIFICATION.md's constraint set is C1-C5 and
* SOLUTIONS_FORMAT.md states outright that "a re-implementation that omits
* C3 produces a strict SUPERSET". This loop checked C4/C2/C5 and never
* computed C3, so a record with cd = 1080 against the 776 ceiling was
* certified ARTIFACT=PASS by BOTH implementations. The seven-negative
* controls table could not catch it: a controls table exercises the
* counters that exist and is blind, by construction, to a missing
* predicate. Computed from the DECODED SEQUENCE, matching verify.py --
* not via the 16+8*G identity, which this file exists to check rather
* than to assume. */
{
int seq[64];
vc_seq_of(key, orient, seq);
int cd = vc_comp_dist(seq);
if (cd > vc_c3_ceiling()) {
bad_c3++;
if (shown < 5) { printf(" record %lld: complement distance %d > %d (C3)\n", idx, cd, vc_c3_ceiling()); shown++; }
}
}
/* (2)+(3): strictly increasing on the pair-identity bytes. */
if (have_prev) {
int c = 0;
for (int i = 0; i < 32 && c == 0; i++) c = (prev[i] & 0xFC) - (rec[i] & 0xFC);
if (c >= 0) { bad_order++; if (shown < 5) { printf(" record %lld: pair-order not strictly greater than predecessor (%s)\n", idx, c == 0 ? "duplicate class" : "out of order"); shown++; } }
}
memcpy(prev, rec, 32); have_prev = 1;
/* (1): validate the STORED orientations, not some recomputed ideal. */
int budget[7]; memcpy(budget, vc_budget0, sizeof(budget));
int P0 = key[0], a0 = PA[P0], b0 = PB[P0];
int f0 = orient[0] ? b0 : a0, s0 = orient[0] ? a0 : b0;
if (!(f0 == 63 && s0 == 0)) { bad_open++; if (shown < 5) { printf(" record %lld: opening is not the forced 63->0\n", idx); shown++; } continue; }
int wd0 = hamming(63, 0);
if (budget[wd0] <= 0) { bad_budget++; continue; }
budget[wd0]--;
int last = 0, fail = 0;
for (int slot = 1; slot < 32 && !fail; slot++) {
int P = key[slot], a = PA[P], b = PB[P];
int f = orient[slot] ? b : a, s = orient[slot] ? a : b;
int bd = hamming(last, f);
if (bd == 5) { bad_hd5++; fail = 1; if (shown < 5) { printf(" record %lld: HD-5 transition into slot %d\n", idx, slot); shown++; } break; }
if (budget[bd] <= 0) { bad_budget++; fail = 1; break; }
budget[bd]--;
int wd = hamming(f, s);
if (budget[wd] <= 0) { bad_budget++; fail = 1; break; }
budget[wd]--;
last = s;
}
if (fail) continue;
/* BAD_BUDGET_RESIDUE is a defensive guard that is STRUCTURALLY UNREACHABLE,
* and is recorded as such rather than claimed as tested: the budget totals
* 63 (asserted by vc_build_budget) and a complete record consumes exactly
* 1 + 31*2 = 63 units, so if every decrement above succeeded the residue is
* necessarily zero. It stays only to fail closed if that identity is ever
* broken by a table change. No negative control exercises it because none
* can. */
for (int d = 0; d < 7; d++) if (budget[d] != 0) { bad_residue++; break; }
}
gzclose(fh);
/* GEOMETRY: the declared record count must match the stream. Only meaningful
* on a WHOLE-FILE read. Ignoring the count for loop TERMINATION is a
* deliberate convention that makes the [N] [OFFSET] sub-range form work --
* but that explains not USING the count, never not CHECKING it, so the
* default full pass compares them and a sub-range invocation stays green.
* Measured on the logical (post-inflate) stream via gzread, so a .gz artifact
* is checked on its contents rather than its compressed size. */
if (want < 0 && off == 0 && (unsigned long long)n != hdr_declared) {
bad_geometry = 1;
printf(" header declares %llu records but the stream holds %lld\n", hdr_declared, n);
}
long long bad_total = bad_key + bad_spare + bad_open + bad_hd5 + bad_budget + bad_residue
+ bad_order + bad_c3 + bad_hdr_version + bad_hdr_reserved + bad_geometry;
printf("RECORDS=%lld\nBAD_KEY=%lld\nBAD_SPARE_BIT=%lld\nBAD_OPENING=%lld\n"
"BAD_HD5=%lld\nBAD_BUDGET=%lld\nBAD_BUDGET_RESIDUE=%lld\nBAD_ORDER=%lld\n"
"BAD_C3=%lld\nBAD_HDR_VERSION=%lld\nBAD_HDR_RESERVED=%lld\nBAD_GEOMETRY=%lld\n",
n, bad_key, bad_spare, bad_open, bad_hd5, bad_budget, bad_residue, bad_order,
bad_c3, bad_hdr_version, bad_hdr_reserved, bad_geometry);
if (n > 0 && bad_total == 0) {
printf("ARTIFACT=PASS\nSCOPE=validity_sortedness_dedup_only_NOT_completeness\n");
return 0;
}
printf("ARTIFACT=FAIL\n");
return 1;
}
/* --check-repr FILE [N] [OFFSET] -- verdicts are KEY=value for `grep -qx`.
*
* NOTE: for solutions.bin as produced today this is EXPECTED to disagree; see
* the --check-artifact header above. It becomes the right instrument only after
* the repr(k) post-pass, applied to that post-pass's OUTPUT. */
static int vc_check_repr_main(int argc, char **argv) {
if (argc < 3) { fprintf(stderr, "usage: %s --check-repr FILE [N] [OFFSET]\n", argv[0]); return 2; }
const char *path = argv[2];
long long want = (argc >= 4) ? atoll(argv[3]) : 1000;
long long off = (argc >= 5) ? atoll(argv[4]) : 0;
if (!build_pairs() || !vc_build_budget()) { printf("CHECK_REPR=FAIL_tables\n"); return 2; }
gzFile fh = gzopen(path, "rb");
if (!fh) { printf("CHECK_REPR=FAIL_open\n"); return 2; }
unsigned char hdr[32];
if (gzread(fh, hdr, 32) != 32) { printf("CHECK_REPR=FAIL_short_header\n"); gzclose(fh); return 2; }
/* Skip by READING, not by seeking: gzseek on a large member re-inflates
* anyway, and a short read here must be distinguishable from EOF at the
* target offset rather than silently landing somewhere else. */
unsigned char rec[32];
for (long long i = 0; i < off; i++)
if (gzread(fh, rec, 32) != 32) { printf("CHECK_REPR=FAIL_offset_past_eof\n"); gzclose(fh); return 2; }
long long checked = 0, agree = 0, disagree = 0, incomputable = 0;
unsigned char mine[32];
while (checked < want) {
int got = gzread(fh, rec, 32);
if (got == 0) break;
if (got != 32) { printf("CHECK_REPR=FAIL_partial_record\n"); gzclose(fh); return 2; }
int key[32]; uint32_t seen = 0; int bad = 0;
for (int i = 0; i < 32; i++) {
key[i] = (rec[i] >> 2) & 0x3F;
if (key[i] >= 32 || (seen >> key[i]) & 1u) { bad = 1; break; }
seen |= 1u << key[i];
}
if (bad) { printf("CHECK_REPR=FAIL_malformed_key at %lld\n", off + checked); gzclose(fh); return 2; }
checked++;
if (!vc_repr_of_key(key, mine)) incomputable++;
else if (memcmp(mine, rec, 32) == 0) agree++;
else {
disagree++;
if (disagree <= 3) printf(" record %lld: stored != independent repr\n", off + checked - 1);
}
}
gzclose(fh);
printf("CHECKED=%lld\nAGREE=%lld\nDISAGREE=%lld\nINCOMPUTABLE=%lld\n",
checked, agree, disagree, incomputable);
/* Fail closed: an incomputable key is a finding too -- the artifact claims a
* canonical record for a key this instrument says cannot be completed. */
if (checked > 0 && disagree == 0 && incomputable == 0) {
printf("CHECK_REPR=PASS\nSCOPE=records_read_only_NOT_whole_artifact\n");
return 0;
}
printf("CHECK_REPR=FAIL\n");
return 1;
}
/* ---------- big enough integers: 128-bit with overflow detection ---------- */
typedef unsigned __int128 u128;
static int OVERFLOWED = 0;
static u128 add_ck(u128 a, u128 b) { u128 s = a + b; if (s < a) OVERFLOWED = 1; return s; }
static void print_u128(u128 v, char *out) { /* out must hold >=40 bytes */
char tmp[40]; int i = 0;
if (v == 0) { strcpy(out, "0"); return; }
while (v) { tmp[i++] = '0' + (int)(v % 10); v /= 10; }
int j = 0; while (i) out[j++] = tmp[--i];
out[j] = 0;
}
/* ---------- B0 via TR-11 §5 Step 1: deterministic first-completion DFS ----------
* Scans unplaced pairs in ascending index and, for each, orientation o=0 (enter b, exit a)
* then o=1 (enter a, exit b). B0 is the boundary-class multiset of the FIRST complete walk.
* Derived here; cross-checked against solve.c's manifest by the caller. */
static int NFREE; /* pairs 1..31 are free; pair 0 is C4-pinned */
static int b0[5];
static int b0_dfs_res[5];
static int b0_found;
static int b0_cnt[5];
static void b0_dfs(int depth, int last, uint32_t used) {
if (b0_found) return;
if (depth == NFREE) { memcpy(b0_dfs_res, b0_cnt, sizeof b0_dfs_res); b0_found = 1; return; }
for (int i = 0; i < NFREE && !b0_found; i++) {
if (used & (1u << i)) continue;
int a = PA[i + 1], b = PB[i + 1]; /* free pairs are 1..31 */
for (int o = 0; o < 2 && !b0_found; o++) {
int f = o == 0 ? b : a; /* o=0 enters b, exits a */
int s = o == 0 ? a : b;
int d = hamming(last, f);
if (d == 5 || d == 0) continue;
int ci = cls_ix(d);
b0_cnt[ci]++;
b0_dfs(depth + 1, s, used | (1u << i));
if (!b0_found) b0_cnt[ci]--;
}
}
}
/* ---------- plain layered DP: state = (mask, last, budget vector) ---------- */
typedef struct { uint32_t mask; uint8_t last; uint8_t p[5]; u128 val; } Ent;
/* open-addressing hash table, grown by doubling */
typedef struct { Ent *e; size_t cap, n; } Tab;
static uint64_t mix(uint64_t x) {
x ^= x >> 33; x *= 0xff51afd7ed558ccdULL;
x ^= x >> 33; x *= 0xc4ceb9fe1a85ec53ULL;
x ^= x >> 33; return x;
}
static uint64_t keyhash(uint32_t mask, int last, const uint8_t *p) {
uint64_t k = ((uint64_t)mask << 8) | (uint64_t)last;
for (int i = 0; i < 5; i++) k = k * 1099511628211ULL + p[i];
return mix(k);
}
static int same(const Ent *e, uint32_t mask, int last, const uint8_t *p) {
if (e->mask != mask || e->last != last) return 0;
for (int i = 0; i < 5; i++) if (e->p[i] != p[i]) return 0;
return 1;
}
static void tab_init(Tab *t, size_t cap) {
/* on OOM sets cap=0; callers must check */
t->cap = cap; t->n = 0;
t->e = calloc(cap, sizeof(Ent));
if (!t->e) { fprintf(stderr, "\n[memory exhausted allocating %zu entries — stopping cleanly]\n", cap); t->cap = 0; return; }
for (size_t i = 0; i < cap; i++) t->e[i].last = 0xFF; /* 0xFF marks empty */
}
static void tab_free(Tab *t) { free(t->e); t->e = NULL; t->cap = t->n = 0; }
static void tab_add(Tab *t, uint32_t mask, int last, const uint8_t *p, u128 v);
static void tab_grow(Tab *t) {
Tab nt; tab_init(&nt, t->cap * 2);
for (size_t i = 0; i < t->cap; i++)
if (t->e[i].last != 0xFF) tab_add(&nt, t->e[i].mask, t->e[i].last, t->e[i].p, t->e[i].val);
free(t->e); *t = nt;
}
static void tab_add(Tab *t, uint32_t mask, int last, const uint8_t *p, u128 v) {
if ((t->n + 1) * 10 >= t->cap * 7) tab_grow(t);
size_t i = keyhash(mask, last, p) & (t->cap - 1);
for (;;) {
Ent *e = &t->e[i];
if (e->last == 0xFF) {
e->mask = mask; e->last = (uint8_t)last; memcpy(e->p, p, 5); e->val = v;
t->n++; return;
}
if (same(e, mask, last, p)) { e->val = add_ck(e->val, v); return; }
i = (i + 1) & (t->cap - 1);
}
}
/* ---------- run.out parsing (reads only the published per-layer mass line) ---------- */
static int parse_masses(const char *path, char masses[32][48]) {
FILE *f = fopen(path, "r");
if (!f) { fprintf(stderr, "cannot open %s\n", path); return -1; }
char line[8192]; int found = 0;
for (int i = 0; i < 32; i++) masses[i][0] = 0;
while (fgets(line, sizeof line, f)) {
int k; const char *q;
if (sscanf(line, "[f1c5] layer k=%d/31:", &k) != 1) continue;
if (k < 0 || k > 31) continue;
q = strstr(line, "mass=");
if (!q) continue;
q += 5;
int j = 0; while (*q >= '0' && *q <= '9' && j < 46) masses[k][j++] = *q++;
masses[k][j] = 0;
if (j) found++;
}
fclose(f);
return found;
}
/* ==========================================================================
* LAYER-FILE READER (--check-layers DIR [max_k]) [task (A), TR-11 §10vi]
*
* Reads solve.c's on-disk layer files DIRECTLY and checks the invariants that
* hold them together, written AGAINST documentation/F1C5_LAYER_FORMAT.md and
* NOTHING from solve.c — the same two-step discipline that surfaced F-3: the
* spec was published first, this reader was written against the spec second.
*
* The mass-DP mode above reaches only k≈4-6 (plain state blows up ~16×/layer).
* This mode is entry-streaming and O(nm) in memory, so it reaches ALL layers
* present on disk, including the final k=31 — where the summed value bytes must
* equal the published 39-digit count. That is an end-to-end content check of
* the headline integer, read from the real bytes, with no solve.c dependency.
*
* Checks per layer:
* header magic/version/n/k/start_exit/pl_hash/b0 vs the manifest;
* pl_hash recomputed from the spec's FNV-1a-64 WORD variant, == manifest;
* layout masks strictly ascending; off[] monotone, off[0]=0, off[nm]=ne;
* per mask popcount == k; no bits ≥ n; CANONICAL (numeric min of its orbit
* under the run's restricted pair-permutations);
* per entry last∈[0,63] (bits 22-31 zero); rid<R; keys ascending within span;
* value nonzero; and the SUM INVARIANT — the rid mixed-radix digits
* sum to k, each ≤ b0[c] (a strong per-entry content check, free);
* mass the §Reading-recipe step-5/6 ORBIT-WEIGHTED MASS, Σ_i s_i ·
* (geff/|stab(mask_i)|), re-derived from the layer bytes under the
* independently-derived TR-11 §2 group (24 pair-perms from
* C_{S6}(rev), restricted to the run's pair list) and compared to
* solve.c's reported mass= for every layer when a run log is given
* — the full-scale counterpart of the small-k mass-DP check;
* layer 0 exactly {mask 0, key start_exit<<16, value 1};
* layer n nm==1, mask==2^n-1, orbit 1, every rid==R-1, and for full-31
* Σvalues == PUBLISHED COUNT and ≡ 0 (mod 24).
* A v2 block whose Adler-32 or decompressed size is wrong fails in zlib/inflate.
*
* Any mismatch is a FINDING (F1C5_LAYER_FORMAT.md: "report it, do not patch
* around it"), never silently repaired.
*
* Memory: masks[nm] + off[nm+1] in RAM (peak full-31 ~156 MB); entries stream.
* This is a CAMPAIGN-VM tool, not an orchestrator tool — run it where the layers
* live. `--check-layers-selftest` builds tiny synthetic v1+v2 fixtures and needs
* neither real data nor much memory.
* ========================================================================== */
#define LC_PUBLISHED_COUNT "1097051278789181790036112071176579186688" /* |C1∩C2∩C4∩C5| */
/* |C1∩C2∩C4| — published exact (TR-4 §"exact vs estimator" table / TR-11;
* same integer as verify.py's _C1C2C4_EXACT and the solve.c §f1-exact comment). */
#define LC_PUBLISHED_COUNT_C1C2C4 "757058601340255440651419713405330315358208"
/* |C1∩C2∩C4∩C5∩C6∩C7| (= |C1–C7| with C3 dropped) — published exact
* (METHODS.md estimate-vs-exact table; first computed 2026-07-25 by the T3
* pinned-step IE recount). --dp-count's full-31 pinned default target. */
#define LC_PUBLISHED_COUNT_C1C7NOC3 "516880238445773965371923491676160"
typedef struct { uint64_t l[3]; } u192; /* value = l0 + 2^64 l1 + 2^128 l2 */
static int u192_add(u192 *a, u192 b) { /* a+=b; returns 1 on 192-bit overflow */
unsigned __int128 s = (unsigned __int128)a->l[0] + b.l[0]; a->l[0] = (uint64_t)s;
s = (unsigned __int128)a->l[1] + b.l[1] + (s >> 64); a->l[1] = (uint64_t)s;
s = (unsigned __int128)a->l[2] + b.l[2] + (s >> 64); a->l[2] = (uint64_t)s;
return (s >> 64) != 0;
}
static int u192_zero(u192 a) { return (a.l[0] | a.l[1] | a.l[2]) == 0; }
static int u192_eq(u192 a, u192 b) { return a.l[0]==b.l[0] && a.l[1]==b.l[1] && a.l[2]==b.l[2]; }
static unsigned u192_mod(u192 a, unsigned m) { /* a mod m, big-endian limb walk */
unsigned __int128 r = 0;
for (int i = 2; i >= 0; i--) { r = (r << 64) | a.l[i]; r %= m; }
return (unsigned)r;
}
static u192 u192_dec(const char *s) { /* decimal string -> u192 */
u192 v = {{0,0,0}};
for (; *s; s++) { if (*s < '0' || *s > '9') continue;
unsigned __int128 c = (unsigned)(*s - '0');
for (int i = 0; i < 3; i++) { unsigned __int128 t = (unsigned __int128)v.l[i]*10 + c;
v.l[i] = (uint64_t)t; c = t >> 64; } }
return v;
}
static void u192_print(u192 v, char *out) { /* out >= 60 bytes */
if (u192_zero(v)) { strcpy(out, "0"); return; }
char t[64]; int n = 0; u192 x = v;
while (!u192_zero(x)) { unsigned __int128 r = 0;
for (int i = 2; i >= 0; i--) { r = (r << 64) | x.l[i]; x.l[i] = (uint64_t)(r/10); r %= 10; }
t[n++] = '0' + (int)r; }
int j = 0; while (n) out[j++] = t[--n]; out[j] = 0;
}
static int u192_mul_small(u192 *a, uint32_t s) { /* a*=s; 1 on 192-bit overflow */
unsigned __int128 c = 0;
for (int i = 0; i < 3; i++) {
unsigned __int128 t = (unsigned __int128)a->l[i] * s + c;
a->l[i] = (uint64_t)t; c = t >> 64;
}
return c != 0;
}
/* full 192x192 product; *ovf set to 1 if the true product exceeds 192 bits.
* Valid-ladder products f(s)*g(s) / f(s)*t(s) never do (each is <= the total
* node count < 2^192); the guard exists for the corrupt-file case. */
static u192 u192_mul(u192 a, u192 b, int *ovf) {
uint64_t r[6] = {0, 0, 0, 0, 0, 0};
for (int i = 0; i < 3; i++) {
unsigned __int128 carry = 0;
for (int j = 0; j < 3; j++) {
unsigned __int128 t = (unsigned __int128)a.l[i] * b.l[j] + r[i + j] + carry;
r[i + j] = (uint64_t)t; carry = t >> 64;
}
for (int q = i + 3; carry && q < 6; q++) {
unsigned __int128 t = (unsigned __int128)r[q] + carry;
r[q] = (uint64_t)t; carry = t >> 64;
}
}
if (r[3] | r[4] | r[5]) *ovf = 1;
u192 out; out.l[0] = r[0]; out.l[1] = r[1]; out.l[2] = r[2];
return out;
}
/* pl_hash: FNV-1a-64 absorbing 64-bit WORDS (n, start_exit, pl[0..n-1]) — the
* project-convention variant stated verbatim in F1C5_LAYER_FORMAT.md §Manifest. */
static uint64_t lc_pl_hash(uint32_t n, uint32_t start_exit, const uint32_t *pl) {
uint64_t h = 0xcbf29ce484222325ULL;
h ^= n; h *= 0x100000001b3ULL;
h ^= start_exit; h *= 0x100000001b3ULL;
for (uint32_t i = 0; i < n; i++) { h ^= pl[i]; h *= 0x100000001b3ULL; }
return h;
}
/* radices / place-values / R from b0, per §Entry encoding. */
static void lc_radix(const int b0v[5], uint32_t rad[5], uint32_t *R) {
uint32_t pv = 1;
for (int c = 0; c < 5; c++) { rad[c] = pv; pv *= (uint32_t)(b0v[c] + 1); }
*R = pv;
}
/* decode rid -> per-class digits; return digit sum, or -1 if any digit > b0[c]. */
static int lc_rid_digits(uint32_t rid, const int b0v[5], const uint32_t rad[5]) {
int sum = 0;
for (int c = 4; c >= 0; c--) { uint32_t p = rid / rad[c]; rid %= rad[c];
if ((int)p > b0v[c]) return -1;
sum += (int)p; }
return sum;
}
/* ---------------------------------------------------------------------------
* The TR-11 §2 group, DERIVED here from the published definition — the same
* derivation verify.py's --recount performs (_commuting_bitperms + induce +
* dedup) and nothing from solve.c: enumerate the 720 bit-position permutations
* of S6, keep the 48 commuting with reversal (g[5-i] == 5-g[i], TR-5's
* C_{S6}(rev)), induce each on the 32 KW pairs (a pair maps to the pair whose
* unordered hexagram set is its image), dedup (kernel {id, rev}) -> exactly 24
* distinct pair-permutations (≅ S4), every one fixing pair 0.
*
* These 24 power the §Reading-recipe step-5 orbit weighting: mask bit i of a
* run stands for pair pl[i], a pair-perm σ acts on a mask by relabeling its
* set bits through pl, and orbit(mask) = |G_run| / |stab(mask)| where G_run is
* the group of DISTINCT RESTRICTED permutations on the run's pair list (all 24
* restrict when pl is group-closed, as every real run's is; fewer may remain
* distinct after restriction). Group closure is re-verified numerically both
* before and after restriction, so orbit-stabilizer genuinely applies.
* ------------------------------------------------------------------------- */
static uint8_t PP[24][32]; static int NPP = 0; /* the 24 induced pair-perms */
static uint8_t PPG[24][6]; /* one witness bit-perm per pair-perm
* (recorded for --ie-count's elementwise
* startup re-verification; no other use) */
static int pp_n48; /* how many g commute with rev */
static int pp_fail;
static void pp_rec(int depth, int *g, int used) {
if (pp_fail) return;
if (depth == 6) {
for (int i = 0; i < 6; i++) if (g[5-i] != 5-g[i]) return; /* keep C_{S6}(rev) */
pp_n48++;
uint8_t m[32];
for (int j = 0; j < 32; j++) {
int ga = 0, gb = 0; /* bit i -> position g[i] */
for (int t = 0; t < 6; t++) {
if ((PA[j] >> t) & 1) ga |= 1 << g[t];
if ((PB[j] >> t) & 1) gb |= 1 << g[t];
}
int found = -1;
for (int q = 0; q < 32; q++)
if ((PA[q]==ga && PB[q]==gb) || (PA[q]==gb && PB[q]==ga)) { found = q; break; }
if (found < 0) { pp_fail = 1; return; } /* g fails to permute the pairs — a finding */
m[j] = (uint8_t)found;
}
for (int q = 0; q < NPP; q++) if (!memcmp(PP[q], m, 32)) return;
if (NPP >= 24) { pp_fail = 2; return; } /* >24 distinct — a finding */
for (int t = 0; t < 6; t++) PPG[NPP][t] = (uint8_t)g[t]; /* witness bit-perm */
memcpy(PP[NPP++], m, 32);
return;
}
for (int v = 0; v < 6; v++)
if (!(used & (1 << v))) { g[depth] = v; pp_rec(depth+1, g, used | (1 << v)); }
}
static int derive_pair_perms(void) { /* 1 ok; prints its own failure */
if (NPP == 24) return 1; /* idempotent */
if (!build_pairs()) return 0;
int g[6]; pp_n48 = 0; pp_fail = 0; NPP = 0;
pp_rec(0, g, 0);
if (pp_fail == 1) { printf("*** FAIL: a C_{S6}(rev) element does not permute the 32 pairs\n"); return 0; }
if (pp_fail == 2 || NPP != 24) { printf("*** FAIL: induced pair-perms = %d, expected 24\n", NPP); return 0; }
if (pp_n48 != 48) { printf("*** FAIL: |C_{S6}(rev)| = %d, expected 48\n", pp_n48); return 0; }
for (int q = 0; q < NPP; q++) {
uint32_t seen = 0;
if (PP[q][0] != 0) { printf("*** FAIL: pair-perm %d moves the C4 anchor pair\n", q); return 0; }
for (int j = 0; j < 32; j++) seen |= 1u << PP[q][j];
if (seen != 0xffffffffu) { printf("*** FAIL: pair-perm %d is not a bijection\n", q); return 0; }
}
for (int a = 0; a < NPP; a++) /* closure: {24} must be a group */
for (int b = 0; b < NPP; b++) {
uint8_t c[32]; int found = 0;
for (int j = 0; j < 32; j++) c[j] = PP[a][PP[b][j]];
for (int t = 0; t < NPP; t++) if (!memcmp(PP[t], c, 32)) { found = 1; break; }
if (!found) { printf("*** FAIL: pair-perms not closed under composition\n"); return 0; }
}
return 1;
}
/* Restrict the 24 pair-perms to the run's pair list pl[0..n-1] (mask bit i =
* pair pl[i]). Keeps those preserving the pl SET, rewrites them on subset
* indices, dedups, and re-verifies closure. Returns the group order geff
* (1..24, divides 24), or -1 on failure. */
static int lc_restrict_perms(const uint32_t *pl, uint32_t n, uint8_t rp[24][32]) {
int inv[32]; for (int i = 0; i < 32; i++) inv[i] = -1;
if (n == 0 || n > 31) return -1;
for (uint32_t i = 0; i < n; i++) {
if (pl[i] < 1 || pl[i] > 31 || inv[pl[i]] >= 0) return -1;
inv[pl[i]] = (int)i;
}
int geff = 0;
for (int q = 0; q < NPP; q++) {
uint8_t r[32]; int ok = 1;
for (uint32_t i = 0; i < n && ok; i++) {
int im = inv[PP[q][pl[i]]];
if (im < 0) ok = 0; else r[i] = (uint8_t)im;
}
if (!ok) continue; /* does not preserve the pl set */
int dup = 0;
for (int t = 0; t < geff; t++) if (!memcmp(rp[t], r, n)) { dup = 1; break; }
if (!dup) memcpy(rp[geff++], r, n);
}
if (geff < 1 || 24 % geff) return -1; /* order must divide 24 (Lagrange) */
for (int a = 0; a < geff; a++) /* closure of the restricted set */
for (int b = 0; b < geff; b++) {
uint8_t c[32]; int found = 0;
for (uint32_t i = 0; i < n; i++) c[i] = rp[a][rp[b][i]];
for (int t = 0; t < geff; t++) if (!memcmp(rp[t], c, n)) { found = 1; break; }
if (!found) return -1;
}
return geff;
}
static uint32_t lc_mask_img(uint32_t m, const uint8_t *sig) {
uint32_t r = 0;
while (m) { int b = __builtin_ctz(m); m &= m - 1; r |= 1u << sig[b]; }
return r;
}
/* Orbit size of mask m under the geff restricted perms (orbit-stabilizer:
* geff / |stab|); *canon set to 1 iff m is the numeric minimum of its orbit.
* Returns 0 if geff % |stab| != 0 — impossible under a true group action,
* guarded anyway so a closure bug can never mis-weight silently. */
static int lc_orbit_of(uint32_t m, uint8_t rp[24][32], int geff, int *canon) {
int stab = 0; uint32_t mn = m;
for (int q = 0; q < geff; q++) {
uint32_t im = lc_mask_img(m, rp[q]);
if (im == m) stab++;
if (im < mn) mn = im;
}
*canon = (mn == m);
if (stab == 0 || geff % stab) return 0;
return geff / stab;
}
/* =========================================================================
* --scan-layers: multi-observable parallel scan driver (config + rider state)
*
* One pass over the ladder, N registered integer accumulators, L parallel
* O_DIRECT read lanes. The FULL implementation (stream reader, lane workers,
* merge, self-test) lives after lc_selftest below; these declarations sit
* here because the shared driver lc_check_layers_impl dispatches on them.