mirror of
https://github.com/allaunthefox/Research-Stack.git
synced 2026-07-31 03:05:21 +00:00
allaun
475f6319ea
This squashes all local history (768 commits) onto the scrubbed PR #90 baseline. Individual commits were lost during filter-repo corruption; the working tree content is preserved intact. Build: N/A (working tree state only)
61 lines
1.9 KiB
WebGPU Shading Language
61 lines
1.9 KiB
WebGPU Shading Language
// Q16_16 Comparison Monotonicity Verification Shader
|
|
//
|
|
// Depends on: q16_arithmetic.wgsl (shared include)
|
|
//
|
|
// This shader verifies monotonicity lemmas for Q16_16 comparisons:
|
|
// 1. val_ge_implies_toInt_ge: a.val >= b.val → a.toInt >= b.toInt
|
|
// 2. val_le_implies_toInt_le: a.val <= b.val → a.toInt <= b.toInt
|
|
//
|
|
// Tests all pairs of Q16_16 values (65,536² = 4.3 billion pairs) in parallel.
|
|
// Uses 2D grid to iterate over (a, b) pairs efficiently.
|
|
|
|
struct ComparisonResult {
|
|
val_ge_toInt_ge_ok: u32,
|
|
val_le_toInt_le_ok: u32,
|
|
counterexamples_found: u32,
|
|
}
|
|
|
|
@group(0) @binding(0) var<storage, read_write> results: array<ComparisonResult>;
|
|
|
|
const Q16_SPACE: u32 = 65536u;
|
|
|
|
@compute @workgroup_size(8, 8, 1)
|
|
fn main(@builtin(global_invocation_id) gid: vec3<u32>) {
|
|
let a = gid.x;
|
|
let b = gid.y;
|
|
|
|
if (a >= Q16_SPACE || b >= Q16_SPACE) {
|
|
return;
|
|
}
|
|
|
|
// Lemma 1: val_ge_implies_toInt_ge
|
|
// If a.val >= b.val, then a.toInt >= b.toInt
|
|
let val_ge = a >= b;
|
|
let a_int = q16_to_int(a);
|
|
let b_int = q16_to_int(b);
|
|
let toInt_ge = a_int >= b_int;
|
|
|
|
// The implication: val_ge → toInt_ge
|
|
// This is false only when val_ge is true but toInt_ge is false
|
|
let val_ge_toInt_ge_ok = select(1u, 0u, !(val_ge && !toInt_ge));
|
|
|
|
// Lemma 2: val_le_implies_toInt_le
|
|
// If a.val <= b.val, then a.toInt <= b.toInt
|
|
let val_le = a <= b;
|
|
let toInt_le = a_int <= b_int;
|
|
|
|
// The implication: val_le → toInt_le
|
|
// This is false only when val_le is true but toInt_le is false
|
|
let val_le_toInt_le_ok = select(1u, 0u, !(val_le && !toInt_le));
|
|
|
|
// Track counterexamples
|
|
let counterexamples = select(0u, 1u, !val_ge_toInt_ge_ok || !val_le_toInt_le_ok);
|
|
|
|
// Store result (use linear index)
|
|
let idx = a * Q16_SPACE + b;
|
|
results[idx] = ComparisonResult(
|
|
val_ge_toInt_ge_ok,
|
|
val_le_toInt_le_ok,
|
|
counterexamples
|
|
);
|
|
}
|