Library GotoSem
Require Import
Coqlib Utf8
Relations
Integers
LatticeSignatures
AbMachineNonrel
Goto.
Require CompleteLattice.
Ltac vauto :=
(econstructor (first [ now eauto | econstructor (now eauto) ])) || idtac.
Definition flag_state := flag → bool.
Definition eval_flag (i j: int) (f: flag) : bool :=
match f with
| FLE ⇒ negb (Int.lt j i)
| FLT ⇒ Int.lt i j
| FEQ ⇒ Int.eq i j
end.
Definition compare := eval_flag.
Definition register_state := register → int.
Notation "R # r ← v" := (upd R r v) (at level 60, r at next level).
Definition memory := int → int.
Record machine_config := {
pc : int;
mc_flg : flag_state;
mc_reg : register_state;
mc_mem : memory
}.
Inductive machine_state :=
| Halted (v:int)
| Running (c:machine_config)
.
Notation "⌈ v ⌉" := (Halted v) (at level 2).
Notation "⟨ pp , f , r , m ⟩" := (Running {| pc := pp; mc_flg:= f; mc_reg:= r; mc_mem := m |}) (at level 2).
Notation "⌊ x ⌋" := (Some x).
Lemma run_not_hlt {pp f r m v} :
⟨ pp, f, r, m ⟩ = ⌈v⌉ → ∀ P : Prop, P.
Lemma run_inv {pp f r m pp' f' r' m'} :
⟨ pp, f, r, m ⟩ = ⟨ pp', f', r', m' ⟩ →
∀ P : _ → _ → _ → _ → Prop,
P pp f r m →
P pp' f' r' m'.
Reserved Notation "a =~> b" (at level 70).
Coercion Z.of_nat : nat >-> Z.
Notation "p + q" := (Int.add p (Int.repr q)) (left associativity, at level 50) : goto_scope.
Notation "x [ op ] y" := (eval_int_binop op x y) (at level 80) : goto_scope.
Notation "'dec'" := (decode_from) (only parsing) : goto_scope.
Local Open Scope goto_scope.
Inductive small_step : relation machine_state :=
| SCst pp f r m v rd z : dec m pp = ⌊(ICst v rd, z)⌋ →
⟨ pp, f, r, m ⟩ =~> ⟨ pp+z, f, r#rd ← v, m ⟩
| SCmp pp f r m rs rd z : dec m pp = ⌊(ICmp rs rd, z)⌋ →
⟨ pp, f, r, m ⟩ =~> ⟨ pp+z, compare (r rd) (r rs), r, m ⟩
| SBinop pp f r m op rs rd z : dec m pp = ⌊(IBinop op rs rd, z)⌋ →
⟨ pp, f, r, m ⟩ =~> ⟨ pp+z, f, r#rd ← (r rs [op] r rd), m ⟩
| SLoad pp f r m rs rd z : dec m pp = ⌊(ILoad rs rd, z)⌋ →
⟨ pp, f, r, m ⟩ =~> ⟨ pp+z, f, r#rd ← m (r rs), m ⟩
| SStore pp f r m rs rd z : dec m pp = ⌊(IStore rs rd, z)⌋ →
⟨ pp, f, r, m ⟩ =~> ⟨ pp+z, f, r, m # r rd ← r rs ⟩
| SGoto pp f r m v z : dec m pp = ⌊(IGoto v, z)⌋ →
⟨ pp, f, r, m ⟩ =~> ⟨ v, f, r, m ⟩
| SGotoCond pp f r m c v z : dec m pp = ⌊(IGotoCond c v, z)⌋ →
⟨ pp, f, r, m ⟩ =~> ⟨ if f(c) then v else pp+z, f, r, m ⟩
| SGotoInd pp f r m rd z : dec m pp = ⌊(IGotoInd rd, z)⌋ →
⟨ pp, f, r, m ⟩ =~> ⟨ r(rd), f, r, m ⟩
| SSkip pp f r m z : dec m pp = ⌊(ISkip, z)⌋ →
⟨ pp, f, r, m ⟩ =~> ⟨ pp+z, f, r, m ⟩
| SHalt pp f r m rd z : dec m pp = ⌊(IHalt rd, z)⌋ →
⟨ pp, f, r, m ⟩ =~> ⌈r rd⌉
where "a =~> b" := (small_step a b).
Lemma small_step_hlt_inv_P msi res (P: machine_state → int → Prop) :
msi =~> ⌈res⌉ →
(∀ pc f r m, ∀ rd z,
⟨ pc, f, r, m ⟩ =~> ⌈r rd⌉ →
decode_from m pc = ⌊(IHalt rd, z)⌋ →
P ⟨ pc, f, r, m ⟩ (r rd)
) →
P msi res.
Corollary small_step_hlt_inv msi res :
msi =~> ⌈res⌉ →
∃ pc f r m rd z, msi = ⟨pc, f, r, m⟩ ∧ res = r rd ∧ decode_from m pc = ⌊(IHalt rd, z)⌋.
Definition initial_state f r m : machine_state :=
⟨ Int.zero, f, r, m ⟩.
Definition sos_star := clos_refl_trans _ small_step.
Notation "a ⇉★ b" := (sos_star a b) (at level 70).
Definition reachable I (s: machine_state) : Prop :=
∃ f r, initial_state f r I ⇉★ s.
Lemma reachable_step I s :
reachable I s →
∀ s', s =~> s' →
reachable I s'.
Coqlib Utf8
Relations
Integers
LatticeSignatures
AbMachineNonrel
Goto.
Require CompleteLattice.
Ltac vauto :=
(econstructor (first [ now eauto | econstructor (now eauto) ])) || idtac.
Definition flag_state := flag → bool.
Definition eval_flag (i j: int) (f: flag) : bool :=
match f with
| FLE ⇒ negb (Int.lt j i)
| FLT ⇒ Int.lt i j
| FEQ ⇒ Int.eq i j
end.
Definition compare := eval_flag.
Definition register_state := register → int.
Notation "R # r ← v" := (upd R r v) (at level 60, r at next level).
Definition memory := int → int.
Record machine_config := {
pc : int;
mc_flg : flag_state;
mc_reg : register_state;
mc_mem : memory
}.
Inductive machine_state :=
| Halted (v:int)
| Running (c:machine_config)
.
Notation "⌈ v ⌉" := (Halted v) (at level 2).
Notation "⟨ pp , f , r , m ⟩" := (Running {| pc := pp; mc_flg:= f; mc_reg:= r; mc_mem := m |}) (at level 2).
Notation "⌊ x ⌋" := (Some x).
Lemma run_not_hlt {pp f r m v} :
⟨ pp, f, r, m ⟩ = ⌈v⌉ → ∀ P : Prop, P.
Lemma run_inv {pp f r m pp' f' r' m'} :
⟨ pp, f, r, m ⟩ = ⟨ pp', f', r', m' ⟩ →
∀ P : _ → _ → _ → _ → Prop,
P pp f r m →
P pp' f' r' m'.
Reserved Notation "a =~> b" (at level 70).
Coercion Z.of_nat : nat >-> Z.
Notation "p + q" := (Int.add p (Int.repr q)) (left associativity, at level 50) : goto_scope.
Notation "x [ op ] y" := (eval_int_binop op x y) (at level 80) : goto_scope.
Notation "'dec'" := (decode_from) (only parsing) : goto_scope.
Local Open Scope goto_scope.
Inductive small_step : relation machine_state :=
| SCst pp f r m v rd z : dec m pp = ⌊(ICst v rd, z)⌋ →
⟨ pp, f, r, m ⟩ =~> ⟨ pp+z, f, r#rd ← v, m ⟩
| SCmp pp f r m rs rd z : dec m pp = ⌊(ICmp rs rd, z)⌋ →
⟨ pp, f, r, m ⟩ =~> ⟨ pp+z, compare (r rd) (r rs), r, m ⟩
| SBinop pp f r m op rs rd z : dec m pp = ⌊(IBinop op rs rd, z)⌋ →
⟨ pp, f, r, m ⟩ =~> ⟨ pp+z, f, r#rd ← (r rs [op] r rd), m ⟩
| SLoad pp f r m rs rd z : dec m pp = ⌊(ILoad rs rd, z)⌋ →
⟨ pp, f, r, m ⟩ =~> ⟨ pp+z, f, r#rd ← m (r rs), m ⟩
| SStore pp f r m rs rd z : dec m pp = ⌊(IStore rs rd, z)⌋ →
⟨ pp, f, r, m ⟩ =~> ⟨ pp+z, f, r, m # r rd ← r rs ⟩
| SGoto pp f r m v z : dec m pp = ⌊(IGoto v, z)⌋ →
⟨ pp, f, r, m ⟩ =~> ⟨ v, f, r, m ⟩
| SGotoCond pp f r m c v z : dec m pp = ⌊(IGotoCond c v, z)⌋ →
⟨ pp, f, r, m ⟩ =~> ⟨ if f(c) then v else pp+z, f, r, m ⟩
| SGotoInd pp f r m rd z : dec m pp = ⌊(IGotoInd rd, z)⌋ →
⟨ pp, f, r, m ⟩ =~> ⟨ r(rd), f, r, m ⟩
| SSkip pp f r m z : dec m pp = ⌊(ISkip, z)⌋ →
⟨ pp, f, r, m ⟩ =~> ⟨ pp+z, f, r, m ⟩
| SHalt pp f r m rd z : dec m pp = ⌊(IHalt rd, z)⌋ →
⟨ pp, f, r, m ⟩ =~> ⌈r rd⌉
where "a =~> b" := (small_step a b).
Lemma small_step_hlt_inv_P msi res (P: machine_state → int → Prop) :
msi =~> ⌈res⌉ →
(∀ pc f r m, ∀ rd z,
⟨ pc, f, r, m ⟩ =~> ⌈r rd⌉ →
decode_from m pc = ⌊(IHalt rd, z)⌋ →
P ⟨ pc, f, r, m ⟩ (r rd)
) →
P msi res.
Corollary small_step_hlt_inv msi res :
msi =~> ⌈res⌉ →
∃ pc f r m rd z, msi = ⟨pc, f, r, m⟩ ∧ res = r rd ∧ decode_from m pc = ⌊(IHalt rd, z)⌋.
Definition initial_state f r m : machine_state :=
⟨ Int.zero, f, r, m ⟩.
Definition sos_star := clos_refl_trans _ small_step.
Notation "a ⇉★ b" := (sos_star a b) (at level 70).
Definition reachable I (s: machine_state) : Prop :=
∃ f r, initial_state f r I ⇉★ s.
Lemma reachable_step I s :
reachable I s →
∀ s', s =~> s' →
reachable I s'.
The machine is stuck if it is not halted yet cannot make progress.
Definition stuck (s: machine_state) : Prop :=
match s with
| ⌈_⌉ ⇒ False
| ⟨_, _, _, _⟩ ⇒ ∀ s', ¬ s =~> s'
end.
match s with
| ⌈_⌉ ⇒ False
| ⟨_, _, _, _⟩ ⇒ ∀ s', ¬ s =~> s'
end.
Here, being stuck means that the instruction at current program point
cannot be decoded.
Lemma stuck_is_decode_failure s :
stuck s ↔ match s with ⟨ pp, f, r, m ⟩ ⇒ decode_from m pp = None | _ ⇒ False end.
Lemma small_step_dec s :
{∃ v, s = ⌈v⌉ } + { ∃ s', s =~> s' } + { stuck s }.
Lemma not_stuck s :
¬ stuck s →
(∃ v, s = ⌈v⌉) ∨ (∃ s', s =~> s').
stuck s ↔ match s with ⟨ pp, f, r, m ⟩ ⇒ decode_from m pp = None | _ ⇒ False end.
Lemma small_step_dec s :
{∃ v, s = ⌈v⌉ } + { ∃ s', s =~> s' } + { stuck s }.
Lemma not_stuck s :
¬ stuck s →
(∃ v, s = ⌈v⌉) ∨ (∃ s', s =~> s').
A program is safe if it cannot reach a state in which it is stuck.
Definition safe P : Prop :=
∀ s, reachable P s → ¬ stuck s.
Notation Env := (machine_state → Prop).
Definition initial_env (I: memory) : Env := λ ms,
match ms with
| ⟨ z, _, _, m ⟩ ⇒ z = Int.zero ∧ m = I
| ⌈_⌉ ⇒ False
end.
Definition post : Env → Env := fun E msi ⇒
∃ msi', E msi' ∧ msi' =~> msi.
Definition semantics_fun (I: memory) : Env → Env :=
λ e, initial_env I ∪ post e.
Instance semantics_fun_mon (I:memory) : CompleteLattice.monotone Env Env (semantics_fun I).
Definition semantics prg : Env := CompleteLattice.lfp (semantics_fun_mon prg).
Notation "⟦ c ⟧" := (semantics c) (at level 2).
Definition reachable_env (I: memory) : Env :=
fun s ⇒
∃ i, initial_env I i
∧ clos_refl_trans _ small_step i s.
Lemma reachable_in_sem (prg:memory) :
reachable prg ⊆ ⟦ prg ⟧.
Lemma sem_in_reachable (prg: memory) :
⟦prg⟧ ⊆ reachable(prg).
Definition upd_mem : memory → addr → int → memory := upd.
Definition encode_program (prg: list instruction) (m:memory) : memory × list int :=
@List.fold_left
(memory × list int) instruction
(λ m_n i,
let v := encode_instr i in
@List.fold_left
(memory × list int) int
(λ m_n j,
let (m, n) := m_n in
let (pp, ppl) := match n with hd::tl ⇒ (Int.add hd Int.one, n) | nil ⇒ (Int.zero, nil) end in
(upd_mem m pp j, pp::ppl))
v
m_n)
prg
(m, nil).
∀ s, reachable P s → ¬ stuck s.
Notation Env := (machine_state → Prop).
Definition initial_env (I: memory) : Env := λ ms,
match ms with
| ⟨ z, _, _, m ⟩ ⇒ z = Int.zero ∧ m = I
| ⌈_⌉ ⇒ False
end.
Definition post : Env → Env := fun E msi ⇒
∃ msi', E msi' ∧ msi' =~> msi.
Definition semantics_fun (I: memory) : Env → Env :=
λ e, initial_env I ∪ post e.
Instance semantics_fun_mon (I:memory) : CompleteLattice.monotone Env Env (semantics_fun I).
Definition semantics prg : Env := CompleteLattice.lfp (semantics_fun_mon prg).
Notation "⟦ c ⟧" := (semantics c) (at level 2).
Definition reachable_env (I: memory) : Env :=
fun s ⇒
∃ i, initial_env I i
∧ clos_refl_trans _ small_step i s.
Lemma reachable_in_sem (prg:memory) :
reachable prg ⊆ ⟦ prg ⟧.
Lemma sem_in_reachable (prg: memory) :
⟦prg⟧ ⊆ reachable(prg).
Definition upd_mem : memory → addr → int → memory := upd.
Definition encode_program (prg: list instruction) (m:memory) : memory × list int :=
@List.fold_left
(memory × list int) instruction
(λ m_n i,
let v := encode_instr i in
@List.fold_left
(memory × list int) int
(λ m_n j,
let (m, n) := m_n in
let (pp, ppl) := match n with hd::tl ⇒ (Int.add hd Int.one, n) | nil ⇒ (Int.zero, nil) end in
(upd_mem m pp j, pp::ppl))
v
m_n)
prg
(m, nil).