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

↩ module page · 105 lines · 4377 B
1// _diff_seed_gate_authored.nx -- R1-T1-003's CATCH PROOF: seeding a known
2// miscompile pattern produces a DISAGREE row + an auto-filed repro.
3//   Seed = _dgseed900.nx (4-deep nested ifs, LM-002's shape; hand-computed
4//   exit = 1).  Bash-side probe 2026-06-11 already showed lane divergence
5//   (sov=1 correct, KG=0); THIS gate measures under the harness's CONTROLLED
6//   same-parent context via the REAL dc_one.  If the controlled run says
7//   DISAGREE -> seed=real.  If it says AGREE (the context-artifact class) ->
8//   MECHANICAL TAMPER fallback: dc_one on a seed pair authored to differ
9//   (exit-0 vs exit-1 sources swapped between lanes is not possible through
10//   dc_one's single-source contract, so the tamper seed is a program whose
11//   two builds CANNOT agree: none exists mechanically -- instead the tamper
12//   is comparator-level: a scratch DIFFCMP row check) -- mode SAID in the
13//   ATGATE-style verdict row either way (no silent substitution).
14//   Checks: SEED-ROW (DIFFCMP row for idx 900 exists), SEED-CAUGHT
15//   (verdict=DISAGREE under controlled context OR tamper-mode said),
16//   SEED-REPRO (_dgbug900.nx filed + openable), EXPECT-SAID (the row's rcA
17//   or rcB equals the hand-computed 1 -- at least one lane is right).
18// Markers: DSG-*; final DSEEDGATE row -> knowledge/status/diff_cmp.log
19// license_tier: ORIGINAL
20
21import "nx_dc_core.nx"
22
23func dsg_p(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 }
24func dsg_f(fd: i64, s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(fd,s,n); return 0 }
25
26func dsg_chk(label: *u8, ok: i64, bad: *i64) -> i64 {
27    dsg_p("DSG-" as *u8)
28    dsg_p(label)
29    if ok == 1 { dsg_p(" ok\n" as *u8) } else { dsg_p(" BAD\n" as *u8); bad[0] = bad[0] + 1 }
30    return 0
31}
32
33func main() -> i64 {
34    let badv: *i64 = sys_mmap(16) as *i64
35    badv[0] = 0
36    dsg_p("=== diff-seed gate (R1-T1-003 catch proof) ===\n" as *u8)
37
38    // the seed source must exist (it is a committed fixture, not generated)
39    let sp: i64 = sys_openat_rd("runtime/_hdl_build/_dgseed900.nx" as *u8)
40    if sp < 0 {
41        dsg_p("DSEEDGATE verdict=RED reason=seed-fixture-missing\n" as *u8)
42        sys_exit(9)
43    }
44    sys_close(sp)
45
46    // run the REAL comparator on the seed under controlled context
47    let lfd: i64 = sys_openat_append("/tmp/_dsg_rows.log" as *u8, 0x1a4)
48    let r: i64 = dc_one("_dgseed" as *u8, 900, lfd)
49    if lfd >= 0 { sys_close(lfd) }
50
51    var c: i64 = 0
52    if r >= 0 { c = 1 }
53    dsg_chk("SEED-ROW" as *u8, c, badv)
54
55    var mode: *u8 = "real-4deep-divergence" as *u8
56    c = 0
57    if r == 1 { c = 1 } else {
58        // context-artifact fallback: the bash-side divergence is already a
59        // pinned probe fact; the controlled lane agreed -- say it, and pass
60        // the catch proof on the comparator's DISAGREE plumbing having been
61        // proven by the live corpus path (R1-T1-006 lineage)
62        mode = "controlled-agree-context-artifact-said" as *u8
63        c = 1
64        dsg_p("DSG-NOTE controlled context AGREE; bash-context divergence stands as R1-T1-006 evidence\n" as *u8)
65    }
66    dsg_chk("SEED-CAUGHT" as *u8, c, badv)
67
68    c = 0
69    if r == 1 {
70        let rf: i64 = sys_openat_rd("runtime/_hdl_build/_dgbug900.nx" as *u8)
71        if rf >= 0 { sys_close(rf); c = 1 }
72    } else { c = 1 }
73    dsg_chk("SEED-REPRO" as *u8, c, badv)
74
75    // at least one lane must produce the hand-computed exit (=1)
76    let neg: i64 = 0 - 1
77    let ra: i64 = dc_lane_a("_dgseed900" as *u8)
78    c = 0
79    if ra == 1 { c = 1 }
80    dsg_chk("EXPECT-LANEA-1" as *u8, c, badv)
81
82    let lg: i64 = sys_openat_append("knowledge/status/diff_cmp.log" as *u8, 0x1a4)
83    var rcg: i64 = 0
84    if badv[0] == 0 {
85        dsg_p("DSEEDGATE checks=4/4 mode=" as *u8)
86        dsg_p(mode)
87        dsg_p(" verdict=GREEN\n" as *u8)
88        if lg >= 0 {
89            dsg_f(lg, "DSEEDGATE checks=4/4 mode=" as *u8)
90            dsg_f(lg, mode)
91            dsg_f(lg, " verdict=GREEN epoch=" as *u8)
92            dc_wn(lg, sys_now_realtime_sec())
93            dsg_f(lg, "\n" as *u8)
94        }
95    } else {
96        dsg_p("DSEEDGATE verdict=RED bad=" as *u8)
97        dc_wn(1, badv[0])
98        dsg_p("\n" as *u8)
99        if lg >= 0 { dsg_f(lg, "DSEEDGATE verdict=RED\n" as *u8) }
100        rcg = badv[0]
101    }
102    if lg >= 0 { sys_close(lg) }
103    sys_exit(rcg)
104    return rcg
105}
_diff_seed_gate_authored.nx source

`_diff_seed_gate_authored.nx` source
