-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathindex.html
More file actions
1369 lines (1250 loc) · 95.4 KB
/
Copy pathindex.html
File metadata and controls
1369 lines (1250 loc) · 95.4 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
<!--
Generative Logic: A deterministic reasoning and knowledge generation engine.
Copyright (C) 2025-2026 Generative Logic UG (haftungsbeschränkt).
Dual-licensed under the GNU Affero General Public License v3 or later
and a commercial license — see https://generative-logic.com/license.
MPU 0.1 — mapping today's Generative Logic onto silicon, with a cost estimate.
Concept-and-cost companion for a hardware / architecture audience.
-->
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="UTF-8">
<meta name="viewport" content="width=device-width, initial-scale=1.0">
<title>MPU 0.1 — The Mathematical Processing Unit</title>
<meta name="copyright" content="© 2025-2026 Generative Logic UG">
<meta name="license" content="AGPL-3.0-or-later">
<meta name="robots" content="noindex, nofollow, noai, noimageai">
<link rel="stylesheet" href="assets/mpu.css">
</head>
<body>
<nav id="side">
<div class="brand">GL · <span>MPU 0.1</span></div>
<div class="tag">The Mathematical Processing Unit — architecture & cost</div>
<ol>
<li class="pre"><a href="#top">Preamble — the two ceilings</a></li>
<li><a href="#compute">What GL computes, in HW terms</a></li>
<li><a href="#lb">The Logic Block = one core</a></li>
<li><a href="#memory">LB memory & its management</a></li>
<li><a href="#mail">The mail system — shared-RAM pull</a></li>
<li><a href="#split">LB split = scaling runtime</a></li>
<li><a href="#floorplan">The MPU floorplan</a></li>
<li><a href="#cost">Cost estimation</a></li>
<li><a href="#verdict">The verdict</a></li>
</ol>
<div class="secnote">Appendix</div>
<ol style="counter-reset:none">
<li><a href="#constants">Price & sizing constants</a></li>
</ol>
</nav>
<main>
<!-- ============================== PREAMBLE ============================== -->
<section id="top">
<div class="hero">
<div class="eyebrow">Generative Logic · Hardware track</div>
<h1>MPU 0.1 — The Mathematical Processing Unit</h1>
<p>Mapping <b>today's</b> Generative Logic onto silicon — what the machine
actually is in hardware terms, and an estimate of what it would
cost to build. The lineage is <b>CPU → GPU → TPU → MPU</b>: a processor whose
native workload is not arithmetic, not graphics, not tensors, but
<b>deductive inference</b>.</p>
<p class="stamp">Version 0.1 — a starting point to build on, not a finished part.
Sizing from the live prover; prices dated, refreshed only at release.</p>
</div>
<p class="lede">This is a record of where GL-on-silicon stands today, written for the
engineer who would build it — not a pitch. Every number comes from the running system
or is flagged as a rough, dated estimate; the problems are stated as plainly as the
wins.</p>
<h2 id="thesis" style="border-top:none;margin-top:10px">The whole argument, on one page</h2>
<p>
A proof engine has exactly two ways to run out of road. It runs out of
<b>memory</b> — the state of a hard problem no longer fits — or it runs out of
<b>time</b> — there are more deductions to make than one machine can make before
you lose patience. The MPU is the claim that <b>both ceilings are now
architectural, not fundamental</b>, because the GL prover was rebuilt into a
shape that lifts them:
</p>
<figure>
<svg viewBox="0 0 760 250" role="img" aria-label="The two ceilings GL hits and how the MPU lifts each: memory spills to SSD (virtually unlimited), runtime spreads across cores by LB split (virtually unlimited)">
<defs>
<marker id="p-ar" viewBox="0 0 10 10" refX="9" refY="5" markerWidth="7" markerHeight="7" orient="auto"><path d="M0 0 L10 5 L0 10 z" fill="#5DCAA5"/></marker>
</defs>
<!-- memory ceiling -->
<rect x="30" y="30" width="330" height="190" rx="12" fill="#20232F" stroke="#3A3D4A"/>
<text x="195" y="56" fill="#F2766B" font-size="14" font-weight="bold" text-anchor="middle">Ceiling 1 — MEMORY</text>
<text x="195" y="78" fill="#8B8FA5" font-size="11" text-anchor="middle">a hard problem's state stops fitting in RAM</text>
<rect x="70" y="96" width="250" height="34" rx="6" fill="#262938" stroke="#5DCAA5"/>
<text x="195" y="118" fill="#F0E8DC" font-size="11.5" text-anchor="middle">working set held in fast memory</text>
<path d="M195 130 L195 152" stroke="#5DCAA5" stroke-width="1.5" marker-end="url(#p-ar)"/>
<rect x="70" y="154" width="250" height="44" rx="6" fill="#1C1F2B" stroke="#EF9F27"/>
<text x="195" y="172" fill="#EF9F27" font-size="11.5" font-weight="bold" text-anchor="middle">the rest spills to SSD</text>
<text x="195" y="188" fill="#8B8FA5" font-size="10" text-anchor="middle">virtually unlimited · pages back on demand</text>
<!-- runtime ceiling -->
<rect x="400" y="30" width="330" height="190" rx="12" fill="#20232F" stroke="#3A3D4A"/>
<text x="565" y="56" fill="#F2766B" font-size="14" font-weight="bold" text-anchor="middle">Ceiling 2 — RUNTIME</text>
<text x="565" y="78" fill="#8B8FA5" font-size="11" text-anchor="middle">more deductions than one core can chew</text>
<rect x="440" y="96" width="250" height="34" rx="6" fill="#262938" stroke="#5DCAA5"/>
<text x="565" y="118" fill="#F0E8DC" font-size="11.5" text-anchor="middle">one calculation, one (or few) blocks</text>
<path d="M565 130 L565 152" stroke="#5DCAA5" stroke-width="1.5" marker-end="url(#p-ar)"/>
<rect x="440" y="154" width="250" height="44" rx="6" fill="#1C1F2B" stroke="#EF9F27"/>
<text x="565" y="172" fill="#EF9F27" font-size="11.5" font-weight="bold" text-anchor="middle">LB split across N cores</text>
<text x="565" y="188" fill="#8B8FA5" font-size="10" text-anchor="middle">virtually unlimited · min(work, cores)</text>
</svg>
<figcaption><b>Two ceilings, two levers.</b> Memory becomes an SSD-backed
hierarchy; runtime becomes a parallel fabric. Neither lever is hypothetical —
both already exist in the software, which is exactly why a hardware version is
worth costing.</figcaption>
</figure>
<div class="key">
<b>The MPU is a force multiplier, not a product on its own.</b> Put the value as:
<div style="text-align:center;font-size:19px;margin:14px 0;color:var(--fg)">
value = <span style="color:var(--amber)">(1 + N)</span>
×
<span style="color:var(--mint)">(does GL do real math?)</span>
</div>
GL on its own is the <b>1</b> — it runs today, without any of this. The MPU adds the
<b>N</b>: the same engine, accelerated. So the ASIC is not make-or-break for GL; it
takes a working engine from 1 to 1 + N. Both terms are gated by the second factor: if
GL cannot do real mathematics the whole thing is <b>zero</b>, and the <b>Fundamental
Theorem of Arithmetic (FTA) campaign is the test that decides it</b>. This document
estimates N and says nothing about the second factor; that one is settled in proofs,
not here.</div>
<div class="caveat">
<span class="lab">One commitment up front — no surprises later</span>
<b>The cores' working memory is SRAM</b> — <b>many small macros, one per 256 KiB
block</b> (block == SRAM). Each block has its own port, so thousands of concurrent
accesses run at the same time and access bandwidth scales with core count. And the
SRAM need <i>not</i> hold the whole multi-GB working set: <b>deload</b> streams blocks
between SRAM and SSD in the background (§<a href="#memory">3</a>), so the SRAM holds
only the resident <b>window</b> the cores are working on — drastically smaller than the
working set, and a tunable knob. That is the whole point of building deload: decouple
SRAM size from problem size. SSD is the bulk tier (virtually unlimited), streamed and
prefetched — never the cores' random-access path. <b>Cheapness is not the goal; being
alive is</b> — and a small-window all-SRAM design is alive <i>and</i> affordable.</div>
<div class="win">
<span class="lab">Why this is the right time to map it</span>
The recently-completed statification campaign moved <b>all</b> per-block prover
memory into <b>fixed pools with virtual-offset addressing, a working-set pager, and a
two-format SSD deload path</b> (a byte-identical canonical format for archival
images, a near-memcpy raw format for the eviction hot loop). It was
undertaken for the <b>Fundamental Theorem of Arithmetic campaign</b> — the next
milestone — whose memory and runtime demands exceed those of prior work and require a
bounded, fixed-size memory model. That model is, by construction, what a dedicated
<b>GL processor</b> also requires: a memory hierarchy, single-level address
translation (an MMU), and a cache controller. The two needs are the same steps, taken
once and combined — the software the FTA campaign requires and the data layout silicon
requires coincide. Since then a second campaign statified the <b>transient</b> side as
well: every working structure inside the proof kernel — string scratch, admission and
rejection state, equivalence-class processing, origin records, the disintegration and
integration working forms, the mail absorb — now runs on the same virtual-offset
substrate, and the result is <b>compiler-verified</b>: a semantic call-graph inventory
over the built binaries shows <b>zero heap-using functions on the kernel's compute
paths</b>. Removing the allocator traffic alone made the software ~13% faster on the
regression workload — before any silicon. MPU 0.1 is therefore a transcription of the
running system rather than a forward proposal: the design already runs, in software,
on the machine you have. It is a starting point to build and iterate on, not a
finished part.</div>
<div class="toc">
<strong>What's in here</strong>
<ol>
<li><a href="#compute">What GL computes, in hardware terms</a> — the datapath, why determinism is a gift.</li>
<li><a href="#lb">The Logic Block as one core</a> — the engine, the register line, the phase machine.</li>
<li><a href="#memory">LB memory & its management</a> — pools, the per-block MMU, the pager, SSD deload; what is & isn't static yet.</li>
<li><a href="#mail">The mail system</a> — a pull over shared RAM; the tree is logical, not wiring.</li>
<li><a href="#split">LB split as the runtime lever</a> — the two ways it maps to cores.</li>
<li><a href="#floorplan">The whole-chip floorplan</a> — every GL concept to a hardware block.</li>
<li><a href="#cost">Cost estimation</a> — the two cost axes, the four volume tiers, the multiplier N.</li>
<li><a href="#verdict">The verdict</a> — what works, what's hard, the shrink trajectory.</li>
</ol>
</div>
</section>
<!-- ============================== SECTION 1 ============================== -->
<section id="compute">
<h2><span class="num">1 ·</span> What GL computes, in hardware terms</h2>
<p>
Forget theorem-proving for a moment and look at the workload as a hardware
engineer would. GL is a machine that does one thing in a tight loop: it takes
known facts, looks up rules whose pattern they match, and writes down whatever
those rules conclude — then repeats until nothing new appears. Crucially, the
match step is a <b>hash lookup, not a search</b>: every rule is stored under the
signature of the premise it needs, every fact under its own structural signature,
so "does any rule fire on what I know?" is answered by indexing a table, not by
exploring a tree. Inference is a <b>memory-access problem</b>.
</p>
<p>That single design choice fixes the datapath, and the datapath is friendly:</p>
<div class="stats">
<div class="stat"><div class="big">32-bit</div><div class="lbl">symbol & scope ids (the working width). 64-bit packed statement keys; 64-bit hash digests.</div></div>
<div class="stat"><div class="big">0</div><div class="lbl">floating-point operations on the proof path. None. (The whole prover has one FP compare, and it only picks how to split work.)</div></div>
<div class="stat"><div class="big">352 B</div><div class="lbl">one statement line (<code>IntEncodedExpr</code>) — a fixed, all-int32 record. The natural SRAM line / register width.</div></div>
<div class="stat"><div class="big">FNV-1a</div><div class="lbl">the hash — a per-byte XOR-then-multiply. A few gates, one pipelined multiplier.</div></div>
</div>
<p>
A statement line is a fixed-capacity record: a name id, a handful of flags, and
up to <b>16 arguments</b> (<code>MAX_ARITY</code>), each a 32-bit id — all int32,
176 bytes, identical shape for every fact in the system. A hash key holds up to
<b>8 sub-expressions</b> of those. There are no variable-length structures and no
pointers in the hot record: the engine compares ids, tests set membership and
subset, looks up a packed key, and folds an FNV-1a digest. That is the entire
arithmetic vocabulary of the inner loop. No multiplier array, no FPU, no
transcendental units — the silicon a TPU spends on matrix math, the MPU does not
need at all.
</p>
<h3>Determinism is the feature, not a footnote</h3>
<p>
GL is <b>fully deterministic</b>: the same inputs produce byte-identical outputs
across runs, across thread counts, and <b>across machines</b>. This is enforced
as a project-wide doctrine — every cross-run or cross-host deviation is treated
as a bug — with physical addresses and parallel scheduling order never
observable in the outputs. It survives all the way down to the <b>archival</b>
on-disk deload images, which are a pure function of logical content (element order
in, bytes out). The <b>eviction hot-loop</b> images are the one deliberate
exception — a fast raw memory copy whose bytes are not reproducible but whose
restored state is, so the proof output (which depends only on the state) stays
byte-identical.
</p>
<div class="win">
<span class="lab">Why a hardware designer should care</span>
Determinism without floating point removes the single hardest thing about
parallel accelerators: <b>reproducibility</b>. There is no FP-rounding skew to
reconcile across lanes, no run-to-run drift to chase. A result computed on one
core, a thousand cores, or a farm of chips is <b>bit-identical</b>, so the
external verifier can re-check any proof exactly, and a multi-chip run needs no
consensus protocol to agree on an answer — they cannot disagree. For an ASIC this
is worth a great deal: validation, replay, and scale-out all get simpler at once.
</div>
</section>
<!-- ============================== SECTION 2 ============================== -->
<section id="lb">
<h2><span class="num">2 ·</span> The Logic Block = one core</h2>
<p>
The unit of execution in GL is the <b>Logic Block (LB)</b>. An LB is a
self-contained reasoning context: it owns its own hash rules, its own known
statements, its own scope/validity stack, its own equivalence classes and
provenance map, and its own mailboxes. LBs never reach into each other's memory;
the main thing that crosses between them is mail. The remaining cross-block
effects — induction activation, deferred ancestor admissions, global-rule
updates — travel through analyzer-level deferred-action collectors drained
single-threaded at the cycle boundary, off the parallel hashburst rather than
through any shared-memory access during it. <b>One LB maps to one core.</b> A GL run is a tree of LBs (a goal
spawns sub-blocks for hypotheses, case splits, induction), and the prover sweeps
the whole active set each cycle. <b>MPU 0.1 is built with 32 LB cores</b> — a
one-to-one map of the 32 logical cores GL runs on today. We map what we have: the
~1,757 active LBs of a heavy batch (IncubatorPeano1 — the booklet's own measured
peak, appendix A; not reproduced from a committed run log) stream through those 32
cores 32-at-a-time, just
as they do across 32 CPU threads now, with deload (§<a href="#memory">3</a>) paging
the rest.
</p>
<figure>
<svg viewBox="0 0 760 380" role="img" aria-label="Block diagram of one LB mapped to a core: a control FSM running three phases, a hash-inference engine (the ALU), a register file of statement lines, the LB's container set living in the shared pools, and mail in/out ports">
<defs>
<marker id="lb-ar" viewBox="0 0 10 10" refX="9" refY="5" markerWidth="7" markerHeight="7" orient="auto"><path d="M0 0 L10 5 L0 10 z" fill="#5DCAA5"/></marker>
</defs>
<rect x="20" y="16" width="720" height="348" rx="12" fill="#1C1F2B" stroke="#5DCAA5" stroke-width="2"/>
<text x="40" y="40" fill="#5DCAA5" font-size="13" font-weight="bold">Logic Block = one core</text>
<!-- control FSM -->
<rect x="40" y="56" width="220" height="120" rx="9" fill="#262938" stroke="#B084EB"/>
<text x="150" y="78" fill="#B084EB" font-size="12" font-weight="bold" text-anchor="middle">control FSM</text>
<text x="150" y="95" fill="#8B8FA5" font-size="9.5" text-anchor="middle">three phases per cycle</text>
<rect x="56" y="104" width="188" height="20" rx="4" fill="#1C1F2B" stroke="#3A3D4A"/><text x="150" y="118" fill="#F0E8DC" font-size="9.5" text-anchor="middle">P1 · absorb mail (may discharge)</text>
<rect x="56" y="128" width="188" height="20" rx="4" fill="#3A2E16" stroke="#EF9F27"/><text x="150" y="142" fill="#EF9F27" font-size="9.5" text-anchor="middle">P2 · hashburst (read-only)</text>
<rect x="56" y="152" width="188" height="20" rx="4" fill="#1C1F2B" stroke="#3A3D4A"/><text x="150" y="166" fill="#F0E8DC" font-size="9.5" text-anchor="middle">P3 · commit · discharge · sanitize</text>
<!-- hash engine (ALU) -->
<rect x="280" y="56" width="220" height="120" rx="9" fill="#3A2E16" stroke="#EF9F27" stroke-width="2"/>
<text x="390" y="78" fill="#EF9F27" font-size="12" font-weight="bold" text-anchor="middle">hash-inference engine</text>
<text x="390" y="93" fill="#8B8FA5" font-size="9.5" text-anchor="middle">the "ALU" · int32 + FNV only</text>
<text x="390" y="116" fill="#F0E8DC" font-size="9.5" text-anchor="middle">FNV-1a key → table lookup</text>
<text x="390" y="131" fill="#F0E8DC" font-size="9.5" text-anchor="middle">subset / membership compare</text>
<text x="390" y="146" fill="#F0E8DC" font-size="9.5" text-anchor="middle">bind args · admission gate</text>
<text x="390" y="161" fill="#F0E8DC" font-size="9.5" text-anchor="middle">build conclusion · emit record</text>
<!-- register file -->
<rect x="520" y="56" width="200" height="120" rx="9" fill="#262938" stroke="#5DCAA5"/>
<text x="620" y="78" fill="#5DCAA5" font-size="12" font-weight="bold" text-anchor="middle">register file</text>
<text x="620" y="93" fill="#8B8FA5" font-size="9.5" text-anchor="middle">known statements</text>
<g font-size="8">
<rect x="536" y="104" width="168" height="14" rx="2" fill="#1C1F2B" stroke="#3A3D4A"/><text x="620" y="114" fill="#8B8FA5" text-anchor="middle">IntEncodedExpr line · 352 B · all int32</text>
<rect x="536" y="120" width="168" height="14" rx="2" fill="#1C1F2B" stroke="#3A3D4A"/><text x="620" y="130" fill="#8B8FA5" text-anchor="middle">name · flags · ≤16 arg ids</text>
<rect x="536" y="136" width="168" height="14" rx="2" fill="#1C1F2B" stroke="#3A3D4A"/><text x="620" y="146" fill="#8B8FA5" text-anchor="middle">…</text>
<rect x="536" y="152" width="168" height="14" rx="2" fill="#1C1F2B" stroke="#3A3D4A"/><text x="620" y="162" fill="#8B8FA5" text-anchor="middle">fixed-width rows</text>
</g>
<!-- container set (in shared pools) -->
<rect x="40" y="196" width="680" height="96" rx="9" fill="#20232F" stroke="#5DCAA5"/>
<text x="380" y="216" fill="#5DCAA5" font-size="12" font-weight="bold" text-anchor="middle">the LB's container set — logically private, physically in the shared pools (§3)</text>
<g font-size="9">
<rect x="56" y="228" width="150" height="50" rx="5" fill="#262938" stroke="#EF9F27"/><text x="131" y="248" fill="#EF9F27" text-anchor="middle">hash engine ×4</text><text x="131" y="262" fill="#8B8FA5" text-anchor="middle">rule tables + admission</text>
<rect x="214" y="228" width="150" height="50" rx="5" fill="#262938" stroke="#5DCAA5"/><text x="289" y="248" fill="#5DCAA5" text-anchor="middle">4 statement vectors</text><text x="289" y="262" fill="#8B8FA5" text-anchor="middle">known / local / delta / ext</text>
<rect x="372" y="228" width="150" height="50" rx="5" fill="#262938" stroke="#B084EB"/><text x="447" y="248" fill="#B084EB" text-anchor="middle">scope · equi-classes</text><text x="447" y="262" fill="#8B8FA5" text-anchor="middle">validity · provenance</text>
<rect x="530" y="228" width="174" height="50" rx="5" fill="#262938" stroke="#E879F9"/><text x="617" y="248" fill="#E879F9" text-anchor="middle">goal registry · mail</text><text x="617" y="262" fill="#8B8FA5" text-anchor="middle">to-prove · in/out · logs</text>
</g>
<!-- mail ports -->
<rect x="40" y="308" width="680" height="40" rx="9" fill="#1C1F2B" stroke="#E879F9"/>
<text x="380" y="332" fill="#E879F9" font-size="11" text-anchor="middle">mail ports — pull ancestors' logs from the shared mail pool (§4)</text>
<path d="M260 130 L278 130" stroke="#EF9F27" stroke-width="1.5" marker-end="url(#lb-ar)"/>
<path d="M500 130 L518 130" stroke="#5DCAA5" stroke-width="1.5" marker-end="url(#lb-ar)"/>
</svg>
<figcaption><b>One LB, one core.</b> A control FSM runs three phases per cycle;
the hash engine is the datapath; known statements are the register file; the
container set lives in the shared RAM pools (logically private to the LB); mail is
pulled from ancestors' logs in the shared mail pool (§4). Every block here is a real
software structure, named so you can grep the source.</figcaption>
</figure>
<h3>The elementary step — what the engine does each cycle</h3>
<p>
The engine's job is "fire every rule that can fire on what is currently known,
once." Concretely, per cycle it <b>generates requests</b> (candidate
premise-patterns assembled from known statements), <b>looks each up</b> in the
rule table by its FNV key, and for every hit <b>binds</b> the rule's variables,
checks an <b>admission gate</b>, builds the conclusion, and emits a <b>firing
record</b>. The lookup is O(1) amortised and there is no backtracking on the step
itself — the breadth comes from many LBs firing in the same cycle and exchanging
results through mail at the cycle boundary. In silicon terms it is a streaming
match-and-emit pipeline over a hash table, not a recursive search machine.
</p>
<h3>Three phases, and why the split matters for hardware</h3>
<ul class="inv">
<li><b>Phase 1 — absorb.</b> Pull mail from ancestors, fold it into local rules and
facts so this cycle's request generation sees it. A goal that mail just closed can
deactivate the block here.</li>
<li><b>Phase 2 — hashburst.</b> The compute-heavy part, and <b>strictly read-only on
the block.</b> It captures firings as records and mutates nothing shared. This is
the property that lets phase 2 run on many compute units at once (§5) and is the
hard contract behind the runtime lever.</li>
<li><b>Phase 3 — commit.</b> Single-threaded per block. The captured firings are
merged and applied first — concatenated and sorted into a canonical order (so the
result is independent of how phase 2 was parallelised) in a per-block finalize the
moment the parallel units join, at the tail of phase 2; commit proper then flushes
mail, discharges/deactivates finished goals, sanitises, and wipes closed scopes.</li>
</ul>
<p>
The read-only phase 2 is the linchpin. Because the heavy work touches no shared
state, you can throw cores at it freely and merge deterministically afterwards —
which is exactly what §5 turns into the runtime lever.
</p>
</section>
<!-- ============================== SECTION 3 ============================== -->
<section id="memory">
<h2><span class="num">3 ·</span> LB memory & its management</h2>
<p>
This is the part of GL that was rebuilt to be silicon-ready, so it is the part a
hardware reader should study most. Essentially all of the prover's <b>per-LB</b> working state —
every per-LB payload and the whole mail system — now lives inside <b>fixed
reservations made once at start-up</b>, never grown, never freed during the run
(the bounded exceptions are in the note below). There is no
<code>malloc</code> in the hot path; exhaustion is a loud assert that names the
knob to raise, never a silent fallback. Four reservations, each a candidate for a
physical memory bank:
</p>
<table>
<tr><th>Pool</th><th>Size (provisioned)</th><th>Block</th><th>Backs</th><th>Deloads to SSD?</th></tr>
<tr><td><b>Main</b></td><td class="num">12 GiB</td><td class="num">256 KiB</td><td>all per-LB working containers (the bump arena)</td><td><b>yes</b></td></tr>
<tr><td><b>Persistent</b></td><td class="num">1 GiB</td><td class="num">32 KiB</td><td>the goal registry — kept always-resident so deactivation logic can read it while a block is cold</td><td>no</td></tr>
<tr><td><b>Mail</b></td><td class="num">2 GiB</td><td class="num">256 KiB</td><td>the cross-block mail log (who sent what to whom)</td><td>no</td></tr>
<tr><td><b>LB-body</b></td><td class="num">2 GiB</td><td class="num">256 KiB</td><td>the block objects themselves (fixed slots, never moved)</td><td>no</td></tr>
</table>
<p>
Total program-start reservation: <b>17 GiB</b>, fixed. These are <i>ceilings</i>,
not consumption — the sizing knob you would tune for a real part is the
<i>measured peak</i>, which §7 puts (from the booklet's own dated figures) at
roughly 1 GB for the named theorem batches and ~4–5 GB for the heaviest exploration
batch. The "provisioned vs. measured" gap
is the whole reason the cost story has a hot tier and a cold tier.
</p>
<h3>The hierarchy is pool → block → page → per-LB arena</h3>
<figure>
<svg viewBox="0 0 760 430" role="img" aria-label="The static memory hierarchy: one pool reservation carved into 256 KiB blocks, each LB's arena carves blocks into 8 KiB pages, containers pack fixed records into pages and address them by a virtual offset resolved with one shift and one mask">
<defs><marker id="h2-ar" viewBox="0 0 10 10" refX="9" refY="5" markerWidth="7" markerHeight="7" orient="auto"><path d="M0 0 L10 5 L0 10 z" fill="#5DCAA5"/></marker></defs>
<rect x="20" y="14" width="720" height="96" rx="10" fill="#1C1F2B" stroke="#EF9F27" stroke-width="2"/>
<text x="380" y="36" fill="#EF9F27" font-size="12" font-weight="bold" text-anchor="middle">POOL — one reservation at start-up (Main = 12 GiB = 49152 blocks)</text>
<text x="380" y="52" fill="#8B8FA5" font-size="9.5" text-anchor="middle">the software model of the SRAM-macro fabric — block == one 256 KiB SRAM · carved under one mutex · never grown</text>
<g font-size="8.5">
<rect x="40" y="64" width="64" height="32" rx="4" fill="#262938" stroke="#5DCAA5"/><text x="72" y="84" fill="#5DCAA5" text-anchor="middle">LB A</text>
<rect x="112" y="64" width="64" height="32" rx="4" fill="#262938" stroke="#5DCAA5"/><text x="144" y="84" fill="#5DCAA5" text-anchor="middle">LB A</text>
<rect x="184" y="64" width="64" height="32" rx="4" fill="#262938" stroke="#B084EB"/><text x="216" y="84" fill="#B084EB" text-anchor="middle">LB B</text>
<rect x="256" y="64" width="64" height="32" rx="4" fill="#262938" stroke="#E879F9"/><text x="288" y="84" fill="#E879F9" text-anchor="middle">LB C</text>
<rect x="328" y="64" width="64" height="32" rx="4" fill="#20232F" stroke="#3A3D4A"/><text x="360" y="84" fill="#8B8FA5" text-anchor="middle">free</text>
<rect x="400" y="64" width="64" height="32" rx="4" fill="#20232F" stroke="#3A3D4A"/><text x="432" y="84" fill="#8B8FA5" text-anchor="middle">free</text>
<rect x="472" y="64" width="64" height="32" rx="4" fill="#20232F" stroke="#3A3D4A"/><text x="504" y="84" fill="#8B8FA5" text-anchor="middle">free</text>
<rect x="544" y="64" width="64" height="32" rx="4" fill="#20232F" stroke="#3A3D4A"/><text x="576" y="84" fill="#8B8FA5" text-anchor="middle">free</text>
<rect x="616" y="64" width="104" height="32" rx="4" fill="#20232F" stroke="#3A3D4A"/><text x="668" y="84" fill="#8B8FA5" text-anchor="middle">… 256 KiB blocks</text>
</g>
<path d="M216 110 L216 150" stroke="#5DCAA5" stroke-width="1.5" marker-end="url(#h2-ar)"/>
<text x="130" y="134" fill="#8B8FA5" font-size="9.5" text-anchor="middle">acquireBlock (mutex)</text>
<rect x="80" y="152" width="600" height="96" rx="10" fill="#262938" stroke="#5DCAA5" stroke-width="2"/>
<text x="380" y="174" fill="#5DCAA5" font-size="12" font-weight="bold" text-anchor="middle">PER-LB ARENA — this LB's blocks, carved into 8 KiB pages</text>
<g font-size="8.5">
<rect x="104" y="186" width="150" height="40" rx="4" fill="#1C1F2B" stroke="#5DCAA5"/><text x="179" y="202" fill="#5DCAA5" text-anchor="middle">block 0</text><text x="179" y="216" fill="#8B8FA5" text-anchor="middle">32 pages × 8 KiB</text>
<rect x="262" y="186" width="150" height="40" rx="4" fill="#1C1F2B" stroke="#5DCAA5"/><text x="337" y="202" fill="#5DCAA5" text-anchor="middle">block 1</text><text x="337" y="216" fill="#8B8FA5" text-anchor="middle">32 pages × 8 KiB</text>
<rect x="420" y="186" width="150" height="40" rx="4" fill="#1C1F2B" stroke="#EF9F27"/><text x="495" y="202" fill="#EF9F27" text-anchor="middle">block 2</text><text x="495" y="216" fill="#8B8FA5" text-anchor="middle">▸ free pages</text>
</g>
<path d="M380 248 L380 286" stroke="#5DCAA5" stroke-width="1.5" marker-end="url(#h2-ar)"/>
<text x="470" y="272" fill="#8B8FA5" font-size="9.5" text-anchor="middle">allocPage → virtual offset (vid)</text>
<rect x="80" y="288" width="600" height="84" rx="10" fill="#3A2E16" stroke="#EF9F27" stroke-width="2"/>
<text x="380" y="310" fill="#EF9F27" font-size="12" font-weight="bold" text-anchor="middle">CONTAINER — packs fixed records into pages, stores virtual offsets</text>
<g font-size="8.5">
<rect x="150" y="322" width="32" height="22" rx="3" fill="#262938" stroke="#5DCAA5"/><text x="166" y="337" fill="#F0E8DC" text-anchor="middle">e0</text>
<rect x="186" y="322" width="32" height="22" rx="3" fill="#262938" stroke="#5DCAA5"/><text x="202" y="337" fill="#F0E8DC" text-anchor="middle">e1</text>
<rect x="222" y="322" width="32" height="22" rx="3" fill="#262938" stroke="#5DCAA5"/><text x="238" y="337" fill="#F0E8DC" text-anchor="middle">e2</text>
<text x="300" y="337" fill="#8B8FA5" text-anchor="start">… packed contiguously within a page</text>
</g>
<text x="380" y="362" fill="#8B8FA5" font-size="9.5" text-anchor="middle">no physical pointers stored — only the virtual offset</text>
<!-- MMU resolve callout -->
<rect x="500" y="14" width="0" height="0"/>
</svg>
<figcaption><b>One reservation, blocks, per-LB pages.</b> A global manager hands
out 256 KiB blocks under a mutex; each LB carves its blocks into 8 KiB pages and
packs fixed-width records into them. The only cross-core touch in the whole
hierarchy is that one mutex.</figcaption>
</figure>
<h3>The virtual-offset arena is a tiny per-LB MMU</h3>
<p>
Containers never store a physical address. They store a <b>32-bit virtual
offset</b>, and a resolve step turns it into a pointer on every access:
</p>
<pre><code>physical = blocks[ offset >> 18 ] + ( offset & 0x3FFFF )
└ which SRAM macro ┘ └ address within that 256 KiB SRAM ┘</code></pre>
<p>
One shift, one mask, one add — because the block size is a power of two. This is
exactly an MMU's page-table-walk collapsed to a single level, and it buys two
things at once: <b>determinism</b> (the offset is a pure function of allocation
order, so nothing observable depends on which physical block the data landed in)
and <b>relocatability</b> (a block can be written to disk and reloaded anywhere
without rewriting a single stored offset). In hardware this is a small adder and a
register holding the block-base table — cheap, and replicated per core.
</p>
<p>
<b>And in the MPU each block is one small SRAM macro</b> — block == SRAM. The resolve
above is a (macro-select, intra-macro-address) decode. The cores random-access only
these macros, and because each block has <b>its own port</b>, accesses to different
blocks happen <i>at the same time</i> — that concurrency, scaling with core count, is
the whole basis of the runtime lever (§<a href="#split">5</a>). And the SRAM holds only the resident
<b>window</b>: the pager (below) keeps the macros the cores are working on, and
<b>deload streams the rest from SSD</b>, so the physical SRAM is far smaller than the
4 GiB pool — the working set lives on SSD; the SRAM is just the hot window.
</p>
<p>
<b>One core addresses many macros, and the count flexes with the problem.</b> A core's
arena is not a single fixed SRAM — it spans <b>as many 256 KiB macros as its LB
currently needs</b>, and the resolve's macro-select field picks among them. Macros are
granted on demand (<code>acquireBlock</code>) as an LB grows and returned when it
shrinks or discharges, so a trivial LB holds one or two while a fat one (the heavy
Gauss blocks reach ~13 MiB ≈ <b>dozens of macros</b>) holds many. The macros are a
shared pool the steward apportions across the 32 cores by live demand — so the
SRAM-per-core <b>adjusts to problem complexity dynamically</b>, rather than a fixed
per-core partition. One core handles trivial and hard problems alike; it just draws
more macros for the hard ones.
</p>
<h3>The pager is a cache controller</h3>
<p>
RAM is treated as a <b>cache of the working set</b> — the blocks being processed
now plus the next few. A background <b>steward</b> thread maintains that window
every cycle: it prefetches the blocks about to be needed and, when memory gets
tight, evicts the rest to SSD, biggest first. A worker that reaches a block still
on disk loads it itself and deloads the biggest out-of-window block in exchange.
The policy is pure watermarks on pool occupancy:
</p>
<ul class="inv">
<li><b>Below 50% full</b> — the steward is parked. No eviction, so no reload. A light batch
runs at full speed with zero disk traffic.</li>
<li><b>Cross 50%</b> — the steward wakes (asynchronously) and drains: each reload is paid for by
evicting the biggest out-of-window block (<b>one-for-one</b>), pulling occupancy down to a
<b>40% floor</b> before it parks again. The 50%→40% gap is a hysteresis band, so it never
oscillates at the wake mark.</li>
<li><b>Above ¾ (75%)</b> — the <b>synchronous hard water</b>: a worker that needs a block while the
pool is this full does the swap itself — load its block, evict the biggest out-of-window block —
rather than wait for the steward, which above this mark mass-evicts.</li>
<li><b>Working set itself won't fit</b> — that is a genuinely too-small pool, and
the run stops at a loud assert. A 30-second stuck-detector turns any unexpected
wait into an assert too.</li>
</ul>
<p>
For the MPU this is the cache controller between the SRAM hot tier and the
SSD cold tier. The eviction <i>timing</i> can vary with load, but — by
construction — the <b>proof output never does</b>: what to discharge is decided at
a single-threaded barrier from deterministic block state, and the pager only moves
bytes, never changes them.
</p>
<h3>SSD deload / reload is the cold tier</h3>
<p>
Blocks move to and from SSD in <b>two formats</b>, chosen by purpose. The
<b>eviction hot loop</b> — the pager cycling live blocks in and out under memory
pressure — uses a <b>raw arena image</b>: a near-memcpy byte copy of the block's
live memory pages plus a small map of which pages are live. Because every
container (including its throw-away hash index) packs its pages into the one block
arena, and the tiny per-container bookkeeping lives in the never-evicted block
shell, the page image is a complete record: reload binds the same page ids to
freshly-packed pages and reads the bytes straight back — no element walk, no
index rebuild, one copy. This is what makes the cold-tier stream run at
<b>memory-copy bandwidth</b>, which the block-granular datapath (and the optional
DRAM L2 below) is sized for. The price, accepted deliberately: raw image bytes are
<b>not reproducible</b> (fragmentation leaks into them), so they are not
byte-comparable — but the restored logical state is identical, which is all the
proof output depends on.
</p>
<p>
The <b>discharge / archival</b> path (a block that leaves the working set for
good, and the read-only proof-export reloads) instead uses the <b>canonical</b>
format: containers streamed element by element, in logical order. Its byte stream
is a <b>pure function of logical content</b> — two blocks with the same contents
produce identical files regardless of fragmentation, so these images ARE
byte-comparable across runs and machines. The format is self-describing (a
<code>GLDL</code> magic, a version, a per-block ordinal as the filename, a per-tag
directory, the block's full identity chain verbatim, then fixed-width
little-endian payload). Reload rebuilds the containers onto a fresh, compact arena
and is allowed only at a handful of enumerated touch points; touching cold storage
anywhere else is an assert, not a degraded read. <b>This SSD cold tier is the
lever that makes memory virtually unlimited:</b> an SSD is cheap and enormous.
</p>
<div class="note">
<b>Optional, not in the current design: a DRAM L2.</b> The current design is two
tiers — <b>SRAM (L1)</b>, the cores' working window, and <b>SSD (L3)</b>, the cold
backing store. A <b>DRAM L2</b> could sit between them as a <i>deload-staging
cache</i>: the steward pre-uploads the next blocks from SSD into DRAM and parks
just-deloaded blocks there before they trickle out to SSD, hiding SSD latency on the
streaming path. It would be <b>block-granular and off the cores' random-access
path</b> — staging whole 256 KiB blocks as they move between SRAM and SSD, never
serving a core's random access. A future option; MPU 0.1 is <b>SRAMs + SSD</b>.
</div>
<h3>What is <i>not</i> static — the complete accounting</h3>
<div class="caveat">
<span class="lab">Stated plainly</span>
The first campaign moved all per-LB <b>persistent state — including the mail
system</b> — into the static pools; the second statified the kernel's <b>transient
scratch</b>: each worker's working memory is two per-worker arenas drawn from the
same pool and released whole at the end of each task, so a core's scratch is a
<b>fixed, enumerable SRAM budget</b>, not an open-ended allocator. <b>Mail is static:</b> the cross-block log, global ids, and transient inboxes live on the
dedicated mail pool; each outbox, its private interner, and the internal channels
live on the LB's deloadable main-pool arena (§<a href="#mail">4</a>). None is on the malloc heap. Within the
block-memory subsystem, two things genuinely remain on the ordinary heap:
<ul style="margin:8px 0 0">
<li><b>The global pool's recycle queue</b> — one process-wide root that hands out
blocks — and the compaction's transient scratch. O(blocks), not O(payload), and
outside any one LB. (Each arena's own list of which blocks/pages it holds — once
the last per-LB heap carve-out — is now pool-backed: a small-buffer directory that
keeps a tiny arena's table inline at zero pool cost and spills only a large one
onto pool blocks. So the per-LB arena bookkeeping is now static too.)</li>
<li><b>Transient mail strings</b> — each deloadable outbox stores int32 ids from
its own private interner; commit translates them into <b>global mail-interner
int32 ids</b> for the retained log and receiver inbox. The
persistent log <i>bytes</i> are static; the absorb/pull side now decodes the frozen
blob bytes straight into the receiving block's static columns with no heap working
form at all. What still touches the heap is the short-lived encoding at the
single-threaded commit and load seams — a bounded, per-cycle residue off the
parallel compute path.</li>
</ul>
<b>What this means for silicon.</b> The persistent state — payloads, mail, and the
per-LB arena bookkeeping — is static, and the per-worker working scratch is itself
drawn from the statified pool and returned per task; the only ordinary read/write
heap a host process keeps is the global pool's recycle queue, the compaction's
transient scratch, and a staging area for mail serialisation at the single-threaded
seams. The heap residue is bounded and per-cycle, not
per-LB growth — so "mail is on the heap" would be wrong; only its transient
encoding is. (In the proof kernel — <code>performElem1/2/3</code> — the ONLY heap
permitted is generating the <code>hashburst_trace.txt</code> debug dump, which is off
the compute path and not silicon-mapped; the kernel's production paths are
compiler-verified heap-free. The compiled-definition (config) layer remains the one
data-on-heap residual — read through zero-allocation probes during the burst, and on
silicon that layer is ROM. So the precise claim is "the kernel's compute paths are
heap-free; the config layer is heap-resident data behind static read fences; transient
heap encoding survives only at the single-threaded commit and load seams," not "zero
heap process-wide.")
</div>
</section>
<!-- ============================== SECTION 4 ============================== -->
<section id="mail">
<h2><span class="num">4 ·</span> The mail system — a pull over shared RAM (the tree is logical)</h2>
<p>
LBs do not share working memory; they exchange results through <b>mail</b> at cycle
boundaries, and mail is, logically, a <b>tree</b>: a block reads only mail authored
by its direct ancestors (parent, grandparent, …, root) — never a sibling, never
upward, never an unrelated subtree. That tree is a <i>software access pattern</i>, not
a connectivity property of the silicon: it does not make the interconnect any sparser.
</p>
<p>
Physically, mail is <b>random-access reads into a shared log pool</b>: a receiver
reads its ancestors' logs at arbitrary addresses, and the interconnect must be able
to reach <i>every</i> address — because the LB tree is built at <b>run time</b>
(blocks spawn as goals split), each log lands at an <b>unpredictable address</b>
(blocks are granted in nondeterministic order under the pool mutex, so different LBs'
batches interleave anywhere in the pool), and the root, as everyone's ancestor, is
read by <i>all</i>. Connectivity cannot be narrowed to a graph that does not exist
until run time and whose logs sit at unpredictable addresses. The tree only bounds
<i>which</i> cells a given receiver touches, not what the hardware must address — it is
random access either way.
</p>
<figure>
<svg viewBox="0 0 760 330" role="img" aria-label="Mail is random-access reads into a shared retained-log pool. Cores on the left connect through an any-to-any memory NoC to a shared mail pool on the right that holds per-LB retained chains and a global mail-id table. A highlighted receiver reads its ancestors' chains at arbitrary addresses; delivered pages and the id table may be recycled between cycles when no block was born dormant, while routing and cumulative cursors remain resident.">
<defs><marker id="m-ar" viewBox="0 0 10 10" refX="9" refY="5" markerWidth="7" markerHeight="7" orient="auto"><path d="M0 0 L10 5 L0 10 z" fill="#EF9F27"/></marker></defs>
<text x="380" y="22" fill="#5DCAA5" font-size="12" font-weight="bold" text-anchor="middle">Mail = random-access reads into a shared log pool</text>
<!-- cores -->
<text x="58" y="48" fill="#8B8FA5" font-size="9" text-anchor="middle">LB cores + cold mailOut</text>
<rect x="20" y="58" width="78" height="30" rx="6" fill="#262938" stroke="#EF9F27"/><text x="59" y="78" fill="#EF9F27" font-size="9.5" text-anchor="middle">core (here)</text>
<rect x="20" y="108" width="78" height="30" rx="6" fill="#262938" stroke="#5DCAA5"/><text x="59" y="128" fill="#F0E8DC" font-size="9.5" text-anchor="middle">core</text>
<rect x="20" y="158" width="78" height="30" rx="6" fill="#262938" stroke="#5DCAA5"/><text x="59" y="178" fill="#F0E8DC" font-size="9.5" text-anchor="middle">core</text>
<rect x="20" y="208" width="78" height="30" rx="6" fill="#262938" stroke="#5DCAA5"/><text x="59" y="228" fill="#F0E8DC" font-size="9.5" text-anchor="middle">core</text>
<!-- NoC switch -->
<rect x="150" y="58" width="64" height="180" rx="8" fill="#1C1F2B" stroke="#B084EB" stroke-width="2"/>
<text x="182" y="148" fill="#B084EB" font-size="10.5" text-anchor="middle" transform="rotate(-90 182 148)">memory NoC — any to any</text>
<!-- cores to NoC (all connect) -->
<path d="M98 73 L150 96" stroke="#3A3D4A" stroke-width="1"/>
<path d="M98 123 L150 118" stroke="#3A3D4A" stroke-width="1"/>
<path d="M98 173 L150 158" stroke="#3A3D4A" stroke-width="1"/>
<path d="M98 223 L150 198" stroke="#3A3D4A" stroke-width="1"/>
<!-- shared mail pool -->
<rect x="300" y="50" width="440" height="196" rx="10" fill="#20232F" stroke="#E879F9" stroke-width="2"/>
<text x="520" y="70" fill="#E879F9" font-size="10.5" font-weight="bold" text-anchor="middle">shared mail pool — retained chains + global ids + transient mailIn</text>
<rect x="330" y="86" width="120" height="22" rx="4" fill="#3A2E16" stroke="#EF9F27"/><text x="390" y="101" fill="#EF9F27" font-size="9" text-anchor="middle">root log (hot)</text>
<rect x="560" y="92" width="80" height="22" rx="4" fill="#262938" stroke="#5DCAA5"/><text x="600" y="107" fill="#8B8FA5" font-size="9" text-anchor="middle">log Q</text>
<rect x="430" y="132" width="120" height="22" rx="4" fill="#262938" stroke="#5DCAA5"/><text x="490" y="147" fill="#8B8FA5" font-size="9" text-anchor="middle">log P (ancestor)</text>
<rect x="648" y="150" width="72" height="22" rx="4" fill="#262938" stroke="#5DCAA5"/><text x="684" y="165" fill="#8B8FA5" font-size="9" text-anchor="middle">log R</text>
<rect x="340" y="180" width="80" height="22" rx="4" fill="#262938" stroke="#5DCAA5"/><text x="380" y="195" fill="#8B8FA5" font-size="9" text-anchor="middle">log S</text>
<rect x="520" y="196" width="80" height="22" rx="4" fill="#262938" stroke="#5DCAA5"/><text x="560" y="211" fill="#8B8FA5" font-size="9" text-anchor="middle">log T</text>
<rect x="630" y="198" width="90" height="22" rx="4" fill="#2D2538" stroke="#E879F9"/><text x="675" y="213" fill="#E879F9" font-size="8.5" text-anchor="middle">global mail ids</text>
<!-- NoC reaches all addresses (faint) -->
<path d="M214 110 L330 97" stroke="#3A3D4A" stroke-width="1"/>
<path d="M214 120 L560 103" stroke="#3A3D4A" stroke-width="1"/>
<path d="M214 140 L430 143" stroke="#3A3D4A" stroke-width="1"/>
<path d="M214 150 L648 161" stroke="#3A3D4A" stroke-width="1"/>
<path d="M214 170 L340 191" stroke="#3A3D4A" stroke-width="1"/>
<path d="M214 180 L520 207" stroke="#3A3D4A" stroke-width="1"/>
<!-- highlighted receiver pull: core(here) -> NoC -> root log + log P -->
<path d="M98 73 L150 88" stroke="#EF9F27" stroke-width="2"/>
<path d="M214 95 L328 97" stroke="#EF9F27" stroke-width="2" marker-end="url(#m-ar)"/>
<path d="M214 105 L428 143" stroke="#EF9F27" stroke-width="2" marker-end="url(#m-ar)"/>
<text x="380" y="272" fill="#8B8FA5" font-size="10" text-anchor="middle">The receiver reads its ancestors' logs (root + parent) at ARBITRARY addresses — the wiring must reach every cell.</text>
<text x="380" y="290" fill="#8B8FA5" font-size="10" text-anchor="middle">The "tree" is which logs a receiver picks (software). The LB tree is built at run time and logs land at unpredictable addresses.</text>
<text x="380" y="308" fill="#EF9F27" font-size="10" text-anchor="middle">root log is read by EVERY core (it is everyone's ancestor) — a hotspot, not a sparse fan-in.</text>
</svg>
<figcaption><b>Random access into shared RAM — the tree is logical, not wiring.</b>
Mail is a pull: each receiver reads its ancestors' logs out of one shared pool, at
arbitrary addresses. Because the LB tree is built at run time and a log lands at an
unpredictable address (nondeterministic grant order under the pool mutex), the
interconnect must reach every address (an any-to-any memory NoC).
The tree bounds <i>which</i> logs a receiver reads, not what the silicon must
address — and the root, read by all, is a hotspot. The earlier "tree, not a
crossbar" framing was wrong: it is random access either way.</figcaption>
</figure>
<h3>The mux is a pull over retained log windows</h3>
<p>
Concretely: each block writes the mail it emits <b>once</b>, into its own
retained chain, at a single-threaded commit point each cycle. A receiver, in its
phase 1, walks its ancestor list and <b>pulls</b> the batches it has not yet
ingested from each ancestor's log, advancing a private per-(receiver, ancestor)
cursor. There is no outbound copy and no shared inbox to contend on — the parallel
readers only read frozen logs and bump their own cursor cells. That is the mux:
<b>select-and-merge at the receiver</b> — but the selection is by <i>memory
address</i> (which ancestor logs to read), over a shared pool the core can address
in full.
</p>
<p>
Retention is chosen once when the run-time LB grid is complete. If every block is
active, the post-phase-3 barrier recycles the delivered blob/reference pages before
resetting the matching global mail-id table and opening a fresh window at the next
commit. If any block is born dormant, the complete history and id table remain so
that block can catch up when activated. In both modes the
ancestor routing edges, cumulative producer counts, and receiver cursors stay in
always-on RAM. For silicon this turns the common incubator case into a bounded
rolling mail working set without changing the provisioned pool, address fabric, or
mail protocol.
</p>
<h3>Three mail channels — which SRAM is always-on</h3>
<p>This split tells you exactly which memory must stay powered and resident:</p>
<table>
<tr><th>Channel</th><th>Home</th><th>Always-on?</th></tr>
<tr><td>routing inbox (<code>mailIn</code>)</td><td>the mail pool</td><td><b>yes</b> until phase-1 absorb; blocks then returned</td></tr>
<tr><td>routing outbox + private ids (<code>mailOut</code>)</td><td>the block's main-pool arena</td><td>no — deloads after phase 3; pending blocks reload one at a time for commit</td></tr>
<tr><td>cross-block retained window + global id table (the mux)</td><td>dedicated mail pool</td><td><b>yes</b> — never deloaded; both may be recycled at the safe seam</td></tr>
<tr><td>internal one-step channels</td><td>the block's deloadable arena</td><td>no — pages out with the block</td></tr>
</table>
<p>
A mail message carries proved statements (including compact rule forms) plus
provenance lines; on large batches provenance dominates. There is exactly
<b>one</b> cross-block path that is not the ancestor pull — a point-to-point deposit
addressed from the root to one tree node — and effects that travel <i>up</i> the
tree are not mail at all (single-threaded collectors drained after the join). Net
for the floorplan: an <b>any-to-any memory interconnect to the shared pools, plus a
small always-on mail SRAM</b> — not a crossbar of message links, but not a sparse
tree either. What the tree <i>does</i> buy is access <b>locality</b> (a receiver
reads only its ancestor chain, not all <code>N</code> logs); what it does
<b>not</b> buy is cheaper wiring. In this shared-memory model the real scaling limit
is <b>memory bandwidth and contention on hot cells</b> (the root log, the shared
pools), not interconnect topology — the caveat §5 and §7 carry into the runtime
lever.
</p>
<h3>The mux, in hardware: a banked crossbar</h3>
<p>
That any-to-any memory access is a <b>standard banked crossbar</b> (a network-on-chip
at larger scale): the SRAM macros are independent banks, and an N-port crossbar lets
all 32 cores reach memory <b>in parallel as long as they hit different banks</b>; two
cores hitting the same bank serialize — a <b>bank conflict</b>. This is not exotic — it
is exactly how <b>GPU shared memory</b> works (32 banks; a warp's lanes run in one
transaction unless they collide on a bank, where an <i>n</i>-way conflict serialises
into <i>n</i>). The hot cells of §<a href="#split">5</a> (the root mail log, read by
every block) are that bank-conflict case by another name.
</p>
<p>
It exists off the shelf as IP, not a discrete chip. On the FPGA prototype you drop in a
configurable non-blocking crossbar — e.g. <b>AMD/Xilinx LogiCORE IP AXI SmartConnect</b>
(product guide <b>PG247</b>); for the ASIC, a mesh NoC such as <b>Arm CoreLink
CMN-700</b> or <b>Arteris FlexNoC</b>. A fully non-blocking crossbar costs ~O(N×M)
area — trivial at 32 ports (GPU territory); at thousands of macros you group them into
banks or move to the NoC, which trades the guaranteed-parallel crossbar for
near-parallel routing with occasional internal blocking.
</p>
</section>
<!-- ============================== SECTION 5 ============================== -->
<section id="split">
<h2><span class="num">5 ·</span> LB split = scaling runtime across cores</h2>
<p>
This is the runtime lever. Before the static rebuild, a hard calculation lived
inside a single block (or a couple) and ran at the speed of one thread — the work
of one LB's hashburst was a sequential lump. <b>LB split</b> breaks that lump
across cores: because phase 2 is read-only on the block (§2), the candidate-firing
work can be partitioned, run on many compute units at once, and merged
deterministically. A heavy LB is partitioned by <b>expression search</b>, not by rule
owner: one read-only producer enumerates expression stumps over the whole LB, deals
them into at most one bucket per logical core, and each bucket accepts every rule
while generating only requests that contain one of its stumps. A block therefore
spreads across <b>min(expression buckets, cores available)</b>. The larger headroom
belongs to the <i>whole workload's</i> flat task pool across all active blocks, not to
a single block.
</p>
<p>The expression partition matters for silicon because it divides one irregular
search without adding a block-memory write port. A recordable short combination that
would disappear when the producer advances to a larger level is retained as a
<b>terminal pre-stump</b>: one bucket validates that combination through the normal
request path but does not grow it, while the larger child stumps cover all larger
combinations. No valid request is discarded.</p>
<p>The user named two ways to realise this in silicon. Both already exist in the
software, in two different subsystems:</p>
<figure>
<svg viewBox="0 0 760 320" role="img" aria-label="Two ways to split. Left: N compute units share one LB's memory read-only, each takes an expression-stump bucket while accepting every rule, and results merge in canonical sorted order — the main prover. Right: clone the LB's facts N times, run an independent slice on each core — the counterexample filter.">
<defs><marker id="s-ar" viewBox="0 0 10 10" refX="9" refY="5" markerWidth="7" markerHeight="7" orient="auto"><path d="M0 0 L10 5 L0 10 z" fill="#5DCAA5"/></marker></defs>
<!-- model a -->
<rect x="14" y="14" width="365" height="292" rx="10" fill="#1C1F2B" stroke="#EF9F27"/>
<text x="196" y="34" fill="#EF9F27" font-size="12" font-weight="bold" text-anchor="middle">(a) Shared memory, N compute units</text>
<text x="196" y="50" fill="#8B8FA5" font-size="9.5" text-anchor="middle">the live main-prover model</text>
<rect x="116" y="60" width="160" height="40" rx="6" fill="#20232F" stroke="#5DCAA5"/><text x="196" y="78" fill="#5DCAA5" font-size="10" text-anchor="middle">ONE LB's memory</text><text x="196" y="92" fill="#8B8FA5" font-size="8.5" text-anchor="middle">read-only during phase 2</text>
<g font-size="9">
<rect x="34" y="128" width="100" height="46" rx="6" fill="#3A2E16" stroke="#EF9F27"/><text x="84" y="148" fill="#EF9F27" text-anchor="middle">unit 0</text><text x="84" y="162" fill="#8B8FA5" text-anchor="middle">stump bucket 0</text>
<rect x="146" y="128" width="100" height="46" rx="6" fill="#3A2E16" stroke="#EF9F27"/><text x="196" y="148" fill="#EF9F27" text-anchor="middle">unit 1</text><text x="196" y="162" fill="#8B8FA5" text-anchor="middle">stump bucket 1</text>
<rect x="258" y="128" width="100" height="46" rx="6" fill="#3A2E16" stroke="#EF9F27"/><text x="308" y="148" fill="#EF9F27" text-anchor="middle">unit 2</text><text x="308" y="162" fill="#8B8FA5" text-anchor="middle">stump bucket 2</text>
</g>
<path d="M120 100 L84 126" stroke="#5DCAA5" stroke-width="1.2" marker-end="url(#s-ar)"/>
<path d="M196 100 L196 126" stroke="#5DCAA5" stroke-width="1.2" marker-end="url(#s-ar)"/>
<path d="M272 100 L308 126" stroke="#5DCAA5" stroke-width="1.2" marker-end="url(#s-ar)"/>
<path d="M84 174 L180 214" stroke="#5DCAA5" stroke-width="1.2" marker-end="url(#s-ar)"/>
<path d="M196 174 L196 214" stroke="#5DCAA5" stroke-width="1.2" marker-end="url(#s-ar)"/>
<path d="M308 174 L212 214" stroke="#5DCAA5" stroke-width="1.2" marker-end="url(#s-ar)"/>
<rect x="96" y="216" width="200" height="44" rx="6" fill="#262938" stroke="#5DCAA5"/><text x="196" y="234" fill="#5DCAA5" font-size="10" text-anchor="middle">merge — canonical SORT</text><text x="196" y="248" fill="#8B8FA5" font-size="8.5" text-anchor="middle">result independent of N & order</text>
<text x="196" y="286" fill="#8B8FA5" font-size="9" text-anchor="middle">"N copies of phase 2 within an LB"</text>
<text x="196" y="300" fill="#8B8FA5" font-size="9" text-anchor="middle">multiplies compute, shares the memory</text>
<!-- model b -->
<rect x="395" y="14" width="351" height="292" rx="10" fill="#1C1F2B" stroke="#B084EB"/>
<text x="570" y="34" fill="#B084EB" font-size="12" font-weight="bold" text-anchor="middle">(b) Clone the memory N times</text>
<text x="570" y="50" fill="#8B8FA5" font-size="9.5" text-anchor="middle">the live counterexample-filter model</text>
<rect x="490" y="60" width="160" height="40" rx="6" fill="#20232F" stroke="#B084EB"/><text x="570" y="78" fill="#B084EB" font-size="10" text-anchor="middle">facts template</text><text x="570" y="92" fill="#8B8FA5" font-size="8.5" text-anchor="middle">deep-copied per work item</text>
<g font-size="9">
<rect x="420" y="128" width="96" height="80" rx="6" fill="#262938" stroke="#B084EB"/><text x="468" y="150" fill="#B084EB" text-anchor="middle">clone → core 0</text><text x="468" y="166" fill="#8B8FA5" text-anchor="middle">own memory</text><text x="468" y="182" fill="#8B8FA5" text-anchor="middle">slice 0</text><text x="468" y="198" fill="#8B8FA5" text-anchor="middle">full CE check</text>
<rect x="522" y="128" width="96" height="80" rx="6" fill="#262938" stroke="#B084EB"/><text x="570" y="150" fill="#B084EB" text-anchor="middle">clone → core 1</text><text x="570" y="166" fill="#8B8FA5" text-anchor="middle">own memory</text><text x="570" y="182" fill="#8B8FA5" text-anchor="middle">slice 1</text><text x="570" y="198" fill="#8B8FA5" text-anchor="middle">full CE check</text>
<rect x="624" y="128" width="96" height="80" rx="6" fill="#262938" stroke="#B084EB"/><text x="672" y="150" fill="#B084EB" text-anchor="middle">clone → core 2</text><text x="672" y="166" fill="#8B8FA5" text-anchor="middle">own memory</text><text x="672" y="182" fill="#8B8FA5" text-anchor="middle">slice 2</text><text x="672" y="198" fill="#8B8FA5" text-anchor="middle">full CE check</text>
</g>
<path d="M530 100 L478 126" stroke="#B084EB" stroke-width="1.2" marker-end="url(#s-ar)"/>
<path d="M570 100 L570 126" stroke="#B084EB" stroke-width="1.2" marker-end="url(#s-ar)"/>
<path d="M610 100 L662 126" stroke="#B084EB" stroke-width="1.2" marker-end="url(#s-ar)"/>
<text x="570" y="240" fill="#8B8FA5" font-size="9" text-anchor="middle">each clone fully independent —</text>
<text x="570" y="254" fill="#8B8FA5" font-size="9" text-anchor="middle">only its own result slot is written</text>
<text x="570" y="286" fill="#8B8FA5" font-size="9" text-anchor="middle">"copy memory N times, distribute"</text>
<text x="570" y="300" fill="#8B8FA5" font-size="9" text-anchor="middle">multiplies memory and compute</text>
</svg>
<figcaption><b>Two splits, both real.</b> Model (a) — many read-only units over
one shared memory, merged by a sort — is how the main prover splits one heavy
block today. Model (b) — clone the state per core and run an independent slice —
is how the counterexample filter parallelises across thousands of candidate
checks. An MPU can do either or both: (a) for one giant calculation, (b) for many
independent ones.</figcaption>
</figure>
<h3>Why the merge is a sort, and why that matters</h3>
<p>
In model (a) the units do not deposit their firings as they go; each writes its
own record list, and a single-threaded per-block finalize step — the tail of
phase 2, once the parallel units join — <b>concatenates and sorts</b> them by a
total content key before applying. The sort is the whole trick: it makes the merged result a
function of <i>content</i>, not of which unit found what first or how many units
there were. So <b>2 cores and 200 cores produce byte-identical output</b> — the
runtime lever costs you nothing in reproducibility. (And because phase 2 wrote
nothing to the block, bucket tasks may execute in any order with no partial state
to clean up.)
</p>
<h3>How much it splits, adaptively</h3>
<p>
Every main-path burst runs to completion. At the end of an iteration, GL compares
each LB's deterministic total submatch work with the balanced per-core share and a
minimum setup threshold. A straggler is pre-split for the next iteration into up to
<code>logicalCores</code> expression buckets; an LB that falls below the threshold
returns to one part. A newly activated induction-zero LB takes the split path once
immediately because no prior statistic exists. This spends parallelism where the
completed work shows it can shorten the makespan, without a timing-dependent trigger.
<b>MPU 0.1 maps the current host's approximately 32 logical workers to 32 LB cores</b>;
more independent LBs and expression buckets remain queued in the flat phase-2 pool.
</p>
<div class="caveat">
<span class="lab">What feeds the cores — and the residual ceiling</span>
Cores are cheap; <b>feeding them</b> is the hard part. Every core does random accesses
into the shared memory (§4), so the lever only works if the memory can serve thousands
of those at once. That is precisely why the memory is <b>many small SRAM macros, one
per block</b> (§<a href="#cost">7.1</a>): each block is its own port, so aggregate
bandwidth scales with core count. The residual limit is not raw
bandwidth but a few <b>hot cells</b> (above all the root mail log, read by every
block) plus the serial fractions (phase 3, the per-cycle mail barrier). So scaling is
sub-linear, but the parallel phase-2 fraction — almost all the work — is what the SRAM
fabric is built to feed.
</div>
</section>
<!-- ============================== SECTION 6 ============================== -->
<section id="floorplan">
<h2><span class="num">6 ·</span> The MPU floorplan</h2>
<p>
Put the pieces together and the chip draws itself. The MPU is a <b>fabric of 32 LB
cores</b> (§2) over an <b>any-to-any memory network-on-chip</b> to the shared RAM
pools (§4); the <b>resident window</b> of the working set lives in <b>SRAM — many
small macros, one per block</b> (§3) — the full multi-GB working set is far larger
and streams from SSD — with a <b>steward / cache controller</b> paging blocks between
the SRAM fabric and an <b>SSD cold tier</b> (§3), under a thin <b>host interface</b> that loads axioms
and streams proofs out. Split (§5) is realised by giving each core
several phase-2 compute lanes and/or by cloning a core's state across the fabric.
</p>
<figure>
<svg viewBox="0 0 760 420" role="img" aria-label="MPU whole-chip floorplan: a grid of 32 LB cores with phase-2 lanes, connected by an any-to-any memory NoC to a fabric of small SRAM macros, with a steward cache controller managing the SRAM fabric and an SSD cold tier, under a host interface.">
<defs><marker id="fp-ar" viewBox="0 0 10 10" refX="9" refY="5" markerWidth="7" markerHeight="7" orient="auto"><path d="M0 0 L10 5 L0 10 z" fill="#5DCAA5"/></marker></defs>
<rect x="16" y="14" width="728" height="392" rx="14" fill="#15171F" stroke="#5DCAA5" stroke-width="2"/>
<text x="40" y="38" fill="#5DCAA5" font-size="13" font-weight="bold">MPU 0.1 — floorplan</text>
<!-- host -->
<rect x="40" y="50" width="680" height="30" rx="7" fill="#262938" stroke="#8B8FA5"/>
<text x="380" y="70" fill="#F0E8DC" font-size="11" text-anchor="middle">host interface — load axioms / config · stream proofs out (PCIe / CXL)</text>
<!-- core fabric -->
<rect x="40" y="92" width="480" height="208" rx="10" fill="#1C1F2B" stroke="#EF9F27"/>
<text x="280" y="112" fill="#EF9F27" font-size="11" font-weight="bold" text-anchor="middle">LB-core fabric — 32 cores (one per Logic Block)</text>
<g font-size="7.5">
<!-- a 3x3 sample of cores -->
<g>
<rect x="56" y="124" width="146" height="52" rx="5" fill="#262938" stroke="#EF9F27"/>
<text x="92" y="138" fill="#EF9F27" text-anchor="middle">core</text>
<rect x="120" y="128" width="76" height="20" rx="3" fill="#1C1F2B" stroke="#5DCAA5"/><text x="158" y="142" fill="#5DCAA5" text-anchor="middle">SRAM I/O</text>
<rect x="60" y="150" width="40" height="22" rx="3" fill="#3A2E16" stroke="#EF9F27"/><text x="80" y="164" fill="#EF9F27" text-anchor="middle">P2 ×k</text>
<rect x="104" y="150" width="42" height="22" rx="3" fill="#20232F" stroke="#B084EB"/><text x="125" y="164" fill="#B084EB" text-anchor="middle">FSM</text>
<rect x="150" y="150" width="46" height="22" rx="3" fill="#20232F" stroke="#5DCAA5"/><text x="173" y="164" fill="#5DCAA5" text-anchor="middle">regs</text>
</g>
<rect x="216" y="124" width="146" height="52" rx="5" fill="#262938" stroke="#EF9F27"/><text x="289" y="154" fill="#8B8FA5" text-anchor="middle">core (P2 lanes)</text>
<rect x="376" y="124" width="128" height="52" rx="5" fill="#262938" stroke="#EF9F27"/><text x="440" y="154" fill="#8B8FA5" text-anchor="middle">core …</text>
<rect x="56" y="186" width="146" height="52" rx="5" fill="#262938" stroke="#EF9F27"/><text x="129" y="216" fill="#8B8FA5" text-anchor="middle">core …</text>
<rect x="216" y="186" width="146" height="52" rx="5" fill="#262938" stroke="#EF9F27"/><text x="289" y="216" fill="#8B8FA5" text-anchor="middle">core …</text>
<rect x="376" y="186" width="128" height="52" rx="5" fill="#262938" stroke="#EF9F27"/><text x="440" y="216" fill="#8B8FA5" text-anchor="middle">core …</text>
<rect x="56" y="248" width="448" height="42" rx="5" fill="#20232F" stroke="#E879F9"/><text x="280" y="273" fill="#E879F9" text-anchor="middle" font-size="10">memory NoC (any → any) — cores ↔ shared pools; mail is a pull pattern (§4)</text>
</g>
<!-- steward + memory tiers -->
<rect x="536" y="92" width="184" height="208" rx="10" fill="#1C1F2B" stroke="#B084EB"/>
<text x="628" y="112" fill="#B084EB" font-size="11" font-weight="bold" text-anchor="middle">steward</text>
<text x="628" y="126" fill="#8B8FA5" font-size="8.5" text-anchor="middle">cache controller</text>
<text x="628" y="139" fill="#8B8FA5" font-size="8.5" text-anchor="middle">40/50/75% watermarks</text>
<rect x="552" y="150" width="152" height="80" rx="6" fill="#262938" stroke="#5DCAA5"/><text x="628" y="171" fill="#5DCAA5" font-size="9.5" text-anchor="middle">SRAM — hot tier</text><text x="628" y="187" fill="#8B8FA5" font-size="8" text-anchor="middle">the resident window</text><text x="628" y="200" fill="#8B8FA5" font-size="8" text-anchor="middle">many small macros</text><text x="628" y="213" fill="#8B8FA5" font-size="8" text-anchor="middle">block == SRAM</text>
<path d="M628 230 L628 244" stroke="#5DCAA5" stroke-width="1.2" marker-end="url(#fp-ar)"/>
<rect x="552" y="246" width="152" height="44" rx="6" fill="#262938" stroke="#E879F9"/><text x="628" y="265" fill="#E879F9" font-size="9.5" text-anchor="middle">SSD — cold tier</text><text x="628" y="279" fill="#8B8FA5" font-size="8" text-anchor="middle">deload · virtually unlimited</text>
<!-- always-on note -->
<rect x="40" y="312" width="680" height="78" rx="10" fill="#20232F" stroke="#3A3D4A"/>
<text x="380" y="332" fill="#F0E8DC" font-size="10.5" font-weight="bold" text-anchor="middle">always-on (never deloaded): goal registry · mail log · block-object store  |  deloadable: per-LB working containers</text>
<text x="380" y="352" fill="#8B8FA5" font-size="9.5" text-anchor="middle">Cores touch only SRAM (many small macros, block == SRAM). The SRAM holds the resident window; deload streams the rest from SSD.</text>
<text x="380" y="370" fill="#8B8FA5" font-size="9.5" text-anchor="middle">The expected GL shrink (100–1000×) cuts the macro count, shrinking the SRAM toward a single cheap die.</text>
</svg>
<figcaption><b>The whole chip.</b> A core fabric over an any-to-any memory NoC to
the shared pools, a steward paging <b>two</b> tiers — the SRAM-macro fabric (hot)
and SSD (cold). The SRAM holds only the working window — deload streams the
rest from SSD — so it is far smaller than the working set; the shrink (§8) cuts it
further.</figcaption>
</figure>
<h3>Every GL concept maps to a hardware block</h3>
<p>This extends the short correspondence already in the GL user documentation:</p>
<table class="map">
<tr><th>GL concept</th><th>Silicon</th><th>Note</th></tr>
<tr><td>logic block</td><td>a core</td><td>logically self-contained; peers exchange only via mail (shared pools underneath)</td></tr>
<tr><td>hash-inference engine</td><td>match-and-emit datapath</td><td>FNV unit + int32 compare/subset; no FPU</td></tr>
<tr><td>known statements</td><td>register file / SRAM lines</td><td>fixed 352-byte all-int32 records</td></tr>
<tr><td>per-LB containers</td><td>blocks in the SRAM-macro fabric (block == SRAM)</td><td>virtual-offset = (macro-select, intra-macro address)</td></tr>
<tr><td>phase-2 split parts</td><td>compute lanes per core</td><td>read-only; merged by a sort</td></tr>
<tr><td>mail (pull from ancestors)</td><td>any-to-any memory NoC</td><td>tree = access pattern, not wiring; the root log is a hotspot</td></tr>
<tr><td>the steward / pager</td><td>cache controller</td><td>SRAM macros ↔ SSD, watermark policy</td></tr>
<tr><td>SSD deload format</td><td>cold-tier page format</td><td>byte-identical across runs & hosts</td></tr>
<tr><td>cycle boundary</td><td>a global barrier / clock edge</td><td>mail commits here; results merge here</td></tr>
<tr><td>determinism doctrine</td><td>no consensus needed</td><td>chips cannot disagree on a result</td></tr>
</table>
</section>
<!-- ============================== SECTION 7 ============================== -->
<section id="cost">
<h2><span class="num">7 ·</span> Cost estimation</h2>
<p>
Here is the money. Two ground rules first. <b>One:</b> the numbers below are
<i>order-of-magnitude</i>, dated, and concentrated in the
<a href="#constants">constants appendix</a> so they can be refreshed at release
without touching the prose. <b>Two:</b> this section prices the
<span style="color:var(--amber)">N</span> in
<code>value = (1 + N) × (is GL real?)</code>. It does <b>not</b> argue the second factor —
that is what the FTA campaign is for. If GL is not real math automation, every
dollar below buys nothing. If it is, every dollar buys a multiplier.
</p>
<p>The cost has two axes and they are wildly unequal:</p>
<ul class="inv">
<li><b>Memory dominates.</b> GL's working set today is gigabytes (§3). Holding and
moving that is essentially the entire cost.</li>
<li><b>Compute is nearly free by comparison.</b> An LB core is an integer
match-and-emit pipeline with an FNV unit and no FPU (§1–2). Cores are small; you
can afford a great many of them.</li>
</ul>
<h3>7.1 · Memory — the cost driver: many small SRAMs</h3>
<p>
The measured peak working set (full pipeline) is ~1 GB for the named theorem batches
and ~4–5 GB for the heaviest exploration batch — but that is what lives on <b>SSD</b>,
not what must be in SRAM. The cores random-access <b>SRAM</b> only, built as <b>many
small macros, one per 256 KiB block</b> (block == SRAM, §<a href="#memory">3</a>): each
block is its own port, so thousands of concurrent accesses serve the 32 cores at once and
the runtime lever holds. And the SRAM holds the resident <b>window</b> of the