Skip to content

Lean2Js.Cost

Imports 2

How much fuel a program can possibly need #

How much fuel a program can possibly need. Fuel counts the nesting of the expression being evaluated and the depth of the call stack, and nothing else: the traversals (evalArgs, evalMapItems and the four beside it) hand the rest of the list the same fuel they were given, so a longer array costs nothing.

That leaves the call stack, and the subset is built so that it cannot grow without end. A call from the declaration at index i lands on a declaration at an index below i -- directly, because callsPrecede refuses a call that does not go backwards, and through a function-typed parameter, because a function argument has to be a declared function named before the callee. So the depth is at most the number of declarations, and each level costs at most the deepest body in the program.

The conditions are collected in progOk, a Bool the emitter checks once per program rather than a hypothesis a caller has to discharge.

Depth #

The fuel one expression needs before any call is followed. evalExpr spends one on every node and hands f to each of the parts, so this is the height of the tree.

def

Lean2Js.Cost.exprDepth

:

Core.Expr → Nat

Equations

Lean2Js.Cost.exprDepth (Lean2Js.Core.Expr.lit l) = 1
Lean2Js.Cost.exprDepth (Lean2Js.Core.Expr.var name) = 1
Lean2Js.Cost.exprDepth (Lean2Js.Core.Expr.fnRef name) = 1
Lean2Js.Cost.exprDepth (Lean2Js.Core.Expr.noneE elem) = 1
Lean2Js.Cost.exprDepth (Lean2Js.Core.Expr.un op x_1) = 1 + Lean2Js.Cost.exprDepth x_1
Lean2Js.Cost.exprDepth (Lean2Js.Core.Expr.strUn op x_1) = 1 + Lean2Js.Cost.exprDepth x_1
Lean2Js.Cost.exprDepth x_1.someE = 1 + Lean2Js.Cost.exprDepth x_1
Lean2Js.Cost.exprDepth (Lean2Js.Core.Expr.okE err x_1) = 1 + Lean2Js.Cost.exprDepth x_1
Lean2Js.Cost.exprDepth (Lean2Js.Core.Expr.errorE ok x_1) = 1 + Lean2Js.Cost.exprDepth x_1
Lean2Js.Cost.exprDepth (x_1.proj field) = 1 + Lean2Js.Cost.exprDepth x_1
Lean2Js.Cost.exprDepth x_1.length = 1 + Lean2Js.Cost.exprDepth x_1
Lean2Js.Cost.exprDepth x_1.arrayReverse = 1 + Lean2Js.Cost.exprDepth x_1
Lean2Js.Cost.exprDepth x_1.dictKeys = 1 + Lean2Js.Cost.exprDepth x_1
Lean2Js.Cost.exprDepth x_1.dictValues = 1 + Lean2Js.Cost.exprDepth x_1
Lean2Js.Cost.exprDepth (Lean2Js.Core.Expr.bin op a b) = 1 + max (Lean2Js.Cost.exprDepth a) (Lean2Js.Cost.exprDepth b)
Lean2Js.Cost.exprDepth (Lean2Js.Core.Expr.strBin op a b) = 1 + max (Lean2Js.Cost.exprDepth a) (Lean2Js.Cost.exprDepth b)
Lean2Js.Cost.exprDepth (a.index b) = 1 + max (Lean2Js.Cost.exprDepth a) (Lean2Js.Cost.exprDepth b)
Lean2Js.Cost.exprDepth (a.dictGet b) = 1 + max (Lean2Js.Cost.exprDepth a) (Lean2Js.Cost.exprDepth b)
Lean2Js.Cost.exprDepth (a.dictHas b) = 1 + max (Lean2Js.Cost.exprDepth a) (Lean2Js.Cost.exprDepth b)
Lean2Js.Cost.exprDepth (a.dictDelete b) = 1 + max (Lean2Js.Cost.exprDepth a) (Lean2Js.Cost.exprDepth b)
Lean2Js.Cost.exprDepth (Lean2Js.Core.Expr.letE name ty a b) = 1 + max (Lean2Js.Cost.exprDepth a) (Lean2Js.Cost.exprDepth b)
Lean2Js.Cost.exprDepth (a.mapE binder b) = 1 + max (Lean2Js.Cost.exprDepth a) (Lean2Js.Cost.exprDepth b)
Lean2Js.Cost.exprDepth (a.filterE binder b) = 1 + max (Lean2Js.Cost.exprDepth a) (Lean2Js.Cost.exprDepth b)
Lean2Js.Cost.exprDepth (a.findE binder b) = 1 + max (Lean2Js.Cost.exprDepth a) (Lean2Js.Cost.exprDepth b)
Lean2Js.Cost.exprDepth (Lean2Js.Core.Expr.quantE op a binder b) = 1 + max (Lean2Js.Cost.exprDepth a) (Lean2Js.Cost.exprDepth b)
Lean2Js.Cost.exprDepth (a.sortByKeyE binder b) = 1 + max (Lean2Js.Cost.exprDepth a) (Lean2Js.Cost.exprDepth b)
Lean2Js.Cost.exprDepth (a.cond b c) = 1 + max (Lean2Js.Cost.exprDepth a) (max (Lean2Js.Cost.exprDepth b) (Lean2Js.Cost.exprDepth c))
Lean2Js.Cost.exprDepth (a.substring b c) = 1 + max (Lean2Js.Cost.exprDepth a) (max (Lean2Js.Cost.exprDepth b) (Lean2Js.Cost.exprDepth c))
Lean2Js.Cost.exprDepth (a.arraySlice b c) = 1 + max (Lean2Js.Cost.exprDepth a) (max (Lean2Js.Cost.exprDepth b) (Lean2Js.Cost.exprDepth c))
Lean2Js.Cost.exprDepth (a.dictSet b c) = 1 + max (Lean2Js.Cost.exprDepth a) (max (Lean2Js.Cost.exprDepth b) (Lean2Js.Cost.exprDepth c))
Lean2Js.Cost.exprDepth (a.reduceE b accName elemName c) = 1 + max (Lean2Js.Cost.exprDepth a) (max (Lean2Js.Cost.exprDepth b) (Lean2Js.Cost.exprDepth c))
Lean2Js.Cost.exprDepth (Lean2Js.Core.Expr.call fn args) = 1 + Lean2Js.Cost.exprDepthList args
Lean2Js.Cost.exprDepth (Lean2Js.Core.Expr.ctor typeName tyArgs ctorName args) = 1 + Lean2Js.Cost.exprDepthList args
Lean2Js.Cost.exprDepth (Lean2Js.Core.Expr.arrayLit elem args) = 1 + Lean2Js.Cost.exprDepthList args
Lean2Js.Cost.exprDepth (Lean2Js.Core.Expr.dictLit value obj entries) = 1 + Lean2Js.Cost.exprDepthEntries entries
Lean2Js.Cost.exprDepth (scrut.matchE alts) = 1 + max (Lean2Js.Cost.exprDepth scrut) (Lean2Js.Cost.exprDepthAlts alts)
Lean2Js.Cost.exprDepth (scrut.foldE typeName tyArgs result alts) = 1 + max (Lean2Js.Cost.exprDepth scrut) (Lean2Js.Cost.exprDepthAlts alts)

