allaun/Research-Stack
1
0
Fork 0
mirror of https://github.com/allaunthefox/Research-Stack.git synced 2026-07-31 03:05:21 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions
Research-Stack/0-Core-Formalism
History
Brandon Schneider 5290413080 fix(avm-isa): stabilize AVMIsa + PIST.Trace build; canary #eval fires clean 
AVMIsa fixes (all pre-existing errors from the upstream merge):
- Types.lean: add Repr to AvmTy
- Value.lean: replace `deriving Inhabited` with explicit instance (AnyVal
  is a dependent structure; auto-derive can't pick a default ty+val pair);
  add Repr instance that delegates to AvmVal.repr
- Instr.lean: add Repr to Prim and Instr
- State.lean: fix `List.set ⟨i, h⟩` → `List.set i` (List.set takes Nat,
  not Fin); drop now-dead `h` binding; add Repr to State
- Step.lean: rewrite evalPrim branches to pattern-match directly on AnyVal
  `⟨ty, val⟩` pairs instead of `if v.ty = T` + separate val match (Lean
  can't unify `AvmVal v.ty` with `AvmVal T` from a propositional if-guard);
  replace `List.get? pc` (removed in Lean 4.30) with `list[pc]?` subscript;
  rename Q0_16.addSat/subSat → Q0_16.add/sub (no sat variants exist);
  add Repr to StepError and Outcome

PIST.Trace fixes:
- Drop invalid `set_option pp.pretty true`
- MVarId.toNat → MVarId.name.toString
- List.size → List.length (then .toArray for Json.arr)
- Json.num takes JsonNumber {mantissa : Int, exponent : Int}; cast Nat → Int
- goals.mapM goalToJson: lift MetaM → TacticM via liftMetaM

Canary result: `#eval run 8 canaryNot canaryState` →
  Outcome.ok { pc := 2, stack := [AvmVal.b true], halted := true }

Generated with [Devin](https://cli.devin.ai/docs)

Co-Authored-By: Devin <158243242+devin-ai-integration[bot]@users.noreply.github.com>
2026-05-26 21:39:46 -05:00
..
core Remove legacy Python prototypes superseded by Lean formalization 2026-05-19 15:34:17 +00:00
lean fix(avm-isa): stabilize AVMIsa + PIST.Trace build; canary #eval fires clean 2026-05-26 21:39:46 -05:00
otom Add Phys.org May 2026 source intake for bees, biocoatings, THz, and diamond membranes 2026-05-23 19:27:37 -05:00
receipts docs: add bio optical witness living light equations 2026-05-09 20:53:51 -05:00
rust/ftdi_gimbal initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00
README.md initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00

README.md

0-Core-Formalism

Purpose: Formal foundations for the entire Research Stack — Lean modules, bind primitive, Triumvirate consensus, core source.

No external dependencies. All other layers depend on this.

Contents (Target)

Source Destination
0-Core-Formalism/lean/Semantics/ 0-Core-Formalism/lean/Semantics/
core/ 0-Core-Formalism/core/

Concepts

  • bind — State → (State → Action) → State
  • TriumvirateClock — ternary consensus (ADD/PAUSE/SUBTRACT)
  • Builder/Judge/Warden — roles mapped to hardware registers
  • OTOM — Ordered Transformation & Orchestration Model

Build

cd "0-Core-Formalism"
lake build