Require Import Classical Epsilon.
Require Import ssreflect ssrbool ssrnat.
Require Import Arith_ext ZArith_ext Lists_ext.
Require Import machine_int.
Import MachineInt.
Require Import mips_bipl.
Export mips_bipl.
Import expr_m.
Require while.

Local Close Scope positive_scope.
Local Open Scope heap_scope.

Definition immediate := int 16.
Definition shifta := int 5.
Inductive cmd0 : Type :=
| nop : cmd0
| add : reg -> reg -> reg -> cmd0
| addi : reg -> reg -> immediate -> cmd0
| addiu : reg -> reg -> immediate -> cmd0
| addu : reg -> reg -> reg -> cmd0
| cmd_and : reg -> reg -> reg -> cmd0
| andi : reg -> reg -> immediate -> cmd0
| lw : reg -> immediate -> reg -> cmd0
| lwxs : reg -> reg -> reg -> cmd0
| maddu : reg -> reg -> cmd0
| mfhi : reg -> cmd0
| mflhxu : reg -> cmd0
| mflo : reg -> cmd0
| movn : reg -> reg -> reg -> cmd0
| movz : reg -> reg -> reg -> cmd0
| msubu : reg -> reg -> cmd0
| mthi : reg -> cmd0
| mtlo : reg -> cmd0
| multu : reg -> reg -> cmd0
| nor : reg -> reg -> reg -> cmd0
| cmd_or : reg -> reg -> reg -> cmd0
| sll : reg -> reg -> shifta -> cmd0
| sllv : reg -> reg -> reg -> cmd0
| sltu : reg -> reg -> reg -> cmd0
| sra : reg -> reg -> shifta -> cmd0
| srl : reg -> reg -> shifta -> cmd0
| srlv : reg -> reg -> reg -> cmd0
| subu : reg -> reg -> reg -> cmd0
| sw : reg -> immediate -> reg -> cmd0
| xor : reg -> reg -> reg -> cmd0
| xori : reg -> reg -> immediate -> cmd0.

Lemma cmd0_dec_nop : forall c, { c = nop } + { c <> nop }.
Proof. elim=> //; (left; reflexivity) || (move=> *; right=> X //). Qed.

Local Open Scope mips_expr_scope.

Definition state := (store.t * heap.t)%type.

Local Open Scope machine_int_scope.
Local Open Scope zarith_ext_scope.

Delimit Scope mips_cmd_scope with mips_cmd.
Local Open Scope mips_cmd_scope.

Reserved Notation "s '--' c '---->' t" (at level 74 , no associativity).
Inductive exec0 : option state -> cmd0 -> option state -> Prop :=
| exec0_nop : forall st, Some st -- nop ----> Some st
| exec0_add : forall s h rd rs rt,
  - 2 ^^ 31 <= s2Z [rs]_s + s2Z [rt]_s < 2 ^^ 31 ->
  Some (s,h) -- add rd rs rt ----> Some (store.upd rd ([rs]_s [.+] [rt]_s) s, h)
| exec0_add_error : forall s h rd rs rt,
  ~ (- 2 ^^ 31 <= s2Z [rs]_s + s2Z [rt]_s < 2 ^^ 31) ->
  Some (s,h) -- add rd rs rt ----> None
| exec0_addi : forall s h rt rs imm,
  - 2 ^^ 31 <= s2Z [rs]_s + s2Z (sext 16 imm) < 2 ^^ 31 ->
  Some (s,h) -- addi rt rs imm ----> Some (store.upd rt ([rs]_s [.+] sext 16 imm) s,h)
| exec0_addi_error : forall s h rt rs imm,
  ~ (- 2 ^^ 31 <= s2Z ([rs]_s) + s2Z (sext 16 imm) < 2 ^^ 31) ->
  Some (s, h) -- addi rt rs imm ----> None
| exec0_addiu : forall s h rt rs imm,
  Some (s, h) -- addiu rt rs imm ----> Some (store.upd rt ([rs]_s [.+] sext 16 imm) s,h)
| exec0_addu : forall s h rd rs rt,
  Some (s,h) -- addu rd rs rt ----> Some (store.upd rd ([rs]_s [.+] [rt]_s) s,h)
| exec0_and : forall s h rd rs rt,
  Some (s,h) -- cmd_and rd rs rt ----> Some (store.upd rd ([rs]_s [.&] [rt]_s) s,h)
| exec0_andi : forall s h rt rs imm,
  Some (s,h) -- andi rt rs imm ----> Some (store.upd rt ([rs]_s [.&] zext 16 imm) s,h)
| exec0_lw : forall s h rt (off : immediate) base p z,
  u2Z ([base]_s [.+] sext 16 off) = 4 * Z_of_nat p -> heap.get p h = Some z ->
  Some (s,h) -- lw rt off base ----> Some (store.upd rt z s,h)
| exec0_lw_error : forall s h rt (off : immediate) base,
  ~ (exists l, u2Z ([base]_s [.+] sext 16 off) = 4 * Z_of_nat l /\ exists z, heap.get l h = Some z) ->
  Some (s,h) -- lw rt off base ----> None
| exec0_lwxs : forall s h rt idx base p z,
  u2Z ([base]_s [.+] ([idx]_s [.<<] 2)) = 4 * Z_of_nat p -> heap.get p h = Some z ->
  Some (s,h) -- lwxs rt idx base ----> Some (store.upd rt z s,h)
| exec0_lwxs_error : forall s h rt idx base,
  ~ (exists l, u2Z ([base]_s [.+] ([idx]_s [.<<] 2)) = 4 * Z_of_nat l /\ exists z, heap.get l h = Some z) ->
  Some (s,h) -- lwxs rt idx base ----> None
| exec0_maddu : forall s h rs rt,
  Some (s,h) -- maddu rs rt ----> Some (store.maddu_op ([rs]_s [.*] [rt]_s) s,h)
| exec0_mfhi : forall s h rd,
  Some (s, h) -- mfhi rd ----> Some (store.upd rd (store.hi s) s, h)
| exec0_mflhxu : forall s h rd,
  Some (s,h) -- mflhxu rd ----> Some (store.mflhxu_op (store.upd rd (store.lo s) s), h)
| exec0_mflo : forall s h rd,
  Some (s, h) -- mflo rd ----> Some (store.upd rd (store.lo s) s, h)
| exec0_movn_true : forall s h rd rs rt,
  [rt]_s <> zero32 ->
  Some (s, h) -- movn rd rs rt ----> Some (store.upd rd [rs]_s s, h)
| exec0_movn_false : forall s h rd rs rt,
  [rt]_s = zero32 -> Some (s, h) -- movn rd rs rt ----> Some (s, h)
| exec0_movz_true : forall s h rd rs rt,
  [rt]_s = zero32 ->
  Some (s, h) -- movz rd rs rt ----> Some (store.upd rd [rs]_s s, h)
| exec0_movz_false : forall s h rd rs rt,
  [rt]_s <> zero32 -> Some (s, h) -- movz rd rs rt ----> Some (s, h)
| exec0_msubu : forall s h rs rt,
  Some (s, h) -- msubu rs rt ----> Some (store.msubu_op ([rs]_s [.*] [rt]_s) s, h)
| exec0_mthi : forall s h rs,
  Some (s, h) -- mthi rs ----> Some (store.mthi_op [rs]_s s, h)
| exec0_mtlo : forall s h rs,
  Some (s, h) -- mtlo rs ----> Some (store.mtlo_op [rs]_s s, h)
| exec0_multu : forall s h rs rt,
  Some (s, h) -- multu rs rt ----> Some (store.multu_op ([rs]_s [.*] [rt]_s) s, h)
| exec0_nor : forall s h rd rs rt,
  Some (s, h) -- nor rd rs rt ----> Some (store.upd rd (int_not ([rs]_s [.|] [rt]_s)) s, h)
| exec0_or : forall s h rd rs rt,
  Some (s, h) -- cmd_or rd rs rt ----> Some (store.upd rd ([rs]_s [.|] [rt]_s) s, h)
| exec0_sll : forall s h rx ry sa,
  Some (s,h) -- sll rx ry sa ----> Some (store.upd rx ([ry]_s [.<<] Zabs_nat (u2Z sa)) s,h)
| exec0_sllv : forall s h rd rt rs,
  Some (s,h) -- sllv rd rt rs ----> Some (store.upd rd ([rt]_s[.<<]Zabs_nat (u2Z ([rs]_s [.%] 5))) s,h)
| exec0_sltu : forall s h rd rs rt flag,
  flag = (if Zlt_bool (u2Z [rs]_s) (u2Z [rt]_s) then one32 else zero32) ->
  Some (s,h) -- sltu rd rs rt ----> Some (store.upd rd flag s,h)