Instances For

Used by

def

Lean2Js.Cost.exprDepthList

:

List Core.Expr → Nat

Equations

Lean2Js.Cost.exprDepthList [] = 0
Lean2Js.Cost.exprDepthList (e :: rest) = max (Lean2Js.Cost.exprDepth e) (Lean2Js.Cost.exprDepthList rest)

Instances For

Used by

def

Lean2Js.Cost.exprDepthAlts

:

List Core.Alt → Nat

Equations

Lean2Js.Cost.exprDepthAlts [] = 0
Lean2Js.Cost.exprDepthAlts (a :: rest) = max (Lean2Js.Cost.exprDepth a.snd) (Lean2Js.Cost.exprDepthAlts rest)

Instances For

Used by

def

Lean2Js.Cost.exprDepthEntries

:

List (String × Core.Expr) → Nat

Equations

Lean2Js.Cost.exprDepthEntries [] = 0
Lean2Js.Cost.exprDepthEntries (e :: rest) = max (Lean2Js.Cost.exprDepth e.snd) (Lean2Js.Cost.exprDepthEntries rest)

Instances For

Used by

def

Lean2Js.Cost.maxBodyDepth

:

List Core.Decl → Nat

Equations

Lean2Js.Cost.maxBodyDepth [] = 0
Lean2Js.Cost.maxBodyDepth (d :: rest) = max (Lean2Js.Cost.exprDepth d.body) (Lean2Js.Cost.maxBodyDepth rest)

Instances For

Used by

def

Lean2Js.Cost.callStep

(p : Core.Program) :

What one level of the call stack costs: the deepest body, plus the node the call itself spends.

Equations

Lean2Js.Cost.callStep p = Lean2Js.Cost.maxBodyDepth p.decls + 1

Instances For

Used by

def

Lean2Js.Cost.cost

(p : Core.Program) :

The fuel no evaluation of this program can outrun: the deepest body, plus one level per declaration.

Equations

Lean2Js.Cost.cost p = Lean2Js.Cost.maxBodyDepth p.decls + p.decls.length * Lean2Js.Cost.callStep p

Instances For

Used by

Where a name is declared #

Program.find? answers with the declaration; the proof needs its position too, since that is what decreases at every call.

def

Lean2Js.Cost.declAtFrom

:

Nat → List Core.Decl → String → Option (Nat × Core.Decl)

Equations

Lean2Js.Cost.declAtFrom x✝¹ [] x✝ = none
Lean2Js.Cost.declAtFrom x✝¹ (d :: rest) x✝ = if (d.name == x✝) = true then some (x✝¹, d) else Lean2Js.Cost.declAtFrom (x✝¹ + 1) rest x✝

Instances For

Used by

def

Lean2Js.Cost.declAt?

(p : Core.Program) (name : String) :

Option (Nat × Core.Decl)

Equations

Lean2Js.Cost.declAt? p name = Lean2Js.Cost.declAtFrom 0 p.decls name

Instances For

Used by

def

Lean2Js.Cost.fnBefore

(p : Core.Program) (j : Nat) (g : String) :

Equations

Lean2Js.Cost.fnBefore p j g = match Lean2Js.Cost.declAt? p g with | some (k, snd) => decide (k < j) | none => false

Instances For

Used by

The conditions #

bodyOk is Compile.callsPrecede -- every call and function reference goes backwards -- together with the two restrictions that keep a function value from reaching a call site the check has not seen: a fnRef may only stand as an argument, and a function-typed parameter may only be called, never read.

The parameter it stands in for has to be function-typed, which is what makes the callee's environment say which of its names can hold a function at all.

def

Lean2Js.Cost.notFnRef

:

Core.Expr → Bool

Whether an argument is anything but a function reference. A function reference is the only shape a function-typed parameter may be given, and the only expression that answers with a function.

Equations

Lean2Js.Cost.notFnRef (Lean2Js.Core.Expr.fnRef name) = false
Lean2Js.Cost.notFnRef x✝ = true

Instances For

Used by

def

Lean2Js.Cost.argFnOk

(p : Core.Program) (j : Nat) (pm : Core.Param) :

Core.Expr → Bool

The condition on one argument of a call to the declaration at index j: a function reference has to stand at a function-typed parameter and name a declaration before j.

Equations

Lean2Js.Cost.argFnOk p j pm (Lean2Js.Core.Expr.fnRef name) = (pm.ty.isFn && Lean2Js.Cost.fnBefore p j name)
Lean2Js.Cost.argFnOk p j pm x✝ = true

Instances For

Used by

def

Lean2Js.Cost.fnRefArgsOk

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

List Core.Param → List Core.Expr → Bool

Equations

Lean2Js.Cost.fnRefArgsOk p j [] [] = true
Lean2Js.Cost.fnRefArgsOk p j (pm :: ps) (a :: rest) = (Lean2Js.Cost.argFnOk p j pm a && Lean2Js.Cost.fnRefArgsOk p j ps rest)
Lean2Js.Cost.fnRefArgsOk p j x✝¹ x✝ = false

Instances For

Used by

def

Lean2Js.Cost.bodyOk

(p : Core.Program) (i : Nat) (fns : List String) :

Core.Expr → Bool

fns are the names that may hold a function value: the function-typed parameters of the declaration whose body this is. A shadowed one stays in the list, so a body that rebinds such a name and reads the rebinding is refused; erasing it on the way in would take a binders walk over patterns to buy a program nobody writes.

Equations

