From f36b88ed687ff9610acb707c4415eeca7ebbf5e3 Mon Sep 17 00:00:00 2001 From: Aaron Stainback Date: Fri, 3 Jul 2026 14:20:05 -0400 Subject: [PATCH] =?UTF-8?q?feat(isaspec):=20spec-driven=20mix=20over=20the?= =?UTF-8?q?=206502=20=E2=80=94=20the=20dynarec=20on=20a=20real,=20memory-b?= =?UTF-8?q?earing=20ISA=20(shadow*)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Aaron 2026-07-03 "build whatever you like" — the named #1 follow-on to the 6502 spec: the actual Futamura 1st projection (partial evaluation = dynarec) on a real ISA's real memory model, not the CHIP-8 toy. specializeMem extends the spec-driven mix to fold static ZERO-PAGE MEMORY as well as static registers, over any ISA given its spec + a register loadImm builder: - setreg with a static value (incl. a static mem read whose cell is known) FOLDS; a dynamic value residualizes (static reg reads materialized via loadImm). - setmem addr,val (static addr): static val FOLDS into known memory; dynamic val residualizes and marks that cell dynamic. Dynamic addr is out of the fragment. tryStatic/readsInKnown now thread a knownMem model (mem-read folds; the register- only `specialize` is untouched, passes an empty mem). For the 6502's zero-page ops the address is always a static field, so no dynamic-address materialization arises. Added LDX_IMM/LDY_IMM (real 6502 A2/A0) + load6502 so the loadImm builder is total over the ISA's A/X/Y registers, and the ADC_ZP constructor. The EXTENDED S-m-n law is machine-checked differentially: evalSpecFull spec residual dynReg dynMem ⊕ (knownReg, knownMem) = evalSpecFull spec p (staticReg∪dynReg) (staticMem∪dynMem) 12 IsaSpec tests green (2 new: the law over regs+memory across dynamic cell values; specialization reduces an all-static program to an EMPTY residual). Build 0/0. Co-Authored-By: Claude Fable 5 AgencySignature-v1: persona: otto actor: otto-column-b surface: src/Core/IsaSpec.fs topology: cowork-sandbox-clone intent: dynarec-over-a-real-memory-bearing-isa-partial-evaluation-folding-static-memory authorization: aaron-2026-07-03-build-whatever-you-like uncertainty: low measure: specializeMem-folds-static-regs-and-zero-page-mem-extended-s-m-n-law-differential-green-12-tests-build-0-0 delta-u: the-futamura-1st-projection-now-runs-on-a-real-isas-memory-model-proven-correct-not-just-the-toy seed: S4 --- src/Core/IsaSpec.fs | 137 +++++++++++++++++++++++++--- tests/Tests.FSharp/IsaSpec.Tests.fs | 57 ++++++++++++ 2 files changed, 182 insertions(+), 12 deletions(-) diff --git a/src/Core/IsaSpec.fs b/src/Core/IsaSpec.fs index 1f658b1dfc..9388bcaf69 100644 --- a/src/Core/IsaSpec.fs +++ b/src/Core/IsaSpec.fs @@ -262,6 +262,8 @@ module IsaSpec = let y = cst 2 isa [ op "LDA_IMM" [ setReg a (fld "imm") ] // A9 — A ← #imm + op "LDX_IMM" [ setReg x (fld "imm") ] // A2 — X ← #imm + op "LDY_IMM" [ setReg y (fld "imm") ] // A0 — Y ← #imm op "LDA_ZP" [ setReg a (memRead (fld "addr")) ] // A5 — A ← mem[addr] op "STA_ZP" [ setMem (fld "addr") (reg a) ] // 85 — mem[addr] ← A op "TAX" [ setReg x (reg a) ] // AA — X ← A @@ -282,11 +284,22 @@ module IsaSpec = // 6502 instruction constructors (programs are DynamicValue — homoiconic, like Isa.prog). let ldaImm nn = DynamicValue.Object [ "op", DynamicValue.String "LDA_IMM"; "imm", DynamicValue.Int(int64 nn) ] + let ldxImm nn = DynamicValue.Object [ "op", DynamicValue.String "LDX_IMM"; "imm", DynamicValue.Int(int64 nn) ] + let ldyImm nn = DynamicValue.Object [ "op", DynamicValue.String "LDY_IMM"; "imm", DynamicValue.Int(int64 nn) ] + /// The `loadImm` builder for the 6502's registers (A/X/Y = 0/1/2) — sets register `r` to `v` in + /// one instruction. Total over the ISA's actual registers; used to materialize static reads in `mix`. + let load6502 (r: int) (v: int) : DynamicValue = + match r with + | 0 -> ldaImm v + | 1 -> ldxImm v + | 2 -> ldyImm v + | _ -> DynamicValue.Object [ "op", DynamicValue.String "NOP" ] // unreachable: only A/X/Y exist let ldaZp addr = DynamicValue.Object [ "op", DynamicValue.String "LDA_ZP"; "addr", DynamicValue.Int(int64 addr) ] let staZp addr = DynamicValue.Object [ "op", DynamicValue.String "STA_ZP"; "addr", DynamicValue.Int(int64 addr) ] let tax = DynamicValue.Object [ "op", DynamicValue.String "TAX" ] let inx = DynamicValue.Object [ "op", DynamicValue.String "INX" ] let adcImm nn = DynamicValue.Object [ "op", DynamicValue.String "ADC_IMM"; "imm", DynamicValue.Int(int64 nn) ] + let adcZp addr = DynamicValue.Object [ "op", DynamicValue.String "ADC_ZP"; "addr", DynamicValue.Int(int64 addr) ] let ske nn = DynamicValue.Object [ "op", DynamicValue.String "SKE"; "imm", DynamicValue.Int(int64 nn) ] let jmp addr = DynamicValue.Object [ "op", DynamicValue.String "JMP"; "addr", DynamicValue.Int(int64 addr) ] let brk = DynamicValue.Object [ "op", DynamicValue.String "BRK" ] @@ -303,7 +316,7 @@ module IsaSpec = // immediate); the S-m-n law holds regardless, which is what the test checks. /// Is value `v` fully static under `known` (reads only known registers; indices resolvable)? - let rec private tryStatic (v: DynamicValue) (ins: DynamicValue) (known: System.Collections.Generic.Dictionary) : int option = + let rec private tryStatic (v: DynamicValue) (ins: DynamicValue) (known: System.Collections.Generic.Dictionary) (knownMem: System.Collections.Generic.Dictionary) : int option = match DynamicValue.get "v" v with | Some(DynamicValue.String "fld") -> match DynamicValue.get "k" v with @@ -319,44 +332,57 @@ module IsaSpec = | Some(DynamicValue.String "reg") -> match DynamicValue.get "i" v with | Some iv -> - match tryStatic iv ins known with + match tryStatic iv ins known knownMem with | Some idx -> match known.TryGetValue idx with | true, x -> Some x | _ -> None | None -> None | _ -> None + // a memory read is static iff its address is static AND that cell is currently known. + | Some(DynamicValue.String "mem") -> + match DynamicValue.get "addr" v with + | Some av -> + match tryStatic av ins known knownMem with + | Some a -> + match knownMem.TryGetValue a with + | true, x -> Some x + | _ -> None + | None -> None + | _ -> None | Some(DynamicValue.String "add") -> match DynamicValue.get "a" v, DynamicValue.get "b" v with | Some a, Some b -> - match tryStatic a ins known, tryStatic b ins known with + match tryStatic a ins known knownMem, tryStatic b ins known knownMem with | Some x, Some y -> Some(x + y) | _ -> None | _ -> None | Some(DynamicValue.String "sub") -> match DynamicValue.get "a" v, DynamicValue.get "b" v with | Some a, Some b -> - match tryStatic a ins known, tryStatic b ins known with + match tryStatic a ins known knownMem, tryStatic b ins known knownMem with | Some x, Some y -> Some(x - y) | _ -> None | _ -> None | _ -> None /// Register indices read inside `v` that are currently static (in `known`) — to materialize. - let rec private readsInKnown (v: DynamicValue) (ins: DynamicValue) (known: System.Collections.Generic.Dictionary) : int list = + let rec private readsInKnown (v: DynamicValue) (ins: DynamicValue) (known: System.Collections.Generic.Dictionary) (knownMem: System.Collections.Generic.Dictionary) : int list = match DynamicValue.get "v" v with | Some(DynamicValue.String "reg") -> match DynamicValue.get "i" v with | Some iv -> - let deeper = readsInKnown iv ins known - match tryStatic iv ins known with + let deeper = readsInKnown iv ins known knownMem + match tryStatic iv ins known knownMem with | Some idx when known.ContainsKey idx -> idx :: deeper | _ -> deeper | None -> [] + | Some(DynamicValue.String "mem") -> + DynamicValue.get "addr" v |> Option.map (fun x -> readsInKnown x ins known knownMem) |> Option.defaultValue [] | Some(DynamicValue.String "add") | Some(DynamicValue.String "sub") -> - let a = DynamicValue.get "a" v |> Option.map (fun x -> readsInKnown x ins known) |> Option.defaultValue [] - let b = DynamicValue.get "b" v |> Option.map (fun x -> readsInKnown x ins known) |> Option.defaultValue [] + let a = DynamicValue.get "a" v |> Option.map (fun x -> readsInKnown x ins known knownMem) |> Option.defaultValue [] + let b = DynamicValue.get "b" v |> Option.map (fun x -> readsInKnown x ins known knownMem) |> Option.defaultValue [] a @ b | _ -> [] @@ -384,6 +410,7 @@ module IsaSpec = let known = System.Collections.Generic.Dictionary() for KeyValue(k, v) in statics do known.[k] <- wrap v + let noMem = System.Collections.Generic.Dictionary() // register-only: no static memory let residual = System.Collections.Generic.List() let mutable err = None for ins in instrs do @@ -400,14 +427,14 @@ module IsaSpec = | Some(DynamicValue.String "setreg") -> match DynamicValue.get "i" eff, DynamicValue.get "val" eff with | Some iv, Some vv -> - match tryStatic iv ins known with + match tryStatic iv ins known noMem with | None -> err <- Some "isaspec specialize: dynamic write index not supported" | Some idx -> - match tryStatic vv ins known with + match tryStatic vv ins known noMem with | Some v -> known.[idx] <- wrap v // fold | None -> // dynamic: materialize static reads, emit the op as-is, write goes dynamic - for r in readsInKnown vv ins known do + for r in readsInKnown vv ins known noMem do residual.Add(loadImm r known.[r]) residual.Add ins known.Remove idx |> ignore @@ -420,3 +447,89 @@ module IsaSpec = let knownMap = known |> Seq.map (fun (KeyValue(k, v)) -> k, v) |> Map.ofSeq Ok(DynamicValue.Array(List.ofSeq residual), knownMap) | _ -> Error "isaspec: program must be an array of instructions" + + /// The memory-aware spec-driven `mix` (the dynarec over a real, memory-bearing ISA — e.g. the + /// 6502). Partial-evaluates a straight-line, single-effect program w.r.t. BOTH static registers + /// AND static zero-page memory, over any ISA given its `spec` and a register `loadImm` builder. + /// Returns the residual + the folded static registers + the folded static memory. Fragment: + /// - `setreg` with a fully-static value (incl. a static `mem` read whose cell is known) FOLDS; + /// a dynamic value residualizes (static register reads materialized first via `loadImm`). + /// - `setmem addr,val` with a static `addr`: a static `val` FOLDS into known memory; a dynamic + /// `val` residualizes (static reg reads materialized) and marks that cell dynamic. A dynamic + /// `addr` is out of the fragment (rejected) — real zero-page ops address a constant cell. + /// The extended S-m-n law holds (proven differentially against `evalSpecFull`): + /// `evalSpecFull spec residual dynReg dynMem ⊕ (knownReg, knownMem) = evalSpecFull spec p full`. + let specializeMem + (isaSpec: DynamicValue) + (loadImm: int -> int -> DynamicValue) + (program: DynamicValue) + (staticRegs: Map) + (staticMem: Map) + : Result * Map, string> = + let table = System.Collections.Generic.Dictionary() + match DynamicValue.get "ops" isaSpec with + | Some(DynamicValue.Array ops) -> + for o in ops do + match DynamicValue.get "op" o, DynamicValue.get "eff" o with + | Some(DynamicValue.String name), Some(DynamicValue.Array effs) -> table.[name] <- List.toArray effs + | _ -> () + | _ -> () + + match program with + | DynamicValue.Array instrs -> + let known = System.Collections.Generic.Dictionary() + for KeyValue(k, v) in staticRegs do + known.[k] <- wrap v + let knownMem = System.Collections.Generic.Dictionary() + for KeyValue(k, v) in staticMem do + knownMem.[k] <- wrap v + let residual = System.Collections.Generic.List() + let mutable err = None + for ins in instrs do + if err.IsNone then + let opName = + match DynamicValue.get "op" ins with + | Some(DynamicValue.String s) -> s + | _ -> "?" + match table.TryGetValue opName with + | false, _ -> err <- Some(sprintf "isaspec specializeMem: no spec for op '%s'" opName) + | true, [| eff |] -> + match DynamicValue.get "e" eff with + | Some(DynamicValue.String "halt") -> () + | Some(DynamicValue.String "setreg") -> + match DynamicValue.get "i" eff, DynamicValue.get "val" eff with + | Some iv, Some vv -> + match tryStatic iv ins known knownMem with + | None -> err <- Some "isaspec specializeMem: dynamic write index not supported" + | Some idx -> + match tryStatic vv ins known knownMem with + | Some v -> known.[idx] <- wrap v // fold (a static mem read folds here too) + | None -> + for r in readsInKnown vv ins known knownMem do + residual.Add(loadImm r known.[r]) + residual.Add ins + known.Remove idx |> ignore + | _ -> err <- Some "isaspec specializeMem: setreg operands" + | Some(DynamicValue.String "setmem") -> + match DynamicValue.get "addr" eff, DynamicValue.get "val" eff with + | Some av, Some vv -> + match tryStatic av ins known knownMem with + | None -> err <- Some "isaspec specializeMem: dynamic memory address not in the fragment" + | Some addr -> + match tryStatic vv ins known knownMem with + | Some v -> knownMem.[addr] <- wrap v // fold into known memory + | None -> + for r in readsInKnown vv ins known knownMem do + residual.Add(loadImm r known.[r]) + residual.Add ins + knownMem.Remove addr |> ignore // cell goes dynamic + | _ -> err <- Some "isaspec specializeMem: setmem operands" + | _ -> err <- Some "isaspec specializeMem: only setreg/setmem/halt in the straight-line fragment" + | true, _ -> err <- Some(sprintf "isaspec specializeMem: op '%s' is not single-effect (control flow / multi-effect)" opName) + match err with + | Some e -> Error e + | None -> + let knownRegMap = known |> Seq.map (fun (KeyValue(k, v)) -> k, v) |> Map.ofSeq + let knownMemMap = knownMem |> Seq.map (fun (KeyValue(k, v)) -> k, v) |> Map.ofSeq + Ok(DynamicValue.Array(List.ofSeq residual), knownRegMap, knownMemMap) + | _ -> Error "isaspec: program must be an array of instructions" diff --git a/tests/Tests.FSharp/IsaSpec.Tests.fs b/tests/Tests.FSharp/IsaSpec.Tests.fs index e13c0f0401..02e93271f6 100644 --- a/tests/Tests.FSharp/IsaSpec.Tests.fs +++ b/tests/Tests.FSharp/IsaSpec.Tests.fs @@ -184,3 +184,60 @@ let ``THE 6502 RUNS A REAL LOOP THROUGH MEMORY: count a zero-page cell up to N`` [] let ``THE 6502 SPEC IS BYTE-LOCKABLE DATA: a second real ISA rides the codec stack`` () = Assert.Empty(ValueTreeCodec.crossVerify [ ValueTreeCodec.parity ValueTreeCodec.json; ValueTreeCodec.cbor ] IsaSpec.mos6502) + +// ── the SPEC-DRIVEN MIX over the 6502 (the dynarec on a real, memory-bearing ISA) — shadow*, +// Aaron 2026-07-03 "build whatever you like". specializeMem folds static registers AND static +// zero-page memory. Proofs: +// 8. THE EXTENDED S-m-n LAW: evalSpecFull spec residual dynReg dynMem ⊕ (knownReg, knownMem) +// = evalSpecFull spec p (static∪dyn) — the memory-aware mix is correct (differential). +// 9. SPECIALIZATION REDUCES: the residual is strictly shorter when there is static memory to fold. + +// Overlay: the folded static map wins over the residual's dynamic result (folded cells/regs untouched). +let private overlay (known: Map) (dyn: Map) = + Map.fold (fun m k v -> Map.add k v m) dyn known + +[] +let ``THE 6502 MIX obeys the extended S-m-n law over registers AND memory`` () = + // A static; mem[20] dynamic. Static ops fold (incl. a static mem read); the dynamic ADC_ZP + // and everything after it residualize. + let p = + DynamicValue.Array + [ IsaSpec.staZp 10 // mem[10] = A (A static → fold) + IsaSpec.ldaZp 10 // A = mem[10] (static cell → fold) + IsaSpec.adcImm 5 // A = A + 5 (fold) + IsaSpec.staZp 11 // mem[11] = A (fold) + IsaSpec.adcZp 20 // A = A + mem[20] (mem[20] dynamic → A goes dynamic) + IsaSpec.staZp 12 // mem[12] = A (A dynamic → residualize) + IsaSpec.brk ] + let staticRegs = Map.ofList [ 0, 7 ] // A = 7 static + let staticMem = Map.empty + match IsaSpec.specializeMem IsaSpec.mos6502 IsaSpec.load6502 p staticRegs staticMem with + | Ok(residual, knownReg, knownMem) -> + for dynCell in [ 0; 1; 100; 250 ] do + let dynReg = Map.empty + let dynMem = Map.ofList [ 20, dynCell ] + match IsaSpec.evalSpecFull IsaSpec.mos6502 residual dynReg dynMem with + | Ok(rRegs, rMem) -> + let gotRegs = overlay knownReg rRegs + let gotMem = overlay knownMem rMem + match IsaSpec.evalSpecFull IsaSpec.mos6502 p (overlay staticRegs dynReg) (overlay staticMem dynMem) with + | Ok(fullRegs, fullMem) -> + Assert.Equal>(fullRegs, gotRegs) + Assert.Equal>(fullMem, gotMem) + | Error e -> Assert.Fail(sprintf "full run failed: %s" e) + | Error e -> Assert.Fail(sprintf "residual run failed: %s" e) + | Error e -> Assert.Fail(sprintf "specializeMem failed: %s" e) + +[] +let ``THE 6502 MIX reduces: an all-static program folds to an empty residual`` () = + // Everything static → the residual should carry no runtime work (all folded into known). + let p = DynamicValue.Array [ IsaSpec.ldaImm 10; IsaSpec.staZp 5; IsaSpec.adcImm 3; IsaSpec.staZp 6; IsaSpec.brk ] + match IsaSpec.specializeMem IsaSpec.mos6502 IsaSpec.load6502 p Map.empty Map.empty with + | Ok(residual, knownReg, knownMem) -> + (match residual with + | DynamicValue.Array xs -> Assert.Empty xs // fully folded — no residual instructions + | _ -> Assert.Fail "residual not an array") + Assert.Equal(13, Map.tryFind 0 knownReg |> Option.defaultValue 0) // A = 10 + 3 + Assert.Equal(10, Map.tryFind 5 knownMem |> Option.defaultValue 0) // mem[5] = 10 + Assert.Equal(13, Map.tryFind 6 knownMem |> Option.defaultValue 0) // mem[6] = 13 + | Error e -> Assert.Fail(sprintf "specializeMem failed: %s" e)