Documentation

MIPRE.Foundations.Cost.Machine

The evaluation machine #

A small-step abstract machine (CEK style) for the ambient language: a configuration is a control (a program to evaluate, or a value being returned), an environment and a stack of continuation frames. It is the common core of the two "universal" artifacts of the project:

The machine charges the cost of each Eval rule at a designated step (stepCost), so that the accumulated cost of a run is exactly the cost of the Eval derivation. The two directions of the correspondence are eval_steps (a derivation yields a run of the machine) and eval_of_steps (a halting run of the machine yields a derivation).

source
inductive MIPRE.Cost.Machine.Frame :
Type

Continuation frames.

  • cons1 (t : Prog) (env : Env) : Frame

    Evaluating the head of cons h t; next evaluate t in env.

  • cons2 (a : Data) : Frame

    The head value a of a cons; next return cons a v.

  • let1 (b : Prog) (env : Env) : Frame

    Evaluating the binding of let_ e b; next evaluate b in v :: env.

  • loop1 (b : Prog) (env : Env) : Frame

    Evaluating the body of loop b in env; next dispatch on the value.

Instances For
    source
    def MIPRE.Cost.Machine.instDecidableEqFrame.decEq (x✝ x✝¹ : Frame) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      source
      @[instance_reducible]
      instance MIPRE.Cost.Machine.instDecidableEqFrame :
      DecidableEq Frame
      Equations
      source
      inductive MIPRE.Cost.Machine.Ctrl :
      Type

      The control: a program to evaluate, or a value being returned.

      Instances For
        source
        @[instance_reducible]
        instance MIPRE.Cost.Machine.instDecidableEqCtrl :
        DecidableEq Ctrl
        Equations
        source
        def MIPRE.Cost.Machine.instDecidableEqCtrl.decEq (x✝ x✝¹ : Ctrl) :
        Decidable (x✝ = x✝¹)
        Equations
        Instances For
          source
          structure MIPRE.Cost.Machine.Cfg :
          Type

          Configurations.

          Instances For
            source
            @[instance_reducible]
            instance MIPRE.Cost.Machine.instDecidableEqCfg :
            DecidableEq Cfg
            Equations
            source
            def MIPRE.Cost.Machine.instDecidableEqCfg.decEq (x✝ x✝¹ : Cfg) :
            Decidable (x✝ = x✝¹)
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def MIPRE.Cost.Machine.step :
              Cfg → Cfg

              One step of the machine. Final configurations (a value with an empty stack) are fixed.

              Equations
              Instances For
                source
                def MIPRE.Cost.Machine.stepCost :
                Cfg → ℕ

                The Eval cost charged at a step: the rule's own unit (plus the size of the value read, for var and const); loop rules are charged when the body's value is dispatched.

                Equations
                Instances For
                  source
                  def MIPRE.Cost.Machine.costSum (c : Cfg) :
                  ℕ → ℕ

                  The cost accumulated over n steps.

                  Equations
                  Instances For
                    source
                    def MIPRE.Cost.Machine.Steps (c : Cfg) (N : ℕ) (c' : Cfg) (t : ℕ) :
                    Prop

                    Steps c N c' t: N steps lead from c to c', accumulating cost t.

                    Equations
                    Instances For
                      source
                      theorem MIPRE.Cost.Machine.costSum_add (c : Cfg) (m n : ℕ) :
                      costSum c (m + n) = costSum c m + costSum (step^[m] c) n
                      source
                      theorem MIPRE.Cost.Machine.Steps.one (c : Cfg) :
                      Steps c 1 (step c) (stepCost c)
                      source
                      theorem MIPRE.Cost.Machine.Steps.trans {c₁ c₂ c₃ : Cfg} {m n t₁ t₂ : ℕ} (h₁ : Steps c₁ m c₂ t₁) (h₂ : Steps c₂ n c₃ t₂) :
                      Steps c₁ (m + n) c₃ (t₁ + t₂)
                      source
                      theorem MIPRE.Cost.Machine.Steps.cast {c c' : Cfg} {N t t' : ℕ} (h : Steps c N c' t) (e : t = t') :
                      Steps c N c' t'
                      source
                      theorem MIPRE.Cost.Machine.Steps.of_succ {c c' : Cfg} {N t : ℕ} (h : Steps c (N + 1) c' t) :
                      ∃ (t' : ℕ), t = stepCost c + t' ∧ Steps (step c) N c' t'
                      source
                      theorem MIPRE.Cost.Machine.Steps.ne_zero {p : Prog} {env : Env} {k : List Frame} {N : ℕ} {r : Data} {e : Env} {t : ℕ} (h : Steps { ctrl := Ctrl.ev p, env := env, kont := k } N { ctrl := Ctrl.ret r, env := e, kont := k } t) :
                      N ≠ 0

                      Forward: derivations give machine runs #

                      source
                      theorem MIPRE.Cost.Machine.eval_steps {env : Env} {p : Prog} {r : Data} {t : ℕ} (h : Eval env p r t) (k : List Frame) :
                      ∃ (N : ℕ) (env' : Env), Steps { ctrl := Ctrl.ev p, env := env, kont := k } N { ctrl := Ctrl.ret r, env := env', kont := k } t

                      Backward: halting runs give derivations #

                      source
                      def MIPRE.Cost.Machine.IsFinal (c : Cfg) :
                      Prop

                      A final configuration: a value with an empty stack.

                      Equations
                      Instances For
                        source
                        theorem MIPRE.Cost.Machine.eval_of_steps (N : ℕ) (p : Prog) (env : Env) (k : List Frame) (r : Data) (e : Env) :
                        step^[N] { ctrl := Ctrl.ev p, env := env, kont := k } = { ctrl := Ctrl.ret r, env := e, kont := [] } → ∃ (r' : Data) (t : ℕ) (M : ℕ) (e' : Env) (N' : ℕ), N = M + N' ∧ Eval env p r' t ∧ Steps { ctrl := Ctrl.ev p, env := env, kont := k } M { ctrl := Ctrl.ret r', env := e', kont := k } t
                        source
                        theorem MIPRE.Cost.Machine.halts_iff (p : Prog) (x r : Data) :
                        (∃ (t : ℕ), p.Runs x r t) ↔ ∃ (N : ℕ) (e : Env), step^[N] { ctrl := Ctrl.ev p, env := [x], kont := [] } = { ctrl := Ctrl.ret r, env := e, kont := [] }

                        The two directions together: p on x halts with r iff the machine started at ⟨ev p, [x], []⟩ reaches the final configuration with value r.