code wiki / (root) / nx_worldpipe_render_gate.nx
`nx_worldpipe_render_gate.nx` source

↩ module page · 234 lines · 11739 B
1// nx_worldpipe_render_gate.nx -- GATE for the rung "erosion reaches the PUBLISHED picture".
2//
3// THE SUBJECT IS NOT "DOES EROSION WORK". nx_worldpipe_erode_gate already proves that, 21/21, over the
4// full 102,400-cell population. The subject HERE is the single behavioural claim nx_worldpipe_render
5// makes and that a green erosion gate cannot make for it: that the bake changes the heights AT THE
6// EXACT POINTS THE RENDERER TURNS INTO PIXELS, and that a consumer which does not bake is untouched.
7// A capability can be proven and still never reach a surface; this gate measures the reaching.
8//
9// EVERY ASSERTION IS BOUND TO A DENOMINATOR (gv_subjects), and the denominators are the two real
10// populations: the whole hydrology grid, and the whole hero sample lattice the render loop walks.
11// No sampling.
12//
13// ANTI-VACUITY. "The picture changed" is passed by a uniform offset, by added noise, and by any bug
14// that perturbs every height equally -- so a tooth that only counts changed points is not a tooth.
15// This gate additionally requires the changes to be NON-UNIFORM (at least two distinct delta values
16// among the changed points), which a constant offset cannot satisfy.
17//
18// NEGATIVE CONTROLS, NAMED SO A CENSUS CAN FIND THEM:
19//   neg-control-wp_erode-INERT-...   proves the opt-in is real: before any bake every one of the
20//                                    102,400 cells reads exactly zero, so an importer that never
21//                                    bakes is byte-identical. This is the "nobody else moves" claim.
22//   neg-control-zero-tick-budget-... proves the instrument does not manufacture erosion: asked for a
23//                                    zero budget it must return every sampled height to its
24//                                    pre-bake value and report zero material moved.
25//
26// license_tier: ORIGINAL   expect_exit: 0   No hw writes (Rule 26).
27import "nx_syscalls.nx"
28import "nx_gate_verdict.nx"
29import "nx_worldpipe.nx"
30
31// Seed and budget are the RENDERER'S, not the gate's -- a gate that exercises a different world or a
32// different budget than the thing it certifies is measuring a different subject.
33const WRG_SEED: i64 = 1
34const WRG_TICKS: i64 = 8
35// The render's hero lattice, copied from nx_worldpipe_render so these are the very points that become
36// pixels: 97 x 97 samples at 110 world units, centred by subtracting 48.
37const WRG_TN: i64 = 97
38const WRG_SP: i64 = 110
39const WRG_OFF: i64 = 48
40const WRG_ART: *u8 = "knowledge/nx_worldpipe_eroded.png"
41
42func wrg_hero_x(i: i64) -> i64 { return (i - WRG_OFF)*WRG_SP }
43
44// Independent recomputation of the derived talus, written HERE so the lib's answer is checked against
45// a second implementation of the same definition rather than against itself. This catches the failure
46// that matters -- a derivation that silently returns a constant, or reads the wrong surface -- and it
47// is deliberately the ONLY duplicated arithmetic in this file.
48func wrg_talus_oracle() -> i64 {
  let gn: i64 = HYW
  let n: i64 = gn * gn
  let g: *i64 = sys_mmap(n*8) as *i64
  var y: i64 = 0
  while y < gn {
      var x: i64 = 0
      while x < gn { g[y*gn + x] = wp_flow_h(x*HYCELL - HYSPAN, y*HYCELL - HYSPAN); x = x + 1 }
      y = y + 1
  }
  var sum: i64 = 0
  var y2: i64 = 0
  while y2 < gn {
      var x2: i64 = 0
      while x2 < gn {
          let k: i64 = y2*gn + x2
          let h: i64 = g[k]
          var m: i64 = 0
          if x2 > 0      { let da: i64 = wp_iabs(h - g[k-1]);  if da > m { m = da } }
          if x2 < gn - 1 { let db: i64 = wp_iabs(h - g[k+1]);  if db > m { m = db } }
          if y2 > 0      { let dc: i64 = wp_iabs(h - g[k-gn]); if dc > m { m = dc } }
          if y2 < gn - 1 { let dd: i64 = wp_iabs(h - g[k+gn]); if dd > m { m = dd } }
          sum = sum + m
          x2 = x2 + 1
      }
      y2 = y2 + 1
  }
  return sum / n
76}
77
78// Fill dst with wp_height at every hero lattice point, in render order.
79func wrg_sample_hero(dst: *i64) -> i64 {
  var gz: i64 = 0
  while gz < WRG_TN {
      var gx: i64 = 0
      while gx < WRG_TN {
          dst[gz*WRG_TN + gx] = wp_height(wrg_hero_x(gx), wrg_hero_x(gz))
          gx = gx + 1
      }
      gz = gz + 1
  }
  return WRG_TN * WRG_TN
90}
91
92func main() -> i64 {
  let c: *i64 = gv_ctr()
  gv_head("=== nx_worldpipe_render_gate -- does stage-3.5 erosion reach the PUBLISHED picture? ===" as *u8)
95
  wp_init(WRG_SEED)
  let nspr: i64 = wp_hydro_bake()
  gv_puts("  world: seed=" as *u8); gv_num(WRG_SEED)
  gv_puts(" hydrology springs=" as *u8); gv_num(nspr); gv_puts("\n" as *u8)
100
  let gn: i64 = HYW
  let n: i64 = gn * gn
  gv_subjects("hydrology-grid-cells-full-population" as *u8, n, c)
104
  // ---- neg-control: the opt-in is the BAKE. Nothing has baked yet, so every cell must read zero.
  var inert: i64 = 0
  var y1: i64 = 0
  while y1 < gn {
      var x1: i64 = 0
      while x1 < gn {
          if wp_erode(x1*HYCELL - HYSPAN, y1*HYCELL - HYSPAN) != 0 { inert = inert + 1 }
          x1 = x1 + 1
      }
      y1 = y1 + 1
  }
  gv_puts("  before any bake: non-zero wp_erode readings=" as *u8); gv_num(inert)
  gv_puts(" of=" as *u8); gv_num(n); gv_puts("\n" as *u8)
  gv_check("neg-control-wp_erode-INERT-at-EVERY-cell-before-a-bake-so-a-non-baking-consumer-is-byte-identical" as *u8,
      inert == 0, c)
120
  // ---- the hero lattice: the points that become pixels, sampled BEFORE the bake
  let hn: i64 = WRG_TN * WRG_TN
  gv_subjects("render-hero-lattice-points-full-population" as *u8, hn, c)
  let pre: *i64 = sys_mmap(hn*8) as *i64
  let post1: *i64 = sys_mmap(hn*8) as *i64
  let zero: *i64 = sys_mmap(hn*8) as *i64
  let post2: *i64 = sys_mmap(hn*8) as *i64
  wrg_sample_hero(pre)
129
  // ---- the derived talus, checked against an independent recomputation
  let tl: i64 = wp_erode_talus_derived()
  let tlo: i64 = wrg_talus_oracle()
  gv_puts("  derived talus=" as *u8); gv_num(tl)
  gv_puts(" independent oracle=" as *u8); gv_num(tlo); gv_puts("\n" as *u8)
  gv_check("terrain-has-relief-so-the-derived-talus-is-a-measurement-not-a-default" as *u8, tl > 0, c)
  gv_check("derived-talus-EQUALS-an-independent-recomputation-so-it-is-the-formula-not-a-constant" as *u8,
      tl == tlo, c)
138
  // ---- the bake the renderer makes
  let tl2: i64 = wp_erode_bake_derived(WRG_TICKS)
  let moved: i64 = wp_erode_stat(1)
  let hi0: i64 = wp_erode_stat(2)
  let hi1: i64 = wp_erode_stat(3)
  gv_puts("  bake: ticks=" as *u8); gv_num(wp_erode_stat(0))
  gv_puts(" talus=" as *u8); gv_num(tl2)
  gv_puts(" material_moved=" as *u8); gv_num(moved)
  gv_puts(" hypsometric_permil " as *u8); gv_num(hi0)
  gv_puts(" -> " as *u8); gv_num(hi1); gv_puts("\n" as *u8)
  gv_check("bake-at-the-renderers-budget-MOVED-material" as *u8, moved > 0, c)
  gv_check("bake_derived-reports-the-same-talus-it-derived" as *u8, tl2 == tl, c)
151
  wrg_sample_hero(post1)
  var changed: i64 = 0
  var firstd: i64 = 0
  var distinct2: i64 = 0
  var i2: i64 = 0
  while i2 < hn {
      let d: i64 = post1[i2] - pre[i2]
      if d != 0 {
          changed = changed + 1
          if firstd == 0 { firstd = d } else { if d != firstd { distinct2 = 1 } }
      }
      i2 = i2 + 1
  }
  var permil: i64 = 0
  if hn > 0 { permil = changed * 1000 / hn }
  gv_puts("  render lattice: heights changed by the bake=" as *u8); gv_num(changed)
  gv_puts(" of=" as *u8); gv_num(hn)
  gv_puts(" permil=" as *u8); gv_num(permil)
  gv_puts(" second_distinct_delta=" as *u8); gv_num(distinct2); gv_puts("\n" as *u8)
  gv_check("THE-RUNG-erosion-changes-the-heights-at-the-points-the-renderer-turns-into-pixels" as *u8,
      changed > 0, c)
  gv_check("anti-vacuity-the-deltas-are-NON-UNIFORM-so-a-constant-offset-or-a-global-perturbation-cannot-pass" as *u8,
      distinct2 == 1, c)
175
  // The paired cell: the SAME detector must FIRE on the baked world and stay SILENT on the unbaked
  // one. The silent side is the pre-bake full-grid census taken above -- reused rather than
  // re-measured, because by this point the world IS baked and a second reading here would be a
  // reading of the wrong state dressed up as a control.
  var sees_after: i64 = 0
  if changed > 0 { sees_after = 1 }
  var sees_before: i64 = 0
  if inert != 0 { sees_before = 1 }
  gv_bite("bite-render-sampler-sees-erosion-ONLY-after-a-bake" as *u8, sees_after, sees_before, c)
185
  // ---- neg-control: a zero-tick budget must return every sampled height to its pre-bake value
  let tl3: i64 = wp_erode_bake_derived(0)
  let moved0: i64 = wp_erode_stat(1)
  wrg_sample_hero(zero)
  var restored: i64 = 0
  var i4: i64 = 0
  while i4 < hn { if zero[i4] == pre[i4] { restored = restored + 1 } i4 = i4 + 1 }
  gv_puts("  zero-tick budget: material_moved=" as *u8); gv_num(moved0)
  gv_puts(" lattice points back at their pre-bake height=" as *u8); gv_num(restored)
  gv_puts(" of=" as *u8); gv_num(hn); gv_puts(" talus=" as *u8); gv_num(tl3); gv_puts("\n" as *u8)
  gv_check("neg-control-zero-tick-budget-moves-NO-material" as *u8, moved0 == 0, c)
  gv_check("neg-control-zero-tick-budget-restores-EVERY-lattice-point-so-the-organ-cannot-manufacture-erosion" as *u8,
      restored == hn, c)
199
  // ---- determinism: the published picture must be reproducible by anybody else
  wp_erode_bake_derived(WRG_TICKS)
  wrg_sample_hero(post2)
  var same: i64 = 0
  var i5: i64 = 0
  while i5 < hn { if post2[i5] == post1[i5] { same = same + 1 } i5 = i5 + 1 }
  gv_puts("  determinism: lattice points identical across two bakes=" as *u8); gv_num(same)
  gv_puts(" of=" as *u8); gv_num(hn); gv_puts("\n" as *u8)
  gv_check("two-bakes-at-one-seed-and-budget-agree-at-EVERY-lattice-point" as *u8, same == hn, c)
209
  // ---- the artifact, as a PRECONDITION not a verdict: if the renderer has never been run there is
  // nothing to look at, and "I could not look" is not "it is broken".
  let afd: i64 = sys_openat_rd(WRG_ART)
  var have: i64 = 0
  var abytes: i64 = 0
  var amagic: i64 = 0
  if afd >= 0 {
      let hdr: *u8 = sys_mmap(16)
      let got: i64 = sys_read(afd, hdr, 8)
      abytes = sys_lseek(afd, 0, 2)
      sys_close(afd)
      have = 1
      if got == 8 { if hdr[0] == (137 as u8) { if hdr[1] == (80 as u8) { if hdr[2] == (78 as u8) { if hdr[3] == (71 as u8) { amagic = 1 } } } } }
  }
  gv_puts("  artifact " as *u8); gv_puts(WRG_ART)
  gv_puts(": present=" as *u8); gv_num(have)
  gv_puts(" bytes=" as *u8); gv_num(abytes)
  gv_puts(" png_signature=" as *u8); gv_num(amagic); gv_puts("\n" as *u8)
  if gv_need("knowledge/nx_worldpipe_eroded.png (run nx_worldpipe_render first)" as *u8, have, c) == 1 {
      gv_check("the-rendered-artifact-on-disk-carries-a-real-PNG-signature" as *u8, amagic == 1, c)
  }
231
  return gv_verdict("nx_worldpipe_render_gate" as *u8, c,
      "The rung is REACH, not correctness: erosion was proven by nx_worldpipe_erode_gate and was still inert in production because no consumer baked. Every tooth here is bound to a full population -- 102,400 hydrology cells and 9,409 hero lattice points, the very points the renderer turns into pixels -- and the two negative controls are the load-bearing ones: an unbaked world reads exactly zero at every cell (so no other importer moves), and a zero-tick budget restores every sampled height (so the organ cannot manufacture the erosion it reports). Scope, declared: this gate measures HEIGHTS, not pixels; that the PNG on disk decodes and that the live page serves it are proven outside, by nx_page_verify." as *u8)
234}
nx_worldpipe_render_gate.nx source

`nx_worldpipe_render_gate.nx` source
