Skip to content

Lean2Js.StepAgree

Imports 3

The small-step machine answers what `eval` answers #

The small-step machine answers what eval answers.

eval spends fuel on the depth of what it evaluates and the machine spends a step on every transition, so the two bounds do not line up: a long array costs the machine a step per element and eval nothing. The claim is therefore that the machine, given enough steps, reaches the answer eval gives. The proof follows eval's recursion on fuel and carries the continuation the machine holds when it enters an expression.

def

Lean2Js.StepAgree.steps

(p : Core.Program) :

Nat → State → State

Equations

Lean2Js.StepAgree.steps p 0 x✝ = x✝
Lean2Js.StepAgree.steps p n.succ x✝ = Lean2Js.StepAgree.steps p n (Lean2Js.step p x✝)

Instances For

Used by

theorem

Lean2Js.StepAgree.steps_add

(p : Core.Program) (m n : Nat) (s : State) :

steps p (m + n) s = steps p n (steps p m s)

Used by

theorem

Lean2Js.StepAgree.steps_done

(p : Core.Program) (r : Except Err Value) (n : Nat) :

steps p n (State.done r) = State.done r

Used by

def

Lean2Js.StepAgree.Reaches

(p : Core.Program) (s t : State) :

Equations

Lean2Js.StepAgree.Reaches p s t = ∃ (n : Nat ), Lean2Js.StepAgree.steps p n s = t

Instances For

Used by

theorem

Lean2Js.StepAgree.Reaches.refl

@[simp]

{p : Core.Program} {s : State} :

Used by

theorem

Lean2Js.StepAgree.Reaches.trans

{p : Core.Program} {s t u : State} (h1 : Reaches p s t) (h2 : Reaches p t u) :

Used by

theorem

Lean2Js.StepAgree.Reaches.head

{p : Core.Program} {s t : State} (h : Reaches p (step p s) t) :

Used by

def

Lean2Js.StepAgree.outcome

:

Except Err Value → List Frame → State

Where the machine stands once eval's answer is in: a value has been handed to the continuation, and an error has stopped the machine whatever the continuation was.

Equations

Lean2Js.StepAgree.outcome (Except.ok v) x✝ = Lean2Js.State.finish v x✝
Lean2Js.StepAgree.outcome (Except.error e) x✝ = Lean2Js.State.done (Except.error e)

Instances For

Used by

theorem

Lean2Js.StepAgree.outcome_nil

(r : Except Err Value) :

outcome r [] = State.done r

Used by

theorem

Lean2Js.StepAgree.finishOrFail

(p : Core.Program) (r : Except Err Value) (k : List Frame) :

Reaches p (match r with | Except.ok w => State.finish w k | Except.error e => State.fail e) (outcome r k)

Used by

def

Lean2Js.StepAgree.Sim

(p : Core.Program) (f : Nat) :

Equations

One or more equations did not get rendered due to their size.

Instances For

Used by

theorem

Lean2Js.StepAgree.sub

{p : Core.Program} {f : Nat} {env : Env} {x : Core.Expr} {fr : Frame} {k : List Frame} {t : State} (ih : Sim p f) (hne : evalExpr p f env x ≠ Except.error Err.outOfFuel) (hok : ∀ (v : Value), evalExpr p f env x = Except.ok v → Reaches p (step p (State.apply v (fr :: k))) t) (herr : ∀ (err : Err), evalExpr p f env x = Except.error err → t = State.done (Except.error err)) :

Reaches p (State.eval env x (fr :: k)) t

Enters a subterm under one more frame and resumes from what it returned.

Used by

theorem

Lean2Js.StepAgree.args

{p : Core.Program} {f : Nat} (ih : Sim p f) (env : Env) (k : List Frame) (build : List Value → State) (frame : List Value → List Core.Expr → Frame) (hframe : ∀ (v : Value) (done : List Value) (rest : List Core.Expr), step p (State.apply v (frame done rest :: k)) = continueArgs build (done ++ [v]) rest env k frame) (es : List Core.Expr) (done : List Value) (t : State) :

evalArgs p f env es ≠ Except.error Err.outOfFuel → (∀ (vs : List Value), evalArgs p f env es = Except.ok vs → Reaches p (build (done ++ vs)) t) → (∀ (err : Err), evalArgs p f env es = Except.error err → t = State.done (Except.error err)) → Reaches p (continueArgs build done es env k frame) t

Used by

theorem

Lean2Js.StepAgree.mapItems

{p : Core.Program} {f : Nat} (ih : Sim p f) (env : Env) (binder : String) (body : Core.Expr) (k : List Frame) (xs done : List Value) (t : State) :