| exec0_sra : forall s h rd rt sa,
  Some (s,h) -- sra rd rt sa ----> Some (store.upd rd (shra (Zabs_nat (u2Z sa)) [rt]_s) s,h)
| exec0_srl : forall s h rd rt sa,
  Some (s,h) -- srl rd rt sa ----> Some (store.upd rd ([rt]_s[.>>]Zabs_nat (u2Z sa)) s,h)
| exec0_srlv : forall s h rd rt rs,
  Some (s,h) -- srlv rd rt rs ----> Some (store.upd rd ([rt]_s[.>>]Zabs_nat (u2Z ([rs]_s [.%] 5))) s,h)
| exec0_subu : forall s h rd rs rt,
  Some (s,h) -- subu rd rs rt ----> Some (store.upd rd ([rs]_s [.+] (cplt2 [rt]_s)) s,h)
| exec0_sw : forall s h rt (off : immediate) base p,
  u2Z ([base]_s [.+] sext 16 off) = 4 * Z_of_nat p -> (exists z, heap.get p h = Some z) ->
  Some (s,h) -- sw rt off base ----> Some (s,heap.upd p [rt]_s h)
| exec0_sw_err : forall s h rt (off : immediate) base,
  ~ (exists l, u2Z ([base]_s [.+] sext 16 off) = 4 * Z_of_nat l /\ exists z, heap.get l h = Some z) ->
  Some (s,h) -- sw rt off base ----> None
| exec0_xor : forall s h rd rs rt,
  Some (s,h) -- xor rd rs rt ----> Some (store.upd rd (int_xor [rs]_s [rt]_s) s,h)
| exec0_xori : forall s h rt rs imm,
  Some (s,h) -- xori rt rs imm ----> Some (store.upd rt (int_xor [rs]_s (zext 16 imm)) s,h)
where "s -- c ----> t" := (exec0 s c t) : mips_cmd_scope.

Lemma exec0_nop_inv : forall s s', Some s -- nop ----> s' -> s' = Some s.
Proof. move=> s s'; by inversion 1. Qed.

Lemma exec0_addi_inv : forall s h rt rs imm s',
  Some (s, h) -- addi rt rs imm ----> s' ->
  - 2 ^^ 31 <= s2Z [rs]_s + s2Z (sext 16 imm) < 2 ^^ 31 /\
  s' = Some (store.upd rt ([rs]_s [.+] sext 16 imm) s, h)
  \/
  ~ (- 2 ^^ 31 <= s2Z [rs]_s + s2Z (sext 16 imm) < 2 ^^ 31) /\
  s' = None.
Proof. move=> s h rt rs imm s'. inversion 1; tauto. Qed.

Lemma exec0_addiu_inv : forall s h rt rs imm s',
  Some (s, h) -- addiu rt rs imm ----> s' ->
  s' = Some (store.upd rt ([rs]_s [.+] sext 16 imm) s, h).
Proof. move=> s h rt rs imm s'. by inversion 1. Qed.

Lemma exec0_add_inv : forall s h rd rs rt s',
  Some (s,h) -- add rd rs rt ----> s' ->
  - 2 ^^ 31 <= s2Z [rs]_s + s2Z [rt]_s < 2 ^^ 31 /\
  s' = Some (store.upd rd ([rs]_s [.+] [rt]_s) s,h)
  \/
  ~ (- 2 ^^ 31 <= s2Z [rs]_s + s2Z [rt]_s < 2 ^^ 31) /\
  s' = None.
Proof. move=> s h rd rs rt s'. inversion 1; tauto. Qed.

Lemma exec0_addu_inv : forall s h rd rs rt s',
  Some (s,h) -- addu rd rs rt ----> s' ->
  s' = Some (store.upd rd ([rs]_s [.+] [rt]_s) s,h).
Proof. move=> s h rd rs rt s'; by inversion 1. Qed.

Lemma exec0_and_inv : forall s h rd rs rt s',
  Some (s,h) -- cmd_and rd rs rt ----> s' ->
  s' = Some (store.upd rd ([rs]_s [.&] [rt]_s) s,h).
Proof. move=> s h rd rs rt s'; by inversion 1. Qed.

Lemma exec0_andi_inv : forall s h rt rs imm s',
  Some (s,h) -- andi rt rs imm ----> s' ->
  s' = Some (store.upd rt ([rs]_s [.&] zext 16 imm) s,h).
Proof. move=> s h rt rs imm s'; by inversion 1. Qed.

