mirror of
https://github.com/allaunthefox/Research-Stack.git
synced 2026-07-31 03:05:21 +00:00
254 lines
11 KiB
Text
254 lines
11 KiB
Text
/- Copyright (c) 2026 Sovereign Research Stack. All rights reserved.
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
Authors: Research Stack Team
|
|
|
|
CompileBridge.lean — GPU-Accelerated Compilation Bridge Formal Specification
|
|
|
|
This module formalizes the interface between the Lean 4 build system (lake)
|
|
and GPU-accelerated theorem verification. It defines the receipt schema,
|
|
theorem batch descriptors, and verification result types that the Rust
|
|
lake_compile_bridge binary reads and writes.
|
|
|
|
Architecture:
|
|
lake build ──► CompileBridge (Lean) ──► Rust bridge (wgpu) ──► WGSL compute
|
|
▲ │
|
|
└──────────── build_receipt.json ◄───────────────────────┘
|
|
|
|
Per AGENTS.md §1.4: Q16_16 fixed-point for scoring.
|
|
Per AGENTS.md §4: Eval witnesses and theorems required.
|
|
-/
|
|
|
|
namespace Semantics.CompileBridge
|
|
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
-- §1 Theorem Registry
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
|
|
/-- Canonical theorem IDs for GPU-accelerated verification.
|
|
Each ID maps to a theorem in FixedPoint.lean and a verification kernel
|
|
in the WGSL compile_bridge shader. -/
|
|
inductive TheoremID
|
|
| zeroMul -- zero * a = zero
|
|
| mulZero -- a * zero = zero
|
|
| addZero -- a + zero = a
|
|
| zeroAdd -- zero + a = a
|
|
| subSelf -- a - a = zero
|
|
| oneMul -- one * a = a
|
|
| mulOne -- a * one = a
|
|
| addComm -- a + b = b + a
|
|
| negInvolutive -- -(-a) = a
|
|
| subViaNeg -- a - b = a + (-b)
|
|
| q0_2_mulSelfNonneg -- q0_2_mul_self_nonneg (4 cases)
|
|
| q0_2_mulNonneg -- q0_2_mul_nonneg (16 cases)
|
|
| q0_2_addNonneg -- q0_2_add_nonneg (16 cases)
|
|
deriving Repr, DecidableEq, BEq, Inhabited
|
|
|
|
instance : ToString TheoremID where
|
|
toString
|
|
| .zeroMul => "zero_mul"
|
|
| .mulZero => "mul_zero"
|
|
| .addZero => "add_zero"
|
|
| .zeroAdd => "zero_add"
|
|
| .subSelf => "sub_self"
|
|
| .oneMul => "one_mul"
|
|
| .mulOne => "mul_one"
|
|
| .addComm => "add_comm"
|
|
| .negInvolutive => "neg_involutive"
|
|
| .subViaNeg => "sub_via_neg"
|
|
| .q0_2_mulSelfNonneg => "q0_2_mul_self_nonneg"
|
|
| .q0_2_mulNonneg => "q0_2_mul_nonneg"
|
|
| .q0_2_addNonneg => "q0_2_add_nonneg"
|
|
|
|
namespace TheoremID
|
|
|
|
/-- Map theorem ID to its WGSL shader kernel name. -/
|
|
def toKernelName : TheoremID → String
|
|
| .zeroMul => "check_zero_mul"
|
|
| .mulZero => "check_mul_zero"
|
|
| .addZero => "check_add_zero"
|
|
| .zeroAdd => "check_zero_add"
|
|
| .subSelf => "check_sub_self"
|
|
| .oneMul => "check_one_mul"
|
|
| .mulOne => "check_mul_one"
|
|
| .addComm => "check_add_comm"
|
|
| .negInvolutive => "check_neg_involutive"
|
|
| .subViaNeg => "check_sub_via_neg"
|
|
| .q0_2_mulSelfNonneg => "check_q0_2_mul_self_nonneg"
|
|
| .q0_2_mulNonneg => "check_q0_2_mul_nonneg"
|
|
| .q0_2_addNonneg => "check_q0_2_add_nonneg"
|
|
|
|
/-- Map theorem ID to numeric dispatch index (matches WGSL switch). -/
|
|
def toDispatchIndex : TheoremID → Nat
|
|
| .zeroMul => 0
|
|
| .mulZero => 1
|
|
| .addZero => 2
|
|
| .zeroAdd => 3
|
|
| .subSelf => 4
|
|
| .oneMul => 5
|
|
| .mulOne => 6
|
|
| .addComm => 7
|
|
| .negInvolutive => 8
|
|
| .subViaNeg => 9
|
|
| .q0_2_mulSelfNonneg => 10
|
|
| .q0_2_mulNonneg => 11
|
|
| .q0_2_addNonneg => 12
|
|
|
|
/-- Number of GPU-verifiable theorems. -/
|
|
def count : Nat := 13
|
|
|
|
end TheoremID
|
|
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
-- §2 GPU Verification Batch
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
|
|
/-- A single test vector for Q16_16 theorem verification. -/
|
|
structure TestVector where
|
|
a : UInt32 -- First Q16_16 operand
|
|
b : UInt32 -- Second Q16_16 operand
|
|
expected : UInt32 -- Expected result (0 for property-based checks)
|
|
deriving Repr, BEq, Inhabited
|
|
|
|
/-- Descriptor for a GPU theorem verification batch. -/
|
|
structure TheoremBatch where
|
|
theoremId : UInt32 -- Dispatch index from TheoremID.toDispatchIndex
|
|
count : UInt32 -- Number of test vectors
|
|
deriving Repr, BEq, Inhabited
|
|
|
|
/-- Result of GPU theorem verification. -/
|
|
structure TheoremResult where
|
|
theoremId : UInt32 -- Matching dispatch index
|
|
passed : Bool -- True if all test vectors passed
|
|
total : UInt32 -- Total test vectors checked
|
|
failed : UInt32 -- Number of test vectors that failed
|
|
deriving Repr, BEq, Inhabited
|
|
|
|
/-- Complete GPU verification receipt. -/
|
|
structure VerificationReceipt where
|
|
schema : String -- "lake_compile_bridge_receipt_v1"
|
|
version : String -- "0.1.0"
|
|
target : String -- Lake build target (e.g., "Semantics.FixedPoint")
|
|
jobs : UInt32 -- Parallel jobs used for lake build
|
|
vectorsPerTheorem : UInt32 -- Test vectors per theorem
|
|
gpuAvailable : Bool -- Whether GPU was available
|
|
gpuDevice : String -- GPU device name
|
|
theorems : List TheoremResult -- Per-theorem results
|
|
totalTheorems : Nat -- Total theorems checked
|
|
passed : Nat -- Theorems passing
|
|
failed : Nat -- Theorems failing
|
|
buildExitCode : Int -- lake build exit code
|
|
elapsedMs : Nat -- Total elapsed time in milliseconds
|
|
timestampUtc : String -- ISO 8601 timestamp
|
|
deriving Repr, Inhabited
|
|
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
-- §3 Bridge Invariants
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
|
|
/-- Invariant: theorem IDs in result match canonical registry. -/
|
|
def resultIdsValid (receipt : VerificationReceipt) : Bool :=
|
|
receipt.theorems.all (fun r =>
|
|
r.theoremId.toNat < TheoremID.count)
|
|
|
|
/-- Invariant: if passed then failed = 0, else failed = total. -/
|
|
def resultCountsValid (receipt : VerificationReceipt) : Bool :=
|
|
receipt.theorems.all (fun r =>
|
|
if r.passed then r.failed = 0 else r.failed = r.total)
|
|
|
|
/-- Invariant: totalTheorems = |theorems|. -/
|
|
def totalCountMatches (receipt : VerificationReceipt) : Bool :=
|
|
receipt.totalTheorems = receipt.theorems.length
|
|
|
|
/-- All bridge invariants hold simultaneously. -/
|
|
def invariantsHold (receipt : VerificationReceipt) : Bool :=
|
|
resultIdsValid receipt &&
|
|
resultCountsValid receipt &&
|
|
totalCountMatches receipt
|
|
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
-- §4 Lean-side Theorem Verification Wrapper
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
|
|
/--
|
|
Promote a GPU-verified theorem result into the Lean formal theory.
|
|
|
|
This is the receiving end of the bridge. The Rust binary writes a receipt,
|
|
and this function reads it, checks invariants, and returns a VerifiedClaim
|
|
that can be used in proofs.
|
|
-/
|
|
structure VerifiedClaim where
|
|
theoremId : TheoremID
|
|
gpuReceipt : TheoremResult
|
|
leanTheorem : String -- Name of the Lean theorem this verifies
|
|
deriving Repr, Inhabited
|
|
|
|
/--
|
|
GPU results are an *accelerator* for native_decide, not a replacement.
|
|
The Lean-side theorem remains the authoritative proof. GPU verification
|
|
provides a fast, parallel cross-check that catches regressions early.
|
|
-/
|
|
def promoteToClaim (receipt : VerificationReceipt) (idx : Nat) : Option VerifiedClaim :=
|
|
if h : idx < receipt.theorems.length then
|
|
let res := receipt.theorems.get ⟨idx, h⟩
|
|
let theoremId : TheoremID :=
|
|
match res.theoremId with
|
|
| 0 => TheoremID.zeroMul
|
|
| 1 => TheoremID.mulZero
|
|
| 2 => TheoremID.addZero
|
|
| 3 => TheoremID.zeroAdd
|
|
| 4 => TheoremID.subSelf
|
|
| 5 => TheoremID.oneMul
|
|
| 6 => TheoremID.mulOne
|
|
| 7 => TheoremID.addComm
|
|
| 8 => TheoremID.negInvolutive
|
|
| 9 => TheoremID.subViaNeg
|
|
| 10 => TheoremID.q0_2_mulSelfNonneg
|
|
| 11 => TheoremID.q0_2_mulNonneg
|
|
| 12 => TheoremID.q0_2_addNonneg
|
|
| _ => TheoremID.zeroMul
|
|
some {
|
|
theoremId := theoremId
|
|
gpuReceipt := res
|
|
leanTheorem := toString theoremId
|
|
}
|
|
else
|
|
none
|
|
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
-- §5 Eval Witnesses
|
|
-- ═══════════════════════════════════════════════════════════════════════════
|
|
|
|
/-- Empty receipt for invariant check (trivially valid). -/
|
|
def emptyReceipt : VerificationReceipt :=
|
|
{ schema := "lake_compile_bridge_receipt_v1"
|
|
version := "0.1.0"
|
|
target := ""
|
|
jobs := 0
|
|
vectorsPerTheorem := 0
|
|
gpuAvailable := false
|
|
gpuDevice := ""
|
|
theorems := []
|
|
totalTheorems := 0
|
|
passed := 0
|
|
failed := 0
|
|
buildExitCode := 0
|
|
elapsedMs := 0
|
|
timestampUtc := "" }
|
|
|
|
#eval invariantsHold emptyReceipt
|
|
|
|
#eval List.map TheoremID.toDispatchIndex
|
|
[TheoremID.zeroMul, TheoremID.mulZero, TheoremID.addZero, TheoremID.zeroAdd,
|
|
TheoremID.subSelf, TheoremID.oneMul, TheoremID.mulOne, TheoremID.addComm,
|
|
TheoremID.negInvolutive, TheoremID.subViaNeg,
|
|
TheoremID.q0_2_mulSelfNonneg, TheoremID.q0_2_mulNonneg, TheoremID.q0_2_addNonneg]
|
|
-- Expected: [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12]
|
|
|
|
#eval (List.map TheoremID.toDispatchIndex
|
|
[TheoremID.zeroMul, TheoremID.mulZero, TheoremID.addZero, TheoremID.zeroAdd,
|
|
TheoremID.subSelf, TheoremID.oneMul, TheoremID.mulOne, TheoremID.addComm,
|
|
TheoremID.negInvolutive, TheoremID.subViaNeg,
|
|
TheoremID.q0_2_mulSelfNonneg, TheoremID.q0_2_mulNonneg, TheoremID.q0_2_addNonneg]).all (fun idx => idx < TheoremID.count)
|
|
-- Expected: true
|
|
|
|
end Semantics.CompileBridge
|