One or more equations did not get rendered due to their size.
Lean2Js.Cost.bodyOk p i fns (Lean2Js.Core.Expr.lit l) = true
Lean2Js.Cost.bodyOk p i fns (Lean2Js.Core.Expr.noneE elem) = true
Lean2Js.Cost.bodyOk p i fns (Lean2Js.Core.Expr.var x_1) = !fns.contains x_1
Lean2Js.Cost.bodyOk p i fns (Lean2Js.Core.Expr.fnRef name) = false
Lean2Js.Cost.bodyOk p i fns (Lean2Js.Core.Expr.un op x_1) = Lean2Js.Cost.bodyOk p i fns x_1
Lean2Js.Cost.bodyOk p i fns (Lean2Js.Core.Expr.strUn op x_1) = Lean2Js.Cost.bodyOk p i fns x_1
Lean2Js.Cost.bodyOk p i fns x_1.someE = Lean2Js.Cost.bodyOk p i fns x_1
Lean2Js.Cost.bodyOk p i fns (Lean2Js.Core.Expr.okE err x_1) = Lean2Js.Cost.bodyOk p i fns x_1
Lean2Js.Cost.bodyOk p i fns (Lean2Js.Core.Expr.errorE ok x_1) = Lean2Js.Cost.bodyOk p i fns x_1
Lean2Js.Cost.bodyOk p i fns (x_1.proj field) = Lean2Js.Cost.bodyOk p i fns x_1
Lean2Js.Cost.bodyOk p i fns x_1.length = Lean2Js.Cost.bodyOk p i fns x_1
Lean2Js.Cost.bodyOk p i fns x_1.arrayReverse = Lean2Js.Cost.bodyOk p i fns x_1
Lean2Js.Cost.bodyOk p i fns x_1.dictKeys = Lean2Js.Cost.bodyOk p i fns x_1
Lean2Js.Cost.bodyOk p i fns x_1.dictValues = Lean2Js.Cost.bodyOk p i fns x_1
Lean2Js.Cost.bodyOk p i fns (Lean2Js.Core.Expr.bin op a b) = (Lean2Js.Cost.bodyOk p i fns a && Lean2Js.Cost.bodyOk p i fns b)
Lean2Js.Cost.bodyOk p i fns (Lean2Js.Core.Expr.strBin op a b) = (Lean2Js.Cost.bodyOk p i fns a && Lean2Js.Cost.bodyOk p i fns b)
Lean2Js.Cost.bodyOk p i fns (a.index b) = (Lean2Js.Cost.bodyOk p i fns a && Lean2Js.Cost.bodyOk p i fns b)
Lean2Js.Cost.bodyOk p i fns (a.dictGet b) = (Lean2Js.Cost.bodyOk p i fns a && Lean2Js.Cost.bodyOk p i fns b)
Lean2Js.Cost.bodyOk p i fns (a.dictHas b) = (Lean2Js.Cost.bodyOk p i fns a && Lean2Js.Cost.bodyOk p i fns b)
Lean2Js.Cost.bodyOk p i fns (a.dictDelete b) = (Lean2Js.Cost.bodyOk p i fns a && Lean2Js.Cost.bodyOk p i fns b)
Lean2Js.Cost.bodyOk p i fns (Lean2Js.Core.Expr.letE name ty a b) = (Lean2Js.Cost.bodyOk p i fns a && Lean2Js.Cost.bodyOk p i fns b)
Lean2Js.Cost.bodyOk p i fns (a.mapE binder b) = (Lean2Js.Cost.bodyOk p i fns a && Lean2Js.Cost.bodyOk p i fns b)
Lean2Js.Cost.bodyOk p i fns (a.filterE binder b) = (Lean2Js.Cost.bodyOk p i fns a && Lean2Js.Cost.bodyOk p i fns b)
Lean2Js.Cost.bodyOk p i fns (a.findE binder b) = (Lean2Js.Cost.bodyOk p i fns a && Lean2Js.Cost.bodyOk p i fns b)
Lean2Js.Cost.bodyOk p i fns (Lean2Js.Core.Expr.quantE op a binder b) = (Lean2Js.Cost.bodyOk p i fns a && Lean2Js.Cost.bodyOk p i fns b)
Lean2Js.Cost.bodyOk p i fns (a.sortByKeyE binder b) = (Lean2Js.Cost.bodyOk p i fns a && Lean2Js.Cost.bodyOk p i fns b)
Lean2Js.Cost.bodyOk p i fns (a.cond b c) = (Lean2Js.Cost.bodyOk p i fns a && Lean2Js.Cost.bodyOk p i fns b && Lean2Js.Cost.bodyOk p i fns c)
Lean2Js.Cost.bodyOk p i fns (a.substring b c) = (Lean2Js.Cost.bodyOk p i fns a && Lean2Js.Cost.bodyOk p i fns b && Lean2Js.Cost.bodyOk p i fns c)
Lean2Js.Cost.bodyOk p i fns (a.arraySlice b c) = (Lean2Js.Cost.bodyOk p i fns a && Lean2Js.Cost.bodyOk p i fns b && Lean2Js.Cost.bodyOk p i fns c)
Lean2Js.Cost.bodyOk p i fns (a.dictSet b c) = (Lean2Js.Cost.bodyOk p i fns a && Lean2Js.Cost.bodyOk p i fns b && Lean2Js.Cost.bodyOk p i fns c)
Lean2Js.Cost.bodyOk p i fns (a.reduceE b accName elemName c) = (Lean2Js.Cost.bodyOk p i fns a && Lean2Js.Cost.bodyOk p i fns b && Lean2Js.Cost.bodyOk p i fns c)
Lean2Js.Cost.bodyOk p i fns (Lean2Js.Core.Expr.ctor typeName tyArgs ctorName args) = Lean2Js.Cost.bodyOkList p i fns args
Lean2Js.Cost.bodyOk p i fns (Lean2Js.Core.Expr.arrayLit elem args) = Lean2Js.Cost.bodyOkList p i fns args
Lean2Js.Cost.bodyOk p i fns (Lean2Js.Core.Expr.dictLit value obj entries) = Lean2Js.Cost.bodyOkEntries p i fns entries
Lean2Js.Cost.bodyOk p i fns (scrut.matchE alts) = (Lean2Js.Cost.bodyOk p i fns scrut && Lean2Js.Cost.bodyOkAlts p i fns alts)
Lean2Js.Cost.bodyOk p i fns (scrut.foldE typeName tyArgs result alts) = (Lean2Js.Cost.bodyOk p i fns scrut && Lean2Js.Cost.bodyOkAlts p i fns alts)

Instances For

Used by

def

Lean2Js.Cost.bodyOkList

(p : Core.Program) (i : Nat) (fns : List String) :

List Core.Expr → Bool

Equations

Lean2Js.Cost.bodyOkList p i fns [] = true
Lean2Js.Cost.bodyOkList p i fns (e :: rest) = (Lean2Js.Cost.bodyOk p i fns e && Lean2Js.Cost.bodyOkList p i fns rest)

