Generals lemmas for asmblockgenproof

4 files changed, 896 insertions, 13 deletions

diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v
index 5e41d96a..c163ea10 100644
--- a/aarch64/Asmblock.v
+++ b/aarch64/Asmblock.v
@@ -41,6 +41,8 @@ Require Export Asm.
 
 Local Open Scope option_monad_scope.
 
+Notation regset := Asm.regset.
+
 (** * Abstract syntax *)
 
 (* First task: splitting the big [instruction] type below into CFI and basic instructions.
diff --git a/aarch64/Asmblockgen.v b/aarch64/Asmblockgen.v
index d68cd7ac..96e7db4b 100644
--- a/aarch64/Asmblockgen.v
+++ b/aarch64/Asmblockgen.v
@@ -1159,11 +1159,11 @@ Definition it1_is_parent (before: bool) (i: Machblock.basic_inst) : bool :=
   | _ => false
   end.
 
-Fixpoint transl_basic_code (f: Machblock.function) (il: list Machblock.basic_inst) (it1p: bool) (k: bcode):=
+Fixpoint transl_basic_code (f: Machblock.function) (il: list Machblock.basic_inst) (it1p: bool) :=
   match il with
-  | nil => OK (k)
+  | nil => OK (nil)
   | i1 :: il' =>
-      do k1 <- transl_basic_code f il' (it1_is_parent it1p i1) k;
+      do k1 <- transl_basic_code f il' (it1_is_parent it1p i1);
       transl_instr_basic f i1 it1p k1
   end.
 
@@ -1196,12 +1196,29 @@ Program Definition gen_bblocks (hd: list label) (c: bcode) (ctl: list instructio
 
 (* XXX: the simulation proof may be complex with this pattern. We may fix this later *)
 Program Definition cons_bblocks (ll: list label) (bdy: list basic) (ex: option control): bblocks :=
-  match non_empty_bblockb bdy ex with
-  | true => {| header := ll; body:= bdy; exit := ex |} :: nil
-  | false => {| header := ll; body:= Pnop::nil; exit := None |} :: nil
+  match ex with
+  | None =>
+    match bdy with
+    | nil => {| header := ll; body:= Pnop::nil; exit := None |} :: nil
+    | _ => {| header := ll; body:= bdy; exit := None |} :: nil
+    end
+  | _ =>
+    match bdy with
+    | nil => {| header := ll; body:= nil; exit := ex |} :: nil
+    | _ => {| header := ll; body:= bdy; exit := ex |} :: nil
+    end
   end.
-Obligation 1.
-  rewrite <- Heq_anonymous. constructor.
+Next Obligation.
+  induction bdy. congruence.
+  simpl. auto.
+Qed.
+Next Obligation.
+  destruct ex. simpl. auto.
+  congruence.
+Qed.
+Next Obligation.
+  induction bdy. congruence.
+  simpl. auto.
 Qed.
 
 Definition transl_control (f: Machblock.function) (ctl: control_flow_inst) : res (bcode*control) :=
@@ -1227,10 +1244,9 @@ Definition transl_exit (f: Machblock.function) (ext: option control_flow_inst) :
   end.
 
 Definition transl_block (f: Machblock.function) (fb: Machblock.bblock) (ep: bool) : res (list bblock) :=
-  let stub := false in
-  do (bdy, ex) <- transl_exit f fb.(Machblock.exit);
-  do bdy' <- transl_basic_code f fb.(Machblock.body) ep bdy;
-  OK (cons_bblocks fb.(Machblock.header) bdy' ex) 
+  do (bdy2, ex) <- transl_exit f fb.(Machblock.exit);
+  do bdy1 <- transl_basic_code f fb.(Machblock.body) ep;
+  OK (cons_bblocks fb.(Machblock.header) (bdy1 @@ bdy2) ex) 
   .
 
 Fixpoint transl_blocks (f: Machblock.function) (lmb: list Machblock.bblock) (ep: bool) :=
diff --git a/aarch64/Asmblockgenproof.v b/aarch64/Asmblockgenproof.v
index bd96ff3b..33acc110 100644
--- a/aarch64/Asmblockgenproof.v
+++ b/aarch64/Asmblockgenproof.v
@@ -29,6 +29,20 @@ Hypothesis TRANSF: match_prog prog tprog.
 Let ge := Genv.globalenv prog.
 Let tge := Genv.globalenv tprog.
 
+Lemma symbols_preserved:
+  forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
+Proof (Genv.find_symbol_match TRANSF).
+
+Lemma senv_preserved:
+  Senv.equiv ge tge.
+Proof (Genv.senv_match TRANSF).
+
+Lemma functions_translated:
+  forall b f,
+  Genv.find_funct_ptr ge b = Some f ->
+  exists tf,
+  Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = OK tf.
+Proof (Genv.find_funct_ptr_transf_partial TRANSF).
 
 Hypothesis symbol_high_low: forall (id: ident) (ofs: ptrofs),
   Val.addl (symbol_high lk id ofs) (symbol_low lk id ofs) = Genv.symbol_address tge id ofs.
@@ -46,6 +60,64 @@ Proof.
   omega.
 Qed.
 
+(** * Proof of semantic preservation *)
+
+(** Semantic preservation is proved using a complex simulation diagram
+  of the following form.
+<<
+                                     MB.step
+                      ---------------------------------------->
+                      header      body          exit
+                  st1 -----> st2 -----> st3 ------------------> st4
+                   |          |          |                       |
+                   |   (A)    |   (B)    |         (C)           |
+   match_codestate |          |          |                       |
+                   |  header  |   body1  |  body2                |  match_states
+                  cs1 -----> cs2 -----> cs3 ------> cs4          |
+                   |                  /                \  exit   |
+   match_asmstate  |   ---------------                  --->---  |
+                   |  /   match_asmstate                       \ |
+                  st'1 ---------------------------------------> st'2
+                                     AB.step                  *
+>>
+  The invariant between each MB.step/AB.step is the [match_states] predicate below.
+  However, we also need to introduce an intermediary state [Codestate] which allows
+  us to reason on a finer grain, executing header, body and exit separately.
+
+  This [Codestate] consists in a state like [Asmblock.State], except that the
+  code is directly stored in the state, much like [Machblock.State]. It also features
+  additional useful elements to keep track of while executing a bblock.
+*)
+
+Inductive match_states: Machblock.state -> Asm.state -> Prop :=
+  | match_states_intro:
+      forall s fb sp c ep ms m m' rs f tf tc
+        (STACKS: match_stack ge s)
+        (FIND: Genv.find_funct_ptr ge fb = Some (Internal f))
+        (MEXT: Mem.extends m m')
+        (AT: transl_code_at_pc ge (rs PC) fb f c ep tf tc)
+        (AG: agree ms sp rs)
+        (DXP: ep = true -> rs#X29 = parent_sp s),
+      match_states (Machblock.State s fb sp c ms m)
+                   (Asm.State rs m')
+  | match_states_call:
+      forall s fb ms m m' rs
+        (STACKS: match_stack ge s)
+        (MEXT: Mem.extends m m')
+        (AG: agree ms (parent_sp s) rs)
+        (ATPC: rs PC = Vptr fb Ptrofs.zero)
+        (ATLR: rs RA = parent_ra s),
+      match_states (Machblock.Callstate s fb ms m)
+                   (Asm.State rs m')
+  | match_states_return:
+      forall s ms m m' rs
+        (STACKS: match_stack ge s)
+        (MEXT: Mem.extends m m')
+        (AG: agree ms (parent_sp s) rs)
+        (ATPC: rs PC = parent_ra s),
+      match_states (Machblock.Returnstate s ms m)
+                   (Asm.State rs m').
+
 (** Existence of return addresses *)
 
 Lemma return_address_exists:
@@ -61,11 +133,689 @@ Proof.
 - exact transf_function_no_overflow.
 Qed.
 
+(* Useful for dealing with the many cases in some proofs *)
+Ltac exploreInst :=
+  repeat match goal with
+  | [ H : match ?var with | _ => _ end = _ |- _ ] => destruct var
+  | [ H : OK _ = OK _ |- _ ] => monadInv H
+  | [ |- context[if ?b then _ else _] ] => destruct b
+  | [ |- context[match ?m with | _ => _ end] ] => destruct m
+  | [ |- context[match ?m as _ return _ with | _ => _ end]] => destruct m
+  | [ H : bind _ _ = OK _ |- _ ] => monadInv H
+  | [ H : Error _ = OK _ |- _ ] => inversion H
+  end.
+  
+Ltac desif :=
+  repeat match goal with
+  | [ |- context[if ?f then _ else _ ] ] => destruct f
+  end.
+
+(** Some translation properties *)
+
+Lemma no_builtin_preserved:
+  forall f ex x1 x2,
+  (forall ef args res, ex <> Some (MBbuiltin ef args res)) ->
+  transl_exit f ex = OK(x1, x2) ->
+  (exists i, x2 = Some (PCtlFlow i))
+    \/ x2 = None.
+Proof.
+  intros until x2. intros Hbuiltin TIC.
+  destruct ex.
+  - destruct c.
+    (* MBcall *)
+    + simpl in TIC. monadInv TIC. exploreInst; simpl; eauto.
+    (* MBtailcall *)
+    + simpl in TIC. monadInv TIC. exploreInst; simpl; eauto.
+    (* MBbuiltin *)
+    + assert (H: Some (MBbuiltin e l b) <>  Some (MBbuiltin e l b)).
+        apply Hbuiltin. contradict H; auto.
+    (* MBgoto *)
+    + simpl in TIC. exploreInst; simpl; eauto.
+    (* MBcond *)
+    + simpl in TIC. unfold transl_cond_branch, transl_cond_branch_default in TIC.
+      monadInv TIC; exploreInst; simpl; eauto.
+    (* MBjumptable *)
+    + simpl in TIC. monadInv TIC. exploreInst; simpl; eauto.
+    (* MBreturn *)
+    + simpl in TIC. monadInv TIC. simpl. eauto.
+  - monadInv TIC. simpl; auto.
+Qed.
+
+Lemma transl_blocks_distrib:
+  forall c f bb tbb tc ep,
+  transl_blocks f (bb::c) ep = OK (tbb::tc)
+  -> (forall ef args res, MB.exit bb <> Some (MBbuiltin ef args res))
+  -> transl_block f bb (if MB.header bb then ep else false) = OK (tbb :: nil)
+  /\ transl_blocks f c false = OK tc.
+Proof.
+  intros until ep. intros TLBS Hbuiltin.
+  destruct bb as [hd bdy ex].
+  monadInv TLBS. monadInv EQ.
+  exploit no_builtin_preserved; eauto. intros Hectl. destruct Hectl.
+  - destruct H as [i Hectl].
+    unfold cons_bblocks in H0. rewrite Hectl in H0.
+    destruct (x3 @@ x1) eqn: CBDY; inv H0; inv EQ0;
+    simpl in *; unfold transl_block; simpl; rewrite H0; simpl;
+    rewrite EQ; simpl; rewrite CBDY; auto.
+  - unfold cons_bblocks in H0. rewrite H in H0.
+    destruct (x3 @@ x1) eqn: CBDY; inv H0; inv EQ0;
+    simpl in *; unfold transl_block; simpl; rewrite H0; simpl;
+    rewrite EQ; simpl; rewrite CBDY; auto.
+Qed.
+
+Lemma cons_bblocks_nobuiltin:
+  forall thd tbdy tex tbb,
+  (tbdy <> nil \/ tex <> None) ->
+  (forall ef args res, tex <> Some (Pbuiltin ef args res)) ->
+  cons_bblocks thd tbdy tex = tbb :: nil ->
+     header tbb = thd
+  /\ body tbb = tbdy
+  /\ exit tbb = tex.
+Proof.
+  intros until tbb. intros Hnonil Hnobuiltin CONSB. unfold cons_bblocks in CONSB.
+  destruct (tex) eqn:ECTL.
+  - destruct tbdy; inv CONSB; simpl; auto.
+  - inversion Hnonil.
+    + destruct tbdy as [|bi tbdy]; [ contradiction H; auto | inv CONSB; auto].
+    + contradict H; simpl; auto.
+Qed.
+
+Lemma transl_blocks_nonil:
+  forall f bb c tc ep,
+  transl_blocks f (bb::c) ep = OK tc ->
+  exists tbb tc', tc = tbb :: tc'.
+Proof.
+  intros until ep. intros TLBS. monadInv TLBS. monadInv EQ. unfold cons_bblocks.
+  destruct (x2);
+  destruct (x3 @@ x1); simpl; eauto.
+Qed.
+
+Definition mb_remove_header bb := {| MB.header := nil; MB.body := MB.body bb; MB.exit := MB.exit bb |}.
+
+Definition mb_remove_body (bb: MB.bblock) := 
+  {| MB.header := MB.header bb; MB.body := nil; MB.exit := MB.exit bb |}.
+  
+Definition mbsize (bb: MB.bblock) := (length (MB.body bb) + length_opt (MB.exit bb))%nat.
+
+Lemma mbsize_eqz:
+  forall bb, mbsize bb = 0%nat -> MB.body bb = nil /\ MB.exit bb = None.
+Proof.
+  intros. destruct bb as [hd bdy ex]; simpl in *. unfold mbsize in H.
+  remember (length _) as a. remember (length_opt _) as b.
+  assert (a = 0%nat) by omega. assert (b = 0%nat) by omega. subst. clear H.
+  inv H0. inv H1. destruct bdy; destruct ex; auto.
+  all: try discriminate.
+Qed.
+
+Lemma mbsize_neqz:
+  forall bb, mbsize bb <> 0%nat -> (MB.body bb <> nil \/ MB.exit bb <> None).
+Proof.
+  intros. destruct bb as [hd bdy ex]; simpl in *.
+  destruct bdy; destruct ex; try (right; discriminate); try (left; discriminate).
+  contradict H. unfold mbsize. simpl. auto.
+Qed.
+
+Record codestate :=
+  Codestate {     pstate: state;        (**r projection to Asmblock.state *)
+                  pheader: list label;
+                  pbody1: list basic;   (**r list of basic instructions coming from the translation of the Machblock body *)
+                  pbody2: list basic;   (**r list of basic instructions coming from the translation of the Machblock exit *)
+                  pctl: option control; (**r exit instruction, coming from the translation of the Machblock exit *)
+                  ep: bool;             (**r reflects the [ep] variable used in the translation *)
+                  rem: list AB.bblock;  (**r remaining bblocks to execute *)
+                  cur: bblock           (**r current bblock to execute - to keep track of its size when incrementing PC *)
+            }.
+
+(* The part that deals with Machblock <-> Codestate agreement
+ * Note about DXP: the property of [ep] only matters if the current block doesn't have a header, hence the condition *)
+Inductive match_codestate fb: Machblock.state -> codestate -> Prop :=
+  | match_codestate_intro:
+      forall s sp ms m rs0 m0 f tc ep c bb tbb tbc1 tbc2 ex
+        (STACKS: match_stack ge s)
+        (FIND: Genv.find_funct_ptr ge fb = Some (Internal f))
+        (MEXT: Mem.extends m m0)
+        (TBC: transl_basic_code f (MB.body bb) (if MB.header bb then ep else false) = OK tbc1)
+        (TIC: transl_exit f (MB.exit bb) = OK (tbc2, ex))
+        (TBLS: transl_blocks f c false = OK tc)
+        (AG: agree ms sp rs0)
+        (DXP: (if MB.header bb then ep else false) = true -> rs0#X29 = parent_sp s)
+        ,
+      match_codestate fb (Machblock.State s fb sp (bb::c) ms m)
+        {|  pstate := (Asm.State rs0 m0);
+            pheader := (MB.header bb);
+            pbody1 := tbc1;
+            pbody2 := tbc2;
+            pctl := ex;
+            ep := ep;
+            rem := tc;
+            cur := tbb
+        |}
+.
+
+(* The part ensuring that the code in Codestate actually resides at [rs PC] *)
+Inductive match_asmstate fb: codestate -> Asm.state -> Prop :=
+  | match_asmstate_some:
+      forall rs f tf tc m tbb ofs ep tbdy1 tbdy2 tex lhd
+        (FIND: Genv.find_funct_ptr ge fb = Some (Internal f))
+        (TRANSF: transf_function f = OK tf)
+        (PCeq: rs PC = Vptr fb ofs)
+        (TAIL: code_tail (Ptrofs.unsigned ofs) (fn_blocks tf) (tbb::tc))
+        ,
+      match_asmstate fb 
+        {|  pstate := (Asm.State rs m);
+            pheader := lhd;
+            pbody1 := tbdy1;
+            pbody2 := tbdy2;
+            pctl := tex;
+            ep := ep;
+            rem := tc;
+            cur := tbb |}
+        (Asm.State rs m)
+.
+
+Lemma indexed_memory_access_nonil: forall f ofs r i k,
+  indexed_memory_access_bc f ofs r i k <> nil.
+Proof.
+  intros.
+  unfold indexed_memory_access_bc, loadimm64, loadimm, loadimm_z, loadimm_n;
+  desif; try congruence.
+  all: destruct decompose_int; try destruct p; try congruence.
+Qed.
+
+Lemma loadimm_nonil: forall sz x n k,
+  loadimm sz x n k <> nil.
+Proof.
+  intros.
+  unfold loadimm. desif;
+  unfold loadimm_n, loadimm_z.
+  all: destruct decompose_int; try destruct p; try congruence.
+Qed.
+
+Lemma loadimm32_nonil: forall sz x n,
+  loadimm32 sz x n <> nil.
+Proof.
+  intros.
+  unfold loadimm32. desif; try congruence.
+  apply loadimm_nonil.
+Qed.
+
+Lemma loadimm64_nonil: forall sz x n,
+  loadimm64 sz x n <> nil.
+Proof.
+  intros.
+  unfold loadimm64. desif; try congruence.
+  apply loadimm_nonil.
+Qed.
+
+Lemma loadsymbol_nonil: forall sz x n k,
+  loadsymbol sz x n k <> nil.
+Proof.
+  intros.
+  unfold loadsymbol. desif; try congruence.
+Qed.
+
+Lemma move_extended_nonil: forall x0 x1 x2 a k,
+  move_extended x1 x2 x0 a k <> nil.
+Proof.
+  intros. unfold move_extended, move_extended_base.
+  desif; try congruence.
+Qed.
+
+Lemma arith_extended_nonil: forall insnX insnS x0 x1 x2 x3 a k,
+  arith_extended insnX insnS x1 x2 x3 x0 a k <> nil.
+Proof.
+  intros. unfold arith_extended, move_extended_base.
+  desif; try congruence.
+Qed.
+
+Lemma transl_instr_basic_nonil:
+  forall k f bi ep x,
+  transl_instr_basic f bi ep k = OK x ->
+  x <> nil.
+Proof.
+  intros until x. intros TIB.
+  destruct bi.
+  - simpl in TIB. unfold loadind in TIB;
+    exploreInst; try discriminate; apply indexed_memory_access_nonil.
+  - simpl in TIB. unfold storeind in TIB;
+    exploreInst; try discriminate; apply indexed_memory_access_nonil.
+  - simpl in TIB. monadInv TIB. unfold loadind in EQ. exploreInst; try discriminate;
+    unfold loadptr_bc; apply indexed_memory_access_nonil.
+  - simpl in TIB. unfold transl_op in TIB. exploreInst; try discriminate;
+    unfold addimm32, addimm64, shrx32, shrx64,
+    logicalimm32, logicalimm64, addimm_aux.
+    all: desif; try congruence;
+    try apply loadimm32_nonil; try apply loadimm64_nonil; try apply loadsymbol_nonil;
+    try apply move_extended_nonil; try apply arith_extended_nonil.
+    all: unfold transl_cond in *; exploreInst; try discriminate;
+      try apply loadimm32_nonil; try apply loadimm64_nonil.
+  - simpl in TIB. unfold transl_load in TIB. exploreInst; try discriminate;
+    unfold transl_addressing in *; exploreInst; try discriminate.
+    all: try apply loadimm64_nonil; try apply arith_extended_nonil; try apply loadsymbol_nonil.
+  - simpl in TIB. unfold transl_store in TIB. exploreInst; try discriminate;
+    unfold transl_addressing in *; exploreInst; try discriminate.
+    all: try apply loadimm64_nonil; try apply arith_extended_nonil; try apply loadsymbol_nonil.
+Qed.
+
+Lemma transl_basic_code_nonil:
+  forall bdy f x ep,
+  bdy <> nil ->
+  transl_basic_code f bdy ep = OK x ->
+  x <> nil.
+Proof.
+  induction bdy as [|bi bdy].
+    intros. contradict H0; auto.
+  destruct bdy as [|bi2 bdy].
+  - clear IHbdy. intros f x b _ TBC. simpl in TBC. eapply transl_instr_basic_nonil; eauto.
+  - intros f x b Hnonil TBC. remember (bi2 :: bdy) as bdy'.
+    monadInv TBC.
+    assert (x0 <> nil).
+      eapply IHbdy; eauto. subst bdy'. discriminate.
+    eapply transl_instr_basic_nonil; eauto.
+Qed.
+
+Lemma transl_exit_nonil:
+  forall ex f bdy x,
+  ex <> None ->
+  transl_exit f ex = OK(bdy, x) ->
+  x <> None.
+Proof.
+  intros ex f bdy x Hnonil TIC.
+  destruct ex as [ex|].
+  - clear Hnonil. destruct ex.
+    all: try (simpl in TIC; try monadInv TIC; exploreInst; discriminate).
+  - contradict Hnonil; auto.
+Qed.
+
+Lemma transl_exit_nobuiltin:
+  forall f ex bdy x,
+  (forall ef args res, ex <> Some (MBbuiltin ef args res)) ->
+  transl_exit f ex = OK (bdy, x) ->
+  (forall ef args res, x <> Some (Pbuiltin ef args res)).
+Proof.
+  intros until x. intros Hnobuiltin TIC. intros until res.
+  unfold transl_exit, transl_control in TIC. exploreInst. monadInv TIC.
+  exploreInst.
+  all: try discriminate.
+  - assert False. eapply Hnobuiltin; eauto. destruct H.
+  - unfold transl_cond_branch, transl_cond_branch_default in EQ. exploreInst.
+    all: try discriminate.
+Qed.
+
+Theorem app_nonil: forall A (l1 l2: list A),
+  l1 <> nil ->
+  l1 @@ l2 <> nil.
+Proof.
+  induction l2.
+  - intros; rewrite app_nil_r; auto.
+  - intros. unfold not. intros. symmetry in H0. 
+    generalize (app_cons_not_nil); intros. unfold not in H1.
+    generalize (H0). apply H1.
+Qed.
+
+Theorem match_state_codestate:
+  forall mbs abs s fb sp bb c ms m,
+  (forall ef args res, MB.exit bb <> Some (MBbuiltin ef args res)) ->
+  (MB.body bb <> nil \/ MB.exit bb <> None) ->
+  mbs = (Machblock.State s fb sp (bb::c) ms m) ->
+  match_states mbs abs ->
+  exists cs fb f tbb tc ep,
+    match_codestate fb mbs cs /\ match_asmstate fb cs abs
+    /\ Genv.find_funct_ptr ge fb = Some (Internal f)
+    /\ transl_blocks f (bb::c) ep = OK (tbb::tc)
+    /\ body tbb = pbody1 cs ++ pbody2 cs
+    /\ exit tbb = pctl cs
+    /\ cur cs = tbb /\ rem cs = tc
+    /\ pstate cs = abs.
+Proof.
+  intros until m. intros Hnobuiltin Hnotempty Hmbs MS. subst. inv MS.
+  inv AT. clear H0. exploit transl_blocks_nonil; eauto. intros (tbb & tc' & Htc). subst.
+  exploit transl_blocks_distrib; eauto. intros (TLB & TLBS). clear H2.
+  monadInv TLB. exploit cons_bblocks_nobuiltin; eauto.
+    { inversion Hnotempty.
+      - destruct (MB.body bb) as [|bi bdy]; try (contradict H0; simpl; auto; fail).
+        left. apply app_nonil. eapply transl_basic_code_nonil; eauto.
+      - destruct (MB.exit bb) as [ei|]; try (contradict H0; simpl; auto; fail).
+        right. eapply transl_exit_nonil; eauto. }
+    eapply transl_exit_nobuiltin; eauto.
+  intros (Hth & Htbdy & Htexit).
+  exists {| pstate := (State rs m'); pheader := (Machblock.header bb); pbody1 := x1; pbody2 := x;
+            pctl := x0; ep := ep0; rem := tc'; cur := tbb |}, fb, f, tbb, tc', ep0.
+  repeat split. 1-2: econstructor; eauto.
+  { destruct (MB.header bb). eauto. discriminate. } eauto.
+  unfold transl_blocks. fold transl_blocks. unfold transl_block. rewrite EQ. simpl. rewrite EQ1; simpl.
+  rewrite TLBS. simpl. rewrite H2.
+  all: simpl; auto.
+Qed.
+
+(* Bringing theorems (A), (B) and (C) together, for the case of the absence of builtin instruction *)
+(* This more general form is easier to prove, but the actual theorem is step_simulation_bblock further below *)
+Lemma step_simulation_bblock':
+  forall sf f sp bb bb' bb'' rs m rs' m' s'' c S1,
+  bb' = mb_remove_header bb ->
+  body_step ge sf f sp (Machblock.body bb') rs m rs' m' ->
+  bb'' = mb_remove_body bb' ->
+  (forall ef args res, MB.exit bb'' <> Some (MBbuiltin ef args res)) ->
+  exit_step return_address_offset ge (Machblock.exit bb'') (Machblock.State sf f sp (bb'' :: c) rs' m') E0 s'' ->
+  match_states (Machblock.State sf f sp (bb :: c) rs m) S1 ->
+  exists S2 : state, plus (step lk) tge S1 E0 S2 /\ match_states s'' S2.
+Proof.
+  intros until S1. intros Hbb' BSTEP Hbb'' Hbuiltin ESTEP MS.
+  destruct (mbsize bb) eqn:SIZE.
+  - apply mbsize_eqz in SIZE. destruct SIZE as (Hbody & Hexit).
+    destruct bb as [hd bdy ex]; simpl in *; subst.
+    inv MS. inv AT. exploit transl_blocks_nonil; eauto. intros (tbb & tc' & Htc). subst. rename tc' into tc.
+    monadInv H2. simpl in *. inv ESTEP. inv BSTEP.
+    eexists. split.
+    + eapply plus_one.
+      exploit functions_translated; eauto. intros (tf0 & FIND' & TRANSF'). monadInv TRANSF'.
+      assert (x = tf). { unfold transf_function in H1. monadInv H1.
+      destruct (zlt Ptrofs.max_unsigned (size_blocks (fn_blocks x0))); try congruence. }
+      subst x.
+      eapply exec_step_internal; eauto. eapply find_bblock_tail; eauto.
+      unfold exec_bblock. simpl.
+      eexists; eexists; split; eauto.
+      econstructor.
+    + econstructor.
+      1,2,3: eauto.
+      *
+      unfold incrPC. rewrite Pregmap.gss.
+      unfold Val.offset_ptr. rewrite <- H.
+    assert (NOOV: size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned).
+      { eapply transf_function_no_overflow; eauto. }
+    econstructor; eauto.
+      generalize (code_tail_next_int _ _ _ _ NOOV H3). intro CT1. eauto.
+      *
+    eapply agree_exten; eauto. intros. unfold incrPC. rewrite Pregmap.gso; auto.
+    unfold data_preg in H2. destruct r; try congruence.
+   *
+    intros. discriminate.
+  - subst. exploit mbsize_neqz. { instantiate (1 := bb). rewrite SIZE. discriminate. }
+    intros Hnotempty.
+
+    (* initial setting *)
+    exploit match_state_codestate.
+      2: eapply Hnotempty.
+      all: eauto.
+    intros (cs1 & fb & f0 & tbb & tc & ep & MCS & MAS & FIND & TLBS & Hbody & Hexit & Hcur & Hrem & Hpstate).
+
+    (* step_simu_header part *)
+    assert (exists rs1 m1, pstate cs1 = State rs1 m1). { inv MAS. simpl. eauto. }
+    destruct H as (rs1 & m1 & Hpstate2). subst.
+    assert (f = fb). { inv MCS. auto. } subst fb.
+    all: admit.
+    (*exploit step_simu_header.
+      2: eapply MCS.
+      all: eauto.
+    intros (cs1' & EXEH & MCS2).
+
+    (* step_simu_body part *)
+    assert (Hpstate': pstate cs1' = pstate cs1). { inv EXEH; auto. }
+    exploit step_simu_body.
+      3: eapply BSTEP.
+      4: eapply MCS2.
+      all: eauto. rewrite Hpstate'. eauto.
+    intros (rs2 & m2 & cs2 & ep' & Hcs2 & EXEB & MCS').
+
+    (* step_simu_control part *)
+    assert (exists tf, Genv.find_funct_ptr tge f = Some (Internal tf)).
+    { exploit functions_translated; eauto. intros (tf & FIND' & TRANSF'). monadInv TRANSF'. eauto. }
+    destruct H as (tf & FIND').
+    assert (exists tex, pbody2 cs1 = extract_basic tex /\ pctl cs1 = extract_ctl tex).
+    { inv MAS. simpl in *. eauto. }
+    destruct H as (tex & Hpbody2 & Hpctl).
+    inv EXEH. simpl in *.
+    subst. exploit step_simu_control.
+      9: eapply MCS'. all: simpl.
+      10: eapply ESTEP.
+      all: simpl; eauto.
+      rewrite Hpbody2. rewrite Hpctl.
+      { inv MAS; simpl in *. inv Hpstate2. eapply match_asmstate_some; eauto.
+        erewrite exec_body_pc; eauto. }
+    intros (rs3 & m3 & rs4 & m4 & EXEB' & EXECTL' & MS').
+
+    (* bringing the pieces together *)
+    exploit exec_body_trans.
+      eapply EXEB.
+      eauto.
+    intros EXEB2.
+    exploit exec_body_control; eauto.
+    rewrite <- Hpbody2 in EXEB2. rewrite <- Hbody in EXEB2. eauto.
+    rewrite Hexit. rewrite Hpctl. eauto.
+    intros EXECB. inv EXECB.
+    exists (State rs4 m4).
+    split; auto. eapply plus_one. rewrite Hpstate2.
+    assert (exists ofs, rs1 PC = Vptr f ofs).
+    { rewrite Hpstate2 in MAS. inv MAS. simpl in *. eauto. }
+    destruct H0 as (ofs & Hrs1pc).
+    eapply exec_step_internal; eauto.
+
+    (* proving the initial find_bblock *)
+    rewrite Hpstate2 in MAS. inv MAS. simpl in *. 
+    assert (f1 = f0) by congruence. subst f0.
+    rewrite PCeq in Hrs1pc. inv Hrs1pc.
+    exploit functions_translated; eauto. intros (tf1 & FIND'' & TRANS''). rewrite FIND' in FIND''.
+    inv FIND''. monadInv TRANS''. rewrite TRANSF0 in EQ. inv EQ.
+    eapply find_bblock_tail; eauto.
+Qed.*)
+Admitted.
+
+Theorem step_simulation_bblock:
+  forall sf f sp bb ms m ms' m' S2 c,
+  body_step ge sf f sp (Machblock.body bb) ms m ms' m' ->
+  (forall ef args res, MB.exit bb <> Some (MBbuiltin ef args res)) ->
+  exit_step return_address_offset ge (Machblock.exit bb) (Machblock.State sf f sp (bb :: c) ms' m') E0 S2 ->
+  forall S1', match_states (Machblock.State sf f sp (bb :: c) ms m) S1' ->
+  exists S2' : state, plus (step lk) tge S1' E0 S2' /\ match_states S2 S2'.
+Proof.
+  intros until c. intros BSTEP Hbuiltin ESTEP S1' MS.
+  eapply step_simulation_bblock'; eauto.
+  all: destruct bb as [hd bdy ex]; simpl in *; eauto.
+  inv ESTEP.
+  - econstructor. inv H; try (econstructor; eauto; fail).
+  - econstructor.
+Qed.
+
+(* Measure to prove finite stuttering, see the other backends *)
+Definition measure (s: MB.state) : nat :=
+  match s with
+  | MB.State _ _ _ _ _ _ => 0%nat
+  | MB.Callstate _ _ _ _ => 0%nat
+  | MB.Returnstate _ _ _ => 1%nat
+  end.
+
+(* The actual MB.step/AB.step simulation, using the above theorems, plus extra proofs
+   for the internal and external function cases *)
+Theorem step_simulation:
+  forall S1 t S2, MB.step return_address_offset ge S1 t S2 ->
+  forall S1' (MS: match_states S1 S1'),
+  (exists S2', plus (step lk) tge S1' t S2' /\ match_states S2 S2')
+  \/ (measure S2 < measure S1 /\ t = E0 /\ match_states S2 S1')%nat.
+Proof.
+  induction 1; intros.
+
+- (* bblock *)
+  left. destruct (Machblock.exit bb) eqn:MBE; try destruct c0.
+  all: admit.
+all: admit.
+Admitted.
+  (*all: try(inversion H0; subst; inv H2; eapply step_simulation_bblock; 
+            try (rewrite MBE; try discriminate); eauto).
+  + (* MBbuiltin *)
+    destruct (MB.body bb) eqn:MBB.
+    * inv H. eapply step_simulation_builtin; eauto. rewrite MBE. eauto.
+    * eapply match_states_split_builtin in MS; eauto.
+        2: rewrite MBB; discriminate.
+      simpl split in MS.
+      rewrite <- MBB in H.
+      remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb1.
+      assert (MB.body bb = MB.body bb1). { subst. simpl. auto. }
+      rewrite H1 in H. subst.
+      exploit step_simulation_bblock. eapply H.
+        discriminate.
+        simpl. constructor.
+        eauto.
+      intros (S2' & PLUS1 & MS').
+      rewrite MBE in MS'.
+      assert (exit_step return_address_offset ge (Some (MBbuiltin e l b)) 
+              (MB.State sf f sp ({| MB.header := nil; MB.body := nil; MB.exit := Some (MBbuiltin e l b) |}::c) 
+                rs' m') t s').
+      { inv H0. inv H3. econstructor. econstructor; eauto. }
+      exploit step_simulation_builtin.
+        4: eapply MS'.
+        all: simpl; eauto.
+      intros (S3' & PLUS'' & MS'').
+      exists S3'. split; eauto.
+      eapply plus_trans. eapply PLUS1. eapply PLUS''. eauto.
+  + inversion H0. subst. eapply step_simulation_bblock; try (rewrite MBE; try discriminate); eauto.
+
+- (* internal function *)
+  inv MS.
+  exploit functions_translated; eauto. intros [tf [A B]]. monadInv B.
+  generalize EQ; intros EQ'. monadInv EQ'.
+  destruct (zlt Ptrofs.max_unsigned (size_blocks x0.(fn_blocks))); inversion EQ1. clear EQ1. subst x0.
+  unfold Mach.store_stack in *.
+  exploit Mem.alloc_extends. eauto. eauto. apply Z.le_refl. apply Z.le_refl.
+  intros [m1' [C D]].
+  exploit Mem.storev_extends. eexact D. eexact H1. eauto. eauto.
+  intros [m2' [F G]].
+  simpl chunk_of_type in F.
+  exploit Mem.storev_extends. eexact G. eexact H2. eauto. eauto.
+  intros [m3' [P Q]].
+  (* Execution of function prologue *)
+  monadInv EQ0.
+  set (tfbody := make_prologue f x0) in *.
+  set (tf := {| fn_sig := MB.fn_sig f; fn_blocks := tfbody |}) in *.
+  set (rs2 := rs0#FP <- (parent_sp s) #SP <- sp #RTMP <- Vundef).
+  exploit (Pget_correct tge GPRA RA nil rs2 m2'); auto.
+  intros (rs' & U' & V').
+  exploit (storeind_ptr_correct tge SP (fn_retaddr_ofs f) GPRA nil rs' m2').
+  { rewrite chunk_of_Tptr in P.
+    assert (rs' GPRA = rs0 RA). { apply V'. }
+    assert (rs' SP = rs2 SP). { apply V'; discriminate. }
+    rewrite H4. rewrite H3.
+    rewrite ATLR.
+    change (rs2 SP) with sp. eexact P. }
+  intros (rs3 & U & V).
+  assert (EXEC_PROLOGUE: exists rs3',
+            exec_straight_blocks tge tf
+              tf.(fn_blocks) rs0 m'
+              x0 rs3' m3'
+          /\ forall r, r <> PC -> rs3' r = rs3 r).
+  { eexists. split.
+    - change (fn_blocks tf) with tfbody; unfold tfbody.
+      econstructor; eauto. unfold exec_bblock. simpl exec_body.
+      rewrite C. fold sp. rewrite <- (sp_val _ _ _ AG). rewrite chunk_of_Tptr in F. simpl in F. rewrite F.
+      Simpl. unfold parexec_store_offset. rewrite Ptrofs.of_int64_to_int64. unfold eval_offset.
+      rewrite chunk_of_Tptr in P. Simpl. rewrite ATLR. unfold Mptr in P. assert (Archi.ptr64 = true) by auto. 2: auto. rewrite H3 in P. rewrite P.
+      simpl. apply next_sep; eauto. reflexivity.
+    - intros. destruct V' as (V'' & V'). destruct r.
+      + Simpl.
+        destruct (gpreg_eq g0 GPR16). { subst. Simpl. rewrite V; try discriminate. rewrite V''. subst rs2. Simpl. }
+        destruct (gpreg_eq g0 GPR32). { subst. Simpl. rewrite V; try discriminate. rewrite V'; try discriminate. subst rs2. Simpl. }
+        destruct (gpreg_eq g0 GPR12). { subst. Simpl. rewrite V; try discriminate. rewrite V'; try discriminate. subst rs2. Simpl. }
+        destruct (gpreg_eq g0 GPR17). { subst. Simpl. rewrite V; try discriminate. rewrite V'; try discriminate. subst rs2. Simpl. }
+        Simpl. rewrite V; try discriminate. rewrite V'; try discriminate. subst rs2. Simpl. { destruct g0; try discriminate. contradiction. }
+      + Simpl. rewrite V; try discriminate. rewrite V'; try discriminate. subst rs2. Simpl.
+      + contradiction.
+  } destruct EXEC_PROLOGUE as (rs3' & EXEC_PROLOGUE & Heqrs3').
+  exploit exec_straight_steps_2; eauto using functions_transl.
+  simpl fn_blocks. simpl fn_blocks in g. omega. constructor.
+  intros (ofs' & X & Y).                    
+  left; exists (State rs3' m3'); split.
+  eapply exec_straight_steps_1; eauto.
+  simpl fn_blocks. simpl fn_blocks in g. omega.
+  constructor.
+  econstructor; eauto.
+  rewrite X; econstructor; eauto. 
+  apply agree_exten with rs2; eauto with asmgen.
+  unfold rs2. 
+  apply agree_set_other; auto with asmgen.
+  apply agree_change_sp with (parent_sp s). 
+  apply agree_undef_regs with rs0. auto.
+Local Transparent destroyed_at_function_entry.
+  simpl; intros; Simpl.
+  unfold sp; congruence.
+
+  intros.
+  assert (r <> RTMP). { contradict H3; rewrite H3; unfold data_preg; auto. }
+  rewrite Heqrs3'. Simpl. rewrite V. inversion V'. rewrite H6. auto.
+  assert (r <> GPRA). { contradict H3; rewrite H3; unfold data_preg; auto. }
+  assert (forall r : preg, r <> PC -> r <> GPRA -> rs' r = rs2 r). { apply V'. }
+  contradict H3; rewrite H3; unfold data_preg; auto.
+  contradict H3; rewrite H3; unfold data_preg; auto.
+  contradict H3; rewrite H3; unfold data_preg; auto.
+  contradict H3; rewrite H3; unfold data_preg; auto.
+  intros. rewrite Heqrs3'. rewrite V by auto with asmgen.
+  assert (forall r : preg, r <> PC -> r <> GPRA -> rs' r = rs2 r). { apply V'. }
+  rewrite H4 by auto with asmgen. reflexivity. discriminate.
+
+- (* external function *)
+  inv MS.
+  exploit functions_translated; eauto.
+  intros [tf [A B]]. simpl in B. inv B.
+  exploit extcall_arguments_match; eauto.
+  intros [args' [C D]].
+  exploit external_call_mem_extends; eauto.
+  intros [res' [m2' [P [Q [R S]]]]].
+  left; econstructor; split.
+  apply plus_one. eapply exec_step_external; eauto.
+  eapply external_call_symbols_preserved; eauto. apply senv_preserved.
+  econstructor; eauto.
+  unfold loc_external_result.
+  apply agree_set_other; auto.
+  apply agree_set_pair; auto.
+  apply agree_undef_caller_save_regs; auto.
+
+- (* return *) 
+  inv MS.
+  inv STACKS. simpl in *.
+  right. split. omega. split. auto.
+  rewrite <- ATPC in H5.
+  econstructor; eauto. congruence.
+Qed.*)
+
+Lemma transf_initial_states:
+  forall st1, MB.initial_state prog st1 ->
+  exists st2, AB.initial_state tprog st2 /\ match_states st1 st2.
+Proof.
+  intros. inversion H. unfold ge0 in *.
+  econstructor; split.
+  econstructor.
+  eapply (Genv.init_mem_transf_partial TRANSF); eauto.
+  replace (Genv.symbol_address (Genv.globalenv tprog) (prog_main tprog) Ptrofs.zero)
+     with (Vptr fb Ptrofs.zero).
+  econstructor; eauto.
+  constructor.
+  apply Mem.extends_refl.
+  split. auto. simpl. unfold Vnullptr; destruct Archi.ptr64; congruence.
+  intros. rewrite Mach.Regmap.gi. auto.
+  unfold Genv.symbol_address.
+  rewrite (match_program_main TRANSF).
+  rewrite symbols_preserved.
+  unfold ge; rewrite H1. auto.
+Qed.
+
+Lemma transf_final_states:
+  forall st1 st2 r,
+  match_states st1 st2 -> MB.final_state st1 r -> AB.final_state st2 r.
+Proof.
+  intros. inv H0. inv H. constructor. assumption.
+  compute in H1. inv H1.
+  generalize (preg_val _ _ _ R0 AG). rewrite H2. intros LD; inv LD. auto.
+Qed.
+
 Definition return_address_offset : Machblock.function -> Machblock.code -> ptrofs -> Prop := 
   Asmblockgenproof0.return_address_offset.
 
 Lemma transf_program_correct:
   forward_simulation (MB.semantics return_address_offset prog) (AB.semantics lk tprog).
+Proof.
+  eapply forward_simulation_star with (measure := measure).
+  - apply senv_preserved.
+  - eexact transf_initial_states.
+  - eexact transf_final_states.
+  - exact step_simulation.
 Admitted.
 
 End PRESERVATION.
diff --git a/aarch64/Asmblockgenproof0.v b/aarch64/Asmblockgenproof0.v
index 0187a494..69d6037c 100644
--- a/aarch64/Asmblockgenproof0.v
+++ b/aarch64/Asmblockgenproof0.v
@@ -42,6 +42,31 @@ Require Import Asmblockprops.
 Module MB:=Machblock.
 Module AB:=Asmblock.
 
+(** * Agreement between Mach registers and processor registers *)
+
+Record agree (ms: Mach.regset) (sp: val) (rs: AB.regset) : Prop := mkagree {
+  agree_sp: rs#SP = sp;
+  agree_sp_def: sp <> Vundef;
+  agree_mregs: forall r: mreg, Val.lessdef (ms r) (rs#(preg_of r))
+}.
+
+Lemma agree_exten:
+  forall ms sp rs rs',
+  agree ms sp rs ->
+  (forall r, data_preg r = true -> rs'#r = rs#r) ->
+  agree ms sp rs'.
+Proof.
+  intros. destruct H. split; auto.
+  rewrite H0; auto. auto.
+  intros. rewrite H0; auto. apply preg_of_data.
+Qed.
+
+Lemma preg_val:
+  forall ms sp rs r, agree ms sp rs -> Val.lessdef (ms r) rs#(preg_of r).
+Proof.
+  intros. destruct H. auto.
+Qed.
+
 Inductive code_tail: Z -> bblocks -> bblocks -> Prop :=
   | code_tail_0: forall c,
       code_tail 0 c c
@@ -211,4 +236,94 @@ Proof.
   + exists Ptrofs.zero; red; intros. congruence.
 Qed.
 
-End RETADDR_EXISTS.
\ No newline at end of file
+End RETADDR_EXISTS.
+
+(** [transl_code_at_pc pc fb f c ep tf tc] holds if the code pointer [pc] points
+  within the Asmblock code generated by translating Machblock function [f],
+  and [tc] is the tail of the generated code at the position corresponding
+  to the code pointer [pc]. *)
+
+Inductive transl_code_at_pc (ge: MB.genv):
+    val -> block -> MB.function -> MB.code -> bool -> AB.function -> AB.bblocks -> Prop :=
+  transl_code_at_pc_intro:
+    forall b ofs f c ep tf tc,
+    Genv.find_funct_ptr ge b = Some(Internal f) ->
+    transf_function f = Errors.OK tf ->
+    transl_blocks f c ep = OK tc ->
+    code_tail (Ptrofs.unsigned ofs) (fn_blocks tf) tc ->
+    transl_code_at_pc ge (Vptr b ofs) b f c ep tf tc.
+
+Remark code_tail_no_bigger:
+  forall pos c1 c2, code_tail pos c1 c2 -> (length c2 <= length c1)%nat.
+Proof.
+  induction 1; simpl; omega.
+Qed.
+
+Remark code_tail_unique:
+  forall fn c pos pos',
+  code_tail pos fn c -> code_tail pos' fn c -> pos = pos'.
+Proof.
+  induction fn; intros until pos'; intros ITA CT; inv ITA; inv CT; auto.
+  generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; omega.
+  generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; omega.
+  f_equal. eauto.
+Qed.
+
+Lemma return_address_offset_correct:
+  forall ge b ofs fb f c tf tc ofs',
+  transl_code_at_pc ge (Vptr b ofs) fb f c false tf tc ->
+  return_address_offset f c ofs' ->
+  ofs' = ofs.
+Proof.
+  intros. inv H. red in H0.
+  exploit code_tail_unique. eexact H12. eapply H0; eauto. intro.
+  rewrite <- (Ptrofs.repr_unsigned ofs).
+  rewrite <- (Ptrofs.repr_unsigned ofs').
+  congruence.
+Qed.
+
+(** * Properties of the Machblock call stack *)
+
+Section MATCH_STACK.
+
+Variable ge: MB.genv.
+
+Inductive match_stack: list MB.stackframe -> Prop :=
+  | match_stack_nil:
+      match_stack nil
+  | match_stack_cons: forall fb sp ra c s f tf tc,
+      Genv.find_funct_ptr ge fb = Some (Internal f) ->
+      transl_code_at_pc ge ra fb f c false tf tc ->
+      sp <> Vundef ->
+      match_stack s ->
+      match_stack (Stackframe fb sp ra c :: s).
+
+Lemma parent_sp_def: forall s, match_stack s -> parent_sp s <> Vundef.
+Proof.
+  induction 1; simpl.
+  unfold Vnullptr; destruct Archi.ptr64; congruence.
+  auto.
+Qed.
+
+Lemma parent_ra_def: forall s, match_stack s -> parent_ra s <> Vundef.
+Proof.
+  induction 1; simpl.
+  unfold Vnullptr; destruct Archi.ptr64; congruence.
+  inv H0. congruence.
+Qed.
+
+Lemma lessdef_parent_sp:
+  forall s v,
+  match_stack s -> Val.lessdef (parent_sp s) v -> v = parent_sp s.
+Proof.
+  intros. inv H0. auto. exploit parent_sp_def; eauto. tauto.
+Qed.
+
+Lemma lessdef_parent_ra:
+  forall s v,
+  match_stack s -> Val.lessdef (parent_ra s) v -> v = parent_ra s.
+Proof.
+  intros. inv H0. auto. exploit parent_ra_def; eauto. tauto.
+Qed.
+
+End MATCH_STACK.
\ No newline at end of file