code wiki / _hdl_build / nx_hairdyn_gate.nx
`nx_hairdyn_gate.nx` source

↩ module page · 258 lines · 12803 B
1// nx_hairdyn_gate.nx -- GATE: prove the hair chain is a CHAIN, that its plant is DERIVED rather
2// than tuned, and that the measurement which says so cannot pass on hair that does not move.
3//
4// WHAT THIS GATE IS FOR. knowledge/gamefeel_oracle.conf's hair_k_q10 row has never had a plant
5// behind it; the shipping hair was two hand-picked integers driving one point. The teeth below do
6// not assert that hair is right, they MEASURE it: ask the derivation for a frequency, run a free
7// decay, and read the frequency back out with the estate's one ringdown analyser.
8//
9// NO TOLERANCE IS CHOSEN ANYWHERE IN THIS FILE. The frequency teeth compare against the DAMPED
10// prediction (a ringdown cannot measure an undamped frequency) inside the ANALYSER'S OWN
11// resolution, both derived below. The damping teeth assert MONOTONICITY, which needs no tolerance
12// at all -- a stronger property than an equality with a number picked to make it hold.
13//
14// license_tier: ORIGINAL   No hw writes (Rule 26).
15import "nx_syscalls.nx"
16import "nx_gate_verdict.nx"
17import "nx_hairdyn_lib.nx"
18
19const HG_NSEG: i64 = 6
20const HG_NSEG_SHORT: i64 = 2
21const HG_NSEG_LONG: i64 = 12
22// segment length is pure GEOMETRY -- T4 exists precisely to prove the frequency does not depend on
23// it, so these two differ by a factor of two and nothing else.
24const HG_SEGLEN_A: i64 = 256
25const HG_SEGLEN_B: i64 = 512
26// ZETA TEST POINTS ARE BANKED VALUES, NOT INVENTED. 100 and 300 permil are the exact endpoints of
27// knowledge/gamefeel_oracle.conf's chest_zeta_permil row -- the estate's own banked band for
28// "underdamped envelope, VISIBLE oscillation". Using its endpoints means both points are, by the
29// estate's own definition, in the regime where a decrement is measurable, rather than two numbers
30// chosen by me because they happened to pass. A gate that invents its own constants to test a lane
31// about invented constants would be its own counter-example.
32const HG_ZETA_LO: i64 = 100
33const HG_ZETA_HI: i64 = 300
34
35// A ringdown measures the DAMPED natural frequency fn*sqrt(1-zeta^2), never the undamped one.
36// Comparing a measurement against the UNDAMPED target is an error that GROWS WITH DAMPING -- at
37// 480 permil it is a 12% offset, easily large enough to read as a broken derivation and send the
38// next reader into a solver that is working correctly. Integer form: sqrt(1-z^2) for z in permil
39// is isqrt(10^6 - z^2)/1000, exact enough that the instrument resolution below dominates it.
40func hg_fn_damped(fn_mhz: i64, zeta_permil: i64) -> i64 {
  return fn_mhz * rd_isqrt(1000000 - zeta_permil*zeta_permil) / 1000
42}
43
44// THE INSTRUMENT'S OWN RESOLUTION, DERIVED -- never a tolerance chosen to make a test pass.
45// rd_analyze times one full period by counting SAMPLES between zero crossings, so the period is
46// known to +-1 sample. With P samples per period a one-sample error moves the frequency by about
47// fn/P, and P = ticks_per_second*1000/fn_mhz. The +1 absorbs the integer division's truncation.
48// This is why the bar TIGHTENS at low frequency (more samples per period) rather than being one
49// slack number across the range.
50func hg_res_mhz(fn_mhz: i64) -> i64 {
  let per_samples: i64 = hd_ticks_per_s()*1000/fn_mhz
  if per_samples < 1 { return fn_mhz }
  return fn_mhz/per_samples + 1
54}
55
56func hg_report(tag: *u8, rc: i64, out: *i64) -> i64 {
  gv_puts("    " as *u8)
  gv_puts(tag)
  gv_puts(": fn=" as *u8)
  gv_num(out[RD_R_FN_MHZ])
  gv_puts(" mhz zeta=" as *u8)
  gv_num(out[RD_R_ZETA])
  gv_puts(" permil peaks=" as *u8)
  gv_num(out[RD_R_PEAKS])
  gv_puts(" a1=" as *u8)
  gv_num(out[RD_R_A1])
  gv_puts(" a2=" as *u8)
  gv_num(out[RD_R_A2])
  gv_puts(" resid=" as *u8)
  gv_num(out[RD_R_RESID])
  gv_puts(" rc=" as *u8)
  gv_num(rc)
  gv_puts(" " as *u8)
  gv_puts(rd_reason(rc))
  gv_puts("\n" as *u8)
  return 0
77}
78
79func main() -> i64 {
  let ctr: *i64 = gv_ctr()
  gv_head("nx_hairdyn gate -- hair as a CHAIN on the one solver, plant MEASURED in band units" as *u8)
  let out: *i64 = sys_mmap(RD_R_N*8 + 64) as *i64
  let tipS: *i64 = sys_mmap(HD_RD_SAMPLES*8 + 64) as *i64
  let rootS: *i64 = sys_mmap(HD_RD_SAMPLES*8 + 64) as *i64
  let lag: *i64 = sys_mmap(64) as *i64
86
  gv_puts("  tick rate DERIVED from nx_softbind SB_MHZ_TICK_SQ = " as *u8)
  gv_num(hd_ticks_per_s())
  gv_puts(" hz, sample period " as *u8)
  gv_num(hd_dt_us())
  gv_puts(" us, excitation " as *u8)
  gv_num(hd_amp_q8())
  gv_puts(" q8 (half the banked SB_MAXD_HAIR clamp)\n" as *u8)
94
  // ---- T1: the frequency derivation round-trips, at BOTH ends of the proven range. Two points,
  // because a single frequency that happens to read back is a coincidence, not a derivation.
  var rt: i64 = 1
  var reached: i64 = 0
  var fi: i64 = 0
  while fi < 2 {
      var fn: i64 = HD_FN_LO_MHZ
      if fi == 1 { fn = HD_FN_HI_MHZ }
      let rc: i64 = hd_ringdown(HG_NSEG, HG_SEGLEN_A, fn, HG_ZETA_LO, out)
      let want: i64 = hg_fn_damped(fn, HG_ZETA_LO)
      let got: i64 = out[RD_R_FN_MHZ]
      let res: i64 = hg_res_mhz(fn)
      gv_puts("  ask fn=" as *u8)
      gv_num(fn)
      gv_puts(" zeta=" as *u8)
      gv_num(HG_ZETA_LO)
      gv_puts(" -> damped-predicted " as *u8)
      gv_num(want)
      gv_puts(" +-" as *u8)
      gv_num(res)
      gv_puts("\n" as *u8)
      hg_report("measured" as *u8, rc, out)
      if rc == RD_OK { reached = reached + 1 }
      if rc != RD_OK { rt = 0 }
      if got < want - res { rt = 0 }
      if got > want + res { rt = 0 }
      fi = fi + 1
  }
  // BIND THE ASSERTION TO ITS DENOMINATOR: a tooth that passes because the loop never ran is not
  // a tooth. Both frequencies must actually have produced a measurable decay.
  if reached != 2 { rt = 0 }
  gv_check("fixture-reached-the-condition: BOTH endpoint ringdowns produced a measurable plant" as *u8, reached == 2, ctr)
  gv_check("frequency derivation ROUND-TRIPS at both ends (damped-corrected, within analyser resolution)" as *u8, rt, ctr)
128
  // ---- T2: damping is actually driven by the derivation: more requested zeta, more measured zeta.
  // MONOTONICITY, so no tolerance is needed and none is invented.
  let rzl: i64 = hd_ringdown(HG_NSEG, HG_SEGLEN_A, HD_FN_HI_MHZ, HG_ZETA_LO, out)
  let zlo: i64 = out[RD_R_ZETA]
  hg_report("zeta-lo" as *u8, rzl, out)
  let rzh: i64 = hd_ringdown(HG_NSEG, HG_SEGLEN_A, HD_FN_HI_MHZ, HG_ZETA_HI, out)
  let zhi: i64 = out[RD_R_ZETA]
  hg_report("zeta-hi" as *u8, rzh, out)
  var zmono: i64 = 0
  if rzl == RD_OK {
      if rzh == RD_OK {
          if zhi > zlo { zmono = 1 }
      }
  }
  gv_check("measured damping RISES with requested damping (both observable, monotone)" as *u8, zmono, ctr)
144
  // ---- T3: frequency is set by the SPRING, not by the geometry. Same plant, segment length
  // doubled: the measured frequency must not move. This is what makes the derivation meaningful --
  // if geometry moved the frequency, sb_k_sym would not be the ruler that sets it.
  let rg1: i64 = hd_ringdown(HG_NSEG, HG_SEGLEN_A, HD_FN_HI_MHZ, HG_ZETA_LO, out)
  let fg1: i64 = out[RD_R_FN_MHZ]
  let rg2: i64 = hd_ringdown(HG_NSEG, HG_SEGLEN_B, HD_FN_HI_MHZ, HG_ZETA_LO, out)
  let fg2: i64 = out[RD_R_FN_MHZ]
  var ginv: i64 = 0
  if rg1 == RD_OK {
      if rg2 == RD_OK {
          if fg1 == fg2 { ginv = 1 }
      }
  }
  gv_puts("  seglen " as *u8)
  gv_num(HG_SEGLEN_A)
  gv_puts(" -> " as *u8)
  gv_num(fg1)
  gv_puts(" mhz ; seglen " as *u8)
  gv_num(HG_SEGLEN_B)
  gv_puts(" -> " as *u8)
  gv_num(fg2)
  gv_puts(" mhz\n" as *u8)
  gv_check("frequency is INVARIANT to segment length (the spring sets it, not the geometry)" as *u8, ginv, ctr)
168
  // ---- T4: it is a CHAIN, not N independent copies of one spring. The tip must LAG the root, and
  // that lag must GROW with chain length. N uncoupled springs would give the same lag at any
  // length; only one-hop coupling makes the delay accumulate down the strand.
  let rl1: i64 = hd_ringdown_t(HG_NSEG_SHORT, HG_SEGLEN_A, HD_FN_HI_MHZ, HG_ZETA_LO, out, tipS, rootS)
  var lag_short: i64 = 0 - 1
  if rl1 == RD_OK {
      let ps1: i64 = out[RD_R_PER_US]/hd_dt_us()
      if rd_phase_lag_permil(rootS, tipS, HD_RD_SAMPLES, ps1, lag) == RD_OK { lag_short = lag[0] }
  }
  let rl2: i64 = hd_ringdown_t(HG_NSEG_LONG, HG_SEGLEN_A, HD_FN_HI_MHZ, HG_ZETA_LO, out, tipS, rootS)
  var lag_long: i64 = 0 - 1
  if rl2 == RD_OK {
      let ps2: i64 = out[RD_R_PER_US]/hd_dt_us()
      if rd_phase_lag_permil(rootS, tipS, HD_RD_SAMPLES, ps2, lag) == RD_OK { lag_long = lag[0] }
  }
  gv_puts("  tip-vs-root phase lag: " as *u8)
  gv_num(HG_NSEG_SHORT)
  gv_puts(" segments -> " as *u8)
  gv_num(lag_short)
  gv_puts(" permil of a period ; " as *u8)
  gv_num(HG_NSEG_LONG)
  gv_puts(" segments -> " as *u8)
  gv_num(lag_long)
  gv_puts(" permil\n" as *u8)
  var chain: i64 = 0
  if lag_short >= 0 {
      if lag_long > lag_short { chain = 1 }
  }
  gv_check("IT IS A CHAIN: tip-vs-root phase lag GROWS with strand length" as *u8, chain, ctr)
198
  // ---- T5: THE ANTI-VACUITY TOOTH. A RIGID hair chain -- joints that exist and follow the head
  // but carry no dynamics, i.e. the trivial wrong implementation that reads on screen as a helmet
  // -- MUST NOT yield a plant. If this passes, every measurement above is decoration, because the
  // instrument would be reporting a frequency for hair that does not move.
  let rr: i64 = hd_ringdown_rigid(HG_NSEG, HG_SEGLEN_A, out)
  hg_report("RIGID control" as *u8, rr, out)
  gv_check("neg-control-rigid-chain-cannot-produce-a-plant (third state, not a frequency)" as *u8, rr != RD_OK, ctr)
  // and it must not fake the CHAIN property either: no dynamics, no lag.
  var rigid_lag: i64 = 0 - 1
  if rd_phase_lag_permil(rootS, rootS, HD_RD_SAMPLES, 8, lag) == RD_OK { rigid_lag = lag[0] }
  gv_check("neg-control-a-signal-against-itself-has-zero-lag (the lag probe is not fabricating)" as *u8, rigid_lag == 0, ctr)
210
  // ---- T6: THE SHIPPED PLANT, MEASURED. nx_softbind's SB_K_HAIR / SB_C_HAIR are two hand-picked
  // integers that were never derived from a frequency. This does not assert them against a band --
  // there IS no citable hair band (see the lib header: the source slug resolves to nothing) -- it
  // REPORTS what the estate has actually been shipping, in the units a band would use.
  let rs: i64 = hd_ringdown_kc(HG_NSEG, HG_SEGLEN_A, SB_K_HAIR, SB_C_HAIR, out)
  gv_puts("  SHIPPED nx_softbind hair plant K=" as *u8)
  gv_num(SB_K_HAIR)
  gv_puts(" C=" as *u8)
  gv_num(SB_C_HAIR)
  gv_puts(":\n" as *u8)
  hg_report("shipped" as *u8, rs, out)
  gv_check("the SHIPPED hair plant is observable at all (a plant nobody can measure is not a plant)" as *u8, rs == RD_OK, ctr)
223
  // ---- T7: ANTI-DRIFT. nx_softbind now states the shipped hair plant twice -- once as the two
  // per-1024 integers the solver consumes, and once as the frequency and damping ratio a reader
  // (or a future citation) can understand. Two spellings of one fact is exactly how a citation
  // quietly stops being load-bearing, so the equality is asserted here rather than trusted. If
  // anyone edits either side, this goes RED instead of the two drifting apart in silence.
  let kfrom: i64 = sb_k_sym(SB_HAIR_FN_MHZ)
  let cfrom: i64 = sb_c_for_zeta(SB_K_HAIR, SB_HAIR_ZETA_PERMIL)
  gv_puts("  shipped K " as *u8)
  gv_num(SB_K_HAIR)
  gv_puts(" vs sb_k_sym(" as *u8)
  gv_num(SB_HAIR_FN_MHZ)
  gv_puts(" mhz) = " as *u8)
  gv_num(kfrom)
  gv_puts(" ; shipped C " as *u8)
  gv_num(SB_C_HAIR)
  gv_puts(" vs sb_c_for_zeta(K," as *u8)
  gv_num(SB_HAIR_ZETA_PERMIL)
  gv_puts(" permil) = " as *u8)
  gv_num(cfrom)
  gv_puts("\n" as *u8)
  gv_check("the physical spelling of the shipped hair plant is EXACT, not approximate (K)" as *u8, kfrom == SB_K_HAIR, ctr)
  gv_check("the physical spelling of the shipped hair plant is EXACT, not approximate (C)" as *u8, cfrom == SB_C_HAIR, ctr)
  // NEG-CONTROL for that pair: the pinning must be TIGHT. One mhz either side of the declared
  // frequency must NOT still produce the shipped stiffness, or the assertion above would pass for
  // a whole range of frequencies and would be pinning nothing.
  var tight: i64 = 0
  if sb_k_sym(SB_HAIR_FN_MHZ + 30) != SB_K_HAIR {
      if sb_k_sym(SB_HAIR_FN_MHZ - 30) != SB_K_HAIR { tight = 1 }
  }
  gv_check("neg-control-the-frequency-pin-is-tight (a nearby frequency does NOT reproduce it)" as *u8, tight, ctr)
254
  let rc9: i64 = gv_verdict("HAIRDYN" as *u8, ctr, "hair chain plant" as *u8)
  sys_exit(rc9)
  return rc9
258}
nx_hairdyn_gate.nx source

`nx_hairdyn_gate.nx` source