Instances For

Used by

def

Lean2Js.Cost.bodyOkArgs

(p : Core.Program) (i : Nat) (fns : List String) :

List Core.Expr → Bool

Equations

Lean2Js.Cost.bodyOkArgs p i fns [] = true
Lean2Js.Cost.bodyOkArgs p i fns (e :: rest) = ((!Lean2Js.Cost.notFnRef e || Lean2Js.Cost.bodyOk p i fns e) && Lean2Js.Cost.bodyOkArgs p i fns rest)

Instances For

Used by

def

Lean2Js.Cost.bodyOkAlts

(p : Core.Program) (i : Nat) (fns : List String) :

List Core.Alt → Bool

Equations

Lean2Js.Cost.bodyOkAlts p i fns [] = true
Lean2Js.Cost.bodyOkAlts p i fns (a :: rest) = (Lean2Js.Cost.bodyOk p i fns a.snd && Lean2Js.Cost.bodyOkAlts p i fns rest)

Instances For

Used by

def

Lean2Js.Cost.bodyOkEntries

(p : Core.Program) (i : Nat) (fns : List String) :

List (String × Core.Expr) → Bool

Equations

Lean2Js.Cost.bodyOkEntries p i fns [] = true
Lean2Js.Cost.bodyOkEntries p i fns (e :: rest) = (Lean2Js.Cost.bodyOk p i fns e.snd && Lean2Js.Cost.bodyOkEntries p i fns rest)

Instances For

Used by

def

Lean2Js.Cost.declFns

(d : Core.Decl) :

Equations

Lean2Js.Cost.declFns d = List.filterMap (fun (pm : Lean2Js.Core.Param) => if pm.ty.isFn = true then some pm.name else none) d.params

Instances For

Used by

def

Lean2Js.Cost.declsOk

(p : Core.Program) :

Nat → List Core.Decl → Bool

Equations

Lean2Js.Cost.declsOk p x✝ [] = true
Lean2Js.Cost.declsOk p x✝ (d :: rest) = (Lean2Js.Cost.bodyOk p x✝ (Lean2Js.Cost.declFns d) d.body && Lean2Js.Cost.declsOk p (x✝ + 1) rest)

Instances For

Used by

def

Lean2Js.Cost.tyFirstOrder

:

Core.Ty → Bool

A type with no function in it. The entry check is what fixes the shape of the arguments a public function starts with, and it can only rule out a function value where the type cannot hide one.

Equations

Instances For

Used by

def

Lean2Js.Cost.tyFirstOrderList

:

List Core.Ty → Bool

Equations

Lean2Js.Cost.tyFirstOrderList [] = true
Lean2Js.Cost.tyFirstOrderList (t :: rest) = (Lean2Js.Cost.tyFirstOrder t && Lean2Js.Cost.tyFirstOrderList rest)

Instances For

Used by

def

Lean2Js.Cost.typesFirstOrder

(p : Core.Program) :

The declared field types the entry check walks into. A function value can only be turned away where the type it is checked against cannot hide one.

Equations

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

Instances For

Used by

def

Lean2Js.Cost.paramTyOk

(ty : Core.Ty) :

A function type is allowed on a parameter and nowhere inside one, which is Compile.wfParamTy.

Equations

Lean2Js.Cost.paramTyOk (Lean2Js.Core.Ty.fn params ret) = (Lean2Js.Cost.tyFirstOrderList params && Lean2Js.Cost.tyFirstOrder ret)
Lean2Js.Cost.paramTyOk ty = Lean2Js.Cost.tyFirstOrder ty

Instances For

Used by

def

Lean2Js.Cost.declParamsOk

(d : Core.Decl) :

Equations

Lean2Js.Cost.declParamsOk d = d.params.all fun (pm : Lean2Js.Core.Param) => Lean2Js.Cost.paramTyOk pm.ty

Instances For

Used by

def

Lean2Js.Cost.progOk

(p : Core.Program) :

Everything the fuel bound rests on, as one Bool the emitter runs once per program.

Equations

Lean2Js.Cost.progOk p = (Lean2Js.Cost.declsOk p 0 p.decls && p.decls.all Lean2Js.Cost.declParamsOk && Lean2Js.Cost.typesFirstOrder p)

Instances For

Used by

Function values #

The invariant the proof carries: a function value is only ever bound to a function-typed parameter, and the declaration it names comes before the one whose body is running. Nothing else in a value is a function, which is what keeps a function from being smuggled into a call through an array.

def

Lean2Js.Cost.noFn

:

Equations

Lean2Js.Cost.noFn (Lean2Js.Value.bool b) = true
Lean2Js.Cost.noFn (Lean2Js.Value.int53 i) = true
Lean2Js.Cost.noFn (Lean2Js.Value.uint32 n) = true
Lean2Js.Cost.noFn (Lean2Js.Value.str s) = true
Lean2Js.Cost.noFn (Lean2Js.Value.bigint i) = true
Lean2Js.Cost.noFn (Lean2Js.Value.obj ctor fields) = Lean2Js.Cost.noFnFields fields
Lean2Js.Cost.noFn (Lean2Js.Value.arr xs) = Lean2Js.Cost.noFnList xs
Lean2Js.Cost.noFn (Lean2Js.Value.dict entries) = Lean2Js.Cost.noFnFields entries
Lean2Js.Cost.noFn (Lean2Js.Value.fn name) = false

Instances For

Used by

def

Lean2Js.Cost.noFnList

:

List Value → Bool

Equations

Lean2Js.Cost.noFnList [] = true
Lean2Js.Cost.noFnList (v :: rest) = (Lean2Js.Cost.noFn v && Lean2Js.Cost.noFnList rest)

Instances For

Used by

def

Lean2Js.Cost.noFnFields

:

List (String × Value) → Bool

Equations

Lean2Js.Cost.noFnFields [] = true
Lean2Js.Cost.noFnFields (e :: rest) = (Lean2Js.Cost.noFn e.snd && Lean2Js.Cost.noFnFields rest)

Instances For

Used by

def

Lean2Js.Cost.EnvOk

(p : Core.Program) (i : Nat) (fns : List String) (env : Env) :

Equations

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

Instances For

Used by

Reading a declaration's position back #

theorem

Lean2Js.Cost.declAtFrom_find

(name : String) (ds : List Core.Decl) (k j : Nat) (d : Core.Decl) :

declAtFrom k ds name = some (j, d) → List.find? (fun (x : Core.Decl) => x.name == name) ds = some d

Used by