Lemma exec0_lw_inv : forall s h rt (off : immediate) base s',
  Some (s,h) -- lw rt off base ----> s' ->
  (exists p, u2Z ([base]_s [.+] sext 16 off) = 4 * Z_of_nat p /\ exists z, heap.get p h = Some z /\
    s' = Some (store.upd rt z s,h))
    \/
  ~ (exists l, u2Z ([base]_s [.+] sext 16 off) = 4 * Z_of_nat l /\ exists z, heap.get l h = Some z) /\
  s' = None.
Proof.
move=> s h rt off base s'.
inversion 1; subst.
left; exists p; split=> //; by exists z.
by right.
Qed.

Lemma exec0_lwxs_inv : forall s h rt idx base s',
  Some (s,h) -- lwxs rt idx base ----> s' ->
  (exists p, u2Z ([base]_s [.+] ([idx]_s [.<<] 2)) = 4 * Z_of_nat p /\ exists z, heap.get p h = Some z /\ s' = Some (store.upd rt z s, h))
  \/
  ~ (exists l, u2Z ([base]_s [.+] ([idx]_s [.<<] 2)) = 4 * Z_of_nat l /\ exists z, heap.get l h = Some z) /\ s' = None.
Proof.
move=> s h rt off base s'.
inversion 1; subst.
left; exists p; split=> //; by exists z.
by right.
Qed.

Lemma exec0_maddu_inv : forall s h rs rt s',
  Some (s, h) -- maddu rs rt ----> s' ->
  s' = Some (store.maddu_op ([rs]_s [.*] [rt]_s) s, h).
Proof. move=> s h rs rt s'; by inversion 1. Qed.

Lemma exec0_mfhi_inv : forall s h rd s',
  Some (s, h) -- mfhi rd ----> s' ->
  s' = Some (store.upd rd (store.hi s) s, h).
Proof. move=> s h rd s'; by inversion 1. Qed.

Lemma exec0_mflhxu_inv : forall s h rd s',
  Some (s,h) -- mflhxu rd ----> s' ->
  s' = Some (store.mflhxu_op (store.upd rd (store.lo s) s), h).
Proof. move=> s h rd s'; by inversion 1. Qed.

Lemma exec0_mflo_inv : forall s h rd s',
  Some (s, h) -- mflo rd ----> s' ->
  s' = Some (store.upd rd (store.lo s) s, h).
Proof. move=> s h rd s'; by inversion 1. Qed.

Lemma exec0_movn_inv : forall s h rd rs rt s',
  Some (s, h) -- movn rd rs rt ----> s' ->
  [rt]_s <> zero32 /\ s' = Some (store.upd rd [rs]_s s, h)
  \/
  [rt]_s = zero32 /\ s' = Some (s, h).
Proof. move=> s h rd rs rt s'; by inversion 1; auto. Qed.

Lemma exec0_movz_inv : forall s h rd rs rt s',
  Some (s, h) -- movz rd rs rt ----> s' ->
  [rt]_s = zero32 /\ s' = Some (store.upd rd [rs]_s s, h)
  \/
  [rt]_s <> zero32 /\ s' = Some (s, h).
Proof. move=> s h rd rs rt s'; by inversion 1; auto. Qed.

Lemma exec0_msubu_inv : forall s h rs rt s',
  Some (s, h) -- msubu rs rt ----> s' ->
  s' = Some (store.msubu_op ([rs]_s [.*] [rt]_s) s, h).
Proof. move=> s h rs rt s'; by inversion 1. Qed.

Lemma exec0_mthi_inv : forall s h rs s',
  Some (s, h) -- mthi rs ----> s' ->
  s' = Some (store.mthi_op [rs]_s s, h).
Proof. move=> s h rs s'; by inversion 1. Qed.

Lemma exec0_mtlo_inv : forall s h rs s',
  Some (s, h) -- mtlo rs ----> s' ->
  s' = Some (store.mtlo_op [rs]_s s, h).
Proof. move=> s h rs s'; by inversion 1. Qed.

Lemma exec0_multu_inv : forall s h rs rt s',
  Some (s, h) -- multu rs rt ----> s' ->
  s' = Some (store.multu_op ([rs]_s [.*] [rt]_s) s, h).
Proof. move=> s h rs rt s'; by inversion 1. Qed.

Lemma exec0_nor_inv : forall s h rd rs rt s',
  Some (s, h) -- nor rd rs rt ----> s' ->
  s' = Some (store.upd rd (int_not ([rs]_s [.|] [rt]_s)) s, h).
Proof. move=> s h rd rs rt s'; by inversion 1. Qed.

Lemma exec0_or_inv : forall s h rd rs rt s',
  Some (s, h) -- cmd_or rd rs rt ----> s' ->
  s' = Some (store.upd rd ([rs]_s [.|] [rt]_s) s, h).
Proof. move=> s h rd rs rt s'; by inversion 1. Qed.

Lemma exec0_sll_inv : forall s h rx ry sa s',
  Some (s,h) -- sll rx ry sa ----> s' ->
  s' = Some (store.upd rx ([ry]_s [.<<] Zabs_nat (u2Z sa)) s,h).
Proof. move=> s h rx ry sa s'; by inversion 1. Qed.

Lemma exec0_sllv_inv : forall s h rd rt rs s',
  Some (s,h) -- sllv rd rt rs ----> s' ->
  s' = Some (store.upd rd ([rt]_s[.<<]Zabs_nat (u2Z ([rs]_s [.%] 5))) s, h).
Proof. move=> s h rd rt rs s'; by inversion 1. Qed.

Lemma exec0_sltu_inv : forall s h rd rs rt s',
  Some (s,h) -- sltu rd rs rt ----> s' ->
  s' = Some (store.upd rd (if Zlt_bool (u2Z [rs]_s) (u2Z [rt]_s) then one32 else zero32) s, h).
Proof. move=> s h rd rt rs s'; by inversion 1; subst. Qed.

Lemma exec0_sra_inv : forall s h rd rt sa s',
  Some (s,h) -- sra rd rt sa ----> s' ->
  s' = Some (store.upd rd (shra (Zabs_nat (u2Z sa)) [rt]_s) s, h).
Proof. move=> s h rd rt sa s'; by inversion 1. Qed.

Lemma exec0_srl_inv : forall s h rd rt sa s',
  Some (s,h) -- srl rd rt sa ----> s' ->
  s' = Some (store.upd rd ([rt]_s [.>>] Zabs_nat (u2Z sa)) s, h).
Proof. move=> s h rd rt sa s'; by inversion 1. Qed.

Lemma exec0_srlv_inv : forall s h rd rt rs s',
  Some (s,h) -- srlv rd rt rs ----> s' ->
  s' = Some (store.upd rd ([rt]_s [.>>] Zabs_nat (u2Z ([rs]_s [.%] 5))) s, h).
Proof. move=> s h rd rt rs s'; by inversion 1. Qed.

Lemma exec0_subu_inv : forall s h rd rs rt s',
  Some (s,h) -- subu rd rs rt ----> s' ->
  s' = Some (store.upd rd ([rs]_s [.+] (cplt2 [rt]_s)) s,h).
Proof. move=> s h rd rs rt s'; by inversion 1. Qed.

Lemma exec0_sw_inv : forall s h rt (off : immediate) base s',
  Some (s,h) -- sw rt off base ----> s' ->
  (exists p, u2Z ([base]_s [.+] sext 16 off) = 4 * Z_of_nat p /\ exists z, heap.get p h = Some z /\ s' = Some (s,heap.upd p [rt]_s h))
  \/
  ~ (exists l, u2Z ([base]_s [.+] sext 16 off) = 4 * Z_of_nat l /\ exists z, heap.get l h = Some z) /\ s' = None.
Proof.
move=> s h rt off base s'; inversion 1; subst.
- left; exists p; split=> //.
  case: H7 => z H7.
  by exists z.
- by right.
Qed.

Lemma exec0_xor_inv : forall s h rd rs rt s',
  Some (s,h) -- xor rd rs rt ----> s' ->
  s' = Some (store.upd rd ([rs]_s [.(+)] [rt]_s) s,h).
Proof. move=> s h rd rs rt s'; by inversion 1. Qed.

Lemma exec0_xori_inv : forall s h rt rs imm s',
  Some (s, h) -- xori rt rs imm ----> s' ->
  s' = Some (store.upd rt ([rs]_s [.(+)] zext 16 imm) s, h).
Proof. move=> s h rt rs imm s'; by inversion 1. Qed.

Lemma exec0_deter : forall st c st',
  st -- c ----> st' -> forall st'', st -- c ----> st'' -> st' = st''.
Proof.
move=> st c st'; elim=> //; clear st c st'.
- move=> st st'; by move/exec0_nop_inv.
- move=> s h rd rs rt H s'.
  case/exec0_add_inv; last by tauto.
  by case=> _ ->.
- move=> s h rt rs imm H s'.
  case/exec0_add_inv; first by tauto.
  by case.
- move=> s h rt rs imm H s'.
  case/exec0_addi_inv; last by tauto.
  by case=> _ ->.
- move=> s h rt rs imm H s'.
  case/exec0_addi_inv; first by tauto.
  by case.
- move=> s h rt rs imm s'; by move/exec0_addiu_inv.
- move=> s h rd rs rt s'; by move/exec0_addu_inv.
- move=> s h rd rs rt s'; by move/exec0_and_inv.
- move=> s h rd rs rt s'; by move/exec0_andi_inv.
- move=> s h rt off base p z Hp Hz s'.
  case/exec0_lw_inv.
  move=> [p' [Hp' [z' [Hz' Hs']]]].
  have [->//] : z = z'.
    have X : p = p' by omega.
    subst.
    rewrite Hz' in Hz; by case: Hz.
  move=> X.
  suff : False by done.
  apply X.
  exists p; split => //; by exists z.
- move=> s h rt off base X s'.
  case/exec0_lw_inv.
  move=> [p [Hp [z [Hz Hs']]]].
  have [//] : False.
    apply X.
    exists p; split => //; by exists z.
  by case.
- move=> s h rt off base p z Hp Hz s'.
  case/exec0_lwxs_inv.
  move=> [p' [Hp' [z' [Hz' Hs']]]].
  have [->//] : z = z'.
    have X : p = p' by omega.
    subst.
    rewrite Hz' in Hz; by case: Hz.
  move=> X.
  suff : False by done.
  apply X.
  exists p; split => //; by exists z.
- move=> s h rt off base X s'.
  case/exec0_lwxs_inv.
  move=> [p [Hp [z [Hz Hs']]]].
  have [//] : False.
    apply X.
    exists p; split => //; by exists z.
  by case.
- move=> s h rs rt s'; by move/exec0_maddu_inv.
- move=> s h rd s'; by move/exec0_mfhi_inv.
- move=> s h rd s'; by move/exec0_mflhxu_inv.
- move=> s h rd s'; by move/exec0_mflo_inv.
- move=> s h rd rs rt H st''.
  case/exec0_movn_inv.
  case=> _ -> //.
  by case.
- move=> s h rd rs rt H st''.
  case/exec0_movn_inv.
  case=> //.
  by case=> _ ->.
- move=> s h rd rs rt H' st''.
  case/exec0_movz_inv.
  case=> _ -> //.
  by case.
- move=> s h rd rs rt H' st''.
  case/exec0_movz_inv.
  case=> //.
  by case=> _ ->.
- move=> s h rs rt st''; by move/exec0_msubu_inv.
- move=> s h rs st''; by move/exec0_mthi_inv.
- move=> s h rs st''; by move/exec0_mtlo_inv.
- move=> s h rs rt st''; by move/exec0_multu_inv.
- move=> s h rd rs rt st''; by move/exec0_nor_inv.
- move=> s h rd rs rt st''; by move/exec0_or_inv.
- move=> s h rx ry sa st''; by move/exec0_sll_inv.
- move=> s h rd rs st st''; by move/exec0_sllv_inv.
- move=> s h rd rs rt flag H' st''; by move/exec0_sltu_inv; subst.
- move=> s h rd rt sa st''; by move/exec0_sra_inv.
- move=> s h rd rt sa st''; by move/exec0_srl_inv.
- move=> s h rd rt rs st''; by move/exec0_srlv_inv.
- move=> s h rd rs rt st''; by move/exec0_subu_inv; subst.
- move=> s h rt off base p Hp [z Hz] st''.
  case/exec0_sw_inv.
  move=> [p' [Hp' [z' [Hz' ->]]]].
  have [->//] : p = p' by omega.
  move=> X.
  suff : False by done.
  apply X.
  exists p; split => //; by exists z.
- move=> s h rt off base X s'.
  case/exec0_sw_inv.
  move=> [p [Hp [z [Hz Hs']]]].
  have [//] : False.
    apply X.
    exists p; split => //; by exists z.
  by case.
- move=> s h rd rs rt st''; by move/exec0_xor_inv.
- move=> s h rt rs imm st''; by move/exec0_xori_inv.
Qed.

Coercion cmd_cmd0_coercion := @while.cmd_cmd0 cmd0 expr_b.

Notation "c ; d" := (while.seq c d) (at level 81, right associativity) : mips_cmd_scope.
Notation "'ifte_beq' a ',' b 'thendo' x 'elsedo' y" := (while.ifte (beq a b) x y) (at level 80) : mips_cmd_scope.
Notation "'ifte_bltz' a 'thendo' x 'elsedo' y" := (while.ifte (bltz a) x y) (at level 80) : mips_cmd_scope.

Notation "s -- c ---> t" := (@while.exec store.t heap.t _ exec0 _
  (fun eb st => eval_b eb (fst st)) s c t) (at level 74, no associativity) : mips_cmd_scope.

Lemma from_none0 : forall (c : cmd0) s, None -- c ----> s -> s = None.
Proof. by inversion 1. Qed.

Lemma cmd0_terminate : forall (c : cmd0) s, exists s', Some s -- c ----> s'.
Proof.
elim=> //.
- move=> s; exists (Some s); apply exec0_nop.
- move=> g g0 g1 [s h].
  case: (classic (-2 ^^ 31 <= s2Z [g0]_s + s2Z [g1]_s < 2 ^^ 31))=> X.
  + eapply ex_intro; by constructor.
  + exists None; by constructor.
- move=> g g0 i [s h].
  case: (classic (- 2 ^^ 31 <= s2Z [g0]_s + s2Z (sext 16 i) < 2 ^^ 31))=> X.
  + eapply ex_intro; by constructor.
  + exists None; by constructor.
- move=> ? ? ? [s h]; eapply ex_intro; by constructor.
- move=> ? ? ? [s h]; eapply ex_intro; by constructor.
- move => ? ? ? [s h]; eapply ex_intro; by constructor.
- move => ? ? ? [s h]; eapply ex_intro; by constructor.
- move => g i g0 [s h].
  case: (classic (exists l, u2Z ([g0]_s [.+] sext 16 i) = 4 * Z_of_nat l /\ exists z, heap.get l h = Some z)) => X.
  + case: X => l [H [z H']].
    exists (Some (store.upd g z s,h)); by apply (exec0_lw _ _ _ _ _ _ _ H).
  + exists None; by constructor.
- move => g g0 g1 [s h].
  case: (classic (exists l, (u2Z ([g1]_s [.+] shl 2 [g0]_s) = 4 * Z_of_nat l)%Z /\ (exists z, heap.get l h = Some z))) => X.
  + case: X => l [H [z H']].
    exists (Some (store.upd g z s,h)); by apply (exec0_lwxs _ _ _ _ _ _ _ H).
  + exists None; by constructor.
- move=> ? ? [s h]; eapply ex_intro; by constructor.
- move=> ? [s h]; eapply ex_intro; by constructor.
- move=> ? [s h]; eapply ex_intro; by constructor.
- move=> ? [s h]; eapply ex_intro; by constructor.
- move=> rd rs rt [s h].
  case: (dec_int [rt]_s zero32) => X.
  + exists (Some (s, h)); by constructor.
  + exists (Some (store.upd rd [rs]_s s,h)); by constructor.
- move=> rd rs rt [s h].
  elim: (dec_int [rt]_s zero32) => X.
  + exists (Some (store.upd rd [rs]_s s,h)); by constructor.
  + exists (Some (s,h)); by constructor.
- move=> ? ? [s h]; eapply ex_intro; by constructor.
- move=> ? [s h]; eapply ex_intro; by constructor.
- move=> ? [s h]; eapply ex_intro; by constructor.
- move=> ? ? [s h]; eapply ex_intro; by constructor.
- move=> ? ? ? [s h]; eapply ex_intro; by constructor.
- move=> ? ? ? [s h]; eapply ex_intro; by constructor.
- move=> ? ? ? [s h]; eapply ex_intro; by constructor.
- move=> ? ? ? [s h]; eapply ex_intro; by constructor.
- move=> ? ? ? [s h]; eapply ex_intro; by constructor.
- move=> ? ? ? [s h]; eapply ex_intro; by constructor.
- move=> ? ? ? [s h]; eapply ex_intro; by constructor.
- move=> ? ? ? [s h]; eapply ex_intro; by constructor.
- move=> ? ? ? [s h]; eapply ex_intro; by constructor.
- move=> g i g0 [s h].
  case: (classic (exists p,
    u2Z ([g0]_s [.+] sext 16 i) = 4 * Z_of_nat p /\
    (exists z, heap.get p h = Some z))) => X.
  + case: X => p [ H1 [z H2]].
    exists (Some (s, heap.upd p [g]_s h)). apply (exec0_sw _ _ _ _ _ _ H1). by exists z.
  + exists None; by constructor.
- move=> ? ? ? [s h]; eapply ex_intro; by constructor.
- move=> ? ? ? [s h]; eapply ex_intro; by constructor.
Qed.

Module WMIPS_Semop <: while.WHILE_SEMOP.

Definition store : Type := store.t.
Definition heap : Type := heap.t.
Definition state : Type := (store * heap)%type.

Definition cmd0 : Type := cmd0.
Definition exec0 : option state -> cmd0 -> option state -> Prop := exec0.
Notation "s -- c ----> t" := (exec0 s c t) (at level 74 , no associativity) : goto_cmd_scope.
Local Open Scope goto_cmd_scope.

Definition from_none0 : forall c s, None -- c ----> s -> s = None := from_none0.
Definition cmd0_terminate : forall (c : cmd0) s, exists s', Some s -- c ----> s' := cmd0_terminate.

Local Close Scope goto_cmd_scope.

Definition expr_b : Type := expr_b.
Definition neg : expr_b -> expr_b := neg.
Definition eval_b : expr_b -> state -> bool := fun eb s => eval_b eb (fst s).
Lemma eval_b_neg : forall t s, eval_b (neg t) s = ~~ eval_b t s.
Proof. move=> eb [s h]; rewrite /eval_b /=; by apply eval_b_neg. Qed.
Definition cmd := @while.cmd cmd0 expr_b.
Coercion cmd_cmd0_coercion := @while.cmd_cmd0 cmd0 expr_b.
Definition exec : option state -> cmd -> option state -> Prop := @while.exec store heap cmd0 exec0 expr_b
  (fun eb s => eval_b eb (s)).

End WMIPS_Semop.

Module WMIPS_Semop_Deter <: while.WHILE_SEMOP_DETER.

Include WMIPS_Semop.

Definition exec0_deter : forall (st : option state) (c : cmd0) (st' : option state),
  st -- c ----> st' ->
  forall st'', st -- c ----> st'' -> st' = st'' := exec0_deter.

End WMIPS_Semop_Deter.

Module semop_prop_m := while.While_Semop_Prop WMIPS_Semop.

Lemma exec0_add_not_None: forall s h g g0 g1,
  ~ Some (s, h) -- add g g0 g1 ----> None ->
  - 2 ^^ 31 <= s2Z [g0]_s + s2Z [g1]_s < 2 ^^ 31.
Proof. move=> ? ? ? ? ? H; apply NNPP; contradict H; do ! constructor=> //. Qed.

Lemma exec0_addi_not_None: forall s h g g0 i,
  ~ Some (s, h) -- addi g g0 i ----> None ->
  - 2 ^^ 31 <= s2Z [g0]_s + s2Z (sext 16 i) < 2 ^^ 31.
Proof. move=> ? ? ? ? ? H; apply NNPP. contradict H. do ! constructor=> //. Qed.

Lemma exec0_lw_not_None: forall s h g i g0 ,
  ~ Some (s, h) -- lw g i g0 ----> None ->
  exists p, u2Z ([ var_e g0 ]e_ s [.+] sext 16 i) = 4 * Z_of_nat p /\
    exists z, heap.get p h = Some z.
Proof. move=> ? ? ? ? ? H; apply NNPP. contradict H. do ! constructor=> //. Qed.

Lemma exec0_lwxs_not_None: forall s h g g0 g1,
  ~ Some (s, h) -- lwxs g g0 g1 ----> None ->
  exists p, u2Z ([g1]_s [.+] ([g0]_s [.<<] 2)) = 4 * Z_of_nat p /\
    exists z, heap.get p h = Some z.
Proof. move=> ? ? ? ? ? H. apply NNPP. contradict H. repeat constructor=> //. Qed.

Lemma exec0_sw_not_None: forall s h g i g0,
  ~ Some (s, h) -- sw g i g0 ----> None ->
  exists p, u2Z ([ var_e g0 ]e_s [.+] sext 16 i) = 4 * Z_of_nat p /\
    exists z, heap.get p h = Some z.
Proof. move=> ? ? ? ? ? H. apply NNPP. contradict H. repeat constructor=> //. Qed.

Lemma exec0_not_None_to_exec_not_None : forall (s : WMIPS_Semop.store) (h : WMIPS_Semop.heap) (c : cmd0),
  ~ (Some (s, h) -- c ---> None) -> ~ Some (s, h) -- c ----> None.
Proof.
move=> s h c H H'.
apply H.
by apply while.exec_cmd0.
Qed.

Local Close Scope zarith_ext_scope.

Lemma cmd0_terminate' : forall (c : cmd0) s, exists s', Some s -- c ---> s'.
Proof. move=> c s. case: (cmd0_terminate c s) => s' H. exists s'; by apply while.exec_cmd0. Qed.

Lemma exists_exec_seq_assoc'_P : forall s c0 c1 c2 P,
  {s' | s -- c0 ; c1 ; c2 ---> s' /\ P s'} ->
  {s' | s -- (c0 ; c1) ; c2 ---> s' /\ P s'}.
Proof.
move=> s c0 c1 c2 P [s' H]. exists s'.
split; last by tauto.
apply semop_prop_m.exec_seq_assoc'; tauto.
Qed.

Lemma exists_addiu_seq : forall rt rs (i : int 16) c s h,
  {s' | Some (store.upd rt ([rs]_s [.+] sext 16 i) s, h) -- c ---> s'} ->
  {s' | Some (s, h) -- addiu rt rs i; c ---> s'}.
Proof.
move=> rt rs imm c s h [s' H].
exists s'; eapply while.exec_seq; eauto.
do 2 constructor.
Qed.

Lemma exists_nop : forall s, { s' | Some s -- nop ---> s' }.
Proof. move=> s; exists (Some s); by do 2 constructor. Qed.

Lemma exists_nop_P : forall s (P : state -> Prop), P s ->
  {s' | Some s -- nop ---> s' /\ forall st, s' = Some st -> P st}.
Proof.
move=> s P HP; exists (Some s); split.
by do 2 constructor.
by move=> st [] <-.
Qed.

Lemma exists_addiu : forall rt rs (imm : int 16) s h,
  {s' | Some (s, h) -- addiu rt rs imm ---> s'}.
Proof.
move=> rt rs imm s h.
exists (Some (store.upd rt ([rs]_s [.+] sext 16 imm) s, h)).
by do 2 constructor.
Qed.

Lemma exists_addiu_P : forall rt rs (imm : int 16) s h (P : state -> Prop),
  P (store.upd rt ([rs]_s [.+] sext 16 imm) s, h) ->
  {s' | Some (s, h) -- addiu rt rs imm ---> s' /\ forall st, s' = Some st -> P st}.
Proof.
move=> rt rs imm s h P H.
exists (Some (store.upd rt ([rs]_s [.+] sext 16 imm) s, h)); split => //.
do 2 constructor.
move=> st [] <- //.
Qed.

Lemma exists_addiu_seq_P : forall rt rs (imm : int 16) c s h P,
  {s' | Some (store.upd rt ([rs]_s [.+] sext 16 imm) s, h) -- c ---> s' /\ P s'} ->
  {s' | Some (s, h) -- addiu rt rs imm ; c ---> s' /\ P s' }.
Proof.
move=> rt rs imm c s h P [s' [H HP]].
exists s'; split => //.
eapply while.exec_seq; eauto.
by do 2 constructor.
Qed.

Lemma exists_and_P : forall rd rs rt s h (P:state -> Prop),
  P (store.upd rd ([rs]_s [.&] [rt]_s) s, h) ->
  {s' | Some (s, h) -- cmd_and rd rs rt ---> s' /\ forall st, s' = Some st -> P st }.
Proof.
move=> rd rs rt s h P HP.
exists (Some (store.upd rd ([rs]_s [.&] [rt]_s) s, h)); split => //.
by do 2 constructor.
by move=> st [] <-.
Qed.

Lemma exists_andi_seq_P : forall rt rs (imm : int 16) c s h P,
  {s' | Some (store.upd rt ([rs]_s [.&] zext 16 imm) s, h) -- c ---> s' /\ P s'} ->
  {s' | Some (s, h) -- andi rt rs imm; c ---> s' /\ P s' }.
Proof.
move=> rt rs imm c s h P [s' [H HP]].
exists s'; split => //.
eapply while.exec_seq; eauto.
by do 2 constructor.
Qed.

Lemma exists_mthi_seq_P : forall rs c s h P,
  {s' | Some (store.mthi_op [rs]_s s, h) -- c ---> s' /\ P s'} ->
  {s' | Some (s, h) -- mthi rs; c ---> s' /\ P s' }.
Proof.
move=> rs c s h P [s' [H HP]].
exists s'; split => //.
eapply while.exec_seq; eauto; do 2 constructor.
Qed.

Lemma exists_mflhxu_seq_P : forall rd c s h P,
  {s' | Some (store.mflhxu_op (store.upd rd (store.lo s) s), h) -- c ---> s' /\ P s'} ->
  {s' | Some (s, h) -- mflhxu rd; c ---> s' /\ P s' }.
Proof.
move=> rd c s h P [s' [H HP]].
exists s'; split => //.
eapply while.exec_seq; eauto; do 2 constructor.
Qed.

Lemma exists_mtlo_P : forall rs s h (P : state -> Prop),
  P (store.mtlo_op [rs]_s s, h) ->
  {s' | Some (s, h) -- mtlo rs ---> s' /\ forall st, s' = Some st -> P st }.
Proof.
move=> rs s h P H.
exists (Some (store.mtlo_op [rs]_s s, h)); split => //.
do 2 constructor.
by move=> st [] <-.
Qed.

Lemma exists_sll_seq_P : forall rx ry sa c s h P,
  {s' | (Some (store.upd rx ([ry]_s [.<<] Zabs_nat (u2Z sa)) s, h) -- c ---> s') /\ P s'} ->
  {s' | (Some (s, h) -- sll rx ry sa; c ---> s') /\ P s' }.
Proof.
move=> rx ry sa c s h P [s' [H HP]].
exists s'; split => //.
eapply while.exec_seq; eauto; do 2 constructor.
Qed.

Lemma exists_sllv_seq_P : forall rd rt rs c s h P,
  {s' | Some (store.upd rd ([rt]_s [.<<] Zabs_nat (u2Z ([rs]_s [.%] 5))) s, h) -- c ---> s' /\ P s'} ->
  {s' | Some (s, h) -- sllv rd rt rs; c ---> s' /\ P s' }.
Proof.
move=> rd rt rs c s h P [s' [H HP]].
exists s'; split => //.
eapply while.exec_seq; eauto; do 2 constructor.
Qed.

Lemma exists_sra_seq_P : forall rd rt sa c s h P,
  {s' | (Some (store.upd rd (shra (Zabs_nat (u2Z sa)) [rt]_s) s, h) -- c ---> s') /\ P s'} ->
  {s' | (Some (s, h) -- sra rd rt sa; c ---> s')/\ P s' }.
Proof.
move=> rd rt sa c s h P [s' [H HP]].
exists s'; split => //.
eapply while.exec_seq; [by apply while.exec_cmd0, exec0_sra | exact H].
Qed.

Lemma exists_srl_seq_P : forall rd rt sa c s h P,
  {s' | (Some (store.upd rd ([rt]_s [.>>] Zabs_nat (u2Z sa)) s, h) -- c ---> s') /\ P s'} ->
  {s' | (Some (s, h) -- srl rd rt sa; c ---> s')/\ P s' }.
Proof.
move=> rd rt sa c s h P [s' [H HP]].
exists s'; split => //.
eapply while.exec_seq; eauto; do 2 constructor.
Qed.

Lemma exists_or_seq_P : forall rd rs rt c s h P,
  {s' | Some (store.upd rd ([rs]_s [.|] [rt]_s) s, h) -- c ---> s' /\ P s'} ->
  {s' | Some (s, h) -- cmd_or rd rs rt; c ---> s' /\ P s' }.
Proof.
move=> rd rs rt c s h P [s' [H HP]].
exists s'; split => //.
eapply while.exec_seq; eauto; do 2 constructor.
Qed.

Lemma exists_seq : forall c1 c2 s,
  (exists si, s -- c1 ---> si /\ exists s', si -- c2 ---> s') ->
  (exists s' , s -- c1 ; c2 ---> s').
Proof. move=> c1 c2 s [si [H1 [s' H2]]]. exists s'; by apply while.exec_seq with si. Qed.

Lemma exists_seq_P : forall c1 c2 s (P : state -> Prop) Q,
  {si | Some s -- c1 ---> si /\ Q si} ->
  (forall si, Q si -> {s' | (si -- c2 ---> s') /\ forall st, s' = Some st -> P st}) ->
  {s' | Some s -- c1 ; c2 ---> s' /\ forall st, s' = Some st -> P st }.
Proof.
move=> c1 c2 s P Q [si [Hc1 Hsi]] Hc2.
case: {Hc2}(Hc2 _ Hsi) => sf [Hc2 HPsf].
exists sf; split; [by eapply while.exec_seq; eauto | exact HPsf].
Qed.

Lemma exists_seq_P2 : forall c1 c2 s (Q : state -> Prop),
  {si | Some s -- c1 ---> si /\ forall st, si = Some st -> Q st} ->
  (forall si, Q si -> {s' | Some si -- c2 ---> s' }) ->
  {s' | Some s -- c1 ; c2 ---> s' }.
Proof.
move=> c1 c2 s Q [si [Hc1 Hsi]] Hc2.
destruct si as [si|].
- move: {Hsi}(Hsi _ (refl_equal _)) => Hsi.
  case: {Hc2}(Hc2 _ Hsi) => s' Hc2; exists s'. by eapply while.exec_seq; eauto.
- exists None.
  move/while.exec_seq : Hc1; apply. by apply while.exec_none.
Qed.

Lemma exists_ifte : forall s (c1 c2 : while.cmd) bt,
  { s' | Some s -- c1 ---> s' } -> { s' | Some s -- c2 ---> s' } ->
  { s' | Some s -- while.ifte bt c1 c2 ---> s' }.
Proof.
move=> s c1 c2 bt [s'1 H1] [s'2 H2].
apply constructive_indefinite_description.
case/orP : (orbN (eval_b bt (fst s))) => Hbt.
- exists s'1; by apply while.exec_ifte_true.
- exists s'2; apply while.exec_ifte_false => //; by apply/negP.
Qed.

Lemma exists_ifte_P : forall s (c1 c2 : while.cmd) bt (P : state -> Prop),
  { s' | Some s -- c1 ---> s' /\ forall st, s' = Some st -> P st } ->
  { s' | Some s -- c2 ---> s' /\ forall st, s' = Some st -> P st } ->
  { s' | Some s -- while.ifte bt c1 c2 ---> s' /\ forall st, s' = Some st -> P st }.
Proof.
move=> s c1 c2 bt P [s'1 [H1 HP1]] [s'2 [H2 HP2]].
apply constructive_indefinite_description.
case/orP : (orbN (eval_b bt (fst s))) => Hbt.
- exists s'1; split => //; by apply while.exec_ifte_true.
- exists s'2; split => //; apply while.exec_ifte_false => //; by apply/negP.
Qed.

Lemma exists_multu_seq_P : forall rs rt c s h P,
  {s' | Some (store.multu_op ([rs]_s [.*] [rt]_s) s, h) -- c ---> s' /\ P s'} ->
  {s' | Some (s, h) -- multu rs rt ; c ---> s' /\ P s' }.
Proof.
move=> rs rt c s h P [s' [H HP]].
exists s'; split => //; eapply while.exec_seq; eauto; do 2 constructor.
Qed.

Lemma exists_maddu_seq_P : forall rs rt c s h P,
  {s' | Some (store.maddu_op ([rs]_s [.*] [rt]_s) s, h) -- c ---> s' /\ P s'} ->
  {s' | Some (s, h) -- maddu rs rt ; c ---> s' /\ P s' }.
Proof.
move=> rs rt c s h P [s' [H HP]].
exists s'; split => //; eapply while.exec_seq; eauto; do 2 constructor.
Qed.

Lemma exists_mflo_seq_P : forall rd c s h P,
  {s' | Some (store.upd rd (store.lo s) s, h) -- c ---> s' /\ P s'} ->
  {s' | Some (s, h) -- mflo rd ; c ---> s' /\ P s' }.
Proof.
move=> rd c s h P [s' [H HP]].
exists s'; split => //; eapply while.exec_seq; eauto. do 2 constructor.
Qed.

Lemma exists_mfhi_seq_P : forall rd c s h P,
  {s' | Some (store.upd rd (store.hi s) s, h) -- c ---> s' /\ P s'} ->
  {s' | Some (s, h) -- mfhi rd ; c ---> s' /\ P s' }.
Proof.
move=> rd c s h P [s' [H HP]].
exists s'; split => //; eapply while.exec_seq; eauto; do 2 constructor.
Qed.

Lemma exists_mtlo_seq_P : forall rs c s h P,
  {s' | Some (store.mtlo_op [rs]_s s, h) -- c ---> s' /\ P s'} ->
  {s' | Some (s, h) -- mtlo rs ; c ---> s' /\ P s' }.
Proof.
move=> rs c s h P [s' [H HP]].
exists s'; split => //; eapply while.exec_seq; eauto; do 2 constructor.
Qed.

Lemma exists_mflhxu_P : forall rd s h (P : state -> Prop),
  P (store.mflhxu_op (store.upd rd (store.lo s) s), h) ->
  {s' | Some (s, h) -- mflhxu rd ---> s' /\ forall st, s' = Some st -> P st}.
Proof.
move=> rd s h P H.
exists (Some (store.mflhxu_op (store.upd rd (store.lo s) s), h)); split => //.
do 2 constructor.
by move=> st [] <-.
Qed.

Lemma exists_addu_seq_P : forall rd rs rt c s h P,
  {s' | Some (store.upd rd ([rs]_s [.+] [rt]_s) s, h) -- c ---> s' /\ P s'} ->
  {s' | Some (s, h) -- addu rd rs rt ; c ---> s' /\ P s' }.
Proof.
move=> rd rs rt c s h P [s' [H HP]].
exists s'; split => //; eapply while.exec_seq; eauto; do 2 constructor.
Qed.

Lemma exists_sltu_seq_P : forall rd rs rt c s h P flag,
  flag = (if Zlt_bool (u2Z [rs]_s) (u2Z [rt]_s) then one32 else zero32) ->
  {s' | Some (store.upd rd flag s, h) -- c ---> s' /\ P s'} ->
  {s' | Some (s, h) -- sltu rd rs rt ; c ---> s' /\ P s' }.
Proof.
move=> rd rs rt c s h P flag Hflag [s' [H HP]].
exists s'; split => //; eapply while.exec_seq; eauto. do 2 constructor => //.
Qed.

Lemma exists_msubu_seq_P : forall rs rt c s h P,
  {s' | Some (store.msubu_op ([rs]_s [.*] [rt]_s) s, h) -- c ---> s' /\ P s'} ->
  {s' | Some (s, h) -- msubu rs rt; c ---> s' /\ P s' }.
Proof.
move=> rs rt c s h P [s' [H HP]].
exists s'; split => //; eapply while.exec_seq; eauto. do 2 constructor.
Qed.

Lemma exists_movz_true_seq_P : forall rd rs rt c s h P, [ rt ]_s = zero32 ->
 {s' | Some (store.upd rd [rs]_s s, h) -- c ---> s' /\ P s'} ->
 {s' | Some (s, h) -- movz rd rs rt; c ---> s' /\ P s' }.
Proof.
move=> rd rs rt c s h P Hrt [s' [H HP]].
exists s'; split => //; eapply while.exec_seq; eauto; by do 2 constructor.
Qed.

Lemma exists_movz_false_seq_P : forall rd rs rt c s h P, [ rt ]_s <> zero32 ->
 {s' | Some (s, h) -- c ---> s' /\ P s'} ->
 {s' | Some (s, h) -- movz rd rs rt; c ---> s' /\ P s' }.
Proof.
move=> rd rs rt c s h P Hrt [s' [H HP]].
exists s'; split => //; eapply while.exec_seq; eauto; by do 2 constructor.
Qed.

Lemma exists_movz_true_P : forall rd rs rt s h (P : state -> Prop),
 [rt]_s = zero32 ->
 P (store.upd rd [rs]_s s, h) ->
 {s' | Some (s, h) -- movz rd rs rt ---> s' /\ forall st, s' = Some st -> P st }.
Proof.
move=> rd rs rt s h P Hrt HP.
eapply exist; split => //.
do 2 constructor => //.
by move=> st [] <-.
Qed.

Lemma exists_movz_false_P : forall rd rs rt s h (P : state -> Prop),
 [rt]_s <> zero32 -> P (s, h) ->
 {s' | Some (s, h) -- movz rd rs rt ---> s' /\ forall st, s' = Some st -> P st }.
Proof.
move=> rd rs rt s h P Hrt HP.
eapply exist; split => //.
constructor.
apply exec0_movz_false => //.
by move=> st [] <-.
Qed.

Lemma exists_movn_true_seq_P : forall rd rs rt c s h P,
  [rt]_s <> zero32 ->
  {s' | Some (store.upd rd [rs]_s s, h) -- c ---> s' /\ P s'} ->
  {s' | Some (s, h) -- movn rd rs rt; c ---> s' /\ P s' }.
Proof.
move=> rd rs rt c s h P Hrt [s' [H HP]].
exists s'; split => //; eapply while.exec_seq; eauto; by do 2 constructor.
Qed.

Lemma exists_movn_false_seq_P : forall rd rs rt c s h P, [ rt ]_s = zero32 ->
  {s' | Some (s, h) -- c ---> s' /\ P s'} ->
  {s' | Some (s, h) -- movn rd rs rt; c ---> s' /\ P s' }.
Proof.
move=> rd rs rt c s h P Hrt [s' [H HP]].
exists s'; split => //; eapply while.exec_seq; eauto; do 2 constructor => //.
Qed.

Lemma exists_movn_true_P : forall rd rs rt s h (P : state -> Prop),
  [rt]_s <> zero32 -> P (store.upd rd [rs]_s s, h) ->
  {s' | Some (s, h) -- movn rd rs rt ---> s' /\ forall st, s' = Some st -> P st }.
Proof.
move=> rd rs rt s h P Hrt HP.
eapply exist; split => //.
do 2 constructor => //.
by move=> st [] <-.
Qed.

Lemma exists_movn_false_P : forall rd rs rt s h (P : state -> Prop),
  [rt]_s = zero32 -> P (s, h) ->
  {s' | Some (s, h) -- movn rd rs rt ---> s' /\ forall st, s' = Some st -> P st }.
Proof.
move=> rd rs rt s h P Hrt HP.
eapply exist; split => //.
constructor.
apply exec0_movn_false => //.
by move=> st [] <-.
Qed.

Lemma exists_xori_seq_P : forall rt rs (imm : int 16) c s h P,
  {s' | Some (store.upd rt ([rs]_s [.(+)] zext 16 imm) s, h) -- c ---> s' /\ P s'} ->
  {s' | Some (s, h) -- xori rt rs imm; c ---> s' /\ P s' }.
Proof.
move=> rt rs imm c s h P [s' [H HP]].
exists s'; split => //.
eapply while.exec_seq; eauto; by do 2 constructor.
Qed.

Lemma constructive_indefinite_description' :
  forall (A : Type) (P : A -> Prop), { x : A | P x } -> exists x, P x.
Proof. move=> A P [x' Px']; by exists x'. Qed.

Lemma exists_sw_seq : forall rt (off : int 16) base c s h p,
  u2Z ([base]_s [.+] sext 16 off) = 4 * Z_of_nat p ->
  {s' | Some (s, heap.upd p [rt]_s h) -- c ---> s' } ->
  {s' | Some (s, h) -- sw rt off base; c ---> s' }.
Proof.
move=> rt off base c s h p Hp [s' H].
apply constructive_indefinite_description.
case: (classic (exists l , u2Z ([base]_s [.+] sext 16 off) = 4 * Z_of_nat l /\ exists z, heap.get l h = Some z)) => X.
- case:X => l0 [Hl0 [z Hz]].
  exists s'; eapply while.exec_seq; eauto; do 2 constructor.
  omega.
  exists z => //.
  have [->//] : p = l0 by omega.
- exists None.
  eapply while.exec_seq.
  constructor.
  apply exec0_sw_err => //.
  by apply while.exec_none.
Qed.

Lemma exists_sw_seq_P : forall rt (off : int 16) base c s h p (P : state -> Prop),
  u2Z ([base]_s [.+] sext 16 off) = 4 * Z_of_nat p ->
  {s' | Some (s, heap.upd p [rt]_s h) -- c ---> s' /\ forall st, s' = Some st -> P st } ->
  {s' | Some (s, h) -- sw rt off base; c ---> s' /\ forall st, s' = Some st -> P st }.
Proof.
move=> rt off base c s h p P Hp [s' [H HP]].
apply constructive_indefinite_description.
case: (classic (exists l , u2Z ([base]_s [.+] sext 16 off) = 4 * Z_of_nat l /\ exists z, heap.get l h = Some z)) => X.
- case:X => l0 [Hl0 [z Hz]].
  exists s'; split => //; eapply while.exec_seq; eauto; do 2 constructor.
  omega.
  exists z => //.
  have [->//] : p = l0 by omega.
- exists None; split => //.
  eapply while.exec_seq.
  constructor.
  apply exec0_sw_err => //.
  by apply while.exec_none.
Qed.

Lemma exists_lw_seq_P : forall rt (off : int 16) base c s h p z (P : state -> Prop),
  u2Z ([base]_s [.+] sext 16 off) = 4 * Z_of_nat p ->
  heap.get p h = Some z ->
  {s' | Some (store.upd rt z s, h) -- c ---> s' /\ forall st, s' = Some st -> P st } ->
  {s' | Some (s, h) -- lw rt off base ; c ---> s' /\ forall st, s' = Some st -> P st }.
Proof.
move=> rt off base c s h p z P Hp Hz [s' [H HP]].
apply constructive_indefinite_description.
case: (classic (exists l , u2Z ([base]_s [.+] sext 16 off) = 4 * Z_of_nat l /\ exists z, heap.get l h = Some z)) => X.
- case:X => l0 [Hl0 [z0 Hz0]].
  have X : p = l0 by omega.
  subst l0.
  have X : z = z0 by rewrite Hz in Hz0; case: Hz0 => //.
  subst z0.
  exists s'; split => //.
  eapply while.exec_seq; eauto.
  by apply while.exec_cmd0, (exec0_lw _ _ _ _ _ _ _ Hp).
- exists None; split => //.
  eapply while.exec_seq.
  constructor.
  apply exec0_lw_error => //.
  by apply while.exec_none.
Qed.

Lemma exists_sw_P : forall rt (off : int 16) base s h p (P : state -> Prop),
  u2Z ([base]_s [.+] sext 16 off) = 4 * Z_of_nat p ->
  P (s, heap.upd p ([rt]_s) h) ->
  {s' | Some (s, h) -- sw rt off base ---> s' /\ forall st, s' = Some st -> P st }.
Proof.
move=> rt off base s h p P Hp HP.
apply constructive_indefinite_description.
case: (classic (exists z, heap.get p h = Some z)) => X.
apply constructive_indefinite_description'.
eapply exist.
split.
by apply while.exec_cmd0, (exec0_sw _ _ _ _ _ _ Hp X).
by move=> st [] <-.
exists None; split => //.
do 2 constructor.
contradict X.
case: X => l [H1 H2].
have [->//] : p = l by omega.
Qed.

Lemma exists_lwxs_seq_P : forall rt idx base c s h p z (P : state -> Prop),
  u2Z ([base]_s [.+] ([idx]_s [.<<] 2)) = 4 * Z_of_nat p ->
  heap.get p h = Some z ->
  {s' | Some (store.upd rt z s, h) -- c ---> s' /\ forall st, s' = Some st -> P st } ->
  {s' | Some (s, h) -- lwxs rt idx base; c ---> s' /\ forall st, s' = Some st -> P st }.
Proof.
move=> rt idx base c s h p z P Hp Hz [s' [H HP]].
apply constructive_indefinite_description.
case: (classic (exists l, u2Z ([base]_s [.+] ([idx]_s [.<<] 2)) = 4 * Z_of_nat l /\ exists z, heap.get l h = Some z)) => X.
- case:X => l0 [Hl0 [z0 Hz0]].
  have X : p = l0 by omega.
  subst l0.
  have X : z = z0 by rewrite Hz in Hz0; case: Hz0 => //.
  subst z0.
  exists s'; split => //.
  eapply while.exec_seq; eauto.
  by apply while.exec_cmd0, (exec0_lwxs _ _ _ _ _ _ _ Hp).
- exists None; split => //.
  eapply while.exec_seq; by [apply while.exec_cmd0, exec0_lwxs_error | apply while.exec_none].
Qed.

Lemma exists_while : forall s h (c : while.cmd) bt, eval_b bt s ->
  { s' | Some (s, h) -- c ; while.while bt c ---> s'} ->
  { s' | Some (s, h) -- while.while bt c ---> s'}.
Proof.
move=> s h c bt Heval_b [s' H]; exists s'; by apply semop_prop_m.while_seq'.
Qed.

Lemma exists_while_P : forall s h (c : while.cmd) bt (P : state -> Prop),
  eval_b bt s ->
  { s' | Some (s, h) -- c ; while.while bt c ---> s' /\ forall st, s' = Some st -> P st } ->
  { s' | Some (s, h) -- while.while bt c ---> s' /\ forall st, s' = Some st -> P st }.
Proof.
move=> s h c bt P Heval_b [s' [H HP]].
exists s'; split; [by apply semop_prop_m.while_seq' | exact HP ].
Qed.

Lemma exists_while_false : forall s h (c : while.cmd) bt, ~~ eval_b bt s ->
  { s' | Some (s, h) -- while.while bt c ---> s' }.
Proof.
move=> s h c bt Heval_b.
exists (Some (s, h)); by apply while.exec_while_false.
Qed.

Lemma exists_while_false_P : forall s h (c : while.cmd) bt (P : state -> Prop),
  ~~ eval_b bt s -> P (s, h) ->
  { s' | Some (s, h) -- while.while bt c ---> s' /\ forall st, s' = Some st -> P st }.
Proof.
move=> s h c bt P Heval_b HP.
exists (Some (s, h)); split; by [apply while.exec_while_false | move=> st [<-]].
Qed.

Ltac exists_sw1_classic l_idx H_l_idx z_idx H_z_idx X :=
  match goal with
    | |- @ex _ (fun _ => ((Some (?s, ?h) -- (cmd_cmd0_coercion (sw ?rt ?off ?base)) ---> _) /\ _)) =>
            let K := fresh in
            assert (K :
              Decidable.decidable
              (exists l, u2Z ( [base]_ s [.+] sext 16 off) = 4 * Z_of_nat l /\
                exists v, heap.get l h = Some v) );
              [
                by apply Classical_Prop.classic |
                case: K => [ [l_idx [H_l_idx [z_idx H_z_idx] ] ] | X ]
                ]

  end.

Ltac exists_sw1 l_idx H_l_idx z_idx H_z_idx :=
  match goal with
    | |- @sig _ (fun _ => ((Some (?s, ?h) -- (cmd_cmd0_coercion (sw ?rt ?off ?base)) ---> _)%mips_cmd /\ _)) =>
      apply Epsilon.constructive_indefinite_description ;
      let X := fresh in
      exists_sw1_classic l_idx H_l_idx z_idx H_z_idx X ;
      [
        (apply constructive_indefinite_description' ;
          apply exists_sw_P with l_idx ; [assumption | idtac ])
        |
          (exists None ;
           split;
             [ (constructor ; by apply exec0_sw_err)
             |
               done
             ])
      ]
  end.

Ltac exists_sw_classic_new l_idx H_l_idx z_idx H_z_idx X :=
  match goal with
    | |- @ex _ (fun _ => (Some (?s, ?h) -- (cmd_cmd0_coercion (sw ?rt ?off ?base) ; _) ---> _)) =>
            let K := fresh in
            assert (K :
              Decidable.decidable
              (exists l, u2Z ([base]_ s [.+] sext 16 off) = 4 * Z_of_nat l /\
                exists v, heap.get l h = Some v) ) ;
              [by apply Classical_Prop.classic
                |
                  case: K => [ [l_idx [H_l_idx [z_idx H_z_idx] ] ] | X ]
              ]
  end.

Ltac exists_sw_new l_idx H_l_idx z_idx H_z_idx :=
  match goal with
    | |- @sig _ (fun _ => (Some (?s, ?h) -- (cmd_cmd0_coercion (sw ?rt ?off ?base) ; _) ---> _)) =>
      apply Epsilon.constructive_indefinite_description ;
      let X := fresh in
      exists_sw_classic_new l_idx H_l_idx z_idx H_z_idx X;
      [
        (apply constructive_indefinite_description' ;
          apply exists_sw_seq with l_idx ; [assumption | idtac] )
        |
          (exists None ;
           eapply while.exec_seq ;
           constructor => // ;
           apply exec0_sw_err => // ;
           apply while.exec_none )
      ]
  end.

Ltac exists_sw_P_classic l_idx H_l_idx z_idx H_z_idx X :=
  match goal with
    | |- @ex _ (fun _ => ((Some (?s, ?h) -- (cmd_cmd0_coercion (sw ?rt ?off ?base) ; _) ---> _) /\ _)) =>
            let K := fresh in
            assert (K :
              Decidable.decidable
              (exists l, u2Z (([base]_ s) [.+] sext 16 off) = 4 * Z_of_nat l /\
                exists v, heap.get l h = Some v) ) ;
              [by apply Classical_Prop.classic
                |
                  case: K => [ [l_idx [H_l_idx [z_idx H_z_idx] ] ] | X ]
              ]
  end.

Ltac exists_sw_P l_idx H_l_idx z_idx H_z_idx :=
  match goal with
    | |- @sig _ (fun _ => ((Some (?s, ?h) -- (cmd_cmd0_coercion (sw ?rt ?off ?base) ; _) ---> _) /\ _)) =>
      apply Epsilon.constructive_indefinite_description ;
      let X := fresh in
      exists_sw_P_classic l_idx H_l_idx z_idx H_z_idx X ;
      [
        (apply constructive_indefinite_description' ;
          apply exists_sw_seq_P with l_idx ; [assumption | idtac] )
        |
          (exists None ;
           split => // ;
           eapply while.exec_seq ;
           constructor => // ;
           apply exec0_sw_err => // ;
           apply while.exec_none )
      ]
  end.

Ltac exists_lwxs_classic location Hlocation value Hvalue X :=
  match goal with
    | |- @ex _ (fun _ => ((Some (?s, ?h) -- (cmd_cmd0_coercion (lwxs ?rt ?idx ?base) ; _) ---> _)%mips_cmd /\ _)) =>
      let K := fresh in
         assert (K :
           Decidable.decidable
           (exists p, u2Z (([base]_ s)%mips_expr[.+]([idx]_s [.<<] 2)) = 4 * Z_of_nat p /\
           exists v, heap.get p h = Some v)%mips_expr) ;
         [by apply Classical_Prop.classic |
         case : K =>
           [ [location [Hlocation [value Hvalue] ] ] | X ] ]
  end.

Ltac exists_lwxs location Hlocation value Hvalue :=
  match goal with
    | |- @sig _ (fun _ => ((Some (?s, ?h)) -- (cmd_cmd0_coercion (lwxs ?rt ?idx ?base) ; _) ---> _)%mips_cmd /\ _) =>
      apply Epsilon.constructive_indefinite_description ;
      let X := fresh in
      exists_lwxs_classic location Hlocation value Hvalue X ;
      [ (apply constructive_indefinite_description' ;
         apply exists_lwxs_seq_P with location value; [assumption | assumption | idtac ])
      | (apply constructive_indefinite_description' ;
         exists None; split ; [
         apply while.exec_seq with None ;
         [ (apply while.exec_cmd0 ;
            by apply exec0_lwxs_error)
         |
            by apply while.exec_none
         ] | done ])
      ]
  end.

Ltac exists_lw_classic location Hlocation value Hvalue X :=
  match goal with
    | |- @ex _ (fun _ => ((Some (?s, ?h) -- (cmd_cmd0_coercion (lw ?rt ?off ?base) ; _) ---> _)%mips_cmd /\ _)) =>
      let K := fresh in
         assert (K :
           Decidable.decidable
           (exists p, u2Z (([base]_ s)%mips_expr[.+] sext 16 off) = 4 * Z_of_nat p /\
           exists v, heap.get p h = Some v)%mips_expr ) ;
         [ by apply Classical_Prop.classic |
           case: K => [ [location [Hlocation [value Hvalue] ] ] | X ]
           ]
  end.

Ltac exists_lw location Hlocation value Hvalue :=
  match goal with
    | |- @sig _ (fun _ => ((Some (?s, ?h)) -- (cmd_cmd0_coercion (lw ?rt ?off ?base) ; _) ---> _)%mips_cmd /\ _) =>
      apply Epsilon.constructive_indefinite_description ;
      let X := fresh in
      exists_lw_classic location Hlocation value Hvalue X ;
      [ (apply constructive_indefinite_description' ;
         apply exists_lw_seq_P with location value => //)
      | (apply constructive_indefinite_description' ;
         exists None; split => // ;
         apply while.exec_seq with None ;
         [ (apply while.exec_cmd0 ;
            by apply exec0_lw_error)
         |
            by apply while.exec_none
         ])
      ]
  end.

Ltac exists_movn H :=
  match goal with
    | |- @sig _ (fun _ => ((Some (?s, ?h) -- (cmd_cmd0_coercion (movn ?rd ?rs ?rt) ; _) ---> _)%mips_cmd /\ _)) =>
      case: (dec_int ([rt]_(s))
        zero32) => H
  end.

Ltac exists_movz1 H :=
  match goal with
    | |- @sig _ (fun _ => ((Some (?s, ?h) -- (cmd_cmd0_coercion (movz ?rd ?rs ?rt)) ---> _)%mips_cmd /\ _)) =>
      case: (dec_int ([rt]_(s))
        zero32) => H
  end.