Research-Stack

allaun/Research-Stack

Fork 0

mirror of https://github.com/allaunthefox/Research-Stack.git synced 2026-07-31 03:05:21 +00:00

Commit graph

Author	SHA1	Message	Date
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
Brandon Schneider	2a2aa0535f	feat(pist): remove dead PISTMachine root; add Trace tactic module lakefile.toml (PIST lib roots): - Remove "PISTMachine" — PISTMachine.lean does not exist; dead root would cause lake build PIST to fail with "unknown module" error - "Trace" was already added in the prior dirty change; committed here paired with the file it requires 2-Search-Space/PIST/Trace.lean (new): - Lean 4 tactic `trace_state_json "tag"` for Tier 2 flexure recording - Emits structured goal-state JSON (target, hypotheses, goal_count) prefixed with @@PIST_TRACE_JSON@@ sentinel to logInfo stdout - Python trace bridge parses the sentinel to capture mid-proof state - Namespace: PIST.Trace; no sorry, no float, no external deps beyond Lean 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:32:41 -05:00

Author

SHA1

Message

Date

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

Brandon Schneider

2a2aa0535f

feat(pist): remove dead PISTMachine root; add Trace tactic module

lakefile.toml (PIST lib roots):
- Remove "PISTMachine" — PISTMachine.lean does not exist; dead root
  would cause lake build PIST to fail with "unknown module" error
- "Trace" was already added in the prior dirty change; committed here
  paired with the file it requires

2-Search-Space/PIST/Trace.lean (new):
- Lean 4 tactic `trace_state_json "tag"` for Tier 2 flexure recording
- Emits structured goal-state JSON (target, hypotheses, goal_count)
  prefixed with @@PIST_TRACE_JSON@@ sentinel to logInfo stdout
- Python trace bridge parses the sentinel to capture mid-proof state
- Namespace: PIST.Trace; no sorry, no float, no external deps beyond Lean

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:32:41 -05:00

2 commits