theorem

Lean2Js.Cost.declAt?_find

{p : Core.Program} {g : String} {k : Nat} {d : Core.Decl} (h : declAt? p g = some (k, d)) :

p.find? g = some d

Used by

theorem

Lean2Js.Cost.declAtFrom_depth

(name : String) (ds : List Core.Decl) (k j : Nat) (d : Core.Decl) :

declAtFrom k ds name = some (j, d) → exprDepth d.body ≤ maxBodyDepth ds

Used by

theorem

Lean2Js.Cost.declAt?_depth

{p : Core.Program} {g : String} {k : Nat} {d : Core.Decl} (h : declAt? p g = some (k, d)) :

exprDepth d.body ≤ maxBodyDepth p.decls

Used by

theorem

Lean2Js.Cost.declAtFrom_lt

(name : String) (ds : List Core.Decl) (k j : Nat) (d : Core.Decl) :

declAtFrom k ds name = some (j, d) → j < k + ds.length

Used by

theorem

Lean2Js.Cost.declAt?_lt

{p : Core.Program} {g : String} {k : Nat} {d : Core.Decl} (h : declAt? p g = some (k, d)) :

k < p.decls.length

Used by

theorem

Lean2Js.Cost.declsOkFrom_bodyOk

(p : Core.Program) (name : String) (ds : List Core.Decl) (base k : Nat) (d : Core.Decl) :

declsOk p base ds = true → declAtFrom base ds name = some (k, d) → bodyOk p k (declFns d) d.body = true

Used by

theorem

Lean2Js.Cost.declAt?_bodyOk

{p : Core.Program} {g : String} {k : Nat} {d : Core.Decl} (hp : declsOk p 0 p.decls = true) (h : declAt? p g = some (k, d)) :

bodyOk p k (declFns d) d.body = true

Used by

Values that hold no function #

theorem

Lean2Js.Cost.except_bind_ok

{α β : Type} {m : Except Err α} {k : α → Except Err β} {v : β} (h : m >>= k = Except.ok v) :

∃ (c : α), m = Except.ok c ∧ k c = Except.ok v

Used by

theorem

Lean2Js.Cost.except_bind_ne

{α β : Type} {m : Except Err α} {k : α → Except Err β} {e : Err} (hm : m ≠ Except.error e) (hk : ∀ (c : α), k c ≠ Except.error e) :

m >>= k ≠ Except.error e

Used by

theorem

Lean2Js.Cost.noFnList_iff

(xs : List Value) :

noFnList xs = true ↔ ∀ (v : Value), v ∈ xs → noFn v = true

Used by

theorem

Lean2Js.Cost.noFnFields_iff

(es : List (String × Value)) :

noFnFields es = true ↔ ∀ (e : String × Value), e ∈ es → noFn e.snd = true

Used by

theorem

Lean2Js.Cost.noFn_arr

{xs : List Value} (h : ∀ (v : Value), v ∈ xs → noFn v = true) :

noFn (Value.arr xs) = true

Used by

theorem

Lean2Js.Cost.noFn_lookupFieldV

{fields : List (String × Value)} {k : String} {v : Value} (h : ∀ (e : String × Value), e ∈ fields → noFn e.snd = true) (hl : lookupFieldV fields k = some v) :

Used by

theorem

Lean2Js.Cost.noFn_obj

{c : String} {fs : List (String × Value)} (h : ∀ (e : String × Value), e ∈ fs → noFn e.snd = true) :

noFn (Value.obj c fs) = true

Used by

theorem

Lean2Js.Cost.noFn_dict

{es : List (String × Value)} (h : ∀ (e : String × Value), e ∈ es → noFn e.snd = true) :

noFn (Value.dict es) = true

Used by

theorem

Lean2Js.Cost.arr_noFn

{xs : List Value} (h : noFn (Value.arr xs) = true) (v : Value) :

v ∈ xs → noFn v = true

Used by

theorem

Lean2Js.Cost.obj_noFn

{c : String} {fs : List (String × Value)} (h : noFn (Value.obj c fs) = true) (e : String × Value) :

e ∈ fs → noFn e.snd = true

Used by

theorem

Lean2Js.Cost.dict_noFn

{es : List (String × Value)} (h : noFn (Value.dict es) = true) (e : String × Value) :

e ∈ es → noFn e.snd = true

Used by

theorem

Lean2Js.Cost.noFn_litValue

(l : Core.Lit) :

noFn (litValue l) = true

Used by

theorem

Lean2Js.Cost.noFn_mkInt53

{i : Int} {v : Value} (h : mkInt53 i = Except.ok v) :

Used by

theorem

Lean2Js.Cost.noFn_applyUn

{op : Core.UnOp} {x v : Value} (h : applyUn op x = Except.ok v) :

Used by

theorem

Lean2Js.Cost.noFn_applyArith

{op : Core.BinOp} {a b v : Value} (h : applyArith op a b = Except.ok v) :

Used by

theorem

Lean2Js.Cost.noFn_compareValues

{op : Core.BinOp} {a b v : Value} (h : compareValues op a b = Except.ok v) :

Used by

theorem

Lean2Js.Cost.noFn_applyMinMax

{op : Core.BinOp} {a b v : Value} (hn : noFn a = true) (hm : noFn b = true) (h : applyMinMax op a b = Except.ok v) :

Used by

theorem

Lean2Js.Cost.noFn_applyBin

{op : Core.BinOp} {a b v : Value} (hn : noFn a = true) (hm : noFn b = true) (h : applyBin op a b = Except.ok v) :

Used by

theorem

Lean2Js.Cost.noFn_applyStrUn

{op : Core.StrUnOp} {x v : Value} (h : applyStrUn op x = Except.ok v) :

Used by

theorem

Lean2Js.Cost.noFn_applyStrBin

{op : Core.StrBinOp} {a b v : Value} (h : applyStrBin op a b = Except.ok v) :

Used by

theorem

Lean2Js.Cost.noFn_sliceStr

{s lo hi v : Value} (h : sliceStr s lo hi = Except.ok v) :

Used by

theorem

Lean2Js.Cost.noFn_sliceArr

{a lo hi v : Value} (hn : noFn a = true) (h : sliceArr a lo hi = Except.ok v) :

Used by

theorem

Lean2Js.Cost.noFn_asBool

{x v : Value} (h : asBool x = Except.ok v) :

Used by

theorem

Lean2Js.Cost.noFn_dictLookup

{entries : List (String × Value)} {k : String} (h : ∀ (e : String × Value), e ∈ entries → noFn e.snd = true) :

