Documentation

MasterThesis.Compiler.Compiler_v2

Compiler for LOOP language, version 2 #

source
def Compiler.v2.l2s (ev : Ident) (P : LOOP.Com) :
SCORE.Com
Equations
Instances For
    source
    def Compiler.v2.l2s.l2s' (ev : Ident) (P : LOOP.Com) :
    SCORE.Com
    Equations
    Instances For
      source
      def Compiler.eq_states_idents (s : LOOP.State) (t : SCORE.State) (ids : Finset Ident) :
      Prop
      Equations
      Instances For
        source
        def Compiler.«term_∼[_]_» :
        Lean.TrailingParserDescr
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem Compiler.eq_states_idents_no_fail {σ : LOOP.Store} {τ : SCORE.Store} {P : LOOP.Com} {Q : SCORE.Com} {ids : Finset Ident} :
          LOOP.eval P (some σ) ∼[ids] SCORE.eval Q (some τ) → (∃ (σ' : LOOP.Store), LOOP.eval P (some σ) = some σ') ∧ ∃ (τ' : SCORE.Store), SCORE.eval Q (some τ) = some τ'
          source
          theorem Compiler.eq_states_idents_update {σ : LOOP.Store} {τ : SCORE.Store} {ids : Finset Ident} (x : Ident) (v : ℕ) :
          some σ ∼[ids] some τ → some (σ[x ↦ v]) ∼[ids] some (τ[x ↦ ↑v :: τ x])
          source
          theorem Compiler.eq_states_idents_update_right {σ : LOOP.Store} {τ : SCORE.Store} {ids : Finset Ident} {x : Ident} {l : List ℤ} :
          some σ ∼[ids] some τ → x ∉ ids → some σ ∼[ids] some (τ[x ↦ l])
          source
          theorem Compiler.v2.ev_invariant {τ : SCORE.Store} {τ' : SCORE.Store} {ev : Ident} {P : LOOP.Com} (h_ids : ev ∉ P.ids) :
          (τ ev).head? = some 0 → SCORE.eval (Compiler.v2.l2s.l2s' ev P) (some τ) = some τ' → (τ' ev).head? = some 0
          source
          theorem Compiler.v2.ev_inariant_ASN {τ : SCORE.Store} {τ' : SCORE.Store} {x : Ident} {y : Ident} {ev : Ident} (h_ids : ev ∉ (LOOP.Com.ASN x y).ids) :
          (τ ev).head? = some 0 → SCORE.eval (Compiler.v2.l2s.l2s' ev (LOOP.Com.ASN x y)) (some τ) = some τ' → (τ' ev).head? = some 0
          source
          theorem Compiler.v2.soundness'_ext {σ : LOOP.Store} {τ : SCORE.Store} {ev : Ident} {ext : Finset Ident} (P : LOOP.Com) :
          ev ∉ P.ids ∪ ext → (τ ev).head? = some 0 → some σ ∼[P.ids ∪ ext] some τ → LOOP.eval P (some σ) ∼[P.ids ∪ ext] SCORE.eval (Compiler.v2.l2s.l2s' ev P) (some τ)
          source
          theorem Compiler.v2.soundness_ext {s : LOOP.State} {t : SCORE.State} {ev : Ident} {ext : Finset Ident} (P : LOOP.Com) :
          ev ∉ P.ids ∪ ext → s ∼[P.ids ∪ ext] t → LOOP.eval P s ∼[P.ids ∪ ext] SCORE.eval (Compiler.v2.l2s ev P) t
          source
          theorem Compiler.v2.soundness {s : LOOP.State} {t : SCORE.State} {ev : Ident} (P : LOOP.Com) :
          ev ∉ P.ids → s ∼[P.ids] t → LOOP.eval P s ∼[P.ids] SCORE.eval (Compiler.v2.l2s ev P) t