mirror of
https://github.com/allaunthefox/Research-Stack.git
synced 2026-07-31 03:05:21 +00:00
86 lines
2.4 KiB
WebGPU Shading Language
86 lines
2.4 KiB
WebGPU Shading Language
// Q16_16 Min/Max Theorems Verification Shader
|
|
//
|
|
// This shader verifies the min/max comparison theorems from FixedPoint.lean:
|
|
// 1. max_first_whenGe: a.toInt >= b.toInt → max a b = a
|
|
// 2. max_second_whenLt: a.toInt < b.toInt → max a b = b
|
|
// 3. min_first_whenLe: a.toInt <= b.toInt → min a b = a
|
|
// 4. min_second_whenGt: a.toInt > b.toInt → min a b = b
|
|
//
|
|
// Tests all pairs of Q16_16 values in parallel on GPU.
|
|
|
|
struct MinMaxResult {
|
|
max_first_ok: u32,
|
|
max_second_ok: u32,
|
|
min_first_ok: u32,
|
|
min_second_ok: u32,
|
|
}
|
|
|
|
@group(0) @binding(0) var<storage, read_write> results: array<MinMaxResult>;
|
|
|
|
const Q16_SPACE: u32 = 65536u;
|
|
const SIGN_BIT: u32 = 0x80000000u;
|
|
const TWO_POW_32: u32 = 0x100000000u;
|
|
|
|
// Convert Q16_16 val to signed Int (2's complement)
|
|
fn toInt(val: u32) -> i32 {
|
|
let is_negative = val >= SIGN_BIT;
|
|
return select(i32(val), i32(val) - i32(TWO_POW_32), is_negative);
|
|
}
|
|
|
|
// Q16_16 max (as defined in FixedPoint.lean)
|
|
fn q_max(a: u32, b: u32) -> u32 {
|
|
let a_int = toInt(a);
|
|
let b_int = toInt(b);
|
|
return select(a, b, a_int >= b_int);
|
|
}
|
|
|
|
// Q16_16 min (as defined in FixedPoint.lean)
|
|
fn q_min(a: u32, b: u32) -> u32 {
|
|
let a_int = toInt(a);
|
|
let b_int = toInt(b);
|
|
return select(a, b, a_int <= b_int);
|
|
}
|
|
|
|
@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;
|
|
}
|
|
|
|
let a_int = toInt(a);
|
|
let b_int = toInt(b);
|
|
let max_ab = q_max(a, b);
|
|
let min_ab = q_min(a, b);
|
|
|
|
// Lemma 1: max_first_whenGe
|
|
// a.toInt >= b.toInt → max a b = a
|
|
let a_ge_b = a_int >= b_int;
|
|
let max_first_ok = select(1u, 0u, !a_ge_b || max_ab == a);
|
|
|
|
// Lemma 2: max_second_whenLt
|
|
// a.toInt < b.toInt → max a b = b
|
|
let a_lt_b = a_int < b_int;
|
|
let max_second_ok = select(1u, 0u, !a_lt_b || max_ab == b);
|
|
|
|
// Lemma 3: min_first_whenLe
|
|
// a.toInt <= b.toInt → min a b = a
|
|
let a_le_b = a_int <= b_int;
|
|
let min_first_ok = select(1u, 0u, !a_le_b || min_ab == a);
|
|
|
|
// Lemma 4: min_second_whenGt
|
|
// a.toInt > b.toInt → min a b = b
|
|
let a_gt_b = a_int > b_int;
|
|
let min_second_ok = select(1u, 0u, !a_gt_b || min_ab == b);
|
|
|
|
// Store result (use linear index)
|
|
let idx = a * Q16_SPACE + b;
|
|
results[idx] = MinMaxResult(
|
|
max_first_ok,
|
|
max_second_ok,
|
|
min_first_ok,
|
|
min_second_ok
|
|
);
|
|
}
|