Logic.lean

import Lean
import LeanModels.Python.Json
import LeanModels.Python.Semantics

/-!
# Spec layer (`LeanModels.Python`)

The bridge from extracted programs to theorems, per `docs/DESIGN.md`:

* **`ToExpr` instances** for `Span` and every AST type, so elaboration-time
  code can quote a parsed `Module` as a literal Lean term. All instances are
  derived — the core `deriving ToExpr` handler on this toolchain handles the
  nested inductives (`Expr`/`Stmt` recurse through `Array`) fine.
* **`load_program <ident> from "<path>.json"`** — a command elaborator that
  reads an envelope JSON at *elaboration time* (path relative to the package
  root, i.e. the `lake build` cwd), parses it with `Json.lean`, and defines
  `<ident> : Module` as a **literal term**. It is never a runtime parse of an
  embedded string: proofs can unfold `<ident>` (e.g. `simp [tri]`, `unfold
  tri`, or plain kernel reduction via `rfl`/`decide`-style closed evaluation).
* **`#print_program <ident>`** — logs the `Repr` of a loaded program.
* **`CallsTo`** — the partial-correctness call relation (normative signature).
* **`@[spec]`** — the attribute for registered specification lemmas. On this
  toolchain it is core Lean's own `spec` attribute (the name is taken by the
  `mvcgen` spec registry, which also accepts plain simp-shaped theorems), so
  DESIGN.md's surface syntax works verbatim; see the section comment at the
  bottom of this file for details and the recorded deviation.
-/

namespace LeanModels.Python

/-! ## `ToExpr` instances (derived; used by `load_program` at elaboration time) -/

deriving instance Lean.ToExpr for Span
deriving instance Lean.ToExpr for BinOp
deriving instance Lean.ToExpr for UnaryOp
deriving instance Lean.ToExpr for BoolOp
deriving instance Lean.ToExpr for CmpOp
deriving instance Lean.ToExpr for Const
deriving instance Lean.ToExpr for Param
deriving instance Lean.ToExpr for Expr
deriving instance Lean.ToExpr for WithItem
deriving instance Lean.ToExpr for Stmt
deriving instance Lean.ToExpr for FunctionDefn
deriving instance Lean.ToExpr for NamedTupleDefn
deriving instance Lean.ToExpr for ClassDefn
deriving instance Lean.ToExpr for Module

/-! ## `load_program` -/

open Lean Elab Command in
/--
`load_program tri from "Examples/python/tri/tri.json"` reads the standardized
envelope JSON at **elaboration time** and defines `tri : Module` as a
**literal** first-order term (via the `ToExpr` instances above), so proofs can
unfold it. The path is resolved relative to the current working directory,
which under `lake build` is the package root. Missing files and malformed
envelopes are clear elaboration errors, never silent.

The definition lands in the current namespace (companion files use the root
namespace). Rebuild-on-source-change is handled by the sha256 line in the
generated companion file, not by this command.
-/
elab "load_program " name:ident " from " path:str : command => do
  let pathStr := path.getString
  let contents ←
    match ← (IO.FS.readFile ⟨pathStr⟩).toBaseIO with
    | .ok c => pure c
    | .error e =>
        throwErrorAt path
          "load_program: cannot read '{pathStr}': {toString e}\n(relative paths resolve against the current working directory — the package root under `lake build`; current cwd: '{toString (← IO.currentDir)}')"
  let envl ←
    match parseEnvelopeString contents with
    | .error e =>
        throwErrorAt path "load_program: '{pathStr}' is not a valid envelope: {e}"
    | .ok envl => pure envl
  unless envl.language == "python" do
    throwErrorAt path
      "load_program: '{pathStr}' has language '{envl.language}', expected 'python'"
  let declName := (← getCurrNamespace) ++ name.getId
  if (← getEnv).contains declName then
    throwErrorAt name "load_program: '{declName}' has already been declared"
  liftCoreM do
    addAndCompile <| .defnDecl {
      name := declName
      levelParams := []
      type := Lean.mkConst ``LeanModels.Python.Module
      value := Lean.toExpr envl.module
      hints := .abbrev
      safety := .safe }
    -- Without this, `simp [<ident>]` cannot realize the definition's
    -- equational lemmas ("enableRealizationsForConst must be called" error).
    enableRealizationsForConst declName
    addDocStringCore declName
      s!"Program module loaded by `load_program` from `{pathStr}` (source: `{envl.sourceFile}`, sha256 `{envl.sourceSha256}`). A literal `LeanModels.Python.Module` — proofs may unfold it."
  liftTermElabM do
    Term.addTermInfo' name (Lean.mkConst declName) (isBinder := true)

