Documentation

MIPRE.TM.Interp.GetEnv

The getEnv routine #

With the unary index S(ofNat i) under the head of C and the environment envRepr env on E with its head at the end, getEnv writes S(env.get i) at the head of X: it walks left over i separators (phases p1–p3), then to the start of the element (p4), copies it (p5) and returns the head of E to the end (p8); past the start of the environment the index is out of range, the rest of it is consumed (p6, p7) and nil is written (p9). The proof is by induction on the index, over the suffix of the environment not yet passed.

source
theorem MIPRE.TM.Interp.S_ofNat_succ (i : ℕ) :
S (Cost.Data.ofNat (i + 1)) = Sym.one :: Sym.zero :: S (Cost.Data.ofNat i)

The unary index S(ofNat i): (1 0)^i 0.

source
theorem MIPRE.TM.Interp.length_S_ofNat (i : ℕ) :
(S (Cost.Data.ofNat i)).length = 2 * i + 1
source
structure MIPRE.TM.Interp.EnvTape (τ : Tape) (env : Cost.Env) :
Prop

A tape holding the environment from 0, blank before.

Instances For

    The scans #

    source
    theorem MIPRE.TM.Interp.getEnv_scan3 {input : Fin 7 → List Sym} {k : ProgId} {pc : Fin maxPc} (hins : instrAt k pc = Instr.getEnv) (l : List Sym) (hl : ∀ s ∈ l, s = Sym.zero ∨ s = Sym.one) (c : Cfg input) :
    c.state = some { k := k, pc := pc, ph := Phase.p3 } → Holds (c.workTapes E) (c.workTapePos E + 1 - ↑l.length) l → ∃ (c' : Cfg input), Reach c l.length c' [] ∧ c'.state = some { k := k, pc := pc, ph := Phase.p3 } ∧ Untouched c c' [] [E] ∧ c'.workTapes E = c.workTapes E ∧ c'.workTapePos E = c.workTapePos E - ↑l.length

    Phase p3: over the bits l held on p₀ … p₀ + |l| - 1, from the last, to p₀ - 1.

    source
    theorem MIPRE.TM.Interp.getEnv_scan4 {input : Fin 7 → List Sym} {k : ProgId} {pc : Fin maxPc} (hins : instrAt k pc = Instr.getEnv) (l : List Sym) (hl : ∀ s ∈ l, s = Sym.zero ∨ s = Sym.one) (c : Cfg input) :
    c.state = some { k := k, pc := pc, ph := Phase.p4 } → Holds (c.workTapes E) (c.workTapePos E + 1 - ↑l.length) l → c.workTapes E (c.workTapePos E - ↑l.length) = some Sym.sep ∨ c.workTapes E (c.workTapePos E - ↑l.length) = none → ∃ (c' : Cfg input), Reach c (l.length + 1) c' [] ∧ c'.state = some { k := k, pc := pc, ph := Phase.p5 } ∧ Untouched c c' [] [E] ∧ c'.workTapes E = c.workTapes E ∧ c'.workTapePos E = c.workTapePos E - ↑l.length + 1

    Phase p4: over the bits l, from the last, to p₀ - 1, then one right to p₀ at p5.

    source
    theorem MIPRE.TM.Interp.getEnv_copy5 {input : Fin 7 → List Sym} {k : ProgId} {pc : Fin maxPc} (hins : instrAt k pc = Instr.getEnv) (l : List Sym) (hl : ∀ s ∈ l, s = Sym.zero ∨ s = Sym.one) (c : Cfg input) :
    c.state = some { k := k, pc := pc, ph := Phase.p5 } → Holds (c.workTapes E) (c.workTapePos E) l → c.workTapes E (c.workTapePos E + ↑l.length) = some Sym.sep → ∃ (c' : Cfg input), Reach c (l.length + 1) c' [] ∧ c'.state = some { k := k, pc := pc, ph := Phase.p8 } ∧ Untouched c c' [] [E, X] ∧ c'.workTapes E = c.workTapes E ∧ c'.workTapePos E = c.workTapePos E + ↑l.length ∧ DstEff X c c' l

    Phase p5: copy the bits l under the head of E to X, to the # after them.

    source
    theorem MIPRE.TM.Interp.getEnv_toEnd {input : Fin 7 → List Sym} {k : ProgId} {pc : Fin maxPc} (hins : instrAt k pc = Instr.getEnv) (hpc : ↑pc + 1 < maxPc) (ph : Phase) (hph : ph = Phase.p8 ∨ ph = Phase.p9) (l : List Sym) (c : Cfg input) :
    c.state = some { k := k, pc := pc, ph := ph } → Holds (c.workTapes E) (c.workTapePos E) l → c.workTapes E (c.workTapePos E + ↑l.length) = none → ∃ (c' : Cfg input), Reach c (l.length + 1) c' [] ∧ c'.state = next_ k pc hpc ∧ Untouched c c' [] [E] ∧ c'.workTapes E = c.workTapes E ∧ c'.workTapePos E = c.workTapePos E + ↑l.length

    Phases p8/p9: the head of E right to the first blank.

    source
    theorem MIPRE.TM.Interp.getEnv_consume {input : Fin 7 → List Sym} {k : ProgId} {pc : Fin maxPc} (hins : instrAt k pc = Instr.getEnv) (j : ℕ) (c : Cfg input) :
    c.state = some { k := k, pc := pc, ph := Phase.p6 } → Holds (c.workTapes C) (c.workTapePos C) (S (Cost.Data.ofNat j)) → ∃ (c' : Cfg input), Reach c (2 * j + 1) c' [] ∧ c'.state = some { k := k, pc := pc, ph := Phase.p9 } ∧ Untouched c c' [] [C, E, X] ∧ c'.workTapes C = c.workTapes C ∧ c'.workTapePos C = c.workTapePos C + ↑(2 * j + 1) ∧ c'.workTapes E = c.workTapes E ∧ c'.workTapePos E = c.workTapePos E + 1 ∧ DstEff X c c' [Sym.zero]

    Phases p6/p7: consume the index S(ofNat j) on C, then write nil on X and move E one right, at p9.

    The walk #

    source
    theorem MIPRE.TM.Interp.EnvTape.suffix_cells {τ : Tape} {env : Cost.Env} (h : EnvTape τ env) (v : Cost.Data) (rest : Cost.Env) {l₀ : List Sym} (hpre : envRepr env = envRepr (v :: rest) ++ l₀) :
    Holds τ (↑(envRepr rest).length) (S v) ∧ τ (↑(envRepr rest).length + ↑(S v).length) = some Sym.sep ∧ (τ (↑(envRepr rest).length - 1) = some Sym.sep ∨ τ (↑(envRepr rest).length - 1) = none)

    Cells of a suffix of the environment: for env' = v :: rest a prefix of env, S v sits at |envRepr rest|, followed by #, and preceded by # or the blank before the tape.

    source
    theorem MIPRE.TM.Interp.EnvTape.tail_cells {τ : Tape} {env : Cost.Env} (h : EnvTape τ env) (q : ℕ) (hq : q ≤ (envRepr env).length) :
    Holds τ (↑q) (List.drop q (envRepr env)) ∧ τ (↑q + ↑(List.drop q (envRepr env)).length) = none

    The cells from q to the end of the environment.

    source
    theorem MIPRE.TM.Interp.Env.get_nil' (j : ℕ) :
    Cost.Env.get [] j = Cost.Data.nil
    source
    theorem MIPRE.TM.Interp.getEnv_walk {input : Fin 7 → List Sym} {k : ProgId} {pc : Fin maxPc} (hins : instrAt k pc = Instr.getEnv) (hpc : ↑pc + 1 < maxPc) (env : Cost.Env) (j : ℕ) (env' : Cost.Env) (c : Cfg input) :
    c.state = some { k := k, pc := pc, ph := Phase.p1 } → EnvTape (c.workTapes E) env → (∃ (l₀ : List Sym), envRepr env = envRepr env' ++ l₀) → c.workTapePos E = ↑(envRepr env').length - 1 → Holds (c.workTapes C) (c.workTapePos C) (S (Cost.Data.ofNat j)) → ∃ n ≤ 3 * j + 2 * (envRepr env).length + (envRepr env').length + 8, ∃ (c' : Cfg input), Reach c n c' [] ∧ c'.state = next_ k pc hpc ∧ Untouched c c' [] [C, E, X] ∧ c'.workTapes C = c.workTapes C ∧ c'.workTapePos C = c.workTapePos C + ↑(2 * j + 1) ∧ c'.workTapes E = c.workTapes E ∧ c'.workTapePos E = ↑(envRepr env).length ∧ DstEff X c c' (S (env'.get j))

    The walk from phase p1: at the separator of the last element of the suffix env' of env (or before the tape if env' is empty), with the index S(ofNat j) on C.

    source
    theorem MIPRE.TM.Interp.exec_getEnv {input : Fin 7 → List Sym} {k : ProgId} {pc : Fin maxPc} (hins : instrAt k pc = Instr.getEnv) (hpc : ↑pc + 1 < maxPc) (env : Cost.Env) (i : ℕ) (c : Cfg input) (hq : c.state = at_ k pc) (hE : EnvTape (c.workTapes E) env) (hpos : c.workTapePos E = ↑(envRepr env).length) (hC : Holds (c.workTapes C) (c.workTapePos C) (S (Cost.Data.ofNat i))) :
    ∃ n ≤ 3 * i + 3 * (envRepr env).length + 9, ∃ (c' : Cfg input), Reach c n c' [] ∧ c'.state = next_ k pc hpc ∧ Untouched c c' [] [C, E, X] ∧ c'.workTapes C = c.workTapes C ∧ c'.workTapePos C = c.workTapePos C + ↑(2 * i + 1) ∧ c'.workTapes E = c.workTapes E ∧ c'.workTapePos E = ↑(envRepr env).length ∧ DstEff X c c' (S (env.get i))

    getEnv: with S(ofNat i) under the head of C and the environment on E with its head at the end, write S(env.get i) at the head of X.