nx_editstack_gate.nx source

1// nx_editstack_gate.nx -- the gate for nx_editstack_lib (/compare/dcc DC1 and DC2). 2// THE CLAIM UNDER TEST is the one no float DCC can make: replaying the operation log from the base 3// reproduces the state BIT-IDENTICALLY, and re-evaluating a parameter at depth equals building the whole 4// log again from scratch with that parameter. Both are asserted on a DIGEST OF THE STATE, never on a 5// return code, because a leaking or no-op implementation answers identical return codes. 6// 7// ANTI-VACUITY IS EXPLICIT, in three places, because "replay equals live" is trivially true for a stack 8// that does nothing at all: 9// - the digest is proven to DISCRIMINATE (three different states must give three different digests); 10// a constant digest function would otherwise pass every other tooth on this gate. 11// - undo is proven to reach an EARLIER state, so replay cannot be a no-op: it must genuinely reset to 12// the base and re-apply a PREFIX of the log. 13// - re-evaluation is proven equal to an INDEPENDENTLY BUILT stack, not merely different from before. 14// Every refusal cell is a gv_bite: it must fire on the bad input AND stay silent on the good one. 15// 100% sovereign. No hardware writes (Rule 26). license_tier: ORIGINAL expect_exit: 0 16import "nx_syscalls.nx" 17import "nx_gate_verdict.nx" 18import "nx_editstack_lib.nx" 19 20const EG_NCELL: i64 = 6 21const EG_CAP: i64 = 8 22const EG_SMALLCAP: i64 = 2 23 24// The fixture base is an arithmetic ramp, DERIVED rather than six hand-written index/value pairs: cell i 25// holds EG_BASE0 + i * EG_BASE_STEP. Writing an index beside its value once per cell is two copies of the 26// same mapping, and a hand-written seed silently stops covering the array the moment EG_NCELL moves; the 27// derived seed below cannot. The step is wide enough that every cell is distinguishable in a digest. 28const EG_BASE0: i64 = 10 29const EG_BASE_STEP: i64 = 10 30 31// The cells the fixture programme operates on, named so each tooth reads as the claim it is making. 32const EG_TGT_ADD: i64 = 0 33const EG_TGT_SCALE: i64 = 1 34// A third distinct cell, so each of the truncation fixture's pushes is independently observable. 35const EG_TGT_THIRD: i64 = 2 36 37// The fixture programme is exactly this many operations -- ADD, SCALE, RADD. Every counter tooth below is 38// stated against this rather than against a 3 counted by hand at each assertion. 39const EG_PROG_OPS: i64 = 3 40 41// One operation survives the undo in the truncation fixture, plus the one pushed after it. 42const EG_TRUNC_SURVIVORS: i64 = 2 43 44const EG_ADD0: i64 = 5 45const EG_ADD0_ALT: i64 = 9 46const EG_SCALE_NUM: i64 = 3 47const EG_SCALE_DEN: i64 = 2 48const EG_RADD_LO: i64 = 2 49const EG_RADD_HI: i64 = 5 50const EG_RADD_AMT: i64 = 7 51const EG_UNUSED: i64 = 0 52 53func eg_eq(a: i64, b: i64) -> i64 { if a == b { return 1 } return 0 } 54func eg_ne(a: i64, b: i64) -> i64 { if a != b { return 1 } return 0 } 55 56// The base value of cell i. ONE mapping from index to value, so an assertion about a cell can never quote 57// a value that belongs to a different cell. 58func eg_base(i: i64) -> i64 { return EG_BASE0 + i * EG_BASE_STEP } 59 60// Seed a stack with the fixture base. Returns the stack, or 0 if the allocation refused. The loop is bound 61// to EG_NCELL, so the seed covers the whole cell array by construction rather than by hand. 62func eg_seed(cap: i64) -> *i64 { 63 let st: *i64 = es_new(cap, EG_NCELL) 64 if (st as i64) == 0 { return st } 65 var i: i64 = 0 66 while i < EG_NCELL { es_base_set(st, i, eg_base(i)); i = i + 1 } 67 return st 68} 69 70// Push the three-op fixture programme onto a seeded stack, with the first ADD amount as a parameter so 71// the same builder serves both the re-evaluated stack and the independently built comparison stack. 72func eg_program(st: *i64, add0: i64) -> i64 { 73 es_push(st, ES_OP_ADD, EG_TGT_ADD, add0, EG_UNUSED, EG_UNUSED) 74 es_push(st, ES_OP_SCALE, EG_TGT_SCALE, EG_SCALE_NUM, EG_SCALE_DEN, EG_UNUSED) 75 es_push(st, ES_OP_RADD, EG_RADD_LO, EG_RADD_HI, EG_RADD_AMT, EG_UNUSED) 76 return 0 77} 78 79func main(argc: i64, argv: *i64) -> i64 { 80 let ctr: *i64 = gv_ctr() 81 gv_head("nx_editstack_gate -- non-destructive operation stack: record, undo, redo, replay, re-evaluate" as *u8) 82 83 let st: *i64 = eg_seed(EG_CAP) 84 gv_check("fixture-allocated" as *u8, eg_ne(st as i64, 0), ctr) 85 86 let d_base: i64 = es_digest(st) 87 es_push(st, ES_OP_ADD, EG_TGT_ADD, EG_ADD0, EG_UNUSED, EG_UNUSED) 88 let d1: i64 = es_digest(st) 89 es_push(st, ES_OP_SCALE, EG_TGT_SCALE, EG_SCALE_NUM, EG_SCALE_DEN, EG_UNUSED) 90 let d2: i64 = es_digest(st) 91 es_push(st, ES_OP_RADD, EG_RADD_LO, EG_RADD_HI, EG_RADD_AMT, EG_UNUSED) 92 let d3: i64 = es_digest(st) 93 94 // ASSERT THE FIXTURE REACHED THE CONDITION BEFORE ASSERTING ANY OUTCOME. 95 gv_check("fixture-recorded-three-ops" as *u8, eg_eq(es_count(st), EG_PROG_OPS), ctr) 96 gv_check("fixture-head-at-three" as *u8, eg_eq(es_head(st), EG_PROG_OPS), ctr) 97 gv_check("fixture-arithmetic-add" as *u8, eg_eq(es_cell(st, EG_TGT_ADD), eg_base(EG_TGT_ADD) + EG_ADD0), ctr) 98 gv_check("fixture-arithmetic-rational-scale" as *u8, eg_eq(es_cell(st, EG_TGT_SCALE), eg_base(EG_TGT_SCALE) * EG_SCALE_NUM / EG_SCALE_DEN), ctr) 99 // the last cell INSIDE the half-open range [EG_RADD_LO, EG_RADD_HI), derived so the bound cannot drift 100 gv_check("fixture-arithmetic-range-add" as *u8, eg_eq(es_cell(st, EG_RADD_HI - 1), eg_base(EG_RADD_HI - 1) + EG_RADD_AMT), ctr) 101 // and the first cell OUTSIDE it, which is exactly what this tooth's name claims 102 gv_check("fixture-range-add-respects-upper-bound" as *u8, eg_eq(es_cell(st, EG_RADD_HI), eg_base(EG_RADD_HI)), ctr) 103 104 // ANTI-VACUITY ON THE INSTRUMENT ITSELF: a digest that returned a constant would pass every 105 // equality tooth below. Four states, four distinct digests, asserted before anything relies on them. 106 var disc: i64 = 1 107 if eg_ne(d_base, d1) == 0 { disc = 0 } 108 if eg_ne(d1, d2) == 0 { disc = 0 } 109 if eg_ne(d2, d3) == 0 { disc = 0 } 110 if eg_ne(d_base, d3) == 0 { disc = 0 } 111 gv_check("digest-discriminates-distinct-states" as *u8, disc, ctr) 112 113 // UNDO IS EXACT, and because it reaches an EARLIER state it also proves replay is not a no-op. 114 gv_check("undo-returns-ok" as *u8, eg_eq(es_undo(st), ES_OK), ctr) 115 gv_check("undo-restores-exact-prior-digest" as *u8, eg_eq(es_digest(st), d2), ctr) 116 gv_check("undo-lowers-head-without-discarding-the-log" as *u8, eg_eq(es_head(st), EG_PROG_OPS - 1), ctr) 117 gv_check("undo-preserves-count-for-redo" as *u8, eg_eq(es_count(st), EG_PROG_OPS), ctr) 118 es_undo(st) 119 gv_check("undo-twice-restores-exact-digest" as *u8, eg_eq(es_digest(st), d1), ctr) 120 121 gv_check("redo-returns-ok" as *u8, eg_eq(es_redo(st), ES_OK), ctr) 122 gv_check("redo-restores-exact-digest" as *u8, eg_eq(es_digest(st), d2), ctr) 123 es_redo(st) 124 gv_check("redo-to-head-restores-exact-digest" as *u8, eg_eq(es_digest(st), d3), ctr) 125 126 // THE BIT-EXACT CLAIM: replay the whole log from the base and land on the identical digest. 127 gv_check("replay-returns-ok" as *u8, eg_eq(es_replay(st), ES_OK), ctr) 128 gv_check("replay-from-base-is-bit-identical-to-live" as *u8, eg_eq(es_digest(st), d3), ctr) 129 gv_check("replay-did-not-collapse-to-base" as *u8, eg_ne(es_digest(st), d_base), ctr) 130 131 // DC2: re-evaluating a parameter at DEPTH must preserve every operation after it, and must equal a 132 // stack built from scratch with the new parameter. Equality with an INDEPENDENT build is the tooth -- 133 // "it changed" would be satisfied by an implementation that simply corrupted the state. 134 gv_check("reeval-returns-ok" as *u8, eg_eq(es_reeval(st, 0, EG_TGT_ADD, EG_ADD0_ALT, EG_UNUSED, EG_UNUSED), ES_OK), ctr) 135 let d_re: i64 = es_digest(st) 136 gv_check("reeval-changed-the-state" as *u8, eg_ne(d_re, d3), ctr) 137 gv_check("reeval-preserved-the-whole-log" as *u8, eg_eq(es_count(st), EG_PROG_OPS), ctr) 138 gv_check("reeval-preserved-downstream-range-add" as *u8, eg_eq(es_cell(st, EG_RADD_HI - 1), eg_base(EG_RADD_HI - 1) + EG_RADD_AMT), ctr) 139 gv_check("reeval-preserved-downstream-scale" as *u8, eg_eq(es_cell(st, EG_TGT_SCALE), eg_base(EG_TGT_SCALE) * EG_SCALE_NUM / EG_SCALE_DEN), ctr) 140 gv_check("reeval-applied-the-new-parameter" as *u8, eg_eq(es_cell(st, EG_TGT_ADD), eg_base(EG_TGT_ADD) + EG_ADD0_ALT), ctr) 141 142 let fresh: *i64 = eg_seed(EG_CAP) 143 eg_program(fresh, EG_ADD0_ALT) 144 gv_check("reeval-equals-an-independently-built-stack" as *u8, eg_eq(d_re, es_digest(fresh)), ctr) 145 146 // DETERMINISM: two stacks built independently from the same base and the same programme agree exactly. 147 let twinA: *i64 = eg_seed(EG_CAP) 148 let twinB: *i64 = eg_seed(EG_CAP) 149 eg_program(twinA, EG_ADD0) 150 eg_program(twinB, EG_ADD0) 151 gv_check("two-independent-builds-agree-bit-for-bit" as *u8, eg_eq(es_digest(twinA), es_digest(twinB)), ctr) 152 gv_check("independent-build-reproduces-the-original-run" as *u8, eg_eq(es_digest(twinA), d3), ctr) 153 154 // ---- NEGATIVE CONTROLS: every guard must FIRE on the bad input and stay SILENT on the good one ---- 155 let g1: *i64 = eg_seed(EG_CAP) 156 let d_g1: i64 = es_digest(g1) 157 let bad_cell: i64 = es_push(g1, ES_OP_ADD, EG_NCELL, EG_ADD0, EG_UNUSED, EG_UNUSED) 158 let cell_unchanged: i64 = eg_eq(es_digest(g1), d_g1) 159 let cell_notrecorded: i64 = eg_eq(es_count(g1), 0) 160 let good_cell: i64 = es_push(g1, ES_OP_ADD, 0, EG_ADD0, EG_UNUSED, EG_UNUSED) 161 gv_bite("neg-control-cell-index-out-of-range" as *u8, eg_eq(bad_cell, ES_E_CELL), eg_ne(good_cell, ES_OK), ctr) 162 gv_check("refused-op-left-the-state-untouched" as *u8, cell_unchanged, ctr) 163 gv_check("refused-op-was-not-recorded-in-the-log" as *u8, cell_notrecorded, ctr) 164 165 let g2: *i64 = eg_seed(EG_CAP) 166 let d_g2: i64 = es_digest(g2) 167 let bad_div: i64 = es_push(g2, ES_OP_SCALE, 1, EG_SCALE_NUM, 0, EG_UNUSED) 168 let div_unchanged: i64 = eg_eq(es_digest(g2), d_g2) 169 let good_div: i64 = es_push(g2, ES_OP_SCALE, 1, EG_SCALE_NUM, EG_SCALE_DEN, EG_UNUSED) 170 gv_bite("neg-control-scale-denominator-zero" as *u8, eg_eq(bad_div, ES_E_DIV), eg_ne(good_div, ES_OK), ctr) 171 gv_check("refused-divide-left-the-state-untouched" as *u8, div_unchanged, ctr) 172 173 let g3: *i64 = eg_seed(EG_CAP) 174 let bad_kind: i64 = es_push(g3, 0, 0, EG_ADD0, EG_UNUSED, EG_UNUSED) 175 let good_kind: i64 = es_push(g3, ES_OP_ADD, 0, EG_ADD0, EG_UNUSED, EG_UNUSED) 176 gv_bite("neg-control-unknown-op-kind" as *u8, eg_eq(bad_kind, ES_E_KIND), eg_ne(good_kind, ES_OK), ctr) 177 178 let g4: *i64 = eg_seed(EG_CAP) 179 let bad_range: i64 = es_push(g4, ES_OP_RADD, EG_RADD_LO, EG_NCELL + 1, EG_RADD_AMT, EG_UNUSED) 180 let good_range: i64 = es_push(g4, ES_OP_RADD, EG_RADD_LO, EG_RADD_HI, EG_RADD_AMT, EG_UNUSED) 181 gv_bite("neg-control-cell-range-past-the-end" as *u8, eg_eq(bad_range, ES_E_RANGE), eg_ne(good_range, ES_OK), ctr) 182 183 // A FULL STACK REFUSES BY NAME AND NEVER SILENTLY DROPS THE OPERATION. 184 let g5: *i64 = eg_seed(EG_SMALLCAP) 185 es_push(g5, ES_OP_ADD, 0, EG_ADD0, EG_UNUSED, EG_UNUSED) 186 let good_cap: i64 = es_push(g5, ES_OP_ADD, 0, EG_ADD0, EG_UNUSED, EG_UNUSED) 187 let d_full: i64 = es_digest(g5) 188 let bad_cap: i64 = es_push(g5, ES_OP_ADD, 0, EG_ADD0, EG_UNUSED, EG_UNUSED) 189 gv_bite("neg-control-op-cap-reached" as *u8, eg_eq(bad_cap, ES_E_FULL), eg_ne(good_cap, ES_OK), ctr) 190 gv_check("cap-refusal-did-not-drop-the-op-silently" as *u8, eg_eq(es_count(g5), EG_SMALLCAP), ctr) 191 gv_check("cap-refusal-left-the-state-untouched" as *u8, eg_eq(es_digest(g5), d_full), ctr) 192 193 let g6: *i64 = eg_seed(EG_CAP) 194 let bad_base: i64 = es_undo(g6) 195 es_push(g6, ES_OP_ADD, 0, EG_ADD0, EG_UNUSED, EG_UNUSED) 196 let good_base: i64 = es_undo(g6) 197 gv_bite("neg-control-undo-past-the-base" as *u8, eg_eq(bad_base, ES_E_ATBASE), eg_ne(good_base, ES_OK), ctr) 198 199 let g7: *i64 = eg_seed(EG_CAP) 200 es_push(g7, ES_OP_ADD, 0, EG_ADD0, EG_UNUSED, EG_UNUSED) 201 let bad_head: i64 = es_redo(g7) 202 es_undo(g7) 203 let good_head: i64 = es_redo(g7) 204 gv_bite("neg-control-redo-past-the-head" as *u8, eg_eq(bad_head, ES_E_ATHEAD), eg_ne(good_head, ES_OK), ctr) 205 206 let g8: *i64 = eg_seed(EG_CAP) 207 let bad_idx: i64 = es_reeval(g8, 0, 0, EG_ADD0_ALT, EG_UNUSED, EG_UNUSED) 208 es_push(g8, ES_OP_ADD, 0, EG_ADD0, EG_UNUSED, EG_UNUSED) 209 let good_idx: i64 = es_reeval(g8, 0, 0, EG_ADD0_ALT, EG_UNUSED, EG_UNUSED) 210 gv_bite("neg-control-reeval-op-index-out-of-range" as *u8, eg_eq(bad_idx, ES_E_IDX), eg_ne(good_idx, ES_OK), ctr) 211 212 // A PUSH AFTER AN UNDO TRUNCATES THE REDO TAIL, and the counters must SHOW it. 213 let g9: *i64 = eg_seed(EG_CAP) 214 es_push(g9, ES_OP_ADD, 0, EG_ADD0, EG_UNUSED, EG_UNUSED) 215 es_push(g9, ES_OP_ADD, 1, EG_ADD0, EG_UNUSED, EG_UNUSED) 216 es_undo(g9) 217 es_push(g9, ES_OP_ADD, EG_TGT_THIRD, EG_ADD0, EG_UNUSED, EG_UNUSED) 218 gv_check("push-after-undo-truncates-the-redo-tail" as *u8, eg_eq(es_count(g9), EG_TRUNC_SURVIVORS), ctr) 219 gv_check("truncated-tail-cannot-be-redone" as *u8, eg_eq(es_redo(g9), ES_E_ATHEAD), ctr) 220 221 gv_check("every-refusal-carries-a-distinct-name" as *u8, eg_ne(es_err_name(ES_E_CELL) as i64, es_err_name(ES_E_FULL) as i64), ctr) 222 223 return gv_verdict("nx_editstack_gate" as *u8, ctr, "the operation log is the state: undo and re-evaluation are replays from the base, so they cannot drift the way an inverse-op undo does in a float editor" as *u8) 224}