Time- and resource-bounded runs of abstract machines

DefinitionOne iteration step with absorbing halted states#✓fully proved

One iteration, preserving a state once its output is available.

def next (step : State → State) (out : State → Option Output) (s : State) : State :=
  match out s with
  | some _ => s
  | none => step s

Used by 10

Used byOutput reachability gives stable outputs and bounded iterates · Iterates of a halted state are constant · Terminal iterates are stable · The output of a successful run persists · Output reachability via bounded iterates after halting · Characterization of output reachability by iterates · Output reachability from the iteration condition · Canonical finite path to an output bounds all iterates · Input-initialized iteration with absorbing halting · Uniqueness of reached outputs

DefinitionResource-bounded active step#✓fully proved

An active step with a resource bound on its source.

def boundedStep (step : State → State) (out : State → Option Output)
    (measure : State → ℕ) (S : ℕ) (s t : State) : Prop :=
  out s = none ∧ measure s ≤ S ∧ t = step s

Used by 6

Used byA halted state reaches its output with any time budget · Output reachability gives stable outputs and bounded iterates · Monotonicity of output reachability in the bounds · Prepending a bounded step to a successful computation · Output reachability within time and resource bounds · Canonical finite path to an output bounds all iterates

DefinitionOutput reachability within time and resource bounds#✓fully proved

Reach an output in at most T active steps, with every state bounded by S.

def ReachesOutput (step : State → State) (out : State → Option Output)
    (measure : State → ℕ) (s : State) (T S : ℕ) (b : Output) : Prop :=
  ∃ t, Relation.RelatesWithinSteps (boundedStep step out measure S) s t T ∧
    out t = some b ∧ measure t ≤ S

Uses 1 · Used by 9

Statement usesResource-bounded active step

Used byA halted state reaches its output with any time budget · Output reachability gives stable outputs and bounded iterates · Monotonicity of output reachability in the bounds · Prepending a bounded step to a successful computation · Output reachability via bounded iterates after halting · Characterization of output reachability by iterates · Output reachability from the iteration condition · Bounded run from an input's initial state · Uniqueness of reached outputs

DefinitionBounded run from an input's initial state#✓fully proved

Reach an output starting from an input's initial state.

def Runs (init : Input → State) (step : State → State) (out : State → Option Output)
    (measure : State → ℕ) (a : Input) (T S : ℕ) (b : Output) : Prop :=
  ReachesOutput step out measure (init a) T S b

Uses 1 · Used by 4

Statement usesOutput reachability within time and resource bounds

Used byMonotonicity of bounded runs in time and resources · The output of a successful run persists · Characterization of bounded runs by initialized iteration · Uniqueness of run outputs

TheoremIterates of a halted state are constant#✓fully proved

Every iterate of an already halted state is that state.

theorem iterate_of_some (h : out s = some b) (n : ℕ) : (next step out)^[n] s = s

Uses 1 · Used by 3

Statement usesOne iteration step with absorbing halted states

Used byTerminal iterates are stable · Output reachability from the iteration condition · Canonical finite path to an output bounds all iterates

TheoremA halted state reaches its output with any time budget#✓fully proved

A halted state reaches its output with any remaining time budget.

theorem ReachesOutput.halt (ho : out s = some b) (hs : measure s ≤ S) :
    ReachesOutput step out measure s T S b

Uses 2 · Used by 1

Statement usesOutput reachability within time and resource bounds

Proof usesResource-bounded active step

Used byOutput reachability from the iteration condition

TheoremPrepending a bounded step to a successful computation#✓fully proved

Prepend an active bounded step to a successful computation.

theorem ReachesOutput.prepend (ho : out s = none) (hs : measure s ≤ S)
    (h : ReachesOutput step out measure (step s) T S b) :
    ReachesOutput step out measure s (T + 1) S b

Uses 2 · Used by 1

Statement usesOutput reachability within time and resource bounds

Proof usesResource-bounded active step

Used byOutput reachability from the iteration condition

TheoremCanonical finite path to an output bounds all iterates#✓fully proved

A canonical finite path ending in an output has the source's all-iterate bounds.

theorem relatesInSteps_iterate {n : ℕ}
    (h : Relation.RelatesInSteps (boundedStep step out measure S) s t n)
    (ho : out t = some b) (hs : measure t ≤ S) :
    (∀ T, n ≤ T → out ((next step out)^[T] s) = some b) ∧
      ∀ k, measure ((next step out)^[k] s) ≤ S

Uses 3 · Used by 1

Statement usesResource-bounded active step · One iteration step with absorbing halted states

Proof usesIterates of a halted state are constant

Used byOutput reachability gives stable outputs and bounded iterates

TheoremOutput reachability gives stable outputs and bounded iterates#✓fully proved

Reachability gives stable outputs after the budget and bounds every iterate.

theorem ReachesOutput.iterate (h : ReachesOutput step out measure s T S b) :
    (∀ U, T ≤ U → out ((next step out)^[U] s) = some b) ∧
      ∀ n, measure ((next step out)^[n] s) ≤ S

Uses 4 · Used by 3

Statement usesOutput reachability within time and resource bounds · One iteration step with absorbing halted states

Proof usesResource-bounded active step · Canonical finite path to an output bounds all iterates

Used byThe output of a successful run persists · Characterization of output reachability by iterates · Uniqueness of reached outputs

TheoremOutput reachability from the iteration condition#✓fully proved

The source iteration condition constructs a canonical bounded path.

