mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-07-31 01:25:21 +00:00
allaun
fec200205e
Ports three Research Stack RRC gates into formal/SilverSight/RRC/ using the existing CoreFormalism braid and Q16_16 surfaces. Adds a Lean ↔ C ↔ Python Q16_16 roundtrip test: - c/q16_canonical.c: canonical saturating Q16_16 C library - exe/Q16_16Roundtrip.lean: Lake extern_lib linked executable - tests/test_q16_roundtrip.py: Python ↔ C harness (revived from quarantine) Updates lakefile.lean with q16-roundtrip executable and extern_lib q16_canonical. Build: lake build SilverSightRRC 3006 jobs, 0 errors; q16-roundtrip 5949 jobs, 0 errors
105 lines
3.7 KiB
Text
105 lines
3.7 KiB
Text
import SilverSight.FixedPoint
|
||
|
||
open SilverSight.FixedPoint
|
||
open SilverSight.FixedPoint.Q16_16
|
||
|
||
-- C functions linked through extern_lib q16_canonical.
|
||
@[extern "q16_to_float"] opaque cQ16ToFloat (q : UInt32) : Float
|
||
@[extern "float_to_q16_nearbyint"] opaque cFloatToQ16 (f : Float) : UInt32
|
||
@[extern "q16_add"] opaque cQ16Add (a b : UInt32) : UInt32
|
||
@[extern "q16_sub"] opaque cQ16Sub (a b : UInt32) : UInt32
|
||
|
||
private def q16ToBits (q : Q16_16) : UInt32 := Q16_16.toBits q
|
||
private def bitsToQ16 (u : UInt32) : Q16_16 := Q16_16.ofBits u
|
||
|
||
private def floatEq (a b : Float) (ε : Float := 1e-9) : Bool :=
|
||
let d := a - b
|
||
d < ε && d > -ε
|
||
|
||
private def intCases : List Int :=
|
||
[ 0, 1, 32768, 65536, 19661, -65536,
|
||
-2147483648, 2147483647,
|
||
-1000000, 1000000 ]
|
||
|
||
-- Values chosen so that floor and round-to-nearest-even agree at Q16.16 scale,
|
||
-- keeping Lean's floor-based `ofFloat` consistent with C's `nearbyint`.
|
||
private def floatCases : List Float :=
|
||
[ 0.0, -0.0, 0.5, 1.0, -1.0, 2.5, -2.5,
|
||
32767.5, -32768.0, 1e12, -1e12 ]
|
||
|
||
private def addCases : List (Int × Int) :=
|
||
[ (0, 0), (1, 1), (32768, 32768), (65536, 65536),
|
||
(2147483647, 1), (-2147483648, -1), (-65536, 65536),
|
||
(1000000, 2000000) ]
|
||
|
||
private def subCases : List (Int × Int) :=
|
||
[ (0, 0), (1, 0), (0, 1), (2147483647, -1),
|
||
(-2147483648, 1), (65536, -65536) ]
|
||
|
||
private structure TestCase where
|
||
name : String
|
||
passed : Bool
|
||
detail : String
|
||
deriving Repr
|
||
|
||
private def runToFloatTests : List TestCase :=
|
||
intCases.map fun raw =>
|
||
let q := Q16_16.ofRawInt raw
|
||
let cVal := cQ16ToFloat (q16ToBits q)
|
||
let leanVal := q.toFloat
|
||
let ok := floatEq cVal leanVal
|
||
{ name := s!"to_float {raw}", passed := ok,
|
||
detail := s!"C={cVal} Lean={leanVal}" }
|
||
|
||
private def runFromFloatTests : List TestCase :=
|
||
floatCases.map fun f =>
|
||
let leanRaw := (Q16_16.ofFloat f).toInt
|
||
let cRaw := (bitsToQ16 (cFloatToQ16 f)).toInt
|
||
let ok := leanRaw == cRaw
|
||
{ name := s!"from_float {f}", passed := ok,
|
||
detail := s!"C={cRaw} Lean={leanRaw}" }
|
||
|
||
private def runAddTests : List TestCase :=
|
||
addCases.map fun (aRaw, bRaw) =>
|
||
let a := Q16_16.ofRawInt aRaw
|
||
let b := Q16_16.ofRawInt bRaw
|
||
let leanRaw := (Q16_16.add a b).toInt
|
||
let cRaw := (bitsToQ16 (cQ16Add (q16ToBits a) (q16ToBits b))).toInt
|
||
let ok := leanRaw == cRaw
|
||
{ name := s!"add {aRaw} {bRaw}", passed := ok,
|
||
detail := s!"C={cRaw} Lean={leanRaw}" }
|
||
|
||
private def runSubTests : List TestCase :=
|
||
subCases.map fun (aRaw, bRaw) =>
|
||
let a := Q16_16.ofRawInt aRaw
|
||
let b := Q16_16.ofRawInt bRaw
|
||
let leanRaw := (Q16_16.sub a b).toInt
|
||
let cRaw := (bitsToQ16 (cQ16Sub (q16ToBits a) (q16ToBits b))).toInt
|
||
let ok := leanRaw == cRaw
|
||
{ name := s!"sub {aRaw} {bRaw}", passed := ok,
|
||
detail := s!"C={cRaw} Lean={leanRaw}" }
|
||
|
||
private def jBool (b : Bool) : String := if b then "true" else "false"
|
||
|
||
private def jStr (s : String) : String :=
|
||
"\"" ++ (s.replace "\\" "\\\\" |>.replace "\"" "\\\"") ++ "\""
|
||
|
||
private def jCase (t : TestCase) : String :=
|
||
s!"\{\"name\":{jStr t.name},\"passed\":{jBool t.passed},\"detail\":{jStr t.detail}}"
|
||
|
||
private def jCases (cs : List TestCase) : String :=
|
||
"[" ++ String.intercalate "," (cs.map jCase) ++ "]"
|
||
|
||
def main : IO UInt32 := do
|
||
let tests := runToFloatTests ++ runFromFloatTests ++ runAddTests ++ runSubTests
|
||
let passed := tests.filter (·.passed)
|
||
let failed := tests.filter (!·.passed)
|
||
let ok := failed.isEmpty
|
||
IO.println <|
|
||
s!"\{\"schema\":\"q16_16_lean_c_roundtrip_v1\"," ++
|
||
s!"\"ok\":{jBool ok}," ++
|
||
s!"\"total\":{tests.length}," ++
|
||
s!"\"passed\":{passed.length}," ++
|
||
s!"\"failed\":{failed.length}," ++
|
||
s!"\"tests\":{jCases tests}}"
|
||
return if ok then 0 else 1
|