SilverSight/scala/avm.scala
allaun 540236e617 feat(cartan-dna): Cartan-DNA bridge — derive spectral gap from encoder
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.
2026-06-30 20:06:38 -05:00

135 lines
6.5 KiB
Scala

// AVM ISA v1 — Scala Port (Strict Functional Execution)
package silversight.avm
object AVM {
// ── Constants ──────────────────────────────────────────────────
val AVMClampMin = -2147483647
val AVMClampMax = 2147483647
val AVMQ0Min = -32767
val AVMQ0Max = 32767
val Q16Scale = 65536
val AVMMaxStack = 1024
def avmClamp(x: Long): Int = math.min(AVMClampMax.toLong, math.max(AVMClampMin.toLong, x)).toInt
def avmQ0Clamp(x: Long): Int = math.min(AVMQ0Max.toLong, math.max(AVMQ0Min.toLong, x)).toInt
def floorDiv(a: Long, b: Long): Int = {
if (b == 0) throw new ArithmeticException("division by zero")
val q = a / b; val r = a % b
(if (r != 0 && ((a ^ b) < 0)) q - 1 else q).toInt
}
def ltQ16V6(a: Int, b: Int): Boolean = {
val sa = a < 0; val sb = b < 0
if (sa != sb) sa else a < b
}
// ── Types ────────────────────────────────────────────────────
sealed trait Ty
case object Q0_16 extends Ty; case object Q16_16 extends Ty; case object BoolTy extends Ty
case class Val(ty: Ty, i: Int = 0, b: Boolean = false)
object Val { def q16(x: Int) = Val(Q16_16, i = avmClamp(x))
def q0(x: Int) = Val(Q0_16, i = avmQ0Clamp(x))
def bool(x: Boolean) = Val(BoolTy, b = x) }
// ── Primitives ──────────────────────────────────────────────
sealed trait Prim
case object AddSatQ0 extends Prim; case object SubSatQ0 extends Prim
case object AddSatQ16 extends Prim; case object SubSatQ16 extends Prim
case object MulSatQ16 extends Prim; case object DivSatQ16 extends Prim
case object LtQ16 extends Prim; case object EqQ16 extends Prim
case object And extends Prim; case object Or extends Prim; case object Not extends Prim
def primArity(p: Prim): Int = if (p == Not) 1 else 2
def execPrim(p: Prim, a: Val, b: Val): Val = (p, a.ty, b.ty) match {
case (AddSatQ0, Q0_16, Q0_16) => Val.q0(avmQ0Clamp(a.i.toLong + b.i))
case (SubSatQ0, Q0_16, Q0_16) => Val.q0(avmQ0Clamp(a.i.toLong - b.i))
case (AddSatQ16, Q16_16, Q16_16) => Val.q16(avmClamp(a.i.toLong + b.i))
case (SubSatQ16, Q16_16, Q16_16) => Val.q16(avmClamp(a.i.toLong - b.i))
case (MulSatQ16, Q16_16, Q16_16) => Val.q16(avmClamp(floorDiv(a.i.toLong * b.i, Q16Scale)))
case (DivSatQ16, Q16_16, Q16_16) => Val.q16(avmClamp(floorDiv(a.i.toLong * Q16Scale, b.i)))
case (LtQ16, Q16_16, Q16_16) => Val.bool(ltQ16V6(a.i, b.i))
case (EqQ16, Q16_16, Q16_16) => Val.bool(a.i == b.i)
case (And, BoolTy, BoolTy) => Val.bool(a.b && b.b)
case (Or, BoolTy, BoolTy) => Val.bool(a.b || b.b)
case (Not, BoolTy, _) => Val.bool(!a.b)
case _ => throw new RuntimeException("type mismatch")
}
// ── Instructions ────────────────────────────────────────────
sealed trait Op
case class PushQ16(x: Int) extends Op; case class PushBool(b: Boolean) extends Op
case class PushQ0(x: Int) extends Op; case object Pop extends Op
case object Dup extends Op; case object Swap extends Op
case class Load(i: Int) extends Op; case class Store(i: Int) extends Op
case class Jump(t: Int) extends Op; case class JumpIf(t: Int) extends Op
case class Primitive(p: Prim) extends Op; case object Halt extends Op
// ── State ───────────────────────────────────────────────────
case class State(pc: Int, stack: List[Val], locals: Vector[Option[Val]], halted: Boolean)
def initState(nLocals: Int = 0): State = State(0, Nil, Vector.fill(nLocals)(None), false)
// ── Step ────────────────────────────────────────────────────
def step(s: State, prog: Vector[Op]): Option[State] = {
if (s.halted) return None
if (s.pc < 0 || s.pc >= prog.length) return Some(State(s.pc, s.stack, s.locals, true))
val instr = prog(s.pc); var stack = s.stack; val npc = s.pc + 1
val growing = instr match {
case _: PushQ16 | _: PushBool | _: PushQ0 | Dup | Load => true; case _ => false
}
if (growing && stack.length >= AVMMaxStack) return None
instr match {
case PushQ16(x) => stack = Val.q16(x) :: stack
case PushBool(b) => stack = Val.bool(b) :: stack
case PushQ0(x) => stack = Val.q0(x) :: stack
case Pop => stack match {
case Nil => return None; case _ :: xs => stack = xs}
case Dup => stack match {
case Nil => return None; case x :: xs => stack = x :: x :: xs}
case Swap => stack match {
case a :: b :: xs => stack = b :: a :: xs; case _ => return None}
case Load(i) =>
if (i >= s.locals.length || s.locals(i).isEmpty) return None
stack = s.locals(i).get :: stack
case Store(i) => stack match {
case Nil => return None
case v :: xs =>
if (i >= s.locals.length) return None
val newLocals = s.locals.updated(i, Some(v))
return Some(State(npc, xs, newLocals, false))
}
case Jump(t) => if (t < 0 || t >= prog.length) return None
else return Some(State(t, stack, s.locals, false))
case JumpIf(t) => stack match {
case Val(BoolTy, _, true) :: xs =>
if (t < 0 || t >= prog.length) return None
return Some(State(t, xs, s.locals, false))
case Val(BoolTy, _, false) :: xs => stack = xs
case _ => return None
}
case Primitive(p) =>
val arity = primArity(p)
if (stack.length < arity) return None
val b = if (arity >= 2) { val (v, rest) = (stack.head, stack.tail); stack = rest; v } else Val.bool(false)
val a = stack.head; stack = stack.tail
try { stack = execPrim(p, a, b) :: stack } catch { case _: Throwable => return None }
case Halt => return Some(State(s.pc, stack, s.locals, true))
}
Some(State(npc, stack, s.locals, false))
}
// ── Run (fuel-bounded) ─────────────────────────────────────
@annotation.tailrec
def run(s: State, prog: Vector[Op], fuel: Int = 10000): Option[State] = {
if (fuel <= 0 || s.halted) return Some(s)
step(s, prog) match {
case None => None
case Some(next) => run(next, prog, fuel - 1)
}
}
}