theorem reachesOutput_of_iterate
    (ho : out ((next step out)^[T] s) = some b)
    (hs : ∀ n, measure ((next step out)^[n] s) ≤ S) :
    ReachesOutput step out measure s T S b

Uses 5 · Used by 1

Statement usesOutput reachability within time and resource bounds · One iteration step with absorbing halted states

Proof usesA halted state reaches its output with any time budget · Prepending a bounded step to a successful computation · Iterates of a halted state are constant

Used byCharacterization of output reachability by iterates

TheoremCharacterization of output reachability by iterates#✓fully proved

Exact source characterization, including bounds on all natural-number iterates.

theorem reachesOutput_iff_iterate :
    ReachesOutput step out measure s T S b ↔
      out ((next step out)^[T] s) = some b ∧
        ∀ n, measure ((next step out)^[n] s) ≤ S

Uses 4 · Used by 2

Statement usesOutput reachability within time and resource bounds · One iteration step with absorbing halted states

Proof usesOutput reachability gives stable outputs and bounded iterates · Output reachability from the iteration condition

Used byOutput reachability via bounded iterates after halting · Characterization of bounded runs by initialized iteration

TheoremTerminal iterates are stable#✓fully proved

A terminal iterate remains unchanged at every later iteration count.

theorem iterate_stable (ho : out ((next step out)^[T] s) = some b)
    {U : ℕ} (hU : T ≤ U) : (next step out)^[U] s = (next step out)^[T] s

Uses 2 · Used by 1

Statement usesOne iteration step with absorbing halted states

Proof usesIterates of a halted state are constant

Used byOutput reachability via bounded iterates after halting

TheoremOutput reachability via bounded iterates after halting#✓fully proved

Finite visited-state bounds are equivalent to all-iterate bounds after halting.

theorem reachesOutput_iff_bounded_iterate :
    ReachesOutput step out measure s T S b ↔
      out ((next step out)^[T] s) = some b ∧
        ∀ n ≤ T, measure ((next step out)^[n] s) ≤ S

Uses 4

Statement usesOutput reachability within time and resource bounds · One iteration step with absorbing halted states

Proof usesTerminal iterates are stable · Characterization of output reachability by iterates

TheoremMonotonicity of output reachability in the bounds#✓fully proved

Increasing either bound preserves reachability.

theorem ReachesOutput.mono {U R : ℕ} (h : ReachesOutput step out measure s T S b)
    (hT : T ≤ U) (hS : S ≤ R) : ReachesOutput step out measure s U R b

Uses 2 · Used by 1

Statement usesOutput reachability within time and resource bounds

Proof usesResource-bounded active step

Used byMonotonicity of bounded runs in time and resources

TheoremUniqueness of reached outputs#✓fully proved

Output values reached from the same state are unique, regardless of bounds.

theorem ReachesOutput.unique {U R : ℕ} {c : Output}
    (h : ReachesOutput step out measure s T S b)
    (h' : ReachesOutput step out measure s U R c) : b = c

Uses 3 · Used by 1

Statement usesOutput reachability within time and resource bounds

Proof usesOutput reachability gives stable outputs and bounded iterates · One iteration step with absorbing halted states

Used byUniqueness of run outputs

DefinitionInput-initialized iteration with absorbing halting#✓fully proved

Iteration initialized by an input, with absorbing halting.

def run (init : Input → State) (step : State → State) (out : State → Option Output)
    (a : Input) (n : ℕ) : State := (next step out)^[n] (init a)

Uses 1 · Used by 2

Statement usesOne iteration step with absorbing halted states

Used byThe output of a successful run persists · Characterization of bounded runs by initialized iteration

TheoremCharacterization of bounded runs by initialized iteration#✓fully proved

The source Runs interface, stated using initialized iteration.

theorem runs_iff_iterate {init : Input → State} {a : Input} :
    Runs init step out measure a T S b ↔
      out (run init step out a T) = some b ∧
        ∀ n, measure (run init step out a n) ≤ S

Uses 3

Statement usesBounded run from an input's initial state · Input-initialized iteration with absorbing halting

Proof usesCharacterization of output reachability by iterates

TheoremThe output of a successful run persists#✓fully proved

The output of a successful initialized run is present at every later time.

theorem Runs.out_run {init : Input → State} {a : Input}
    (h : Runs init step out measure a T S b) {U : ℕ} (hU : T ≤ U) :
    out (run init step out a U) = some b

Uses 4

Statement usesBounded run from an input's initial state · Input-initialized iteration with absorbing halting

Proof usesOutput reachability gives stable outputs and bounded iterates · One iteration step with absorbing halted states

TheoremMonotonicity of bounded runs in time and resources#✓fully proved

Increasing time and resource bounds preserves initialized runs.

theorem Runs.mono {init : Input → State} {a : Input} {U R : ℕ}
    (h : Runs init step out measure a T S b) (hT : T ≤ U) (hS : S ≤ R) :
    Runs init step out measure a U R b

Uses 2

Statement usesBounded run from an input's initial state

Proof usesMonotonicity of output reachability in the bounds

TheoremUniqueness of run outputs#✓fully proved

Initialized runs have unique outputs.

theorem Runs.unique {init : Input → State} {a : Input} {U R : ℕ} {c : Output}
    (h : Runs init step out measure a T S b)
    (h' : Runs init step out measure a U R c) : b = c

Uses 2

Statement usesBounded run from an input's initial state

Proof usesUniqueness of reached outputs

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.