noFn (dictLookup entries k) = true

Used by

theorem

Lean2Js.Cost.noFn_dictWith

{entries : List (String × Value)} {k : String} {v : Value} (h : ∀ (e : String × Value), e ∈ entries → noFn e.snd = true) (hv : noFn v = true) (e : String × Value) :

e ∈ dictWith entries k v → noFn e.snd = true

Used by

Running without running out #

Safe r P is the pair of facts the induction carries: r is not what running out of fuel looks like, and if it answered, the answer holds no function. Both travel through do the same way, so every case is one Safe.bind' per part.

def

Lean2Js.Cost.Safe

{α : Type} (r : Except Err α) (P : α → Prop) :

Equations

Lean2Js.Cost.Safe r P = (r ≠ Except.error Lean2Js.Err.outOfFuel ∧ ∀ (v : α), r = Except.ok v → P v)

Instances For

Used by

theorem

Lean2Js.Cost.Safe.ok'

{α : Type} {v : α} {P : α → Prop} (h : P v) :

Safe (Except.ok v) P

Used by

theorem

Lean2Js.Cost.Safe.err

{α : Type} {e : Err} {P : α → Prop} (h : e ≠ Err.outOfFuel) :

Safe (Except.error e) P

Used by

theorem

Lean2Js.Cost.Safe.bind'

{α β : Type} {m : Except Err α} {k : α → Except Err β} {P : α → Prop} {Q : β → Prop} (hm : Safe m P) (hk : ∀ (c : α), P c → Safe (k c) Q) :

Safe (m >>= k) Q

Used by

theorem

Lean2Js.Cost.Safe.weaken

{α : Type} {r : Except Err α} {P Q : α → Prop} (h : Safe r P) (hpq : ∀ (v : α), P v → Q v) :

Safe r Q

Used by

theorem

Lean2Js.Cost.safe_mkInt53

(x : Int) :

Safe (mkInt53 x) fun (v : Value) => noFn v = true

Used by

theorem

Lean2Js.Cost.safe_applyUn

(op : Core.UnOp) (x : Value) :

Safe (applyUn op x) fun (v : Value) => noFn v = true

Used by

theorem

Lean2Js.Cost.safe_applyArith

(op : Core.BinOp) (a b : Value) :

Safe (applyArith op a b) fun (v : Value) => noFn v = true

Used by

theorem

Lean2Js.Cost.safe_compareValues

(op : Core.BinOp) (a b : Value) :

Safe (compareValues op a b) fun (v : Value) => noFn v = true

Used by

theorem

Lean2Js.Cost.safe_applyMinMax

(op : Core.BinOp) (a b : Value) (hn : noFn a = true) (hm : noFn b = true) :

Safe (applyMinMax op a b) fun (v : Value) => noFn v = true

Used by

theorem

Lean2Js.Cost.safe_applyBin

(op : Core.BinOp) (a b : Value) (hn : noFn a = true) (hm : noFn b = true) :

Safe (applyBin op a b) fun (v : Value) => noFn v = true

Used by

theorem

Lean2Js.Cost.safe_applyStrUn

(op : Core.StrUnOp) (x : Value) :

Safe (applyStrUn op x) fun (v : Value) => noFn v = true

Used by

theorem

Lean2Js.Cost.safe_applyStrBin

(op : Core.StrBinOp) (a b : Value) :

Safe (applyStrBin op a b) fun (v : Value) => noFn v = true

Used by

theorem

Lean2Js.Cost.safe_sliceStr

(s lo hi : Value) :

Safe (sliceStr s lo hi) fun (v : Value) => noFn v = true

Used by

theorem

Lean2Js.Cost.safe_sliceArr

(a lo hi : Value) (hn : noFn a = true) :

Safe (sliceArr a lo hi) fun (v : Value) => noFn v = true

Used by

theorem

Lean2Js.Cost.safe_asBool

(x : Value) :

Safe (asBool x) fun (v : Value) => noFn v = true

Used by

Environments #

theorem

Lean2Js.Cost.lookup_cons

(x : String) (w : Value) (env : Env) (y : String) :

Env.lookup? ((x, w) :: env) y = if (x == y) = true then some w else env.lookup? y

Used by

theorem

Lean2Js.Cost.lookup_append_cases

(b env : Env) (y : String) (u : Value) :

(b ++ env).lookup? y = some u → b.lookup? y = some u ∨ env.lookup? y = some u

Used by

theorem

Lean2Js.Cost.lookup_noFn

{env : Env} (h : ∀ (e : String × Value), e ∈ env → noFn e.snd = true) {x : String} {w : Value} (hx : env.lookup? x = some w) :

Used by

theorem

Lean2Js.Cost.envOk_cons

{p : Core.Program} {i : Nat} {fns : List String} {x : String} {w : Value} {env : Env} (hw : noFn w = true) (he : EnvOk p i fns env) :

EnvOk p i fns ((x, w) :: env)

Used by

theorem

Lean2Js.Cost.envOk_append

{p : Core.Program} {i : Nat} {fns : List String} {b env : Env} (hb : ∀ (e : String × Value), e ∈ b → noFn e.snd = true) (he : EnvOk p i fns env) :

EnvOk p i fns (b ++ env)

Used by

What a pattern binds #

theorem

Lean2Js.Cost.matchPat_noFn

{pat : Core.Pat} {v : Value} {binds : Env} :

noFn v = true → matchPat pat v = some binds → ∀ (e : String × Value), e ∈ binds → noFn e.snd = true

Used by

theorem

Lean2Js.Cost.matchPats_noFn

{pats : List Core.Pat} {vs : List Value} {binds : Env} :

(∀ (v : Value), v ∈ vs → noFn v = true) → matchPats pats vs = some binds → ∀ (e : String × Value), e ∈ binds → noFn e.snd = true

Used by

theorem

Lean2Js.Cost.firstMatch_noFn

{alts : List Core.Alt} {sv : Value} {binds : Env} {body : Core.Expr} (hv : noFn sv = true) (h : firstMatch alts sv = some (binds, body)) (e : String × Value) :

e ∈ binds → noFn e.snd = true

Used by

theorem

Lean2Js.Cost.firstMatch_body

{alts : List Core.Alt} {sv : Value} {binds : Env} {body : Core.Expr} (h : firstMatch alts sv = some (binds, body)) :

∃ (alt : Core.Alt ), alt ∈ alts ∧ body = alt.snd

Used by

Reading the checks back #

theorem

Lean2Js.Cost.exprDepth_pos

(e : Core.Expr) :

1 ≤ exprDepth e

