Library simu
Require Import Permutation.
Require Import ssreflect ssrbool eqtype.
Require Import ZArith_ext Lists_ext.
Require Import nodup encode_decode multi_int integral_type.
Require syntax.
Require Import machine_int.
Import MachineInt.
Require Import mips_bipl mips_cmd mips_seplog mips_frame mips_syntax.
Import mips_bipl.expr_m.
Local Open Scope machine_int_scope.
Local Open Scope zarith_ext_scope.
Ltac disj_remove_duplicates_R :=
match goal with
| |- disj ?L (?HD :: ?TL) =>
let tmp := remove_duplicates (HD :: TL) in
apply (disj_incl_R L tmp)
end.
Ltac disj_remove_duplicates_L :=
match goal with
| |- disj (?HD :: ?TL) _ =>
let tmp := remove_duplicates (HD :: TL) in
apply (disj_incl_L tmp)
end.
Ltac Disj_remove_dup :=
match goal with
| |- disj (_ :: _) (_ :: _) =>
( disj_remove_duplicates_L; last by rewrite /incl /=; intuition ) ;
( disj_remove_duplicates_R; last by rewrite /incl /=; intuition )
| |- disj (?HD :: ?TL) _ =>
disj_remove_duplicates_L; last by rewrite /incl /=; intuition
| |- disj _ (?HD :: ?TL) =>
disj_remove_duplicates_R; last by rewrite /incl /=; intuition
end.
Module Simu (A : IntegralType).
Module syntax_m := syntax.Syntax A.
Notation "e1 '+e' e2" :=
(syntax_m.seplog_m.assert_m.expr_m.bop_e syntax_m.seplog_m.assert_m.expr_m.add_e e1 e2)
(at level 75) : seplog_expr_scope.
Notation "e1 '.-e' e2" :=
(syntax_m.seplog_m.assert_m.expr_m.bop_e syntax_m.seplog_m.assert_m.expr_m.min_e e1 e2)
(at level 75) : seplog_expr_scope.
Notation "e1 '*e' e2" :=
(syntax_m.seplog_m.assert_m.expr_m.bop_e syntax_m.seplog_m.assert_m.expr_m.mul_e e1 e2)
(at level 75) : seplog_expr_scope.
Notation "e1 './e' e2" :=
(syntax_m.seplog_m.assert_m.expr_m.bop_e syntax_m.seplog_m.assert_m.expr_m.div_e e1 e2)
(at level 75) : seplog_expr_scope.
Notation "e1 'mode' e2" :=
(syntax_m.seplog_m.assert_m.expr_m.bop_e syntax_m.seplog_m.assert_m.expr_m.mod_e e1 e2)
(at level 75) : seplog_expr_scope.
Notation "e &e e'" :=
(syntax_m.seplog_m.assert_m.expr_m.bop_b2 syntax_m.seplog_m.assert_m.expr_m.and_b e e')
(at level 77) : seplog_expr_scope.
Notation "'.--e' e" :=
(syntax_m.seplog_m.assert_m.expr_m.uop_e syntax_m.seplog_m.assert_m.expr_m.negate_e e)
(at level 75) : seplog_expr_scope.
Notation "e =e e'" :=
(syntax_m.seplog_m.assert_m.expr_m.bop_b syntax_m.seplog_m.assert_m.expr_m.eq_b e e')
(at level 76) : seplog_expr_scope.
Notation "e <>e e'" :=
(syntax_m.seplog_m.assert_m.expr_m.bop_b syntax_m.seplog_m.assert_m.expr_m.neq_b e e')
(at level 76) : seplog_expr_scope.
Notation "e >>= e'" :=
(syntax_m.seplog_m.assert_m.expr_m.bop_b syntax_m.seplog_m.assert_m.expr_m.ge_b e e')
(at level 76) : seplog_expr_scope.
Notation "e >> e'" :=
(syntax_m.seplog_m.assert_m.expr_m.bop_b syntax_m.seplog_m.assert_m.expr_m.gt_b e e')
(at level 76) : seplog_expr_scope.
Notation "'[' x ']_' s" := (syntax_m.seplog_m.assert_m.expr_m.store.get x s) (at level 9) : seplog_expr_scope.
Notation "'[' e ']e_' s" := (syntax_m.seplog_m.assert_m.expr_m.eval e s) (at level 9) : seplog_expr_scope.
Notation "'[' e ']b_' s" := (syntax_m.seplog_m.assert_m.expr_m.eval_b e s) (at level 9) : seplog_expr_scope.
Delimit Scope seplog_expr_scope with seplog_expr.
Notation "s -- c ---> t" := (syntax_m.seplog_m.semop_m.exec s c t) (at level 74) : seplog_cmd_scope.
Notation " s '--' c '---->' t " := (syntax_m.seplog_m.exec0 s c t) (at level 74, no associativity) : seplog_cmd_scope.
Notation "c ; d" := (while.seq c d) (at level 81, right associativity) : seplog_cmd_scope.
Notation "x <- e" := (syntax_m.seplog_m.assign x e) (at level 80) : seplog_cmd_scope.
Delimit Scope seplog_cmd_scope with seplog_cmd.
Notation "'pemp'" := (syntax_m.seplog_m.assert_m.heap.emp) : seplog_cmd_scope.
Notation "{{ P }} c {{ Q }}" := (syntax_m.seplog_m.hoare_m.hoare P c Q) (at level 82) : seplog_hoare_scope.
Delimit Scope seplog_hoare_scope with seplog_hoare.
Notation "'nat_e'" := (syntax_m.seplog_m.assert_m.expr_m.nat_e) : seplog_expr_scope.
Notation "'var_e'" := (syntax_m.seplog_m.assert_m.expr_m.var_e) : seplog_expr_scope.
Notation "'var_e'" := (mips_bipl.expr_m.var_e) : mips_expr_scope.
Delimit Scope mips_expr_scope with mips_expr.
Notation "P ** Q" := (assert_m.con P Q) (at level 80) : mips_assert_scope.
Notation "e1 |~> e2" := (assert_m.mapsto e1 e2) (at level 77) : mips_assert_scope.
Notation "x '|-->' l" := (assert_m.mapstos x l) (at level 77) : mips_assert_scope.
Delimit Scope mips_assert_scope with mips_assert.
Delimit Scope mips_cmd_scope with mips_cmd.
Delimit Scope mips_hoare_scope with mips_hoare.
Require Import ssreflect ssrbool eqtype.
Require Import ZArith_ext Lists_ext.
Require Import nodup encode_decode multi_int integral_type.
Require syntax.
Require Import machine_int.
Import MachineInt.
Require Import mips_bipl mips_cmd mips_seplog mips_frame mips_syntax.
Import mips_bipl.expr_m.
Local Open Scope machine_int_scope.
Local Open Scope zarith_ext_scope.
Ltac disj_remove_duplicates_R :=
match goal with
| |- disj ?L (?HD :: ?TL) =>
let tmp := remove_duplicates (HD :: TL) in
apply (disj_incl_R L tmp)
end.
Ltac disj_remove_duplicates_L :=
match goal with
| |- disj (?HD :: ?TL) _ =>
let tmp := remove_duplicates (HD :: TL) in
apply (disj_incl_L tmp)
end.
Ltac Disj_remove_dup :=
match goal with
| |- disj (_ :: _) (_ :: _) =>
( disj_remove_duplicates_L; last by rewrite /incl /=; intuition ) ;
( disj_remove_duplicates_R; last by rewrite /incl /=; intuition )
| |- disj (?HD :: ?TL) _ =>
disj_remove_duplicates_L; last by rewrite /incl /=; intuition
| |- disj _ (?HD :: ?TL) =>
disj_remove_duplicates_R; last by rewrite /incl /=; intuition
end.
Module Simu (A : IntegralType).
Module syntax_m := syntax.Syntax A.
Notation "e1 '+e' e2" :=
(syntax_m.seplog_m.assert_m.expr_m.bop_e syntax_m.seplog_m.assert_m.expr_m.add_e e1 e2)
(at level 75) : seplog_expr_scope.
Notation "e1 '.-e' e2" :=
(syntax_m.seplog_m.assert_m.expr_m.bop_e syntax_m.seplog_m.assert_m.expr_m.min_e e1 e2)
(at level 75) : seplog_expr_scope.
Notation "e1 '*e' e2" :=
(syntax_m.seplog_m.assert_m.expr_m.bop_e syntax_m.seplog_m.assert_m.expr_m.mul_e e1 e2)
(at level 75) : seplog_expr_scope.
Notation "e1 './e' e2" :=
(syntax_m.seplog_m.assert_m.expr_m.bop_e syntax_m.seplog_m.assert_m.expr_m.div_e e1 e2)
(at level 75) : seplog_expr_scope.
Notation "e1 'mode' e2" :=
(syntax_m.seplog_m.assert_m.expr_m.bop_e syntax_m.seplog_m.assert_m.expr_m.mod_e e1 e2)
(at level 75) : seplog_expr_scope.
Notation "e &e e'" :=
(syntax_m.seplog_m.assert_m.expr_m.bop_b2 syntax_m.seplog_m.assert_m.expr_m.and_b e e')
(at level 77) : seplog_expr_scope.
Notation "'.--e' e" :=
(syntax_m.seplog_m.assert_m.expr_m.uop_e syntax_m.seplog_m.assert_m.expr_m.negate_e e)
(at level 75) : seplog_expr_scope.
Notation "e =e e'" :=
(syntax_m.seplog_m.assert_m.expr_m.bop_b syntax_m.seplog_m.assert_m.expr_m.eq_b e e')
(at level 76) : seplog_expr_scope.
Notation "e <>e e'" :=
(syntax_m.seplog_m.assert_m.expr_m.bop_b syntax_m.seplog_m.assert_m.expr_m.neq_b e e')
(at level 76) : seplog_expr_scope.
Notation "e >>= e'" :=
(syntax_m.seplog_m.assert_m.expr_m.bop_b syntax_m.seplog_m.assert_m.expr_m.ge_b e e')
(at level 76) : seplog_expr_scope.
Notation "e >> e'" :=
(syntax_m.seplog_m.assert_m.expr_m.bop_b syntax_m.seplog_m.assert_m.expr_m.gt_b e e')
(at level 76) : seplog_expr_scope.
Notation "'[' x ']_' s" := (syntax_m.seplog_m.assert_m.expr_m.store.get x s) (at level 9) : seplog_expr_scope.
Notation "'[' e ']e_' s" := (syntax_m.seplog_m.assert_m.expr_m.eval e s) (at level 9) : seplog_expr_scope.
Notation "'[' e ']b_' s" := (syntax_m.seplog_m.assert_m.expr_m.eval_b e s) (at level 9) : seplog_expr_scope.
Delimit Scope seplog_expr_scope with seplog_expr.
Notation "s -- c ---> t" := (syntax_m.seplog_m.semop_m.exec s c t) (at level 74) : seplog_cmd_scope.
Notation " s '--' c '---->' t " := (syntax_m.seplog_m.exec0 s c t) (at level 74, no associativity) : seplog_cmd_scope.
Notation "c ; d" := (while.seq c d) (at level 81, right associativity) : seplog_cmd_scope.
Notation "x <- e" := (syntax_m.seplog_m.assign x e) (at level 80) : seplog_cmd_scope.
Delimit Scope seplog_cmd_scope with seplog_cmd.
Notation "'pemp'" := (syntax_m.seplog_m.assert_m.heap.emp) : seplog_cmd_scope.
Notation "{{ P }} c {{ Q }}" := (syntax_m.seplog_m.hoare_m.hoare P c Q) (at level 82) : seplog_hoare_scope.
Delimit Scope seplog_hoare_scope with seplog_hoare.
Notation "'nat_e'" := (syntax_m.seplog_m.assert_m.expr_m.nat_e) : seplog_expr_scope.
Notation "'var_e'" := (syntax_m.seplog_m.assert_m.expr_m.var_e) : seplog_expr_scope.
Notation "'var_e'" := (mips_bipl.expr_m.var_e) : mips_expr_scope.
Delimit Scope mips_expr_scope with mips_expr.
Notation "P ** Q" := (assert_m.con P Q) (at level 80) : mips_assert_scope.
Notation "e1 |~> e2" := (assert_m.mapsto e1 e2) (at level 77) : mips_assert_scope.
Notation "x '|-->' l" := (assert_m.mapstos x l) (at level 77) : mips_assert_scope.
Delimit Scope mips_assert_scope with mips_assert.
Delimit Scope mips_cmd_scope with mips_cmd.
Delimit Scope mips_hoare_scope with mips_hoare.
simulation of programs
Notation "'pstore'" := (syntax_m.seplog_m.assert_m.expr_m.store.t) : simu_scope.
Local Open Scope simu_scope.
Definition relat := pstore -> store.t -> heap.t -> Prop.
Notation "'relat'" := (syntax_m.seplog_m.assert_m.expr_m.store.t -> store.t -> heap.t -> Prop) : simu_scope.
Notation "'pcmd'" := (syntax_m.seplog_m.semop_m.cmd) : simu_scope.
Local Open Scope simu_scope.
Definition relat := pstore -> store.t -> heap.t -> Prop.
Notation "'relat'" := (syntax_m.seplog_m.assert_m.expr_m.store.t -> store.t -> heap.t -> Prop) : simu_scope.
Notation "'pcmd'" := (syntax_m.seplog_m.semop_m.cmd) : simu_scope.
forward simulation
Definition fwd_sim (R P0 : relat) (p : pcmd) (c : WMIPS_Semop.cmd) :=
forall s st h, R s st h -> P0 s st h ->
forall s', (Some (s, pemp) -- p ---> Some (s', pemp))%seplog_cmd ->
exists st', exists h',
(Some (st, h) -- c ---> Some (st', h'))%mips_cmd /\ R s' st' h'.
Lemma fwd_sim_assoc_L : forall R P p1 p2 p3 c,
(fwd_sim R P (p1 ; p2 ; p3) c -> fwd_sim R P ((p1 ; p2) ; p3) c)%seplog_cmd.
Proof.
move=> R P p1 p2 p3 c H s st h HR HP s' Hp.
move: (H s st h HR HP s').
apply syntax_m.seplog_m.semop_prop_m.exec_seq_assoc in Hp.
by move/(_ Hp).
Qed.
Lemma fwd_sim_assoc_R : forall R P p c1 c2 c3,
(fwd_sim R P p (c1 ; c2 ; c3) -> fwd_sim R P p ((c1 ; c2) ; c3))%mips_cmd.
Proof.
move=> R P p1 p2 p3 c H s st h HR HP s' Hp.
case: (H s st h HR HP s' Hp) => [st' [h' H']].
exists st', h'.
split; last by tauto.
apply semop_prop_m.exec_seq_assoc'; tauto.
Qed.
Lemma fwd_sim_stren : forall R (P P' : relat) p c,
(forall s st h, P' s st h -> P s st h) ->
fwd_sim R P p c -> fwd_sim R P' p c.
Proof.
move=> R P P' p c H H'.
rewrite /fwd_sim.
move=> s st h HR HP' s' Hp.
apply (H' s st h HR (H _ _ _ HP') s' Hp).
Qed.
forall s st h, R s st h -> P0 s st h ->
forall s', (Some (s, pemp) -- p ---> Some (s', pemp))%seplog_cmd ->
exists st', exists h',
(Some (st, h) -- c ---> Some (st', h'))%mips_cmd /\ R s' st' h'.
Lemma fwd_sim_assoc_L : forall R P p1 p2 p3 c,
(fwd_sim R P (p1 ; p2 ; p3) c -> fwd_sim R P ((p1 ; p2) ; p3) c)%seplog_cmd.
Proof.
move=> R P p1 p2 p3 c H s st h HR HP s' Hp.
move: (H s st h HR HP s').
apply syntax_m.seplog_m.semop_prop_m.exec_seq_assoc in Hp.
by move/(_ Hp).
Qed.
Lemma fwd_sim_assoc_R : forall R P p c1 c2 c3,
(fwd_sim R P p (c1 ; c2 ; c3) -> fwd_sim R P p ((c1 ; c2) ; c3))%mips_cmd.
Proof.
move=> R P p1 p2 p3 c H s st h HR HP s' Hp.
case: (H s st h HR HP s' Hp) => [st' [h' H']].
exists st', h'.
split; last by tauto.
apply semop_prop_m.exec_seq_assoc'; tauto.
Qed.
Lemma fwd_sim_stren : forall R (P P' : relat) p c,
(forall s st h, P' s st h -> P s st h) ->
fwd_sim R P p c -> fwd_sim R P' p c.
Proof.
move=> R P P' p c H H'.
rewrite /fwd_sim.
move=> s st h HR HP' s' Hp.
apply (H' s st h HR (H _ _ _ HP') s' Hp).
Qed.
relational Hoare logic
Definition rela_hoare (P Q : relat) (p : pcmd) (c : WMIPS_Semop.cmd) :=
forall s st h, P s st h ->
forall s', (Some (s, pemp) -- p ---> Some (s', pemp))%seplog_cmd ->
forall st' h', (Some (st, h) -- c ---> Some (st', h'))%mips_cmd ->
Q s' st' h'.
Lemma rela_hoare_stren : forall (P P' Q : relat) p c,
(forall s st h, P s st h -> P' s st h) ->
rela_hoare P' Q p c -> rela_hoare P Q p c.
Proof.
move=> P P' Q p c H P'_Q s st h HP s' exec_p st' h' exec_c.
apply (P'_Q s st h) => //; by apply H.
Qed.
Lemma rela_hoare_weak : forall (P Q Q' : relat) p c,
(forall s st h, Q' s st h -> Q s st h) ->
rela_hoare P Q' p c -> rela_hoare P Q p c.
Proof.
move=> P Q Q' p c H P_Q' s st h HP s' exec_p st' h' exec_c.
by apply H, (P_Q' s st h).
Qed.
Lemma rela_hoare_seq : forall (Q' P Q:relat) p1 p2 c1 c2,
~~ syntax_m.contains_malloc p1 ->
~~ syntax_m.contains_malloc p2 ->
rela_hoare P Q' p1 c1 ->
rela_hoare Q' Q p2 c2 ->
rela_hoare P Q (p1 ; p2)%seplog_cmd (c1 ; c2)%mips_cmd.
Proof.
move=> Q' P Q p1 p2 c1 c2 malloc1 malloc2 H1 H2 s st h HP s' exec_pseudo st' h' exec_asm.
case/syntax_m.seplog_m.semop_prop_m.exec_seq_inv_Some : exec_pseudo.
case=> s'' h'' [exec_p1 exec_p2].
move: (syntax_m.no_malloc_heap_invariant _ _ _ exec_p1 malloc1 _ _ _ (refl_equal _) (refl_equal _)) => ?; subst h''.
case/semop_prop_m.exec_seq_inv_Some : exec_asm.
case=> st'' h''_ [exec_c1 exec_c2].
move: (H1 _ _ _ HP _ exec_p1 _ _ exec_c1) => HQ'.
by apply (H2 _ _ _ HQ' _ exec_p2 _ _ exec_c2).
Qed.
Lemma rela_hoare_ifte : forall (P Q : relat) t p1 p2 a b c1 c2,
~~ syntax_m.contains_malloc p1 ->
~~ syntax_m.contains_malloc p2 ->
rela_hoare
(fun s st h => P s st h /\ ([t]b_s)%seplog_expr /\
forall st' h', (Some (st, h) -- a ---> Some (st', h'))%mips_cmd -> mips_bipl.expr_m.eval_b b st')
Q p1 (a ; c1)%mips_cmd ->
rela_hoare
(fun s st h => P s st h /\ (~~ [t]b_s)%seplog_expr /\
forall st' h', (Some (st, h) -- a ---> Some (st', h'))%mips_cmd -> ~~ mips_bipl.expr_m.eval_b b st')
Q p2 (a ; c2)%mips_cmd ->
rela_hoare
(fun s st h =>
P s st h /\
(forall st' h',
(Some (st, h) -- a ---> Some (st', h'))%mips_cmd ->
(([t]b_s)%seplog_expr <->
mips_bipl.expr_m.eval_b b st')))
Q (while.ifte t p1 p2)%seplog_cmd (a ; while.ifte b c1 c2)%mips_cmd.
Proof.
move=> P Q t p1 p2 a b c1 c2 malloc1 malloc2 H1 H2 s st h HP s' exec_pseudo st' h' exec_asm.
case/semop_prop_m.exec_seq_inv_Some : exec_asm.
case=> st'' h'' [exec_a exec_asm].
case/orP : (orbN ([t]b_s)%seplog_expr) => Ht.
- apply syntax_m.seplog_m.semop_prop_m.exec_ifte_true_inv in exec_pseudo => //.
case/orP : (orbN (eval_b b st'')%seplog_expr) => Hb.
+ apply semop_prop_m.exec_ifte_true_inv in exec_asm => //.
apply (H1 s st h) => //.
split; first by tauto.
split; first by tauto.
move=> st'0 h'0 exec_a0.
by case: (semop_deter_prop_m.exec_deter _ _ _ exec_a _ exec_a0) => ? ?; subst st'0 h'0.
by econstructor; eauto.
+ case: HP => _.
case/(_ _ _ exec_a) => X.
apply X in Ht.
by rewrite Ht in Hb.
- apply syntax_m.seplog_m.semop_prop_m.exec_ifte_false_inv in exec_pseudo => //.
case/orP : (orbN (eval_b b st'')%seplog_expr) => Hb.
+ case: HP => _.
case/(_ _ _ exec_a) => _ X.
apply X in Hb.
by rewrite Hb in Ht.
+ apply semop_prop_m.exec_ifte_false_inv in exec_asm => //.
apply (H2 s st h) => //.
split; first by tauto.
split; first by tauto.
move=> st'0 h'0 exec_a0.
by case: (semop_deter_prop_m.exec_deter _ _ _ exec_a _ exec_a0) => ? ?; subst st'0 h'0.
by econstructor; eauto.
Qed.
Lemma rela_hoare_ignore_R : forall P Q p c1 c2,
rela_hoare P Q p c2 ->
(forall st h st'' h'',
(Some (st, h) -- c1 ---> Some (st'', h''))%mips_cmd ->
(forall s, P s st h -> P s st'' h'')) ->
rela_hoare P Q p (c1 ; c2)%mips_cmd.
Proof.
move=> P Q p c1 c2 P_Q H.
move=> s st h HP s' exec_p st' h' exec_c1c2.
case/semop_prop_m.exec_seq_inv_Some : exec_c1c2 => [[st'' h''] [Hc1 Hc2]].
apply (P_Q s st'' h'') => //.
eapply H.
apply Hc1.
done.
Qed.
forall s st h, P s st h ->
forall s', (Some (s, pemp) -- p ---> Some (s', pemp))%seplog_cmd ->
forall st' h', (Some (st, h) -- c ---> Some (st', h'))%mips_cmd ->
Q s' st' h'.
Lemma rela_hoare_stren : forall (P P' Q : relat) p c,
(forall s st h, P s st h -> P' s st h) ->
rela_hoare P' Q p c -> rela_hoare P Q p c.
Proof.
move=> P P' Q p c H P'_Q s st h HP s' exec_p st' h' exec_c.
apply (P'_Q s st h) => //; by apply H.
Qed.
Lemma rela_hoare_weak : forall (P Q Q' : relat) p c,
(forall s st h, Q' s st h -> Q s st h) ->
rela_hoare P Q' p c -> rela_hoare P Q p c.
Proof.
move=> P Q Q' p c H P_Q' s st h HP s' exec_p st' h' exec_c.
by apply H, (P_Q' s st h).
Qed.
Lemma rela_hoare_seq : forall (Q' P Q:relat) p1 p2 c1 c2,
~~ syntax_m.contains_malloc p1 ->
~~ syntax_m.contains_malloc p2 ->
rela_hoare P Q' p1 c1 ->
rela_hoare Q' Q p2 c2 ->
rela_hoare P Q (p1 ; p2)%seplog_cmd (c1 ; c2)%mips_cmd.
Proof.
move=> Q' P Q p1 p2 c1 c2 malloc1 malloc2 H1 H2 s st h HP s' exec_pseudo st' h' exec_asm.
case/syntax_m.seplog_m.semop_prop_m.exec_seq_inv_Some : exec_pseudo.
case=> s'' h'' [exec_p1 exec_p2].
move: (syntax_m.no_malloc_heap_invariant _ _ _ exec_p1 malloc1 _ _ _ (refl_equal _) (refl_equal _)) => ?; subst h''.
case/semop_prop_m.exec_seq_inv_Some : exec_asm.
case=> st'' h''_ [exec_c1 exec_c2].
move: (H1 _ _ _ HP _ exec_p1 _ _ exec_c1) => HQ'.
by apply (H2 _ _ _ HQ' _ exec_p2 _ _ exec_c2).
Qed.
Lemma rela_hoare_ifte : forall (P Q : relat) t p1 p2 a b c1 c2,
~~ syntax_m.contains_malloc p1 ->
~~ syntax_m.contains_malloc p2 ->
rela_hoare
(fun s st h => P s st h /\ ([t]b_s)%seplog_expr /\
forall st' h', (Some (st, h) -- a ---> Some (st', h'))%mips_cmd -> mips_bipl.expr_m.eval_b b st')
Q p1 (a ; c1)%mips_cmd ->
rela_hoare
(fun s st h => P s st h /\ (~~ [t]b_s)%seplog_expr /\
forall st' h', (Some (st, h) -- a ---> Some (st', h'))%mips_cmd -> ~~ mips_bipl.expr_m.eval_b b st')
Q p2 (a ; c2)%mips_cmd ->
rela_hoare
(fun s st h =>
P s st h /\
(forall st' h',
(Some (st, h) -- a ---> Some (st', h'))%mips_cmd ->
(([t]b_s)%seplog_expr <->
mips_bipl.expr_m.eval_b b st')))
Q (while.ifte t p1 p2)%seplog_cmd (a ; while.ifte b c1 c2)%mips_cmd.
Proof.
move=> P Q t p1 p2 a b c1 c2 malloc1 malloc2 H1 H2 s st h HP s' exec_pseudo st' h' exec_asm.
case/semop_prop_m.exec_seq_inv_Some : exec_asm.
case=> st'' h'' [exec_a exec_asm].
case/orP : (orbN ([t]b_s)%seplog_expr) => Ht.
- apply syntax_m.seplog_m.semop_prop_m.exec_ifte_true_inv in exec_pseudo => //.
case/orP : (orbN (eval_b b st'')%seplog_expr) => Hb.
+ apply semop_prop_m.exec_ifte_true_inv in exec_asm => //.
apply (H1 s st h) => //.
split; first by tauto.
split; first by tauto.
move=> st'0 h'0 exec_a0.
by case: (semop_deter_prop_m.exec_deter _ _ _ exec_a _ exec_a0) => ? ?; subst st'0 h'0.
by econstructor; eauto.
+ case: HP => _.
case/(_ _ _ exec_a) => X.
apply X in Ht.
by rewrite Ht in Hb.
- apply syntax_m.seplog_m.semop_prop_m.exec_ifte_false_inv in exec_pseudo => //.
case/orP : (orbN (eval_b b st'')%seplog_expr) => Hb.
+ case: HP => _.
case/(_ _ _ exec_a) => _ X.
apply X in Hb.
by rewrite Hb in Ht.
+ apply semop_prop_m.exec_ifte_false_inv in exec_asm => //.
apply (H2 s st h) => //.
split; first by tauto.
split; first by tauto.
move=> st'0 h'0 exec_a0.
by case: (semop_deter_prop_m.exec_deter _ _ _ exec_a _ exec_a0) => ? ?; subst st'0 h'0.
by econstructor; eauto.
Qed.
Lemma rela_hoare_ignore_R : forall P Q p c1 c2,
rela_hoare P Q p c2 ->
(forall st h st'' h'',
(Some (st, h) -- c1 ---> Some (st'', h''))%mips_cmd ->
(forall s, P s st h -> P s st'' h'')) ->
rela_hoare P Q p (c1 ; c2)%mips_cmd.
Proof.
move=> P Q p c1 c2 P_Q H.
move=> s st h HP s' exec_p st' h' exec_c1c2.
case/semop_prop_m.exec_seq_inv_Some : exec_c1c2 => [[st'' h''] [Hc1 Hc2]].
apply (P_Q s st'' h'') => //.
eapply H.
apply Hc1.
done.
Qed.
simulation of sequences
Lemma fwd_sim_seq : forall R p (Hp : ~~ syntax_m.contains_malloc p)
p' (Hp' : ~~ syntax_m.contains_malloc p') c c' P Q,
rela_hoare P Q p c -> fwd_sim R P p c -> fwd_sim R Q p' c' ->
fwd_sim R P (p ; p')%seplog_cmd (c ; c')%mips_cmd.
Proof.
move=> R p Hp p' Hp' c c' P Q HPQ Hfwd_sim_p Hfwd_sim_p'; move=> s st h HR HP s' Hexec_pp'.
case/syntax_m.seplog_m.semop_prop_m.exec_seq_inv : Hexec_pp' => s'' [Hexec_p Hexec_p'].
destruct s'' as [[s'' h'']|]; last by move/syntax_m.seplog_m.semop_prop_m.from_none : Hexec_p'.
move: (syntax_m.no_malloc_heap_invariant _ _ _ Hexec_p Hp s _ _ (refl_equal _) (refl_equal _)) => Hh''; subst h''.
case: {Hfwd_sim_p}(Hfwd_sim_p _ _ _ HR HP _ Hexec_p) => st'' [h'' [Hexec_c HR'']].
have HQ'' : Q s'' st'' h''.
rewrite /rela_hoare in HPQ; by apply HPQ with s st h.
case: {Hfwd_sim_p'}(Hfwd_sim_p' _ _ _ HR'' HQ'' _ Hexec_p') => st' [h' [Hexec_c' HR']].
exists st', h'; split; last by done.
by apply while.exec_seq with (Some (st'', h'')).
Qed.
Definition equivalent_pseudo_code p p' :=
forall s s', (Some s -- p ---> Some s')%seplog_cmd <-> (Some s -- p' ---> Some s')%seplog_cmd.
Lemma equivalent_pseudo_code_op : forall A e' (e : syntax_m.seplog_m.assert_m.expr_m.expr) op,
(forall s, ([op (var_e A) e ]e_
(syntax_m.seplog_m.assert_m.expr_m.store.upd A [e' ]e_ s s) = [op e' e]e_s))%seplog_expr ->
(equivalent_pseudo_code
(while.cmd_cmd0 (A <- e') ; while.cmd_cmd0 (A <- op (var_e A) e))
(while.cmd_cmd0 (A <- op e' e)))%seplog_expr%seplog_cmd.
Proof.
move=> A e' e op Hop.
rewrite /equivalent_pseudo_code; case=> [s h] [s' h']; split => HA.
case/syntax_m.seplog_m.hoare_prop_m.while_semop_prop_m.exec_seq_inv_Some : HA.
case=> [s'' h''] [HA1 HA2].
move/syntax_m.seplog_m.hoare_prop_m.while_semop_prop_m.exec_cmd0_inv : HA1.
case/syntax_m.seplog_m.exec0_assign_inv => [? ?]; subst h'' s''.
move/syntax_m.seplog_m.hoare_prop_m.while_semop_prop_m.exec_cmd0_inv : HA2.
case/syntax_m.seplog_m.exec0_assign_inv => [? ?]; subst h' s'.
constructor.
rewrite syntax_m.seplog_m.assert_m.expr_m.store.upd_upd_eq Hop; by constructor.
eapply while.exec_seq.
constructor.
by constructor.
constructor.
move/syntax_m.seplog_m.hoare_prop_m.while_semop_prop_m.exec_cmd0_inv : HA.
case/syntax_m.seplog_m.exec0_assign_inv => [? ?]; subst h' s'.
set s0 := syntax_m.seplog_m.assert_m.expr_m.store.upd A _ _.
set s1 := syntax_m.seplog_m.assert_m.expr_m.store.upd A _ _.
have -> : s1 = syntax_m.seplog_m.assert_m.expr_m.store.upd A
([ op (var_e A) e ]e_ s0)%seplog_expr s0.
by rewrite /s0 syntax_m.seplog_m.assert_m.expr_m.store.upd_upd_eq Hop.
by apply syntax_m.seplog_m.exec0_assign.
Qed.
Lemma equivalent_pseudo_code_uop : forall A e' op,
(forall s, ([op (var_e A) ]e_
(syntax_m.seplog_m.assert_m.expr_m.store.upd A [e' ]e_ s s) = [op e']e_s))%seplog_expr ->
(equivalent_pseudo_code
(while.cmd_cmd0 (A <- e') ; while.cmd_cmd0 (A <- op (var_e A)))
(while.cmd_cmd0 (A <- op e')))%seplog_expr%seplog_cmd.
Proof.
move=> A e' op Hop.
apply equivalent_pseudo_code_op with (op := fun a _ => op a).
exact (syntax_m.seplog_m.assert_m.expr_m.cst_e (A.nat2t 0)).
move=> s /=.
by rewrite Hop.
Qed.
Lemma equivalent_pseudo_code_example : forall A e',
(equivalent_pseudo_code
(while.cmd_cmd0 (A <- e') ; while.cmd_cmd0 (A <- var_e A ./e nat_e 2))
(while.cmd_cmd0 (A <- e' ./e nat_e 2)))%seplog_expr%seplog_cmd.
Proof.
move=> A e'.
apply equivalent_pseudo_code_op => s /=.
by rewrite syntax_m.seplog_m.assert_m.expr_m.store.get_upd'.
Qed.
Lemma equivalent_pseudo_code_example2 : forall v2 u,
u <> v2 ->
(equivalent_pseudo_code
(while.cmd_cmd0 (v2 <- nat_e 1%nat); while.cmd_cmd0 (v2 <- (var_e v2 .-e var_e u)))
(while.cmd_cmd0 (v2 <- (nat_e 1 .-e var_e u))))%seplog_expr%seplog_cmd.
Proof.
move=> v2 u v2_u.
apply equivalent_pseudo_code_op => s /=.
by rewrite syntax_m.seplog_m.assert_m.expr_m.store.get_upd' syntax_m.seplog_m.assert_m.expr_m.store.get_upd.
Qed.
Lemma equivalent_pseudo_code_example3 : forall A e',
(equivalent_pseudo_code
(while.cmd_cmd0 (A <- e') ; while.cmd_cmd0 (A <- .--e var_e A))
(while.cmd_cmd0 (A <- (.--e e'))))%seplog_expr%seplog_cmd.
Proof.
move=> A e'.
apply equivalent_pseudo_code_uop => s /=.
by rewrite syntax_m.seplog_m.assert_m.expr_m.store.get_upd'.
Qed.
Lemma equivalent_pseudo_code_example_assign : forall A e e',
(forall s, [ e ]e_s = [ e' ]e_s)%seplog_expr ->
(equivalent_pseudo_code
(while.cmd_cmd0 (A <- e))
(while.cmd_cmd0 (A <- e')))%seplog_expr%seplog_cmd.
Proof.
move=> A e e' H; rewrite /equivalent_pseudo_code => s s'; split => H'.
- move/syntax_m.seplog_m.semop_prop_m.exec_cmd0_inv : H'.
inversion 1 => //; subst. rewrite H.
by do 2 constructor.
- move/syntax_m.seplog_m.semop_prop_m.exec_cmd0_inv : H'.
inversion 1 => //; subst. rewrite -H.
by do 2 constructor.
Qed.
Lemma equivalent_pseudo_code_trans : forall a b c,
equivalent_pseudo_code a b -> equivalent_pseudo_code b c ->
equivalent_pseudo_code a c.
Proof.
move=> a b c; rewrite /equivalent_pseudo_code => a_b b_c s s'; split => [Ha | Hc].
by apply b_c, a_b.
by apply a_b, b_c.
Qed.
Lemma equivalent_pseudo_code_sym : forall a b,
equivalent_pseudo_code a b -> equivalent_pseudo_code b a.
Proof.
move=> a b; rewrite /equivalent_pseudo_code => H s s'; split => H'.
by rewrite H.
by rewrite -H.
Qed.
Lemma equivalent_pseudo_code_seq : forall a a' b b',
equivalent_pseudo_code a a' ->
equivalent_pseudo_code b b' ->
(equivalent_pseudo_code (a ; b) (a' ; b'))%seplog_cmd.
Proof.
move=> a a' b b' Ha Hb; move=> s s'; split => H.
case/syntax_m.seplog_m.hoare_prop_m.while_semop_prop_m.exec_seq_inv_Some : H.
case=> [s'' h''] [H1 H2].
apply while.exec_seq with (Some (s'', h'')).
by apply (proj1 (Ha _ _) H1).
by apply (proj1 (Hb _ _) H2).
case/syntax_m.seplog_m.hoare_prop_m.while_semop_prop_m.exec_seq_inv_Some : H.
case=> [s'' h''] [H1 H2].
apply while.exec_seq with (Some (s'', h'')).
by apply (proj2 (Ha _ _) H1).
by apply (proj2 (Hb _ _) H2).
Qed.
Lemma equivalent_pseudo_code_expr : forall A e' (e : syntax_m.seplog_m.assert_m.expr_m.expr),
(forall s, [e ]e_ s = [ e' ]e_s)%seplog_expr ->
(equivalent_pseudo_code
(while.cmd_cmd0 (A <- e'))
(while.cmd_cmd0 (A <- e)))%seplog_expr%seplog_cmd.
Proof.
move=> A e' e H.
rewrite /equivalent_pseudo_code; case=> [s h] [s' h']; split => HA.
move/syntax_m.seplog_m.hoare_prop_m.while_semop_prop_m.exec_cmd0_inv : HA.
case/syntax_m.seplog_m.exec0_assign_inv => [? ?]; subst h' s'.
rewrite -H.
by do 2 constructor.
move/syntax_m.seplog_m.hoare_prop_m.while_semop_prop_m.exec_cmd0_inv : HA.
case/syntax_m.seplog_m.exec0_assign_inv => [? ?]; subst h' s'.
rewrite H.
by do 2 constructor.
Qed.
Lemma fwd_sim_pcode_equiv : forall R P p p' c, fwd_sim R P p c ->
equivalent_pseudo_code p p' -> fwd_sim R P p' c.
Proof.
move=> R P p p' c p_c p_p' s st h HR HP s' Hp'.
move: {p_p' Hp'}(proj2 (p_p' _ _) Hp').
by move/(p_c _ _ _ HR HP).
Qed.
p' (Hp' : ~~ syntax_m.contains_malloc p') c c' P Q,
rela_hoare P Q p c -> fwd_sim R P p c -> fwd_sim R Q p' c' ->
fwd_sim R P (p ; p')%seplog_cmd (c ; c')%mips_cmd.
Proof.
move=> R p Hp p' Hp' c c' P Q HPQ Hfwd_sim_p Hfwd_sim_p'; move=> s st h HR HP s' Hexec_pp'.
case/syntax_m.seplog_m.semop_prop_m.exec_seq_inv : Hexec_pp' => s'' [Hexec_p Hexec_p'].
destruct s'' as [[s'' h'']|]; last by move/syntax_m.seplog_m.semop_prop_m.from_none : Hexec_p'.
move: (syntax_m.no_malloc_heap_invariant _ _ _ Hexec_p Hp s _ _ (refl_equal _) (refl_equal _)) => Hh''; subst h''.
case: {Hfwd_sim_p}(Hfwd_sim_p _ _ _ HR HP _ Hexec_p) => st'' [h'' [Hexec_c HR'']].
have HQ'' : Q s'' st'' h''.
rewrite /rela_hoare in HPQ; by apply HPQ with s st h.
case: {Hfwd_sim_p'}(Hfwd_sim_p' _ _ _ HR'' HQ'' _ Hexec_p') => st' [h' [Hexec_c' HR']].
exists st', h'; split; last by done.
by apply while.exec_seq with (Some (st'', h'')).
Qed.
Definition equivalent_pseudo_code p p' :=
forall s s', (Some s -- p ---> Some s')%seplog_cmd <-> (Some s -- p' ---> Some s')%seplog_cmd.
Lemma equivalent_pseudo_code_op : forall A e' (e : syntax_m.seplog_m.assert_m.expr_m.expr) op,
(forall s, ([op (var_e A) e ]e_
(syntax_m.seplog_m.assert_m.expr_m.store.upd A [e' ]e_ s s) = [op e' e]e_s))%seplog_expr ->
(equivalent_pseudo_code
(while.cmd_cmd0 (A <- e') ; while.cmd_cmd0 (A <- op (var_e A) e))
(while.cmd_cmd0 (A <- op e' e)))%seplog_expr%seplog_cmd.
Proof.
move=> A e' e op Hop.
rewrite /equivalent_pseudo_code; case=> [s h] [s' h']; split => HA.
case/syntax_m.seplog_m.hoare_prop_m.while_semop_prop_m.exec_seq_inv_Some : HA.
case=> [s'' h''] [HA1 HA2].
move/syntax_m.seplog_m.hoare_prop_m.while_semop_prop_m.exec_cmd0_inv : HA1.
case/syntax_m.seplog_m.exec0_assign_inv => [? ?]; subst h'' s''.
move/syntax_m.seplog_m.hoare_prop_m.while_semop_prop_m.exec_cmd0_inv : HA2.
case/syntax_m.seplog_m.exec0_assign_inv => [? ?]; subst h' s'.
constructor.
rewrite syntax_m.seplog_m.assert_m.expr_m.store.upd_upd_eq Hop; by constructor.
eapply while.exec_seq.
constructor.
by constructor.
constructor.
move/syntax_m.seplog_m.hoare_prop_m.while_semop_prop_m.exec_cmd0_inv : HA.
case/syntax_m.seplog_m.exec0_assign_inv => [? ?]; subst h' s'.
set s0 := syntax_m.seplog_m.assert_m.expr_m.store.upd A _ _.
set s1 := syntax_m.seplog_m.assert_m.expr_m.store.upd A _ _.
have -> : s1 = syntax_m.seplog_m.assert_m.expr_m.store.upd A
([ op (var_e A) e ]e_ s0)%seplog_expr s0.
by rewrite /s0 syntax_m.seplog_m.assert_m.expr_m.store.upd_upd_eq Hop.
by apply syntax_m.seplog_m.exec0_assign.
Qed.
Lemma equivalent_pseudo_code_uop : forall A e' op,
(forall s, ([op (var_e A) ]e_
(syntax_m.seplog_m.assert_m.expr_m.store.upd A [e' ]e_ s s) = [op e']e_s))%seplog_expr ->
(equivalent_pseudo_code
(while.cmd_cmd0 (A <- e') ; while.cmd_cmd0 (A <- op (var_e A)))
(while.cmd_cmd0 (A <- op e')))%seplog_expr%seplog_cmd.
Proof.
move=> A e' op Hop.
apply equivalent_pseudo_code_op with (op := fun a _ => op a).
exact (syntax_m.seplog_m.assert_m.expr_m.cst_e (A.nat2t 0)).
move=> s /=.
by rewrite Hop.
Qed.
Lemma equivalent_pseudo_code_example : forall A e',
(equivalent_pseudo_code
(while.cmd_cmd0 (A <- e') ; while.cmd_cmd0 (A <- var_e A ./e nat_e 2))
(while.cmd_cmd0 (A <- e' ./e nat_e 2)))%seplog_expr%seplog_cmd.
Proof.
move=> A e'.
apply equivalent_pseudo_code_op => s /=.
by rewrite syntax_m.seplog_m.assert_m.expr_m.store.get_upd'.
Qed.
Lemma equivalent_pseudo_code_example2 : forall v2 u,
u <> v2 ->
(equivalent_pseudo_code
(while.cmd_cmd0 (v2 <- nat_e 1%nat); while.cmd_cmd0 (v2 <- (var_e v2 .-e var_e u)))
(while.cmd_cmd0 (v2 <- (nat_e 1 .-e var_e u))))%seplog_expr%seplog_cmd.
Proof.
move=> v2 u v2_u.
apply equivalent_pseudo_code_op => s /=.
by rewrite syntax_m.seplog_m.assert_m.expr_m.store.get_upd' syntax_m.seplog_m.assert_m.expr_m.store.get_upd.
Qed.
Lemma equivalent_pseudo_code_example3 : forall A e',
(equivalent_pseudo_code
(while.cmd_cmd0 (A <- e') ; while.cmd_cmd0 (A <- .--e var_e A))
(while.cmd_cmd0 (A <- (.--e e'))))%seplog_expr%seplog_cmd.
Proof.
move=> A e'.
apply equivalent_pseudo_code_uop => s /=.
by rewrite syntax_m.seplog_m.assert_m.expr_m.store.get_upd'.
Qed.
Lemma equivalent_pseudo_code_example_assign : forall A e e',
(forall s, [ e ]e_s = [ e' ]e_s)%seplog_expr ->
(equivalent_pseudo_code
(while.cmd_cmd0 (A <- e))
(while.cmd_cmd0 (A <- e')))%seplog_expr%seplog_cmd.
Proof.
move=> A e e' H; rewrite /equivalent_pseudo_code => s s'; split => H'.
- move/syntax_m.seplog_m.semop_prop_m.exec_cmd0_inv : H'.
inversion 1 => //; subst. rewrite H.
by do 2 constructor.
- move/syntax_m.seplog_m.semop_prop_m.exec_cmd0_inv : H'.
inversion 1 => //; subst. rewrite -H.
by do 2 constructor.
Qed.
Lemma equivalent_pseudo_code_trans : forall a b c,
equivalent_pseudo_code a b -> equivalent_pseudo_code b c ->
equivalent_pseudo_code a c.
Proof.
move=> a b c; rewrite /equivalent_pseudo_code => a_b b_c s s'; split => [Ha | Hc].
by apply b_c, a_b.
by apply a_b, b_c.
Qed.
Lemma equivalent_pseudo_code_sym : forall a b,
equivalent_pseudo_code a b -> equivalent_pseudo_code b a.
Proof.
move=> a b; rewrite /equivalent_pseudo_code => H s s'; split => H'.
by rewrite H.
by rewrite -H.
Qed.
Lemma equivalent_pseudo_code_seq : forall a a' b b',
equivalent_pseudo_code a a' ->
equivalent_pseudo_code b b' ->
(equivalent_pseudo_code (a ; b) (a' ; b'))%seplog_cmd.
Proof.
move=> a a' b b' Ha Hb; move=> s s'; split => H.
case/syntax_m.seplog_m.hoare_prop_m.while_semop_prop_m.exec_seq_inv_Some : H.
case=> [s'' h''] [H1 H2].
apply while.exec_seq with (Some (s'', h'')).
by apply (proj1 (Ha _ _) H1).
by apply (proj1 (Hb _ _) H2).
case/syntax_m.seplog_m.hoare_prop_m.while_semop_prop_m.exec_seq_inv_Some : H.
case=> [s'' h''] [H1 H2].
apply while.exec_seq with (Some (s'', h'')).
by apply (proj2 (Ha _ _) H1).
by apply (proj2 (Hb _ _) H2).
Qed.
Lemma equivalent_pseudo_code_expr : forall A e' (e : syntax_m.seplog_m.assert_m.expr_m.expr),
(forall s, [e ]e_ s = [ e' ]e_s)%seplog_expr ->
(equivalent_pseudo_code
(while.cmd_cmd0 (A <- e'))
(while.cmd_cmd0 (A <- e)))%seplog_expr%seplog_cmd.
Proof.
move=> A e' e H.
rewrite /equivalent_pseudo_code; case=> [s h] [s' h']; split => HA.
move/syntax_m.seplog_m.hoare_prop_m.while_semop_prop_m.exec_cmd0_inv : HA.
case/syntax_m.seplog_m.exec0_assign_inv => [? ?]; subst h' s'.
rewrite -H.
by do 2 constructor.
move/syntax_m.seplog_m.hoare_prop_m.while_semop_prop_m.exec_cmd0_inv : HA.
case/syntax_m.seplog_m.exec0_assign_inv => [? ?]; subst h' s'.
rewrite H.
by do 2 constructor.
Qed.
Lemma fwd_sim_pcode_equiv : forall R P p p' c, fwd_sim R P p c ->
equivalent_pseudo_code p p' -> fwd_sim R P p' c.
Proof.
move=> R P p p' c p_c p_p' s st h HR HP s' Hp'.
move: {p_p' Hp'}(proj2 (p_p' _ _) Hp').
by move/(p_c _ _ _ HR HP).
Qed.
partial forward simulation
Definition pfwd_sim (R P0 : relat) (p : pcmd) (c : WMIPS_Semop.cmd) :=
forall s st h, R s st h -> P0 s st h ->
forall s', (Some (s, pemp) -- p ---> Some (s', pemp))%seplog_cmd ->
forall st' h', (Some (st, h) -- c ---> Some (st', h'))%mips_cmd ->
R s' st' h'.
Lemma pfwd_sim_stren : forall R (I0 I0' : relat) p c,
(forall s st h, I0 s st h -> I0' s st h) ->
pfwd_sim R I0' p c -> pfwd_sim R I0 p c.
Proof. move=> A I0 I0' p c H H' s st h HA HI0.
apply H' => //; by apply H. Qed.
Lemma pfwd_sim_is_rela_hoare : forall (R P0 : relat) (p : syntax_m.seplog_m.semop_m.cmd) (c : WMIPS_Semop.cmd),
rela_hoare (fun s st h => R s st h /\ P0 s st h) R p c <-> pfwd_sim R P0 p c.
Proof.
move=> R P0 p c; rewrite /rela_hoare /pfwd_sim; split=> H s st h.
- move=> HR HP0 s' Hexec_p st' h' Hexec_c.
by eapply H; eauto.
- move=> [HR HP0] s' Hexec_p st' h' Hexec_c.
by eapply H; eauto.
Qed.
Definition safe_termination (R : relat) c :=
forall s st h, R s st h -> exists s', (Some (st, h) -- c ---> Some s')%mips_cmd.
forall s st h, R s st h -> P0 s st h ->
forall s', (Some (s, pemp) -- p ---> Some (s', pemp))%seplog_cmd ->
forall st' h', (Some (st, h) -- c ---> Some (st', h'))%mips_cmd ->
R s' st' h'.
Lemma pfwd_sim_stren : forall R (I0 I0' : relat) p c,
(forall s st h, I0 s st h -> I0' s st h) ->
pfwd_sim R I0' p c -> pfwd_sim R I0 p c.
Proof. move=> A I0 I0' p c H H' s st h HA HI0.
apply H' => //; by apply H. Qed.
Lemma pfwd_sim_is_rela_hoare : forall (R P0 : relat) (p : syntax_m.seplog_m.semop_m.cmd) (c : WMIPS_Semop.cmd),
rela_hoare (fun s st h => R s st h /\ P0 s st h) R p c <-> pfwd_sim R P0 p c.
Proof.
move=> R P0 p c; rewrite /rela_hoare /pfwd_sim; split=> H s st h.
- move=> HR HP0 s' Hexec_p st' h' Hexec_c.
by eapply H; eauto.
- move=> [HR HP0] s' Hexec_p st' h' Hexec_c.
by eapply H; eauto.
Qed.
Definition safe_termination (R : relat) c :=
forall s st h, R s st h -> exists s', (Some (st, h) -- c ---> Some s')%mips_cmd.
partial forward simulation implies forward simulation
Lemma pfwd_sim_fwd_sim : forall (R P0 : relat) (p : pcmd) (c : WMIPS_Semop.cmd),
pfwd_sim R P0 p c -> safe_termination R c -> fwd_sim R P0 p c.
Proof.
move=> R P0 p c Hpfwd_sim Hterm_c s st h HR HP0 s' Hexec_p.
case: (Hterm_c _ _ _ HR).
move=> [st' h'] Hexec_c.
move: {Hpfwd_sim}(Hpfwd_sim _ _ _ HR HP0 _ Hexec_p _ _ Hexec_c) => Hpfwd_sim.
by exists st', h'.
Qed.
pfwd_sim R P0 p c -> safe_termination R c -> fwd_sim R P0 p c.
Proof.
move=> R P0 p c Hpfwd_sim Hterm_c s st h HR HP0 s' Hexec_p.
case: (Hterm_c _ _ _ HR).
move=> [st' h'] Hexec_c.
move: {Hpfwd_sim}(Hpfwd_sim _ _ _ HR HP0 _ Hexec_p _ _ Hexec_c) => Hpfwd_sim.
by exists st', h'.
Qed.
backward simulation
Definition bck_sim (R P0 : relat) (p : syntax_m.seplog_m.semop_m.cmd) (c : WMIPS_Semop.cmd) :=
forall s st h, R s st h -> P0 s st h ->
forall st' h', (Some (st, h) -- c ---> Some (st', h'))%mips_cmd ->
exists s', (Some (s, syntax_m.seplog_m.assert_m.heap.emp) -- p --->
Some (s', syntax_m.seplog_m.assert_m.heap.emp))%seplog_cmd /\ R s' st' h'.
Definition terminating p := forall s, exists s',
(Some (s, syntax_m.seplog_m.assert_m.heap.emp) -- p --->
Some (s', syntax_m.seplog_m.assert_m.heap.emp))%seplog_cmd.
forall s st h, R s st h -> P0 s st h ->
forall st' h', (Some (st, h) -- c ---> Some (st', h'))%mips_cmd ->
exists s', (Some (s, syntax_m.seplog_m.assert_m.heap.emp) -- p --->
Some (s', syntax_m.seplog_m.assert_m.heap.emp))%seplog_cmd /\ R s' st' h'.
Definition terminating p := forall s, exists s',
(Some (s, syntax_m.seplog_m.assert_m.heap.emp) -- p --->
Some (s', syntax_m.seplog_m.assert_m.heap.emp))%seplog_cmd.
forward simulation implies backward simulation
Lemma fwd_sim_bck_sim : forall R P0 p c,
terminating p -> fwd_sim R P0 p c -> bck_sim R P0 p c.
Proof.
move=> R P0 p c Hp.
rewrite /fwd_sim /bck_sim => Hfwd_sim_R s st h HR HP0 st' h' Hc.
case: (Classical_Prop.classic (exists s', (Some (s, syntax_m.seplog_m.assert_m.heap.emp) -- p --->
Some (s', syntax_m.seplog_m.assert_m.heap.emp))%seplog_cmd /\ ~ R s' st' h')) => X.
- case: X => s' [Hs' HR'].
move: {Hfwd_sim_R}(Hfwd_sim_R _ _ _ HR HP0 _ Hs') => Hfwd_sim_R.
case: Hfwd_sim_R => st'_ [h'_ [Hc_ HR'_]].
by case: (mips_syntax.semop_deter_prop_m.exec_deter _ _ _ Hc _ Hc_) => Hst' Hh'; subst st'_ h'_.
- have {X}X : forall s', (~ (Some (s, syntax_m.seplog_m.assert_m.heap.emp) -- p --->
Some (s', syntax_m.seplog_m.assert_m.heap.emp))%seplog_cmd) \/ R s' st' h'.
move/Classical_Pred_Type.not_ex_all_not : X => X s'.
move/Classical_Prop.not_and_or: {X}(X s').
case; first by auto.
right; by apply Classical_Prop.NNPP.
case: {Hp}(Hp s) => s' Hp.
case: {X}(X s') => // HR'.
by exists s'.
Qed.
terminating p -> fwd_sim R P0 p c -> bck_sim R P0 p c.
Proof.
move=> R P0 p c Hp.
rewrite /fwd_sim /bck_sim => Hfwd_sim_R s st h HR HP0 st' h' Hc.
case: (Classical_Prop.classic (exists s', (Some (s, syntax_m.seplog_m.assert_m.heap.emp) -- p --->
Some (s', syntax_m.seplog_m.assert_m.heap.emp))%seplog_cmd /\ ~ R s' st' h')) => X.
- case: X => s' [Hs' HR'].
move: {Hfwd_sim_R}(Hfwd_sim_R _ _ _ HR HP0 _ Hs') => Hfwd_sim_R.
case: Hfwd_sim_R => st'_ [h'_ [Hc_ HR'_]].
by case: (mips_syntax.semop_deter_prop_m.exec_deter _ _ _ Hc _ Hc_) => Hst' Hh'; subst st'_ h'_.
- have {X}X : forall s', (~ (Some (s, syntax_m.seplog_m.assert_m.heap.emp) -- p --->
Some (s', syntax_m.seplog_m.assert_m.heap.emp))%seplog_cmd) \/ R s' st' h'.
move/Classical_Pred_Type.not_ex_all_not : X => X s'.
move/Classical_Prop.not_and_or: {X}(X s').
case; first by auto.
right; by apply Classical_Prop.NNPP.
case: {Hp}(Hp s) => s' Hp.
case: {X}(X s') => // HR'.
by exists s'.
Qed.
simulation of a boolean expression
Definition fwd_sim_b (R : relat) (b : syntax_m.seplog_m.assert_m.expr_m.expr_b) (pre_b : while.cmd) (post_b : expr_b) :=
forall s st he, R s st he ->
exists st', (Some (st, he) -- pre_b ---> Some (st', he))%mips_cmd /\
((([ b ]b_ s)%seplog_expr -> eval_b post_b st') /\
((~~ [ b ]b_s)%seplog_expr -> ~~ eval_b post_b st')).
Definition fwd_sim_b' (R : relat) (b : syntax_m.seplog_m.assert_m.expr_m.expr_b) (pre_b : while.cmd) (post_b : expr_b) :=
forall s st he, R s st he ->
(([ b ]b_ s)%seplog_expr ->
exists st', (Some (st, he) -- pre_b ---> Some (st', he))%mips_cmd /\ eval_b post_b st') /\
(~~ ([ b ]b_ s)%seplog_expr ->
exists st', (Some (st, he) -- pre_b ---> Some (st', he))%mips_cmd /\ ~~ eval_b post_b st').
Lemma fwd_sim_b_fwd_sim_b' : forall R b pre_b post_b,
fwd_sim_b R b pre_b post_b <-> fwd_sim_b' R b pre_b post_b.
Proof.
move=> R b pre_b post_b; rewrite /fwd_sim_b /fwd_sim_b'; split=> Hb s st h.
- case/(Hb _) => st' [Hexec_pre_b [Ht Hf]]; split=> ?; exists st'; by auto.
- case/(Hb _) => Ht Hf; destruct ([ b ]b_s)%seplog_expr.
+ case: (Ht (refl_equal _)) => st' ?; exists st'; split; by intuition.
+ case: (Hf (refl_equal _)) => st' ?; exists st'; split; by intuition.
Qed.
Lemma fwd_sim_b_stren : forall (R R' : relat) p c bt,
(forall s st h, R s st h -> R' s st h) ->
fwd_sim_b R' p c bt -> fwd_sim_b R p c bt.
Proof.
move=> R R' p c bt R'R H; rewrite /fwd_sim_b => s st h HR.
by apply (H s st h (R'R _ _ _ HR)).
Qed.
Lemma fwd_sim_b_cond : forall (R : relat) p p' c bt,
(forall s st h, R s st h -> ([ p ]b_s = [ p' ]b_s)%seplog_expr) ->
fwd_sim_b R p' c bt -> fwd_sim_b R p c bt.
Proof.
move=> R p p' c bt Hp H.
rewrite /fwd_sim_b => s st h HR.
case: (H s st h HR) => st' Hst'.
exists st'.
rewrite (Hp _ _ _ HR); tauto.
Qed.
Lemma fwd_sim_b_cond_neg : forall (R : relat) p p' c bt bt',
(forall s st h, R s st h -> ([ p ]b_s = ~~ [ p' ]b_s)%seplog_expr) ->
(forall st, (eval_b bt st = ~~ eval_b bt' st)%mips_expr) ->
fwd_sim_b R p' c bt' -> fwd_sim_b R p c bt.
Proof.
move=> R p p' c bt bt' Hp Hbt H.
rewrite /fwd_sim_b => s st h HR.
case: (H s st h HR) => st' Hst'.
exists st'.
rewrite (Hp _ _ _ HR).
rewrite (Hbt st').
split; first by tauto.
split; first by tauto.
do 2 apply contra; tauto.
Qed.
Definition inv_R (R : relat) (c : while.cmd) :=
forall s st h, R s st h -> forall st' h', (Some (st, h) -- c ---> Some (st', h'))%mips_cmd -> R s st' h'.
Lemma inv_R_equiv : forall (R R' : relat) p,
(forall s st h, R' s st h <-> R s st h) -> inv_R R p -> inv_R R' p.
Proof.
move=> R R' p H R_p.
rewrite /inv_R => s st h HR' st' h' exec_p.
rewrite /inv_R in R_p.
apply H.
apply R_p with st h => //.
by apply H.
Qed.
forall s st he, R s st he ->
exists st', (Some (st, he) -- pre_b ---> Some (st', he))%mips_cmd /\
((([ b ]b_ s)%seplog_expr -> eval_b post_b st') /\
((~~ [ b ]b_s)%seplog_expr -> ~~ eval_b post_b st')).
Definition fwd_sim_b' (R : relat) (b : syntax_m.seplog_m.assert_m.expr_m.expr_b) (pre_b : while.cmd) (post_b : expr_b) :=
forall s st he, R s st he ->
(([ b ]b_ s)%seplog_expr ->
exists st', (Some (st, he) -- pre_b ---> Some (st', he))%mips_cmd /\ eval_b post_b st') /\
(~~ ([ b ]b_ s)%seplog_expr ->
exists st', (Some (st, he) -- pre_b ---> Some (st', he))%mips_cmd /\ ~~ eval_b post_b st').
Lemma fwd_sim_b_fwd_sim_b' : forall R b pre_b post_b,
fwd_sim_b R b pre_b post_b <-> fwd_sim_b' R b pre_b post_b.
Proof.
move=> R b pre_b post_b; rewrite /fwd_sim_b /fwd_sim_b'; split=> Hb s st h.
- case/(Hb _) => st' [Hexec_pre_b [Ht Hf]]; split=> ?; exists st'; by auto.
- case/(Hb _) => Ht Hf; destruct ([ b ]b_s)%seplog_expr.
+ case: (Ht (refl_equal _)) => st' ?; exists st'; split; by intuition.
+ case: (Hf (refl_equal _)) => st' ?; exists st'; split; by intuition.
Qed.
Lemma fwd_sim_b_stren : forall (R R' : relat) p c bt,
(forall s st h, R s st h -> R' s st h) ->
fwd_sim_b R' p c bt -> fwd_sim_b R p c bt.
Proof.
move=> R R' p c bt R'R H; rewrite /fwd_sim_b => s st h HR.
by apply (H s st h (R'R _ _ _ HR)).
Qed.
Lemma fwd_sim_b_cond : forall (R : relat) p p' c bt,
(forall s st h, R s st h -> ([ p ]b_s = [ p' ]b_s)%seplog_expr) ->
fwd_sim_b R p' c bt -> fwd_sim_b R p c bt.
Proof.
move=> R p p' c bt Hp H.
rewrite /fwd_sim_b => s st h HR.
case: (H s st h HR) => st' Hst'.
exists st'.
rewrite (Hp _ _ _ HR); tauto.
Qed.
Lemma fwd_sim_b_cond_neg : forall (R : relat) p p' c bt bt',
(forall s st h, R s st h -> ([ p ]b_s = ~~ [ p' ]b_s)%seplog_expr) ->
(forall st, (eval_b bt st = ~~ eval_b bt' st)%mips_expr) ->
fwd_sim_b R p' c bt' -> fwd_sim_b R p c bt.
Proof.
move=> R p p' c bt bt' Hp Hbt H.
rewrite /fwd_sim_b => s st h HR.
case: (H s st h HR) => st' Hst'.
exists st'.
rewrite (Hp _ _ _ HR).
rewrite (Hbt st').
split; first by tauto.
split; first by tauto.
do 2 apply contra; tauto.
Qed.
Definition inv_R (R : relat) (c : while.cmd) :=
forall s st h, R s st h -> forall st' h', (Some (st, h) -- c ---> Some (st', h'))%mips_cmd -> R s st' h'.
Lemma inv_R_equiv : forall (R R' : relat) p,
(forall s st h, R' s st h <-> R s st h) -> inv_R R p -> inv_R R' p.
Proof.
move=> R R' p H R_p.
rewrite /inv_R => s st h HR' st' h' exec_p.
rewrite /inv_R in R_p.
apply H.
apply R_p with st h => //.
by apply H.
Qed.
simulation of while-loops
Lemma fwd_sim_while : forall b pre_b post_b p c
(Hnomalloc : ~~ syntax_m.contains_malloc p) R P0,
inv_R (fun s st h => R s st h /\ P0 s st h) pre_b ->
rela_hoare (fun s st h => P0 s st h /\ eval_b post_b st /\
([ b ]b_s)%seplog_expr) P0 p c ->
fwd_sim_b (fun s st h => R s st h /\ P0 s st h) b pre_b post_b ->
fwd_sim R (fun s st h => P0 s st h /\
eval_b post_b st /\
([ b ]b_s)%seplog_expr) p c ->
fwd_sim R P0 (while.while b p) (pre_b ; while.while (post_b) (c ; pre_b))%mips_cmd.
Proof.
move=> b pre_b post_b p c Hnomalloc R P0 Hinv HP0_pc Hsimu_b Hpc.
move=> s st h HR HP0 s'.
move HST : (Some (s, _)) => ST.
move HST' : (Some (s', _)) => ST'.
move Hw : (while.while _ _) => w Hexec_w.
move: Hexec_w b pre_b post_b p c Hnomalloc P0 Hinv HP0_pc Hsimu_b Hpc s st h HR HP0 s' HST HST' Hw.
elim => //.
- move=> {ST ST' w} [s h_] ST' ST'' b p Heval_b_s Hexec_p _ Hexec_while IH_while b_ pre_b post_b p_ c
Hnomalloc P0 Hinv HP0_pc Hsimu_b Hpc s_ st h HR HP0 s''.
case=> X Y; subst s_ h_.
move=> HST''.
case=> X Y; subst b_ p_.
destruct ST' as [[s' h']|]; last by subst ST''; by move/syntax_m.seplog_m.semop_prop_m.from_none : Hexec_while.
have : h' = syntax_m.seplog_m.assert_m.heap.emp.
by move: (syntax_m.no_malloc_heap_invariant _ _ _ Hexec_p Hnomalloc s s' h' (refl_equal _) (refl_equal _)).
move=> Hh'; subst h'.
move: {IH_while}(IH_while b pre_b post_b p c Hnomalloc P0 Hinv HP0_pc Hsimu_b Hpc s') => IH_while.
case: (Hsimu_b _ _ _ (conj HR HP0) ) => st1 [Hexec_pre_b []].
move/(_ Heval_b_s) => Heval_b_post_b _.
have HR1 : R s st1 h.
exact (proj1 (Hinv s st h (conj HR HP0) _ _ Hexec_pre_b)).
rewrite /fwd_sim in Hpc.
have HP01 : P0 s st1 h /\ eval_b post_b st1 /\
syntax_m.seplog_m.assert_m.expr_m.eval_b b s.
move: (proj2 (Hinv s st h (conj HR HP0) _ _ Hexec_pre_b)).
tauto.
case: {Hpc}(Hpc _ _ _ HR1 HP01 _ Hexec_p) => st2 [h2 [Hc' HR2]].
have HP02 : P0 s' st2 h2 by apply HP0_pc with s st1 h.
move: {IH_while}(IH_while st2 h2 HR2 HP02 s'' (refl_equal _) HST'' (refl_equal _)) =>
[st'' [h'' [Hexec_asm HR'']]].
exists st'', h''; split; last by done.
apply while.exec_seq with (Some (st1, h)); first by done.
apply mips_cmd.semop_prop_m.while_seq'; first by done.
apply mips_cmd.semop_prop_m.exec_seq_assoc'.
by apply while.exec_seq with (Some (st2, h2)).
- move=> {ST ST' w} [s h_] b c Hb b_ pre_b post_b p_ c_ Hnomalloc P0 Hinv
HP0_p_c_ Hsimu_b Hp_c_ s_ st h HR HP0 s__.
case=> X Y; subst s_ h_.
case=> X; subst s__.
case=> X Y; subst b_ p_.
case: (Hsimu_b _ _ _ (conj HR HP0)) => st1 [Hexec_pre_b []] _.
move/(_ Hb) => Heval_post_b.
exists st1, h; split.
+ move/while.exec_seq : Hexec_pre_b; apply.
by apply while.exec_while_false.
+ exact (proj1 (Hinv s st h (conj HR HP0) _ _ Hexec_pre_b)).
Qed.
Lemma fwd_sim_while_alt : forall b pre_b post_b p c
(Hnomalloc : ~~ syntax_m.contains_malloc p) R P0,
inv_R (fun s st h => R s st h /\ P0 s st h) pre_b ->
fwd_sim_b (fun s st h => R s st h /\ P0 s st h) b pre_b post_b ->
fwd_sim (fun s st h => R s st h /\ P0 s st h) (fun s st h => eval_b post_b st /\
([ b ]b_s)%seplog_expr) p c ->
fwd_sim R P0 (while.while b p) (pre_b ; while.while (post_b) (c ; pre_b))%mips_cmd.
Proof.
move=> b pre_b post_b p c Hnomalloc R P0 Hinv Hsimu_b Hpc.
move=> s st h HR HP0 s'.
move HST : (Some (s, _)) => ST.
move HST' : (Some (s', _)) => ST'.
move Hw : (while.while _ _) => w Hexec_w.
move: Hexec_w b pre_b post_b p c Hnomalloc P0 Hinv Hsimu_b Hpc s st h HR HP0 s' HST HST' Hw.
elim => //.
- move=> {ST ST' w} [s h_] ST' ST'' b p Heval_b_s Hexec_p _ Hexec_while IH_while b_ pre_b post_b p_ c
Hnomalloc P0 Hinv Hsimu_b Hpc s_ st h HR HP0 s''.
case=> X Y; subst s_ h_.
move=> HST''.
case=> X Y; subst b_ p_.
destruct ST' as [[s' h']|]; last by subst ST''; by move/syntax_m.seplog_m.semop_prop_m.from_none : Hexec_while.
have : h' = syntax_m.seplog_m.assert_m.heap.emp.
by move: (syntax_m.no_malloc_heap_invariant _ _ _ Hexec_p Hnomalloc s s' h' (refl_equal _) (refl_equal _)).
move=> Hh'; subst h'.
move: {IH_while}(IH_while b pre_b post_b p c Hnomalloc P0 Hinv Hsimu_b Hpc s') => IH_while.
case: (Hsimu_b _ _ _ (conj HR HP0)) => st1 [Hexec_pre_b []].
move/(_ Heval_b_s) => Heval_b_post_b _.
have HR1 : R s st1 h.
exact (proj1 (Hinv s st h (conj HR HP0) _ _ Hexec_pre_b)).
rewrite /fwd_sim in Hpc.
have HP01 : P0 s st1 h /\ eval_b post_b st1 /\
syntax_m.seplog_m.assert_m.expr_m.eval_b b s.
move: (proj2 (Hinv s st h (conj HR HP0) _ _ Hexec_pre_b)).
tauto.
case: (Hpc _ _ _ (conj HR1 (proj1 HP01)) (proj2 HP01) _ Hexec_p) => st2 [h2 [Hc' HR2]].
move: {IH_while}(IH_while st2 h2 (proj1 HR2) (proj2 HR2) s'' (refl_equal _) HST'' (refl_equal _)) =>
[st'' [h'' [Hexec_asm HR'']]].
exists st'', h''; split; last by done.
apply while.exec_seq with (Some (st1, h)); first by done.
apply mips_cmd.semop_prop_m.while_seq'; first by done.
apply mips_cmd.semop_prop_m.exec_seq_assoc'.
by apply while.exec_seq with (Some (st2, h2)).
- move=> {ST ST' w} [s h_] b c Hb b_ pre_b post_b p_ c_ Hnomalloc P0 Hinv
Hsimu_b Hp_c_ s_ st h HR HP0 s__.
case=> X Y; subst s_ h_.
case=> X; subst s__.
case=> X Y; subst b_ p_.
case: (Hsimu_b _ _ _ (conj HR HP0)) => st1 [Hexec_pre_b []] _.
move/(_ Hb) => Heval_post_b.
exists st1, h; split.
+ move/while.exec_seq : Hexec_pre_b; apply.
by apply while.exec_while_false.
+ exact (proj1 (Hinv s st h (conj HR HP0) _ _ Hexec_pre_b)).
Qed.
Lemma fwd_sim_ifte : forall b pre_b post_b p1 p2 c1 c2
(Hnomalloc1 : ~~ syntax_m.contains_malloc p1) (Hnomalloc2 : ~~ syntax_m.contains_malloc p2) R P0,
inv_R (fun s st h => R s st h /\ P0 s st h) pre_b ->
fwd_sim_b R b pre_b post_b ->
fwd_sim R (fun s st h => P0 s st h /\ eval_b post_b st /\ ([ b ]b_s)%seplog_expr) p1 c1 ->
fwd_sim R (fun s st h => P0 s st h /\ ~~ eval_b post_b st /\ ~~ ([ b ]b_s)%seplog_expr) p2 c2 ->
fwd_sim R P0 (while.ifte b p1 p2) (pre_b ; while.ifte (post_b) c1 c2)%mips_cmd.
Proof.
move=> b pre_b post_b p1 p2 c1 c2 Hnomalloc1 Hnomalloc2 R P0 Hinv Hsimu_b Hp1c1 Hp2c2.
move=> s st h HR HP0 s'.
move HST : (Some (s, _)) => ST.
move HST' : (Some (s', _)) => ST'.
move Hp : (while.ifte _ _ _) => p Hexec_p.
move: Hexec_p b pre_b post_b p1 p2 c1 c2 Hnomalloc1 Hnomalloc2 P0 Hinv Hsimu_b Hp1c1 Hp2c2 s st h HR HP0 s' HST HST' Hp.
elim => //.
- move=> {ST ST' p} [s h_] ST1 b p1 p2 Heval_b_s Hexec_p1 _ b_ pre_b post_b p1_ p2_ c1 c2
Hnomalloc1 Hnomalloc2 P0 Hinv Hsimu_b Hp1c1 Hp2c2 s_ st h HR HP0 s''.
case=> ? ?; subst s_ h_.
move=> HST''.
case=> ? ? ?; subst b_ p1_ p2_.
destruct ST1 as [[s1 h1]|]; last by done.
have : h1 = syntax_m.seplog_m.assert_m.heap.emp.
by move: (syntax_m.no_malloc_heap_invariant _ _ _ Hexec_p1 Hnomalloc1 s s1 h1 (refl_equal _) (refl_equal _)).
move=> ?; subst h1.
case: HST'' => ?; subst s''.
case: (Hsimu_b _ _ _ HR) => st1 [Hexec_pre_b []].
move/(_ Heval_b_s) => Heval_b_post_b _.
have HR1 : R s st1 h by exact (proj1 (Hinv s st h (conj HR HP0) _ _ Hexec_pre_b)).
rewrite /fwd_sim in Hp1c1.
have HP01 : P0 s st1 h /\ eval_b post_b st1 /\ ([ b ]b_s)%seplog_expr.
have HP01 : P0 s st1 h.
exact (proj2 (Hinv s st h (conj HR HP0) _ _ Hexec_pre_b)).
tauto.
case: {Hp1c1}(Hp1c1 _ _ _ HR1 HP01 _ Hexec_p1) => st2 [h2 [Hc' HR2]].
exists st2, h2; split; last by done.
apply while.exec_seq with (Some (st1, h)) => //.
by apply while.exec_ifte_true.
- move=> {ST ST' p} [s h_] ST2 b p1 p2 Heval_b_s Hexec_p1 _ b_ pre_b post_b p1_ p2_ c1 c2
Hnomalloc1 Hnomalloc2 P0 Hinv Hsimu_b Hp1c1 Hp2c2 s_ st h HR HP0 s''.
case=> ? ?; subst s_ h_.
move=> HST''.
case=> ? ? ?; subst b_ p1_ p2_.
destruct ST2 as [[s2 h2]|]; last by done.
have : h2 = syntax_m.seplog_m.assert_m.heap.emp.
by move: (syntax_m.no_malloc_heap_invariant _ _ _ Hexec_p1 Hnomalloc2 s s2 h2 (refl_equal _) (refl_equal _)).
move=> ?; subst h2.
case: HST'' => ?; subst s''.
case: (Hsimu_b _ _ _ HR) => st2 [Hexec_pre_b []] _.
move/(_ Heval_b_s) => Heval_b_post_b.
have HR2 : R s st2 h.
exact (proj1 (Hinv s st h (conj HR HP0) _ _ Hexec_pre_b)).
rewrite /fwd_sim in Hp2c2.
have HP02 : P0 s st2 h /\ ~~ eval_b post_b st2 /\ ~~ ([ b ]b_s)%seplog_expr.
by move: (proj2 (Hinv s st h (conj HR HP0) _ _ Hexec_pre_b)) => HP01.
case: {Hp2c2}(Hp2c2 _ _ _ HR2 HP02 _ Hexec_p1) => st1 [h1 [Hc' HR2_]].
exists st1, h1; split; last by done.
apply while.exec_seq with (Some (st2, h)) => //.
by apply while.exec_ifte_false.
Qed.
End Simu.
Module Import simu_m := Simu ZIT.
Module heap_tac_m := finmap.Map_Tac heap.
Lemma fwd_sim_nop : forall R I0, fwd_sim R I0 syntax_m.seplog_m.skip nop.
Proof.
move=> R I0. rewrite /fwd_sim. move=> s st h HR HI0 s'.
move/syntax_m.seplog_m.hoare_prop_m.while_semop_prop_m.exec_cmd0_inv.
inversion 1; subst.
exists st, h; split; [by do 2 constructor | exact HR].
Qed.
Lemma equivalent_pseudo_code_op : forall A e' (e : syntax_m.seplog_m.assert_m.expr_m.expr) op,
(forall s, ([op (var_e A) e ]e_
(syntax_m.seplog_m.assert_m.expr_m.store.upd A [e' ]e_ s s) = [op e' e]e_s))%seplog_expr ->
(equivalent_pseudo_code
(A <- e' ; A <- op (var_e A) e)
(A <- op e' e))%seplog_expr%seplog_cmd.
Proof.
move=> A e' e op Hop.
rewrite /equivalent_pseudo_code; case=> [s h] [s' h']; split => HA.
case/syntax_m.seplog_m.hoare_prop_m.while_semop_prop_m.exec_seq_inv_Some : HA.
case=> [s'' h''] [HA1 HA2].
move/syntax_m.seplog_m.hoare_prop_m.while_semop_prop_m.exec_cmd0_inv : HA1.
case/syntax_m.seplog_m.exec0_assign_inv => [? ?]; subst h'' s''.
move/syntax_m.seplog_m.hoare_prop_m.while_semop_prop_m.exec_cmd0_inv : HA2.
case/syntax_m.seplog_m.exec0_assign_inv => [? ?]; subst h' s'.
constructor.
rewrite syntax_m.seplog_m.assert_m.expr_m.store.upd_upd_eq Hop; by constructor.
eapply while.exec_seq.
constructor.
by constructor.
constructor.
move/syntax_m.seplog_m.hoare_prop_m.while_semop_prop_m.exec_cmd0_inv : HA.
case/syntax_m.seplog_m.exec0_assign_inv => [? ?]; subst h' s'.
set s0 := syntax_m.seplog_m.assert_m.expr_m.store.upd A _ _.
set s1 := syntax_m.seplog_m.assert_m.expr_m.store.upd A _ _.
have -> : s1 = syntax_m.seplog_m.assert_m.expr_m.store.upd A
([ op (var_e A) e ]e_ s0)%seplog_expr s0.
by rewrite /s0 syntax_m.seplog_m.assert_m.expr_m.store.upd_upd_eq Hop.
by apply syntax_m.seplog_m.exec0_assign.
Qed.
(Hnomalloc : ~~ syntax_m.contains_malloc p) R P0,
inv_R (fun s st h => R s st h /\ P0 s st h) pre_b ->
rela_hoare (fun s st h => P0 s st h /\ eval_b post_b st /\
([ b ]b_s)%seplog_expr) P0 p c ->
fwd_sim_b (fun s st h => R s st h /\ P0 s st h) b pre_b post_b ->
fwd_sim R (fun s st h => P0 s st h /\
eval_b post_b st /\
([ b ]b_s)%seplog_expr) p c ->
fwd_sim R P0 (while.while b p) (pre_b ; while.while (post_b) (c ; pre_b))%mips_cmd.
Proof.
move=> b pre_b post_b p c Hnomalloc R P0 Hinv HP0_pc Hsimu_b Hpc.
move=> s st h HR HP0 s'.
move HST : (Some (s, _)) => ST.
move HST' : (Some (s', _)) => ST'.
move Hw : (while.while _ _) => w Hexec_w.
move: Hexec_w b pre_b post_b p c Hnomalloc P0 Hinv HP0_pc Hsimu_b Hpc s st h HR HP0 s' HST HST' Hw.
elim => //.
- move=> {ST ST' w} [s h_] ST' ST'' b p Heval_b_s Hexec_p _ Hexec_while IH_while b_ pre_b post_b p_ c
Hnomalloc P0 Hinv HP0_pc Hsimu_b Hpc s_ st h HR HP0 s''.
case=> X Y; subst s_ h_.
move=> HST''.
case=> X Y; subst b_ p_.
destruct ST' as [[s' h']|]; last by subst ST''; by move/syntax_m.seplog_m.semop_prop_m.from_none : Hexec_while.
have : h' = syntax_m.seplog_m.assert_m.heap.emp.
by move: (syntax_m.no_malloc_heap_invariant _ _ _ Hexec_p Hnomalloc s s' h' (refl_equal _) (refl_equal _)).
move=> Hh'; subst h'.
move: {IH_while}(IH_while b pre_b post_b p c Hnomalloc P0 Hinv HP0_pc Hsimu_b Hpc s') => IH_while.
case: (Hsimu_b _ _ _ (conj HR HP0) ) => st1 [Hexec_pre_b []].
move/(_ Heval_b_s) => Heval_b_post_b _.
have HR1 : R s st1 h.
exact (proj1 (Hinv s st h (conj HR HP0) _ _ Hexec_pre_b)).
rewrite /fwd_sim in Hpc.
have HP01 : P0 s st1 h /\ eval_b post_b st1 /\
syntax_m.seplog_m.assert_m.expr_m.eval_b b s.
move: (proj2 (Hinv s st h (conj HR HP0) _ _ Hexec_pre_b)).
tauto.
case: {Hpc}(Hpc _ _ _ HR1 HP01 _ Hexec_p) => st2 [h2 [Hc' HR2]].
have HP02 : P0 s' st2 h2 by apply HP0_pc with s st1 h.
move: {IH_while}(IH_while st2 h2 HR2 HP02 s'' (refl_equal _) HST'' (refl_equal _)) =>
[st'' [h'' [Hexec_asm HR'']]].
exists st'', h''; split; last by done.
apply while.exec_seq with (Some (st1, h)); first by done.
apply mips_cmd.semop_prop_m.while_seq'; first by done.
apply mips_cmd.semop_prop_m.exec_seq_assoc'.
by apply while.exec_seq with (Some (st2, h2)).
- move=> {ST ST' w} [s h_] b c Hb b_ pre_b post_b p_ c_ Hnomalloc P0 Hinv
HP0_p_c_ Hsimu_b Hp_c_ s_ st h HR HP0 s__.
case=> X Y; subst s_ h_.
case=> X; subst s__.
case=> X Y; subst b_ p_.
case: (Hsimu_b _ _ _ (conj HR HP0)) => st1 [Hexec_pre_b []] _.
move/(_ Hb) => Heval_post_b.
exists st1, h; split.
+ move/while.exec_seq : Hexec_pre_b; apply.
by apply while.exec_while_false.
+ exact (proj1 (Hinv s st h (conj HR HP0) _ _ Hexec_pre_b)).
Qed.
Lemma fwd_sim_while_alt : forall b pre_b post_b p c
(Hnomalloc : ~~ syntax_m.contains_malloc p) R P0,
inv_R (fun s st h => R s st h /\ P0 s st h) pre_b ->
fwd_sim_b (fun s st h => R s st h /\ P0 s st h) b pre_b post_b ->
fwd_sim (fun s st h => R s st h /\ P0 s st h) (fun s st h => eval_b post_b st /\
([ b ]b_s)%seplog_expr) p c ->
fwd_sim R P0 (while.while b p) (pre_b ; while.while (post_b) (c ; pre_b))%mips_cmd.
Proof.
move=> b pre_b post_b p c Hnomalloc R P0 Hinv Hsimu_b Hpc.
move=> s st h HR HP0 s'.
move HST : (Some (s, _)) => ST.
move HST' : (Some (s', _)) => ST'.
move Hw : (while.while _ _) => w Hexec_w.
move: Hexec_w b pre_b post_b p c Hnomalloc P0 Hinv Hsimu_b Hpc s st h HR HP0 s' HST HST' Hw.
elim => //.
- move=> {ST ST' w} [s h_] ST' ST'' b p Heval_b_s Hexec_p _ Hexec_while IH_while b_ pre_b post_b p_ c
Hnomalloc P0 Hinv Hsimu_b Hpc s_ st h HR HP0 s''.
case=> X Y; subst s_ h_.
move=> HST''.
case=> X Y; subst b_ p_.
destruct ST' as [[s' h']|]; last by subst ST''; by move/syntax_m.seplog_m.semop_prop_m.from_none : Hexec_while.
have : h' = syntax_m.seplog_m.assert_m.heap.emp.
by move: (syntax_m.no_malloc_heap_invariant _ _ _ Hexec_p Hnomalloc s s' h' (refl_equal _) (refl_equal _)).
move=> Hh'; subst h'.
move: {IH_while}(IH_while b pre_b post_b p c Hnomalloc P0 Hinv Hsimu_b Hpc s') => IH_while.
case: (Hsimu_b _ _ _ (conj HR HP0)) => st1 [Hexec_pre_b []].
move/(_ Heval_b_s) => Heval_b_post_b _.
have HR1 : R s st1 h.
exact (proj1 (Hinv s st h (conj HR HP0) _ _ Hexec_pre_b)).
rewrite /fwd_sim in Hpc.
have HP01 : P0 s st1 h /\ eval_b post_b st1 /\
syntax_m.seplog_m.assert_m.expr_m.eval_b b s.
move: (proj2 (Hinv s st h (conj HR HP0) _ _ Hexec_pre_b)).
tauto.
case: (Hpc _ _ _ (conj HR1 (proj1 HP01)) (proj2 HP01) _ Hexec_p) => st2 [h2 [Hc' HR2]].
move: {IH_while}(IH_while st2 h2 (proj1 HR2) (proj2 HR2) s'' (refl_equal _) HST'' (refl_equal _)) =>
[st'' [h'' [Hexec_asm HR'']]].
exists st'', h''; split; last by done.
apply while.exec_seq with (Some (st1, h)); first by done.
apply mips_cmd.semop_prop_m.while_seq'; first by done.
apply mips_cmd.semop_prop_m.exec_seq_assoc'.
by apply while.exec_seq with (Some (st2, h2)).
- move=> {ST ST' w} [s h_] b c Hb b_ pre_b post_b p_ c_ Hnomalloc P0 Hinv
Hsimu_b Hp_c_ s_ st h HR HP0 s__.
case=> X Y; subst s_ h_.
case=> X; subst s__.
case=> X Y; subst b_ p_.
case: (Hsimu_b _ _ _ (conj HR HP0)) => st1 [Hexec_pre_b []] _.
move/(_ Hb) => Heval_post_b.
exists st1, h; split.
+ move/while.exec_seq : Hexec_pre_b; apply.
by apply while.exec_while_false.
+ exact (proj1 (Hinv s st h (conj HR HP0) _ _ Hexec_pre_b)).
Qed.
Lemma fwd_sim_ifte : forall b pre_b post_b p1 p2 c1 c2
(Hnomalloc1 : ~~ syntax_m.contains_malloc p1) (Hnomalloc2 : ~~ syntax_m.contains_malloc p2) R P0,
inv_R (fun s st h => R s st h /\ P0 s st h) pre_b ->
fwd_sim_b R b pre_b post_b ->
fwd_sim R (fun s st h => P0 s st h /\ eval_b post_b st /\ ([ b ]b_s)%seplog_expr) p1 c1 ->
fwd_sim R (fun s st h => P0 s st h /\ ~~ eval_b post_b st /\ ~~ ([ b ]b_s)%seplog_expr) p2 c2 ->
fwd_sim R P0 (while.ifte b p1 p2) (pre_b ; while.ifte (post_b) c1 c2)%mips_cmd.
Proof.
move=> b pre_b post_b p1 p2 c1 c2 Hnomalloc1 Hnomalloc2 R P0 Hinv Hsimu_b Hp1c1 Hp2c2.
move=> s st h HR HP0 s'.
move HST : (Some (s, _)) => ST.
move HST' : (Some (s', _)) => ST'.
move Hp : (while.ifte _ _ _) => p Hexec_p.
move: Hexec_p b pre_b post_b p1 p2 c1 c2 Hnomalloc1 Hnomalloc2 P0 Hinv Hsimu_b Hp1c1 Hp2c2 s st h HR HP0 s' HST HST' Hp.
elim => //.
- move=> {ST ST' p} [s h_] ST1 b p1 p2 Heval_b_s Hexec_p1 _ b_ pre_b post_b p1_ p2_ c1 c2
Hnomalloc1 Hnomalloc2 P0 Hinv Hsimu_b Hp1c1 Hp2c2 s_ st h HR HP0 s''.
case=> ? ?; subst s_ h_.
move=> HST''.
case=> ? ? ?; subst b_ p1_ p2_.
destruct ST1 as [[s1 h1]|]; last by done.
have : h1 = syntax_m.seplog_m.assert_m.heap.emp.
by move: (syntax_m.no_malloc_heap_invariant _ _ _ Hexec_p1 Hnomalloc1 s s1 h1 (refl_equal _) (refl_equal _)).
move=> ?; subst h1.
case: HST'' => ?; subst s''.
case: (Hsimu_b _ _ _ HR) => st1 [Hexec_pre_b []].
move/(_ Heval_b_s) => Heval_b_post_b _.
have HR1 : R s st1 h by exact (proj1 (Hinv s st h (conj HR HP0) _ _ Hexec_pre_b)).
rewrite /fwd_sim in Hp1c1.
have HP01 : P0 s st1 h /\ eval_b post_b st1 /\ ([ b ]b_s)%seplog_expr.
have HP01 : P0 s st1 h.
exact (proj2 (Hinv s st h (conj HR HP0) _ _ Hexec_pre_b)).
tauto.
case: {Hp1c1}(Hp1c1 _ _ _ HR1 HP01 _ Hexec_p1) => st2 [h2 [Hc' HR2]].
exists st2, h2; split; last by done.
apply while.exec_seq with (Some (st1, h)) => //.
by apply while.exec_ifte_true.
- move=> {ST ST' p} [s h_] ST2 b p1 p2 Heval_b_s Hexec_p1 _ b_ pre_b post_b p1_ p2_ c1 c2
Hnomalloc1 Hnomalloc2 P0 Hinv Hsimu_b Hp1c1 Hp2c2 s_ st h HR HP0 s''.
case=> ? ?; subst s_ h_.
move=> HST''.
case=> ? ? ?; subst b_ p1_ p2_.
destruct ST2 as [[s2 h2]|]; last by done.
have : h2 = syntax_m.seplog_m.assert_m.heap.emp.
by move: (syntax_m.no_malloc_heap_invariant _ _ _ Hexec_p1 Hnomalloc2 s s2 h2 (refl_equal _) (refl_equal _)).
move=> ?; subst h2.
case: HST'' => ?; subst s''.
case: (Hsimu_b _ _ _ HR) => st2 [Hexec_pre_b []] _.
move/(_ Heval_b_s) => Heval_b_post_b.
have HR2 : R s st2 h.
exact (proj1 (Hinv s st h (conj HR HP0) _ _ Hexec_pre_b)).
rewrite /fwd_sim in Hp2c2.
have HP02 : P0 s st2 h /\ ~~ eval_b post_b st2 /\ ~~ ([ b ]b_s)%seplog_expr.
by move: (proj2 (Hinv s st h (conj HR HP0) _ _ Hexec_pre_b)) => HP01.
case: {Hp2c2}(Hp2c2 _ _ _ HR2 HP02 _ Hexec_p1) => st1 [h1 [Hc' HR2_]].
exists st1, h1; split; last by done.
apply while.exec_seq with (Some (st2, h)) => //.
by apply while.exec_ifte_false.
Qed.
End Simu.
Module Import simu_m := Simu ZIT.
Module heap_tac_m := finmap.Map_Tac heap.
Lemma fwd_sim_nop : forall R I0, fwd_sim R I0 syntax_m.seplog_m.skip nop.
Proof.
move=> R I0. rewrite /fwd_sim. move=> s st h HR HI0 s'.
move/syntax_m.seplog_m.hoare_prop_m.while_semop_prop_m.exec_cmd0_inv.
inversion 1; subst.
exists st, h; split; [by do 2 constructor | exact HR].
Qed.
Lemma equivalent_pseudo_code_op : forall A e' (e : syntax_m.seplog_m.assert_m.expr_m.expr) op,
(forall s, ([op (var_e A) e ]e_
(syntax_m.seplog_m.assert_m.expr_m.store.upd A [e' ]e_ s s) = [op e' e]e_s))%seplog_expr ->
(equivalent_pseudo_code
(A <- e' ; A <- op (var_e A) e)
(A <- op e' e))%seplog_expr%seplog_cmd.
Proof.
move=> A e' e op Hop.
rewrite /equivalent_pseudo_code; case=> [s h] [s' h']; split => HA.
case/syntax_m.seplog_m.hoare_prop_m.while_semop_prop_m.exec_seq_inv_Some : HA.
case=> [s'' h''] [HA1 HA2].
move/syntax_m.seplog_m.hoare_prop_m.while_semop_prop_m.exec_cmd0_inv : HA1.
case/syntax_m.seplog_m.exec0_assign_inv => [? ?]; subst h'' s''.
move/syntax_m.seplog_m.hoare_prop_m.while_semop_prop_m.exec_cmd0_inv : HA2.
case/syntax_m.seplog_m.exec0_assign_inv => [? ?]; subst h' s'.
constructor.
rewrite syntax_m.seplog_m.assert_m.expr_m.store.upd_upd_eq Hop; by constructor.
eapply while.exec_seq.
constructor.
by constructor.
constructor.
move/syntax_m.seplog_m.hoare_prop_m.while_semop_prop_m.exec_cmd0_inv : HA.
case/syntax_m.seplog_m.exec0_assign_inv => [? ?]; subst h' s'.
set s0 := syntax_m.seplog_m.assert_m.expr_m.store.upd A _ _.
set s1 := syntax_m.seplog_m.assert_m.expr_m.store.upd A _ _.
have -> : s1 = syntax_m.seplog_m.assert_m.expr_m.store.upd A
([ op (var_e A) e ]e_ s0)%seplog_expr s0.
by rewrite /s0 syntax_m.seplog_m.assert_m.expr_m.store.upd_upd_eq Hop.
by apply syntax_m.seplog_m.exec0_assign.
Qed.
memory int: multi-precision integers pointed to by registers
Inductive mint : Type :=
| unsign of reg & reg
| signed of nat & reg .
Definition mintP (t1 t2 : mint) : bool :=
match t1, t2 with
| unsign r1 r1', unsign r2 r2' => regP r1 r2 && regP r1' r2'
| signed l1 r1, signed l2 r2 => beq_nat l1 l2 && regP r1 r2
| _, _ => false
end.
Lemma mintP_eq : forall n m, mintP n m -> n = m.
Proof.
case=> // [u1 u1'|l1 s1] // [u2 u2'|l2 s2] //= H.
- case/andP : H; move/eqP=> ->; by move/eqP=> ->.
- case/andP : H.
move/beq_nat_true => ->.
by move/eqP => ->.
Qed.
Lemma mintP_refl : forall n, mintP n n.
Proof.
case=> [r1 r1'|l1 s1] /=.
- apply/andP; split; by apply/eqregP.
- rewrite -beq_nat_refl /=; by apply/eqregP.
Qed.
Lemma eqmintP : Equality.axiom mintP.
Proof.
move=> n m. apply: (iffP idP) => [H | <-].
- move: (mintP_eq n m); tauto.
- by rewrite mintP_refl.
Qed.
Canonical Structure mint_eqMixin := EqMixin eqmintP.
Canonical Structure mint_eqType := Eval hnf in EqType _ mint_eqMixin.
Definition mint_regs t :=
match t with
| unsign rk rx => rk :: rx :: nil
| signed n rx => rx :: nil
end.
Lemma mint_regs_unsigned1 : forall a b, In a (mint_regs (unsign a b)).
Proof. move=> a b /=; by auto. Qed.
Lemma mint_regs_unsigned2 : forall a b, In a (mint_regs (unsign b a)).
Proof. move=> a b /=; by auto. Qed.
Definition mints_regs d := flat_map mint_regs d.
Lemma In_mints_regs : forall d rx t, In rx (mint_regs t) -> In t d ->
In rx (mints_regs d).
Proof.
elim=> // h t IH rx [rk ry|l ry] /=.
- case.
+ move=> ?; subst rx.
case=> [-> | H]; apply in_or_app.
* left; rewrite /=. by intuition.
* right; apply: (IH _ _ _ H); rewrite /=; by intuition.
+ case=> // ?; subst ry.
case=> [->|H]; apply in_or_app.
* left; rewrite /=; by intuition.
* right; apply: (IH _ _ _ H) => /=; by intuition.
- case=> // ?; subst rx.
case=> [->|H]; apply in_or_app.
+ left; by rewrite /=; intuition.
+ right; apply: (IH _ _ _ H) => /=; by intuition.
Qed.
Lemma incl_mint_regs : forall d r, In r d -> incl (mint_regs r) (mints_regs d).
Proof.
elim=> // hd tl IH r /= [] H x Hx.
- rewrite H.
apply in_or_app; by left.
- apply in_or_app.
move/IH : Hx => Hx.
right; by apply Hx.
Qed.
Lemma Permutation_mints_regs : Permutation_preserving mints_regs.
Proof.
rewrite /Permutation_preserving.
induction 1 => /=.
- by apply Permutation_refl.
- by apply Permutation_app_head.
- rewrite -!app_ass; by apply Permutation_app_tail, Permutation_app_swap.
- by eapply Permutation_trans; eauto.
Qed.
Definition mint_ptr t := match t with unsign _ rx => rx | signed _ rx => rx end.
Lemma nodup_mint_ptr : forall l, nodup (map mint_ptr l) -> nodup l.
Proof.
elim=> // hd tl IH /=.
case/andP => H1 H2.
apply/andP.
split; last by auto.
move/negP : H1 => H1.
apply/negP.
contradict H1.
apply/(In_inb_true regP_eq regP_refl).
apply in_map.
by apply/(In_inb_true mintP_eq mintP_refl).
Qed.
Lemma not_In_mint_ptr : forall l t, ~ In (mint_ptr t) (map mint_ptr l) -> ~ In t l.
Proof.
elim=> // h t IH ty /= X.
contradict X; case : X => [<-|X].
- by left.
- move: {IH}(IH ty); tauto.
Qed.
| unsign of reg & reg
| signed of nat & reg .
Definition mintP (t1 t2 : mint) : bool :=
match t1, t2 with
| unsign r1 r1', unsign r2 r2' => regP r1 r2 && regP r1' r2'
| signed l1 r1, signed l2 r2 => beq_nat l1 l2 && regP r1 r2
| _, _ => false
end.
Lemma mintP_eq : forall n m, mintP n m -> n = m.
Proof.
case=> // [u1 u1'|l1 s1] // [u2 u2'|l2 s2] //= H.
- case/andP : H; move/eqP=> ->; by move/eqP=> ->.
- case/andP : H.
move/beq_nat_true => ->.
by move/eqP => ->.
Qed.
Lemma mintP_refl : forall n, mintP n n.
Proof.
case=> [r1 r1'|l1 s1] /=.
- apply/andP; split; by apply/eqregP.
- rewrite -beq_nat_refl /=; by apply/eqregP.
Qed.
Lemma eqmintP : Equality.axiom mintP.
Proof.
move=> n m. apply: (iffP idP) => [H | <-].
- move: (mintP_eq n m); tauto.
- by rewrite mintP_refl.
Qed.
Canonical Structure mint_eqMixin := EqMixin eqmintP.
Canonical Structure mint_eqType := Eval hnf in EqType _ mint_eqMixin.
Definition mint_regs t :=
match t with
| unsign rk rx => rk :: rx :: nil
| signed n rx => rx :: nil
end.
Lemma mint_regs_unsigned1 : forall a b, In a (mint_regs (unsign a b)).
Proof. move=> a b /=; by auto. Qed.
Lemma mint_regs_unsigned2 : forall a b, In a (mint_regs (unsign b a)).
Proof. move=> a b /=; by auto. Qed.
Definition mints_regs d := flat_map mint_regs d.
Lemma In_mints_regs : forall d rx t, In rx (mint_regs t) -> In t d ->
In rx (mints_regs d).
Proof.
elim=> // h t IH rx [rk ry|l ry] /=.
- case.
+ move=> ?; subst rx.
case=> [-> | H]; apply in_or_app.
* left; rewrite /=. by intuition.
* right; apply: (IH _ _ _ H); rewrite /=; by intuition.
+ case=> // ?; subst ry.
case=> [->|H]; apply in_or_app.
* left; rewrite /=; by intuition.
* right; apply: (IH _ _ _ H) => /=; by intuition.
- case=> // ?; subst rx.
case=> [->|H]; apply in_or_app.
+ left; by rewrite /=; intuition.
+ right; apply: (IH _ _ _ H) => /=; by intuition.
Qed.
Lemma incl_mint_regs : forall d r, In r d -> incl (mint_regs r) (mints_regs d).
Proof.
elim=> // hd tl IH r /= [] H x Hx.
- rewrite H.
apply in_or_app; by left.
- apply in_or_app.
move/IH : Hx => Hx.
right; by apply Hx.
Qed.
Lemma Permutation_mints_regs : Permutation_preserving mints_regs.
Proof.
rewrite /Permutation_preserving.
induction 1 => /=.
- by apply Permutation_refl.
- by apply Permutation_app_head.
- rewrite -!app_ass; by apply Permutation_app_tail, Permutation_app_swap.
- by eapply Permutation_trans; eauto.
Qed.
Definition mint_ptr t := match t with unsign _ rx => rx | signed _ rx => rx end.
Lemma nodup_mint_ptr : forall l, nodup (map mint_ptr l) -> nodup l.
Proof.
elim=> // hd tl IH /=.
case/andP => H1 H2.
apply/andP.
split; last by auto.
move/negP : H1 => H1.
apply/negP.
contradict H1.
apply/(In_inb_true regP_eq regP_refl).
apply in_map.
by apply/(In_inb_true mintP_eq mintP_refl).
Qed.
Lemma not_In_mint_ptr : forall l t, ~ In (mint_ptr t) (map mint_ptr l) -> ~ In t l.
Proof.
elim=> // h t IH ty /= X.
contradict X; case : X => [<-|X].
- by left.
- move: {IH}(IH ty); tauto.
Qed.
sign-magnitude representation
Definition var_signed k rx val st h : Prop :=
u2Z ([ rx ]_st)%mips_expr + 4 * 2 < Zbeta 1 /\
exists slen, exists ptr, exists A, length A = k /\
s2Z slen = Zsgn (s2Z slen) * Z_of_nat k /\
Zsgn (s2Z slen) = Zsgn val /\
Zabs val < Zbeta k /\
u2Z ptr + 4 * Z_of_nat k < Zbeta 1 /\
val = Zsgn (s2Z slen) * Sum k A /\
((var_e rx |--> slen :: ptr :: nil) ** (int_e ptr |--> A))%mips_expr%mips_assert st h.
Local Open Scope simu_scope.
Definition var_unsign k rx val st h : Prop :=
u2Z ([ rx ]_st)%mips_expr + 4 * Z_of_nat k < Zbeta 1 /\
0 <= val < Zbeta k /\
(var_e rx |--> Z2ints 32 k val)%mips_expr%mips_assert st h.
Definition var_mint (x : bipl.var.v) (t : mint) : relat := fun s st h =>
match t with
| unsign rk rx =>
var_unsign (Zabs_nat (u2Z ([ rk ]_st))%mips_expr) rx ([ x ]_s)%seplog_expr st h
| signed nk rx =>
var_signed nk rx ( [ x ]_s )%seplog_expr st h
end.
Lemma var_mint_invariant_unsign : forall x rk rx s s' st st' h,
([ rx ]_ st = [ rx ]_ st')%mips_expr -> ([ rk ]_ st = [ rk ]_ st')%mips_expr ->
([ x ]_s = [ x ]_s')%seplog_expr ->
var_mint x (unsign rk rx) s st h ->
var_mint x (unsign rk rx) s' st' h.
Proof.
move=> x rk rx_ s s' st st' h Hrx Hrk Hx.
rewrite /var_mint /var_unsign Hrk Hx Hrx.
case=> Hfit [Hover Hmem].
split; first by tauto.
split; first by tauto.
move: Hmem; by apply assert_m.mapstos_ext.
Qed.
Lemma var_mint_invariant_signed : forall x nk rx s s' st st' h,
([ rx ]_ st = [ rx ]_ st')%mips_expr -> ([ x ]_s = [ x ]_s')%seplog_expr ->
var_mint x (signed nk rx) s st h ->
var_mint x (signed nk rx) s' st' h.
Proof.
move=> x nk rx s s' st st' h Hrx Hx.
rewrite /var_mint /var_signed Hx.
case=> rx_fit [slen [ptr [A [A_nk [nk_slen [fit [sign [bound [Sum_A mem]]]]]]]]].
split; first by rewrite -Hrx.
exists slen, ptr, A.
repeat (split; first by done).
move: mem; apply assert_m.monotony => h'; by apply assert_m.mapstos_ext.
Qed.
Lemma var_mint_invariant : forall (x : bipl.var.v) t (s s' : pstore)
(st st' : store.t) (h : heap.t),
(forall rx, In rx (mint_regs t) -> [rx ]_ st = [rx ]_ st')%mips_expr ->
([x ]_ s = [x ]_ s')%seplog_expr ->
var_mint x t s st h -> var_mint x t s' st' h.
Proof.
move=> x [rk rx | nk rx] s s' st st' h H1 H2.
apply var_mint_invariant_unsign.
apply H1. simpl. by intuition.
apply H1. simpl. by intuition.
done.
apply var_mint_invariant_signed.
apply H1. simpl. by intuition.
exact H2.
Qed.
Notation "k '---' l" := (heap.dif k l) (at level 69) : heap_scope.
Notation "k '+++' m" := (heap.union k m) (at level 69) : heap_scope.
Notation "k '#' m" := (heap.disj k m) (at level 79) : heap_scope.
Notation "k '[\m]' m" := (heap.difs k m) (at level 69) : heap_scope.
Local Open Scope heap_scope.
Definition heap_cut h (x : heap.l) (k : nat) := heap.proj h (seq_ext.l2s (List.seq x k)).
Definition heap_mint (t : mint) (st : store.t) h : heap.t :=
match t with
| unsign rk rx =>
(heap_cut h (Zabs_nat (u2Z [rx]_st / 4)) (Zabs_nat (u2Z [rk]_st)))%mips_expr
| signed nk rx =>
let olen := heap.get (Zabs_nat (u2Z [rx]_st / 4))%mips_expr h in
let optr := heap.get (Zabs_nat (u2Z ([rx ]_ st [.+] four32) / 4))%mips_expr h in
match olen, optr with
| Some len, Some ptr =>
heap_cut h (Zabs_nat (u2Z [rx]_st / 4))%mips_expr 2 +++
heap_cut h (Zabs_nat (u2Z ptr / 4)) nk
| _, _ => h
end
end.
Lemma var_mint_length_heap_to_list : forall x s rk rx st h,
var_mint x (unsign rk rx) s st (heap_mint (unsign rk rx) st h)%mips_expr ->
(length (heap2list (Zabs_nat (u2Z ([rx ]_ st) / 4)) (Zabs_nat (u2Z ([rk ]_ st))) h) =
Zabs_nat (u2Z ([rk ]_ st)))%mips_expr.
Proof.
move=> x s rk rx st h H.
rewrite len_heap2list //.
case: H => Hfit [Hover Hmem].
move/assert_m.mapstos_inv_dom : Hmem.
rewrite len_Z2ints.
move/(_ Hfit) => ->.
rewrite -/(Equality.sort heap.l). apply/seq_ext.incP.
by rewrite heap.inc_dom_proj_dom.
Qed.
Lemma var_signed_exists_get_ptr : forall x nk rx s st h,
var_mint x (signed nk rx) s st h ->
exists ptr, heap.get (Zabs_nat (u2Z ([rx]_st [.+] four32)%mips_expr / 4)) h = Some ptr.
Proof.
move=> x nk rx s st h.
case=> rx_fit.
case=> slen [ptr [A [A_nk [Hlen [Hsgn [Hx [ptr_fit [Sum_A Hmem]]]]]]]].
exists ptr.
rewrite /= in Hmem.
rewrite !assert_m.con_assoc_equiv assert_m.con_com_equiv !assert_m.con_assoc_equiv in Hmem.
case: Hmem => h1 [h2 [h1_d_h2 [h1_U_h2 [Hh1 Hh2]]]].
case: Hh1 => p [Hp Hh1].
rewrite Hp h1_U_h2.
apply heap.get_union_L => //.
by rewrite Hh1 Zmult_comm Z_div_mult_full // Zabs_nat_Z_of_nat // heap.get_sing.
Qed.
Lemma var_signed_exists_get_slen : forall x nk rx s st h,
var_mint x (signed nk rx) s st h ->
exists slen, heap.get (Zabs_nat (u2Z ([rx]_st)%mips_expr / 4)) h = Some slen.
Proof.
move=> x nk rx s st h.
case=> rx_fit.
case=> slen [ptr [A [A_nk [Hlen [Hsgn [Hx [ptr_fit [Sum_A Hmem]]]]]]]].
exists slen.
rewrite /= in Hmem.
rewrite !assert_m.con_assoc_equiv in Hmem.
case: Hmem => h1 [h2 [h1_d_h2 [h1_U_h2 [Hh1 Hh2]]]].
case: Hh1 => p [Hp Hh1].
rewrite Hp h1_U_h2.
apply heap.get_union_L => //.
by rewrite Hh1 Zmult_comm Z_div_mult_full // Zabs_nat_Z_of_nat // heap.get_sing.
Qed.
Module heap_prop_m := finmap.Map_Prop heap.
Lemma con_heap_mint_signed_con_TT : forall st h nk rx Q P,
(Q ** P)%mips_assert st (heap_mint (signed nk rx) st h) ->
(Q ** assert_m.TT)%mips_assert st h.
Proof.
move=> st h nk rx Q P [h1 [h2 [h1dh2 [h1Uh2 [Hh1 Hh2]]]]].
exists h1, (h [\m] (heap.dom h1)).
split; first by apply heap.disj_difs', seq_ext.inc_refl.
split; last by done.
rewrite /= in h1Uh2; move: h1Uh2.
move Heq : (heap.get (Zabs_nat (u2Z ([rx ]_ st)%mips_expr / 4)) h) => [slen'|]; last first.
move=> ->; by rewrite heap_prop_m.union_difs_L_old.
move Heq2 : (heap.get (Zabs_nat (u2Z (([rx ]_ st)%mips_expr[.+]four32) / 4)) h) => [ptr'|]; last first.
move=> ->; by rewrite heap_prop_m.union_difs_L_old.
move=> H0.
apply heap.union_difs; last by reflexivity.
have : heap.inclu h1 (h1 +++ h2) by apply heap_prop_m.inclu_union_L_old.
rewrite -H0 -heap.proj_app.
by move/heap.proj_inclu.
Qed.
Lemma heap_mint_signed_proj : forall st h nk rA ptrA lenA,
(var_e rA |--> lenA :: ptrA :: nil ** assert_m.TT)%mips_expr%mips_assert st (heap_mint (signed nk rA) st h) ->
heap_mint (signed nk rA) st h = heap.proj h (seq.cat
(seq_ext.l2s (seq (Zabs_nat (u2Z ([rA ]_ st)%mips_expr / 4)) 2))
(seq_ext.l2s
(seq (Zabs_nat (u2Z ([ int_e ptrA ]e_ st)%mips_expr / 4)) nk))).
Proof.
move=> st h nk rA ptrA lenA mem.
simpl assert_m.mapstos in mem.
move/con_heap_mint_signed_con_TT : (mem).
rewrite mips_bipl.assert_m.con_assoc_equiv.
move/mips_bipl.assert_m.mapsto_con_get.
simpl heap_mint.
move=> ->.
move/con_heap_mint_signed_con_TT : mem.
rewrite mips_bipl.assert_m.con_assoc_equiv.
rewrite mips_bipl.assert_m.con_com_equiv.
rewrite 2!mips_bipl.assert_m.con_assoc_equiv.
move/mips_bipl.assert_m.mapsto_con_get.
move=> ->.
by rewrite /heap_cut -heap.proj_app.
Qed.
Lemma heap_mint_signed_unchanged : forall st' st h n s, ([ s ]_ st = [ s ]_ st')%mips_expr ->
heap_mint (signed n s) st h = heap_mint (signed n s) st' h.
Proof. move=> st' st h n s H; by rewrite /heap_mint -H. Qed.
Lemma heap_mint_unsign_unchanged : forall st' st h rk rx,
([ rk ]_ st = [ rk ]_ st')%mips_expr -> ([ rx ]_ st = [ rx ]_ st')%mips_expr ->
heap_mint (unsign rk rx) st h = heap_mint (unsign rk rx) st' h.
Proof. move=> st' st h rk rx Hrk Hrx; by rewrite /heap_mint -Hrk -Hrx. Qed.
Lemma heap_mint_unchanged : forall st' st h t,
(forall x, In x (mint_regs t) -> ([x ]_ st = [x ]_ st')%mips_expr) ->
heap_mint t st h = heap_mint t st' h.
Proof.
move=> st' st h t Ht.
destruct t as [rk rx|rx].
apply heap_mint_unsign_unchanged; apply Ht; simpl; intuition.
apply heap_mint_signed_unchanged; apply Ht; simpl; intuition.
Qed.
Lemma var_mint_unsign_dom_heap_mint : forall x s rk rx st h,
var_mint x (unsign rk rx) s st (heap_mint (unsign rk rx) st h) ->
heap.dom (heap_mint (unsign rk rx) st h) =
seq_ext.l2s (List.seq (Zabs_nat (u2Z ([rx ]_ st) / 4)) (Zabs_nat (u2Z ([rk ]_ st))))%mips_expr.
Proof.
move=> x s rk rx st h.
case => Hfit [Hover Hheap].
apply assert_m.mapstos_inv_dom in Hheap => //; last by rewrite len_Z2ints.
rewrite len_Z2ints in Hheap.
by rewrite Hheap /heap_cut /heap_mint seq_ext.l2s2l.
Qed.
Lemma heap_inclu_heap_mint_signed : forall h st nk rx, heap.inclu (heap_mint (signed nk rx) st h) h.
Proof.
move=> h st nk rx /=.
set a := heap.get _ _.
destruct a as [a|]; last by apply heap.inclu_refl.
set b := heap.get _ _.
destruct b as [b|]; last by apply heap.inclu_refl.
rewrite /heap_cut.
by apply heap_prop_m.inclu_union; apply heap.inclu_proj.
Qed.
Lemma dom_heap_mint_unsign_unchanged2 : forall h h' rk rx st st' x s,
([rk ]_ st = [rk ]_ st')%mips_expr ->
([rx ]_ st = [rx ]_ st')%mips_expr ->
var_mint x (unsign rk rx) s st (heap_mint (unsign rk rx) st h) ->
heap.dom h = heap.dom h' ->
heap.dom (heap_mint (unsign rk rx) st h) = heap.dom (heap_mint (unsign rk rx) st' h').
Proof.
move=> h h' rk rx st st' x s Hrk Hrx_invariant Hnew H_h_h' /=.
rewrite -Hrx_invariant -Hrk /heap_cut.
have Htmp' : seq_ext.l2s (List.seq (Zabs_nat (u2Z ([rx ]_ st) / 4)) (Zabs_nat (u2Z ([rk ]_ st))))%mips_expr =
heap.dom (heap_cut h (Zabs_nat (u2Z ([rx ]_ st) / 4)) (Zabs_nat (u2Z ([rk ]_ st))))%mips_expr.
case : Hnew => Hfit [Hover Hmem].
apply assert_m.mapstos_inv_dom in Hmem => //; last by rewrite len_Z2ints.
rewrite len_Z2ints in Hmem.
by rewrite Hmem /heap_cut /heap_mint seq_ext.l2s2l.
have Htmp'' : seq_ext.l2s (List.seq (Zabs_nat (u2Z ([rx ]_ st') / 4)) (Zabs_nat (u2Z ([rk ]_ st'))))%mips_expr =
heap.dom (heap_cut h (Zabs_nat (u2Z ([rx ]_ st') / 4)) (Zabs_nat (u2Z ([rk ]_ st'))))%mips_expr.
case : Hnew => Hfit [Hover Hmem].
apply assert_m.mapstos_inv_dom in Hmem => //; last by rewrite len_Z2ints.
rewrite len_Z2ints in Hmem.
by rewrite -Hrx_invariant -Hrk Hmem /heap_cut /heap_mint seq_ext.l2s2l.
by rewrite -Htmp' -(heap.dom_dom_proj h).
Qed.
Lemma heap_get_heap_mint_inv : forall x s h t y,
heap.get x (heap_mint t s h) = Some y -> heap.get x h = Some y.
Proof.
move=> x s h [ rk rx | nk rx] y /= H.
- rewrite /heap_cut in H.
move/heap_prop_m.get_proj_Some_inv : (H) => H'.
by rewrite heap.get_proj in H.
- move: H.
move H1 : (heap.get (Zabs_nat (u2Z ([rx ]_ s)%mips_expr / 4)) _) => [a|] //.
move H2 : (heap.get (Zabs_nat (u2Z (([rx ]_ s)%mips_expr[.+]four32) / 4)) _) => [b|] //.
case/heap.get_union_Some_inv => H.
+ move/heap_prop_m.get_proj_Some_inv : (H) => H'.
by rewrite heap.get_proj in H.
+ move/heap_prop_m.get_proj_Some_inv : (H) => H'.
by rewrite heap.get_proj in H.
Qed.
Lemma dom_heap_mint_sign_unchanged2 : forall h h' nk rx st st' x s slen slen',
([rx ]_ st = [rx ]_ st')%mips_expr ->
(heap.get (Zabs_nat (u2Z [rx]_ st / 4)) h = Some slen)%mips_expr ->
(heap.get (Zabs_nat (u2Z [rx]_ st' / 4)) h' = Some slen')%mips_expr ->
(heap.get ((Zabs_nat (u2Z ([rx]_ st [.+] four32) / 4))) h =
heap.get ((Zabs_nat (u2Z ([rx]_ st' [.+] four32) / 4))) h')%mips_expr ->
var_mint x (signed nk rx) s st (heap_mint (signed nk rx) st h) ->
heap.dom h = heap.dom h' ->
heap.dom (heap_mint (signed nk rx) st h) = heap.dom (heap_mint (signed nk rx) st' h').
Proof.
move=> h h' nk rx st st' x s slen slen' Hrx Hslen Hslen' Hptr Hvar_mint h_h'.
case: Hvar_mint => header_fit [slen_ [ptr [A [A_nk [Hnk [Hsgn [Hx [payload_fit [Sum_A H]]]]]]]]].
case: H => h1 [h2 [Hdisj [Hunion [Hh1 Hh2]]]].
rewrite /=.
have ? : slen = slen_.
have X : heap.get (Zabs_nat (u2Z ([rx ]_ st)%mips_expr / 4)) (heap_mint (signed nk rx) st h) = Some slen_.
rewrite Hunion.
apply heap.get_union_L => //.
rewrite /= in Hh1.
case: Hh1 => h11 [h12 [h11_d_h12 [h11_U_h12 [Hh11 Hh12]]]].
case: Hh11 => p [Hp Hh11].
rewrite h11_U_h12.
apply heap.get_union_L => //.
by rewrite Hh11 Hp Zmult_comm Z_div_mult_full // Zabs_nat_Z_of_nat heap.get_sing.
move/heap_get_heap_mint_inv : X.
rewrite Hslen.
by case.
subst slen_.
have H'slen : heap.get (Zabs_nat (u2Z ([rx ]_ st)%mips_expr / 4)) h = Some slen.
have H'slen : heap.get (Zabs_nat (u2Z ([rx ]_ st)%mips_expr / 4)) h1 = Some slen.
rewrite -(plus_0_r (Zabs_nat (u2Z ([rx ]_ st)%mips_expr / 4))).
rewrite -/(eval (var_e rx) st)%mips_expr.
apply (assert_m.mapstos_get_inv 2 (slen :: ptr :: List.nil)%list) => //; by auto.
apply heap_get_heap_mint_inv with st (signed nk rx).
rewrite Hunion; by apply heap.get_union_L.
have H'ptr: heap.get ((Zabs_nat (u2Z ([rx ]_ st [.+] four32 )%mips_expr / 4))) h = Some ptr.
have H'ptr : heap.get (Zabs_nat (u2Z ([rx ]_ st)%mips_expr / 4) + 1)%nat h1 = Some ptr.
rewrite -/(eval (var_e rx) st)%mips_expr.
apply (assert_m.mapstos_get_inv 2 (slen :: ptr :: List.nil)%list) => //; by auto.
apply heap_get_heap_mint_inv with st (signed nk rx).
rewrite u2Z_add_Z2u //.
rewrite -{1}(Zmult_1_l 4) Z_div_plus_full // Zabs_nat_plus_pos //; last first.
by apply Z_div_pos => //; apply min_u2Z.
rewrite (_ : Zabs_nat 1 = 1%nat) //.
rewrite Hunion; by apply heap.get_union_L.
rewrite -/(Zbeta 1); omega.
move: Hunion => /=.
rewrite H'slen Hslen' H'ptr.
move=> Hunion.
rewrite -Hptr H'ptr /heap_cut -heap.proj_app -heap.proj_app -Hrx.
by apply heap.dom_dom_proj.
Qed.
Lemma dom_heap_mint_signed_unchanged : forall h h' nk rx st st' x s,
([rx ]_ st = [rx ]_ st')%mips_expr ->
(heap.get (Zabs_nat (u2Z [rx]_ st / 4)) h = heap.get (Zabs_nat (u2Z [rx]_ st' / 4)) h')%mips_expr ->
(heap.get (S (Zabs_nat (u2Z [rx]_ st / 4))) h = heap.get (S (Zabs_nat (u2Z [rx]_ st' / 4))) h')%mips_expr ->
var_mint x (signed nk rx) s st (heap_mint (signed nk rx) st h) ->
heap.dom h = heap.dom h' ->
heap.dom (heap_mint (signed nk rx) st h) = heap.dom (heap_mint (signed nk rx) st' h').
Proof.
move=> h h' nk rx st st' x s Hrx Hslen Hptr Hvar_mint h_h'.
case: Hvar_mint => header_fit [slen [ptr [A [A_nk [Hnk [Hsgn [Hx [payload_fit [Sum_A H]]]]]]]]].
case: H => h1 [h2 [Hdisj [Hunion [Hh1 Hh2]]]].
rewrite /=.
have H'slen : heap.get (Zabs_nat (u2Z ([rx ]_ st)%mips_expr / 4)) h = Some slen.
have H'slen : heap.get (Zabs_nat (u2Z ([rx ]_ st)%mips_expr / 4)) h1 = Some slen.
rewrite -(plus_0_r (Zabs_nat (u2Z ([rx ]_ st)%mips_expr / 4))).
rewrite -/(eval (var_e rx) st)%mips_expr.
apply (assert_m.mapstos_get_inv 2 (slen :: ptr :: nil)) => //; by auto.
apply heap_get_heap_mint_inv with st (signed nk rx).
rewrite Hunion; by apply heap.get_union_L.
have H'ptr: heap.get (S (Zabs_nat (u2Z ([rx ]_ st)%mips_expr / 4))) h = Some ptr.
have H'ptr : heap.get (Zabs_nat (u2Z ([rx ]_ st)%mips_expr / 4) + 1)%nat h1 = Some ptr.
rewrite -/(eval (var_e rx) st)%mips_expr.
apply (assert_m.mapstos_get_inv 2 (slen :: ptr :: nil)) => //; by auto.
apply heap_get_heap_mint_inv with st (signed nk rx).
rewrite plus_comm in H'ptr.
rewrite Hunion; by apply heap.get_union_L.
move: Hunion => /=.
rewrite -Hslen H'slen u2Z_add_Z2u //; last by rewrite -Zbeta1_Zpower2; omega.
rewrite -{1}(Zmult_1_l 4) Z_div_plus_full // Zabs_nat_plus_pos //; last first.
apply Z_div_pos => //; apply min_u2Z.
rewrite plus_comm (_ : Zabs_nat 1 = 1%nat) //= H'ptr.
move=> Hunion.
rewrite u2Z_add_Z2u //; last by rewrite -Zbeta1_Zpower2 -Hrx; omega.
rewrite -{3}(Zmult_1_l 4) Z_div_plus_full // Zabs_nat_plus_pos //; last first.
apply Z_div_pos => //; apply min_u2Z.
rewrite plus_comm (_ : Zabs_nat 1 = 1%nat) //= -Hptr H'ptr /heap_cut.
rewrite -2!heap.proj_app -Hrx; by apply heap.dom_dom_proj.
Qed.
Lemma heap_mint_unsign_unchanged2 : forall d h h' rk rx st st' x s,
([rk ]_ st = [rk ]_ st')%mips_expr ->
([rx ]_ st = [rx ]_ st')%mips_expr ->
var_mint x (unsign rk rx) s st (heap_mint (unsign rk rx) st h) ->
h[\m] heap.dom d = h'[\m] heap.dom d ->
heap_mint (unsign rk rx) st h # d ->
heap_mint (unsign rk rx) st h = heap_mint (unsign rk rx) st' h'.
Proof.
move=> d h h' rk rx st st' x s Hrk Hrx_invariant Hnew H_h_h' Hdisj.
have dom_h_t :
seq_ext.l2s (List.seq (Zabs_nat (u2Z ([rx ]_ st) / 4)) (Zabs_nat (u2Z ([rk ]_ st))))%mips_expr =
heap.dom (heap_cut h (Zabs_nat (u2Z ([rx ]_ st) / 4)) (Zabs_nat (u2Z ([rk ]_ st))))%mips_expr.
symmetry.
by eapply var_mint_unsign_dom_heap_mint; eauto.
rewrite /= /heap_cut.
rewrite {1}(heap.proj_restrict (h [\m] heap.dom d)); last 2 first.
by apply heap.inclu_difs.
rewrite dom_h_t.
apply heap.inclu_inc_dom, heap.disj_proj_inclu.
rewrite /heap_mint in Hdisj.
by rewrite dom_h_t heap.proj_dom_proj.
symmetry.
have -> : seq_ext.l2s
(seq (Zabs_nat (u2Z ([rx ]_ st')%mips_expr / 4)) (Zabs_nat (u2Z ([rk ]_ st')%mips_expr))) =
seq_ext.l2s
(seq (Zabs_nat (u2Z ([rx ]_ st)%mips_expr / 4)) (Zabs_nat (u2Z ([rk ]_ st)%mips_expr))).
by rewrite Hrk Hrx_invariant.
rewrite {1}(heap.proj_restrict (h' [\m] heap.dom d)); last 2 first.
by apply heap.inclu_difs.
rewrite dom_h_t -H_h_h'.
apply heap.inclu_inc_dom, heap.disj_proj_inclu.
rewrite /heap_mint in Hdisj.
by rewrite dom_h_t heap.proj_dom_proj.
by rewrite H_h_h'.
Qed.
Require Import seq.
Lemma heap_mint_signed_unchanged2 : forall d h h' nk rx st st' x s,
([rx ]_ st = [rx ]_ st')%mips_expr ->
var_mint x (signed nk rx) s st (heap_mint (signed nk rx) st h) ->
h[\m] heap.dom d = h'[\m] heap.dom d ->
heap_mint (signed nk rx) st h # d ->
heap_mint (signed nk rx) st h = heap_mint (signed nk rx) st' h'.
Proof.
move=> d h h' nk rx st st' x s rx_unchanged Hnew H_h_h' Hdisj /=.
rewrite -rx_unchanged.
case : Hnew => rx_fit [slen [ptr [A [A_nk [Hnk [sign [bound [fit [Sum_A mem]]]]]]]]].
have H0 : heap.get (Zabs_nat (u2Z ([rx ]_ st)%mips_expr / 4)) h = Some slen.
move: mem; rewrite assert_m.con_assoc_equiv.
move/con_heap_mint_signed_con_TT; by move/assert_m.mapsto_con_get.
rewrite H0.
have H1 : heap.get (Zabs_nat (u2Z (([rx ]_ st)%mips_expr[.+]four32) / 4)) h = Some ptr.
move/con_heap_mint_signed_con_TT : mem => mem.
rewrite /= in mem.
rewrite assert_m.con_assoc_equiv assert_m.con_com_equiv assert_m.con_assoc_equiv assert_m.con_assoc_equiv in mem.
by move/assert_m.mapsto_con_get : mem.
rewrite H1.
have H2 : heap.get (Zabs_nat (u2Z ([rx ]_ st)%mips_expr / 4)) h' =
heap.get (Zabs_nat (u2Z ([rx ]_ st)%mips_expr / 4)) h.
set adr := Zabs_nat _.
have Htmp : adr \notin heap.dom d.
rewrite /= H0 H1 heap.disjE in Hdisj.
apply: seq_ext.dis_not_in; last by apply Hdisj.
apply heap.in_dom_union_L, heap.in_dom_proj.
- apply/seq_ext.inP; rewrite seq_ext.s2l2s; apply In_seq; rewrite /adr; omega.
- eapply heap.get_Some_in_dom; by apply H0.
transitivity (heap.get adr (h' [\m] heap.dom d)); by [rewrite heap.get_difs | rewrite -H_h_h' heap.get_difs].
rewrite H2 H0.
have H3 : heap.get (Zabs_nat (u2Z (([rx ]_ st)%mips_expr[.+]four32) / 4)) h' =
heap.get (Zabs_nat (u2Z (([rx ]_ st)%mips_expr[.+]four32) / 4)) h.
set adr := Zabs_nat _.
have Htmp : adr \notin heap.dom d.
rewrite /= H0 H1 heap.disjE in Hdisj.
apply: seq_ext.dis_not_in; last by apply Hdisj.
apply heap.in_dom_union_L, heap.in_dom_proj; last first.
eapply heap.get_Some_in_dom; by apply H1.
apply/seq_ext.inP.
rewrite seq_ext.s2l2s.
apply In_seq.
rewrite /adr u2Z_add_Z2u //; last by rewrite -Zbeta1_Zpower2; omega.
rewrite {2}(_ : 4 = 1 * 4) // Z_div_plus_full // Zabs_nat_plus_pos //; last first.
apply Z_div_pos => //; by apply min_u2Z.
split; first by omega.
rewrite [Zabs_nat 1](_ : Zabs_nat _ = 1%nat) //; omega.
transitivity (heap.get adr (h' [\m] heap.dom d)).
- by rewrite heap.get_difs.
- by rewrite -H_h_h' heap.get_difs.
rewrite H3 H1 /heap_cut.
set seq_rx_2 := {1 2}(seq_ext.l2s _). set seq_ptr_slen := (seq_ext.l2s _).
f_equal.
- have Htmp : seq_rx_2 = heap.dom (heap_cut h (Zabs_nat (u2Z ([rx ]_ st) / 4)) 2)%mips_expr.
rewrite /heap_cut heap.dom_proj_exact; [done | by apply ordset.ordered_seq | ].
move: mem; move/con_heap_mint_signed_con_TT.
by apply assert_m.mapstos_inc_inv.
rewrite {1}Htmp (heap.proj_restrict (h [\m] heap.dom d)); last 2 first.
by apply heap.inclu_difs.
apply heap.inclu_inc_dom, heap.disj_proj_inclu.
rewrite /heap_mint H0 H1 /heap_cut in Hdisj.
move/heap.disj_sym : Hdisj; case/heap.disj_union_inv; by move/heap.disj_sym.
rewrite Htmp (heap.proj_restrict (h' [\m] heap.dom d) h'); last 2 first.
by apply heap.inclu_difs.
rewrite -H_h_h'.
apply heap.inclu_inc_dom, heap.disj_proj_inclu.
rewrite /heap_mint H0 H1 /heap_cut in Hdisj.
move/heap.disj_sym : Hdisj; case/heap.disj_union_inv; by move/heap.disj_sym.
by rewrite H_h_h'.
- have Htmp : seq_ptr_slen = heap.dom (heap_cut h (Zabs_nat (u2Z ptr / 4)) nk).
rewrite /heap_cut heap.dom_proj_exact; [done | by apply ordset.ordered_seq | ].
move: mem.
do 2 rewrite assert_m.con_assoc_equiv assert_m.con_com_equiv; rewrite assert_m.con_assoc_equiv.
move/con_heap_mint_signed_con_TT.
move/assert_m.mapstos_inc_inv.
rewrite A_nk.
by apply.
rewrite {1}Htmp (heap.proj_restrict (h [\m] heap.dom d)); last 2 first.
by apply heap.inclu_difs.
apply heap.inclu_inc_dom, heap.disj_proj_inclu.
rewrite /heap_mint H0 H1 /heap_cut in Hdisj.
move/heap.disj_sym : Hdisj; case/heap.disj_union_inv=> _; by move/heap.disj_sym.
rewrite Htmp (heap.proj_restrict (h' [\m] heap.dom d) h'); last 2 first.
by apply heap.inclu_difs.
rewrite -H_h_h'.
apply heap.inclu_inc_dom, heap.disj_proj_inclu.
rewrite /heap_mint H0 H1 /heap_cut in Hdisj.
move/heap.disj_sym : Hdisj; case/heap.disj_union_inv=> _; by move/heap.disj_sym.
by rewrite -H_h_h'.
Qed.
Lemma heap_mint_unchanged2 : forall d h h' tx st st' x s,
(forall x, In x (mint_regs tx) -> ([x ]_ st = [x ]_ st')%mips_expr) ->
var_mint x tx s st (heap_mint tx st h) ->
h[\m] heap.dom d = h'[\m] heap.dom d ->
heap_mint tx st h # d ->
heap_mint tx st h = heap_mint tx st' h'.
Proof.
move=> d h h' [rk rx|nk rx] st st' x s Hunchanged Hvar_mint Hdifs Hdisj.
- eapply heap_mint_unsign_unchanged2.
by apply Hunchanged, mint_regs_unsigned1.
by apply Hunchanged, mint_regs_unsigned2.
by apply Hvar_mint.
by apply Hdifs.
done.
- eapply heap_mint_signed_unchanged2.
apply Hunchanged; by rewrite /=; intuition.
by apply Hvar_mint.
by apply Hdifs.
done.
Qed.
u2Z ([ rx ]_st)%mips_expr + 4 * 2 < Zbeta 1 /\
exists slen, exists ptr, exists A, length A = k /\
s2Z slen = Zsgn (s2Z slen) * Z_of_nat k /\
Zsgn (s2Z slen) = Zsgn val /\
Zabs val < Zbeta k /\
u2Z ptr + 4 * Z_of_nat k < Zbeta 1 /\
val = Zsgn (s2Z slen) * Sum k A /\
((var_e rx |--> slen :: ptr :: nil) ** (int_e ptr |--> A))%mips_expr%mips_assert st h.
Local Open Scope simu_scope.
Definition var_unsign k rx val st h : Prop :=
u2Z ([ rx ]_st)%mips_expr + 4 * Z_of_nat k < Zbeta 1 /\
0 <= val < Zbeta k /\
(var_e rx |--> Z2ints 32 k val)%mips_expr%mips_assert st h.
Definition var_mint (x : bipl.var.v) (t : mint) : relat := fun s st h =>
match t with
| unsign rk rx =>
var_unsign (Zabs_nat (u2Z ([ rk ]_st))%mips_expr) rx ([ x ]_s)%seplog_expr st h
| signed nk rx =>
var_signed nk rx ( [ x ]_s )%seplog_expr st h
end.
Lemma var_mint_invariant_unsign : forall x rk rx s s' st st' h,
([ rx ]_ st = [ rx ]_ st')%mips_expr -> ([ rk ]_ st = [ rk ]_ st')%mips_expr ->
([ x ]_s = [ x ]_s')%seplog_expr ->
var_mint x (unsign rk rx) s st h ->
var_mint x (unsign rk rx) s' st' h.
Proof.
move=> x rk rx_ s s' st st' h Hrx Hrk Hx.
rewrite /var_mint /var_unsign Hrk Hx Hrx.
case=> Hfit [Hover Hmem].
split; first by tauto.
split; first by tauto.
move: Hmem; by apply assert_m.mapstos_ext.
Qed.
Lemma var_mint_invariant_signed : forall x nk rx s s' st st' h,
([ rx ]_ st = [ rx ]_ st')%mips_expr -> ([ x ]_s = [ x ]_s')%seplog_expr ->
var_mint x (signed nk rx) s st h ->
var_mint x (signed nk rx) s' st' h.
Proof.
move=> x nk rx s s' st st' h Hrx Hx.
rewrite /var_mint /var_signed Hx.
case=> rx_fit [slen [ptr [A [A_nk [nk_slen [fit [sign [bound [Sum_A mem]]]]]]]]].
split; first by rewrite -Hrx.
exists slen, ptr, A.
repeat (split; first by done).
move: mem; apply assert_m.monotony => h'; by apply assert_m.mapstos_ext.
Qed.
Lemma var_mint_invariant : forall (x : bipl.var.v) t (s s' : pstore)
(st st' : store.t) (h : heap.t),
(forall rx, In rx (mint_regs t) -> [rx ]_ st = [rx ]_ st')%mips_expr ->
([x ]_ s = [x ]_ s')%seplog_expr ->
var_mint x t s st h -> var_mint x t s' st' h.
Proof.
move=> x [rk rx | nk rx] s s' st st' h H1 H2.
apply var_mint_invariant_unsign.
apply H1. simpl. by intuition.
apply H1. simpl. by intuition.
done.
apply var_mint_invariant_signed.
apply H1. simpl. by intuition.
exact H2.
Qed.
Notation "k '---' l" := (heap.dif k l) (at level 69) : heap_scope.
Notation "k '+++' m" := (heap.union k m) (at level 69) : heap_scope.
Notation "k '#' m" := (heap.disj k m) (at level 79) : heap_scope.
Notation "k '[\m]' m" := (heap.difs k m) (at level 69) : heap_scope.
Local Open Scope heap_scope.
Definition heap_cut h (x : heap.l) (k : nat) := heap.proj h (seq_ext.l2s (List.seq x k)).
Definition heap_mint (t : mint) (st : store.t) h : heap.t :=
match t with
| unsign rk rx =>
(heap_cut h (Zabs_nat (u2Z [rx]_st / 4)) (Zabs_nat (u2Z [rk]_st)))%mips_expr
| signed nk rx =>
let olen := heap.get (Zabs_nat (u2Z [rx]_st / 4))%mips_expr h in
let optr := heap.get (Zabs_nat (u2Z ([rx ]_ st [.+] four32) / 4))%mips_expr h in
match olen, optr with
| Some len, Some ptr =>
heap_cut h (Zabs_nat (u2Z [rx]_st / 4))%mips_expr 2 +++
heap_cut h (Zabs_nat (u2Z ptr / 4)) nk
| _, _ => h
end
end.
Lemma var_mint_length_heap_to_list : forall x s rk rx st h,
var_mint x (unsign rk rx) s st (heap_mint (unsign rk rx) st h)%mips_expr ->
(length (heap2list (Zabs_nat (u2Z ([rx ]_ st) / 4)) (Zabs_nat (u2Z ([rk ]_ st))) h) =
Zabs_nat (u2Z ([rk ]_ st)))%mips_expr.
Proof.
move=> x s rk rx st h H.
rewrite len_heap2list //.
case: H => Hfit [Hover Hmem].
move/assert_m.mapstos_inv_dom : Hmem.
rewrite len_Z2ints.
move/(_ Hfit) => ->.
rewrite -/(Equality.sort heap.l). apply/seq_ext.incP.
by rewrite heap.inc_dom_proj_dom.
Qed.
Lemma var_signed_exists_get_ptr : forall x nk rx s st h,
var_mint x (signed nk rx) s st h ->
exists ptr, heap.get (Zabs_nat (u2Z ([rx]_st [.+] four32)%mips_expr / 4)) h = Some ptr.
Proof.
move=> x nk rx s st h.
case=> rx_fit.
case=> slen [ptr [A [A_nk [Hlen [Hsgn [Hx [ptr_fit [Sum_A Hmem]]]]]]]].
exists ptr.
rewrite /= in Hmem.
rewrite !assert_m.con_assoc_equiv assert_m.con_com_equiv !assert_m.con_assoc_equiv in Hmem.
case: Hmem => h1 [h2 [h1_d_h2 [h1_U_h2 [Hh1 Hh2]]]].
case: Hh1 => p [Hp Hh1].
rewrite Hp h1_U_h2.
apply heap.get_union_L => //.
by rewrite Hh1 Zmult_comm Z_div_mult_full // Zabs_nat_Z_of_nat // heap.get_sing.
Qed.
Lemma var_signed_exists_get_slen : forall x nk rx s st h,
var_mint x (signed nk rx) s st h ->
exists slen, heap.get (Zabs_nat (u2Z ([rx]_st)%mips_expr / 4)) h = Some slen.
Proof.
move=> x nk rx s st h.
case=> rx_fit.
case=> slen [ptr [A [A_nk [Hlen [Hsgn [Hx [ptr_fit [Sum_A Hmem]]]]]]]].
exists slen.
rewrite /= in Hmem.
rewrite !assert_m.con_assoc_equiv in Hmem.
case: Hmem => h1 [h2 [h1_d_h2 [h1_U_h2 [Hh1 Hh2]]]].
case: Hh1 => p [Hp Hh1].
rewrite Hp h1_U_h2.
apply heap.get_union_L => //.
by rewrite Hh1 Zmult_comm Z_div_mult_full // Zabs_nat_Z_of_nat // heap.get_sing.
Qed.
Module heap_prop_m := finmap.Map_Prop heap.
Lemma con_heap_mint_signed_con_TT : forall st h nk rx Q P,
(Q ** P)%mips_assert st (heap_mint (signed nk rx) st h) ->
(Q ** assert_m.TT)%mips_assert st h.
Proof.
move=> st h nk rx Q P [h1 [h2 [h1dh2 [h1Uh2 [Hh1 Hh2]]]]].
exists h1, (h [\m] (heap.dom h1)).
split; first by apply heap.disj_difs', seq_ext.inc_refl.
split; last by done.
rewrite /= in h1Uh2; move: h1Uh2.
move Heq : (heap.get (Zabs_nat (u2Z ([rx ]_ st)%mips_expr / 4)) h) => [slen'|]; last first.
move=> ->; by rewrite heap_prop_m.union_difs_L_old.
move Heq2 : (heap.get (Zabs_nat (u2Z (([rx ]_ st)%mips_expr[.+]four32) / 4)) h) => [ptr'|]; last first.
move=> ->; by rewrite heap_prop_m.union_difs_L_old.
move=> H0.
apply heap.union_difs; last by reflexivity.
have : heap.inclu h1 (h1 +++ h2) by apply heap_prop_m.inclu_union_L_old.
rewrite -H0 -heap.proj_app.
by move/heap.proj_inclu.
Qed.
Lemma heap_mint_signed_proj : forall st h nk rA ptrA lenA,
(var_e rA |--> lenA :: ptrA :: nil ** assert_m.TT)%mips_expr%mips_assert st (heap_mint (signed nk rA) st h) ->
heap_mint (signed nk rA) st h = heap.proj h (seq.cat
(seq_ext.l2s (seq (Zabs_nat (u2Z ([rA ]_ st)%mips_expr / 4)) 2))
(seq_ext.l2s
(seq (Zabs_nat (u2Z ([ int_e ptrA ]e_ st)%mips_expr / 4)) nk))).
Proof.
move=> st h nk rA ptrA lenA mem.
simpl assert_m.mapstos in mem.
move/con_heap_mint_signed_con_TT : (mem).
rewrite mips_bipl.assert_m.con_assoc_equiv.
move/mips_bipl.assert_m.mapsto_con_get.
simpl heap_mint.
move=> ->.
move/con_heap_mint_signed_con_TT : mem.
rewrite mips_bipl.assert_m.con_assoc_equiv.
rewrite mips_bipl.assert_m.con_com_equiv.
rewrite 2!mips_bipl.assert_m.con_assoc_equiv.
move/mips_bipl.assert_m.mapsto_con_get.
move=> ->.
by rewrite /heap_cut -heap.proj_app.
Qed.
Lemma heap_mint_signed_unchanged : forall st' st h n s, ([ s ]_ st = [ s ]_ st')%mips_expr ->
heap_mint (signed n s) st h = heap_mint (signed n s) st' h.
Proof. move=> st' st h n s H; by rewrite /heap_mint -H. Qed.
Lemma heap_mint_unsign_unchanged : forall st' st h rk rx,
([ rk ]_ st = [ rk ]_ st')%mips_expr -> ([ rx ]_ st = [ rx ]_ st')%mips_expr ->
heap_mint (unsign rk rx) st h = heap_mint (unsign rk rx) st' h.
Proof. move=> st' st h rk rx Hrk Hrx; by rewrite /heap_mint -Hrk -Hrx. Qed.
Lemma heap_mint_unchanged : forall st' st h t,
(forall x, In x (mint_regs t) -> ([x ]_ st = [x ]_ st')%mips_expr) ->
heap_mint t st h = heap_mint t st' h.
Proof.
move=> st' st h t Ht.
destruct t as [rk rx|rx].
apply heap_mint_unsign_unchanged; apply Ht; simpl; intuition.
apply heap_mint_signed_unchanged; apply Ht; simpl; intuition.
Qed.
Lemma var_mint_unsign_dom_heap_mint : forall x s rk rx st h,
var_mint x (unsign rk rx) s st (heap_mint (unsign rk rx) st h) ->
heap.dom (heap_mint (unsign rk rx) st h) =
seq_ext.l2s (List.seq (Zabs_nat (u2Z ([rx ]_ st) / 4)) (Zabs_nat (u2Z ([rk ]_ st))))%mips_expr.
Proof.
move=> x s rk rx st h.
case => Hfit [Hover Hheap].
apply assert_m.mapstos_inv_dom in Hheap => //; last by rewrite len_Z2ints.
rewrite len_Z2ints in Hheap.
by rewrite Hheap /heap_cut /heap_mint seq_ext.l2s2l.
Qed.
Lemma heap_inclu_heap_mint_signed : forall h st nk rx, heap.inclu (heap_mint (signed nk rx) st h) h.
Proof.
move=> h st nk rx /=.
set a := heap.get _ _.
destruct a as [a|]; last by apply heap.inclu_refl.
set b := heap.get _ _.
destruct b as [b|]; last by apply heap.inclu_refl.
rewrite /heap_cut.
by apply heap_prop_m.inclu_union; apply heap.inclu_proj.
Qed.
Lemma dom_heap_mint_unsign_unchanged2 : forall h h' rk rx st st' x s,
([rk ]_ st = [rk ]_ st')%mips_expr ->
([rx ]_ st = [rx ]_ st')%mips_expr ->
var_mint x (unsign rk rx) s st (heap_mint (unsign rk rx) st h) ->
heap.dom h = heap.dom h' ->
heap.dom (heap_mint (unsign rk rx) st h) = heap.dom (heap_mint (unsign rk rx) st' h').
Proof.
move=> h h' rk rx st st' x s Hrk Hrx_invariant Hnew H_h_h' /=.
rewrite -Hrx_invariant -Hrk /heap_cut.
have Htmp' : seq_ext.l2s (List.seq (Zabs_nat (u2Z ([rx ]_ st) / 4)) (Zabs_nat (u2Z ([rk ]_ st))))%mips_expr =
heap.dom (heap_cut h (Zabs_nat (u2Z ([rx ]_ st) / 4)) (Zabs_nat (u2Z ([rk ]_ st))))%mips_expr.
case : Hnew => Hfit [Hover Hmem].
apply assert_m.mapstos_inv_dom in Hmem => //; last by rewrite len_Z2ints.
rewrite len_Z2ints in Hmem.
by rewrite Hmem /heap_cut /heap_mint seq_ext.l2s2l.
have Htmp'' : seq_ext.l2s (List.seq (Zabs_nat (u2Z ([rx ]_ st') / 4)) (Zabs_nat (u2Z ([rk ]_ st'))))%mips_expr =
heap.dom (heap_cut h (Zabs_nat (u2Z ([rx ]_ st') / 4)) (Zabs_nat (u2Z ([rk ]_ st'))))%mips_expr.
case : Hnew => Hfit [Hover Hmem].
apply assert_m.mapstos_inv_dom in Hmem => //; last by rewrite len_Z2ints.
rewrite len_Z2ints in Hmem.
by rewrite -Hrx_invariant -Hrk Hmem /heap_cut /heap_mint seq_ext.l2s2l.
by rewrite -Htmp' -(heap.dom_dom_proj h).
Qed.
Lemma heap_get_heap_mint_inv : forall x s h t y,
heap.get x (heap_mint t s h) = Some y -> heap.get x h = Some y.
Proof.
move=> x s h [ rk rx | nk rx] y /= H.
- rewrite /heap_cut in H.
move/heap_prop_m.get_proj_Some_inv : (H) => H'.
by rewrite heap.get_proj in H.
- move: H.
move H1 : (heap.get (Zabs_nat (u2Z ([rx ]_ s)%mips_expr / 4)) _) => [a|] //.
move H2 : (heap.get (Zabs_nat (u2Z (([rx ]_ s)%mips_expr[.+]four32) / 4)) _) => [b|] //.
case/heap.get_union_Some_inv => H.
+ move/heap_prop_m.get_proj_Some_inv : (H) => H'.
by rewrite heap.get_proj in H.
+ move/heap_prop_m.get_proj_Some_inv : (H) => H'.
by rewrite heap.get_proj in H.
Qed.
Lemma dom_heap_mint_sign_unchanged2 : forall h h' nk rx st st' x s slen slen',
([rx ]_ st = [rx ]_ st')%mips_expr ->
(heap.get (Zabs_nat (u2Z [rx]_ st / 4)) h = Some slen)%mips_expr ->
(heap.get (Zabs_nat (u2Z [rx]_ st' / 4)) h' = Some slen')%mips_expr ->
(heap.get ((Zabs_nat (u2Z ([rx]_ st [.+] four32) / 4))) h =
heap.get ((Zabs_nat (u2Z ([rx]_ st' [.+] four32) / 4))) h')%mips_expr ->
var_mint x (signed nk rx) s st (heap_mint (signed nk rx) st h) ->
heap.dom h = heap.dom h' ->
heap.dom (heap_mint (signed nk rx) st h) = heap.dom (heap_mint (signed nk rx) st' h').
Proof.
move=> h h' nk rx st st' x s slen slen' Hrx Hslen Hslen' Hptr Hvar_mint h_h'.
case: Hvar_mint => header_fit [slen_ [ptr [A [A_nk [Hnk [Hsgn [Hx [payload_fit [Sum_A H]]]]]]]]].
case: H => h1 [h2 [Hdisj [Hunion [Hh1 Hh2]]]].
rewrite /=.
have ? : slen = slen_.
have X : heap.get (Zabs_nat (u2Z ([rx ]_ st)%mips_expr / 4)) (heap_mint (signed nk rx) st h) = Some slen_.
rewrite Hunion.
apply heap.get_union_L => //.
rewrite /= in Hh1.
case: Hh1 => h11 [h12 [h11_d_h12 [h11_U_h12 [Hh11 Hh12]]]].
case: Hh11 => p [Hp Hh11].
rewrite h11_U_h12.
apply heap.get_union_L => //.
by rewrite Hh11 Hp Zmult_comm Z_div_mult_full // Zabs_nat_Z_of_nat heap.get_sing.
move/heap_get_heap_mint_inv : X.
rewrite Hslen.
by case.
subst slen_.
have H'slen : heap.get (Zabs_nat (u2Z ([rx ]_ st)%mips_expr / 4)) h = Some slen.
have H'slen : heap.get (Zabs_nat (u2Z ([rx ]_ st)%mips_expr / 4)) h1 = Some slen.
rewrite -(plus_0_r (Zabs_nat (u2Z ([rx ]_ st)%mips_expr / 4))).
rewrite -/(eval (var_e rx) st)%mips_expr.
apply (assert_m.mapstos_get_inv 2 (slen :: ptr :: List.nil)%list) => //; by auto.
apply heap_get_heap_mint_inv with st (signed nk rx).
rewrite Hunion; by apply heap.get_union_L.
have H'ptr: heap.get ((Zabs_nat (u2Z ([rx ]_ st [.+] four32 )%mips_expr / 4))) h = Some ptr.
have H'ptr : heap.get (Zabs_nat (u2Z ([rx ]_ st)%mips_expr / 4) + 1)%nat h1 = Some ptr.
rewrite -/(eval (var_e rx) st)%mips_expr.
apply (assert_m.mapstos_get_inv 2 (slen :: ptr :: List.nil)%list) => //; by auto.
apply heap_get_heap_mint_inv with st (signed nk rx).
rewrite u2Z_add_Z2u //.
rewrite -{1}(Zmult_1_l 4) Z_div_plus_full // Zabs_nat_plus_pos //; last first.
by apply Z_div_pos => //; apply min_u2Z.
rewrite (_ : Zabs_nat 1 = 1%nat) //.
rewrite Hunion; by apply heap.get_union_L.
rewrite -/(Zbeta 1); omega.
move: Hunion => /=.
rewrite H'slen Hslen' H'ptr.
move=> Hunion.
rewrite -Hptr H'ptr /heap_cut -heap.proj_app -heap.proj_app -Hrx.
by apply heap.dom_dom_proj.
Qed.
Lemma dom_heap_mint_signed_unchanged : forall h h' nk rx st st' x s,
([rx ]_ st = [rx ]_ st')%mips_expr ->
(heap.get (Zabs_nat (u2Z [rx]_ st / 4)) h = heap.get (Zabs_nat (u2Z [rx]_ st' / 4)) h')%mips_expr ->
(heap.get (S (Zabs_nat (u2Z [rx]_ st / 4))) h = heap.get (S (Zabs_nat (u2Z [rx]_ st' / 4))) h')%mips_expr ->
var_mint x (signed nk rx) s st (heap_mint (signed nk rx) st h) ->
heap.dom h = heap.dom h' ->
heap.dom (heap_mint (signed nk rx) st h) = heap.dom (heap_mint (signed nk rx) st' h').
Proof.
move=> h h' nk rx st st' x s Hrx Hslen Hptr Hvar_mint h_h'.
case: Hvar_mint => header_fit [slen [ptr [A [A_nk [Hnk [Hsgn [Hx [payload_fit [Sum_A H]]]]]]]]].
case: H => h1 [h2 [Hdisj [Hunion [Hh1 Hh2]]]].
rewrite /=.
have H'slen : heap.get (Zabs_nat (u2Z ([rx ]_ st)%mips_expr / 4)) h = Some slen.
have H'slen : heap.get (Zabs_nat (u2Z ([rx ]_ st)%mips_expr / 4)) h1 = Some slen.
rewrite -(plus_0_r (Zabs_nat (u2Z ([rx ]_ st)%mips_expr / 4))).
rewrite -/(eval (var_e rx) st)%mips_expr.
apply (assert_m.mapstos_get_inv 2 (slen :: ptr :: nil)) => //; by auto.
apply heap_get_heap_mint_inv with st (signed nk rx).
rewrite Hunion; by apply heap.get_union_L.
have H'ptr: heap.get (S (Zabs_nat (u2Z ([rx ]_ st)%mips_expr / 4))) h = Some ptr.
have H'ptr : heap.get (Zabs_nat (u2Z ([rx ]_ st)%mips_expr / 4) + 1)%nat h1 = Some ptr.
rewrite -/(eval (var_e rx) st)%mips_expr.
apply (assert_m.mapstos_get_inv 2 (slen :: ptr :: nil)) => //; by auto.
apply heap_get_heap_mint_inv with st (signed nk rx).
rewrite plus_comm in H'ptr.
rewrite Hunion; by apply heap.get_union_L.
move: Hunion => /=.
rewrite -Hslen H'slen u2Z_add_Z2u //; last by rewrite -Zbeta1_Zpower2; omega.
rewrite -{1}(Zmult_1_l 4) Z_div_plus_full // Zabs_nat_plus_pos //; last first.
apply Z_div_pos => //; apply min_u2Z.
rewrite plus_comm (_ : Zabs_nat 1 = 1%nat) //= H'ptr.
move=> Hunion.
rewrite u2Z_add_Z2u //; last by rewrite -Zbeta1_Zpower2 -Hrx; omega.
rewrite -{3}(Zmult_1_l 4) Z_div_plus_full // Zabs_nat_plus_pos //; last first.
apply Z_div_pos => //; apply min_u2Z.
rewrite plus_comm (_ : Zabs_nat 1 = 1%nat) //= -Hptr H'ptr /heap_cut.
rewrite -2!heap.proj_app -Hrx; by apply heap.dom_dom_proj.
Qed.
Lemma heap_mint_unsign_unchanged2 : forall d h h' rk rx st st' x s,
([rk ]_ st = [rk ]_ st')%mips_expr ->
([rx ]_ st = [rx ]_ st')%mips_expr ->
var_mint x (unsign rk rx) s st (heap_mint (unsign rk rx) st h) ->
h[\m] heap.dom d = h'[\m] heap.dom d ->
heap_mint (unsign rk rx) st h # d ->
heap_mint (unsign rk rx) st h = heap_mint (unsign rk rx) st' h'.
Proof.
move=> d h h' rk rx st st' x s Hrk Hrx_invariant Hnew H_h_h' Hdisj.
have dom_h_t :
seq_ext.l2s (List.seq (Zabs_nat (u2Z ([rx ]_ st) / 4)) (Zabs_nat (u2Z ([rk ]_ st))))%mips_expr =
heap.dom (heap_cut h (Zabs_nat (u2Z ([rx ]_ st) / 4)) (Zabs_nat (u2Z ([rk ]_ st))))%mips_expr.
symmetry.
by eapply var_mint_unsign_dom_heap_mint; eauto.
rewrite /= /heap_cut.
rewrite {1}(heap.proj_restrict (h [\m] heap.dom d)); last 2 first.
by apply heap.inclu_difs.
rewrite dom_h_t.
apply heap.inclu_inc_dom, heap.disj_proj_inclu.
rewrite /heap_mint in Hdisj.
by rewrite dom_h_t heap.proj_dom_proj.
symmetry.
have -> : seq_ext.l2s
(seq (Zabs_nat (u2Z ([rx ]_ st')%mips_expr / 4)) (Zabs_nat (u2Z ([rk ]_ st')%mips_expr))) =
seq_ext.l2s
(seq (Zabs_nat (u2Z ([rx ]_ st)%mips_expr / 4)) (Zabs_nat (u2Z ([rk ]_ st)%mips_expr))).
by rewrite Hrk Hrx_invariant.
rewrite {1}(heap.proj_restrict (h' [\m] heap.dom d)); last 2 first.
by apply heap.inclu_difs.
rewrite dom_h_t -H_h_h'.
apply heap.inclu_inc_dom, heap.disj_proj_inclu.
rewrite /heap_mint in Hdisj.
by rewrite dom_h_t heap.proj_dom_proj.
by rewrite H_h_h'.
Qed.
Require Import seq.
Lemma heap_mint_signed_unchanged2 : forall d h h' nk rx st st' x s,
([rx ]_ st = [rx ]_ st')%mips_expr ->
var_mint x (signed nk rx) s st (heap_mint (signed nk rx) st h) ->
h[\m] heap.dom d = h'[\m] heap.dom d ->
heap_mint (signed nk rx) st h # d ->
heap_mint (signed nk rx) st h = heap_mint (signed nk rx) st' h'.
Proof.
move=> d h h' nk rx st st' x s rx_unchanged Hnew H_h_h' Hdisj /=.
rewrite -rx_unchanged.
case : Hnew => rx_fit [slen [ptr [A [A_nk [Hnk [sign [bound [fit [Sum_A mem]]]]]]]]].
have H0 : heap.get (Zabs_nat (u2Z ([rx ]_ st)%mips_expr / 4)) h = Some slen.
move: mem; rewrite assert_m.con_assoc_equiv.
move/con_heap_mint_signed_con_TT; by move/assert_m.mapsto_con_get.
rewrite H0.
have H1 : heap.get (Zabs_nat (u2Z (([rx ]_ st)%mips_expr[.+]four32) / 4)) h = Some ptr.
move/con_heap_mint_signed_con_TT : mem => mem.
rewrite /= in mem.
rewrite assert_m.con_assoc_equiv assert_m.con_com_equiv assert_m.con_assoc_equiv assert_m.con_assoc_equiv in mem.
by move/assert_m.mapsto_con_get : mem.
rewrite H1.
have H2 : heap.get (Zabs_nat (u2Z ([rx ]_ st)%mips_expr / 4)) h' =
heap.get (Zabs_nat (u2Z ([rx ]_ st)%mips_expr / 4)) h.
set adr := Zabs_nat _.
have Htmp : adr \notin heap.dom d.
rewrite /= H0 H1 heap.disjE in Hdisj.
apply: seq_ext.dis_not_in; last by apply Hdisj.
apply heap.in_dom_union_L, heap.in_dom_proj.
- apply/seq_ext.inP; rewrite seq_ext.s2l2s; apply In_seq; rewrite /adr; omega.
- eapply heap.get_Some_in_dom; by apply H0.
transitivity (heap.get adr (h' [\m] heap.dom d)); by [rewrite heap.get_difs | rewrite -H_h_h' heap.get_difs].
rewrite H2 H0.
have H3 : heap.get (Zabs_nat (u2Z (([rx ]_ st)%mips_expr[.+]four32) / 4)) h' =
heap.get (Zabs_nat (u2Z (([rx ]_ st)%mips_expr[.+]four32) / 4)) h.
set adr := Zabs_nat _.
have Htmp : adr \notin heap.dom d.
rewrite /= H0 H1 heap.disjE in Hdisj.
apply: seq_ext.dis_not_in; last by apply Hdisj.
apply heap.in_dom_union_L, heap.in_dom_proj; last first.
eapply heap.get_Some_in_dom; by apply H1.
apply/seq_ext.inP.
rewrite seq_ext.s2l2s.
apply In_seq.
rewrite /adr u2Z_add_Z2u //; last by rewrite -Zbeta1_Zpower2; omega.
rewrite {2}(_ : 4 = 1 * 4) // Z_div_plus_full // Zabs_nat_plus_pos //; last first.
apply Z_div_pos => //; by apply min_u2Z.
split; first by omega.
rewrite [Zabs_nat 1](_ : Zabs_nat _ = 1%nat) //; omega.
transitivity (heap.get adr (h' [\m] heap.dom d)).
- by rewrite heap.get_difs.
- by rewrite -H_h_h' heap.get_difs.
rewrite H3 H1 /heap_cut.
set seq_rx_2 := {1 2}(seq_ext.l2s _). set seq_ptr_slen := (seq_ext.l2s _).
f_equal.
- have Htmp : seq_rx_2 = heap.dom (heap_cut h (Zabs_nat (u2Z ([rx ]_ st) / 4)) 2)%mips_expr.
rewrite /heap_cut heap.dom_proj_exact; [done | by apply ordset.ordered_seq | ].
move: mem; move/con_heap_mint_signed_con_TT.
by apply assert_m.mapstos_inc_inv.
rewrite {1}Htmp (heap.proj_restrict (h [\m] heap.dom d)); last 2 first.
by apply heap.inclu_difs.
apply heap.inclu_inc_dom, heap.disj_proj_inclu.
rewrite /heap_mint H0 H1 /heap_cut in Hdisj.
move/heap.disj_sym : Hdisj; case/heap.disj_union_inv; by move/heap.disj_sym.
rewrite Htmp (heap.proj_restrict (h' [\m] heap.dom d) h'); last 2 first.
by apply heap.inclu_difs.
rewrite -H_h_h'.
apply heap.inclu_inc_dom, heap.disj_proj_inclu.
rewrite /heap_mint H0 H1 /heap_cut in Hdisj.
move/heap.disj_sym : Hdisj; case/heap.disj_union_inv; by move/heap.disj_sym.
by rewrite H_h_h'.
- have Htmp : seq_ptr_slen = heap.dom (heap_cut h (Zabs_nat (u2Z ptr / 4)) nk).
rewrite /heap_cut heap.dom_proj_exact; [done | by apply ordset.ordered_seq | ].
move: mem.
do 2 rewrite assert_m.con_assoc_equiv assert_m.con_com_equiv; rewrite assert_m.con_assoc_equiv.
move/con_heap_mint_signed_con_TT.
move/assert_m.mapstos_inc_inv.
rewrite A_nk.
by apply.
rewrite {1}Htmp (heap.proj_restrict (h [\m] heap.dom d)); last 2 first.
by apply heap.inclu_difs.
apply heap.inclu_inc_dom, heap.disj_proj_inclu.
rewrite /heap_mint H0 H1 /heap_cut in Hdisj.
move/heap.disj_sym : Hdisj; case/heap.disj_union_inv=> _; by move/heap.disj_sym.
rewrite Htmp (heap.proj_restrict (h' [\m] heap.dom d) h'); last 2 first.
by apply heap.inclu_difs.
rewrite -H_h_h'.
apply heap.inclu_inc_dom, heap.disj_proj_inclu.
rewrite /heap_mint H0 H1 /heap_cut in Hdisj.
move/heap.disj_sym : Hdisj; case/heap.disj_union_inv=> _; by move/heap.disj_sym.
by rewrite -H_h_h'.
Qed.
Lemma heap_mint_unchanged2 : forall d h h' tx st st' x s,
(forall x, In x (mint_regs tx) -> ([x ]_ st = [x ]_ st')%mips_expr) ->
var_mint x tx s st (heap_mint tx st h) ->
h[\m] heap.dom d = h'[\m] heap.dom d ->
heap_mint tx st h # d ->
heap_mint tx st h = heap_mint tx st' h'.
Proof.
move=> d h h' [rk rx|nk rx] st st' x s Hunchanged Hvar_mint Hdifs Hdisj.
- eapply heap_mint_unsign_unchanged2.
by apply Hunchanged, mint_regs_unsigned1.
by apply Hunchanged, mint_regs_unsigned2.
by apply Hvar_mint.
by apply Hdifs.
done.
- eapply heap_mint_signed_unchanged2.
apply Hunchanged; by rewrite /=; intuition.
by apply Hvar_mint.
by apply Hdifs.
done.
Qed.
relation between a store of seplog variables and several mips multi_ints
Require order finmap.
Module Mint <: finmap.EQTYPE.
Definition A : eqType := mint_eqType.
End Mint.
Module assoc := finmap.map order.NatOrder Mint.
Notation "k '\U+' m" := (assoc.union k m) (at level 69) : assoc_scope.
Notation "a |=> b" := (assoc.sing a b) (at level 68, no associativity) : assoc_scope.
Ltac assoc_get_Some :=
match goal with
| |- assoc.get ?x (assoc.union (assoc.sing ?x ?rx) ?d) = Some ?rk =>
apply assoc.get_union_sing_eq
| |- assoc.get ?x (assoc.union (assoc.sing ?y ?ry) ?d) = Some ?rk =>
rewrite assoc.get_union_sing_neq; [ assoc_get_Some | Nodup_neq ]
| |- assoc.get ?x (assoc.sing ?x ?rx) = Some ?rx =>
apply assoc.get_sing
| _ => fail
end.
Module assoc_prop_m := finmap.Map_Prop assoc.
Ltac assoc_collect_until' x m seed :=
match m with
| assoc.union (assoc.sing x ?vx) ?m' =>
seed
| assoc.union (assoc.sing ?y ?vy) ?m' =>
let seed' := constr: (assoc.union seed (assoc.sing y vy)) in
assoc_collect_until' x m' seed'
| assoc.sing x ?vx =>
seed
| assoc.sing ?y ?vy =>
constr : ( assoc.union seed (assoc.sing y vy))
end.
Ltac assoc_collect_until x m :=
match m with
| assoc.union (assoc.sing x ?vx) ?m' =>
constr: (assoc.emp)
| assoc.union (assoc.sing ?y ?vy) ?m' =>
let seed := constr: (assoc.sing y vy) in
assoc_collect_until' x m' seed
| assoc.sing x ?vx =>
constr : (assoc.emp)
| assoc.sing ?y ?vy =>
constr : (assoc.sing y vy)
end.
Ltac assoc_collect_after x m :=
match m with
| assoc.union (assoc.sing x ?vx) ?m' =>
m'
| assoc.union (assoc.sing ?y ?vy) ?m' =>
assoc_collect_after x m'
| assoc.union x ?vx =>
constr: (assoc.emp)
| assoc.sing ?y ?vy =>
constr : (assoc.emp)
end.
Ltac assoc_find_image x m :=
match m with
| assoc.union (assoc.sing x ?vx) ?m' => constr : ( Some vx )
| assoc.union (assoc.sing ?y ?vy) ?m' => assoc_find_image x m'
| assoc.sing x ?vx => constr : ( Some vx )
| assoc.sing ?y ?vy => None
end.
Ltac assoc_put_in_front x :=
match goal with
| |- context [assoc.union ?K ?L] =>
let m := constr : (assoc.union K L) in
let pre := assoc_collect_until x m in
let pos := assoc_collect_after x m in
let new_m := constr: (assoc.union pre pos) in
let img := assoc_find_image x m in
match img with
| Some ?vx =>
let ret := constr : ( assoc.union (assoc.sing x vx) new_m) in
rewrite (_ : assoc.union _ _ = ret);
[ (repeat rewrite <- assoc.union_assoc ;
repeat rewrite assoc.union_emp_R ;
repeat rewrite assoc.union_emp_L) | (repeat rewrite <- assoc.union_assoc ;
repeat rewrite assoc.union_emp_R ;
repeat rewrite assoc.union_emp_L ;
assoc.Equal_union) ]
| None => fail
end
end.
Definition state_mint (d : assoc.t) : relat := fun s st h =>
(forall x mx, assoc.get x d = Some mx ->
var_mint x mx s st (heap_mint mx st h)) /\
(forall x y, x <> y ->
forall mx my, assoc.get x d = Some mx -> assoc.get y d = Some my ->
heap_mint mx st h # heap_mint my st h)%mips_expr.
Local Open Scope assoc_scope.
Lemma state_mint_var_mint : forall d s st h x rx, state_mint d s st h ->
assoc.get x d = Some rx -> var_mint x rx s st (heap_mint rx st h)%mips_expr.
Proof. move=> x rx d s st h. case=> H1 _ H; by apply H1. Qed.
Lemma state_mint_align : forall rk x rx d s st h,
state_mint (x |=> unsign rk rx \U+ d) s st h ->
u2Z ([ rx ]_st)%mips_expr mod 4 = 0.
Proof.
move=> rk x rx d s st h.
move/(state_mint_var_mint _ _ _ _ x (unsign rk rx)).
rewrite assoc.get_union_sing_eq.
move/(_ (refl_equal _)).
case=> _ [_].
by move/assert_m.mapstos_inv_addr.
Qed.
Lemma state_mint_unsign_fit : forall rk x rx d s st h,
state_mint (x |=> unsign rk rx \U+ d) s st h ->
(u2Z ([rx ]_ st)%mips_expr + 4 * Z_of_nat (Zabs_nat (u2Z ([rk ]_ st))%mips_expr) < Zbeta 1)%mips_expr.
Proof.
move=> rk x rx d s st h.
rewrite /state_mint.
case=> X _.
move: {X}(X x (unsign rk rx)) => X.
lapply X; last by rewrite assoc.get_union_sing_eq.
rewrite /var_mint /var_unsign; tauto.
Qed.
Lemma state_mint_signed_fit_ptr : forall L x rx d s st h ptr,
state_mint (x |=> signed L rx \U+ d) s st h ->
heap.get (Zabs_nat (u2Z ([rx]_st [.+] four32)%mips_expr / 4)) (heap_mint (signed L rx) st h) = Some ptr ->
(u2Z ptr + 4 * Z_of_nat L < Zbeta 1)%mips_expr.
Proof.
move=> L x rx d s st h ptr s_st_h ptr_vx4.
move: (state_mint_var_mint _ _ _ _ x (signed L rx) s_st_h).
rewrite assoc.get_union_sing_eq.
case/(_ (refl_equal _)) => _ [slen_ [ptr_ [A [A_nk [HL [Hsgn [max_len [ptr_fit [Sum_A H]]]]]]]]].
move/assert_m.mapstos_get2 : H.
rewrite [u2Z _]/= ptr_vx4.
by case => ->.
Qed.
Lemma state_mint_signed_slen_L : forall L x rx d s st h slen,
state_mint (x |=> signed L rx \U+ d) s st h ->
heap.get (Zabs_nat (u2Z ([rx]_st)%mips_expr / 4)) (heap_mint (signed L rx) st h) = Some slen ->
s2Z slen = Zsgn (s2Z slen) * Z_of_nat L.
Proof.
move=> L x rx d s st h slen s_st_h ptr_vx.
move: (state_mint_var_mint _ _ _ _ x (signed L rx) s_st_h).
rewrite assoc.get_union_sing_eq.
case/(_ (refl_equal _)) => _ [slen_ [ptr_ [A [A_nk [HL [Hsgn [max_len [ptr_fit [Sum_A H]]]]]]]]].
move/assert_m.mapstos_get1 : H.
rewrite [u2Z _]/= ptr_vx.
by case => ->.
Qed.
Ltac Var_unchanged :=
match goal with
| Hid : (Some (?s1, ?h1) -- ?c ---> Some (?s2, ?h2))%seplog_cmd
|- ( [ ?x ]_ ?s1 = [ ?x ]_ ?s2 )%seplog_expr =>
apply syntax_m.var_unchanged with h1 c h2; [exact Hid | idtac]
end.
Lemma state_mint_invariant : forall d c, ~~ mips_syntax.contains_sw c ->
disj (mips_frame.modified_regs c) (mints_regs (seq_ext.s2l (assoc.cdom d))) ->
inv_R (fun s st h => state_mint d s st h) c.
Proof.
move=> d c Hnosw Hinter.
rewrite /inv_R => s st he Hs_st_he st' h' Hexec.
rewrite /state_mint; split.
- move=> x rx H_rx_x.
move: {Hs_st_he}(proj1 Hs_st_he x rx H_rx_x) => Hs_st_he.
move: Hs_st_he.
have -> : he = h' by eapply mips_syntax.no_sw_heap_invariant; eauto.
have X : forall rx0 : reg_eqType,
In rx0 (mint_regs rx) -> ([rx0 ]_ st)%mips_expr = ([rx0 ]_ st')%mips_expr.
move=> rx0 Hrx0.
Reg_unchanged.
apply (disj_not_In _ _ _ Hinter).
apply (In_mints_regs _ _ rx) => //.
apply/seq_ext.inP; by move/assoc.get_Some_in_cdom : H_rx_x.
rewrite (heap_mint_unchanged st') //.
by apply var_mint_invariant.
- move=> x y Hxy rx ry H_rx_x H_ry_y.
move: {Hs_st_he}(proj2 Hs_st_he _ _ Hxy _ _ H_rx_x H_ry_y) => Hs_st_he.
have X : forall x0 : reg_eqType,
In x0 (mint_regs rx) -> ([x0 ]_ st')%mips_expr = ([x0 ]_ st)%mips_expr.
move=> x0 Hx0.
symmetry.
Reg_unchanged.
apply (disj_not_In _ _ _ Hinter).
apply (In_mints_regs _ _ rx) => //.
apply/seq_ext.inP; by apply assoc.get_Some_in_cdom in H_rx_x.
have Y : forall x0 : reg_eqType,
In x0 (mint_regs ry) -> ([x0 ]_ st')%mips_expr = ([x0 ]_ st)%mips_expr.
move=> x0 Hx0.
symmetry.
Reg_unchanged.
apply (disj_not_In _ _ _ Hinter).
apply (In_mints_regs _ _ ry) => //.
apply/seq_ext.inP; by apply assoc.get_Some_in_cdom in H_ry_y.
rewrite (heap_mint_unchanged st) // (heap_mint_unchanged st st') //.
suff : he = h' by move=> <-.
by eapply mips_syntax.no_sw_heap_invariant; eauto.
Qed.
Ltac local_Reg_unchanged st :=
match goal with
|- context [store.get ?rk ?st'] =>
cutrewrite (store.get rk st' = store.get rk st) ;
[ assumption |
symmetry ;
mips_syntax.Reg_unchanged ;
simpl mips_frame.modified_regs ;
Nodup_not_In ; fail ]
end.
Lemma state_mint_part2_one_variable : forall x rk rx d h h' st st' s,
state_mint (x |=> unsign rk rx \U+ d) s st h ->
(forall t x0,
t \in assoc.cdom (x |=> unsign rk rx \U+ d) ->
In x0 (mint_regs t) ->
([x0 ]_ st)%mips_expr = ([x0 ]_ st')%mips_expr) ->
h [\m] heap.dom (heap_mint (unsign rk rx) st h) =
h' [\m] heap.dom (heap_mint (unsign rk rx) st h) ->
heap.dom h = heap.dom h' ->
forall x0 y : assoc.l,
x0 <> y ->
forall rx0 ry : assoc.v,
assoc.get x0 (x |=> unsign rk rx \U+ d) = Some rx0 ->
assoc.get y (x |=> unsign rk rx \U+ d) = Some ry ->
heap_mint rx0 st' h' # heap_mint ry st' h'.
Proof.
move=> x rk rx d h h' st st' s s_st_h H1 H2 H3.
- move=> y z y_z ry rz Hry Hrz.
move: (proj2 s_st_h _ _ y_z _ _ Hry Hrz).
case/orP : (orbN (z == x)); [move/eqP => z_x; subst z | move/eqP => z_x].
+ rewrite assoc.get_union_sing_eq // in Hrz. case: Hrz => ?; subst rz.
rewrite assoc.get_union_sing_neq // in Hry.
have <- : heap_mint ry st h = heap_mint ry st' h'.
apply (heap_mint_unchanged2 (heap_mint (unsign rk rx) st h) _ _ _ _ _ y s).
* move=> x0 Hx0.
apply H1 with ry => //.
apply assoc.get_Some_in_cdom with y.
by rewrite assoc.get_union_sing_neq.
* apply (proj1 s_st_h); by rewrite assoc.get_union_sing_neq.
* exact H2.
* apply (proj2 s_st_h _ _ y_z); by [rewrite assoc.get_union_sing_neq | rewrite assoc.get_union_sing_eq].
move=> H.
eapply heap.disj_same_dom; first by apply H.
symmetry. apply (dom_heap_mint_unsign_unchanged2 _ _ _ _ _ _ x s).
apply H1 with (unsign rk rx).
apply assoc.get_Some_in_cdom with x.
by rewrite assoc.get_union_sing_eq.
by apply mint_regs_unsigned1.
apply H1 with (unsign rk rx).
apply assoc.get_Some_in_cdom with x.
by rewrite assoc.get_union_sing_eq.
by apply mint_regs_unsigned2.
eapply state_mint_var_mint; by [apply s_st_h | rewrite assoc.get_union_sing_eq].
exact H3.
+ have : heap_mint rz st h = heap_mint rz st' h'.
apply (heap_mint_unchanged2 (heap_mint (unsign rk rx) st h) _ _ _ _ _ z s).
* move=> x0 Hx0.
apply H1 with rz => //.
by apply assoc.get_Some_in_cdom with z.
* by apply (proj1 s_st_h _ _ Hrz).
* exact H2.
* apply (proj2 s_st_h _ _ z_x) => //; by rewrite assoc.get_union_sing_eq.
move=> ->.
case/orP : (orbN (y == x)); [move/eqP => y_x; subst y | move/eqP => y_x].
* rewrite assoc.get_union_sing_eq in Hry; case: Hry => ?; subst ry.
rewrite assoc.get_union_sing_neq in Hrz; last by auto.
move/heap.disj_sym => H.
apply heap.disj_sym.
eapply heap.disj_same_dom; first by apply H.
symmetry.
apply (dom_heap_mint_unsign_unchanged2 _ _ _ _ _ _ x s).
apply H1 with (unsign rk rx).
apply assoc.get_Some_in_cdom with x.
by rewrite assoc.get_union_sing_eq.
by apply mint_regs_unsigned1.
apply H1 with (unsign rk rx).
apply assoc.get_Some_in_cdom with x.
by rewrite assoc.get_union_sing_eq.
by apply mint_regs_unsigned2.
eapply state_mint_var_mint; by [apply s_st_h | rewrite assoc.get_union_sing_eq].
exact H3.
* suff : heap_mint ry st h = heap_mint ry st' h' by move=> ->.
apply (heap_mint_unchanged2 (heap_mint (unsign rk rx) st h) _ _ _ _ _ y s).
- move=> x0 Hx0.
apply H1 with ry => //.
by apply assoc.get_Some_in_cdom with y.
- by apply (proj1 s_st_h _ _ Hry).
- exact H2.
- apply (proj2 s_st_h _ _ y_x) => //; by rewrite assoc.get_union_sing_eq.
Qed.
Lemma state_mint_part2_two_variables : forall A L rA y ry rk d s st h st' h',
heap.dom (heap_mint (signed L rA) st' h') = heap.dom (heap_mint (signed L rA) st h) ->
heap.dom (heap_mint (unsign rk ry) st' h') = heap.dom (heap_mint (unsign rk ry) st h) ->
state_mint (A |=> signed L rA \U+ (y |=> unsign rk ry \U+ d)) s st h ->
(forall t,
t \in assoc.cdom (A |=> signed L rA \U+ (y |=> unsign rk ry \U+ d)) ->
forall x0, In x0 (mint_regs t) -> [x0 ]_ st = [x0 ]_ st')%mips_expr ->
A \notin assoc.dom d ->
y \notin assoc.dom d ->
A <> y ->
h[\m]
heap.dom (heap_mint (unsign rk ry) st h +++ heap_mint (signed L rA) st h) =
h'[\m]
heap.dom (heap_mint (unsign rk ry) st h +++ heap_mint (signed L rA) st h) ->
forall x y0 : assoc.l,
x <> y0 ->
forall rx ry0 : assoc.v,
assoc.get x (A |=> signed L rA \U+ (y |=> unsign rk ry \U+ d)) = Some rx ->
assoc.get y0 (A |=> signed L rA \U+ (y |=> unsign rk ry \U+ d)) = Some ry0 ->
heap_mint rx st' h' # heap_mint ry0 st' h'.
Proof.
move=> A L rA y ry rk d s st h st' h' dom_rA dom_rx s_st_h H1 A_d y_d A_y H2
x y0 x_y0 rx ry0 Hrx Hry0.
case/assoc.get_union_Some_inv : Hrx => Hrx.
+ case/assoc.get_sing_inv : Hrx => ? ?; subst x rx.
rewrite heap.disjE dom_rA -heap.disjE.
case/assoc.get_union_Some_inv : Hry0 => Hry0.
* case/assoc.get_sing_inv : Hry0 => ? ?; subst y0 ry0.
by move: (x_y0 (refl_equal _)).
* case/assoc.get_union_Some_inv : Hry0 => Hry0.
- case/assoc.get_sing_inv : Hry0 => ? ?; subst y0 ry0.
rewrite heap.disjE dom_rx -heap.disjE.
apply (proj2 s_st_h A y).
by auto.
by assoc_get_Some.
rewrite assoc.get_union_sing_neq; last by auto.
by rewrite assoc.get_union_sing_eq.
- have <- : heap_mint ry0 st h = heap_mint ry0 st' h'.
apply heap_mint_unchanged2 with
(d := heap_mint (unsign rk ry) st h +++ heap_mint (signed L rA) st h) (x := y0) (s := s).
apply H1.
apply assoc.get_Some_in_cdom with y0.
rewrite assoc.get_union_sing_neq; last by auto.
apply assoc.get_union_R => //.
rewrite assoc.disjE assoc.dom_sing /=.
by rewrite (negbTE y_d).
eapply state_mint_var_mint; first by apply s_st_h.
rewrite assoc.get_union_sing_neq; last by auto.
apply assoc.get_union_R => //.
rewrite assoc.disjE assoc.dom_sing /=.
by rewrite (negbTE y_d).
exact H2.
- apply heap.disj_union_R.
+ apply (proj2 s_st_h y0 y).
* move=> abs; subst y0.
move/assoc.get_Some_in_dom : Hry0.
by apply/negPn.
* rewrite assoc.union_assoc.
apply assoc.get_union_R; last by exact Hry0.
apply assoc.disj_union_L.
by rewrite assoc.disjE assoc.dom_sing /= (negbTE A_d).
by rewrite assoc.disjE assoc.dom_sing /= (negbTE y_d).
* rewrite assoc.get_union_sing_neq; last by auto.
by rewrite assoc.get_union_sing_eq.
- apply (proj2 s_st_h y0 A).
* by auto.
* rewrite assoc.union_assoc.
apply assoc.get_union_R; last by exact Hry0.
apply assoc.disj_union_L.
by rewrite assoc.disjE assoc.dom_sing /= (negbTE A_d).
by rewrite assoc.disjE assoc.dom_sing /= (negbTE y_d).
* by assoc_get_Some.
apply (proj2 s_st_h A y0).
- done.
- by rewrite assoc.get_union_sing_eq.
- rewrite assoc.union_assoc.
apply assoc.get_union_R; last by exact Hry0.
apply assoc.disj_union_L.
by rewrite assoc.disjE assoc.dom_sing /= (negbTE A_d).
by rewrite assoc.disjE assoc.dom_sing /= (negbTE y_d).
+ case/assoc.get_union_Some_inv : Hrx => Hrx.
* case/assoc.get_sing_inv : Hrx => ? ?; subst x rx.
rewrite heap.disjE dom_rx -heap.disjE.
case/assoc.get_union_Some_inv : Hry0 => Hry0.
+ case/assoc.get_sing_inv : Hry0 => ? ?; subst y0 ry0.
rewrite heap.disjE dom_rA -heap.disjE.
apply (proj2 s_st_h y A). by auto.
rewrite assoc.get_union_sing_neq; last by auto.
by rewrite assoc.get_union_sing_eq.
by rewrite assoc.get_union_sing_eq.
+ rewrite assoc.get_union_sing_neq in Hry0; last by auto.
have y0_ry0 : assoc.get y0
(y |=> unsign rk ry \U+ (A |=> signed L rA \U+ d)) =
Some ry0.
rewrite assoc.get_union_sing_neq; last by auto.
rewrite assoc.get_union_sing_neq //.
move=> abs; subst y0.
move/assoc.get_Some_in_dom : Hry0.
by apply/negPn.
have <- : heap_mint ry0 st h = heap_mint ry0 st' h'.
apply heap_mint_unchanged2 with
(d := heap_mint (unsign rk ry) st h +++ heap_mint (signed L rA) st h) (x := y0) (s := s).
apply H1.
apply assoc.get_Some_in_cdom with y0.
rewrite assoc.union_assoc.
apply assoc.get_union_R => //.
apply assoc.disj_union_L.
by rewrite assoc.disjE assoc.dom_sing /= (negbTE A_d).
by rewrite assoc.disjE assoc.dom_sing /= (negbTE y_d).
eapply state_mint_var_mint; first by apply s_st_h.
rewrite assoc.union_assoc.
apply assoc.get_union_R => //.
apply assoc.disj_union_L.
by rewrite assoc.disjE assoc.dom_sing /= (negbTE A_d).
by rewrite assoc.disjE assoc.dom_sing /= (negbTE y_d).
exact H2.
- apply heap.disj_union_R.
+ apply (proj2 s_st_h y0 y).
by auto.
rewrite assoc.union_assoc.
apply assoc.get_union_R; last by exact Hry0.
apply assoc.disj_union_L.
by rewrite assoc.disjE assoc.dom_sing /= (negbTE A_d).
by rewrite assoc.disjE assoc.dom_sing /= (negbTE y_d).
rewrite assoc.get_union_sing_neq; last by auto.
by rewrite assoc.get_union_sing_eq.
+ apply (proj2 s_st_h y0 A).
* move=> abs; subst y0.
move/assoc.get_Some_in_dom : Hry0.
by apply/negPn.
* rewrite assoc.union_assoc.
apply assoc.get_union_R; last by exact Hry0.
apply assoc.disj_union_L.
by rewrite assoc.disjE assoc.dom_sing /= (negbTE A_d).
by rewrite assoc.disjE assoc.dom_sing /= (negbTE y_d).
* by assoc_get_Some.
apply (proj2 s_st_h y y0).
- exact x_y0.
- rewrite assoc.get_union_sing_neq; last by auto.
by rewrite assoc.get_union_sing_eq.
- rewrite assoc.union_assoc.
apply assoc.get_union_R; last by exact Hry0.
apply assoc.disj_union_L.
by rewrite assoc.disjE assoc.dom_sing /= (negbTE A_d).
by rewrite assoc.disjE assoc.dom_sing /= (negbTE y_d).
* have <- : heap_mint rx st h = heap_mint rx st' h'.
apply heap_mint_unchanged2 with
(d := (heap_mint (unsign rk ry) st h +++ heap_mint (signed L rA) st h)) (x := x) (s := s).
- apply H1.
apply assoc.get_Some_in_cdom with x.
apply assoc.get_union_R.
apply assoc.disj_union_R.
by apply assoc.disj_sing.
by rewrite assoc.disjE assoc.dom_sing /= (negbTE A_d).
apply assoc.get_union_R => //.
by rewrite assoc.disjE assoc.dom_sing /= (negbTE y_d).
- apply (state_mint_var_mint _ _ _ _ _ _ s_st_h).
rewrite assoc.union_assoc.
apply assoc.get_union_R; last by exact Hrx.
apply assoc.disj_union_L.
by rewrite assoc.disjE assoc.dom_sing /= (negbTE A_d).
by rewrite assoc.disjE assoc.dom_sing /= (negbTE y_d).
- exact H2.
- apply heap.disj_union_R.
+ apply (proj2 s_st_h x y).
* move=> abs; subst x.
move/assoc.get_Some_in_dom : Hrx.
by apply/negPn.
* rewrite assoc.union_assoc.
apply assoc.get_union_R; last by exact Hrx.
apply assoc.disj_union_L.
by rewrite assoc.disjE assoc.dom_sing /= (negbTE A_d).
by rewrite assoc.disjE assoc.dom_sing /= (negbTE y_d).
* rewrite assoc.get_union_sing_neq; last by auto.
by rewrite assoc.get_union_sing_eq.
+ apply (proj2 s_st_h x A).
* move=> abs; subst x.
move/assoc.get_Some_in_dom : Hrx.
by apply/negPn.
* rewrite assoc.union_assoc.
apply assoc.get_union_R; last by exact Hrx.
apply assoc.disj_union_L.
by rewrite assoc.disjE assoc.dom_sing /= (negbTE A_d).
by rewrite assoc.disjE assoc.dom_sing /= (negbTE y_d).
* by assoc_get_Some.
case/assoc.get_union_Some_inv : Hry0 => Hry0.
- case/assoc.get_sing_inv : Hry0 => ? ?; subst y0 ry0.
rewrite heap.disjE dom_rA -heap.disjE.
apply (proj2 s_st_h x A).
+ exact x_y0.
+ rewrite assoc.union_assoc.
apply assoc.get_union_R; last by exact Hrx.
apply assoc.disj_union_L.
by rewrite assoc.disjE assoc.dom_sing /= (negbTE A_d).
by rewrite assoc.disjE assoc.dom_sing /= (negbTE y_d).
+ by assoc_get_Some.
- case/assoc.get_union_Some_inv : Hry0 => Hry0.
+ case/assoc.get_sing_inv : Hry0 => ? ?; subst y0 ry0.
rewrite heap.disjE dom_rx -heap.disjE.
apply (proj2 s_st_h x y).
exact x_y0.
+ rewrite assoc.union_assoc.
apply assoc.get_union_R; last by exact Hrx.
apply assoc.disj_union_L.
by rewrite assoc.disjE assoc.dom_sing /= (negbTE A_d).
by rewrite assoc.disjE assoc.dom_sing /= (negbTE y_d).
rewrite assoc.get_union_sing_neq; last by auto.
by rewrite assoc.get_union_sing_eq.
+ have <- : heap_mint ry0 st h = heap_mint ry0 st' h'.
apply heap_mint_unchanged2 with
(d := heap_mint (unsign rk ry) st h +++ heap_mint (signed L rA) st h) (x := y0) (s := s).
- apply H1.
apply assoc.get_Some_in_cdom with y0.
apply assoc.get_union_R.
apply assoc.disj_union_R.
by apply assoc.disj_sing.
by rewrite assoc.disjE assoc.dom_sing /= (negbTE A_d).
apply assoc.get_union_R => //.
by rewrite assoc.disjE assoc.dom_sing /= (negbTE y_d).
- apply (state_mint_var_mint _ _ _ _ _ _ s_st_h).
rewrite assoc.union_assoc.
apply assoc.get_union_R; last by exact Hry0.
apply assoc.disj_union_L.
by rewrite assoc.disjE assoc.dom_sing /= (negbTE A_d).
by rewrite assoc.disjE assoc.dom_sing /= (negbTE y_d).
- exact H2.
- apply heap.disj_union_R.
+ apply (proj2 s_st_h y0 y).
* move=> abs; subst y0.
move/assoc.get_Some_in_dom : Hry0.
by apply/negPn.
* rewrite assoc.union_assoc.
apply assoc.get_union_R; last by exact Hry0.
apply assoc.disj_union_L.
by rewrite assoc.disjE assoc.dom_sing /= (negbTE A_d).
by rewrite assoc.disjE assoc.dom_sing /= (negbTE y_d).
* rewrite assoc.get_union_sing_neq; last by auto.
by rewrite assoc.get_union_sing_eq.
+ apply (proj2 s_st_h y0 A).
* move=> abs; subst y0.
move/assoc.get_Some_in_dom : Hry0.
by apply/negPn.
* rewrite assoc.union_assoc.
apply assoc.get_union_R; last by exact Hry0.
apply assoc.disj_union_L.
by rewrite assoc.disjE assoc.dom_sing /= (negbTE A_d).
by rewrite assoc.disjE assoc.dom_sing /= (negbTE y_d).
* by assoc_get_Some.
apply (proj2 s_st_h x y0).
exact x_y0.
+ rewrite assoc.union_assoc.
apply assoc.get_union_R; last by exact Hrx.
apply assoc.disj_union_L.
by rewrite assoc.disjE assoc.dom_sing /= (negbTE A_d).
by rewrite assoc.disjE assoc.dom_sing /= (negbTE y_d).
+ rewrite assoc.union_assoc.
apply assoc.get_union_R; last by exact Hry0.
apply assoc.disj_union_L.
by rewrite assoc.disjE assoc.dom_sing /= (negbTE A_d).
by rewrite assoc.disjE assoc.dom_sing /= (negbTE y_d).
Qed.
Definition sim d := fwd_sim (state_mint d).
Definition psim d := pfwd_sim (state_mint d).
Definition sim_b b pre_b post_b d := fwd_sim_b (state_mint d) b pre_b post_b.
Lemma state_mint_inj : forall d s st h s',
state_mint d s st h -> state_mint d s' st h ->
syntax_m.seplog_m.assert_m.expr_m.store.store_heap.proj s (assoc.dom d) =
syntax_m.seplog_m.assert_m.expr_m.store.store_heap.proj s' (assoc.dom d).
Proof.
move=> d s st h s'.
rewrite /state_mint.
move=> [s_st_h1 s_st_h2] [s'_st_h1 s'_st_h2].
apply syntax_m.seplog_m.assert_m.expr_m.store.extensionality => x.
have [X|[rx X]] : assoc.get x d = None \/ exists rx, assoc.get x d = Some rx.
case: (assoc.get x d); [move=> rx_; right; by exists rx_ | by auto].
- rewrite !syntax_m.seplog_m.assert_m.expr_m.store.get_proj' //.
by apply assoc.get_None_notin.
by apply assoc.get_None_notin.
- move: (s_st_h1 _ _ X) => x_s_rx.
move: (s'_st_h1 _ _ X) => x_s'_rx.
destruct rx as [rk rx|rx].
- case : (x_s_rx) => x_s_over [rx_mem rx_fit].
case : (x_s'_rx) => _ [x_s'_over rx'_mem].
have Htmp : ([ x ]_ s = [ x ]_ s')%seplog_expr.
have Htmp : Z2ints 32 (Zabs_nat (u2Z ([rk ]_ st)%mips_expr)) ([ x ]_ s)%seplog_expr =
Z2ints 32 (Zabs_nat (u2Z ([rk ]_ st)%mips_expr)) ([ x ]_ s')%seplog_expr.
eapply assert_m.mapstos_inj.
rewrite len_Z2ints; reflexivity.
rewrite len_Z2ints; reflexivity.
by apply x_s_rx.
exact rx'_mem.
by apply Z2ints_inj in Htmp.
rewrite !syntax_m.seplog_m.assert_m.expr_m.store.get_proj //.
by eapply assoc.get_Some_in_dom; eauto.
by eapply assoc.get_Some_in_dom; eauto.
- case : (x_s_rx) => rx_2_fit [slen [ptr [A [A_nk [Hnk [sign [bound [ptr_fit [Sum_A mem]]]]]]]]].
case : (x_s'_rx) => _ [slen' [ptr' [A' [A'_nk [Hnk' [sign' [bound' [ptr'_fit [Sum_A' mem']]]]]]]]].
rewrite !syntax_m.seplog_m.assert_m.expr_m.store.get_proj //; last 2 first.
by eapply assoc.get_Some_in_dom; eauto.
by eapply assoc.get_Some_in_dom; eauto.
have : slen = slen'.
move/con_heap_mint_signed_con_TT : mem.
rewrite assert_m.con_assoc_equiv; move/assert_m.mapsto_con_get => mem.
move/con_heap_mint_signed_con_TT : mem'.
rewrite assert_m.con_assoc_equiv; move/assert_m.mapsto_con_get => mem'.
rewrite mem in mem'; by case: mem'.
move=> ?; subst slen'.
have : ptr = ptr'.
rewrite assert_m.con_assoc_equiv assert_m.con_com_equiv 2!assert_m.con_assoc_equiv in mem.
move/con_heap_mint_signed_con_TT : mem.
move/assert_m.mapsto_con_get => mem.
rewrite assert_m.con_assoc_equiv assert_m.con_com_equiv 2!assert_m.con_assoc_equiv in mem'.
move/con_heap_mint_signed_con_TT : mem'.
move/assert_m.mapsto_con_get => mem'.
rewrite mem /= in mem'; by case: mem'.
move=> ?; subst ptr'.
case: (Z_zerop (s2Z slen)) => slen_neq0.
rewrite slen_neq0 /= in sign sign'.
symmetry in sign.
apply (proj1 (Zsgn_null _)) in sign.
symmetry in sign'.
apply (proj1 (Zsgn_null _)) in sign'.
congruence.
move: mem; rewrite assert_m.con_com_equiv; move/con_heap_mint_signed_con_TT => mem.
move: mem'; rewrite assert_m.con_com_equiv; move/con_heap_mint_signed_con_TT => mem'.
rewrite -/([ int_e ptr ]e_st)%mips_expr in ptr_fit.
move: (assert_m.mapstos_con_inj _ _ _ _ _ _ _ _ ptr_fit A_nk A'_nk mem mem') => H.
subst A'.
by rewrite Sum_A Sum_A'.
Qed.
Lemma transport : forall d p c I0,
safe_termination (state_mint d) c ->
terminating p ->
incl (syntax_m.cmd_vars p) (seq_ext.s2l (assoc.dom d)) ->
forall encode decode,
(forall s, state_mint d s (fst (encode d s)) (snd (encode d s))) ->
(forall st he, state_mint d (decode d (st, he)) st he /\
syntax_m.seplog_m.assert_m.expr_m.store.store_heap.dom (decode d (st, he)) = assoc.dom d) ->
psim d I0 p c ->
forall (P0 Pf : syntax_m.seplog_m.assert_m.assert),
syntax_m.seplog_m.hoare_m.hoare P0 p Pf ->
forall s,
({{ fun st h => encode d s = (st, h) /\ P0 s syntax_m.seplog_m.assert_m.heap.emp /\ I0 s st h }} c
{{ fun st' h' => Pf
(syntax_m.seplog_m.assert_m.expr_m.store.store_heap.union
(decode d (st', h'))
(syntax_m.seplog_m.assert_m.expr_m.store.store_heap.difs s (assoc.dom d)))
syntax_m.seplog_m.assert_m.heap.emp }})%mips_hoare.
Proof.
move=> d p c I0 Hsafe_term Hterm Hincl enc dec Henc Hdec Hsim_c_c P0 Pf Hhoare_c s.
apply mips_seplog.hoare_prop_m.hoare_complete => /= st h [H_s_st_h [HP0 HI0]]; split.
- move=> Habsurd.
rewrite /safe_termination in Hsafe_term.
lapply (Hsafe_term s st h); last first.
rewrite -/(fst (st, h)) -{2}/(snd (st, h)) -H_s_st_h.
by apply Henc.
case=> s' Hs'.
by move: (mips_syntax.semop_deter_prop_m.exec_deter _ _ _ Hs' _ Habsurd).
- move=> st' h' Hexec_asm.
move/syntax_m.seplog_m.soundness : Hhoare_c.
case/(_ _ _ HP0) => _ Hhoare_c.
apply Hhoare_c.
move=> {Hhoare_c HP0}.
apply pfwd_sim_fwd_sim in Hsim_c_c => //.
apply fwd_sim_bck_sim in Hsim_c_c => //.
move=> {Hsafe_term}.
rewrite /bck_sim in Hsim_c_c.
have Hs_encode_s : state_mint d s (fst (enc d s)) (snd (enc d s)).
move: (Henc s).
by destruct (enc d s).
move=> {Henc}.
destruct (enc d s) as [s1 s2].
case: H_s_st_h => Hs1 Hs2; subst s1 s2.
case: {Hsim_c_c Hexec_asm}(Hsim_c_c _ _ _ Hs_encode_s HI0 _ _ Hexec_asm) => s' [] Hs' H.
move: {Hdec}(Hdec st' h') => [Hdec Hdec2].
move: {Hdec}(state_mint_inj _ _ _ _ _ H Hdec) => Hinj.
have -> : dec d (st', h') = syntax_m.seplog_m.assert_m.expr_m.store.store_heap.proj (dec d (st', h')) (assoc.dom d).
rewrite -Hdec2.
by rewrite syntax_m.seplog_m.assert_m.expr_m.store.store_heap.proj_itself.
have -> : syntax_m.seplog_m.assert_m.expr_m.store.store_heap.difs s (assoc.dom d) = syntax_m.seplog_m.assert_m.expr_m.store.store_heap.difs s' (assoc.dom d).
apply syntax_m.seplog_m.assert_m.expr_m.store.extensionality => v.
case/orP : (orbN (v \in assoc.dom d)) => X.
+ rewrite syntax_m.seplog_m.assert_m.expr_m.store.get_difs' //.
by rewrite syntax_m.seplog_m.assert_m.expr_m.store.get_difs'.
+ rewrite syntax_m.seplog_m.assert_m.expr_m.store.get_difs //.
rewrite syntax_m.seplog_m.assert_m.expr_m.store.get_difs //.
Var_unchanged.
have X' : ~ In v (syntax_m.cmd_vars p).
move/Hincl.
move/(@seq_ext.inP _ (assoc.dom d)).
by rewrite (negbTE X).
contradict X'.
by apply syntax_m.In_cmd_vars.
by rewrite -Hinj -syntax_m.seplog_m.assert_m.expr_m.store.store_heap.proj_difs.
Qed.