Require Import ZArith. Require Import List. Require Import util. Require Import machine_int. Import MachineInt. Require Import machine_int_spec. Require Import state. Open Local Scope asm_heap_scope. Open Local Scope Z_scope. Load heap_tactics. (* * shift left 2 *) Definition shl2 (l:nat) (a:int l) := shl 2 a. Implicit Arguments shl2. Lemma shift_2_mult_4 : forall (v:int 32) n, u2Z v = 4 * n -> v = shl2 (Z2u 32 n). intros. destruct n. unfold shl2. apply u2Z_injection. rewrite (@shl_u2Z 2 32 (Z2u 32 0) 30). rewrite Z2u_injection. simpl. omega. generalize (Zpower_1 32); omega. auto. rewrite Z2u_injection. generalize (Zpower_1 30); omega. generalize (Zpower_1 32); omega. apply u2Z_injection. unfold shl2. assert (Zpos p < Zpower 2 30). apply Zpower_shift_2. assert (u2Z v < Zbeta 1). apply max_u2Z_32. omega. rewrite (@shl_u2Z 2 32 (Z2u 32 (Zpos p)) 30). simpl (Zpower 2 2). rewrite Z2u_injection. omega. split. generalize (Zgt_pos_0 p); omega. apply Zlt_trans with (Zpower 2 30). auto. apply Zpower_2_lt; omega. omega. rewrite Z2u_injection. auto. split. generalize (Zgt_pos_0 p); omega. apply Zlt_trans with (Zpower 2 30). auto. apply Zpower_2_lt; omega. generalize (min_u2Z v); intro. assert (Zneg p >= 0). omega. generalize (Zlt_neg_0 p); intro. red in H1. red in H2. rewrite H2 in H1. tauto. Qed. Lemma shl_zero : forall n m, shl n (Z2u m 0) = Z2u m 0. intros. apply u2Z_injection. assert (n <= m \/ n > m )%nat. omega. inversion_clear H. rewrite (@shl_u2Z n m (Z2u m 0) (m-n)). rewrite Z2u_injection. ring. generalize (Zpower_1 m); omega. rewrite le_plus_minus_r. omega. auto. rewrite Z2u_injection. generalize (Zpower_1 (m-n)); omega. generalize (Zpower_1 m); omega. rewrite shl_u2Z''. rewrite Z2u_injection. auto. generalize (Zpower_1 m); omega. omega. Qed. Lemma shl_S : forall n, 0 <= n -> n + 1 < Zpower 2 30 -> shl2 (Z2u 32 (n+1)) = add four32 (shl2 (Z2u 32 n)). intros. destruct n. simpl. unfold shl2. apply u2Z_injection. rewrite (@shl_u2Z 2 32 (Z2u 32 (1)) 30). rewrite add_u2Z. rewrite (@shl_u2Z 2 32 (Z2u 32 0) 30). rewrite Z2u_injection. rewrite Z2u_injection. unfold four32. rewrite Z2u_injection. auto. split. omega. auto. split. omega. auto. split. omega. auto. auto. rewrite Z2u_injection. simpl. omega. auto. rewrite (@shl_u2Z 2 32 (Z2u 32 0) 30). rewrite Z2u_injection. simpl. unfold four32. rewrite Z2u_injection. simpl; auto. split. omega. simpl; auto. split. omega. auto. auto. rewrite Z2u_injection. auto. split. omega. auto. auto. rewrite Z2u_injection. auto. split. omega. auto. auto. unfold shl2. apply u2Z_injection. rewrite (@shl_u2Z 2 32 (Z2u 32 (Zpos p+1)) 30). rewrite add_u2Z. rewrite (@shl_u2Z 2 32 (Z2u 32 (Zpos p)) 30). rewrite Z2u_injection. rewrite Z2u_injection. unfold four32. rewrite Z2u_injection. simpl (Zpower 2 2). omega. split. omega. apply Zle_lt_trans with (Zpower 2 2). simpl. omega. apply Zpower_2_lt. omega. split. generalize (Zgt_pos_0 p); omega. apply Zlt_trans with (Zpos p + 1). omega. apply Zlt_trans with (Zpower 2 30). omega. apply Zpower_2_lt. omega. split. generalize (Zgt_pos_0 p); omega. apply Zlt_trans with (Zpower 2 30). omega. apply Zpower_2_lt. omega. omega. rewrite Z2u_injection. omega. split. generalize (Zgt_pos_0 p); omega. apply Zlt_trans with (Zpower 2 30). omega. apply Zpower_2_lt. omega. unfold four32. rewrite Z2u_injection. rewrite (@shl_u2Z 2 32 (Z2u 32 (Zpos p)) 30). rewrite Z2u_injection. simpl (Zpower 2 2). cutrewrite (4+Zpos p*4=4 * (Zpos p + 1)). apply Zlt_le_trans with (Zpower 2 2 * Zpower 2 30). simpl (Zpower 2 2). omega. simpl. omega. ring. split. generalize (Zgt_pos_0 p); omega. apply Zlt_trans with (Zpos p + 1). omega. apply Zlt_trans with (Zpower 2 30). auto. apply Zpower_2_lt. omega. omega. rewrite Z2u_injection. omega. split. generalize (Zgt_pos_0 p); omega. apply Zlt_trans with (Zpos p + 1). omega. apply Zlt_trans with (Zpower 2 30). auto. apply Zpower_2_lt. omega. split. omega. apply Zle_lt_trans with (Zpower 2 2). simpl. omega. apply Zpower_2_lt. omega. auto. rewrite Z2u_injection. auto. split. generalize (Zgt_pos_0 p); omega. apply Zlt_trans with (Zpower 2 30). auto. apply Zpower_2_lt. omega. generalize (Zlt_neg_0 p); intro. assert (~(0 <= Zneg p)). omega. tauto. Qed. (********************************************) (* operational semantics*) (********************************************) Definition immediate := int 16. Definition address := int 32. Definition word := int 32. Definition shifta := int 5. Inductive cmd : Set := | skip : cmd | add : gp_reg -> gp_reg -> gp_reg -> cmd | addi : gp_reg -> gp_reg -> immediate -> cmd | addiu : gp_reg -> gp_reg -> immediate -> cmd | addu : gp_reg -> gp_reg -> gp_reg -> cmd | cmd_and : gp_reg -> gp_reg -> word -> cmd | lw : gp_reg -> immediate (*index*) -> gp_reg (*base*) -> cmd | lwxs : gp_reg -> gp_reg (*index*) -> gp_reg (*base*)-> cmd | maddu : gp_reg -> gp_reg -> cmd | mflhxu : gp_reg -> cmd | mflo : gp_reg -> cmd | mfhi : gp_reg -> cmd | mtlo : gp_reg -> cmd | mthi : gp_reg -> cmd | msubu : gp_reg -> gp_reg -> cmd | multu : gp_reg -> gp_reg -> cmd (* | mfc0 : gp_reg -> cp0_reg -> cmd | mtc0 : gp_reg -> cp0_reg -> cmd *) | nor : gp_reg -> gp_reg -> gp_reg -> cmd | sll: gp_reg -> gp_reg -> shifta -> cmd | sltu : gp_reg -> gp_reg -> gp_reg -> cmd | sw : gp_reg -> immediate (*index*) -> gp_reg (*base*) -> cmd (* | sub : gp_reg -> gp_reg -> gp_reg -> cmd | subu : gp_reg -> gp_reg -> gp_reg -> cmd *) | seq : cmd -> cmd -> cmd | ifte_beq : gp_reg -> gp_reg -> cmd -> cmd -> cmd | ifte_bltz : gp_reg -> cmd -> cmd -> cmd | while_bne : gp_reg -> gp_reg -> cmd -> cmd. Notation "c ; d" := (seq c d) (at level 81, right associativity) : mips_scope. Notation "'ifte_beq' a ',' b 'thendo' x 'elsedo' y" := (ifte_beq a b x y) (at level 80) : mips_scope. Notation "'ifte_bltz' a 'thendo' x 'elsedo' y" := (ifte_bltz a x y) (at level 80) : mips_scope. Open Local Scope mips_scope. Close Local Scope Z_scope. Close Local Scope nat_scope. Definition state := gpr.store * cp0.store * multiplier.m * heap.h. Open Local Scope nat_scope. Open Local Scope Z_scope. Definition sign_extend_16_32 (a:int 16) : int 32 := sign_extend 16 a. Lemma sign_extend_16_32': forall n, n < Zpower 2 15 -> sign_extend_16_32 (Z2u 16 n) = Z2u 32 n. unfold sign_extend_16_32. intros. assert (15 > 0)%nat; try omega. apply (@sign_extend_Z2u n 15 16 H0 H). Qed. Inductive expr : Set := | var_e : gp_reg -> expr | int_e : int 32 -> expr | add_e : expr -> expr -> expr | shl2_e : expr -> expr. Fixpoint eval (e:expr) (s:gpr.store) {struct e} : int 32 := match e with | var_e w => gpr.lookup w s | int_e x => x | add_e e1 e2 => eval e1 s (+) eval e2 s | shl2_e e => shl2 (eval e s) end. (* instructions suffixed with "u" does not trap on overflow *) Reserved Notation "s -- c --> t" (at level 82, no associativity). (***************************************) (* a ranger ailleurs *) (***************************************) Definition nat_of_Z (z:Z) : nat := match z with Zpos p => nat_of_P p | _ => O end. (***************************************) Inductive exec : option state -> cmd -> option state -> Prop := exec_none : forall c, None -- c --> None | exec_skip : forall s, Some s -- skip --> Some s | exec_addi : forall s1 s2 m h rt rs vrs imm, gpr.lookup rs s1 = vrs -> - 2^^31 <= s2Z vrs + s2Z (sign_extend_16_32 imm) < 2^^31 -> Some (s1,s2,m,h) -- addi rt rs imm --> Some (gpr.update rt (vrs (+) sign_extend_16_32 imm) s1, s2, m,h) | exec_addiu : forall s1 s2 m h rt rs vrs imm, gpr.lookup rs s1 = vrs -> Some (s1,s2,m,h) -- addiu rt rs imm --> Some (gpr.update rt (vrs (+) sign_extend_16_32 imm) s1, s2, m,h) | exec_add : forall s1 s2 vrt vrs m h rd rs rt, gpr.lookup rs s1 = vrs -> gpr.lookup rt s1 = vrt -> - 2^^ 31 <= s2Z vrt + s2Z vrs < 2^^31 -> Some (s1,s2,m,h) -- add rd rs rt --> Some (gpr.update rd (vrs (+) vrt) s1, s2, m, h) | exec_addu : forall s1 s2 vrt vrs m h rd rs rt, gpr.lookup rt s1 = vrt -> gpr.lookup rs s1 = vrs -> Some (s1,s2,m,h) -- addu rd rs rt --> Some (gpr.update rd (vrs (+) vrt) s1, s2, m, h) | exec_and : forall s1 s2 vrt m h rs rt num, gpr.lookup rt s1 = vrt -> Some (s1, s2,m,h) -- cmd_and rs rt num --> Some (gpr.update rs (int_and vrt num) s1,s2,m,h) | exec_lw : forall s1 s2 m h rt offset base vbase l z, gpr.lookup base s1 = vbase -> u2Z (vbase (+) sign_extend_16_32 offset) = 4 * Z_of_nat l -> heap.lookup l h = Some z -> Some (s1,s2,m,h) -- lw rt offset base --> Some (gpr.update rt z s1,s2,m,h) | exec_lw_error : forall s1 s2 m h rt offset base vbase, gpr.lookup base s1 = vbase -> ~(exists l, u2Z (vbase (+) sign_extend_16_32 offset) = 4 * Z_of_nat l /\ exists z, heap.lookup l h = Some z)-> Some (s1,s2,m,h) -- lw rt offset base --> None | exec_lwxs : forall s1 s2 (m:multiplier.m) h rt index vindex base vbase l z, gpr.lookup base s1 = vbase -> gpr.lookup index s1 = vindex -> u2Z (vbase (+) shl 2 vindex) = 4 * Z_of_nat l -> heap.lookup l h = Some z -> Some (s1,s2,m,h) -- lwxs rt index base --> Some (gpr.update rt z s1,s2,m,h) | exec_lwxs_error : forall s1 s2 (m:multiplier.m) h rt index vindex base vbase, gpr.lookup base s1 = vbase -> gpr.lookup index s1 = vindex -> ~(exists l, u2Z (vbase (+) shl 2 vindex) = 4 * Z_of_nat l /\ exists z, heap.lookup l h = Some z) -> Some (s1,s2,m,h) -- lwxs rt index base --> None | exec_maddu : forall s1 s2 (m:multiplier.m) h rs vrs rt vrt, gpr.lookup rt s1 = vrt -> gpr.lookup rs s1 = vrs -> Some (s1,s2,m,h) -- maddu rs rt --> Some (s1,s2,multiplier.maddu_op (umul vrs vrt) m,h) | exec_mflhxu : forall s1 s2 m h rd, Some (s1,s2,m,h) -- mflhxu rd --> Some (gpr.update rd (multiplier.lo m) s1,s2,multiplier.mflhxu_op m,h) | exec_mfhi : forall s1 s2 m h rd, Some (s1,s2,m,h) -- mfhi rd --> Some (gpr.update rd (multiplier.hi m) s1,s2,m,h) | exec_mflo : forall s1 s2 m h rd, Some (s1,s2,m,h) -- mflo rd --> Some (gpr.update rd (multiplier.lo m) s1,s2,m,h) | exec_mthi : forall s1 s2 m h rs vrs, gpr.lookup rs s1 = vrs -> Some (s1,s2,m,h) -- mthi rs --> Some (s1,s2,multiplier.mthi_op vrs m,h) | exec_mtlo : forall s1 s2 m h rs vrs, gpr.lookup rs s1 = vrs -> Some (s1,s2,m,h) -- mtlo rs --> Some (s1,s2,multiplier.mtlo_op vrs m,h) | exec_msubu : forall s1 s2 (m:multiplier.m) h rs vrs rt vrt, gpr.lookup rt s1 = vrt -> gpr.lookup rs s1 = vrs -> Some (s1,s2,m,h) -- msubu rs rt --> Some (s1,s2,(multiplier.msubu_op (umul vrs vrt) m),h) | exec_multu : forall s1 s2 m h rs vrs rt vrt, gpr.lookup rt s1 = vrt -> gpr.lookup rs s1 = vrs -> Some (s1,s2,m,h) -- multu rs rt --> Some (s1,s2,multiplier.multu_op (umul vrs vrt) m,h) (* | exec_mfc0 : forall s1 s2 vrt m h rs rt, (* TODO: rajouter le test pour les droits *) cp0.lookup rt s2 = vrt -> Some (s1,s2,m,h) -- mfc0 rs rt --> Some (gpr.update rs vrt s1,s2,m,h) | exec_mtc0 : forall s1 s2 vrs m h rs rt, (* TODO: rajouter le test pour les droits *) gpr.lookup rs s1 = vrs -> Some (s1,s2,m,h) -- mtc0 rs rt --> Some (s1,(cp0.update rt vrs s2),m,h) *) | exec_nor : forall rd rs rt vrs vrt s1 s2 m h, gpr.lookup rs s1 = vrs -> gpr.lookup rt s1 = vrt -> Some (s1,s2,m,h) -- nor rd rs rt --> Some (gpr.update rd (int_not (int_or vrs vrt)) s1,s2,m,h) | exec_sll : forall s1 s2 m h rx ry sa, Some (s1,s2,m,h) -- sll rx ry sa --> Some (gpr.update rx (shl (nat_of_Z (u2Z sa)) (gpr.lookup ry s1)) s1,s2,m,h) | exec_sltu : forall s1 s2 m h rd rs rt flag, flag = (if (Zlt_bool (u2Z (gpr.lookup rs s1)) (u2Z (gpr.lookup rt s1))) then one32 else zero32) -> Some (s1,s2,m,h) -- sltu rd rs rt --> Some (gpr.update rd flag s1,s2,m,h) (* | exec_sub : forall s1 s2 vrt vrs m h rd rs rt, gpr.lookup rt s1 = vrt -> gpr.lookup rs s1 = vrs -> u2Z vrt <= u2Z vrs -> Some (s1,s2,m,h) -- sub rd rs rt --> Some (gpr.update rd (MachineInt.sub vrs vrt) s1,s2,m,h) | exec_subu : forall s1 s2 vrt vrs m h rd rs rt, gpr.lookup rt s1 = vrt -> gpr.lookup rs s1 = vrs -> Some (s1,s2,m,h) -- subu rd rs rt --> Some (gpr.update rd (MachineInt.sub vrs vrt) s1,s2,m,h) *) | exec_sw : forall s1 s2 (m:multiplier.m) h rt vrt offset base vbase l, gpr.lookup base s1 = vbase -> gpr.lookup rt s1 = vrt -> u2Z (vbase (+) sign_extend_16_32 offset) = 4 * Z_of_nat l -> (exists z, heap.lookup l h = Some z) -> Some (s1,s2,m,h) -- sw rt offset base --> Some (s1,s2,m,heap.update l vrt h) | exec_sw_err : forall s1 s2 (m:multiplier.m) h rt vrt offset base vbase, gpr.lookup base s1 = vbase -> gpr.lookup rt s1 = vrt -> ~(exists l, u2Z (vbase (+) sign_extend_16_32 offset) = 4 * Z_of_nat l /\ exists z, heap.lookup l h = Some z) -> Some (s1,s2,m,h) -- sw rt offset base --> None | exec_seq : forall s s' s'' c d, exec s c s' -> exec s' d s'' -> exec s (c ; d) s'' | exec_ifte_beq_true : forall s1 s2 m h s' r1 r2 c d, gpr.lookup r1 s1 = gpr.lookup r2 s1 -> Some (s1,s2,m,h) -- c --> s' -> Some (s1,s2,m,h) -- ifte_beq r1, r2 thendo c elsedo d --> s' | exec_ifte_beq_false : forall s1 s2 m h s' r1 r2 c d, gpr.lookup r1 s1 <> gpr.lookup r2 s1 -> Some (s1,s2,m,h) -- d --> s' -> Some (s1,s2,m,h) -- ifte_beq r1, r2 thendo c elsedo d --> s' | exec_ifte_bltz_true : forall s1 s2 m h s' r1 c d, s2Z (gpr.lookup r1 s1) < 0 -> Some (s1,s2,m,h) -- c --> s' -> Some (s1,s2,m,h) -- ifte_bltz r1 thendo c elsedo d --> s' | exec_ifte_bltz_false : forall s1 s2 m h s' r1 c d, s2Z (gpr.lookup r1 s1) >= 0 -> Some (s1,s2,m,h) -- d --> s' -> Some (s1,s2,m,h) -- ifte_bltz r1 thendo c elsedo d --> s' | exec_while_bne_true : forall s1 s2 m h s' s'' r1 r2 c, u2Z (eval (var_e r1) s1) <> u2Z (eval (var_e r2) s1) -> Some (s1,s2,m,h) -- c --> s' -> s' -- while_bne r1 r2 c --> s'' -> Some (s1,s2,m,h) -- while_bne r1 r2 c --> s'' | exec_while_bne_false : forall s1 s2 m h r1 r2 c, u2Z (eval (var_e r1) s1) = u2Z (eval (var_e r2) s1) -> Some (s1,s2,m,h) -- while_bne r1 r2 c --> Some (s1,s2,m,h) where "s -- c --> t" := (exec s c t) : mips_scope. Lemma from_none' : forall s0 c s, (s0 -- c --> s) -> s0 = None -> s = None. do 4 intro. induction H; intro; try auto||discriminate. Qed. Lemma from_none : forall c s, (None -- c --> s) -> s = None. intros; eapply from_none'. apply H. auto. Qed. (**************************************************************************** * assertions ****************************************************************************) Definition assert := gpr.store -> cp0.store -> multiplier.m -> heap.h -> Prop. Definition TT : assert := fun _ _ _ _ => True. Definition And (P Q:assert) : assert := fun s s' m h => P s s' m h /\ Q s s' m h. Definition x_EQ_y (x y : gp_reg) : assert := fun s _ _ _ => gpr.lookup x s = gpr.lookup y s. Module sep. Definition entails (P Q:assert) : Prop := forall s s' m h, P s s' m h -> Q s s' m h. Notation "P ==> Q" := (entails P Q) (at level 90, no associativity). Definition equiv (P Q:assert) : Prop := forall s s' m h, P s s' m h <-> Q s s' m h. Notation "P <==> Q" := (equiv P Q) (at level 90, no associativity). Axiom assert_ext: forall P Q, (P <==> Q) -> P = Q. Definition con (P Q:assert) : assert := fun s s' m h => exists h1, exists h2, h1 # h2 /\ h = h1 +++ h2 /\ P s s' m h1 /\ Q s s' m h2. Notation "P ** Q" := (con P Q) (at level 80) : mips_scope. Lemma con_com_equiv : forall P Q, (P ** Q) = (Q ** P). intros; apply assert_ext. split; intros. inversion_clear H as [h1]. inversion_clear H0 as [h2]. exists h2; exists h1. decompose [and] H; clear H. intuition. Disjoint_heap. Equal_heap. inversion_clear H as [h1]. inversion_clear H0 as [h2]. exists h2; exists h1. intuition. Disjoint_heap. Equal_heap. Qed. Lemma con_assoc_equiv : forall P Q R, ((Q ** P) ** R) = (Q ** (P ** R)). intros; apply assert_ext. split; intros. inversion_clear H as [h1]. inversion_clear H0 as [h2]. decompose [and] H; clear H. inversion_clear H1 as [h11]. inversion_clear H as [h12]. decompose [and] H1; clear H1. exists h11; exists (h12 +++ h2). split. Disjoint_heap. split. Equal_heap. split; auto. exists h12; exists h2. split. Disjoint_heap. split. Equal_heap. split; auto. inversion_clear H as [h1]. inversion_clear H0 as [h2]. decompose [and] H; clear H. inversion_clear H4 as [h21]. inversion_clear H as [h22]. decompose [and] H3; clear H3. exists (h21 +++ h1); exists h22. split. Disjoint_heap. split. Equal_heap. split; auto. exists h1; exists h21. split. Disjoint_heap. split. Equal_heap. split; auto. Qed. Definition imp (P Q:assert) : assert := fun s s' m h => forall h', h # h' /\ P s s' m h' -> forall h'', h'' = h +++ h' -> Q s s' m h''. Notation "P -* Q" := (imp P Q) (at level 80) : mips_scope. Definition emp : assert := fun s s' m h => h = heap.emp. Lemma con_emp: forall P, (P ** sep.emp) ==> P. red; intros. inversion_clear H as [h1]. inversion_clear H0 as [h2]. decompose [and] H; clear H. red in H4. subst h2. cutrewrite (h = h1). auto. Equal_heap. Qed. Lemma con_emp': forall P, P ==> (P ** sep.emp). red; intros. exists h; exists heap.emp. split. Disjoint_heap. split. Equal_heap. split; auto. red; auto. Qed. Lemma con_emp_equiv : forall P, (P ** sep.emp) = P . intros. apply assert_ext. split. apply con_emp. apply con_emp'. Qed. Lemma mp : forall P Q, Q ** (Q -* P) ==> P. red; intros. inversion_clear H as [h1]. inversion_clear H0 as [h2]. decompose [and] H; clear H. eapply H4 with h1. split; auto. Disjoint_heap. Equal_heap. Qed. (* maps register contents to aligned heap-locations only *) Definition mapsto (e e':expr) : assert := fun s s' m h => exists p, u2Z (eval e s) = 4 * Z_of_nat p /\ h = heap.singleton p (eval e' s). Notation "e1 '|->' e2" := (mapsto e1 e2) (at level 80) : mips_scope. (* maps register contents to a set of aligned heap-locations *) Fixpoint mapstos (e:expr) (l:list (int 32)) {struct l} : assert := match l with nil => emp | e1::l1 => (e |-> int_e e1) ** (mapstos (add_e e (int_e four32)) l1) end. Notation "x '|-->' l" := (mapstos x l) (at level 80). End sep. Notation "P ** Q" := (sep.con P Q) (at level 80) : mips_scope. Notation "P -* Q" := (sep.imp P Q) (at level 80) : mips_scope. Notation "P ==> Q" := (sep.entails P Q) (at level 90, no associativity). Notation "P <==> Q" := (sep.equiv P Q) (at level 90, no associativity). Notation "e1 '|->' e2" := (sep.mapsto e1 e2) (at level 79) : mips_scope. Notation "x '|-->' l" := (sep.mapstos x l) (at level 80). Definition Nth idx (lst:list (int 32)) := nth idx lst zero32. Lemma monotony : forall (P1 P2 Q1 Q2:assert), forall s s' m h, ((forall h', P1 s s' m h' -> P2 s s' m h') /\ (forall h'', Q1 s s' m h'' -> Q2 s s' m h'')) -> ((P1 ** Q1) s s' m h -> (P2 ** Q2) s s' m h). intros. inversion_clear H0 as [h1]. inversion_clear H1 as [h2]. decompose [and] H0; clear H0. exists h1; exists h2. split. Disjoint_heap. split. Equal_heap. split; [apply (proj1 H); auto | apply (proj2 H); auto]. Qed. Lemma adjunction : forall (P1 P2 P3:assert), forall s s' m, (forall h, (P1 ** P2) s s' m h -> P3 s s' m h) -> (forall h, P1 s s' m h -> (P2 -* P3) s s' m h). intros. red; intros. apply H. inversion_clear H1. exists h; exists h'. split. Disjoint_heap. split. Equal_heap. auto. Qed. Lemma adjunction' : forall (P1 P2 P3:assert), forall s s' m, (forall h, P1 s s' m h -> (P2 -* P3) s s' m h) -> (forall h, (P1 ** P2) s s' m h -> P3 s s' m h). intros. inversion_clear H0. inversion_clear H1. decompose [and] H0; clear H0. generalize (H _ H2); intro. red in H0. apply (H0 _ (conj H1 H5)). auto. Qed. Lemma my_sep_trivial : forall P Q, P ** Q ==> P ** TT. intros. red; intros. red. inversion_clear H. exists x. inversion_clear H0. exists x0. repeat split; intuition. Qed. Definition strictly_exact (P:assert) := forall s s' m h h', P s s' m h /\ P s s' m h' -> h = h'. Lemma mp' : forall P Q, strictly_exact Q -> And P (Q ** TT) ==> Q ** ( Q -* P). red; intros. inversion_clear H0. inversion_clear H2. inversion_clear H0. decompose [and] H2; clear H2. exists x. exists x0. split; auto. split; auto. split; auto. red; intros. inversion_clear H2. generalize (H _ _ _ _ _ (conj H3 H8)); intro. subst x. assert (h = h''). rewrite H5; rewrite H4. rewrite heap.union_com; auto. rewrite <-H2. auto. Qed. Lemma pm : forall (P Q: assert), Q ==> (P -* (P ** Q)). red; intros. red. intros. inversion_clear H0. exists h'; exists h. split. apply heap.disjoint_com; auto. split. rewrite heap.union_com; auto. apply heap.disjoint_com; auto. split; auto. Qed. Definition Not (P:assert) : assert := fun s s' m h => ~(P s s' m h). Definition FF : assert := fun s s' m h => False. Lemma FF_is_not_TT : FF <==> Not TT. split; intros. red in H; tauto. red in H. apply H. red; auto. Qed. Lemma ex_falso : forall Q, FF ==> Q. red; intros. red in H. tauto. Qed. Lemma mapsto_ext_help : forall e e' x x', (forall s, eval e s = eval e' s /\ eval x s = eval x' s) -> (e' |-> x') ==> (e |-> x). red; intros. inversion_clear H0. exists x0. generalize (H s); intro X; inversion_clear X. rewrite H0; rewrite H2; auto. Qed. Lemma mapsto_ext : forall e e', (forall s, eval e s = eval e' s) -> forall x, (e' |-> x) ==> (e |-> x). intros; apply mapsto_ext_help; auto. Qed. Lemma mapstos_ext : forall lst e e', (forall s, eval e s = eval e' s) -> (e' |--> lst) ==> (e |--> lst). induction lst; intros. simpl. red; auto. simpl. red; intros. inversion_clear H0. exists x. inversion_clear H1. exists x0. split; try intuition. generalize H2. apply mapsto_ext_help. auto. generalize H4. apply IHlst. intros. simpl. rewrite (H s0); auto. Qed. Lemma mapsto_ext' : forall e e' x x' s, eval e s = eval e' s -> eval x s = eval x' s -> forall s' m h, (e' |-> x') s s' m h -> (e |-> x) s s' m h. destruct e; simpl; intros. inversion_clear H1. exists x0. simpl eval. rewrite H. rewrite H0. assumption. inversion_clear H1. exists x0. simpl eval. rewrite H. rewrite H0. assumption. inversion_clear H1. exists x0. simpl eval. rewrite H. rewrite H0. assumption. inversion_clear H1. exists x0. simpl eval. rewrite H. rewrite H0. assumption. Qed. Lemma mapstos_ext' : forall lst e e' s, eval e s = eval e' s -> forall s' m0 h, (e' |--> lst) s s' m0 h -> (e |--> lst) s s' m0 h. induction lst; intros. red; auto. destruct lst. simpl in H0. simpl. inversion_clear H0 as [h1]; exists h1. inversion_clear H1 as [h2]; exists h2. split; try intuition. generalize H2; apply mapsto_ext'; auto. simpl in H0. simpl. inversion_clear H0 as [h1]; exists h1. inversion_clear H1 as [h2]; exists h2. split; try intuition. generalize H2; apply mapsto_ext'; auto. generalize (IHlst (add_e e (int_e four32)) (add_e e' (int_e four32)) s); intro. assert (eval (add_e e (int_e four32)) s = eval (add_e e' (int_e four32)) s). simpl. rewrite H; auto. generalize (H3 H5 s' m0 h2); intro. simpl in H6. auto. Qed. Lemma mapsto_equiv' : forall s s' s0 m0 h e1 e2 e3 e4, (e1 |-> e2) s' s0 m0 h -> eval e1 s' = eval e3 s -> eval e2 s' = eval e4 s -> (e3 |-> e4) s s0 m0 h. intros. red in H. inversion_clear H. inversion_clear H2. red. exists x. rewrite <- H0. rewrite <- H1. auto. Qed. Lemma mapstos_equiv: forall l e e' s s2 s' m h, (e |--> l) s s' m h -> eval e s = eval e' s2 -> (e' |--> l) s2 s' m h. induction l; intros; auto. simpl. simpl in H. inversion_clear H. inversion_clear H1. exists x; exists x0. split; try tauto. split; try tauto. decompose [and] H; clear H. split. eapply mapsto_equiv'. apply H2. assumption. auto. eapply IHl. apply H5. simpl. rewrite H0. reflexivity. Qed. Lemma mapsto_ext_m : forall e e' s s' m m' h, (e |-> e') s s' m h -> (e |-> e') s s' m' h. intros. inversion_clear H. exists x. split; intuition. Qed. Lemma mapstos_ext_m : forall lst e s s' m m' h, (e |--> lst) s s' m h -> (e |--> lst) s s' m' h. induction lst. auto. intros. simpl in H. inversion_clear H as [h1]. inversion_clear H0 as [h2]. decompose [and] H; clear H. generalize (IHlst (add_e e (int_e four32)) s s' m m' h2 H4); intro. simpl. exists h1; exists h2; split; auto. Qed. (**************************************************************************** * axiomatic semantics ****************************************************************************) Definition update_store_addi rt rs imm (P: assert) : assert := fun s s' m h => (- 2^^31 <= s2Z (gpr.lookup rs s) + s2Z (sign_extend_16_32 imm) < 2^^31) -> (P (gpr.update rt (gpr.lookup rs s (+) sign_extend_16_32 imm) s) s' m h). Definition update_store_addiu rt rs imm P : assert := fun s s' m h => P (gpr.update rt (gpr.lookup rs s (+) sign_extend_16_32 imm) s) s' m h. Definition update_store_add rd rs rt (P: assert) : assert := fun s s' m h => (- 2^^31 <= s2Z (gpr.lookup rs s) + s2Z (gpr.lookup rt s) < 2^^31) -> P (gpr.update rd (gpr.lookup rs s (+) gpr.lookup rt s) s) s' m h. Definition update_store_addu rd rs rt P : assert := fun s s' m h => P (gpr.update rd (gpr.lookup rs s (+) gpr.lookup rt s) s) s' m h. Definition update_store_and rd rs num P : assert := fun s s' m h => P (gpr.update rd (int_and (gpr.lookup rs s) num) s) s' m h. Definition lw2 rt offset base P : assert := fun s1 s2 m h => exists p, u2Z (eval (var_e base) s1 (+) sign_extend_16_32 offset) = 4* Z_of_nat p /\ exists z, heap.lookup p h = Some z /\ P (gpr.update rt z s1) s2 m h. Definition lookup_heap_lwxs rt index base P : assert := fun s s' m h => exists l, u2Z (gpr.lookup base s (+) shl2 (gpr.lookup index s)) = 4 * Z_of_nat l /\ exists z, heap.lookup l h = Some z /\ P (gpr.update rt z s) s' m h. Definition update_heap2 rt offset base P : assert := fun s s' m h => exists l, u2Z (gpr.lookup base s (+) sign_extend_16_32 offset) = 4* Z_of_nat l /\ (exists z, heap.lookup l h = Some z) /\ P s s' m (heap.update l (gpr.lookup rt s) h). Definition update_store_mflhxu rd P : assert := fun s s' m h => P (gpr.update rd (multiplier.lo m) s) s' (multiplier.mflhxu_op m) h. Definition update_store_mfhi rd P : assert := fun s s' m h => P (gpr.update rd (multiplier.hi m) s) s' m h. Definition update_store_mflo rd P : assert := fun s s' m h => P (gpr.update rd (multiplier.lo m) s) s' m h. Definition update_store_mthi rs P : assert := fun s s' m h => P s s' (multiplier.mthi_op (gpr.lookup rs s) m) h. Definition update_store_mtlo rs P : assert := fun s s' m h => P s s' (multiplier.mtlo_op (gpr.lookup rs s) m) h. Definition update_store_nor rd rs rt P : assert := fun s s' m h => P (gpr.update rd (int_not (int_or (gpr.lookup rs s) (gpr.lookup rt s))) s) s' m h. Definition update_store_sll rx ry (sa: int 5) P : assert := fun s s' m h => P (gpr.update rx (shl (nat_of_Z (u2Z sa)) (gpr.lookup ry s)) s) s' m h. Definition update_store_sltu rd rs rt P : assert := fun s s' m h => P (gpr.update rd (if (Zlt_bool (u2Z (gpr.lookup rs s)) (u2Z (gpr.lookup rt s))) then one32 else zero32) s) s' m h. (*TODO: for some reason, i cannot use the intended notation in the def of the inductive type... *) Reserved Notation "'{[' p ']}' c '{[' q ']}'" (at level 82, no associativity). Inductive semax : assert -> cmd -> assert -> Prop := | semax_skip: forall P, {[ P ]} skip {[ P ]} | semax_addi : forall P rt rs imm, {[ update_store_addi rt rs imm P ]} addi rt rs imm {[ P ]} | semax_addiu : forall P rt rs imm, {[ update_store_addiu rt rs imm P ]} addiu rt rs imm {[ P ]} | semax_add: forall Q rs rt rd, {[ update_store_add rd rs rt Q ]} add rd rs rt {[ Q ]} | semax_addu: forall Q rs rt rd , {[ update_store_addu rd rs rt Q ]} addu rd rs rt {[ Q ]} | semax_and: forall Q rs rd imm, {[ update_store_and rd rs imm Q ]} cmd_and rd rs imm {[ Q ]} | semax_lw : forall P rt offset base, {[ lw2 rt offset base P ]} lw rt offset base {[ P ]} | semax_lwxs : forall rt index base P, {[ lookup_heap_lwxs rt index base P ]} lwxs rt index base {[ P ]} | semax_maddu : forall Q rs rt, {[ fun s s' m h => Q s s' (multiplier.maddu_op (umul (gpr.lookup rs s) (gpr.lookup rt s)) m) h ]} maddu rs rt {[ Q ]} | semax_mflhxu : forall rd P, {[ update_store_mflhxu rd P ]} mflhxu rd {[ P ]} | semax_mfhi : forall Q rd, {[ update_store_mfhi rd Q ]} mfhi rd {[ Q ]} | semax_mflo : forall Q rd, {[ update_store_mflo rd Q ]} mflo rd {[ Q ]} | semax_mthi : forall Q rs, {[ update_store_mthi rs Q ]} mthi rs {[ Q ]} | semax_mtlo : forall Q rs, {[ update_store_mtlo rs Q ]} mtlo rs {[ Q ]} | semax_multu : forall Q rs rt, {[ fun s s' m h => Q s s' (multiplier.multu_op (umul (gpr.lookup rs s) (gpr.lookup rt s)) m) h ]} multu rs rt {[ Q ]} | semax_msubu : forall Q rs rt, {[fun s s' m h => Q s s' (multiplier.msubu_op (umul (gpr.lookup rs s) (gpr.lookup rt s)) m) h ]} msubu rs rt {[Q]} | semax_nor : forall Q rd rs rt, {[ update_store_nor rd rs rt Q ]} nor rd rs rt {[ Q ]} | semax_sll : forall Q rx ry sa, {[ update_store_sll rx ry sa Q ]} sll rx ry sa {[ Q ]} | semax_sltu : forall Q rd rs rt, {[ update_store_sltu rd rs rt Q ]} sltu rd rs rt {[ Q ]} | semax_sw : forall rt offset base (P:assert), {[ update_heap2 rt offset base P ]} sw rt offset base {[ P ]} | semax_seq : forall P Q R c d, {[ P ]} c {[ Q ]} -> {[ Q ]} d {[ R ]} -> {[ P ]} c ; d {[ R ]} | semax_conseq : forall (P P' Q Q':assert) c, (Q' ==> Q) -> (P ==> P') -> {[ P' ]} c {[ Q' ]} -> {[ P ]} c {[ Q ]} | semax_while_bne : forall P r r' c, {[ fun s s' m h => P s s' m h /\ ~ (u2Z (gpr.lookup r s) = u2Z (gpr.lookup r' s)) ]} c {[ P ]} -> {[ P ]} while_bne r r' c {[ fun s s' m h => P s s' m h /\ u2Z (gpr.lookup r s) = u2Z (gpr.lookup r' s) ]} | semax_ifte_beq : forall P Q r1 r2 c d, {[ fun s1 s2 m h => P s1 s2 m h /\ gpr.lookup r1 s1 = gpr.lookup r2 s1 ]} c {[ Q ]} -> {[ fun s1 s2 m h => P s1 s2 m h /\ gpr.lookup r1 s1 <> gpr.lookup r2 s1 ]} d {[ Q ]} -> {[ P ]} ifte_beq r1, r2 thendo c elsedo d {[ Q ]} | semax_ifte_bltz : forall P Q r1 c d, {[ fun s1 s2 m h => P s1 s2 m h /\ s2Z (gpr.lookup r1 s1) < 0 ]} c {[ Q ]} -> {[ fun s1 s2 m h => P s1 s2 m h /\ s2Z (gpr.lookup r1 s1) >= 0 ]} d {[ Q ]} -> {[ P ]} ifte_bltz r1 thendo c elsedo d {[ Q ]} where "'{[' p ']}' c '{[' q ']}'" := (semax p c q) : tmp_scope. Notation "'{{' p '}}' c '{{' q '}}'" := (semax p c q) (at level 82, no associativity) : mips_scope. Lemma semax_strengthen_pre : forall (P P' Q:assert) c, (P ==> P') -> {{ P' }} c {{ Q }} -> {{ P }} c {{ Q }}. intros. eapply semax_conseq with P' Q; try assumption. red; auto. Qed. Lemma semax_weaken_post : forall (P Q Q':assert) c, (Q' ==> Q) -> {{ P }} c {{ Q' }} -> {{ P }} c {{ Q }}. intros. eapply semax_conseq with P Q'; try assumption. red; auto. Qed. Definition semax' (P:assert) (c:cmd) (Q:assert) : Prop := forall s1 s2 m h, (P s1 s2 m h -> ~(Some (s1,s2,m,h) -- c --> None)) /\ (forall s1' s2' m' h', P s1 s2 m h -> (Some (s1,s2,m,h) -- c --> Some (s1',s2',m',h')) -> Q s1' s2' m' h'). Lemma semax_sound : forall P Q c, {{ P }} c {{ Q }} -> semax' P c Q. intros. induction H. (* case skip *) split; intros. intro X; inversion_clear X. inversion H0. subst s1' s2' m' h'. assumption. (* case addi *) red; intros. split; intros. intro. inversion H0. inversion H0. subst s0 s3 m0 h0 rt0 rs0 imm0 s1' s2' m' h'. red in H. rewrite <- H3. apply H. rewrite H3. auto. (* case addiu *) red; intros. split; intros. intro. inversion H0. inversion H0. subst s0 s3 m0 h0 rt0 rs0 imm0 s2' m' h'. red in H. rewrite H2 in H. assumption. (* case add *) red; intros. split; intros. intro. inversion H0. inversion H0. subst s0 s3 m0 h0 rd0 rs0 rt0 s1' s2' m' h'. red in H. rewrite <-H4. rewrite <-H13. apply H. rewrite H4. rewrite H13. rewrite Zplus_comm. auto. (* case addu *) red; intros. split; intros. intro. inversion H0. inversion H0. subst s0 s3 m0 h0 rd0 rs0 rt0 s1' s2' m' h'. red in H. rewrite H13 in H. rewrite H3 in H. assumption. (* case and *) red; intros. split; intros. intro. inversion H0. inversion H0. subst s0 s3 m0 h0 rt rs0 imm s1' s2' m' h'. red in H. rewrite <- H2; auto. (* case lw *) red; intros. split; intros. intro X; inversion_clear X. red in H. inversion_clear H as [p]. inversion_clear H2. simpl eval in H. inversion_clear H3 as [z]. inversion_clear H2. subst vbase. apply H1. exists p. split; auto. exists z; auto. red in H. inversion_clear H as [p]. inversion_clear H1. inversion_clear H2 as [z]. inversion_clear H1. inversion H0. subst vbase s0 s3 m0 h0 rt0 offset0 base0 s1' s2' m' h'. simpl eval in H. rewrite H in H15. assert (p=l). omega. clear H15; subst l. rewrite H2 in H16; injection H16; clear H16; intro; subst z0. assumption. (* case lwxs *) red; intros. split; intros. intro X; inversion_clear X. red in H. inversion_clear H as [p]. inversion_clear H3. subst vbase. subst vindex. inversion_clear H4 as [x]. inversion_clear H0. apply H2. exists p; split; auto. exists x; auto. red in H. inversion_clear H as [p]. inversion_clear H1. inversion_clear H2 as [z]. inversion_clear H1. inversion H0. subst vbase vindex s0 s3 m0 h0 rt0 index0 base0 s1' s2' m' h'. unfold shl2 in H. rewrite H in H16. assert (p=l). omega. clear H16; subst l. rewrite H2 in H17; injection H17; clear H17; intro; subst z0. assumption. (* case maddu *) red; intros. split; intros. intro X; inversion_clear X. inversion H0. subst vrt vrs s0 s3 m0 h0 rs0 rt0 s1' s2' m' h'. assumption. (* case mflhxu *) red; intros. split; intros. intro X; inversion_clear X. inversion H0. subst s0 s3 m0 h0 rd0 s1' s2' m' h'. assumption. (* case mfhi *) red; intros. split; intros. intro X; inversion_clear X. inversion H0. subst s0 s3 m0 h0 rd0 s1' s2' m' h'. assumption. (* case mflo *) red; intros. split; intros. intro X; inversion_clear X. inversion H0. subst s0 s3 m0 h0 rd0 s1' s2' m' h'. assumption. (* case mthi *) red; intros. split; intros. intro X; inversion_clear X. inversion H0. subst s0 s3 m0 h0 rs0 s1' s2' m' h'. red in H. rewrite H2 in H. assumption. (* case mtlo *) red; intros. split; intros. intro X; inversion_clear X. inversion H0. subst s0 s3 m0 h0 rs0 s1' s2' m' h'. red in H. rewrite H2 in H. assumption. (* case multu *) red; intros. split; intros. intro X; inversion_clear X. inversion H0. subst vrt vrs s0 s3 m0 h0 rs0 rt0 s1' s2' m' h'. assumption. (* case msubu *) red; intros. split; intros. intro X; inversion_clear X. inversion H0. subst vrt vrs s0 s3 m0 h0 rs0 rt0 s1' s2' m' h'. assumption. (* case nor *) red; intros. split; intros. intro X; inversion_clear X. inversion H0. subst vrt vrs rd s0 s3 m0 h0 rs0 rt0 s1' s2' m' h'. assumption. (* case sll *) red; intros. split; intros. intro X; inversion_clear X. inversion H0. red in H. subst s1' s2' m' h'. assumption. (* case sltu *) red; intros. split; intros. intro X; inversion_clear X. inversion H0. red in H. subst s1' s2' m' h'. rewrite H2. assumption. (* case sw *) red; intros. split; intros. intro X; inversion_clear X. red in H. inversion_clear H as [l']. inversion_clear H3. subst vbase. apply H2. exists l'; split; auto. apply (proj1 H4). red in H. inversion_clear H as [l']. inversion_clear H1. inversion H0. subst vbase vrt s0 s3 m0 h0 rt0 offset0 base0 s1' s2' m' h'. rewrite H in H15. assert (l'=l). omega. clear H15; subst l'. inversion_clear H2. assumption. (* case seq *) red; intros. split; intros. intro. inversion H2. subst s c0 d0 s''. red in IHsemax1. generalize (IHsemax1 s1 s2 m h); intro. inversion_clear H3. destruct s'. destruct s as [X h']. destruct X as [Y m']. destruct Y as [s1' s2']. generalize (H5 _ _ _ _ H1 H6); intro. generalize (IHsemax2 s1' s2' m' h'); intro. inversion_clear H7. tauto. tauto. inversion H2. subst s c0 d0 s''. red in IHsemax1. red in IHsemax2. destruct s'. destruct s as [X h'']. destruct X as [Y m'']. destruct Y as [s1'' s2'']. generalize (IHsemax1 s1 s2 m h); intro. inversion_clear H3. generalize (H5 _ _ _ _ H1 H6); intro. generalize (IHsemax2 s1'' s2'' m'' h''); intro. inversion_clear H7. apply H10; auto. generalize (from_none _ _ H8); intro. discriminate. (* case conseq *) red; intros. split; intros. intro. generalize (IHsemax s1 s2 m h); intro. inversion_clear H4. assert (P' s1 s2 m h). apply H0; auto. generalize (H5 H4); clear H4; intro. tauto. generalize (IHsemax s1 s2 m h); intro. inversion_clear H4. apply H. apply H6; auto. (* case while *) red; intros. split; intros. intro. assert (exists d, d = while_bne r r' c). exists (while_bne r r' c); auto. inversion_clear H2 as [d]. rewrite <-H3 in H1. assert (exists S, S = Some (s1,s2,m,h)). exists (Some (s1,s2,m,h)); reflexivity. inversion_clear H2 as [S]. rewrite <-H4 in H1. generalize P r r' c H IHsemax s1 s2 m h H0 H3 H4; clear P r r' c H IHsemax s1 s2 m h H0 H3 H4. assert (exists S, S = @None state). exists (@None state); reflexivity. inversion_clear H as [S']. rewrite <-H0 in H1. generalize H0; clear H0. induction H1; intros; try discriminate. injection H4; clear H4; intros; subst s0 s3 m0 h0. injection H3; clear H3; intros; subst r1 r2 c0. red in IHsemax. generalize (IHsemax s1 s2 m h); intro. inversion_clear H3. simpl in H. generalize (H4 (conj H2 H)); clear H4; intro. destruct s'. destruct s as [X h']. destruct X as [Y m']. destruct Y as [s1' s2']. generalize (H5 s1' s2' m' h' (conj H2 H) H1_); clear H5; intro. generalize (IHexec2 H0 _ _ _ _ H1 IHsemax _ _ _ _ H4). auto. tauto. assert (exists d, d = while_bne r r' c). exists (while_bne r r' c); reflexivity. inversion_clear H2 as [C]. rewrite <-H3 in H1. assert (exists S, S = Some (s1,s2,m,h)). exists (Some (s1,s2,m,h)); reflexivity. inversion_clear H2 as [sigma]. rewrite <-H4 in H1. assert (exists S, S = Some (s1',s2',m',h')). exists (Some (s1',s2',m',h')); reflexivity. inversion_clear H2 as [sigma']. rewrite <-H5 in H1. generalize P r r' c H IHsemax s1 s2 m h s1' s2' m' h' H0 H3 H4 H5; clear P r r' c H IHsemax s1 s2 m h s1' s2' m' h' H0 H3 H4 H5. induction H1; intros; try discriminate. (* * case exec_while_bne true *) injection H3; clear H3; intros; subst c0 r1 r2. injection H4; clear H4; intros; subst s0 s3 m0 h0. clear IHexec1. rename s'' into sigma'. rename s' into sigma''. (* we know s1,s2,m,h |= P /\ r<>r', by the inductive hypothesis IHsemax we have sigma'' |= P *) induction sigma''. destruct a as [X h'']. destruct X as [Y m'']. destruct Y as [s1'' s2'']. assert (P s1'' s2'' m'' h''). red in IHsemax. generalize (IHsemax s1 s2 m h); intro. inversion_clear H2. apply H4; auto. (* since sigma'' --while_bne r r' c--> sigma' and {P}while_bne r r' c{P /\ r=r'}, then we have sigma' |= P /\ ~b *) generalize (IHexec2 _ _ _ _ H0 IHsemax _ _ _ _ s1' s2' m' h' H2 (refl_equal (while_bne r r' c)) (refl_equal (Some (s1'',s2'',m'', h'')))); intro. auto. generalize (from_none _ _ H1_0); intro X; rewrite H5 in X; discriminate X. (* * case exec_while false *) intros. injection H5; clear H5; intros; subst s1' s2' m' h'. injection H4; clear H4; intros; subst s0 s3 m0 h0. injection H3; clear H3; intros; subst r1 r2 c0. auto. (* * ifte_beq *) red. intros. cut ( gpr.lookup r1 s1 = gpr.lookup r2 s1 \/ gpr.lookup r1 s1 <> gpr.lookup r2 s1 ). split; intros. intro. inversion_clear H3. red in IHsemax1. generalize (IHsemax1 s1 s2 m h); intro. inversion_clear H3. apply H6. auto. auto. generalize (IHsemax2 s1 s2 m h); intro. inversion_clear H3. apply H6. auto. auto. inversion_clear H3. red in IHsemax1. generalize (IHsemax1 s1 s2 m h); intro. inversion_clear H3. apply H7. auto. auto. red in IHsemax2. generalize (IHsemax2 s1 s2 m h); intro. inversion_clear H3. apply H7. auto. auto. generalize (dec_equ_fin_int (gpr.lookup r1 s1) (gpr.lookup r2 s1)); intro. inversion_clear H1; auto. (* * ifte_bltz *) red. intros. cut (s2Z (gpr.lookup r1 s1) < 0 \/ s2Z (gpr.lookup r1 s1) >= 0). split; intros. intro. inversion_clear H3. red in IHsemax1. generalize (IHsemax1 s1 s2 m h); intro. inversion_clear H3. apply H6. auto. auto. generalize (IHsemax2 s1 s2 m h); intro. inversion_clear H3. apply H6. auto. auto. inversion_clear H3. red in IHsemax1. generalize (IHsemax1 s1 s2 m h); intro. inversion_clear H3. apply H7. auto. auto. red in IHsemax2. generalize (IHsemax2 s1 s2 m h); intro. inversion_clear H3. apply H7. auto. auto. omega. Qed. Definition wp_semantics (c: cmd) (Q: assert): assert := fun s1 s2 m h => ~ ((Some (s1,s2,m,h)) -- c --> None) /\ forall s1' s2' m' h', (Some (s1,s2,m,h)) -- c --> (Some (s1',s2',m', h')) -> Q s1' s2' m' h'. Require Import Classical. Lemma exec_lw_not_None: forall s s' m h g i g0 , ~ (Some (s,s',m,h) -- lw g i g0 --> None) -> exists p : nat, u2Z (eval (var_e g0) s(+)sign_extend_16_32 i) = 4 * Z_of_nat p /\ (exists z : heap.v, heap.lookup p h = Some z). intros. match goal with | |- ?P => generalize (classic P); let x := fresh in (intro x; inversion_clear x) end. auto. assert (Some (s, s', m, h) -- lw g i g0 --> None). eapply exec_lw_error. intuition. auto. contradiction. Qed. Lemma exec_lwxs_not_None: forall s s' m h g g0 g1, ~ (Some (s,s',m,h) -- lwxs g g0 g1 --> None) -> exists p : nat, u2Z (gpr.lookup g1 s(+)shl2 (gpr.lookup g0 s)) = 4 * Z_of_nat p /\ (exists z : heap.v, heap.lookup p h = Some z). intros. match goal with | |- ?P => generalize (classic P); let x := fresh in (intro x; inversion_clear x) end. auto. assert (Some (s, s', m, h) -- lwxs g g0 g1 --> None). eapply exec_lwxs_error. intuition. intuition. auto. contradiction. Qed. Lemma exec_sw_not_None: forall s s' m h g i g0 , ~ (Some (s,s',m,h) -- sw g i g0 --> None) -> exists p : nat, u2Z (eval (var_e g0) s(+)sign_extend_16_32 i) = 4 * Z_of_nat p /\ (exists z : heap.v, heap.lookup p h = Some z). intros. match goal with | |- ?P => generalize (classic P); let x := fresh in (intro x; inversion_clear x) end. auto. assert (Some (s, s', m, h) -- sw g i g0 --> None). eapply exec_sw_err. intuition. intuition. auto. contradiction. Qed. Lemma exec_seq1_not_None: forall s s' m h c1 c2, ~ (Some (s,s',m,h) -- (c1; c2) --> None) -> ~ (Some (s,s',m,h) -- c1 --> None). intros. red; intros. assert (Some (s,s',m, h) -- c1; c2 --> None). eapply exec_seq. apply H0. apply exec_none. tauto. Qed. Lemma exec_seq2_not_None: forall s1 s2 m h s1' s2' m' h' c1 c2, ~ (Some (s1,s2,m,h) -- (c1; c2) --> None) -> Some (s1,s2,m,h) -- c1 --> Some (s1',s2',m',h') -> ~ (Some (s1',s2',m',h') -- c2 --> None). intros. red; intros. assert (Some (s1,s2,m, h) -- c1; c2 --> None). eapply exec_seq. apply H0. auto. tauto. Qed. Lemma exec_ifte_beq1_not_None: forall s s' m h c1 c2 g g0, ~ (Some (s,s',m,h) -- (ifte_beq g, g0 thendo c1 elsedo c2) --> None) -> gpr.lookup g s = gpr.lookup g0 s -> (~ (Some (s,s',m,h) -- c1 --> None)). intros. red; intros. assert (Some (s,s',m,h) -- (ifte_beq g, g0 thendo c1 elsedo c2) --> None). eapply exec_ifte_beq_true; auto. tauto. Qed. Lemma exec_ifte_beq2_not_None: forall s s' m h c1 c2 g g0, ~ (Some (s,s',m,h) -- (ifte_beq g, g0 thendo c1 elsedo c2) --> None) -> gpr.lookup g s <> gpr.lookup g0 s -> (~ (Some (s,s',m,h) -- c2 --> None)). intros. red; intros. assert (Some (s,s',m,h) -- (ifte_beq g, g0 thendo c1 elsedo c2) --> None). eapply exec_ifte_beq_false; auto. tauto. Qed. Lemma exec_ifte_bltz1_not_None: forall s s' m h c1 c2 g, ~ (Some (s,s',m,h) -- (ifte_bltz g thendo c1 elsedo c2) --> None) -> s2Z (gpr.lookup g s) < 0 -> (~ (Some (s,s',m,h) -- c1 --> None)). intros. red; intros. assert (Some (s,s',m,h) -- (ifte_bltz g thendo c1 elsedo c2) --> None). eapply exec_ifte_bltz_true; auto. tauto. Qed. Lemma exec_ifte_bltz2_not_None: forall s s' m h c1 c2 g, ~ (Some (s,s',m,h) -- (ifte_bltz g thendo c1 elsedo c2) --> None) -> s2Z (gpr.lookup g s) >= 0 -> (~ (Some (s,s',m,h) -- c2 --> None)). intros. red; intros. assert (Some (s,s',m,h) -- (ifte_bltz g thendo c1 elsedo c2) --> None). eapply exec_ifte_bltz_false; auto. tauto. Qed. Lemma exec_while_bne1_not_None: forall s s' m h g g0 c, ~ (Some (s,s',m,h) -- while_bne g g0 c --> None) -> u2Z (gpr.lookup g s) <> u2Z (gpr.lookup g0 s) -> ~ (Some (s,s',m,h) -- c --> None). intros. red; intros. assert (Some (s,s',m,h) -- while_bne g g0 c --> None). eapply exec_while_bne_true. auto. apply H1. apply exec_none. tauto. Qed. Lemma exec_while_bne2_not_None: forall s s' m h g g0 c s0 s0' m0 h0, ~ (Some (s,s',m,h) -- while_bne g g0 c --> None) -> u2Z (gpr.lookup g s) <> u2Z (gpr.lookup g0 s) -> (Some (s,s',m,h) -- c --> Some (s0,s0',m0,h0)) -> ~ (Some (s0,s0',m0,h0) -- while_bne g g0 c --> None). intros. red; intros. assert (Some (s,s',m,h) -- while_bne g g0 c --> None). eapply exec_while_bne_true with (Some (s0, s0', m0, h0)). auto. eapply H1. auto. tauto. Qed. Lemma wp_semantics_sound: forall c Q, {{wp_semantics c Q}} c {{Q}}. induction c; intros. (* skip *) eapply semax_strengthen_pre; [idtac | constructor]. red; intros. red in H. apply (proj2 H). apply exec_skip. (* add *) eapply semax_strengthen_pre; [idtac | constructor]. red; intros. inversion_clear H. red. intros. apply H1. constructor; auto. rewrite Zplus_comm; auto. (* addi *) eapply semax_strengthen_pre; [idtac | constructor]. red; intros. inversion_clear H. red. intros. apply H1. constructor; auto. (* addiu *) eapply semax_strengthen_pre; [idtac | constructor]. red; intros. inversion_clear H. red. intros. apply H1. constructor; auto. (* addu *) eapply semax_strengthen_pre; [idtac | constructor]. red; intros. inversion_clear H. red. apply H1. constructor; auto. (* cmd_add *) eapply semax_strengthen_pre; [idtac | constructor]. red; intros. inversion_clear H. red. apply H1. constructor; auto. (* lw *) eapply semax_strengthen_pre; [idtac | constructor]. red; intros. inversion_clear H. red. generalize (exec_lw_not_None _ _ _ _ _ _ _ H0); intros. inversion_clear H. inversion_clear H2. inversion_clear H3. exists x. split; auto. exists x0; split; auto. apply H1. eapply exec_lw. intuition. simpl eval in H; apply H. auto. (* lwxs *) eapply semax_strengthen_pre; [idtac | constructor]. red; intros. inversion_clear H. red. generalize (exec_lwxs_not_None _ _ _ _ _ _ _ H0); intros. inversion_clear H. inversion_clear H2. inversion_clear H3. exists x. split; auto. exists x0; split; auto. apply H1. eapply exec_lwxs. intuition. intuition. simpl eval in H; apply H. auto. (* maddu *) eapply semax_strengthen_pre; [idtac | constructor]. red; intros. inversion_clear H. eapply H1. constructor; auto. (* mflhxu *) eapply semax_strengthen_pre; [idtac | constructor]. red; intros. inversion_clear H. red. eapply H1. constructor; auto. (* mflo *) eapply semax_strengthen_pre; [idtac | constructor]. red; intros. inversion_clear H. red. eapply H1. constructor; auto. (* mfhi *) eapply semax_strengthen_pre; [idtac | constructor]. red; intros. inversion_clear H. red. eapply H1. constructor; auto. (* mtlo *) eapply semax_strengthen_pre; [idtac | constructor]. red; intros. inversion_clear H. red. eapply H1. constructor; auto. (* mtlhi *) eapply semax_strengthen_pre; [idtac | constructor]. red; intros. inversion_clear H. red. eapply H1. constructor; auto. (* msubu *) eapply semax_strengthen_pre; [idtac | constructor]. red; intros. inversion_clear H. eapply H1. constructor; auto. (* multu *) eapply semax_strengthen_pre; [idtac | constructor]. red; intros. inversion_clear H. eapply H1. constructor; auto. (* nor *) eapply semax_strengthen_pre; [idtac | constructor]. red; intros. inversion_clear H. red. eapply H1. constructor; auto. (* sll *) eapply semax_strengthen_pre; [idtac | constructor]. red; intros. inversion_clear H. red. eapply H1. constructor; auto. (* sltu *) eapply semax_strengthen_pre; [idtac | constructor]. red; intros. inversion_clear H. red. eapply H1. constructor; auto. (* sw *) eapply semax_strengthen_pre; [idtac | constructor]. red; intros. inversion_clear H. red. generalize (exec_sw_not_None _ _ _ _ _ _ _ H0); intros. inversion_clear H. inversion_clear H2. inversion_clear H3. exists x. split; auto. split. exists x0; auto. apply H1. eapply exec_sw. intuition. auto. simpl eval in H; apply H. auto. exists x0; auto. (* seq *) eapply semax_strengthen_pre with ( wp_semantics c1 (wp_semantics c2 Q) ). red; intros. red in H. inversion_clear H. red; split. eapply exec_seq1_not_None. apply H0. intros. red; split. eapply exec_seq2_not_None. apply H0. auto. intros. eapply H1. eapply exec_seq. apply H. auto. eapply semax_seq; [apply IHc1 | apply IHc2]. (* ifte_beq *) eapply semax_ifte_beq. eapply semax_strengthen_pre; [idtac | eapply IHc1]. red; intros. inversion_clear H. red; red in H0. inversion_clear H0. split. eapply exec_ifte_beq1_not_None. apply H. tauto. intros. apply H2. eapply exec_ifte_beq_true. auto. auto. eapply semax_strengthen_pre; [idtac | eapply IHc2]. red; intros. inversion_clear H. red; red in H0. inversion_clear H0. split. eapply exec_ifte_beq2_not_None. apply H. tauto. intros. apply H2. eapply exec_ifte_beq_false. auto. auto. (* ifte_bltz *) eapply semax_ifte_bltz. eapply semax_strengthen_pre; [idtac | eapply IHc1]. red; intros. inversion_clear H. red; red in H0. inversion_clear H0. split. eapply exec_ifte_bltz1_not_None. apply H. tauto. intros. apply H2. eapply exec_ifte_bltz_true. auto. auto. eapply semax_strengthen_pre; [idtac | eapply IHc2]. red; intros. inversion_clear H. red; red in H0. inversion_clear H0. split. eapply exec_ifte_bltz2_not_None. apply H. tauto. intros. apply H2. eapply exec_ifte_bltz_false. auto. auto. (* while_bne *) eapply semax_weaken_post with (fun s s' m h' => (wp_semantics (while_bne g g0 c) Q) s s' m h' /\ u2Z (gpr.lookup g s) = u2Z (gpr.lookup g0 s)). red; intros. inversion_clear H. red in H0. inversion_clear H0. eapply H2. eapply exec_while_bne_false. auto. eapply semax_while_bne. eapply semax_strengthen_pre with (wp_semantics c (wp_semantics (while_bne g g0 c) Q)). red; intros. inversion_clear H. red. red in H0. inversion_clear H0. split. eapply exec_while_bne1_not_None. apply H. auto. intros. red. split. eapply exec_while_bne2_not_None. apply H. auto. auto. intros. apply H2. eapply exec_while_bne_true. auto. apply H0. auto. apply IHc. Qed. Lemma semax_complete : forall P Q c, semax' P c Q -> {{ P }} c {{ Q }}. intros. eapply semax_strengthen_pre; [idtac | apply wp_semantics_sound]. red; intros. red. red in H. generalize (H s s' m h); clear H; intros. inversion_clear H. split. apply (H1 H0). intros. apply H2; auto. Qed. Fixpoint modified_cmd_var (c:cmd) {struct c} : list gpr.var := match c with skip => nil | addi rt rs imm => rt::nil | addiu rt rs imm => rt::nil | addu rd rs rt => rd::nil | add rd _ _ => rd::nil | cmd_and rd rs rt => rd::nil | lw rt offset base => rt::nil | lwxs rt _ _ => rt::nil | maddu rs rt => nil | mflo rd => rd::nil | mfhi rd => rd::nil | mflhxu rd => rd::nil | msubu a b => nil | mthi _ => nil | mtlo _ => nil | multu a b => nil (* | mfc0 rt rd => rt::nil | mtc0 rt rd => nil *) | nor rd rs rt => rd::nil | sll rx ry sa => rx::nil | sltu rd rs rt => rd::nil (* | sub rd _ _ => rd::nil | subu rd rs rt => rd::nil *) | sw rt offset base => nil | while_bne r r' c => modified_cmd_var c | c1 ; c2 => modified_cmd_var c1 ++ modified_cmd_var c2 | ifte_beq r1, r2 thendo c1 elsedo c2 => modified_cmd_var c1 ++ modified_cmd_var c2 | ifte_bltz r1 thendo c1 elsedo c2 => modified_cmd_var c1 ++ modified_cmd_var c2 end. (* TODO: inde w.r.t cp0 registers (?) *) Definition inde l (P:assert) := forall s s' h m, (forall x v, In x l -> (P s s' m h <-> P (gpr.update x v s) s' m h)). Fixpoint modifies_mult (c:cmd) : Prop := match c with skip => False | addi _ _ _ => False | addiu _ _ _ => False | addu _ _ _ => False | add _ _ _ => False | cmd_and _ _ _ => False | lw _ _ _ => False | lwxs _ _ _ => False | maddu _ _ => True | mflhxu _ => True | mflo _ => False | mfhi _ => False | mtlo _ => True | mthi _ => True | msubu _ _ => True | multu _ _ => True (* | mfc0 _ _ => False | mtc0 _ _ => False *) | nor _ _ _ => False | sll _ _ _ => False | sltu _ _ _ => False | sw _ _ _ => False (* | sub _ _ _ => False | subu _ _ _ => False *) | while_bne _ _ c' => modifies_mult c' | seq c1 c2 => modifies_mult c1 \/ modifies_mult c2 | ifte_beq r1, r2 thendo c1 elsedo c2 => modifies_mult c1 \/ modifies_mult c2 | ifte_bltz r1 thendo c1 elsedo c2 => modifies_mult c1 \/ modifies_mult c2 end. (* an assert is independent of the execution of a command modifying the multipler *) Definition inde_cmd_mult c (P:assert) := forall s s' h m, (modifies_mult c -> forall m', (P s s' m h <-> P s s' m' h)). Lemma inde_update_store : forall (P:assert) x z s s' m h, inde (x::nil) P -> P s s' m h -> P (gpr.update x z s) s' m h. intros. red in H. lapply (H s s' h m x z). tauto. simpl; auto. Qed. Lemma inde_sep_con : forall l (P Q:assert), inde l P -> inde l Q -> inde l (P ** Q). split; intros. inversion_clear H2 as [h1]. inversion_clear H3 as [h2]. decompose [and] H2; clear H2. exists h1; exists h2. split; auto. split; auto. split. generalize (H s s' h1 m x v H1); tauto. generalize (H0 s s' h2 m x v H1); tauto. inversion_clear H2 as [h1]. inversion_clear H3 as [h2]. decompose [and] H2; clear H2. exists h1; exists h2. split; auto. split; auto. split. generalize (H s s' h1 m x v H1); tauto. generalize (H0 s s' h2 m x v H1); tauto. Qed. Fixpoint expr_free_vars (e:expr) {struct e} : list gp_reg := match e with var_e x => x::nil | int_e _ => nil | add_e e1 e2 => expr_free_vars e1 ++ expr_free_vars e2 | shl2_e e' => expr_free_vars e' end. Lemma inde_expr : forall e x, ~In x (expr_free_vars e) -> forall s v, eval e s = eval e (gpr.update x v s). induction e; simpl; intros; auto. elim gpr.lookup_update; auto. rewrite <-IHe1. rewrite <-IHe2. auto. intro. apply H. apply in_or_app. auto. intro. apply H. apply in_or_app. auto. rewrite <-IHe. auto. auto. Qed. Lemma inde_mapsto_expr : forall e l v, inter (expr_free_vars e) l nil -> inde l (e |-> int_e v). induction e; simpl; intros. red in H. split; intros. eapply mapsto_equiv'. apply H1. simpl. elim gpr.lookup_update; auto. intro. subst g. generalize (H x); simpl; tauto. reflexivity. eapply mapsto_equiv'. apply H1. simpl. elim gpr.lookup_update; auto. intro. subst g. generalize (H x); simpl; tauto. reflexivity. split; intros. eapply mapsto_equiv'. apply H1. auto. auto. eapply mapsto_equiv'. apply H1. auto. auto. split; intros. eapply mapsto_equiv'. apply H1. simpl. rewrite <-inde_expr. rewrite <-inde_expr. auto. intro. generalize (inter_app _ _ _ _ H); intro. inversion_clear H3. generalize (H5 x); tauto. intro. generalize (inter_app _ _ _ _ H); intro. inversion_clear H3. generalize (H4 x); tauto. auto. eapply mapsto_equiv'. apply H1. simpl. rewrite <-inde_expr. rewrite <-inde_expr. auto. intro. generalize (inter_app _ _ _ _ H); intro. inversion_clear H3. generalize (H5 x); tauto. intro. generalize (inter_app _ _ _ _ H); intro. inversion_clear H3. generalize (H4 x); tauto. auto. split; intros. eapply mapsto_equiv'. apply H1. simpl. rewrite <-inde_expr. auto. intro. generalize (H x); tauto. auto. eapply mapsto_equiv'. apply H1. simpl. rewrite <-inde_expr. auto. intro. generalize (H x); tauto. auto. Qed. Lemma inde_mapsto : forall l a v, ~In a l -> inde l (var_e a |-> int_e v). intros. apply inde_mapsto_expr. simpl. split; intros. simpl in H0. inversion_clear H0. inversion_clear H1. subst x. tauto. tauto. simpl in H0. tauto. Qed. Lemma inde_mapstos_expr : forall v l e, inter (expr_free_vars e) l nil -> inde l (e |--> v). induction v. red; simpl; tauto. simpl; intros. assert (inter (expr_free_vars (add_e e (int_e four32))) l nil). simpl. rewrite <-app_nil_end. auto. generalize (IHv l (add_e e (int_e four32)) H0); intro. split; intros. inversion_clear H3 as [h1]. inversion_clear H4 as [h2]. decompose [and] H3; clear H3. exists h1; exists h2. split; auto. split; auto. split. eapply mapsto_equiv'. apply H5. rewrite <-inde_expr. auto. intro. generalize (H x); tauto. auto. red in H1. generalize (H1 s s' h2 m x v0); intro. tauto. inversion_clear H3 as [h1]. inversion_clear H4 as [h2]. decompose [and] H3; clear H3. exists h1; exists h2. split; auto. split; auto. split. eapply mapsto_equiv'. apply H5. rewrite <-inde_expr. auto. intro. generalize (H x); tauto. auto. red in H1. generalize (H1 s s' h2 m x v0); intro. tauto. Qed. Lemma inde_mapstos : forall v l a, ~In a l -> inde l (var_e a |--> v). intros. apply inde_mapstos_expr. simpl. split; intros. simpl in H0. inversion_clear H0. inversion_clear H1; try tauto. subst x; tauto. simpl in H0. tauto. Qed. Lemma inde_TT : forall l, inde l TT. split; intros; auto. Qed. Ltac Inde_sep_con := match goal with |- inde ?L (?P ** ?Q) => apply inde_sep_con; Inde_sep_con | |- inde ?L (?V |--> ?L') => apply inde_mapstos; simpl; intuition; discriminate | |- inde ?L TT => apply inde_TT | _ => trivial end. Ltac Inde_update_store := apply inde_update_store; Inde_sep_con. Ltac var := intro; discriminate. Lemma inde_seq : forall R c d, inde (modified_cmd_var (c; d)) R -> inde (modified_cmd_var c) R /\ inde (modified_cmd_var d) R. split; split; intros. lapply (H s s' h m x v). tauto. simpl. apply in_or_app; auto. lapply (H s s' h m x v). tauto. simpl. apply in_or_app; auto. lapply (H s s' h m x v). intros. tauto. simpl. apply in_or_app; auto. lapply (H s s' h m x v). intros. tauto. simpl. apply in_or_app; auto. Qed. Lemma inde_cmd_mult_seq : forall R c d, inde_cmd_mult (c; d) R -> inde_cmd_mult c R /\ inde_cmd_mult d R. split; split; intros. lapply (H s s' h m). intro. generalize (H2 m'); tauto. simpl. auto. lapply (H s s' h m). intro. generalize (H2 m'); tauto. simpl. auto. lapply (H s s' h m). intro. generalize (H2 m'); tauto. simpl. auto. lapply (H s s' h m). intro. generalize (H2 m'); tauto. simpl. auto. Qed. Lemma inde_ifte_beq : forall R r1 r2 c d, inde (modified_cmd_var (ifte_beq r1, r2 thendo c elsedo d)) R -> inde (modified_cmd_var c) R /\ inde (modified_cmd_var d) R. intros. split. red. intros. red in H. generalize (H s s' h m x v); intro. apply H1. simpl. apply in_or_app. auto. red. intros. red in H. generalize (H s s' h m x v); intro. apply H1. simpl. apply in_or_app. auto. Qed. Lemma inde_ifte_bltz : forall R r1 c d, inde (modified_cmd_var (ifte_bltz r1 thendo c elsedo d)) R -> inde (modified_cmd_var c) R /\ inde (modified_cmd_var d) R. intros. split. red. intros. red in H. generalize (H s s' h m x v); intro. apply H1. simpl. apply in_or_app. auto. red. intros. red in H. generalize (H s s' h m x v); intro. apply H1. simpl. apply in_or_app. auto. Qed. Definition inde_mult (P:assert) := forall s s' h, (forall m m', P s s' m h <-> P s s' m' h). Lemma inde_mult_sep_con : forall (P Q:assert), inde_mult P -> inde_mult Q -> inde_mult (P ** Q). intros. red. split; intros. inversion_clear H1. inversion_clear H2. exists x; exists x0. split; intuition. generalize (H s s' x m m'); tauto. generalize (H0 s s' x0 m m'); tauto. inversion_clear H1. inversion_clear H2. exists x; exists x0. split; intuition. generalize (H s s' x m m'); tauto. generalize (H0 s s' x0 m m'); tauto. Qed. Lemma inde_mult_TT : inde_mult TT. red; tauto. Qed. Lemma inde_mult_mapstos : forall a v, inde_mult (var_e a |--> v). intros. red; split; intros. apply mapstos_ext_m with m. auto. apply mapstos_ext_m with m'. auto. Qed. Lemma inde_mult_maddu : forall (P:assert) p s s' m h, inde_mult P -> P s s' m h -> P s s' (multiplier.maddu_op p m) h. intros. red in H. generalize (H s s' h m (multiplier.maddu_op p m)); clear H; intro. tauto. Qed. Ltac Inde_mult_sep_con := match goal with |- inde_mult (?P ** ?Q) => apply inde_mult_sep_con; Inde_mult_sep_con | |- inde_mult (?V |--> ?L') => apply inde_mult_mapstos | |- inde_mult TT => apply inde_mult_TT | _ => trivial end. Ltac Inde_mult_maddu := apply inde_mult_maddu; Inde_mult_sep_con. Lemma inde_mult_mflhxu_op : forall (P:assert) s s' m h, inde_mult P -> P s s' m h -> P s s' (multiplier.mflhxu_op m) h. intros. red in H. generalize (H s s' h m (multiplier.mflhxu_op m)); clear H; intro. tauto. Qed. Ltac Inde_mult_mflhxu_op := apply inde_mult_mflhxu_op; Inde_mult_sep_con. Lemma inde_mult_multu : forall (P:assert) p s s' m h, inde_mult P -> P s s' m h -> P s s' (multiplier.multu_op p m) h. intros. red in H. generalize (H s s' h m (multiplier.multu_op p m)); clear H; intro. tauto. Qed. Ltac Inde_mult_multu := apply inde_mult_multu; Inde_mult_sep_con. Lemma inde_mult_mtlo : forall (P:assert) p s s' m h, inde_mult P -> P s s' m h -> P s s' (multiplier.mtlo_op p m) h. intros. red in H. generalize (H s s' h m (multiplier.mtlo_op p m)); clear H; intro. tauto. Qed. Ltac Inde_mult_mtlo := apply inde_mult_mtlo; Inde_mult_sep_con. Lemma inde_mult_mthi : forall (P:assert) p s s' m h, inde_mult P -> P s s' m h -> P s s' (multiplier.mthi_op p m) h. intros. red in H. generalize (H s s' h m (multiplier.mthi_op p m)); clear H; intro. tauto. Qed. Ltac Inde_mult_mthi := apply inde_mult_mthi; Inde_mult_sep_con. Lemma inde_mult_msubu : forall (P:assert) p s s' m h, inde_mult P -> P s s' m h -> P s s' (multiplier.msubu_op p m) h. intros. red in H. generalize (H s s' h m (multiplier.msubu_op p m)); clear H; intro. tauto. Qed. Ltac Inde_mult_msubu := apply inde_mult_msubu; Inde_mult_sep_con. Lemma inde_mult_ifte_beq : forall R r1 r2 c d, (inde_cmd_mult (ifte_beq r1, r2 thendo c elsedo d) R) -> (inde_cmd_mult c R) /\ (inde_cmd_mult d R). intros. split. red. intros. red in H. generalize (H s s' h m); intro. apply H1. simpl. auto. red. intros. red in H. generalize (H s s' h m); intro. apply H1. simpl. auto. Qed. Lemma inde_mult_ifte_bltz : forall R r1 c d, (inde_cmd_mult (ifte_bltz r1 thendo c elsedo d) R) -> (inde_cmd_mult c R) /\ (inde_cmd_mult d R). intros. split. red. intros. red in H. generalize (H s s' h m); intro. apply H1. simpl. auto. red. intros. red in H. generalize (H s s' h m); intro. apply H1. simpl. auto. Qed. Lemma frame_rule : forall P c Q, {{P}} c {{Q}} -> forall R , (inde (modified_cmd_var c) R -> inde_cmd_mult c R -> {{ P ** R }} c {{ Q ** R }}). do 4 intro. induction H. (* case skip *) intros. apply semax_skip. (* case addi *) intros. apply semax_strengthen_pre with (update_store_addi rt rs imm (P**R)). red; intros. red in H1. inversion_clear H1 as [h1]. inversion_clear H2 as [h2]. decompose [and] H1; clear H1. red. intros. red in H3. exists h1; exists h2. split; auto. split; auto. split; auto. apply inde_update_store. auto. auto. apply semax_addi. (* case addiu *) intros. apply semax_strengthen_pre with (update_store_addiu rt rs imm (P**R)). red; intros. red in H1. inversion_clear H1 as [h1]. inversion_clear H2 as [h2]. decompose [and] H1; clear H1. red. exists h1; exists h2. split; auto. split; auto. split; auto. red in H. apply inde_update_store. simpl in H. auto. auto. apply semax_addiu. (* case add *) intros. apply semax_strengthen_pre with (update_store_add rd rs rt (Q**R)). red; intros. red in H1. inversion_clear H1 as [h1]. inversion_clear H2 as [h2]. decompose [and] H1; clear H1. red; intros. red in H3. exists h1; exists h2. split; auto. split; auto. split; auto. apply inde_update_store. auto. auto. apply semax_add. (* case addu *) intros. apply semax_strengthen_pre with (update_store_addu rd rs rt (Q**R)). red; intros. red in H1. inversion_clear H1 as [h1]. inversion_clear H2 as [h2]. decompose [and] H1; clear H1. red. exists h1; exists h2. split; auto. split; auto. split; auto. simpl in H. apply inde_update_store. auto. auto. apply semax_addu. (* cmd_and *) intros. apply semax_strengthen_pre with (update_store_and rd rs imm (Q**R)). red; intros. red in H1. inversion_clear H1 as [h1]. inversion_clear H2 as [h2]. decompose [and] H1; clear H1. red. exists h1; exists h2. split; auto. split; auto. split; auto. apply inde_update_store. auto. auto. apply semax_and. (* case lw *) intros. apply semax_strengthen_pre with (lw2 rt offset base (P**R)). red; intros. red in H1. red. inversion_clear H1 as [h1]. inversion_clear H2 as [h2]. decompose [and] H1; clear H1. unfold lw2 in H3. inversion_clear H3 as [p]. inversion_clear H1. inversion_clear H5 as [z]. inversion_clear H1. exists p; split; auto; exists z; split. rewrite H4. apply heap.lookup_union; auto. exists h1; exists h2. split; auto. split; auto. split; auto. apply inde_update_store. auto. auto. apply semax_lw. (* case lwxs *) intros. apply semax_strengthen_pre with (lookup_heap_lwxs rt index base (P**R)). red; intros. red in H1. red. inversion_clear H1 as [h1]. inversion_clear H2 as [h2]. decompose [and] H1; clear H1. unfold lw2 in H3. inversion_clear H3 as [p]. inversion_clear H1. inversion_clear H5 as [z]. inversion_clear H1. exists p; split; auto; exists z; split. rewrite H4. apply heap.lookup_union; auto. exists h1; exists h2. split; auto. split; auto. split; auto. apply inde_update_store. auto. auto. apply semax_lwxs. (* case maddu *) intros. apply semax_strengthen_pre with (fun s1 s2 m h => (Q**R) s1 s2 (multiplier.maddu_op (umul (gpr.lookup rs s1) (gpr.lookup rt s1)) m) h). red; intros. red in H1. red. inversion_clear H1 as [h1]. inversion_clear H2 as [h2]. decompose [and] H1; clear H1. exists h1; exists h2. split; auto. split; auto. split; auto. red in H0. simpl in H0. generalize (H0 s s' h2 m I (multiplier.maddu_op (umul (gpr.lookup rs s) (gpr.lookup rt s)) m)); intro. tauto. apply semax_maddu. (* case mflhxu *) intros. apply semax_strengthen_pre with (update_store_mflhxu rd (P**R)). red; intros. inversion_clear H1 as [h1]. inversion_clear H2 as [h2]. decompose [and] H1; clear H1. exists h1; exists h2. split; auto. split; auto. split. red in H3. auto. generalize (H0 (gpr.update rd (multiplier.lo m) s) s' h2 m I (multiplier.mflhxu_op m)); intro. red in H. simpl in H. lapply (H s s' h2 (multiplier.mflhxu_op m) rd (multiplier.lo m)). intro. lapply (H s s' h2 m rd (multiplier.lo m)). intro. tauto. auto. auto. apply semax_mflhxu. (* case mfhi *) intros. apply semax_strengthen_pre with (update_store_mfhi rd (Q**R)). red; intros. inversion_clear H1 as [h1]. inversion_clear H2 as [h2]. decompose [and] H1; clear H1. exists h1; exists h2. split; auto. split; auto. red in H3. split; auto. red in H. simpl in H. lapply (H s s' h2 m rd (multiplier.hi m)). intro. tauto. auto. apply semax_mfhi. (* case mflo *) intros. apply semax_strengthen_pre with (update_store_mflo rd (Q**R)). red; intros. inversion_clear H1 as [h1]. inversion_clear H2 as [h2]. decompose [and] H1; clear H1. exists h1; exists h2. split; auto. split; auto. red in H3. split; auto. red in H. simpl in H. lapply (H s s' h2 m rd (multiplier.lo m)). intro. tauto. auto. apply semax_mflo. (* case mthi *) intros. apply semax_strengthen_pre with (update_store_mthi rs (Q**R)). red; intros. inversion_clear H1 as [h1]. inversion_clear H2 as [h2]. decompose [and] H1; clear H1. exists h1; exists h2. split; auto. split; auto. red in H3. split; auto. simpl in H. red in H0. simpl in H0. generalize (H0 s s' h2 (multiplier.mthi_op (gpr.lookup rs s) m) I m); tauto. apply semax_mthi. (* case mtlo *) intros. apply semax_strengthen_pre with (update_store_mtlo rs (Q**R)). red; intros. inversion_clear H1 as [h1]. inversion_clear H2 as [h2]. decompose [and] H1; clear H1. exists h1; exists h2. split; auto. split; auto. red in H3. split; auto. simpl in H. red in H0. simpl in H0. generalize (H0 s s' h2 (multiplier.mtlo_op (gpr.lookup rs s) m) I m); tauto. apply semax_mtlo. (* case multu *) intros. apply semax_strengthen_pre with (fun s s' m h => (Q**R) s s' (multiplier.multu_op (umul (gpr.lookup rs s) (gpr.lookup rt s)) m) h). red; intros. red in H1. red. inversion_clear H1 as [h1]. inversion_clear H2 as [h2]. decompose [and] H1; clear H1. exists h1; exists h2. split; auto. split; auto. split; auto. red in H0. simpl in H0. generalize (H0 s s' h2 m I (multiplier.multu_op (umul (gpr.lookup rs s) (gpr.lookup rt s)) m)); intro. tauto. apply semax_multu. (* case msubu *) intros. apply semax_strengthen_pre with ( fun s s' m h => (Q**R) s s' (multiplier.msubu_op (umul (gpr.lookup rs s) (gpr.lookup rt s)) m) h ). red; intros. inversion_clear H1 as [h1]. inversion_clear H2 as [h2]. decompose [and] H1; clear H1. exists h1; exists h2. split; auto. split; auto. split; auto. red in H0. simpl in H0. generalize (H0 s s' h2 m I (multiplier.msubu_op (umul (gpr.lookup rs s) (gpr.lookup rt s)) m) ); intro. eapply (proj1 H1). tauto. apply semax_msubu. (* case nor *) intros. apply semax_strengthen_pre with (update_store_nor rd rs rt (Q**R)). red; intros. inversion_clear H1 as [h1]. inversion_clear H2 as [h2]. decompose [and] H1; clear H1. red in H3. exists h1; exists h2. split; auto. split; auto. split. auto. apply inde_update_store. auto. auto. apply semax_nor. (* case sll *) intros. apply semax_strengthen_pre with (update_store_sll rx ry sa (Q**R)). red; intros. inversion_clear H1 as [h1]. inversion_clear H2 as [h2]. decompose [and] H1; clear H1. red in H3. exists h1; exists h2. split; auto. split; auto. split. auto. apply inde_update_store. auto. auto. apply semax_sll. (* case sltu *) intros. apply semax_strengthen_pre with (update_store_sltu rd rs rt (Q**R)). red; intros. red in H1. inversion_clear H1 as [h1]. inversion_clear H2 as [h2]. decompose [and] H1; clear H1. red in H3. red. exists h1; exists h2. split; auto. split; auto. split; auto. apply inde_update_store. auto. auto. apply semax_sltu. (* case sw *) intros. apply semax_strengthen_pre with (update_heap2 rt offset base (P**R)). red; intros. red. red in H1. inversion_clear H1 as [h1]. inversion_clear H2 as [h2]. decompose [and] H1; clear H1. red in H3. inversion_clear H3 as [p]. inversion_clear H1. exists p; split; auto. inversion_clear H5. inversion_clear H1 as [z]. split. exists z. rewrite H4. apply heap.lookup_union. auto. auto. red. exists (heap.update p (gpr.lookup rt s) h1); exists h2. split. apply heap.disjoint_update. auto. split. rewrite H4. eapply heap.equal_update_L. auto. apply H5. auto. apply semax_sw. (* case seq *) intros. apply semax_seq with (Q ** R0). apply semax_strengthen_pre with (P ** R0). red; auto. generalize (IHsemax1 R0); intro. apply IHsemax1. exact (proj1 (inde_seq _ _ _ H1)). exact (proj1 (inde_cmd_mult_seq _ _ _ H2)). apply (IHsemax2 R0). apply (proj2 (inde_seq _ _ _ H1)). exact (proj2 (inde_cmd_mult_seq _ _ _ H2)). (* semax_conseq *) intros. generalize (IHsemax _ H2); intros. apply semax_strengthen_pre with (P' ** R). red; intros. red in H5. inversion_clear H5 as [h1]. inversion_clear H6 as [h2]. decompose [and] H5; clear H5. exists h1; exists h2; auto. apply semax_weaken_post with (Q' ** R). red; intros. inversion_clear H5 as [h1]. inversion_clear H6 as [h2]. decompose [and] H5; clear H5. exists h1; exists h2; auto. auto. (* semax_while_bne *) intros. apply semax_weaken_post with (fun s1 s2 m h => (P ** R) s1 s2 m h /\ u2Z (eval (var_e r) s1) = u2Z (eval (var_e r') s1)). red; intros. red. inversion_clear H2. red in H3. inversion_clear H3 as [h1]. inversion_clear H2 as [h2]. decompose [and] H3; clear H3. exists h1; exists h2; auto. apply semax_strengthen_pre with (fun s1 s2 m h => (P ** R) s1 s2 m h). red; intros. auto. simpl eval. apply semax_while_bne with (P:=P**R). assert (inde (modified_cmd_var c) R). simpl in H0. auto. generalize (IHsemax _ H2); intro. apply semax_strengthen_pre with (fun s1 s2 m h => ((fun s0 s0' m0 h0 => P s0 s0' m0 h0 /\ u2Z (eval (var_e r) s1) <> u2Z (eval (var_e r') s1)) ** R) s1 s2 m h). red; intros. red. inversion_clear H4. red in H5. inversion_clear H5 as [h1]. inversion_clear H4 as [h2]. decompose [and] H5; clear H5 . exists h1; exists h2; auto. auto. (* semax_ifte_beq *) intros. apply semax_ifte_beq. assert (inde (modified_cmd_var c) R). exact (proj1 (inde_ifte_beq _ _ _ _ _ H1)). assert (inde_cmd_mult c R). apply (proj1 (inde_mult_ifte_beq _ _ _ _ _ H2)). generalize (IHsemax1 _ H3 H4); intro. apply semax_strengthen_pre with (fun s s' m h => ((fun s0 s0' m0 h0 => P s0 s0' m0 h0 /\ gpr.lookup r1 s0 = gpr.lookup r2 s0) ** R) s s' m h ); auto. red; intros. inversion_clear H6. red in H7. inversion_clear H7 as [h1]. inversion_clear H6 as [h2]. decompose [and] H7; clear H7. red. exists h1; exists h2; auto. assert (inde (modified_cmd_var d) R). exact (proj2 (inde_ifte_beq _ _ _ _ _ H1)). assert (inde_cmd_mult d R). exact (proj2 (inde_mult_ifte_beq _ _ _ _ _ H2)). generalize (IHsemax2 _ H3 H4); intro. apply semax_strengthen_pre with (fun s s' m h => ((fun s0 s0' m0 h0 => P s0 s0' m0 h0 /\ gpr.lookup r1 s0 <> gpr.lookup r2 s0) ** R) s s' m h ); auto. red; intros. inversion_clear H6. red in H7. inversion_clear H7 as [h1]. inversion_clear H6 as [h2]. decompose [and] H7; clear H7. red. exists h1; exists h2; auto. (* semax_ifte_bltz *) intros. apply semax_ifte_bltz. assert (inde (modified_cmd_var c) R). exact (proj1 (inde_ifte_bltz _ _ _ _ H1)). assert (inde_cmd_mult c R). apply (proj1 (inde_mult_ifte_bltz _ _ _ _ H2)). generalize (IHsemax1 _ H3 H4); intro. apply semax_strengthen_pre with (fun s s' m h => ((fun s0 s0' m0 h0 => P s0 s0' m0 h0 /\ s2Z (gpr.lookup r1 s0) < 0) ** R) s s' m h ); auto. red; intros. inversion_clear H6. red in H7. inversion_clear H7 as [h1]. inversion_clear H6 as [h2]. decompose [and] H7; clear H7. red. exists h1; exists h2; auto. assert (inde (modified_cmd_var d) R). exact (proj2 (inde_ifte_bltz _ _ _ _ H1)). assert (inde_cmd_mult d R). exact (proj2 (inde_mult_ifte_bltz _ _ _ _ H2)). generalize (IHsemax2 _ H3 H4); intro. apply semax_strengthen_pre with (fun s s' m h => ((fun s0 s0' m0 h0 => P s0 s0' m0 h0 /\ s2Z (gpr.lookup r1 s0) >= 0) ** R) s s' m h ); auto. red; intros. inversion_clear H6. red in H7. inversion_clear H7 as [h1]. inversion_clear H6 as [h2]. decompose [and] H7; clear H7. red. exists h1; exists h2; auto. Qed.