evalMapItems p f env binder body xs ≠ Except.error Err.outOfFuel → (∀ (vs : List Value), evalMapItems p f env binder body xs = Except.ok vs → Reaches p (State.finish (Value.arr (done ++ vs)) k) t) → (∀ (err : Err), evalMapItems p f env binder body xs = Except.error err → t = State.done (Except.error err)) → Reaches p (continueMap binder body env done xs k) t

Used by

theorem

Lean2Js.StepAgree.sortDone_reaches

(p : Core.Program) (ps : List (Value × Value)) (k : List Frame) :

Reaches p (sortDone ps k) (outcome (do let vs ← sortPairs ps Except.ok (Value.arr vs)) k)

Used by

theorem

Lean2Js.StepAgree.sortItems

{p : Core.Program} {f : Nat} (ih : Sim p f) (env : Env) (binder : String) (body : Core.Expr) (k : List Frame) (xs : List Value) (done : List (Value × Value)) (t : State) :

evalMapItems p f env binder body xs ≠ Except.error Err.outOfFuel → (∀ (keys : List Value), evalMapItems p f env binder body xs = Except.ok keys → Reaches p (sortDone (done ++ keys.zip xs) k) t) → (∀ (err : Err), evalMapItems p f env binder body xs = Except.error err → t = State.done (Except.error err)) → Reaches p (continueSort binder body env done xs k) t

Used by

theorem

Lean2Js.StepAgree.filterItems

{p : Core.Program} {f : Nat} (ih : Sim p f) (env : Env) (binder : String) (body : Core.Expr) (k : List Frame) (xs done : List Value) (t : State) :

evalFilterItems p f env binder body xs ≠ Except.error Err.outOfFuel → (∀ (vs : List Value), evalFilterItems p f env binder body xs = Except.ok vs → Reaches p (State.finish (Value.arr (done ++ vs)) k) t) → (∀ (err : Err), evalFilterItems p f env binder body xs = Except.error err → t = State.done (Except.error err)) → Reaches p (continueFilter binder body env done xs k) t

Used by

theorem

Lean2Js.StepAgree.findItems

{p : Core.Program} {f : Nat} (ih : Sim p f) (env : Env) (binder : String) (body : Core.Expr) (k : List Frame) (xs : List Value) (t : State) :

evalFindItems p f env binder body xs ≠ Except.error Err.outOfFuel → (∀ (v : Value), evalFindItems p f env binder body xs = Except.ok v → Reaches p (State.finish v k) t) → (∀ (err : Err), evalFindItems p f env binder body xs = Except.error err → t = State.done (Except.error err)) → Reaches p (continueFind binder body env xs k) t

Used by

theorem

Lean2Js.StepAgree.quantItems

{p : Core.Program} {f : Nat} (ih : Sim p f) (env : Env) (op : Core.QuantOp) (binder : String) (body : Core.Expr) (k : List Frame) (xs : List Value) (t : State) :

evalQuantItems p f env op binder body xs ≠ Except.error Err.outOfFuel → (∀ (v : Value), evalQuantItems p f env op binder body xs = Except.ok v → Reaches p (State.finish v k) t) → (∀ (err : Err), evalQuantItems p f env op binder body xs = Except.error err → t = State.done (Except.error err)) → Reaches p (continueQuant op binder body env xs k) t

Used by

theorem

Lean2Js.StepAgree.reduceItems

{p : Core.Program} {f : Nat} (ih : Sim p f) (env : Env) (accName elemName : String) (body : Core.Expr) (k : List Frame) (xs : List Value) (acc : Value) (t : State) :

evalReduceItems p f env accName elemName body acc xs ≠ Except.error Err.outOfFuel → (∀ (v : Value), evalReduceItems p f env accName elemName body acc xs = Except.ok v → Reaches p (State.finish v k) t) → (∀ (err : Err), evalReduceItems p f env accName elemName body acc xs = Except.error err → t = State.done (Except.error err)) → Reaches p (continueReduce accName elemName body env acc xs k) t

Used by

The walk a fold takes #

A fold recurses on the value rather than on the expression, so the machine's walk over a node needs an induction of its own: one strong induction on a bound for the value's size, carrying the node walk, the field walk and the element walk at once because they call each other. Each carries the continuation the way mapItems carries it along a list — the state the field walk hands its answer to is the field walk itself with nothing left to walk.

theorem

Lean2Js.StepAgree.foldWalk

{p : Core.Program} {f : Nat} (ih : Sim p f) (env : Env) (tn : String) (ta : List Core.Ty) (alts : List Core.Alt) (m : Nat) :

