mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-07-30 17:16:16 +00:00
python/cartan_dna_bridge.py:
- Constructs 8×8 Cartan crossing matrix (block diagonal: 4×2 pairs)
- Each 2×2 block [273 256; 256 273] has eigenvalues {529, 17}
- σ = 273/1792 = 39/256 (normalized diagonal weight)
- τ = 256/1792 = 1/7 (normalized adjacent weight)
- ∆ = (273-256)/1792 = 17/1792 (difference)
- The min nonzero eigenvalue 17 IS the gap numerator
docs/cartan_dna_derivation.md:
- Step-by-step spec for modifying dna_codec.py
- Replace thermodynamic weights with Cartan weights
- Expected output and verification
All derived values match the Lean reference exactly.
The DNA encoder can now witness the spectral gap chain.
198 lines
7.9 KiB
Fortran
198 lines
7.9 KiB
Fortran
! AVM ISA v1 — Fortran Port (Strict Functional Execution)
|
|
module avm
|
|
implicit none
|
|
|
|
! ── Constants ──────────────────────────────────────────────
|
|
integer, parameter :: AVM_CLAMP_MIN = -2147483647
|
|
integer, parameter :: AVM_CLAMP_MAX = 2147483647
|
|
integer, parameter :: AVM_Q0_MIN = -32767
|
|
integer, parameter :: AVM_Q0_MAX = 32767
|
|
integer, parameter :: Q16_SCALE = 65536
|
|
integer, parameter :: AVM_MAX_STACK = 1024
|
|
integer, parameter :: AVM_MAX_LOCALS = 256
|
|
|
|
! ── Types ──────────────────────────────────────────────────
|
|
integer, parameter :: TY_Q0 = 0, TY_Q16 = 1, TY_BOOL = 2
|
|
|
|
type :: AnyVal
|
|
integer :: ty = TY_Q0
|
|
integer :: i = 0
|
|
logical :: b = .false.
|
|
end type AnyVal
|
|
|
|
! ── Instruction encoding ───────────────────────────────────
|
|
integer, parameter :: OP_PUSH_Q16 = 0, OP_PUSH_BOOL = 1, OP_PUSH_Q0 = 2
|
|
integer, parameter :: OP_POP = 3, OP_DUP = 4, OP_SWAP = 5
|
|
integer, parameter :: OP_LOAD = 6, OP_STORE = 7
|
|
integer, parameter :: OP_JUMP = 8, OP_JUMP_IF = 9, OP_PRIM = 10, OP_HALT = 11
|
|
|
|
integer, parameter :: PRIM_ADD_Q0 = 0, PRIM_SUB_Q0 = 1
|
|
integer, parameter :: PRIM_ADD_Q16 = 2, PRIM_SUB_Q16 = 3
|
|
integer, parameter :: PRIM_MUL_Q16 = 4, PRIM_DIV_Q16 = 5
|
|
integer, parameter :: PRIM_LT_Q16 = 6, PRIM_EQ_Q16 = 7
|
|
integer, parameter :: PRIM_AND = 8, PRIM_OR = 9, PRIM_NOT = 10
|
|
|
|
type :: Instr
|
|
integer :: op = OP_HALT
|
|
integer :: arg = 0
|
|
logical :: arg2 = .false.
|
|
end type Instr
|
|
|
|
type :: State
|
|
integer :: pc = 0
|
|
type(AnyVal) :: stack(AVM_MAX_STACK)
|
|
integer :: sp = 0
|
|
type(AnyVal) :: locals(AVM_MAX_LOCALS)
|
|
logical :: local_set(AVM_MAX_LOCALS) = .false.
|
|
logical :: halted = .false.
|
|
end type State
|
|
|
|
contains
|
|
|
|
! ── Helpers ────────────────────────────────────────────────
|
|
function avm_clamp(x) result(r)
|
|
integer(kind=8), intent(in) :: x
|
|
integer :: r
|
|
if (x > AVM_CLAMP_MAX) then; r = AVM_CLAMP_MAX
|
|
else if (x < AVM_CLAMP_MIN) then; r = AVM_CLAMP_MIN
|
|
else; r = int(x); end if
|
|
end function avm_clamp
|
|
|
|
function avm_q0_clamp(x) result(r)
|
|
integer(kind=8), intent(in) :: x
|
|
integer :: r
|
|
if (x > AVM_Q0_MAX) then; r = AVM_Q0_MAX
|
|
else if (x < AVM_Q0_MIN) then; r = AVM_Q0_MIN
|
|
else; r = int(x); end if
|
|
end function avm_q0_clamp
|
|
|
|
function floor_div(a, b) result(r)
|
|
integer(kind=8), intent(in) :: a, b
|
|
integer :: r
|
|
integer(kind=8) :: q
|
|
q = a / b
|
|
if (mod(a, b) /= 0 .and. ieor(a, b) < 0) q = q - 1
|
|
r = int(q)
|
|
end function floor_div
|
|
|
|
function lt_q16_v6(a, b) result(r)
|
|
integer, intent(in) :: a, b
|
|
logical :: r
|
|
logical :: sa, sb
|
|
sa = a < 0; sb = b < 0
|
|
if (sa .neqv. sb) then; r = sa; else; r = a < b; end if
|
|
end function lt_q16_v6
|
|
|
|
! ── Primitive execution ────────────────────────────────────
|
|
function eval_prim(p, a, b) result(r)
|
|
integer, intent(in) :: p
|
|
type(AnyVal), intent(in) :: a, b
|
|
type(AnyVal) :: r
|
|
r%ty = TY_Q0; r%i = 0; r%b = .false.
|
|
|
|
if (p == PRIM_ADD_Q0) then
|
|
if (a%ty /= TY_Q0 .or. b%ty /= TY_Q0) return
|
|
r%ty = TY_Q0; r%i = avm_q0_clamp(int(a%i, 8) + int(b%i, 8))
|
|
else if (p == PRIM_SUB_Q0) then
|
|
if (a%ty /= TY_Q0 .or. b%ty /= TY_Q0) return
|
|
r%ty = TY_Q0; r%i = avm_q0_clamp(int(a%i, 8) - int(b%i, 8))
|
|
else if (p == PRIM_ADD_Q16) then
|
|
if (a%ty /= TY_Q16 .or. b%ty /= TY_Q16) return
|
|
r%ty = TY_Q16; r%i = avm_clamp(int(a%i, 8) + int(b%i, 8))
|
|
else if (p == PRIM_SUB_Q16) then
|
|
if (a%ty /= TY_Q16 .or. b%ty /= TY_Q16) return
|
|
r%ty = TY_Q16; r%i = avm_clamp(int(a%i, 8) - int(b%i, 8))
|
|
else if (p == PRIM_MUL_Q16) then
|
|
if (a%ty /= TY_Q16 .or. b%ty /= TY_Q16) return
|
|
r%ty = TY_Q16; r%i = avm_clamp(int(floor_div(int(a%i,8)*int(b%i,8), int(Q16_SCALE,8)), 8))
|
|
else if (p == PRIM_DIV_Q16) then
|
|
if (a%ty /= TY_Q16 .or. b%ty /= TY_Q16 .or. b%i == 0) return
|
|
r%ty = TY_Q16; r%i = avm_clamp(int(floor_div(int(a%i,8)*Q16_SCALE, int(b%i,8)), 8))
|
|
else if (p == PRIM_LT_Q16) then
|
|
if (a%ty /= TY_Q16 .or. b%ty /= TY_Q16) return
|
|
r%ty = TY_BOOL; r%b = lt_q16_v6(a%i, b%i)
|
|
else if (p == PRIM_EQ_Q16) then
|
|
if (a%ty /= TY_Q16 .or. b%ty /= TY_Q16) return
|
|
r%ty = TY_BOOL; r%b = (a%i == b%i)
|
|
else if (p == PRIM_AND) then
|
|
if (a%ty /= TY_BOOL .or. b%ty /= TY_BOOL) return
|
|
r%ty = TY_BOOL; r%b = a%b .and. b%b
|
|
else if (p == PRIM_OR) then
|
|
if (a%ty /= TY_BOOL .or. b%ty /= TY_BOOL) return
|
|
r%ty = TY_BOOL; r%b = a%b .or. b%b
|
|
else if (p == PRIM_NOT) then
|
|
if (a%ty /= TY_BOOL) return
|
|
r%ty = TY_BOOL; r%b = .not. a%b
|
|
end if
|
|
end function eval_prim
|
|
|
|
! ── Step ──────────────────────────────────────────────────
|
|
function step(s, prog, prog_len) result(err)
|
|
type(State), intent(inout) :: s
|
|
type(Instr), intent(in) :: prog(*)
|
|
integer, intent(in) :: prog_len
|
|
integer :: err, npc, arity
|
|
type(AnyVal) :: a, b, res
|
|
type(Instr) :: cur
|
|
|
|
err = 0
|
|
if (s%halted) then; err = -1; return; end if
|
|
if (s%pc < 0 .or. s%pc >= prog_len) then; s%halted = .true.; return; end if
|
|
|
|
cur = prog(s%pc + 1)
|
|
npc = s%pc + 1
|
|
|
|
! Stack depth check
|
|
if (cur%op <= OP_PUSH_Q0 .or. cur%op == OP_DUP .or. cur%op == OP_LOAD) then
|
|
if (s%sp >= AVM_MAX_STACK) then; err = -2; return; end if
|
|
end if
|
|
|
|
if (cur%op == OP_PUSH_Q16) then
|
|
s%sp = s%sp + 1; s%stack(s%sp)%ty = TY_Q16; s%stack(s%sp)%i = avm_clamp(int(cur%arg, 8))
|
|
else if (cur%op == OP_PUSH_BOOL) then
|
|
s%sp = s%sp + 1; s%stack(s%sp)%ty = TY_BOOL; s%stack(s%sp)%b = cur%arg2
|
|
else if (cur%op == OP_PUSH_Q0) then
|
|
s%sp = s%sp + 1; s%stack(s%sp)%ty = TY_Q0; s%stack(s%sp)%i = avm_q0_clamp(int(cur%arg, 8))
|
|
else if (cur%op == OP_POP) then
|
|
if (s%sp <= 0) then; err = -3; return; end if; s%sp = s%sp - 1
|
|
else if (cur%op == OP_DUP) then
|
|
if (s%sp <= 0) then; err = -3; return; end if
|
|
s%sp = s%sp + 1; s%stack(s%sp) = s%stack(s%sp - 1)
|
|
else if (cur%op == OP_SWAP) then
|
|
if (s%sp < 2) then; err = -4; return; end if
|
|
a = s%stack(s%sp); s%stack(s%sp) = s%stack(s%sp-1); s%stack(s%sp-1) = a
|
|
else if (cur%op == OP_LOAD) then
|
|
if (cur%arg < 0 .or. cur%arg >= AVM_MAX_LOCALS .or. .not. s%local_set(cur%arg+1)) then
|
|
err = -5; return
|
|
end if
|
|
s%sp = s%sp + 1; s%stack(s%sp) = s%locals(cur%arg+1)
|
|
else if (cur%op == OP_STORE) then
|
|
if (s%sp <= 0) then; err = -3; return; end if
|
|
if (cur%arg < 0 .or. cur%arg >= AVM_MAX_LOCALS) then; err = -5; return; end if
|
|
s%locals(cur%arg+1) = s%stack(s%sp); s%local_set(cur%arg+1) = .true.
|
|
s%sp = s%sp - 1
|
|
else if (cur%op == OP_JUMP) then
|
|
if (cur%arg < 0 .or. cur%arg >= prog_len) then; err = -6; return; end if
|
|
npc = cur%arg
|
|
else if (cur%op == OP_JUMP_IF) then
|
|
if (s%sp <= 0) then; err = -3; return; end if
|
|
a = s%stack(s%sp); s%sp = s%sp - 1
|
|
if (a%ty /= TY_BOOL) then; err = -7; return; end if
|
|
if (a%b) then
|
|
if (cur%arg < 0 .or. cur%arg >= prog_len) then; err = -6; return; end if
|
|
npc = cur%arg
|
|
end if
|
|
else if (cur%op == OP_PRIM) then
|
|
arity = 2; if (cur%arg == PRIM_NOT) arity = 1
|
|
if (s%sp < arity) then; err = -4; return; end if
|
|
if (arity >= 2) then; b = s%stack(s%sp); s%sp = s%sp - 1; end if
|
|
a = s%stack(s%sp); s%sp = s%sp - 1
|
|
res = eval_prim(cur%arg, a, b)
|
|
s%sp = s%sp + 1; s%stack(s%sp) = res
|
|
else if (cur%op == OP_HALT) then
|
|
s%halted = .true.
|
|
end if
|
|
s%pc = npc
|
|
end function step
|
|
|
|
end module avm
|