/-- `#print_program tri` logs the `Repr` of a program previously defined by
`load_program` (or any `Module`-typed constant). -/
macro "#print_program " name:ident : command => `(#eval (repr $name))

/-! ## Spec layer -/

/-- Partial correctness of a call, abstracted over fuel: `CallsTo m f args r`
holds iff *some* fuel makes `callFunction m f args fuel = .ok r`. Fuel
monotonicity is intentionally *not* baked in; theorems quantify over fuel in
the canonical `@[spec]` shape (see the `spec` attribute docstring). -/
def CallsTo (m : Module) (f : String) (args : Array Val) (r : Val) : Prop :=
  ∃ fuel, callFunction m f args fuel = .ok r

/-! ## Proof-automation seed

Reusable lemmas and the `py_simp` tactic for *symbolic execution* of the
interpreter inside proofs. The intended proof pattern for a canonical
partial-correctness theorem (`callFunction p "f" args fuel = .ok r → r = …`)
is:

1. `match fuel with` — split off the small fuels (each reduces to
   `.timeout = .ok r`, which `py_simp at h` closes) from `fuel + k`, where
   `k` bounds the straight-line depth of the function body.
2. `py_simp [p, …] at h` — unfold the program literal and
   symbolically execute. Recursive-call boundaries (`callIn`,
   `execWhile`, `execFor`) are **not** in the default simp set, so they stay
   frozen at symbolic fuel; unfold the outer one with `rw [callIn.eq_2] at h`
   (resp. `execWhile.eq_2`) and pass them explicitly only where full
   unfolding is safe (non-recursive programs). The public `callFunction`
   wrapper is non-recursive and unfolds freely (it is in the default set).
3. `Res.bind_eq_ok` / `Run.bind_eq_ok` (global simp lemmas) turn
   `x >>= f = .ok r` (resp. `Run.bind x f = .ok s r`) into existential
   nests, so after `py_simp` the hypothesis is a nest of existentials whose
   atoms are the frozen recursive calls:
   `obtain` them, discharge each with the induction hypothesis (induction on
   fuel — structural for loops, `Nat.strongRecOn` for recursion), `subst`,
   and `py_simp` again until `h` closes the goal.
-/

/-! (The `Res` bind-normalization simp lemmas — `Res.pure_eq`,
`Res.ok_bind`, `Res.exn_bind`, `Res.timeout_bind`, `Res.unsupported_bind`,
`Res.bind_eq_ok` — moved to Runtime.lean with the H1 re-shape: the
thaw/freeze roundtrip proofs there need them, and Runtime is imported
by everything that previously found them here.) -/

/-! ### `sorted` execution lemmas (Mathlib-free)

`sortInts`/`insertLe` are deliberately NOT in the `py_simp`/`interpUnfolds`
lists: symbolic goals keep the compact `sortInts data` handle (concrete runs
reduce through the compiled evaluator anyway). The two rewrite lemmas below
ARE in the lists — they are what lets symbolic execution step through
`sortedVal` on a `ToVal`-marshalled int list and through the subsequent
`len`/index bounds. The `Pairwise`/`Perm` harvest needs Mathlib and lives in
`Examples/python/bench_statistics/proof.lean` (`sortInts_eq` bridge). -/

/-- Marshalled int lists extract fully: the `asIntList` bridge for symbolic
execution of `sorted(data)` at a `ToVal`-marshalled argument (runtime side
since H1: the argument arrives thawed). -/
theorem asIntList_map_int (l : List Int) :
    asIntList (l.map RVal.int) = some l := by
  induction l with
  | nil => rfl
  | cons x xs ih => simp [asIntList, ih]

/-- `insertLe` grows the list by one (helper of `sortInts_length`). -/
theorem insertLe_length (x : Int) (l : List Int) :
    (insertLe x l).length = l.length + 1 := by
  induction l with
  | nil => rfl
  | cons y ys ih => simp only [insertLe]; split <;> simp [ih]

/-- Sorting preserves length — Mathlib-free (symbolic execution needs it to
decide `len`/index bounds after a `data = sorted(data)` assignment). -/
theorem sortInts_length (l : List Int) :
    (sortInts l).length = l.length := by
  induction l with
  | nil => rfl
  | cons x xs ih => simp [sortInts, insertLe_length, ih]

open Lean Lean.Parser.Tactic in
/-- `py_simp [extra, lemmas] at h` — one stack frame's worth of symbolic
execution of the Python interpreter: `simp` with every interpreter equation
*except* the recursion points `callIn`, `execWhile`, `execFor`, and
(H2) `execForList` — and the fueled `heapEq`/`freezeH` walks —
which stay frozen at symbolic fuel so induction hypotheses can be applied to
them. Pass them explicitly (`py_simp [callIn, execWhile, tri] at h`)
when full unfolding is safe (no recursion, or concrete fuel), or unfold
exactly one step with `rw [callIn.eq_2] at h` / `rw [execWhile.eq_2]
at h` / `rw [execFor.eq_2] at h` / `rw [execForList.eq_2] at h`. The public `callFunction` is a
non-recursive wrapper since H1 (thaw ∘ fresh-world ∘ `callIn` ∘ freeze)
and IS in the default set — unfolding it exposes the frozen `callIn`.
Program literals introduced by `load_program` must also be passed explicitly
(e.g. `py_simp [tri] at h`). `and_assoc` is included so that fully-reduced
existential nests collapse. -/
macro (name := pySimpTactic) "py_simp" "[" args:(simpStar <|> simpErase <|> simpLemma),* "]"
    loc:(location)? : tactic => do
  let extra : Syntax.TSepArray
      [`Lean.Parser.Tactic.simpStar, `Lean.Parser.Tactic.simpErase,
       `Lean.Parser.Tactic.simpLemma] "," := ⟨args.elemsAndSeps⟩
  `(tactic| set_option linter.unusedSimpArgs false in
      -- pass 3: the call-arm equations grew (the builtin trio + the
      -- live-view consults), so one frame of the 955KB shipped module
      -- needs more than simp's default 100k steps — budget only, no
      -- semantic change
      simp (config := { maxSteps := 1000000 })
           [execStmts, execStmt, evalExpr, evalExprs, evalBoolChain,
            evalCompareChain, evalDictItems, findFunction, mkCallEnv, arityOk,
            defaultBindings, Env.lookup, Env.set,
            Const.toVal, Const.toRVal, truthy, truthyH, asInt, RVal.isNone,
            valEq, valEqList, intCmp,
            strCmp, evalCompareOp, evalCompareOpH, evalBinOp, strFormat,
            evalUnaryOp,
            evalUnaryOpH, lenVal, lenValH, sortedVal,
            asIntList, asIntList_map_int, sortInts_length, normIndex,
            indexVal, indexValH, targetNames, bindAll, assignTo, assignToH,
            checkBytesIndex, checkBytesCompare, bytesOperandCheck,
            unpackSeq, unpackStoreH,
            foldExtremum, extremumVal, extremumValH, absVal, intCastArgs, intCastVal, boolCastArgs,
            divmodArgs, importErrorHandlerMatch, excHandlerNamesAux,
            admittedBuiltinExc, builtinExcCatches,
            strOfVal,
            strOfValH, reprArgs, formatValueH, ordVal, chrVal, strJoinList, strJoinH,
            enumStart, enumFrame, countArgs,
            isBuiltinName, sortedValH,
            markUnboundLocals, stmtHasUnboundLocal, stmtHasUnboundLocalList,
            hasLateRaiseNames, directRaiseName, directAssignName,
            hasDirectAssignAfter, markUnboundLocals_noop,
            hashableKey, hashableKeyList, keyEq, keyEqList, RVal.unhashName,
            keyHasInstanceRef, keyHasInstanceRefList, keyRefusal,
            dictFind, dictStore, dictBuild, heapIndex, heapStore, heapLen,
            heapContains, heapContainsScan, valContains, genPlan, genBreak,
            genContinue, heapGet, heapAppend,
            heapPop, heapInsert,
            heapAttrStore, findClass, findClassAux, classAt, getClass?,
            attrReadPlan, attrReadResult, attrCallPlan, execAttrCall,
            endsWithUU, dunderShaped, hasExtraDunder,
            findNamedTuple, findNamedTupleAux, fieldIndex, ntupleProtoName,
            ntupleMethodName, ntupleAttr, ntupleCallPlan,
            sliceVal, strCallPlan,
            RVal.refFree, RVal.refFreeList,
            Val.listFree, Val.listFreeList, Val.listFreeArgs,
            Heap.get?, Heap.update, danglingMsg,
            moduleGlobals, moduleInit, globalsFold, globalsStep, lookupG,
            globalsDirty, Stmt.g1Dirty, Stmt.g1Binds, Stmt.g1BindsList,
            Stmt.g1Stores, Stmt.g1StoresList, Expr.g1Primary,
            Expr.g1TargetStores, Expr.g1TargetStoresList,
            targetBindsG, targetBindsListG, benignImportBinds, isModuleDunder,
            resolvedG, resolvedGAux, targetNamesG, evalGlobalExpr, evalGlobalExprs,
            evalGlobalDictItems, globalFuel,
            sumArgs, sumFold, rangeLen, rangeValsAux, rangeVals, rangeMake,
            RangeBound.toInt, RangeBound.toRVal, asRangeBound, rangeBoundRepr,
            seqBudget, shiftBudget, tupleRepeat, seqSlice, seqSliceElems,
            g1DivGate, g1ExecCandidate, g1HeapPure, g1HeapPureList,
            Stmt.defFree, Stmt.defFreeList, topLevelDefFree,
            initFoldLive, initFoldStep, initExecStmt, initItemsLoop,
            initBodyStmts, flushInitLocals, initBindable, initExecFuel,
            stmtIsClockImport, moduleClockOk, clockRecvOk, isClockCall,
            callFunctionClock,
            callFunction, initWorld, RVal.thaw, RVal.thawList, RVal.thawArgs,
            RVal.freeze, RVal.freezeList, RVal.freezeB, RVal.freezeListB,
            and_assoc, $extra,*] $(loc)?)

@[inherit_doc pySimpTactic]
macro "py_simp" loc:(Lean.Parser.Tactic.location)? : tactic =>
  `(tactic| py_simp [] $(loc)?)

