pure/docs/research, branch masterVerified execution runtime unifying state, persistence, and replication.
http://git.yeowoo.org/pure/atom?h=master2026-10-19T10:58:43Z029: principle 1 broken on UAX #14 (045), written as its own rule asks: (a) 2.19x against 4x, its premise wrong (the source already keeps t.cls[i] in locals: the reads only the proof merges are 16.4 of 549.9), (b) 1.31x against 3x, and the path capped (interpretation is 22 of an instruction's 74 machine instructions: stitching bodies gives at most 1.42x); what was tested (step() on constant instructions, frame and checks as they are) and what was not (an emitter given the proof, the general JIT 008 forbids); where it goes (runtime machinery: a call 1,375, a stored read 331, the lists 22,651 a point) and the 7x the batch lanes give that a fn in a block loses; the 1,774 and 3.2-3.9 ns corrected (the budget's count: 549.9 run, 11.7 ns each) here and in 140; the op counts kept2026-10-19T10:58:43Zeunhhunecpition205@gmail.com2026-10-19T10:58:43Zurn:sha1:3b127e6193026188939f0c8b06fb769518deaef5115: the modules replaced are freed (0 bytes a change over 4,000, was 19,284), how, what checks it (586 of 600 loads at a freed address, answers right; ASan clean), what a mutant comparing addresses showed (nothing: requests hold their module and freeing waits a pass), the push group woken again, the bindings left (24 B an input a module); the bank's queries within 0.4% (s50, s51); CHECKPOINT's remaining list without it2026-10-19T09:01:53Zeunhhunecpition205@gmail.com2026-10-19T09:01:53Zurn:sha1:de1c3dd822c7bd6ae01c510a53372445b1b993ea140: determinism across builds at 027, 028 and 140's state: record_all.py's 486 runs (41 modules) the same with gcc and clang on the Pi (Pure 0896b38, aup 1efe1c7; aup's modules the same bytes under clang); the Mac and WSL2 not reached (ssh timed out, no route), the bundle and r140.sh ready for them2026-10-19T07:20:42Zeunhhunecpition205@gmail.com2026-10-19T07:20:42Zurn:sha1:1f9ddc8a16d7bda640ce2e6c19126c2491c95ec7140: LIST_VALUE's copy reviewed before building (measured by spec: UAX #14 about 10% of its time, JSON tree 6%, HTTP 2%, inflate 0.06%, the rest none; the cost a tree built item by item, 64 ns an item and 250 ns a copy): lend and detach (CoW) noted as the decision point (a branch on every event list's change for 10/6/2/0/0/0), a compile-time move ruled out (it changes LIST_VALUE's contract), the arrays copied whole built (UAX #14 -6.8%, its share to about 3%); 041's five works within 0.03% (b49, b50), the bank's queries within 0.3% (s49, s50), noise between builds larger2026-10-19T07:05:53Zeunhhunecpition205@gmail.com2026-10-19T07:05:53Zurn:sha1:4a7e780278df740e5e37c3307fe687405df72448140: aup's frictions written away and the apps measured again (no core change, no new opcode): lists declared together, targets together (straight when no value can read what a target changes), a list given a list value whole, abs, tick.period, hex where numbers go; lines to Python 1.47-2.04x (were 1.47-2.15x): UAX #14 176 to 169, layout 116 to 110, HTTP 148 to 146 and its last workaround gone; instructions of the four whose modules changed within 0.2%, inflate's and UAX #14's modules the same; the six specs' checks pass on the three paths, module_specs nine; RTO's checks no longer rewrite G (tick.period); the suite table's rows 5, 8 and 92026-10-19T06:34:12Zeunhhunecpition205@gmail.com2026-10-19T06:34:12Zurn:sha1:f1bb9de4ac72136a1b0722ce77ac4ea6fd4fa413140: the decision section before 8 and 10 points to their sections; 8's Python count holds the four lines of its left-to-right total (116 against 50 without them)2026-10-19T05:25:53Zeunhhunecpition205@gmail.com2026-10-19T05:25:53Zurn:sha1:fc13b251f6d244df31d5b4100dc421e3f3fe685a140's 8, box layout, written in aup with no new opcode (aup's examples/layout.aup: a subset of CSS Flexbox 1 written down first, one line, row or column, padding, gap, six justify-content, four align-items, grow and shrink with 9.7's loop, cross sizes stretched, nothing sized by content): 2,000 random trees (29,388 nodes; 7,659 items frozen at their padding by the loop) are Taffy 0.15's within 0.01 (layout_taffy, built by cargo; the worst 8.3e-5) and layout.py's bit for bit on the three paths, the paths the same; the single-pass subset first tried refused 66% of trees, so the loop came in; Taffy given min sizes equal to the padding (given 0 it floors at 0 while resolving lengths, where 9.7 floors the content box), the reference adding from the left (sum compensates since Python 3.12); module_specs in make check: 100 trees (tests/specs/layout); bars: 116 lines against Python's 54, 4,754 ns a node, Taffy's 644 (7.4x), pure Python 5,396 (Pure 1.14x faster), 1,494 instructions a node (9.7's loop 44%); four frictions; aup's rows read by position no longer copy (99,067 ns a node before); the suite table's row 8; CHECKPOINT's direction row2026-10-19T05:18:49Zeunhhunecpition205@gmail.com2026-10-19T05:18:49Zurn:sha1:6215b1177e377b512aaa1296faa6311f809135f2140's 10, RFC 6298's retransmission timer, written in aup with no new opcode (aup's examples/rto.aup, the timer a deadline in the state seen at each periodic tick): 20 scenarios (10 seeds, ticks every 10 and 100 ms; a closed loop: first sendings lost one in five, the receiver acknowledging cumulatively) and their 241,612 events right against rto.py, the model of the same rules (no known implementation takes given events), on the three paths, the paths the same; module_specs in make check: one scenario at both periods (tests/specs/rto, 2,297 events); bars: one workaround (the periodic tick: 2,795.8 ticks a timeout at 10 ms, 281.6 at 100, seen 4.27 and 49.23 ms late on average; ticks 93% and 57% of the counted work), 56 lines against Python's 30, three frictions (an input's period not readable, no abs, send a keyword); the one-shot timer's shape as a decision point, one spec needing it: noted, not made; the suite table's row 102026-10-19T04:54:45Zeunhhunecpition205@gmail.com2026-10-19T04:54:45Zurn:sha1:8071832bc7857634f66c94592b27b188c882ea54028 and 140: list values' copying measured a second time (UAX #14's Text record copies its nine lets' lists a line: with building them, 260 of 1,774 instructions a code point, after inflate's code()), and a keyed list's floor seek (the last item keyed x or below) first wanted (UAX #14's ranges, a binary search by position, 360 instructions a code point), one spec behind it2026-10-19T04:46:11Zeunhhunecpition205@gmail.com2026-10-19T04:46:11Zurn:sha1:475f35cb45a77dc41029126370887fd33b332800140's 5, line breaking (UAX #14, Unicode 16.0), written in aup with no new opcode (aup's examples/linebreak.aup, the properties as data: 2,787 ranges from the UCD 16.0 Vega's text is frozen at, built by Vega's text/unicode.py, loaded once): every line of LineBreakTest.txt (16,672) and 2,000 random lines (their boundaries as linebreak.py, the Python reference, which passes the test whole, works them out) right on the three paths, the paths' outputs the same; module_specs in make check: the ranges and the lines kept in tests/specs/linebreak (derived from the UCD, the Unicode License v3's notice), run by pure-run --views; bars: written, no workaround (three frictions: hex literals always i64, number no let's name, a let's list one a line), 176 lines against Python's 99, 6,920 ns a code point against Vega's C 34.7 (199x), pure Python 2,523 (Pure 2.7x slower), 1,774 instructions a code point (setup 260, the ranges' binary search 360, decide about 1,150 a boundary); the decisions before 8 (box layout: Taffy can be fetched by cargo, a subset to choose first; as a handler) and 10 (a one-shot timer is a core primitive one spec needs: noted, not made); the suite table's row 5; CHECKPOINT's direction row2026-10-19T04:42:00Zeunhhunecpition205@gmail.com2026-10-19T04:42:00Zurn:sha1:c545227f2461e92afc38a0e1317a288e8c653cc6