nx_ltv_pure_gate.nx source
↩ module page · 110 lines · 7549 B
1// nx_ltv_pure_gate.nx -- INDEPENDENT GATE over the PURE DECISION CORE of nx_ltv_lib.
2// ZERO registry writes: proves the PAdES level ladder and the three-valued verdict independently of
3// storage, so a seg_store stall (debt 1785519597) can never make the rules unverifiable.
4//
5// Because pure evaluation is free, the ladder is swept EXHAUSTIVELY over all 64 component combinations
6// and the verdict over every (level x revoked x before/after expiry) cell, rather than on hand-picked
7// cases. Two invariants are asserted across the whole sweep: the level is MONOTONE (adding a component
8// never lowers it), and a revoked certificate is INVALID at EVERY level -- so no combination anywhere
9// can launder a revocation.
10// license_tier: ORIGINAL No hw writes (Rule 26). expect_exit: 0
11
12import "nx_ltv_lib.nx"
13import "nx_gate_verdict.nx"
14
15func main(argc: i64, argv: *i64) -> i64 {
16 let ctr: *i64 = gv_ctr()
17 let lbl: *u8 = sys_mmap(32)
18
19 let expiry: i64 = 20365
20 let early: i64 = 20100
21 let late: i64 = 21000
22 let sunset: i64 = 22000
23
24 gv_head("NISHI-LTV-PURE-GATE (PAdES ladder + three-valued verdict, zero storage, exhaustive sweep)" as *u8)
25
26 // ---- L: the ladder, rung by rung ----
27 gv_check("L0 nothing -> NONE" as *u8, ltv_level_pure(0, 0, 0, 0, 0, 0) == LTV_NONE, ctr)
28 gv_check("L1 signed attrs WITHOUT the signer cert -> NONE" as *u8, ltv_level_pure(1, 0, 0, 0, 0, 0) == LTV_NONE, ctr)
29 gv_check("L1a signer cert WITHOUT signed attrs -> NONE" as *u8, ltv_level_pure(0, 1, 0, 0, 0, 0) == LTV_NONE, ctr)
30 gv_check("L2 attrs + cert -> B-B" as *u8, ltv_level_pure(1, 1, 0, 0, 0, 0) == LTV_B, ctr)
31 gv_check("L3 + timestamp -> B-T" as *u8, ltv_level_pure(1, 1, 1, 0, 0, 0) == LTV_T, ctr)
32 gv_check("L4 + chain but NO revocation data -> still B-T (the half-measure)" as *u8, ltv_level_pure(1, 1, 1, 1, 0, 0) == LTV_T, ctr)
33 gv_check("L4a revocation data WITHOUT the chain -> also still B-T" as *u8, ltv_level_pure(1, 1, 1, 0, 1, 0) == LTV_T, ctr)
34 gv_check("L5 chain AND revocation -> B-LT" as *u8, ltv_level_pure(1, 1, 1, 1, 1, 0) == LTV_LT, ctr)
35 gv_check("L6 + archive timestamp -> B-LTA" as *u8, ltv_level_pure(1, 1, 1, 1, 1, 1) == LTV_LTA, ctr)
36 gv_check("L7 an archive timestamp cannot skip the lower rungs" as *u8, ltv_level_pure(1, 1, 0, 0, 0, 1) == LTV_B, ctr)
37
38 // ---- M: EXHAUSTIVE sweep of all 64 component combinations ----
39 // Invariant 1: the level is MONOTONE -- adding any single component never LOWERS the level.
40 // Invariant 2: a revoked certificate is INVALID at EVERY combination, so nothing can launder it.
41 var mono_viol: i64 = 0
42 var launder: i64 = 0
43 var selfc_viol: i64 = 0
44 var i: i64 = 0
45 while i < 64 {
46 let sa: i64 = (i / 32) % 2
47 let sc: i64 = (i / 16) % 2
48 let ts: i64 = (i / 8) % 2
49 let ch: i64 = (i / 4) % 2
50 let rv: i64 = (i / 2) % 2
51 let ar: i64 = i % 2
52 let base: i64 = ltv_level_pure(sa, sc, ts, ch, rv, ar)
53
54 // adding each absent component must never reduce the level
55 if ltv_level_pure(1, sc, ts, ch, rv, ar) < base { mono_viol = mono_viol + 1 }
56 if ltv_level_pure(sa, 1, ts, ch, rv, ar) < base { mono_viol = mono_viol + 1 }
57 if ltv_level_pure(sa, sc, 1, ch, rv, ar) < base { mono_viol = mono_viol + 1 }
58 if ltv_level_pure(sa, sc, ts, 1, rv, ar) < base { mono_viol = mono_viol + 1 }
59 if ltv_level_pure(sa, sc, ts, ch, 1, ar) < base { mono_viol = mono_viol + 1 }
60 if ltv_level_pure(sa, sc, ts, ch, rv, 1) < base { mono_viol = mono_viol + 1 }
61
62 // a revoked cert is INVALID everywhere, before and after expiry alike
63 if ltv_verify_pure(base, 1, early, expiry) != LTV_INVALID { launder = launder + 1 }
64 if ltv_verify_pure(base, 1, late, expiry) != LTV_INVALID { launder = launder + 1 }
65
66 // self-containment must agree with the level threshold everywhere
67 if base >= LTV_LT {
68 if ltv_self_contained_pure(base) != 1 { selfc_viol = selfc_viol + 1 }
69 }
70 if base < LTV_LT {
71 if ltv_self_contained_pure(base) != 0 { selfc_viol = selfc_viol + 1 }
72 }
73 i = i + 1
74 }
75 gv_check("M1 level is MONOTONE across all 64 combinations" as *u8, mono_viol == 0, ctr)
76 gv_check("M2 a revoked cert is INVALID in all 128 (combination x epoch) cells" as *u8, launder == 0, ctr)
77 gv_check("M3 self-containment matches the B-LT threshold everywhere" as *u8, selfc_viol == 0, ctr)
78
79 // ---- V: the three-valued verdict ----
80 gv_check("V0 INDETERMINATE and INVALID are DISTINCT values" as *u8, LTV_INDETERMINATE == LTV_INVALID == 0, ctr)
81 gv_check("V1 B-B before expiry -> VALID" as *u8, ltv_verify_pure(LTV_B, 0, early, expiry) == LTV_VALID, ctr)
82 gv_check("V2 B-B AFTER expiry -> INDETERMINATE, NOT invalid" as *u8, ltv_verify_pure(LTV_B, 0, late, expiry) == LTV_INDETERMINATE, ctr)
83 gv_check("V3 B-T after expiry -> STILL INDETERMINATE" as *u8, ltv_verify_pure(LTV_T, 0, late, expiry) == LTV_INDETERMINATE, ctr)
84 gv_check("V4 B-LT after expiry -> VALID (proof travels inside)" as *u8, ltv_verify_pure(LTV_LT, 0, late, expiry) == LTV_VALID, ctr)
85 gv_check("V5 B-LTA after expiry -> VALID" as *u8, ltv_verify_pure(LTV_LTA, 0, late, expiry) == LTV_VALID, ctr)
86 gv_check("V6 NONE is INDETERMINATE even before expiry" as *u8, ltv_verify_pure(LTV_NONE, 0, early, expiry) == LTV_INDETERMINATE, ctr)
87 gv_check("V7 revoked at B-LTA -> INVALID, LTV is not a laundry" as *u8, ltv_verify_pure(LTV_LTA, 1, late, expiry) == LTV_INVALID, ctr)
88 gv_check("V8 unknown as-of date -> INDETERMINATE, never guessed" as *u8, ltv_verify_pure(LTV_LT, 0, LTV_UNSET, expiry) == LTV_INDETERMINATE, ctr)
89 gv_check("V8a unknown expiry -> INDETERMINATE" as *u8, ltv_verify_pure(LTV_B, 0, early, LTV_UNSET) == LTV_INDETERMINATE, ctr)
90 gv_check("V9 but revocation still wins over an unknown date" as *u8, ltv_verify_pure(LTV_LTA, 1, LTV_UNSET, LTV_UNSET) == LTV_INVALID, ctr)
91
92 ltv_verdict_label(ltv_verify_pure(LTV_B, 0, late, expiry), lbl)
93 gv_check("V10 expired B-B label" as *u8, mt_streq(lbl, "INDETERMINATE" as *u8) == 1, ctr)
94 ltv_verdict_label(ltv_verify_pure(LTV_LTA, 1, late, expiry), lbl)
95 gv_check("V10a revoked label" as *u8, mt_streq(lbl, "INVALID" as *u8) == 1, ctr)
96 ltv_level_label(LTV_LTA, lbl)
97 gv_check("V11 B-LTA label" as *u8, mt_streq(lbl, "B-LTA" as *u8) == 1, ctr)
98 ltv_level_label(LTV_NONE, lbl)
99 gv_check("V11a NONE label" as *u8, mt_streq(lbl, "NONE" as *u8) == 1, ctr)
100
101 // ---- R: archive-timestamp renewal ----
102 gv_check("R1 B-LT never made the archival promise -> never needs renewal" as *u8, ltv_needs_renewal_pure(LTV_LT, 22500, sunset, LTV_UNSET) == 0, ctr)
103 gv_check("R2 B-LTA before the sunset -> no renewal needed" as *u8, ltv_needs_renewal_pure(LTV_LTA, late, sunset, LTV_UNSET) == 0, ctr)
104 gv_check("R3 B-LTA past the sunset, never renewed -> NEEDS renewal" as *u8, ltv_needs_renewal_pure(LTV_LTA, 22500, sunset, LTV_UNSET) == 1, ctr)
105 gv_check("R4 renewed at/after the sunset -> satisfied" as *u8, ltv_needs_renewal_pure(LTV_LTA, 22500, sunset, 22100) == 0, ctr)
106 gv_check("R5 a renewal BEFORE the sunset does not count" as *u8, ltv_needs_renewal_pure(LTV_LTA, 22500, sunset, 21000) == 1, ctr)
107 gv_check("R6 unknown sunset -> no spurious renewal demand" as *u8, ltv_needs_renewal_pure(LTV_LTA, 22500, LTV_UNSET, LTV_UNSET) == 0, ctr)
108
109 return gv_verdict("PADES-LTV" as *u8, ctr, "monotone ladder over 64 combos; revocation INVALID in all 128 cells" as *u8)
110}