code wiki / (root) / nx_water_erosion_gate.nx

nx_water_erosion_gate.nx source

↩ module page · 230 lines · 13884 B

1// nx_water_erosion_gate.nx -- GATE for the Mei 2007 hydraulic erosion pipeline (PG18, procgen.plan, 2026-08-24). 2// 3// WHY THIS GATE EXISTS: nx_water_erosion.nx implements all seven Mei 2007 stages and its own header names 4// `bug-tape-flow-direction-mass-imbalance` as the hazard -- yet its self-test never once summed the water. 5// Its T9 comment read "check no NaN/overflow" over a range test. A physics organ whose defining invariant is 6// stated in prose and asserted nowhere is the vacuous-tooth shape: green forever, proving nothing. 7// 8// THE INVARIANTS, DERIVED FROM THE SOURCE, NOT ASSUMED: 9// RAIN sum(d) after add_rain == sum(d) before + n*rain. EXACT: pure per-cell addition. 10// FLOW sum(d) after flow+update == sum(d) before, within a bound. Every outflow is a neighbour's 11// inflow and edges emit zero, so the true sum of (in - out) is zero; the per-cell integer 12// division `(in - out) * dt / q` truncates toward zero once per cell, so the bound is n units 13// of Q14 per stage. Printed beside the measurement so it can be tightened on evidence. 14// EROSION sum(h) + sum(s) after terrain_update == before. EXACT, tolerance ZERO: erode is 15// `h - delta, s + delta` and deposit is `h + delta, s - delta` -- sediment is lifted from the 16// bed and set back down and not one unit is created. This is the claim float engines cannot 17// make and the reason an integer erosion sim is a Houdini-exceed, not a Houdini-parity. 18// EVAPORATE sum(d) after <= before, every cell >= 0. 19// TRANSPORT is semi-Lagrangian bilinear resampling and does NOT conserve sediment exactly by 20// construction (Mei 2007 section 3.5 accepts this). It is measured and PRINTED here, never 21// asserted, so nobody reads a green as a conservation proof it is not. 22// 23// The original nine self-test teeth are migrated onto gv_check below so the estate loses nothing; the 24// hand-rolled `__syscall(93, N)` exits they used could not carry a third state and never printed a value. 25// 26// Fixture: a seeded slope in caller-owned mmap, so the gate never touches a production plane. 27 28import "nx_syscalls.nx" 29import "nx_tier.nx" 30import "nx_gate_verdict.nx" 31import "nx_water_erosion.nx" 32 33// Grid DERIVED from the organ's own documented sizing example (64x64) scaled to keep the gate under a 34// second: 16x16 = 256 cells. The exactness teeth do not depend on grid size; the flow bound scales with n. 35const WE_W: i64 = 16 36const WE_H: i64 = 16 37// Slope step per cell in metres: one hundred metres, the organ's own T4 fixture value, so the migrated 38// teeth exercise exactly the surface the old self-test did. 39const WE_STEP_M: i64 = 100 40// Rain per tick: the organ's own T5 fixture value, five metres of depth. 41const WE_RAIN_M: i64 = 5 42const WE_TICKS: i64 = 10 43 44func we_sum_field(state: *i64, n: i64, off: i64) -> i64 { 45 var s: i64 = 0 46 var i: i64 = 0 47 while i < n { s = s + state[i * NX_WATER_STRIDE + off]; i = i + 1 } 48 return s 49} 50 51func we_min_field(state: *i64, n: i64, off: i64) -> i64 { 52 var m: i64 = state[off] 53 var i: i64 = 1 54 while i < n { let v: i64 = state[i * NX_WATER_STRIDE + off]; if v < m { m = v } i = i + 1 } 55 return m 56} 57 58func we_absdiff(a: i64, b: i64) -> i64 { if a > b { return a - b } return b - a } 59 60// The bed-plus-sediment conservation checker, factored so the neg-control can prove it FIRES. 61// Returns the absolute drift between two (h+s) totals: zero means conserved. 62func we_hs_drift(state: *i64, n: i64, before: i64) -> i64 { 63 let after: i64 = we_sum_field(state, n, NX_WATER_OFF_H) + we_sum_field(state, n, NX_WATER_OFF_S) 64 return we_absdiff(after, before) 65} 66 67func we_seed_slope(state: *i64, w: i64, h: i64, q: i64) -> i64 { 68 let n: i64 = w * h 69 var i: i64 = 0 70 while i < n { 71 let xi: i64 = i % w 72 let base: i64 = i * NX_WATER_STRIDE 73 state[base + NX_WATER_OFF_H] = (w - 1 - xi) * WE_STEP_M * q 74 // dirty every other field so init is PROVEN to zero them, exactly as the old T4 did 75 state[base + NX_WATER_OFF_D] = 99 76 state[base + NX_WATER_OFF_S] = 88 77 state[base + NX_WATER_OFF_FL] = 77 78 state[base + NX_WATER_OFF_FR] = 66 79 state[base + NX_WATER_OFF_FT] = 55 80 state[base + NX_WATER_OFF_FB] = 44 81 state[base + NX_WATER_OFF_U] = 33 82 state[base + NX_WATER_OFF_V] = 22 83 i = i + 1 84 } 85 return n 86} 87 88func main() -> i64 { 89 let c: *i64 = gv_ctr() 90 gv_head("NX-WATER-EROSION-GATE -- Mei 2007 pipe model, conservation asserted not described (PG18)" as *u8) 91 let q: i64 = NX_WATER_Q 92 let n: i64 = WE_W * WE_H 93 94 // ---- migrated T1-T3: mode table and parameter pack ------------------------------------------ 95 gv_check("mode-table-accepts-every-declared-regime" as *u8, 96 nx_water_mode_is_valid(NX_WATER_MODE_GENTLE_WEATHERING) == 1 && 97 nx_water_mode_is_valid(NX_WATER_MODE_FLASH_FLOOD) == 1, c) 98 gv_check("neg-control-mode-table-refuses-an-undeclared-regime" as *u8, nx_water_mode_is_valid(99) == 0, c) 99 let d_flat: i64 = nx_water_erosion_delta(0, NX_WATER_MODE_RIVERINE) 100 let d_steep: i64 = nx_water_erosion_delta(q, NX_WATER_MODE_RIVERINE) 101 gv_puts(" v1 delta flat=" as *u8); gv_num(d_flat); gv_puts(" steep=" as *u8); gv_num(d_steep); gv_puts("\n" as *u8) 102 gv_check("v1-stateless-delta-is-zero-on-flat-and-negative-on-steep" as *u8, d_flat == 0 && d_steep < 0, c) 103 104 let params: *i64 = sys_mmap(NX_WATER_PARAM_COUNT * NX_SIZEOF_NX_INT) as *i64 105 nx_water_erosion_params_default(params) 106 gv_check("default-param-pack-carries-the-documented-constants" as *u8, 107 params[NX_WATER_PARAM_GRAVITY] == NX_WATER_DEFAULT_GRAVITY && 108 params[NX_WATER_PARAM_K_EVAP] == NX_WATER_DEFAULT_K_EVAP, c) 109 110 // ---- fixture --------------------------------------------------------------------------------- 111 let state: *i64 = sys_mmap(n * NX_WATER_STRIDE * NX_SIZEOF_NX_INT) as *i64 112 let scratch: *i64 = sys_mmap(n * NX_SIZEOF_NX_INT) as *i64 113 we_seed_slope(state, WE_W, WE_H, q) 114 gv_subjects("cells-in-fixture" as *u8, n, c) 115 116 // ---- migrated T4: init zeroes state and preserves the bed ------------------------------------ 117 nx_water_erosion_init(state, WE_W, WE_H) 118 var dirty: i64 = 0 119 var bed_ok: i64 = 1 120 var k: i64 = 0 121 while k < n { 122 let b: i64 = k * NX_WATER_STRIDE 123 if state[b + NX_WATER_OFF_D] != 0 { dirty = dirty + 1 } 124 if state[b + NX_WATER_OFF_S] != 0 { dirty = dirty + 1 } 125 if state[b + NX_WATER_OFF_FL] != 0 { dirty = dirty + 1 } 126 if state[b + NX_WATER_OFF_FR] != 0 { dirty = dirty + 1 } 127 if state[b + NX_WATER_OFF_FT] != 0 { dirty = dirty + 1 } 128 if state[b + NX_WATER_OFF_FB] != 0 { dirty = dirty + 1 } 129 if state[b + NX_WATER_OFF_U] != 0 { dirty = dirty + 1 } 130 if state[b + NX_WATER_OFF_V] != 0 { dirty = dirty + 1 } 131 let xi: i64 = k % WE_W 132 if state[b + NX_WATER_OFF_H] != (WE_W - 1 - xi) * WE_STEP_M * q { bed_ok = 0 } 133 k = k + 1 134 } 135 gv_puts(" init dirty_fields_left=" as *u8); gv_num(dirty); gv_puts("\n" as *u8) 136 gv_check("init-zeroes-every-dynamic-field-and-preserves-the-bed" as *u8, dirty == 0 && bed_ok == 1, c) 137 138 // ---- RAIN: exact conservation -------------------------------------------------------------- 139 let rain: i64 = WE_RAIN_M * q 140 let d0: i64 = we_sum_field(state, n, NX_WATER_OFF_D) 141 nx_water_erosion_add_rain(state, WE_W, WE_H, rain) 142 let d1: i64 = we_sum_field(state, n, NX_WATER_OFF_D) 143 gv_puts(" rain sum_before=" as *u8); gv_num(d0); gv_puts(" sum_after=" as *u8); gv_num(d1) 144 gv_puts(" expected=" as *u8); gv_num(d0 + n * rain); gv_puts("\n" as *u8) 145 gv_check("rain-adds-exactly-n-times-rain-to-total-water" as *u8, d1 == d0 + n * rain, c) 146 147 // ---- FLOW: conservation within the derived integer bound ------------------------------------- 148 nx_water_erosion_compute_flow(state, WE_W, WE_H, params) 149 let b00: i64 = _w_cell_base(0, 0, WE_W) 150 let bE0: i64 = _w_cell_base(WE_W - 1, 0, WE_W) 151 gv_puts(" flux high_cell_right=" as *u8); gv_num(state[b00 + NX_WATER_OFF_FR]) 152 gv_puts(" edge_cell_right=" as *u8); gv_num(state[bE0 + NX_WATER_OFF_FR]); gv_puts("\n" as *u8) 153 gv_check("flow-runs-downhill-and-the-edge-emits-nothing" as *u8, 154 state[b00 + NX_WATER_OFF_FR] > 0 && state[bE0 + NX_WATER_OFF_FR] == 0, c) 155 156 let d_pre_flow: i64 = we_sum_field(state, n, NX_WATER_OFF_D) 157 nx_water_erosion_update_water_and_velocity(state, WE_W, WE_H, params) 158 let d_post_flow: i64 = we_sum_field(state, n, NX_WATER_OFF_D) 159 let flow_drift: i64 = we_absdiff(d_post_flow, d_pre_flow) 160 let flow_bound: i64 = n 161 gv_puts(" flow water_before=" as *u8); gv_num(d_pre_flow); gv_puts(" after=" as *u8); gv_num(d_post_flow) 162 gv_puts(" drift=" as *u8); gv_num(flow_drift); gv_puts(" derived_bound=" as *u8); gv_num(flow_bound); gv_puts("\n" as *u8) 163 gv_check("flow-conserves-water-within-one-truncation-unit-per-cell" as *u8, flow_drift <= flow_bound, c) 164 gv_check("flow-moves-water-downhill-highest-cell-holds-less-than-lowest" as *u8, 165 state[b00 + NX_WATER_OFF_D] < state[bE0 + NX_WATER_OFF_D], c) 166 167 // ---- EROSION: bed plus sediment is EXACTLY conserved ----------------------------------------- 168 let hs_before: i64 = we_sum_field(state, n, NX_WATER_OFF_H) + we_sum_field(state, n, NX_WATER_OFF_S) 169 let h_before: i64 = we_sum_field(state, n, NX_WATER_OFF_H) 170 nx_water_erosion_terrain_update(state, WE_W, WE_H, params) 171 let hs_drift: i64 = we_hs_drift(state, n, hs_before) 172 let h_after: i64 = we_sum_field(state, n, NX_WATER_OFF_H) 173 gv_puts(" erosion bed+sediment before=" as *u8); gv_num(hs_before) 174 gv_puts(" drift=" as *u8); gv_num(hs_drift); gv_puts(" (tolerance ZERO by construction)\n" as *u8) 175 gv_check("erosion-conserves-bed-plus-sediment-EXACTLY" as *u8, hs_drift == 0, c) 176 // ANTI-VACUITY: conservation of a no-op is meaningless. The bed must actually have moved. 177 gv_puts(" erosion bed_moved=" as *u8); gv_num(we_absdiff(h_after, h_before)); gv_puts("\n" as *u8) 178 gv_check("anti-vacuity-erosion-actually-moved-bed-material" as *u8, h_after != h_before, c) 179 180 // NEG-CONTROL for the checker itself: perturb one cell by one unit and the SAME checker must report 181 // exactly that unit. A conservation tooth that cannot fire on a planted leak is decoration. 182 let good_drift: i64 = we_hs_drift(state, n, hs_before) 183 state[NX_WATER_OFF_H] = state[NX_WATER_OFF_H] + 1 184 let bad_drift: i64 = we_hs_drift(state, n, hs_before) 185 state[NX_WATER_OFF_H] = state[NX_WATER_OFF_H] - 1 186 gv_puts(" neg-control planted_leak_reads=" as *u8); gv_num(bad_drift) 187 gv_puts(" clean_reads=" as *u8); gv_num(good_drift); gv_puts("\n" as *u8) 188 var fires: i64 = 0 189 if bad_drift == 1 { fires = 1 } 190 var silent: i64 = 0 191 if good_drift == 0 { silent = 0 } else { silent = 1 } 192 gv_bite("neg-control-conservation-checker-fires-on-a-planted-one-unit-leak" as *u8, fires, silent, c) 193 194 // ---- TRANSPORT: measured, declared non-exact, never asserted --------------------------------- 195 let s_before: i64 = we_sum_field(state, n, NX_WATER_OFF_S) 196 nx_water_erosion_transport(state, scratch, WE_W, WE_H, params) 197 let s_after: i64 = we_sum_field(state, n, NX_WATER_OFF_S) 198 gv_puts(" transport sediment_before=" as *u8); gv_num(s_before); gv_puts(" after=" as *u8); gv_num(s_after) 199 gv_puts(" (semi-Lagrangian resampling: NOT exact by construction, reported not asserted)\n" as *u8) 200 gv_check("transport-never-produces-negative-sediment" as *u8, we_min_field(state, n, NX_WATER_OFF_S) >= 0, c) 201 202 // ---- EVAPORATE: monotone, non-negative ------------------------------------------------------ 203 let d_pre_ev: i64 = we_sum_field(state, n, NX_WATER_OFF_D) 204 nx_water_erosion_evaporate(state, WE_W, WE_H, params) 205 let d_post_ev: i64 = we_sum_field(state, n, NX_WATER_OFF_D) 206 gv_puts(" evaporate before=" as *u8); gv_num(d_pre_ev); gv_puts(" after=" as *u8); gv_num(d_post_ev); gv_puts("\n" as *u8) 207 gv_check("evaporation-only-removes-water-and-never-below-zero" as *u8, 208 d_post_ev <= d_pre_ev && we_min_field(state, n, NX_WATER_OFF_D) >= 0, c) 209 gv_check("anti-vacuity-evaporation-with-positive-k-strictly-reduces-standing-water" as *u8, 210 d_pre_ev > 0 && d_post_ev < d_pre_ev, c) 211 212 // ---- migrated T9: multi-tick stability, now with the bound DERIVED -------------------------- 213 // Ten ticks at a tenth of the rain. The old test picked 1000*q as a ceiling with no derivation. The 214 // honest ceiling is the water that could possibly exist: everything rained in, nothing evaporated. 215 let tick_rain: i64 = rain / 10 216 var t: i64 = 0 217 while t < WE_TICKS { nx_water_erosion_tick(state, scratch, WE_W, WE_H, tick_rain, params); t = t + 1 } 218 let d_final: i64 = we_sum_field(state, n, NX_WATER_OFF_D) 219 let ceiling: i64 = d_post_ev + n * tick_rain * WE_TICKS 220 gv_puts(" " as *u8); gv_num(WE_TICKS); gv_puts(" ticks total_water=" as *u8); gv_num(d_final) 221 gv_puts(" derived_ceiling=" as *u8); gv_num(ceiling); gv_puts("\n" as *u8) 222 gv_check("multi-tick-water-stays-non-negative-and-under-the-derived-ceiling" as *u8, 223 we_min_field(state, n, NX_WATER_OFF_D) >= 0 && d_final <= ceiling, c) 224 let hs_final_drift: i64 = we_hs_drift(state, n, hs_before) 225 gv_puts(" " as *u8); gv_num(WE_TICKS); gv_puts(" ticks bed+sediment drift=" as *u8); gv_num(hs_final_drift) 226 gv_puts(" (transport resampling is the only non-exact stage; reported)\n" as *u8) 227 228 return gv_verdict("nx_water_erosion_gate" as *u8, c, 229 "Mei 2007 in integer: rain and erosion conserve EXACTLY, flow within one truncation unit per cell, transport reported not asserted. Every bound derived from the source and printed." as *u8) 230}