def walk.fuel

ezx@1.11.0.0 · src/lock/plan.bend:253

import Base
import ezx@1.11.0.0/src/lock/world.bend as W
import ezx@1.11.0.0/src/lock/lock.bend as L

253# how many steps the walk may take: one for each hash the queue starts with,
254# one for each import a verdict can queue, since a hash is resolved at most
255# once, and one more to spare. That is a step for every hash the walk can
256# queue, and it is a function of the walk's inputs rather than a fixed
257# number, as the add walk's is: a proof about inputs it does not know leaves it unevaluated,
258# where bend 2.0.33 and 2.0.34 compare a fixed fuel's walk one stack frame a
259# step and overflow the checker past about 10000.
260def walk.fuel(queue: List<&2, String>, ns: List<&2, L.Name>, js: List<&2, W.Judged>) -> Nat:
261  Nat.add(1n, Nat.add(List.length(&2, String, queue), fuel.judged(js, ns)))