nx_srcfresh_gate.nx source
↩ module page · 148 lines · 7912 B
1// nx_srcfresh_gate.nx -- TEETH FOR THE EXTRACTED FRESHNESS PREDICATE (nx_srcfresh.nx).
2//
3// T1-T5 are DELIBERATELY THE SAME FIVE CASES _freshness_gate.nx already locks against the original
4// oi_src_stale, re-asserted against the extracted copy. An extraction that is not re-asserted is a claim of
5// equivalence, not a proof of it -- and the copies already in this tree are exactly what happens when the
6// claim is trusted (several read only tv_sec and disagree with the predicate the gate proved).
7//
8// T6/T7 ARE THE LOAD-BEARING PAIR AND ARE NEW. They set two files to the SAME SECOND and different
9// NANOSECONDS. Every second-granularity implementation of this predicate answers 0 (fresh) for T6, because
10// the two mtimes compare EQUAL -- so T6 is the tooth that fails for the copies and passes only for a real
11// nanosecond comparison. T7 drives the same fixture the other way so the pair discriminates in BOTH
12// directions and cannot be satisfied by a function that simply always returns 1.
13// LAW: A TOOTH THAT ONLY THE CORRECT IMPLEMENTATION PASSES IS THE ONLY KIND WORTH ADDING TO A COPY.
14//
15// T8-T10 lock the MAGNITUDE, including the absent-artifact case returning -1 rather than 0: "no measurable
16// lag" and "no lag" are different facts, and folding them is the defect class this session kept finding.
17// DETERMINISTIC: mtimes are set explicitly via sys_utimensat -- no sleeps, no filesystem-resolution races.
18// Fixtures live in /tmp and are unlinked at the end. Inherits nx_gate_verdict (D001).
19// license_tier: ORIGINAL No hw writes (Rule 26). expect_exit: 0
20import "nx_syscalls.nx"
21import "nx_srcfresh.nx"
22import "nx_gate_verdict.nx"
23
24const SG_MODE: i64 = 420 // 0644
25const SG_BASE: i64 = 1700000000 // fixed epoch -- the clock is set, never observed
26const SG_LAG: i64 = 100 // seconds the source leads the artifact in T8
27const SG_RT: i64 = 1700000042 // round-trip probe value
28const SG_NS_LO: i64 = 500
29const SG_NS_HI: i64 = 900
30const SG_TSBUF: i64 = 64
31
32func sg_len(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } return n }
33func sg_cat(d: *u8, at: i64, s: *u8) -> i64 {
34 var a: i64 = at
35 var i: i64 = 0
36 while s[i] != (0 as u8) { d[a] = s[i]; a = a + 1; i = i + 1 }
37 d[a] = 0 as u8
38 return a
39}
40func sg_write(path: *u8, content: *u8) -> i64 {
41 let fd: i64 = sys_openat_wr(path, SG_MODE)
42 if fd < 0 { return 0 }
43 sys_write(fd, content, sg_len(content))
44 sys_close(fd)
45 return 1
46}
47// set atime+mtime to (sec, nsec). ts = [atime_sec, atime_nsec, mtime_sec, mtime_nsec].
48func sg_set(path: *u8, sec: i64, nsec: i64) -> i64 {
49 let ts: *i64 = sys_mmap(SG_TSBUF) as *i64
50 ts[0] = sec
51 ts[1] = nsec
52 ts[2] = sec
53 ts[3] = nsec
54 return sys_utimensat(path, ts)
55}
56
57func main(argc: i64, argv: *i64) -> i64 {
58 let ctr: *i64 = gv_ctr()
59 gv_head("nx_srcfresh_gate -- is this artifact built from this source?" as *u8)
60
61 let src: *u8 = "/tmp/_sfsrc" as *u8
62 let art: *u8 = "/tmp/_sfart" as *u8
63 let gone: *u8 = "/tmp/_sfgone_zzq" as *u8
64
65 sys_unlinkat(gone)
66 sg_write(src, "source-v1" as *u8)
67 sg_write(art, "artifact-v1" as *u8)
68
69 // T1 artifact strictly older than source -> STALE
70 sg_set(art, SG_BASE, 0)
71 sg_set(src, SG_BASE + SG_LAG, 0)
72 gv_check("T1 detect-stale" as *u8, (sf_src_stale(art, src) == 1) as i64, ctr)
73
74 // T2 NEG-CONTROL: artifact newer -> NOT stale. Without this, a function that always returns 1 passes T1.
75 sg_set(art, SG_BASE + SG_LAG + SG_LAG, 0)
76 gv_check("T2 neg-control-fresh" as *u8, (sf_src_stale(art, src) == 0) as i64, ctr)
77
78 // T3 artifact absent while the source exists -> STALE (never built)
79 gv_check("T3 artifact-absent-is-stale" as *u8, (sf_src_stale(gone, src) == 1) as i64, ctr)
80
81 // T4 no source -> nothing to be stale against (the deliberate asymmetry with T3)
82 gv_check("T4 source-absent-is-not-stale" as *u8, (sf_src_stale(art, gone) == 0) as i64, ctr)
83
84 // T5 the stat is REAL, not a constant: set a value, read it back
85 sg_set(art, SG_RT, 0)
86 gv_check("T5 mtime-round-trip" as *u8, (sf_mtime_ns(art) / SF_NS_PER_SEC == SG_RT) as i64, ctr)
87
88 // T6 SAME SECOND, artifact nsec LOWER -> STALE. A tv_sec-only implementation returns 0 here and FAILS.
89 sg_set(art, SG_BASE, SG_NS_LO)
90 sg_set(src, SG_BASE, SG_NS_HI)
91 gv_check("T6 same-second-nsec-STALE" as *u8, (sf_src_stale(art, src) == 1) as i64, ctr)
92
93 // T7 same second, artifact nsec HIGHER -> fresh. Both directions, so T6 cannot pass by always-stale.
94 sg_set(art, SG_BASE, SG_NS_HI)
95 sg_set(src, SG_BASE, SG_NS_LO)
96 gv_check("T7 same-second-nsec-FRESH" as *u8, (sf_src_stale(art, src) == 0) as i64, ctr)
97
98 // T8 magnitude: source leads by exactly SG_LAG seconds
99 sg_set(art, SG_BASE, 0)
100 sg_set(src, SG_BASE + SG_LAG, 0)
101 gv_check("T8 lag-seconds-exact" as *u8, (sf_lag_sec(art, src) == SG_LAG) as i64, ctr)
102
103 // T9 a fresh artifact has ZERO lag, not a negative one
104 sg_set(art, SG_BASE + SG_LAG + SG_LAG, 0)
105 gv_check("T9 lag-zero-when-fresh" as *u8, (sf_lag_sec(art, src) == 0) as i64, ctr)
106
107 // T10 an ABSENT artifact has NO MEASURABLE lag (-1), which must not read as "no lag" (0)
108 gv_check("T10 lag-absent-is-minus-one-not-zero" as *u8, (sf_lag_sec(gone, src) == (0 - 1)) as i64, ctr)
109
110 // ==== T11-T15 PROVENANCE (debt 1786113214). Everything above ORDERS writes; these test IDENTITY. ====
111 let prov: *u8 = "/tmp/_sfprov" as *u8
112 sys_unlinkat(prov)
113 sg_write(src, "source-v2-for-provenance" as *u8)
114 // T11 no sidecar -> UNKNOWN. It must NOT read as FRESH: an absent receipt is not agreement.
115 gv_check("T11 no-sidecar-is-UNKNOWN-not-fresh" as *u8, (sf_prov_stale(prov, src) == (0 - 1)) as i64, ctr)
116 let hex: *u8 = sys_mmap(SF_HEXBUF)
117 sf_file_sha_hex(src, hex)
118 let line: *u8 = sys_mmap(512)
119 var lo: i64 = sg_cat(line, 0, "src_sha256=" as *u8)
120 lo = sg_cat(line, lo, hex)
121 sg_cat(line, lo, " elf_sha256=deadbeef src_stable=1" as *u8)
122 sg_write(prov, line)
123 // T12 a sidecar recording the CURRENT digest -> FRESH, by exact content identity, no clock involved.
124 gv_check("T12 matching-digest-is-FRESH" as *u8, (sf_prov_stale(prov, src) == 0) as i64, ctr)
125 // T13 NEG-CONTROL: a recorded digest that is not the current one -> STALE. Without this, a function that
126 // always answered 0 would pass T12.
127 sg_write(prov, "src_sha256=0000000000000000000000000000000000000000000000000000000000000000 src_stable=1" as *u8)
128 gv_check("T13 mismatching-digest-is-STALE" as *u8, (sf_prov_stale(prov, src) == 1) as i64, ctr)
129 // T14 IS WHY THIS API EXISTS. Make the artifact mtime NEWER than the source, so every mtime-based check
130 // in this very file answers FRESH -- then show provenance answering STALE on the same fixtures. This is
131 // the exact false-FRESH that bit nx_gatefresh on nx_mgmt_api hours after it shipped: a concurrent promote
132 // reset the artifact mtime and erased the evidence of an unadopted source edit.
133 // A TOOTH THAT PROVES THE NEW MEASURE SEES WHAT THE OLD ONE CANNOT IS THE ONLY JUSTIFICATION FOR ADDING IT.
134 sg_set(src, SG_BASE, 0)
135 sg_set(art, SG_BASE + SG_LAG, 0)
136 var ok14: i64 = 0
137 if sf_src_stale(art, src) == 0 {
138 if sf_prov_stale(prov, src) == 1 { ok14 = 1 }
139 }
140 gv_check("T14 provenance-catches-the-false-FRESH-that-mtime-misses" as *u8, ok14, ctr)
141 // T15 a HALF-WRITTEN sidecar (hex too short) must read UNKNOWN, never agreement. Fail closed.
142 sg_write(prov, "src_sha256=abc123" as *u8)
143 gv_check("T15 malformed-sidecar-is-UNKNOWN-not-fresh" as *u8, (sf_prov_stale(prov, src) == (0 - 1)) as i64, ctr)
144 sys_unlinkat(prov)
145
146 sys_unlinkat(src)
147 sys_unlinkat(art)
148 return gv_verdict("SRCFRESH-GATE" as *u8, ctr, "mtime ordering (incl. same-second nsec) PLUS content provenance, with the false-FRESH discriminator T14" as *u8)
149}