Uniform Barrington's Theorem - #15

Closed

SamuelSchlesinger wants to merge 75 commits into

devfrom

agent/uniform-barrington

Commits on Jul 22, 2026

feat(circuits): prove textbook Barrington bound
SamuelSchlesinger
committed
3dbe8e1
feat(circuits): unfold circuit outputs to formulas
SamuelSchlesinger
committed
08920e4
feat(circuits): define depth classes and bridge NC1
SamuelSchlesinger
committed
efd1465
feat(circuits): add executable Barrington compiler
SamuelSchlesinger
committed
9cf4c10
feat(circuits): encode width-five branching programs
SamuelSchlesinger
committed
f111718
feat(circuits): specify Barrington code generation
SamuelSchlesinger
committed
8cf928e
feat(classes): define uniform Barrington boundary
SamuelSchlesinger
committed
ec5bd6c
feat(classes): bound uniform Barrington code size
SamuelSchlesinger
committed
43fdd7b
feat(tm): suppress append-only output in finite control
SamuelSchlesinger
committed
ac14d31
feat(tm): add binary output-position probe
SamuelSchlesinger
committed
406a87f
feat(tm): prove marker-safe output probe runs
SamuelSchlesinger
committed
377562e
feat(tm): bound output probe replay space
SamuelSchlesinger
committed
f3d35dc
feat(circuits): add streaming Barrington traversal
SamuelSchlesinger
committed
33973d3
feat(tm): canonicalize output probe capture
SamuelSchlesinger
committed
12ab096
feat(tm): capture arbitrary transducer output bits
SamuelSchlesinger
committed
5f947bd
feat(tm): add restartable output probes
SamuelSchlesinger
committed
6a16919
feat(circuits): add fixed-address Barrington slots
SamuelSchlesinger
committed
9ea5f20
feat(tm): bound complete output probe queries
SamuelSchlesinger
committed
18e6cc0
feat(circuits): query fixed Barrington slots directly
SamuelSchlesinger
committed
991f86e
feat(circuits): query Barrington slots from postfix tokens
SamuelSchlesinger
committed
2ac0c30
feat(circuits): query and serialize Barrington bits
SamuelSchlesinger
committed
19c34b7
feat(circuits): query Barrington programs through probes
SamuelSchlesinger
committed
94ceb80
feat(tm): blank bounded sparse work prefixes
SamuelSchlesinger
committed
27ab637
feat(tm): reset restartable output probes
SamuelSchlesinger
committed
2acdf53
feat(tm): clean output probe work frames
SamuelSchlesinger
committed
42c1fd9
feat(tm): compose restartable output probes
SamuelSchlesinger
committed
b664ee7
feat(barrington): add scan-based probe controller foundation
SamuelSchlesinger
committed
cc6c89a
feat(barrington): latch probe bits for serialization
SamuelSchlesinger
committed
2efac6b
feat(tm): totalize output position probes
SamuelSchlesinger
committed
9210bcb
feat(tm): totalize restartable output probes
SamuelSchlesinger
committed
831682d
feat(tm): add dynamically indexed output probes
SamuelSchlesinger
committed
8c79e7d
feat(tm): dispatch dynamically indexed probes
SamuelSchlesinger
committed
a97b41c
feat(tm): reset output latches before dispatch
SamuelSchlesinger
committed
8feb77f
refactor(tm): expose bounded BinaryFor segments
SamuelSchlesinger
committed
cb970d5
feat(tm): add bounded output probe scans
SamuelSchlesinger
committed
61cb440
feat(tm): count ones through output probes
SamuelSchlesinger
committed
ed6979a
feat(tm): certify output probe prefix counts
SamuelSchlesinger
committed
3dc2a44
feat(tm): derive segment space from entry bounds
SamuelSchlesinger
committed
bf6f028
feat(tm): derive count scans from source space
SamuelSchlesinger
committed
65593c3
feat(tm): add output-probe unary decoder
SamuelSchlesinger
committed
6ded0bd
feat(tm): certify active unary probe steps
SamuelSchlesinger
committed
638e443
feat(tm): certify unary decoder body branches
SamuelSchlesinger
committed
3cca33d
feat(tm): unify unary decoder step semantics
SamuelSchlesinger
committed
fa687e5
feat(tm): certify bounded unary decode segments
SamuelSchlesinger
committed
56194d6
feat(tm): add fixed tag probe decoder
SamuelSchlesinger
committed
1de3d40
feat(tm): certify fixed tag probe runs
SamuelSchlesinger
committed
96b0dd4
feat(tm): dispatch decoded formula tags
SamuelSchlesinger
committed
2851149
feat(tm): share formula token decoder layout
SamuelSchlesinger
committed
991dca1
feat(tm): normalize formula token dispatch
SamuelSchlesinger
committed
fb217bf
feat(tm): compose normalized token decoding
SamuelSchlesinger
committed
7a56593
feat(tm): wire variable token decoding
SamuelSchlesinger
committed
1fe3238
feat(tm): expose bounded loop Hoare contracts
SamuelSchlesinger
committed
5144c66
feat(tm): certify bounded decoder contracts
SamuelSchlesinger
committed
4d28997
feat(tm): certify variable token decoding
SamuelSchlesinger
committed
9c97331
feat(bp): add instruction serializer machine
SamuelSchlesinger
committed
5a2ec2f
feat(bp): emit decoded leaf instructions
SamuelSchlesinger
committed
02e7a26
feat(bp): certify decoded leaf dispatch
SamuelSchlesinger
committed
231959a
feat(bp): expose recursive query boundary
SamuelSchlesinger
committed
1bb6468
feat(bp): add stack-free slot cursor
SamuelSchlesinger
committed
75828b7
feat(bp): reduce slot descent to two bits
SamuelSchlesinger
committed
b2939f3
feat(bp): dispatch recursive slot bits
SamuelSchlesinger
committed
624cd7d
feat(bp): capture and position slot bits
SamuelSchlesinger
committed
5de220f
feat(bp): certify slot address positioning
SamuelSchlesinger
committed
3e5090b
feat(bp): compose initial slot dispatch
SamuelSchlesinger
committed
2cad194

Commits on Jul 23, 2026

feat(bp): certify recursive slot descent
SamuelSchlesinger
committed
42716be
feat(formula): certify forward child split
SamuelSchlesinger
committed
d229ce5
feat(tm): expose binary equality Hoare contracts
SamuelSchlesinger
committed
d3e0d62
feat(tm): normalize binary equality cursors
SamuelSchlesinger
committed
58ccac6
feat(bp): certify forward scan core
SamuelSchlesinger
committed
e30d424
feat(bp): certify forward token updates
SamuelSchlesinger
committed
9169745
feat(bp): connect token decoding to forward scan
SamuelSchlesinger
committed
347eb51
feat(bp): certify decoded forward scan steps
SamuelSchlesinger
committed
de13b81
feat(bp): transport forward scan frames
SamuelSchlesinger
committed
8868f32
feat(bp): bound decoded forward scans
SamuelSchlesinger
committed
987c46f

Commits on Jul 24, 2026

feat(bp): expose forward scan prefix invariants
SamuelSchlesinger
committed
389e200