Skip to content

Commit b9ecf01

Browse files
test: close block-path reject coverage gaps (PRED-04) (#194)
Closes #181. - block.rs: add the missing Requant tampered-output reject test — with it, every one of the 12 BlockOp variants rejects a bumped claimed output with the exact typed error and op_id (Linear/BatchedLinear via Freivalds, the exact-recompute ops via BlockOpMismatch). The accept half pins the hand-computed requant outputs (incl. the ties-to-even case). - lewm_predictor.rs: the small-dims predictor accept tests now pin the exact 24-element integer output vector instead of just is_ok + float tolerance, locking the quantized semantics (kernels, tables, scheme derivation, synthetic weights) end-to-end. Depth 1 and depth 6 pin the same vector: the AdaLN-gated block contributions shift the float reference by less than one f_ln quantization step (documented in the test). - soundness_campaign.rs: add the range_check.modp_predictor mutant — the mod-p accumulator-aliasing forgery (out[0] += p) on a BatchedLinear accumulator, killed only by the block-path Freivalds range guard (asserts the typed AccumulatorRange, not just any rejection) — so the predictor/block path is merge-gated like the flat demo path. Campaign floor raised to 7 mutants. Full workspace suite green (200 tests); real-dims predictor release test unaffected and green. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
1 parent 8c82d9d commit b9ecf01

4 files changed

Lines changed: 132 additions & 14 deletions

File tree

CHANGELOG.md

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -90,6 +90,15 @@ entry.
9090

9191
### Fixed
9292

93+
- Closed the remaining block-path test-coverage gaps (#181): `Requant` was the
94+
one `BlockOp` variant without a tampered-output reject test (all 12 now
95+
reject a bumped claimed output with the exact typed error and `op_id`); the
96+
small-dims predictor accept tests now pin the exact integer output vector
97+
(not just `is_ok` + float tolerance), locking the quantized semantics
98+
end-to-end; and the soundness mutation campaign gained a
99+
`range_check.modp_predictor` mutant — the mod-`p` accumulator-aliasing
100+
forgery on a `BatchedLinear` accumulator — so the predictor/block path's
101+
Freivalds range guard is merge-gated like the flat demo path's.
93102
- The soundness mutation campaign registered no mutant for the `tensor_memory`
94103
(op-to-op wiring) component, so its merge gate passed vacuously; it now exercises
95104
a `WiringMismatch` mutant. The committed `requantize` golden fixture is now run

crates/pwm-testkit/src/lewm_predictor.rs

Lines changed: 29 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -888,7 +888,7 @@ mod tests {
888888
}
889889
}
890890

891-
fn run(d: Dims) {
891+
fn run(d: Dims) -> Vec<i64> {
892892
let c = build_predictor(d);
893893
let artifact = prove(&c).expect("prove");
894894
let out = verify(&artifact).expect("verify");
@@ -899,23 +899,42 @@ mod tests {
899899
err <= c.tolerance.expect("tolerance"),
900900
"float-vs-int error {err} exceeds tolerance"
901901
);
902+
out
902903
}
903904

905+
/// The pinned integer output of the small synthetic predictor (#181): locks
906+
/// the exact quantized semantics end-to-end — kernels, tables, scheme
907+
/// derivation, and the deterministic synthetic weights. Any change to the
908+
/// integer pipeline shows up as a diff here, not just as a tolerance drift.
909+
/// Verified against the float reference within `SYNTH_TOLERANCE` by `run`.
910+
const SMALL_DIMS_OUTPUT: [i64; 24] = [
911+
20, 18, 27, -66, 25, -17, 21, -31, -24, -18, 14, -21, 4, -48, 44, 49, 18, -32, -36, -18,
912+
31, -18, -8, 63,
913+
];
914+
904915
#[test]
905916
fn small_dims_one_block_verifies() {
906-
run(small());
917+
assert_eq!(run(small()), SMALL_DIMS_OUTPUT);
907918
}
908919

909920
#[test]
910921
fn small_dims_six_blocks_verify_within_float_tolerance() {
911-
run(Dims {
912-
d: 8,
913-
s: 3,
914-
h: 2,
915-
dh: 4,
916-
mlp: 16,
917-
depth: 6,
918-
});
922+
// Pins the same vector as the one-block test: the AdaLN-gated block
923+
// contributions at these synthetic weights shift the float reference by
924+
// less than one `f_ln` quantization step, so blocks 2..6 do not move the
925+
// final per-position LayerNorm off the depth-1 grid points (the float
926+
// references differ — ~3e-3 — and both stay within tolerance).
927+
assert_eq!(
928+
run(Dims {
929+
d: 8,
930+
s: 3,
931+
h: 2,
932+
dh: 4,
933+
mlp: 16,
934+
depth: 6,
935+
}),
936+
SMALL_DIMS_OUTPUT
937+
);
919938
}
920939

921940
#[test]

crates/pwm-testkit/src/soundness_campaign.rs

Lines changed: 55 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -15,12 +15,15 @@
1515
//! CI — the gate the green skeleton never provided.
1616
1717
use pwm_core::audit::output_tensor;
18+
use pwm_core::block::{Block, BlockOp};
1819
use pwm_core::commit::claimed_output_commitment;
1920
use pwm_core::field::FREIVALDS_P;
20-
use pwm_core::fixed_point::{requantize, Rounding};
21+
use pwm_core::fixed_point::{requantize, BoundedInt, Rounding};
2122
use pwm_core::planning::verify_argmin;
23+
use pwm_core::tensor::Tensor;
2224
use pwm_core::trace::OpRecord;
23-
use pwm_verifier::{verify, VerifyError};
25+
use pwm_prover::prove_block;
26+
use pwm_verifier::{verify, verify_block, VerifyError};
2427

2528
use crate::demo::prove_demo;
2629
use crate::mutation::{Mutant, MutationCampaign, MutationOperator};
@@ -81,6 +84,47 @@ fn modp_accumulator_rejected() -> bool {
8184
verify(&art).is_err()
8285
}
8386

87+
/// True iff the mod-`p` accumulator-aliasing forgery on the **predictor/block
88+
/// path** (add `p` to a `BatchedLinear` accumulator) is rejected by the live
89+
/// block verifier with the typed range-guard error (#181). Freivalds checks
90+
/// congruence mod `p`, so without the operand range guard this forgery passes
91+
/// every challenge with probability 1 — the named-buffer analog of
92+
/// `range_check.modp_accumulator`. Requiring `AccumulatorRange` (not just any
93+
/// error) pins the rejection to the guard itself.
94+
fn modp_predictor_batched_rejected() -> bool {
95+
// Identity 2x2 weight, two-row batched projection of [3,4],[5,6].
96+
let data = [1i64, 0, 0, 1]
97+
.iter()
98+
.map(|&v| BoundedInt::new(v, -128, 127).expect("i8 weight"))
99+
.collect();
100+
let weights = vec![Tensor::new(10, vec![2, 2], 0, data).expect("2x2 tensor")];
101+
let block = Block {
102+
input_bufs: vec![0],
103+
ops: vec![BlockOp::BatchedLinear {
104+
op_id: 1,
105+
weight_id: 10,
106+
bias_id: None,
107+
in_buf: 0,
108+
out_buf: 1,
109+
out: Vec::new(),
110+
seq: 2,
111+
}],
112+
output_buf: 1,
113+
};
114+
let inputs = vec![(0u32, vec![3, 4, 5, 6])];
115+
let Ok(mut proven) = prove_block(&block, &weights, &[], &inputs) else {
116+
return false;
117+
};
118+
match &mut proven.ops[0] {
119+
BlockOp::BatchedLinear { out, .. } => out[0] += FREIVALDS_P as i64,
120+
_ => return false,
121+
}
122+
matches!(
123+
verify_block(&proven, &weights, &[], &inputs),
124+
Err(VerifyError::AccumulatorRange { op_id: 1 })
125+
)
126+
}
127+
84128
/// True iff breaking the op-to-op wiring is rejected (the `tensor_memory`
85129
/// component): bump a mid-trace record's first input cell while leaving the prior
86130
/// record's output intact, so the threaded running activation no longer matches.
@@ -130,6 +174,12 @@ impl MutationCampaign for SoundnessCampaign {
130174
MutationOperator::DropConstraint,
131175
"drop the Freivalds accumulator range guard: add p to an accumulator (mod-p aliasing)",
132176
),
177+
mutant(
178+
"range_check.modp_predictor",
179+
"range_check",
180+
MutationOperator::DropConstraint,
181+
"drop the block-path Freivalds range guard: add p to a BatchedLinear accumulator (mod-p aliasing on the predictor path)",
182+
),
133183
mutant(
134184
"tensor_memory.break_wiring",
135185
"tensor_memory",
@@ -166,6 +216,7 @@ impl MutationCampaign for SoundnessCampaign {
166216
fn is_killed(&self, mutant: &Mutant) -> bool {
167217
match mutant.id.as_str() {
168218
"range_check.modp_accumulator" => modp_accumulator_rejected(),
219+
"range_check.modp_predictor" => modp_predictor_batched_rejected(),
169220
"tensor_memory.break_wiring" => wiring_tamper_rejected(),
170221
"requant.tamper_output" => tampered_op_rejected(|r| matches!(r, OpRecord::Requant(_))),
171222
"activation_lookup.tamper_output" => {
@@ -190,8 +241,8 @@ mod tests {
190241
fn soundness_campaign_kills_every_mutant() {
191242
let report = run_campaign(&SoundnessCampaign, &[]);
192243
assert!(
193-
report.total >= 5,
194-
"campaign must cover the soundness checks"
244+
report.total >= 7,
245+
"campaign must cover the soundness checks (incl. the predictor path)"
195246
);
196247
assert!(
197248
report.soundness_critical_survivors().is_empty(),

crates/pwm-verifier/tests/block.rs

Lines changed: 39 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -884,3 +884,42 @@ fn reject_layernorm_out_of_range_shift() {
884884
Err(VerifyError::InvalidShift { op_id: 4 })
885885
));
886886
}
887+
888+
#[test]
889+
fn accept_and_reject_tampered_requant_output() {
890+
// Requant was the one BlockOp variant without a tampered-output reject test
891+
// (#181); with it, all 12 variants reject a bumped claimed output:
892+
// Linear (reject_tampered_block_linear), BatchedLinear
893+
// (reject_tampered_encoder_projection), MatMul/Softmax
894+
// (reject_tampered_attention_scores, reject_tampered_elementwise_op_outputs),
895+
// Activation/LayerNorm/Modulate/Gate (reject_tampered_elementwise_op_outputs),
896+
// Add (reject_tampered_block_residual), Slice/Concat
897+
// (reject_tampered_slice_and_concat), and Requant here.
898+
let block = Block {
899+
input_bufs: vec![0],
900+
ops: vec![BlockOp::Requant {
901+
op_id: 1,
902+
in_buf: 0,
903+
out_buf: 1,
904+
out: vec![],
905+
shift: 1,
906+
zero_point: 0,
907+
clamp_lo: -100,
908+
clamp_hi: 100,
909+
rounding: RND,
910+
}],
911+
output_buf: 1,
912+
};
913+
let inputs = vec![(0u32, vec![10, -7])];
914+
// Hand-computed: 10 >> 1 = 5 exactly; -7/2 = -3.5, floor q = -4 with rem 1
915+
// (= half), and the tie bumps to even: q + (q & 1) = -4.
916+
let proven = prove_block(&block, &[], &[], &inputs).unwrap();
917+
assert_eq!(
918+
verify_block(&proven, &[], &[], &inputs).unwrap(),
919+
vec![5, -4]
920+
);
921+
assert!(matches!(
922+
tamper_op(&block, &[], &[], &inputs, 1),
923+
Err(VerifyError::BlockOpMismatch { op_id: 1 })
924+
));
925+
}

0 commit comments

Comments
 (0)