Used by

theorem

Lean2Js.Cost.exprDepthList_mem

{es : List Core.Expr} {e : Core.Expr} :

e ∈ es → exprDepth e ≤ exprDepthList es

Used by

theorem

Lean2Js.Cost.exprDepthAlts_mem

{as : List Core.Alt} {a : Core.Alt} :

a ∈ as → exprDepth a.snd ≤ exprDepthAlts as

Used by

theorem

Lean2Js.Cost.exprDepthEntries_mem

{es : List (String × Core.Expr)} {e : String × Core.Expr} :

e ∈ es → exprDepth e.snd ≤ exprDepthEntries es

Used by

theorem

Lean2Js.Cost.bodyOkAlts_mem

{p : Core.Program} {i : Nat} {fns : List String} {as : List Core.Alt} {a : Core.Alt} :

bodyOkAlts p i fns as = true → a ∈ as → bodyOk p i fns a.snd = true

Used by

theorem

Lean2Js.Cost.declAtFrom_none

(name : String) (ds : List Core.Decl) (k : Nat) :

declAtFrom k ds name = none → List.find? (fun (x : Core.Decl) => x.name == name) ds = none

Used by

theorem

Lean2Js.Cost.declAt?_none

{p : Core.Program} {g : String} (h : declAt? p g = none) :

p.find? g = none

Used by

theorem

Lean2Js.Cost.fnBefore_inv

{p : Core.Program} {j : Nat} {g : String} (h : fnBefore p j g = true) :

∃ (k : Nat ), ∃ (d : Core.Decl ), declAt? p g = some (k, d) ∧ k < j

Used by

The value a call binds to a parameter #

def

Lean2Js.Cost.ArgVal

(p : Core.Program) (j : Nat) (isFnP : Bool) (v : Value) :

Equations

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

Instances For

Used by

def

Lean2Js.Cost.ArgsVals

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

List Core.Param → List Value → Prop

Equations

Lean2Js.Cost.ArgsVals p j (pm :: ps) (v :: vs) = (Lean2Js.Cost.ArgVal p j pm.ty.isFn v ∧ Lean2Js.Cost.ArgsVals p j ps vs)
Lean2Js.Cost.ArgsVals p j x✝¹ x✝ = True

Instances For

Used by

theorem

Lean2Js.Cost.bindParams_nil_left

(vs : List Value) :

bindParams [] vs = []

Used by

theorem

Lean2Js.Cost.bindParams_nil_right

(ps : List Core.Param) :

bindParams ps [] = []

Used by

theorem

Lean2Js.Cost.fnRefArgsOk_nil_cons

(p : Core.Program) (j : Nat) (a : Core.Expr) (rest : List Core.Expr) :

fnRefArgsOk p j [] (a :: rest) = false

Used by

theorem

Lean2Js.Cost.fnRefArgsOk_cons

(p : Core.Program) (j : Nat) (pm : Core.Param) (ps : List Core.Param) (a : Core.Expr) (rest : List Core.Expr) :

fnRefArgsOk p j (pm :: ps) (a :: rest) = (argFnOk p j pm a && fnRefArgsOk p j ps rest)

Used by

theorem

Lean2Js.Cost.bodyOkArgs_cons

(p : Core.Program) (i : Nat) (fns : List String) (a : Core.Expr) (rest : List Core.Expr) :

bodyOkArgs p i fns (a :: rest) = ((!notFnRef a || bodyOk p i fns a) && bodyOkArgs p i fns rest)

Used by

theorem

Lean2Js.Cost.argsVals_nil_right

(p : Core.Program) (j : Nat) (ps : List Core.Param) :

ArgsVals p j ps []

Used by

theorem

Lean2Js.Cost.envOk_bindParams

(p : Core.Program) (j : Nat) (fns : List String) (ps : List Core.Param) (vs : List Value) :

ArgsVals p j ps vs → (∀ (pm : Core.Param), pm ∈ ps → pm.ty.isFn = true → fns.contains pm.name = true) → EnvOk p j fns (bindParams ps vs)

Used by

theorem

Lean2Js.Cost.declFns_mem

{d : Core.Decl} (pm : Core.Param) :

pm ∈ d.params → pm.ty.isFn = true → (declFns d).contains pm.name = true

Used by

theorem

Lean2Js.Cost.bindParams_mem

(ps : List Core.Param) (vs : List Value) (e : String × Value) :

e ∈ bindParams ps vs → e.snd ∈ vs

Used by

theorem

Lean2Js.Cost.envOk_of_noFn

{p : Core.Program} {i : Nat} {fns : List String} {env : Env} (h : ∀ (e : String × Value), e ∈ env → noFn e.snd = true) :

EnvOk p i fns env

Used by

theorem

Lean2Js.Cost.calleeOf_cases

(env : Env) (fn : String) :

(∃ (g : String ), env.lookup? fn = some (Value.fn g) ∧ calleeOf env fn = g) ∨ calleeOf env fn = fn

Used by

theorem

Lean2Js.Cost.safe_typeError

{α : Type} {P : α → Prop} (msg : String) :

Safe (Except.error (Err.typeError msg)) P

Used by

theorem

Lean2Js.Cost.safe_unknownVar

{α : Type} {P : α → Prop} (name : String) :

Safe (Except.error (Err.unknownVar name)) P

Used by

theorem

Lean2Js.Cost.safe_unknownFn

{α : Type} {P : α → Prop} (name : String) :

Safe (Except.error (Err.unknownFn name)) P

Used by

theorem

Lean2Js.Cost.safe_arity

{α : Type} {P : α → Prop} (name : String) :

Safe (Except.error (Err.arity name)) P

Used by

theorem

Lean2Js.Cost.safe_indexOutOfBounds

{α : Type} {P : α → Prop} :

Safe (Except.error Err.indexOutOfBounds) P

Used by

theorem

Lean2Js.Cost.safe_noMatch

{α : Type} {P : α → Prop} :

Safe (Except.error Err.noMatchingAlternative) P

Used by

theorem

Lean2Js.Cost.noFn_wrap

{c k : String} {v : Value} (h : noFn v = true) :

noFn (Value.obj c [(k, v)]) = true

Used by

theorem

Lean2Js.Cost.zip_snd_mem

{α β : Type} (as : List α) (bs : List β) (e : α × β) :

e ∈ as.zip bs → e.snd ∈ bs

Used by

theorem

Lean2Js.Cost.getElem?_mem

{α : Type} (l : List α) (k : Nat) (a : α) :

l[k]? = some a → a ∈ l

Used by

theorem

