Repository navigation
spec(t27f): live_graph_export -- the gx_ graph-data plane (per-node/per-edge accessors, name region, gx_apply_event, gx_replay) - #12148
Merged
Conversation
…er exports: per-node and per-edge accessors (gx_node_count/gx_node_kind/gx_node_name_ptr/gx_node_name_len, gx_edge_count/gx_edge_kind/gx_edge_from/gx_edge_to), the node NAME region tiled above the contract's MEM_CAP (one 32-byte row per node slot; a SPEC node inside the feed's join carries the fixture's own path from a 196-byte local table -- str consts are not runtime-readable in the current gen, measured, the #5980 family -- every other node the 11-byte tagged form), the LOG region of 64 whole #12005 records, gx_apply_event(kind, tick, task) refreshing the live triple into staged row 0 and applying through work_graph's law verbatim, gx_replay(ptr, len) walking whole records with the law's own partial semantics, and refusal band 36 (the one live_struct_glue left empty) with E_GX_LEN/E_GX_PTR while E_STATE/E_LAYOUT stay the contract's by import; 7/7 tests green (70,675 runtime asserts, 0 vacuous, mutation-proven), 3 invariants proved; the two-node round-trip pins the full 69,640-byte image equality with the direct law, and the 24-event fixture replays to the same digest. Refs #12005, advances #10262.
…ruct is the graph-data plane of the wasm memory image (the law's own WorkGraph 557,120 bits + the 2,048-byte log region with its commit + the 65,536-byte name region with its live extent), 1,097,855 bits measured by the checker; ledgered in the same lane as the spec, the #12005 lesson applied one PR earlier. Refs #12005, advances #10262.
Contributor
Summary by t27-beesChecked by the t27 compilert27c parse, parse-complete and typecheck on each changed .t27 file at
Read by the modelThis spec adds the GRAPH-DATA plane ( Worth a look
Read: 2 files, +819 -0, the whole diff. Head |
gHashTag
added a commit
that referenced
this pull request
Oct 25, 2026
The wasm32 law grows its linear memory: SEC_MEMORY 5 / SEC_DATA 11, the min-form limits (mem_limits_min), pages_for_bytes (MEM_CAP 143,692 -> 3 pages, the gx card's end 211,276 -> 4), the MVP active data entry (flags 0x00, i32.const offset, end, uleb length, bytes), the memory export entry (export_entry_kind, kind 0x02), and compose_module_mem -- compose_module's five sections with the memory section between function and export and the data section after code (ids stay ascending 1,3,5,7,10,11). The stateless compose_module is untouched: floor 7's 117-byte trio capstone still pins its bytes, and the new capstone proves the A/B/A in one test -- the same descriptor set composes 39 bytes stateless (export at 19, no memory section) and 61 bytes with one page and 'abc' at offset 4 (export at 24, the memory section's five bytes between). 71/71 tests, 0 vacuous, mutation control kills (n==61 -> 62 fails, restored). gen-rust regenerated with stdout redirect; the wasm seal re-saved through tri seals changed (drift 0, coverage OK, currency 0 stale). Passive segments and the DataCount section are NOT CLAIMED. Refs #12148, advances #10262, #5980.
gHashTag
added a commit
that referenced
this pull request
Oct 25, 2026
The stateful law's second floor: the global section (SEC_GLOBAL 6) with global_type (valtype + mutability byte), global_entry_i32 (type + i32.const init + end) and global_body (pre-joined entries behind a vector count); the memory-backed slot instructions the wide state lowers through -- i32.load 0x28 and i32.store 0x36 with their memarg (uleb alignment, uleb static offset; uleb(143692) = CC E2 08 pinned), the layout plane's own cap -- and global.get 0x23 / global.set 0x24. compose_module_mem grows the globals parameter and splices the global section between memory (5) and export (7); the capstone pins the 69-byte module (floor 12's 61 + the global section's eight bytes) with every section boundary and the memory export entry five bytes right. QUESTION 2 answered and measured: the card's regions are rows, so they are memory-backed slots; the narrow live scalars are the globals; mutable globals are NOT EXPORTED (the memory is the one exported window). 74/74 tests, 0 vacuous; mutation control kills (n==69 -> 70 fails, restored). gen-rust regen (stdout redirect), seal re-saved (drift 0, coverage OK, currency 0 stale). Refs #12148, advances #10262, #5980.
gHashTag
added a commit
that referenced
this pull request
Oct 25, 2026
… records the landing and QUESTION 4 (the walk floors and the emitter-mount budget stop) data_section now routes vec_prefix through the uleb cursor (no unused binding -- the generated Rust adds no warning over master's one pre-existing code_section warning); 74/74 tests, 0 vacuous, seal re-saved. The plan block now states what landed (floors 12-13, with their capstones and mutation controls) and QUESTION 4 names the measured stop: floors 14-16 are spec-side walk work (relax REF_LOCAL_VARIABLE, FACT_ROW reserved word 11 for the local count, While-to-loop lowering, call-index mapping), but the emitter mount needs a ~200-line adapter in cli/t27b/src/wasm32_emitter.rs that the foreign budget (40/file, 80/PR, shrink-only) does not admit -- the two lawful paths are named and neither is assumed. Refs #12148, advances #10262, #5980.
Collaborator
Author
STATUS: stateful floor law -- floors 12-13 landed on
|
gHashTag
added a commit
that referenced
this pull request
Oct 25, 2026
…he memory export, compose_module_mem (min+max limits) and floor 13 globals/load/store survive on #12152's vocabulary; 77/77, mutation-checked, resealed Master's #12152 landed this lane's floor-12 section law under its own names (pages_for, memtype, data_segment_active, memory_section, data_section). The rebase drops this branch's parallel bodies (pages_for_bytes, mem_limits_min, memory_body, data_entry and the colliding memory_section/data_section) and keeps what master lacks: EXPORT_KIND_FUNC/MEM, export_entry_kind, export_body_mem, the stateful composer compose_module_mem (now min+max limits, fail-closed on min>max and max>65536), and floor 13 in full (SEC_GLOBAL, global_type, global_entry_i32, global_body, i32.load/i32.store memargs, global.get/set). The 62-byte stateful leaf and the 70-byte global module pin every section boundary; the code-section body length is pinned 6 against master's own whole-module vector (one hand-pin was caught red by the suite). The A/B/A holds inside the capstone: the stateless composer still emits the 39-byte answer module beside the stateful one. Mutations killed: n==62 and the memory-export kind byte. Refs #12148, advances #10262, #5980.
Collaborator
Author
|
STATUS: the page-side consumer of this law card has landed as a dormant branch of /t27f/live/ -- Trinity-S-AI-DNA/trinity#1744 (t27f_live.js feature-detects the gx_ surface; gx_replay feeds the whole re-encoded log, gx_apply_event walks it per event on the tick grid; nodes/names/edges are read from linear memory, kind colors SPEC amber / AGENT blue / TASK violet / ACTION grey / ARTIFACT green, PRODUCES edges in the particle color). Verified in Node against a mock module answering the gx_ surface with work_graph.t27's own semantics: load path, live path and all silent fallbacks green; today's trio-only wasm leaves the page exactly as it was. The day the stateful-floor lane serves a module with these exports, the graph switches to the law's own topology with zero further PRs on the page. |
gHashTag
added a commit
that referenced
this pull request
Oct 25, 2026
…he windowed refusal, one i32 group per body); 81/81, mutation-checked, resealed Floor 8 refused every var at or beyond nparams; floor 14 opens the local window without moving one byte under it. FACT_ROW's reserved word 11 becomes the fn's i32 local count (fact_put_locals writes it, fact_put still writes 0, fact_locals_n reads it); refused_local_variable_w and expr_refusal_w read var_idx against nparams + locals_n (floor 8's fn is the locals_n 0 case, construct and detail byte for byte); fn_body_bytes_locals grows ONE i32 local group ahead of the floor-9 body (skipped at 0); walk_prog_locals writes each admitted fn's count as a u32le row beside its descriptor and lowers through the windowed body; code_entries_locals and compose_module_mem_l carry the group into the code entry. Capstones: the third(a,b) local leaf pins the group bytes 01 7F ahead of local.get 2 and the seven-byte code entry, with the A/B/A in-test (the same table with the window closed rederives the floor-10 bytes); the 64-byte stateful leaf carries the group beside the 62-byte one. Two hand-pins were caught red by the suite before landing (the code body length 6, the 62-byte leaf's const offset 48). Mutation killed: the group valtype 0x7F -> 0x7E. The 117-byte trio is untouched: walk_prog_locals over a locals-free table is walk_prog. Refs #12148, advances #10262, #5980.
gHashTag
added a commit
that referenced
this pull request
Oct 25, 2026
…t kinds, BS_STMTS_RETURN, the fn gate admits it); 85/85, mutation-checked, resealed gx_replay's While lowers as a node sequence the walk owns: EK_WHILE_OPEN (loop 03 40), EK_COND_BR (br_if, var_idx the depth), EK_LOOP_END (end), EK_LOAD32/EK_STORE32 (floor 13's memargs packed in node_v: align low 32, offset high 32), EK_LOCAL_SET (floor 14's window's write side). One new body shape BS_STMTS_RETURN lowers a payload of statement and expression nodes then the trailing return; the four expression kinds delegate to lower_expr_node byte for byte. stmt_refusal_w admits the statement kinds (the window and operator checks stay through the delegation); fn_refusal admits the shape with body_r's verdict -- BS_OTHER still refuses and the zero-param const gate is untouched. Capstones: the count-down while pins all 17 body bytes (03 40 | 20 00 | 0D 00 | 20 00 41 01 6B 21 00 | 0B | 20 00 | 0B) with the A/B/A in-test (the same fn as floor 10's shape is the three-byte leaf); the whole-prog walk pins the 19-byte code entry. Mutation killed: the trailing end byte. Shapes 0-2 and the 117-byte trio are byte-identical -- fn_body_bytes grew a branch, not a byte. Refs #12148, advances #10262, #5980.
gHashTag
added a commit
that referenced
this pull request
Oct 25, 2026
…dx, call_index_of maps an export name to its admitted index); 87/87, mutation-checked, resealed -- the stateful floor set is complete The gx_ exports call the law's own helpers: EK_CALL joins the statement kinds (call 0x10 + uleb, the arguments on the stack under it), and call_index_of maps an export NAME to its index among the ADMITTED fns in table order -- the same order walk_prog_locals numbers descriptor rows, so the map's answer is the composed module's own function index. A name no admitted fn carries maps to 0xFFFFFFFF: the adapter refuses the call site, it does not guess. Capstones: the call leaf pins 20 00 10 00 0B with the map's own answer as the callee index (helper 0 before wrap 1); the map skips test rows and private rows. Mutation killed: gx_two's index pin. Two test-buffer slips were caught red by the suite before landing (an 18-byte name blob in a 16-byte slice, a name offset taken from put_bytes' end instead of its start). Refs #12148, advances #10262, #5980.
Collaborator
Author
|
STATUS (lane/wasm-stateful, PR #12178): the stateful floor set 12-16 is COMPLETE as law -- reconciled onto #12152's section vocabulary (the branch's parallel floor-12 bodies dropped, the memory export + compose_module_mem + the global section kept), floor 14 the LOCAL WINDOW (FACT_ROW word 11 = locals_n, the windowed refusal, one i32 group per body), floor 15 LOOPS through the payload nodes (six statement kinds, BS_STMTS_RETURN, the fn gate admits it), floor 16 CALLS (EK_CALL, call_index_of). 87/87 tests, 0 vacuous, every floor mutation-checked, gen regenerated, sealed after each step. The 117-byte trio is byte-identical by construction and by the in-test A/B/A capstones. THE MOUNT STOPPED AT A LAWFUL WALL, measured before any foreign line was written: every gx_ export takes |
gHashTag
added a commit
that referenced
this pull request
Oct 25, 2026
…12152, locals/loops/calls as law; the mount's measured stop at the pointer-param wall (#12178) * spec(wasm): reconcile the stateful floors onto master's floor 12 -- the memory export, compose_module_mem (min+max limits) and floor 13 globals/load/store survive on #12152's vocabulary; 77/77, mutation-checked, resealed Master's #12152 landed this lane's floor-12 section law under its own names (pages_for, memtype, data_segment_active, memory_section, data_section). The rebase drops this branch's parallel bodies (pages_for_bytes, mem_limits_min, memory_body, data_entry and the colliding memory_section/data_section) and keeps what master lacks: EXPORT_KIND_FUNC/MEM, export_entry_kind, export_body_mem, the stateful composer compose_module_mem (now min+max limits, fail-closed on min>max and max>65536), and floor 13 in full (SEC_GLOBAL, global_type, global_entry_i32, global_body, i32.load/i32.store memargs, global.get/set). The 62-byte stateful leaf and the 70-byte global module pin every section boundary; the code-section body length is pinned 6 against master's own whole-module vector (one hand-pin was caught red by the suite). The A/B/A holds inside the capstone: the stateless composer still emits the 39-byte answer module beside the stateful one. Mutations killed: n==62 and the memory-export kind byte. Refs #12148, advances #10262, #5980. * spec(wasm): floor 14 -- the LOCAL WINDOW (word 11 carries locals_n, the windowed refusal, one i32 group per body); 81/81, mutation-checked, resealed Floor 8 refused every var at or beyond nparams; floor 14 opens the local window without moving one byte under it. FACT_ROW's reserved word 11 becomes the fn's i32 local count (fact_put_locals writes it, fact_put still writes 0, fact_locals_n reads it); refused_local_variable_w and expr_refusal_w read var_idx against nparams + locals_n (floor 8's fn is the locals_n 0 case, construct and detail byte for byte); fn_body_bytes_locals grows ONE i32 local group ahead of the floor-9 body (skipped at 0); walk_prog_locals writes each admitted fn's count as a u32le row beside its descriptor and lowers through the windowed body; code_entries_locals and compose_module_mem_l carry the group into the code entry. Capstones: the third(a,b) local leaf pins the group bytes 01 7F ahead of local.get 2 and the seven-byte code entry, with the A/B/A in-test (the same table with the window closed rederives the floor-10 bytes); the 64-byte stateful leaf carries the group beside the 62-byte one. Two hand-pins were caught red by the suite before landing (the code body length 6, the 62-byte leaf's const offset 48). Mutation killed: the group valtype 0x7F -> 0x7E. The 117-byte trio is untouched: walk_prog_locals over a locals-free table is walk_prog. Refs #12148, advances #10262, #5980. * spec(wasm): floor 15 -- LOOPS through the payload nodes (six statement kinds, BS_STMTS_RETURN, the fn gate admits it); 85/85, mutation-checked, resealed gx_replay's While lowers as a node sequence the walk owns: EK_WHILE_OPEN (loop 03 40), EK_COND_BR (br_if, var_idx the depth), EK_LOOP_END (end), EK_LOAD32/EK_STORE32 (floor 13's memargs packed in node_v: align low 32, offset high 32), EK_LOCAL_SET (floor 14's window's write side). One new body shape BS_STMTS_RETURN lowers a payload of statement and expression nodes then the trailing return; the four expression kinds delegate to lower_expr_node byte for byte. stmt_refusal_w admits the statement kinds (the window and operator checks stay through the delegation); fn_refusal admits the shape with body_r's verdict -- BS_OTHER still refuses and the zero-param const gate is untouched. Capstones: the count-down while pins all 17 body bytes (03 40 | 20 00 | 0D 00 | 20 00 41 01 6B 21 00 | 0B | 20 00 | 0B) with the A/B/A in-test (the same fn as floor 10's shape is the three-byte leaf); the whole-prog walk pins the 19-byte code entry. Mutation killed: the trailing end byte. Shapes 0-2 and the 117-byte trio are byte-identical -- fn_body_bytes grew a branch, not a byte. Refs #12148, advances #10262, #5980. * spec(wasm): floor 16 -- CALLS (EK_CALL with the callee index in var_idx, call_index_of maps an export name to its admitted index); 87/87, mutation-checked, resealed -- the stateful floor set is complete The gx_ exports call the law's own helpers: EK_CALL joins the statement kinds (call 0x10 + uleb, the arguments on the stack under it), and call_index_of maps an export NAME to its index among the ADMITTED fns in table order -- the same order walk_prog_locals numbers descriptor rows, so the map's answer is the composed module's own function index. A name no admitted fn carries maps to 0xFFFFFFFF: the adapter refuses the call site, it does not guess. Capstones: the call leaf pins 20 00 10 00 0B with the map's own answer as the callee index (helper 0 before wrap 1); the map skips test rows and private rows. Mutation killed: gx_two's index pin. Two test-buffer slips were caught red by the suite before landing (an 18-byte name blob in a 16-byte slice, a name offset taken from put_bytes' end instead of its start). Refs #12148, advances #10262, #5980.
This was referenced Oct 25, 2026
gHashTag
added a commit
that referenced
this pull request
Oct 25, 2026
…12148, #5980) Floor 14 opened the local window as law (#12178), but the deleted emitter's mount fed it nothing: ir::wasm_facts projected no statement shape and wrote fact word 11 as 0, so every fn with an intermediate still refused as fn body. Floor 17 is the adapter floor -- the three pieces the mount calls, nothing else: - stmts_refusal_w: the windowed verdict of a BS_STMTS_RETURN payload. Statements are opcode spellings, the window rides the EK_VAR reads through expr_refusal_w, the value stack closes on exactly one return value, and a store REFUSES when the value it stores refused -- the verdict never rides under a local.set, or the lowering would emit a body missing those bytes. The loop/call/load/store kinds fail closed (their mounts carry the label depth, callee arity and memarg facts; the law already spells their bytes). - bodies_cap_l: bodies_cap plus one local group's six bytes per locals-carrying row -- walk_prog_locals' own reserve. - compose_module_with_image_l: the emit_with_image composer carrying the locals rows; an empty image over all-zero rows delegates to compose_module_with_image, so the scalar and mounted cuts cannot move. Five tests: the window walk, fail-closed (unbalanced, mountless kinds, the adapter's 255 marker, a partial fact row), the capacity +6, and the two composers -- the delegation pinned by byte equality in both cuts, the 49-byte locals leaf (inc: t = a + 1; return t * 2;) pinned byte for byte through walk_prog_locals, its 66-byte image twin in section id order 1, 3, 5, 7, 10, 11. 103/103 via t27b test and t27c test-report; wasm32.rs 12/12 and wasm32_equality 1/1 stay green; resealed. The mount itself (ir.rs projection + lib.rs adapter) lands in the next commit, paid by shrink.
gHashTag
added a commit
that referenced
this pull request
Oct 25, 2026
…1 feeds the walk (floor 17's mount; Refs #11840, #12148, #5980) Floor 17's law landed in the previous commit; this is the mount it serves. The diff shrinks: +10 hand-written foreign lines, -61 (the counted files +1/-32; one duplicated test folded, see below). - ir.rs wasm_facts: a straight-line body (assignments then the trailing return, all-i32-carried locals) projects as BS_STMTS_RETURN -- each assignment lowers postfix(value) then EK_LOCAL_SET, the return walks last -- and fact word 11 carries the local count through fact_put_locals. The body verdict is the law's own windowed fold (stmts_refusal_w), so a var read past nparams + locals_n still refuses with floor 8's construct and detail byte for byte. Any other statement (If, While, Call, Store) keeps BS_OTHER's refusal; a zero-param fn still owes the const shape. - lib.rs emit_with_image: walk_prog_locals + bodies_cap_l + compose_module_with_image_l. All-zero locals rows delegate byte for byte to the old composer, so the 43-byte leaf, the 117-byte trio and the 60-byte mounted cut cannot move. - tests/wasm32.rs: the mount's end-to-end gate -- the inc leaf (the law's 49 bytes, group 01 7F inside the entry) instantiates in Node's WebAssembly and answers inc(7) = 16. The M-B byte-pin test folds: the law pins the identical two-fn framing byte for byte (the 87-byte duo and 117-byte trio, Node-verified per their law tests) and the same latency/frame source keeps its runtime gate in the neighboring Node test; stale narration prose trimmed beside it. A/B on the same spec: pre-mount the wasm32 build refused "unsupported construct fn body at line 4 (fn inc: ...)"; post-mount it emits the 49-byte module and Node answers inc(7)=16, inc(0)=2, byte-identical across rebuilds. wasm32.rs 12/12, wasm32_equality 1/1, wasm.t27 103/103.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What
specs/t27f/live_graph_export.t27-- the GRAPH-DATA plane of the gx_ buffer exports, companion to the #12005 contract (live_struct_glue.t27, unmodified) and the constant plane (live_glue_layout.t27, #12040, unmodified). The page's per-frame reads become small: a count, a kind, a NAME -- and the two ways events enter apply throughwork_graph.t27's law verbatim.gx_graph_ptr()/gx_graph_len()-- the image region, routed through this card's ownIMAGE_OFF/IMAGE_LEN(the layout plane's transcription untouched)gx_node_count/gx_node_kind/gx_node_name_ptr/gx_node_name_len-- per-node; a past-count index answers each type's own one-past-the-end (NK_COUNT, the empty name pair), never a byte of stategx_edge_count/gx_edge_kind/gx_edge_from/gx_edge_to-- per-edge; past-count endpoints answerNODE_CAP, the law's own impossible nodegx_apply_event(kind, tick, task)-- the live path: refreshes the live triple into staged row 0, applies through the law, returns the law's code verbatimgx_replay(ptr, len)-- the load path: walks whole spec(t27f): live_struct_glue -- the struct-path export glue v2 contract as law (Refs #10262, #11781) #12005 records, first law refusal stops the walk with the law's own code (the contract's mid-batch semantics)MEM_CAP: NAME atMEM_CAP(32 B x 2048 rows), LOG above it (64 records)live_struct_glueleft empty for a future card;E_GX_LEN/E_GX_PTRhere,E_STATE/E_LAYOUTstay the contract's by importTwo measured findings (both filed under the #5980 emitter-gap family, stated in the card's QUESTION)
[8]strconst indexed at runtime answers wrong bytes cross-module AND through importers (probed 2026-10-25). The spec paths therefore live as a 196-byte local u8 table (machine-copied from the fixture's ownSPEC_NAMES), pinned by a transcription test: offsets, per-path lens, shared head/tail, whole-table byte sum 17882.Test report (quoted,
t27c test-report specs/t27f/live_graph_export.t27)Mutation-proven: flipping
name_len_of's tagged width toTAGGED_LEN + 1fails 2 of the 7; restored and re-verified 7/7.Local gates (all exit 0)
dupe_scan.py-- no new duplicate body, no known group grewcheck_assertionless_spec_tests.py-- baseline heldtri types ratchet-- ledger 140, observed 140, CLEANcheck_duplicate_agreement.py,check_seal_coverage.py,check_seal_currency.py,check_ring_spec_drift.pycheck_verilog_widths.py --require-- OK: 16 known, 0 new (the spec's 1,097,855-bit struct ledgered in the same lane, with exact arithmetic; the spec(t27f): live_struct_glue -- the struct-path export glue v2 contract as law (Refs #10262, #11781) #12005 lesson applied one PR earlier)0 foreign lines: one new
.t27spec + one data ledger line intools/verilog_width_baseline.txt.Refs #12005, advances #10262. The trinity-side page PR (reading these exports) follows once this lands.