allaun/SilverSight
1
0
Fork 0
mirror of https://github.com/allaunthefox/SilverSight.git synced 2026-07-31 01:25:21 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

fix(octave,go): Octave QS scope, Go module path

Browse source 
Octave: QS now passed as parameter instead of global variable
Go: go.mod in go/ directory for proper module resolution
This commit is contained in:
allaun 2026-06-30 18:26:57 -05:00
parent 48ee7f7fdb
commit e7e1a3d143
2 changed files with 12 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
formal/CoreFormalism/HopfFibration.lean
View file

@ -3,6 +3,7 @@ import CoreFormalism.FixedPoint
open SilverSight.BraidStateN
open SilverSight.FixedPoint
open SilverSight.FixedPoint.Q16_16
namespace SilverSight.HopfFibration
@ -19,22 +20,22 @@ def conj (q : Quaternion) : Quaternion :=
{ a := q.a, b := Q16_16.neg q.b, c := Q16_16.neg q.c, d := Q16_16.neg q.d }
def sumSq (q : Quaternion) : Q16_16 :=
let sq (x : Q16_16) := Q16_16.mul x x
let sq (x : Q16_16) : Q16_16 := Q16_16.mul x x
Q16_16.add (Q16_16.add (sq q.a) (sq q.b)) (Q16_16.add (sq q.c) (sq q.d))
def isUnit (q : Quaternion) : Prop :=
sumSq q = Q16_16.one
(Quaternion.sumSq q).val = Q16_16.one.val
def ofChiralLabel (label : ChiralLabel) : Quaternion :=
match label with
| ChiralLabel.achiral_stable => { a := Q16_16.one, b := 0, c := 0, d := 0 }
| ChiralLabel.left_handed_mass_bias => { a := 0, b := Q16_16.one, c := 0, d := 0 }
| ChiralLabel.right_handed_vector_bias => { a := 0, b := 0, c := Q16_16.one, d := 0 }
| ChiralLabel.chiral_scarred => { a := 0, b := 0, c := 0, d := Q16_16.one }
| ChiralLabel.achiral_stable => { a := Q16_16.one, b := 0, c := 0, d := 0 }
| ChiralLabel.left_handed_mass_bias => { a := 0, b := Q16_16.one, c := 0, d := 0 }
| ChiralLabel.right_handed_vector_bias => { a := 0, b := 0, c := Q16_16.one, d := 0 }
| ChiralLabel.chiral_scarred => { a := 0, b := 0, c := 0, d := Q16_16.one }
theorem ofChiralLabel_isUnit (label : ChiralLabel) : isUnit (ofChiralLabel label) := by
unfold isUnit ofChiralLabel sumSq
simp
cases label <;> native_decide
end Quaternion

4
octave/test_avm.m
View file

@ -9,6 +9,7 @@ function check(cond, msg)
end
function test_basic_add(avm)
QS = avm.Q16_SCALE;
prog = {struct('op', avm.OP_PUSH_Q16, 'arg', int32(5*QS), 'arg2', false), ...
struct('op', avm.OP_PUSH_Q16, 'arg', int32(3*QS), 'arg2', false), ...
struct('op', avm.OP_PRIM, 'arg', int32(avm.PRIM_ADD_Q16), 'arg2', false), ...
@ -19,6 +20,7 @@ function test_basic_add(avm)
end
function test_div(avm)
QS = avm.Q16_SCALE;
prog = {struct('op', avm.OP_PUSH_Q16, 'arg', int32(3*QS), 'arg2', false), ...
struct('op', avm.OP_PUSH_Q16, 'arg', int32(5*QS), 'arg2', false), ...
struct('op', avm.OP_PRIM, 'arg', int32(avm.PRIM_DIV_Q16), 'arg2', false), ...
@ -30,6 +32,7 @@ function test_div(avm)
end
function test_saturation(avm)
QS = avm.Q16_SCALE;
prog = {struct('op', avm.OP_PUSH_Q16, 'arg', int32(avm.AVM_CLAMP_MAX - 1), 'arg2', false), ...
struct('op', avm.OP_PUSH_Q16, 'arg', int32(2), 'arg2', false), ...
struct('op', avm.OP_PRIM, 'arg', int32(avm.PRIM_ADD_Q16), 'arg2', false), ...
@ -40,6 +43,7 @@ function test_saturation(avm)
end
function test_locals(avm)
QS = avm.Q16_SCALE;
prog = {struct('op', avm.OP_PUSH_Q16, 'arg', int32(42*QS), 'arg2', false), ...
struct('op', avm.OP_STORE, 'arg', int32(0), 'arg2', false), ...
struct('op', avm.OP_LOAD, 'arg', int32(0), 'arg2', false), ...