Lean2Js.Cost.bodyOkEntries_map

{p : Core.Program} {i : Nat} {fns : List String} {es : List (String × Core.Expr)} :

bodyOkEntries p i fns es = true → bodyOkList p i fns (List.map (fun (x : String × Core.Expr) => x.snd) es) = true

Used by

theorem

Lean2Js.Cost.exprDepthEntries_map

(es : List (String × Core.Expr)) :

exprDepthList (List.map (fun (x : String × Core.Expr) => x.snd) es) = exprDepthEntries es

Used by

theorem

Lean2Js.Cost.bodyOkArg_not_fnRef

{p : Core.Program} {i : Nat} {fns : List String} {a : Core.Expr} (h : (!notFnRef a || bodyOk p i fns a) = true) (hnf : notFnRef a = true) :

bodyOk p i fns a = true

Used by

theorem

Lean2Js.Cost.safe_arg

{p : Core.Program} {j n : Nat} {env : Env} {pm : Core.Param} {a : Core.Expr} (hok : argFnOk p j pm a = true) (hsafe : notFnRef a = true → Safe (evalExpr p n env a) fun (v : Value) => noFn v = true) (hn : 0 < n) :

Safe (evalExpr p n env a) fun (v : Value) => ArgVal p j pm.ty.isFn v

Used by

theorem

Lean2Js.Cost.eval_safe

(p : Core.Program) (hp : declsOk p 0 p.decls = true) (f i : Nat) (fns : List String) (env : Env) (e : Core.Expr) :

bodyOk p i fns e = true → EnvOk p i fns env → exprDepth e + i * callStep p ≤ f → Safe (evalExpr p f env e) fun (v : Value) => noFn v = true

Enough fuel and the reference semantics never runs out of it, and the answer it gives holds no function value. The induction is on the fuel, so a call is reached at a strictly smaller one; what makes that terminate is the index of the declaration being entered, which bodyOk keeps going down.

Used by

The arguments a public function starts with #

evalCall lets a value into the body only if it has the declared type. That is what rules a function value out at the entry -- but only where the type cannot hide one, which is why progOk asks the declared field types to be first order too.

theorem

Lean2Js.Cost.tyFirstOrder_subst

(sigma : List (String × Core.Ty)) (hs : ∀ (e : String × Core.Ty), e ∈ sigma → tyFirstOrder e.snd = true) (t : Core.Ty) :

tyFirstOrder t = true → tyFirstOrder (Core.Ty.subst sigma t) = true

Used by

theorem

Lean2Js.Cost.tyFirstOrderList_subst

(sigma : List (String × Core.Ty)) (hs : ∀ (e : String × Core.Ty), e ∈ sigma → tyFirstOrder e.snd = true) (ts : List Core.Ty) :

tyFirstOrderList ts = true → tyFirstOrderList (Core.Ty.substArgs sigma ts) = true

Used by

theorem

Lean2Js.Cost.tyFirstOrderList_mem

{ts : List Core.Ty} {t : Core.Ty} :

tyFirstOrderList ts = true → t ∈ ts → tyFirstOrder t = true

Used by

theorem

Lean2Js.Cost.ctorAt_field_firstOrder

{n : String} {p : Core.Program} {t : Core.TypeDef} {args : List Core.Ty} {ctor : String} {c : Core.CtorDef} {f : Core.Field} (ht : typesFirstOrder p = true) (hty : p.findType? n = some t) (hargs : tyFirstOrderList args = true) (hc : t.findAt? args ctor = some c) (hf : f ∈ c.fields) :

tyFirstOrder f.ty = true

Used by

theorem

Lean2Js.Cost.hasTy_noFn

{p : Core.Program} (ht : typesFirstOrder p = true) (v : Value) (ty : Core.Ty) :

tyFirstOrder ty = true → Value.hasTy p v ty = true → noFn v = true

Used by

theorem

Lean2Js.Cost.hasFieldTys_noFn

{p : Core.Program} (ht : typesFirstOrder p = true) (fields : List (String × Value)) (tys : List (String × Core.Ty)) :

(∀ (e : String × Core.Ty), e ∈ tys → tyFirstOrder e.snd = true) → Value.hasFieldTys p fields tys = true → ∀ (e : String × Value), e ∈ fields → noFn e.snd = true

Used by

theorem

Lean2Js.Cost.hasElemTy_noFn

{p : Core.Program} (ht : typesFirstOrder p = true) (xs : List Value) (elem : Core.Ty) :

tyFirstOrder elem = true → Value.hasElemTy p xs elem = true → ∀ (w : Value), w ∈ xs → noFn w = true

Used by

theorem

Lean2Js.Cost.hasEntryTys_noFn

{p : Core.Program} (ht : typesFirstOrder p = true) (es : List (String × Value)) (elem : Core.Ty) :

tyFirstOrder elem = true → Value.hasEntryTys p es elem = true → ∀ (e : String × Value), e ∈ es → noFn e.snd = true

Used by

What the shipped fuel buys #

theorem

Lean2Js.Cost.declAtFrom_of_find

(name : String) (ds : List Core.Decl) (k : Nat) (d : Core.Decl) :

List.find? (fun (x : Core.Decl) => x.name == name) ds = some d → ∃ (j : Nat ), declAtFrom k ds name = some (j, d)

Used by

theorem

Lean2Js.Cost.declAt?_of_find

{p : Core.Program} {name : String} {d : Core.Decl} (h : p.find? name = some d) :

∃ (j : Nat ), declAt? p name = some (j, d)

Used by

theorem

Lean2Js.Cost.paramTyOk_firstOrder

{ty : Core.Ty} (h : paramTyOk ty = true) (hn : ty.isFn = false) :

tyFirstOrder ty = true

Used by

theorem

Lean2Js.Cost.bindParams_noFn

{p : Core.Program} (ht : typesFirstOrder p = true) (ps : List Core.Param) (vs : List Value) :

(∀ (pm : Core.Param), pm ∈ ps → tyFirstOrder pm.ty = true) → ((ps.zip vs).all fun (x : Core.Param × Value) => match x with | (param, v) => Value.hasTy p v param.ty) = true → ∀ (e : String × Value), e ∈ bindParams ps vs → noFn e.snd = true

Used by

theorem

Lean2Js.Cost.evalCall_ne_outOfFuel

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

evalCall p fn args ≠ Except.error Err.outOfFuel

The fuel the artifact runs at is enough for every call the program can make: a program that passes progOk and whose cost fits in defaultFuel never answers outOfFuel to a call whose arguments the entry check can read.

Used by