/-!
### The `@[spec]` attribute

Specification lemmas are registered with **`@[spec]`**, exactly as DESIGN.md
prescribes. Canonical partial-correctness shape:

```
@[spec] theorem tri_spec (n : Int) (hn : 0 ≤ n) {fuel : Nat} {r : Val}
    (h : callFunction tri "tri" #[.int n] fuel = .ok r) :
    r = .int (n * (n + 1) / 2)
```

**Mechanism (toolchain deviation, recorded):** DESIGN.md suggested
`register_simp_attr spec`, but on toolchain v4.33.0-rc1 the attribute name
`spec` is already taken by core Lean (the `mvcgen` spec attribute, initializer
`Lean.Elab.Tactic.Do.SpecAttr.mkSpecAttr` — "Marks Hoare triple specifications
**and simp theorems** for use with `mvcgen` tactics"). Attribute names are
global, so registering our own `spec` collides at initializer time in every
importing module. Resolution: we rely on the core attribute — it explicitly
accepts plain (conditional) simp-shaped theorems like the canonical shape
above, keeps them in a queryable registry (`Lean.Elab.Tactic.Do`'s spec-
theorem extension), and preserves DESIGN.md's surface syntax and intent
(automation can find callee specs) with zero custom code.

Consequences for later phases:
* `@[spec] theorem …` compiles verbatim — nothing changes in spec statements.
* There is no `simp [spec]` simp set; cite registered lemmas by name
  (`simp [tri_spec]`) or query the core spec registry programmatically.
* `native_decide` remains forbidden in `@[spec]` theorems (`#print axioms`
  must show only standard axioms).
-/

/-! ### Trace classes (pass 6, docs/memory-model.md §the trace clock)

Named predicates over clock traces — the AXIOM CLASSES trace-quantified
theorems are conditioned on. `WallClock` is the unconstrained class
(`True` — a `∀ tr` theorem with no side condition IS a WallClock theorem
and consumes no axioms): the first trace-quantified theorem, "safety is
trace-independent when the run never consults the clock", is stated over
it (the sunfish stepped-search pins for ALL traces —
`Examples/python/sunfish/spec.lean`). `Monotone` (nondecreasing
readings) is the class future deadline-abstraction theorems will consume
("once expired, always expired" needs it); it is STATED, nothing spends
it yet — recorded groundwork, not a claim. -/

/-- A clock trace: the finite list of readings `World.clock` serves to
`time.time()` in order (opaque integers — docs/memory-model.md §the
trace clock records the ℤ decision and its soundness argument). -/
abbrev ClockTrace := List Int

/-- The unconstrained trace class: EVERY reading sequence is a possible
wall clock (readings may jump backwards — NTP steps, VM migrations; the
model assumes nothing). `∀ tr` theorems are exactly WallClock theorems. -/
def ClockTrace.WallClock (_ : ClockTrace) : Prop := True

/-- The nondecreasing trace class: each reading is ≤ every later one.
The class deadline-abstraction theorems will consume — once
`t > deadline` holds for a reading, it holds for every later reading of
a Monotone trace. Stated groundwork; no theorem consumes it yet. -/
def ClockTrace.Monotone (tr : ClockTrace) : Prop :=
  tr.Pairwise (· ≤ ·)

/-- Every trace is a wall clock — the class really is unconstrained. -/
theorem ClockTrace.wallClock (tr : ClockTrace) : tr.WallClock := trivial

/-- A Monotone trace's tail is Monotone (the shape pop-stepping
consumes: after `time.time()` pops the head, the residual trace is
still in class). -/
theorem ClockTrace.Monotone.tail {t : Int} {tr : ClockTrace}
    (h : ClockTrace.Monotone (t :: tr)) : ClockTrace.Monotone tr :=
  (List.pairwise_cons.mp h).2

end LeanModels.Python