(∀ (v : Value) (k : List Frame) (t : State), sizeOf v < m → evalFold p f env tn ta alts v ≠ Except.error Err.outOfFuel → (∀ (w : Value), evalFold p f env tn ta alts v = Except.ok w → Reaches p (State.finish w k) t) → (∀ (err : Err), evalFold p f env tn ta alts v = Except.error err → t = State.done (Except.error err)) → Reaches p (beginFold p tn ta alts env v k) t) ∧ (∀ (ctor : String) (fields done : List (String × Value)) (rest : List Core.Field) (k : List Frame) (t : State), sizeOf fields < m → evalFoldFields p f env tn ta alts fields rest ≠ Except.error Err.outOfFuel → (∀ (ps : List (String × Value)), evalFoldFields p f env tn ta alts fields rest = Except.ok ps → Reaches p (continueFoldFields tn ta alts env ctor fields (done ++ ps) [] k) t) → (∀ (err : Err), evalFoldFields p f env tn ta alts fields rest = Except.error err → t = State.done (Except.error err)) → Reaches p (continueFoldFields tn ta alts env ctor fields done rest k) t) ∧ ∀ (ctor : String) (fields done : List (String × Value)) (name : String) (doneXs restXs : List Value) (rest : List Core.Field) (k : List Frame) (t : State), sizeOf restXs < m → evalFoldList p f env tn ta alts restXs ≠ Except.error Err.outOfFuel → (∀ (ys : List Value), evalFoldList p f env tn ta alts restXs = Except.ok ys → Reaches p (continueFoldFields tn ta alts env ctor fields (done ++ [(name, Value.arr (doneXs ++ ys))]) rest k) t) → (∀ (err : Err), evalFoldList p f env tn ta alts restXs = Except.error err → t = State.done (Except.error err)) → Reaches p (continueFoldElems tn ta alts env ctor fields done name doneXs restXs rest k) t

Used by

theorem

Lean2Js.StepAgree.step_bin

{p : Core.Program} {env : Env} {op : Core.BinOp} {lhs rhs : Core.Expr} {k : List Frame} (hop : op ≠ Core.BinOp.and) (hor : op ≠ Core.BinOp.or) :

step p (State.eval env (Core.Expr.bin op lhs rhs) k) = State.eval env lhs (Frame.binL op rhs env :: k)

Used by

def

Lean2Js.StepAgree.tacticResume

:

Lean.ParserDescr

Closes a goal once the machine has applied a frame that computes its answer outright: the frame and eval branch on the same values, so after unfolding both sides the branches pair off.

Equations

Lean2Js.StepAgree.tacticResume = Lean.ParserDescr.node `Lean2Js.StepAgree.tacticResume 1024 (Lean.ParserDescr.nonReservedSymbol "resume" false)

Instances For

Used by

theorem

Lean2Js.StepAgree.sim

(p : Core.Program) (f : Nat) :

Sim p f

Used by

theorem

Lean2Js.StepAgree.steps_of_run

(p : Core.Program) (m : Nat) (s : State) (r : Except Err Value) :

run p m s = r → r ≠ Except.error Err.outOfFuel → ∃ (n : Nat ), n < m ∧ steps p n s = State.done r

Used by

theorem

Lean2Js.StepAgree.run_of_steps

(p : Core.Program) (n : Nat) (s : State) (r : Except Err Value) :

steps p n s = State.done r → ∀ (m : Nat), n < m → run p m s = r

Used by

theorem

Lean2Js.StepAgree.stepCall_eventually

{p : Core.Program} {fn : String} {args : List Value} (hne : evalCall p fn args ≠ Except.error Err.outOfFuel) :

∃ (n : Nat ), ∀ (bound : Nat), n ≤ bound → stepCall p bound fn args = evalCall p fn args

Whenever eval gives an answer, the machine gives the same one once it is allowed enough steps.

Used by

theorem

Lean2Js.StepAgree.stepCall_refines

{p : Core.Program} {bound : Nat} {fn : String} {args : List Value} (hne : evalCall p fn args ≠ Except.error Err.outOfFuel) (hstep : stepCall p bound fn args ≠ Except.error Err.outOfFuel) :

stepCall p bound fn args = evalCall p fn args

The machine is deterministic, so an answer it gives within any bound is the one it settles on.

Used by

theorem

Lean2Js.StepAgree.stepCall_agrees

{p : Core.Program} {fn : String} {d : Core.Decl} {args : List Value} (hp : Cost.progOk p = true) (hfuel : Cost.cost p ≤ defaultFuel) (hd : p.find? fn = some d) (hpub : d.paramsCheckable = true) :

∃ (n : Nat ), ∀ (bound : Nat), n ≤ bound → stepCall p bound fn args = evalCall p fn args

For a program lean2js agrees to emit, the machine answers exactly as eval does, given enough steps, every call whose arguments the entry check can read.

Used by