[WIP: Coq compilation broken] Stub for Asmgen

8 files changed, 2370 insertions, 2768 deletions

diff --git a/aarch64/Asm.v b/aarch64/Asm.v
index 47cd3051..0959d9ca 100644
--- a/aarch64/Asm.v
+++ b/aarch64/Asm.v
@@ -10,149 +10,28 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-(** Abstract syntax and semantics for AArch64 assembly language *)
+(** Abstract syntax and semantics for AArch64 assembly language 
+
+
+W.r.t Asmblock, this is a "flat" syntax and semantics of "Aarch64" assembly:
+  - without the basic block structure
+  - without the hierarchy of instructions.
+
+
+TODO: with respect to original file, remove parts of the syntax/semantics 
+that have been already defined in Asmblock.
+
+*)
 
 Require Import Coqlib Zbits Maps.
 Require Import AST Integers Floats.
 Require Import Values Memory Events Globalenvs Smallstep.
 Require Import Locations Conventions.
 Require Stacklayout.
+Require Import OptionMonad Asmblock.
 
 (** * Abstract syntax *)
 
-(** Integer registers, floating-point registers. *)
-
-(** In assembly files, [Xn] denotes the full 64-bit register
-    and [Wn] the low 32 bits of [Xn]. *)
-
-Inductive ireg: Type :=
-  | X0  | X1  | X2  | X3  | X4  | X5  |  X6  | X7
-  | X8  | X9  | X10 | X11 | X12 | X13 |  X14 | X15
-  | X16 | X17 | X18 | X19 | X20 | X21 |  X22 | X23
-  | X24 | X25 | X26 | X27 | X28 | X29 |  X30.
-
-Inductive ireg0: Type :=
-  | RR0 (r: ireg) | XZR.
-
-Inductive iregsp: Type :=
-  | RR1 (r: ireg) | XSP.
-
-Coercion RR0: ireg >-> ireg0.
-Coercion RR1: ireg >-> iregsp.
-
-Lemma ireg_eq: forall (x y: ireg), {x=y} + {x<>y}.
-Proof. decide equality. Defined.
-
-(** In assembly files, [Dn] denotes the low 64-bit of a vector register,
-    and [Sn] the low 32 bits. *)
-
-Inductive freg: Type :=
-  | D0  | D1  | D2  | D3  | D4  | D5  |  D6  | D7
-  | D8  | D9  | D10 | D11 | D12 | D13 |  D14 | D15
-  | D16 | D17 | D18 | D19 | D20 | D21 |  D22 | D23
-  | D24 | D25 | D26 | D27 | D28 | D29 |  D30 | D31.
-
-Lemma freg_eq: forall (x y: freg), {x=y} + {x<>y}.
-Proof. decide equality. Defined.
-
-(** Bits in the condition register. *)
-
-Inductive crbit: Type :=
-  | CN: crbit    (**r negative *)
-  | CZ: crbit    (**r zero *)
-  | CC: crbit    (**r carry *)
-  | CV: crbit.   (**r overflow *)
-
-Lemma crbit_eq: forall (x y: crbit), {x=y} + {x<>y}.
-Proof. decide equality. Defined.
-
-(** We model the following registers of the ARM architecture. *)
-
-Inductive preg: Type :=
-  | IR: ireg -> preg   (**r 64- or 32-bit integer registers *)
-  | FR: freg -> preg   (**r double- or single-precision float registers *)
-  | CR: crbit -> preg  (**r bits in the condition register *)
-  | SP: preg           (**r register X31 used as stack pointer *)
-  | PC: preg.          (**r program counter *)
-
-Coercion IR: ireg >-> preg.
-Coercion FR: freg >-> preg.
-Coercion CR: crbit >-> preg.
-
-Lemma preg_eq: forall (x y: preg), {x=y} + {x<>y}.
-Proof. decide equality. apply ireg_eq. apply freg_eq. apply crbit_eq. Defined.
-
-Module PregEq.
-  Definition t := preg.
-  Definition eq := preg_eq.
-End PregEq.
-
-Module Pregmap := EMap(PregEq).
-
-Definition preg_of_iregsp (r: iregsp) : preg :=
-  match r with RR1 r => IR r | XSP => SP end.
-
-Coercion preg_of_iregsp: iregsp >-> preg.
-
-(** Conventional name for return address ([RA]) *)
-
-Notation "'RA'" := X30 (only parsing) : asm.
-
-(** The instruction set.  Most instructions correspond exactly to
-  actual AArch64 instructions. See the ARM reference manuals for more
-  details.  Some instructions, described below, are
-  pseudo-instructions: they expand to canned instruction sequences
-  during the printing of the assembly code.  *)
-
-Definition label := positive.
-
-Inductive isize: Type :=
-  | W                                                (**r 32-bit integer operation *)
-  | X.                                               (**r 64-bit integer operation *)
-
-Inductive fsize: Type :=
-  | S                                                (**r 32-bit, single-precision FP operation *)
-  | D.                                               (**r 64-bit, double-precision FP operation *)
-
-Inductive testcond : Type :=
-  | TCeq: testcond    (**r equal *)
-  | TCne: testcond    (**r not equal *)
-  | TChs: testcond    (**r unsigned higher or same *)
-  | TClo: testcond    (**r unsigned lower *)
-  | TCmi: testcond    (**r negative *)
-  | TCpl: testcond    (**r positive *)
-  | TChi: testcond    (**r unsigned higher *)
-  | TCls: testcond    (**r unsigned lower or same *)
-  | TCge: testcond    (**r signed greater or equal *)
-  | TClt: testcond    (**r signed less than *)
-  | TCgt: testcond    (**r signed greater *)
-  | TCle: testcond.   (**r signed less than or equal *)
-
-Inductive addressing: Type :=
-  | ADimm (base: iregsp) (n: int64)                  (**r base plus immediate offset *)
-  | ADreg (base: iregsp) (r: ireg)                   (**r base plus reg *)
-  | ADlsl (base: iregsp) (r: ireg) (n: int)          (**r base plus reg LSL n *)
-  | ADsxt (base: iregsp) (r: ireg) (n: int)          (**r base plus SIGN-EXT(reg) LSL n *)
-  | ADuxt (base: iregsp) (r: ireg) (n: int)          (**r base plus ZERO-EXT(reg) LSL n *)
-  | ADadr (base: iregsp) (id: ident) (ofs: ptrofs)   (**r base plus low address of [id + ofs] *)
-  | ADpostincr (base: iregsp) (n: int64).            (**r base plus offset; base is updated after *)
-
-Inductive shift_op: Type :=
-  | SOnone
-  | SOlsl (n: int)
-  | SOlsr (n: int)
-  | SOasr (n: int)
-  | SOror (n: int).
-
-Inductive extend_op: Type :=
-  | EOsxtb (n: int)
-  | EOsxth (n: int)
-  | EOsxtw (n: int)
-  | EOuxtb (n: int)
-  | EOuxth (n: int)
-  | EOuxtw (n: int)
-  | EOuxtx (n: int).
-
 Inductive instruction: Type :=
   (** Branches *)
   | Pb (lbl: label)                                                   (**r branch *)
@@ -307,65 +186,8 @@ Definition code := list instruction.
 Record function : Type := mkfunction { fn_sig: signature; fn_code: code }.
 Definition fundef := AST.fundef function.
 Definition program := AST.program fundef unit.
-
-(** * Operational semantics *)
-
-(** The semantics operates over a single mapping from registers
-  (type [preg]) to values.  We maintain (but do not enforce)
-  the convention that integer registers are mapped to values of
-  type [Tint], float registers to values of type [Tfloat],
-  and condition bits to either [Vzero] or [Vone]. *)
-
-Definition regset := Pregmap.t val.
 Definition genv := Genv.t fundef unit.
 
-(** The value of an [ireg0] is either the value of the integer register,
-    or 0. *)
-
-Definition ir0w (rs: regset) (r: ireg0) : val :=
-  match r with RR0 r => rs (IR r) | XZR => Vint Int.zero end.
-Definition ir0x (rs: regset) (r: ireg0) : val :=
-  match r with RR0 r => rs (IR r) | XZR => Vlong Int64.zero end.
-
-(** Concise notations for accessing and updating the values of registers. *)
-
-Notation "a # b" := (a b) (at level 1, only parsing) : asm.
-Notation "a # b <- c" := (Pregmap.set b c a) (at level 1, b at next level) : asm.
-Notation "a ## b" := (ir0w a b) (at level 1, only parsing) : asm.
-Notation "a ### b" := (ir0x a b) (at level 1, only parsing) : asm.
-
-Open Scope asm.
-
-(** Undefining some registers *)
-
-Fixpoint undef_regs (l: list preg) (rs: regset) : regset :=
-  match l with
-  | nil => rs
-  | r :: l' => undef_regs l' (rs#r <- Vundef)
-  end.
-
-(** Undefining the condition codes *)
-
-Definition undef_flags (rs: regset) : regset :=
-  fun r => match r with CR _ => Vundef | _ => rs r end.
-
-(** Assigning a register pair *)
-
-Definition set_pair (p: rpair preg) (v: val) (rs: regset) : regset :=
-  match p with
-  | One r => rs#r <- v
-  | Twolong rhi rlo => rs#rhi <- (Val.hiword v) #rlo <- (Val.loword v)
-  end.
-
-(** Assigning the result of a builtin *)
-
-Fixpoint set_res (res: builtin_res preg) (v: val) (rs: regset) : regset :=
-  match res with
-  | BR r => rs#r <- v
-  | BR_none => rs
-  | BR_splitlong hi lo => set_res lo (Val.loword v) (set_res hi (Val.hiword v) rs)
-  end.
-
 (** The two functions below axiomatize how the linker processes
   symbolic references [symbol + offset].  It computes the
   difference between the address and the PC, and splits it into:
@@ -385,6 +207,8 @@ Axiom symbol_high_low:
   forall (ge: genv) (id: ident) (ofs: ptrofs),
   Val.addl (symbol_high ge id ofs) (symbol_low ge id ofs) = Genv.symbol_address ge id ofs.
 
+(** * Operational semantics *)
+
 Section RELSEM.
 
 Variable ge: genv.
@@ -419,19 +243,6 @@ Fixpoint label_pos (lbl: label) (pos: Z) (c: code) {struct c} : option Z :=
       if is_label lbl instr then Some (pos + 1) else label_pos lbl (pos + 1) c'
   end.
 
-(** The semantics is purely small-step and defined as a function
-  from the current state (a register set + a memory state)
-  to either [Next rs' m'] where [rs'] and [m'] are the updated register
-  set and memory state after execution of the instruction at [rs#PC],
-  or [Stuck] if the processor is stuck. *)
-
-Inductive outcome: Type :=
-  | Next: regset -> mem -> outcome
-  | Stuck: outcome.
-
-(** Manipulations over the [PC] register: continuing with the next
-  instruction ([nextinstr]) or branching to a label ([goto_label]). *)
-
 Definition nextinstr (rs: regset) :=
   rs#PC <- (Val.offset_ptr rs#PC Ptrofs.one).
 
@@ -445,88 +256,6 @@ Definition goto_label (f: function) (lbl: label) (rs: regset) (m: mem) :=
     end
   end.
 
-(** Testing a condition *)
-
-Definition eval_testcond (c: testcond) (rs: regset) : option bool :=
-  match c with
-  | TCeq =>                             (**r equal *)
-      match rs#CZ with
-      | Vint n => Some (Int.eq n Int.one)
-      | _ => None
-      end
-  | TCne =>                             (**r not equal *)
-      match rs#CZ with
-      | Vint n => Some (Int.eq n Int.zero)
-      | _ => None
-      end
-  | TClo =>                             (**r unsigned less than  *)
-      match rs#CC with
-      | Vint n => Some (Int.eq n Int.zero)
-      | _ => None
-      end
-  | TCls =>                             (**r unsigned less or equal *)
-      match rs#CC, rs#CZ with
-      | Vint c, Vint z => Some (Int.eq c Int.zero || Int.eq z Int.one)
-      | _, _ => None
-      end
-  | TChs =>                             (**r unsigned greater or equal *)
-      match rs#CC with
-      | Vint n => Some (Int.eq n Int.one)
-      | _ => None
-      end
-  | TChi =>                             (**r unsigned greater *)
-      match rs#CC, rs#CZ with
-      | Vint c, Vint z => Some (Int.eq c Int.one && Int.eq z Int.zero)
-      | _, _ => None
-      end
-  | TClt =>                             (**r signed less than *)
-      match rs#CV, rs#CN with
-      | Vint o, Vint s => Some (Int.eq (Int.xor o s) Int.one)
-      | _, _ => None
-      end
-  | TCle =>                             (**r signed less or equal *)
-      match rs#CV, rs#CN, rs#CZ with
-      | Vint o, Vint s, Vint z => Some (Int.eq (Int.xor o s) Int.one || Int.eq z Int.one)
-      | _, _, _ => None
-      end
-  | TCge =>                             (**r signed greater or equal *)
-      match rs#CV, rs#CN with
-      | Vint o, Vint s => Some (Int.eq (Int.xor o s) Int.zero)
-      | _, _ => None
-      end
-  | TCgt =>                             (**r signed greater *)
-      match rs#CV, rs#CN, rs#CZ with
-      | Vint o, Vint s, Vint z => Some (Int.eq (Int.xor o s) Int.zero && Int.eq z Int.zero)
-      | _, _, _ => None
-      end
-  | TCpl =>                             (**r positive *)
-      match rs#CN with
-      | Vint n => Some (Int.eq n Int.zero)
-      | _ => None
-      end
-  | TCmi =>                             (**r negative *)
-      match rs#CN with
-      | Vint n => Some (Int.eq n Int.one)
-      | _ => None
-      end
-  end.
-
-(** Integer "is zero?" test *)
-
-Definition eval_testzero (sz: isize) (v: val) (m: mem): option bool :=
-  match sz with
-  | W => Val.cmpu_bool (Mem.valid_pointer m) Ceq v (Vint Int.zero)
-  | X => Val.cmplu_bool (Mem.valid_pointer m) Ceq v (Vlong Int64.zero)
-  end.
-
-(** Integer "bit is set?" test *)
-
-Definition eval_testbit (sz: isize) (v: val) (n: int): option bool :=
-  match sz with
-  | W => Val.cmp_bool Cne (Val.and v (Vint (Int.shl Int.one n))) (Vint Int.zero)
-  | X => Val.cmpl_bool Cne (Val.andl v (Vlong (Int64.shl' Int64.one n))) (Vlong Int64.zero)
-  end.
-
 (** Evaluating an addressing mode *)
 
 Definition eval_addressing (a: addressing) (rs: regset): val :=
@@ -557,130 +286,6 @@ Definition exec_store (chunk: memory_chunk)
   | Some m' => Next (nextinstr rs) m'
   end.
 
-(** Comparisons *)
-
-Definition compare_int (rs: regset) (v1 v2: val) (m: mem) :=
-  rs#CN <- (Val.negative (Val.sub v1 v2))
-    #CZ <- (Val.cmpu (Mem.valid_pointer m) Ceq v1 v2)
-    #CC <- (Val.cmpu (Mem.valid_pointer m) Cge v1 v2)
-    #CV <- (Val.sub_overflow v1 v2).
-
-Definition compare_long (rs: regset) (v1 v2: val) (m: mem) :=
-  rs#CN <- (Val.negativel (Val.subl v1 v2))
-    #CZ <- (Val.maketotal (Val.cmplu (Mem.valid_pointer m) Ceq v1 v2))
-    #CC <- (Val.maketotal (Val.cmplu (Mem.valid_pointer m) Cge v1 v2))
-    #CV <- (Val.subl_overflow v1 v2).
-
-(** Semantics of [fcmp] instructions:
-<<
-==	N=0 Z=1 C=1 V=0
-<	N=1 Z=0 C=0 V=0
->	N=0 Z=0 C=1 V=0
-unord	N=0 Z=0 C=1 V=1
->>
-*)
-
-Definition compare_float (rs: regset) (v1 v2: val) :=
-  match v1, v2 with
-  | Vfloat f1, Vfloat f2 =>
-      rs#CN <- (Val.of_bool (Float.cmp Clt f1 f2))
-        #CZ <- (Val.of_bool (Float.cmp Ceq f1 f2))
-        #CC <- (Val.of_bool (negb (Float.cmp Clt f1 f2)))
-        #CV <- (Val.of_bool (negb (Float.ordered f1 f2)))
-  | _, _ =>
-      rs#CN <- Vundef
-        #CZ <- Vundef
-        #CC <- Vundef
-        #CV <- Vundef
-  end.
-
-Definition compare_single (rs: regset) (v1 v2: val) :=
-  match v1, v2 with
-  | Vsingle f1, Vsingle f2 =>
-      rs#CN <- (Val.of_bool (Float32.cmp Clt f1 f2))
-        #CZ <- (Val.of_bool (Float32.cmp Ceq f1 f2))
-        #CC <- (Val.of_bool (negb (Float32.cmp Clt f1 f2)))
-        #CV <- (Val.of_bool (negb (Float32.ordered f1 f2)))
-  | _, _ =>
-      rs#CN <- Vundef
-        #CZ <- Vundef
-        #CC <- Vundef
-        #CV <- Vundef
-  end.
-
-(** Insertion of bits into an integer *)
-
-Definition insert_in_int (x: val) (y: Z) (pos: Z) (len: Z) : val :=
-  match x with
-  | Vint n => Vint (Int.repr (Zinsert (Int.unsigned n) y pos len))
-  | _ => Vundef
-  end.
-
-Definition insert_in_long (x: val) (y: Z) (pos: Z) (len: Z) : val :=
-  match x with
-  | Vlong n => Vlong (Int64.repr (Zinsert (Int64.unsigned n) y pos len))
-  | _ => Vundef
-  end.
-
-(** Evaluation of shifted operands *)
-
-Definition eval_shift_op_int (v: val) (s: shift_op): val :=
-  match s with
-  | SOnone => v
-  | SOlsl n => Val.shl v (Vint n)
-  | SOlsr n => Val.shru v (Vint n)
-  | SOasr n => Val.shr v (Vint n)
-  | SOror n => Val.ror v (Vint n)
-  end.
-
-Definition eval_shift_op_long (v: val) (s: shift_op): val :=
-  match s with
-  | SOnone => v
-  | SOlsl n => Val.shll v (Vint n)
-  | SOlsr n => Val.shrlu v (Vint n)
-  | SOasr n => Val.shrl v (Vint n)
-  | SOror n => Val.rorl v (Vint n)
-  end.
-
-(** Evaluation of sign- or zero- extended operands *)
-
-Definition eval_extend (v: val) (x: extend_op): val :=
-  match x with
-  | EOsxtb n => Val.shll (Val.longofint (Val.sign_ext 8 v)) (Vint n)
-  | EOsxth n => Val.shll (Val.longofint (Val.sign_ext 16 v)) (Vint n)
-  | EOsxtw n => Val.shll (Val.longofint v) (Vint n)
-  | EOuxtb n => Val.shll (Val.longofintu (Val.zero_ext 8 v)) (Vint n)
-  | EOuxth n => Val.shll (Val.longofintu (Val.zero_ext 16 v)) (Vint n)
-  | EOuxtw n => Val.shll (Val.longofintu v) (Vint n)
-  | EOuxtx n => Val.shll v (Vint n)
-  end.
-
-(** Bit-level conversion from integers to FP numbers *)
-
-Definition float32_of_bits (v: val): val :=
-  match v with
-  | Vint n => Vsingle (Float32.of_bits n)
-  | _ => Vundef
-  end.
-
-Definition float64_of_bits (v: val): val :=
-  match v with
-  | Vlong n => Vfloat (Float.of_bits n)
-  | _ => Vundef
-  end.
-
-(** Execution of a single instruction [i] in initial state
-    [rs] and [m].  Return updated state.  For instructions
-    that correspond to actual AArch64 instructions, the cases are
-    straightforward transliterations of the informal descriptions
-    given in the ARMv8 reference manuals.  For pseudo-instructions,
-    refer to the informal descriptions given above.
-
-    Note that we set to [Vundef] the registers used as temporaries by
-    the expansions of the pseudo-instructions, so that the code we
-    generate cannot use those registers to hold values that must
-    survive the execution of the pseudo-instruction.
-*)
 
 Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : outcome :=
   match i with
@@ -704,13 +309,13 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Pret r =>
       Next (rs#PC <- (rs#r)) m
   | Pcbnz sz r lbl =>
-      match eval_testzero sz rs#r m with
+      match eval_testzero sz rs#r with
       | Some true => Next (nextinstr rs) m
       | Some false => goto_label f lbl rs m
       | None => Stuck
       end
   | Pcbz sz r lbl =>
-      match eval_testzero sz rs#r m with
+      match eval_testzero sz rs#r with
       | Some true => goto_label f lbl rs m
       | Some false => Next (nextinstr rs) m
       | None => Stuck
@@ -778,13 +383,13 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Psubimm X rd r1 n =>
       Next (nextinstr (rs#rd <- (Val.subl rs#r1 (Vlong (Int64.repr n))))) m
   | Pcmpimm W r1 n =>
-      Next (nextinstr (compare_int rs rs#r1 (Vint (Int.repr n)) m)) m
+      Next (nextinstr (compare_int rs rs#r1 (Vint (Int.repr n)))) m
   | Pcmpimm X r1 n =>
-      Next (nextinstr (compare_long rs rs#r1 (Vlong (Int64.repr n)) m)) m
+      Next (nextinstr (compare_long rs rs#r1 (Vlong (Int64.repr n)))) m
   | Pcmnimm W r1 n =>
-      Next (nextinstr (compare_int rs rs#r1 (Vint (Int.neg (Int.repr n))) m)) m
+      Next (nextinstr (compare_int rs rs#r1 (Vint (Int.neg (Int.repr n))))) m
   | Pcmnimm X r1 n =>
-      Next (nextinstr (compare_long rs rs#r1 (Vlong (Int64.neg (Int64.repr n))) m)) m
+      Next (nextinstr (compare_long rs rs#r1 (Vlong (Int64.neg (Int64.repr n))))) m
   (** Move integer register *)
   | Pmov rd r1 =>
       Next (nextinstr (rs#rd <- (rs#r1))) m
@@ -802,9 +407,9 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Porrimm X rd r1 n =>
       Next (nextinstr (rs#rd <- (Val.orl rs###r1 (Vlong (Int64.repr n))))) m
   | Ptstimm W r1 n =>
-      Next (nextinstr (compare_int rs (Val.and rs#r1 (Vint (Int.repr n))) (Vint Int.zero) m)) m
+      Next (nextinstr (compare_int rs (Val.and rs#r1 (Vint (Int.repr n))) (Vint Int.zero))) m
   | Ptstimm X r1 n =>
-      Next (nextinstr (compare_long rs (Val.andl rs#r1 (Vlong (Int64.repr n))) (Vlong Int64.zero) m)) m
+      Next (nextinstr (compare_long rs (Val.andl rs#r1 (Vlong (Int64.repr n))) (Vlong Int64.zero))) m
   (** Move wide immediate *)
   | Pmovz W rd n pos =>
       Next (nextinstr (rs#rd <- (Vint (Int.repr (Z.shiftl n pos))))) m
@@ -850,22 +455,22 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Psub X rd r1 r2 s =>
       Next (nextinstr (rs#rd <- (Val.subl rs###r1 (eval_shift_op_long rs#r2 s)))) m
   | Pcmp W r1 r2 s =>
-      Next (nextinstr (compare_int rs rs##r1 (eval_shift_op_int rs#r2 s) m)) m
+      Next (nextinstr (compare_int rs rs##r1 (eval_shift_op_int rs#r2 s))) m
   | Pcmp X r1 r2 s =>
-      Next (nextinstr (compare_long rs rs###r1 (eval_shift_op_long rs#r2 s) m)) m
+      Next (nextinstr (compare_long rs rs###r1 (eval_shift_op_long rs#r2 s))) m
   | Pcmn W r1 r2 s =>
-      Next (nextinstr (compare_int rs rs##r1 (Val.neg (eval_shift_op_int rs#r2 s)) m)) m
+      Next (nextinstr (compare_int rs rs##r1 (Val.neg (eval_shift_op_int rs#r2 s)))) m
   | Pcmn X r1 r2 s =>
-      Next (nextinstr (compare_long rs rs###r1 (Val.negl (eval_shift_op_long rs#r2 s)) m)) m
+      Next (nextinstr (compare_long rs rs###r1 (Val.negl (eval_shift_op_long rs#r2 s)))) m
   (** Integer arithmetic, extending register *)
   | Paddext rd r1 r2 x =>
       Next (nextinstr (rs#rd <- (Val.addl rs#r1 (eval_extend rs#r2 x)))) m
   | Psubext rd r1 r2 x =>
       Next (nextinstr (rs#rd <- (Val.subl rs#r1 (eval_extend rs#r2 x)))) m
   | Pcmpext r1 r2 x =>
-      Next (nextinstr (compare_long rs rs#r1 (eval_extend rs#r2 x) m)) m
+      Next (nextinstr (compare_long rs rs#r1 (eval_extend rs#r2 x))) m
   | Pcmnext r1 r2 x =>
-      Next (nextinstr (compare_long rs rs#r1 (Val.negl (eval_extend rs#r2 x)) m)) m
+      Next (nextinstr (compare_long rs rs#r1 (Val.negl (eval_extend rs#r2 x)))) m
   (** Logical, shifted register *)
   | Pand W rd r1 r2 s =>
       Next (nextinstr (rs#rd <- (Val.and rs##r1 (eval_shift_op_int rs#r2 s)))) m
@@ -892,9 +497,9 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Porn X rd r1 r2 s =>
       Next (nextinstr (rs#rd <- (Val.orl rs###r1 (Val.notl (eval_shift_op_long rs#r2 s))))) m
   | Ptst W r1 r2 s =>
-      Next (nextinstr (compare_int rs (Val.and rs##r1 (eval_shift_op_int rs#r2 s)) (Vint Int.zero) m)) m
+      Next (nextinstr (compare_int rs (Val.and rs##r1 (eval_shift_op_int rs#r2 s)) (Vint Int.zero))) m
   | Ptst X r1 r2 s =>
-      Next (nextinstr (compare_long rs (Val.andl rs###r1 (eval_shift_op_long rs#r2 s)) (Vlong Int64.zero) m)) m
+      Next (nextinstr (compare_long rs (Val.andl rs###r1 (eval_shift_op_long rs#r2 s)) (Vlong Int64.zero))) m
   (** Variable shifts *)
   | Pasrv W rd r1 r2 =>
       Next (nextinstr (rs#rd <- (Val.shr rs#r1 rs#r2))) m
@@ -1118,80 +723,9 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       Stuck
   end.
 
-(** Translation of the LTL/Linear/Mach view of machine registers
-  to the AArch64 view.  Note that no LTL register maps to [X16],
-  [X18], nor [X30].
-  [X18] is reserved as the platform register and never used by the
-  code generated by CompCert.
-  [X30] is used for the return address, and can also be used as temporary.
-  [X16] can be used as temporary. *)
-
-Definition preg_of (r: mreg) : preg :=
-  match r with
-  | R0 => X0   | R1 => X1   | R2 => X2   | R3 => X3
-  | R4 => X4   | R5 => X5   | R6 => X6   | R7 => X7
-  | R8 => X8   | R9 => X9   | R10 => X10 | R11 => X11
-  | R12 => X12 | R13 => X13 | R14 => X14 | R15 => X15
-  | R17 => X17 | R19 => X19
-  | R20 => X20 | R21 => X21 | R22 => X22 | R23 => X23
-  | R24 => X24 | R25 => X25 | R26 => X26 | R27 => X27
-  | R28 => X28 | R29 => X29
-  | F0 => D0   | F1 => D1   | F2 => D2   | F3 => D3
-  | F4 => D4   | F5 => D5   | F6 => D6   | F7 => D7
-  | F8 => D8   | F9 => D9   | F10 => D10 | F11 => D11
-  | F12 => D12 | F13 => D13 | F14 => D14 | F15 => D15
-  | F16 => D16 | F17 => D17 | F18 => D18 | F19 => D19
-  | F20 => D20 | F21 => D21 | F22 => D22 | F23 => D23
-  | F24 => D24 | F25 => D25 | F26 => D26 | F27 => D27
-  | F28 => D28 | F29 => D29 | F30 => D30 | F31 => D31
-  end.
-
-(** Undefine all registers except SP and callee-save registers *)
-
-Definition undef_caller_save_regs (rs: regset) : regset :=
-  fun r =>
-    if preg_eq r SP
-    || In_dec preg_eq r (List.map preg_of (List.filter is_callee_save all_mregs))
-    then rs r
-    else Vundef.
-
-(** Extract the values of the arguments of an external call.
-    We exploit the calling conventions from module [Conventions], except that
-    we use AArch64 registers instead of locations. *)
-
-Inductive extcall_arg (rs: regset) (m: mem): loc -> val -> Prop :=
-  | extcall_arg_reg: forall r,
-      extcall_arg rs m (R r) (rs (preg_of r))
-  | extcall_arg_stack: forall ofs ty bofs v,
-      bofs = Stacklayout.fe_ofs_arg + 4 * ofs ->
-      Mem.loadv (chunk_of_type ty) m
-                (Val.offset_ptr rs#SP (Ptrofs.repr bofs)) = Some v ->
-      extcall_arg rs m (Locations.S Outgoing ofs ty) v.
-
-Inductive extcall_arg_pair (rs: regset) (m: mem): rpair loc -> val -> Prop :=
-  | extcall_arg_one: forall l v,
-      extcall_arg rs m l v ->
-      extcall_arg_pair rs m (One l) v
-  | extcall_arg_twolong: forall hi lo vhi vlo,
-      extcall_arg rs m hi vhi ->
-      extcall_arg rs m lo vlo ->
-      extcall_arg_pair rs m (Twolong hi lo) (Val.longofwords vhi vlo).
-
-Definition extcall_arguments
-    (rs: regset) (m: mem) (sg: signature) (args: list val) : Prop :=
-  list_forall2 (extcall_arg_pair rs m) (loc_arguments sg) args.
-
-Definition loc_external_result (sg: signature) : rpair preg :=
-  map_rpair preg_of (loc_result sg).
-
-(** Execution of the instruction at [rs#PC]. *)
-
-Inductive state: Type :=
-  | State: regset -> mem -> state.
-
 Inductive step: state -> trace -> state -> Prop :=
   | exec_step_internal:
-      forall b ofs f i rs m rs' m',
+      forall b ofs (f:function) i rs m rs' m',
       rs PC = Vptr b ofs ->
       Genv.find_funct_ptr ge b = Some (Internal f) ->
       find_instr (Ptrofs.unsigned ofs) f.(fn_code) = Some i ->
diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v
index 71c0dba3..d52f3c24 100644
--- a/aarch64/Asmblock.v
+++ b/aarch64/Asmblock.v
@@ -475,11 +475,6 @@ Inductive instruction: Type :=
   | Pcfi_adjust (ofs: int)                                            (**r .cfi_adjust debug directive *)
   | Pcfi_rel_offset (ofs: int)                                        (**r .cfi_rel_offset debug directive *)
 .
-
-Definition code := list instruction.
-Record function : Type := mkfunction { fn_sig: signature; fn_code: code }.
-Definition fundef := AST.fundef function.
-Definition program := AST.program fundef unit.
 *)
 
 
@@ -541,6 +536,15 @@ Fixpoint set_res (res: builtin_res preg) (v: val) (rs: regset) : regset :=
   | BR_splitlong hi lo => set_res lo (Val.loword v) (set_res hi (Val.hiword v) rs)
   end.
 
+
+(** FIXME: not clear howto deal with these axioms in Asmblock.
+    The dependency over genv will get us in troubles...
+
+TODO: The solution is probably to put [symbol_low] and [symbol_high] [symbol_high_low]  with any dependency on "ge"
+as an hypothesis in RELSEM section.
+
+*)
+
 (** The two functions below axiomatize how the linker processes
   symbolic references [symbol + offset].  It computes the
   difference between the address and the PC, and splits it into:
diff --git a/aarch64/Asmblockgen.v b/aarch64/Asmblockgen.v
new file mode 100644
index 00000000..83f2b96b
--- /dev/null
+++ b/aarch64/Asmblockgen.v
@@ -0,0 +1,1197 @@
+(* *************************************************************)
+(*                                                             *)
+(*             The Compcert verified compiler                  *)
+(*                                                             *)
+(*           Sylvain Boulmé     Grenoble-INP, VERIMAG          *)
+(*           Justus Fasse       UGA, VERIMAG                   *)
+(*           Xavier Leroy       INRIA Paris-Rocquencourt       *)
+(*           David Monniaux     CNRS, VERIMAG                  *)
+(*           Cyril Six          Kalray                         *)
+(*                                                             *)
+(*  Copyright Kalray. Copyright VERIMAG. All rights reserved.  *)
+(*  This file is distributed under the terms of the INRIA      *)
+(*  Non-Commercial License Agreement.                          *)
+(*                                                             *)
+(* *************************************************************)
+
+(** * Translation from Machblock to AArch64 assembly block language (Asmblock) 
+    Inspired from the Mach->Asm pass of original Leroy's backend, but adapted to the block structure like the KVX backend. *)
+
+Require Import Recdef Coqlib Zwf Zbits.
+Require Import Errors AST Integers Floats Op.
+Require Import Locations Machblock Asmblock.
+
+(* STUB *)
+Definition transf_function (f: Machblock.function) : res Asmblock.function :=
+  Error (msg "Asmblockgen not yet implmented").
+
+Definition transf_fundef (f: Machblock.fundef) : res Asmblock.fundef :=
+  transf_partial_fundef transf_function f.
+
+Definition transf_program (p: Machblock.program) : res Asmblock.program :=
+  transform_partial_program transf_fundef p.
+
+(* ORIGINAL aarch64/Asmgen file that needs to be adapted
+
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*         Xavier Leroy, Collège de France and INRIA Paris             *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Translation from Mach to AArch64. *)
+
+Require Import Recdef Coqlib Zwf Zbits.
+Require Import Errors AST Integers Floats Op.
+Require Import Locations Mach Asm.
+
+Local Open Scope string_scope.
+Local Open Scope list_scope.
+Local Open Scope error_monad_scope.
+
+(** Alignment check for symbols *)
+
+Parameter symbol_is_aligned : ident -> Z -> bool.
+(** [symbol_is_aligned id sz] checks whether the symbol [id] is [sz] aligned *)
+
+(** Extracting integer or float registers. *)
+
+Definition ireg_of (r: mreg) : res ireg :=
+  match preg_of r with IR mr => OK mr | _ => Error(msg "Asmgen.ireg_of") end.
+
+Definition freg_of (r: mreg) : res freg :=
+  match preg_of r with FR mr => OK mr | _ => Error(msg "Asmgen.freg_of") end.
+
+(** Recognition of immediate arguments for logical integer operations.*)
+
+(** Valid immediate arguments are repetitions of a bit pattern [B]
+  of length [e] = 2, 4, 8, 16, 32 or 64.
+  The bit pattern [B] must be of the form [0*1*0*] or [1*0*1*]
+  but must not be all zeros or all ones. *)
+
+(** The following automaton recognizes [0*1*0*|1*0*1*].
+<<
+               0          1          0
+              / \        / \        / \
+              \ /        \ /        \ /
+        -0--> [B] --1--> [D] --0--> [F]
+       /
+     [A]
+       \
+        -1--> [C] --0--> [E] --1--> [G]
+              / \        / \        / \
+              \ /        \ /        \ /
+               1          0          1
+>>
+*)
+
+Module Automaton.
+
+Inductive state : Type := SA | SB | SC | SD | SE | SF | SG | Sbad.
+
+Definition start := SA.
+
+Definition next (s: state) (b: bool) :=
+  match s, b with
+    | SA,false => SB      | SA,true => SC
+    | SB,false => SB      | SB,true => SD
+    | SC,false => SE      | SC,true => SC
+    | SD,false => SF      | SD,true => SD
+    | SE,false => SE      | SE,true => SG
+    | SF,false => SF      | SF,true => Sbad
+    | SG,false => Sbad    | SG,true => SG
+    | Sbad,_ => Sbad
+  end.
+
+Definition accepting (s: state) :=
+  match s with
+  | SA | SB | SC | SD | SE | SF | SG => true
+  | Sbad => false
+  end.
+
+Fixpoint run (len: nat) (s: state) (x: Z) : bool :=
+  match len with
+  | Datatypes.O => accepting s
+  | Datatypes.S len => run len (next s (Z.odd x)) (Z.div2 x)
+  end.
+
+End Automaton.
+
+(** The following function determines the candidate length [e],
+    ensuring that [x] is a repetition [BB...B] 
+    of a bit pattern [B] of length [e]. *)
+
+Definition logical_imm_length (x: Z) (sixtyfour: bool) : nat :=
+  (** [test n] checks that the low [2n] bits of [x] are of the
+      form [BB], that is, two occurrences of the same [n] bits *)
+  let test (n: Z) : bool :=
+    Z.eqb (Zzero_ext n x) (Zzero_ext n (Z.shiftr x n)) in
+  (** If [test n] fails, we know that the candidate length [e] is
+      at least [2n].  Hence we test with decreasing values of [n]:
+      32, 16, 8, 4, 2. *)
+  if sixtyfour && negb (test 32) then 64%nat
+  else if negb (test 16) then 32%nat
+  else if negb (test 8) then 16%nat
+  else if negb (test 4) then 8%nat
+  else if negb (test 2) then 4%nat
+  else 2%nat.
+
+(** A valid logical immediate is 
+- neither [0] nor [-1];
+- composed of a repetition [BBBBB] of a bit-pattern [B] of length [e]
+- the low [e] bits of the number, that is, [B], match [0*1*0*] or [1*0*1*].
+*)
+
+Definition is_logical_imm32 (x: int) : bool :=
+  negb (Int.eq x Int.zero) && negb (Int.eq x Int.mone) &&
+  Automaton.run (logical_imm_length (Int.unsigned x) false)
+                Automaton.start (Int.unsigned x).
+
+Definition is_logical_imm64 (x: int64) : bool :=
+  negb (Int64.eq x Int64.zero) && negb (Int64.eq x Int64.mone) &&
+  Automaton.run (logical_imm_length (Int64.unsigned x) true)
+                Automaton.start (Int64.unsigned x).
+
+(** Arithmetic immediates are 12-bit unsigned numbers, possibly shifted left 12 bits *)
+
+Definition is_arith_imm32 (x: int) : bool :=
+  Int.eq x (Int.zero_ext 12 x)
+  || Int.eq x (Int.shl (Int.zero_ext 12 (Int.shru x (Int.repr 12))) (Int.repr 12)).
+
+Definition is_arith_imm64 (x: int64) : bool :=
+  Int64.eq x (Int64.zero_ext 12 x)
+  || Int64.eq x (Int64.shl (Int64.zero_ext 12 (Int64.shru x (Int64.repr 12))) (Int64.repr 12)).
+
+(** Decompose integer literals into 16-bit fragments *)
+
+Fixpoint decompose_int (N: nat) (n p: Z) {struct N} : list (Z * Z) :=
+  match N with
+  | Datatypes.O => nil
+  | Datatypes.S N =>
+    let frag := Zzero_ext 16 (Z.shiftr n p) in
+    if Z.eqb frag 0 then
+      decompose_int N n (p + 16)
+    else
+      (frag, p) :: decompose_int N (Z.ldiff n (Z.shiftl 65535 p)) (p + 16)
+  end.
+
+Definition negate_decomposition (l: list (Z * Z)) :=
+  List.map (fun np => (Z.lxor (fst np) 65535, snd np)) l.
+
+Definition loadimm_k (sz: isize) (rd: ireg) (l: list (Z * Z)) (k: code) : code :=
+  List.fold_right (fun np k => Pmovk sz rd (fst np) (snd np) :: k) k l.
+
+Definition loadimm_z (sz: isize) (rd: ireg) (l: list (Z * Z)) (k: code) : code :=
+  match l with
+  | nil => Pmovz sz rd 0 0 :: k
+  | (n1, p1) :: l => Pmovz sz rd n1 p1 :: loadimm_k sz rd l k
+  end.
+
+Definition loadimm_n (sz: isize) (rd: ireg) (l: list (Z * Z)) (k: code) : code :=
+  match l with
+  | nil => Pmovn sz rd 0 0 :: k
+  | (n1, p1) :: l => Pmovn sz rd n1 p1 :: loadimm_k sz rd (negate_decomposition l) k
+  end.
+
+Definition loadimm (sz: isize) (rd: ireg) (n: Z) (k: code) : code :=
+  let N := match sz with W => 2%nat | X => 4%nat end in
+  let dz := decompose_int N n 0 in
+  let dn := decompose_int N (Z.lnot n) 0 in
+  if Nat.leb (List.length dz) (List.length dn)
+  then loadimm_z sz rd dz k
+  else loadimm_n sz rd dn k.
+
+Definition loadimm32 (rd: ireg) (n: int) (k: code) : code :=
+  if is_logical_imm32 n
+  then Porrimm W rd XZR (Int.unsigned n) :: k
+  else loadimm W rd (Int.unsigned n) k.
+
+Definition loadimm64 (rd: ireg) (n: int64) (k: code) : code :=
+  if is_logical_imm64 n
+  then Porrimm X rd XZR (Int64.unsigned n) :: k
+  else loadimm X rd (Int64.unsigned n) k.
+
+(** Add immediate *)
+
+Definition addimm_aux (insn: iregsp -> iregsp -> Z -> instruction)
+                        (rd r1: iregsp) (n: Z) (k: code) :=
+  let nlo := Zzero_ext 12 n in
+  let nhi := n - nlo in
+  if Z.eqb nhi 0 then
+    insn rd r1 nlo :: k
+  else if Z.eqb nlo 0 then
+    insn rd r1 nhi :: k
+  else
+    insn rd r1 nhi :: insn rd rd nlo :: k.
+
+Definition addimm32 (rd r1: ireg) (n: int) (k: code) : code :=
+  let m := Int.neg n in
+  if Int.eq n (Int.zero_ext 24 n) then
+    addimm_aux (Paddimm W) rd r1 (Int.unsigned n) k
+  else if Int.eq m (Int.zero_ext 24 m) then
+    addimm_aux (Psubimm W) rd r1 (Int.unsigned m) k
+  else if Int.lt n Int.zero then
+    loadimm32 X16 m (Psub W rd r1 X16 SOnone :: k)
+  else
+    loadimm32 X16 n (Padd W rd r1 X16 SOnone :: k).
+
+Definition addimm64 (rd r1: iregsp) (n: int64) (k: code) : code :=
+  let m := Int64.neg n in
+  if Int64.eq n (Int64.zero_ext 24 n) then
+    addimm_aux (Paddimm X) rd r1 (Int64.unsigned n) k
+  else if Int64.eq m (Int64.zero_ext 24 m) then
+    addimm_aux (Psubimm X) rd r1 (Int64.unsigned m) k
+  else if Int64.lt n Int64.zero then
+    loadimm64 X16 m (Psubext rd r1 X16 (EOuxtx Int.zero) :: k)
+  else
+    loadimm64 X16 n (Paddext rd r1 X16 (EOuxtx Int.zero) :: k).
+
+(** Logical immediate *)
+
+Definition logicalimm32
+              (insn1: ireg -> ireg0 -> Z -> instruction)
+              (insn2: ireg -> ireg0 -> ireg -> shift_op -> instruction)
+              (rd r1: ireg) (n: int) (k: code) : code :=
+  if is_logical_imm32 n
+  then insn1 rd r1 (Int.unsigned n) :: k
+  else loadimm32 X16 n (insn2 rd r1 X16 SOnone :: k).
+
+Definition logicalimm64
+              (insn1: ireg -> ireg0 -> Z -> instruction)
+              (insn2: ireg -> ireg0 -> ireg -> shift_op -> instruction)
+              (rd r1: ireg) (n: int64) (k: code) : code :=
+  if is_logical_imm64 n
+  then insn1 rd r1 (Int64.unsigned n) :: k
+  else loadimm64 X16 n (insn2 rd r1 X16 SOnone :: k).
+
+(** Sign- or zero-extended arithmetic *)
+
+Definition transl_extension (ex: extension) (a: int) : extend_op :=
+  match ex with Xsgn32 => EOsxtw a | Xuns32 => EOuxtw a end.
+
+Definition move_extended_base
+              (rd: ireg) (r1: ireg) (ex: extension) (k: code) : code :=
+  match ex with
+  | Xsgn32 => Pcvtsw2x rd r1 :: k
+  | Xuns32 => Pcvtuw2x rd r1 :: k
+  end.
+
+Definition move_extended
+              (rd: ireg) (r1: ireg) (ex: extension) (a: int) (k: code) : code :=
+  if Int.eq a Int.zero then
+    move_extended_base rd r1 ex k
+  else
+    move_extended_base rd r1 ex (Padd X rd XZR rd (SOlsl a) :: k).
+
+Definition arith_extended 
+              (insnX: iregsp -> iregsp -> ireg -> extend_op -> instruction)
+              (insnS: ireg -> ireg0 -> ireg -> shift_op -> instruction)
+              (rd r1 r2: ireg) (ex: extension) (a: int) (k: code) : code :=
+  if Int.ltu a (Int.repr 5) then
+    insnX rd r1 r2 (transl_extension ex a) :: k
+  else
+    move_extended_base X16 r2 ex (insnS rd r1 X16 (SOlsl a) :: k).
+
+(** Extended right shift *)
+
+Definition shrx32 (rd r1: ireg) (n: int) (k: code) : code :=
+  if Int.eq n Int.zero then
+    Pmov rd r1 :: k
+  else if Int.eq n Int.one then
+         Padd W X16 r1 r1 (SOlsr (Int.repr 31)) ::
+         Porr W rd XZR X16 (SOasr n) :: k
+       else
+         Porr W X16 XZR r1 (SOasr (Int.repr 31)) ::
+         Padd W X16 r1 X16 (SOlsr (Int.sub Int.iwordsize n)) ::
+         Porr W rd XZR X16 (SOasr n) :: k.
+
+Definition shrx64 (rd r1: ireg) (n: int) (k: code) : code :=
+  if Int.eq n Int.zero then
+    Pmov rd r1 :: k
+  else if Int.eq n Int.one then
+         Padd X X16 r1 r1 (SOlsr (Int.repr 63)) ::
+         Porr X rd XZR X16 (SOasr n) :: k
+       else
+         Porr X X16 XZR r1 (SOasr (Int.repr 63)) ::
+         Padd X X16 r1 X16 (SOlsr (Int.sub Int64.iwordsize' n)) ::
+         Porr X rd XZR X16 (SOasr n) :: k.
+
+(** Load the address [id + ofs] in [rd] *)
+
+Definition loadsymbol (rd: ireg) (id: ident) (ofs: ptrofs) (k: code) : code :=
+  if Archi.pic_code tt then
+    if Ptrofs.eq ofs Ptrofs.zero then
+      Ploadsymbol rd id :: k
+    else
+      Ploadsymbol rd id :: addimm64 rd rd (Ptrofs.to_int64 ofs) k
+  else
+    Padrp rd id ofs :: Paddadr rd rd id ofs :: k.
+
+(** Translate a shifted operand *)
+
+Definition transl_shift (s: Op.shift) (a: int): Asm.shift_op :=
+  match s with
+  | Slsl => SOlsl a
+  | Slsr => SOlsr a
+  | Sasr => SOasr a
+  | Sror => SOror a
+  end.
+
+(** Translation of a condition.  Prepends to [k] the instructions
+  that evaluate the condition and leave its boolean result in one of
+  the bits of the condition register.  The bit in question is
+  determined by the [crbit_for_cond] function. *)
+
+Definition transl_cond
+              (cond: condition) (args: list mreg) (k: code) :=
+  match cond, args with
+  | (Ccomp c | Ccompu c), a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Pcmp W r1 r2 SOnone :: k)
+  | (Ccompshift c s a | Ccompushift c s a), a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Pcmp W r1 r2 (transl_shift s a) :: k)
+  | (Ccompimm c n | Ccompuimm c n), a1 :: nil =>
+      do r1 <- ireg_of a1;
+      OK (if is_arith_imm32 n then
+            Pcmpimm W r1 (Int.unsigned n) :: k
+          else if is_arith_imm32 (Int.neg n) then
+            Pcmnimm W r1 (Int.unsigned (Int.neg n)) :: k
+          else
+            loadimm32 X16 n (Pcmp W r1 X16 SOnone :: k))
+  | (Cmaskzero n | Cmasknotzero n), a1 :: nil =>
+      do r1 <- ireg_of a1;
+      OK (if is_logical_imm32 n then
+            Ptstimm W r1 (Int.unsigned n) :: k
+          else
+            loadimm32 X16 n (Ptst W r1 X16 SOnone :: k))
+  | (Ccompl c | Ccomplu c), a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Pcmp X r1 r2 SOnone :: k)
+  | (Ccomplshift c s a | Ccomplushift c s a), a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Pcmp X r1 r2 (transl_shift s a) :: k)
+  | (Ccomplimm c n | Ccompluimm c n), a1 :: nil =>
+      do r1 <- ireg_of a1;
+      OK (if is_arith_imm64 n then
+            Pcmpimm X r1 (Int64.unsigned n) :: k
+          else if is_arith_imm64 (Int64.neg n) then
+            Pcmnimm X r1 (Int64.unsigned (Int64.neg n)) :: k
+          else
+            loadimm64 X16 n (Pcmp X r1 X16 SOnone :: k))
+  | (Cmasklzero n | Cmasklnotzero n), a1 :: nil =>
+      do r1 <- ireg_of a1;
+      OK (if is_logical_imm64 n then
+            Ptstimm X r1 (Int64.unsigned n) :: k
+          else
+            loadimm64 X16 n (Ptst X r1 X16 SOnone :: k))
+  | Ccompf cmp, a1 :: a2 :: nil =>
+      do r1 <- freg_of a1; do r2 <- freg_of a2;
+      OK (Pfcmp D r1 r2 :: k)
+  | Cnotcompf cmp, a1 :: a2 :: nil =>
+      do r1 <- freg_of a1; do r2 <- freg_of a2;
+      OK (Pfcmp D r1 r2 :: k)
+  | Ccompfzero cmp, a1 :: nil =>
+      do r1 <- freg_of a1;
+      OK (Pfcmp0 D r1 :: k)
+  | Cnotcompfzero cmp, a1 :: nil =>
+      do r1 <- freg_of a1;
+      OK (Pfcmp0 D r1 :: k)
+  | Ccompfs cmp, a1 :: a2 :: nil =>
+      do r1 <- freg_of a1; do r2 <- freg_of a2;
+      OK (Pfcmp S r1 r2 :: k)
+  | Cnotcompfs cmp, a1 :: a2 :: nil =>
+      do r1 <- freg_of a1; do r2 <- freg_of a2;
+      OK (Pfcmp S r1 r2 :: k)
+  | Ccompfszero cmp, a1 :: nil =>
+      do r1 <- freg_of a1;
+      OK (Pfcmp0 S r1 :: k)
+  | Cnotcompfszero cmp, a1 :: nil =>
+      do r1 <- freg_of a1;
+      OK (Pfcmp0 S r1 :: k)
+  | _, _ =>
+      Error(msg "Asmgen.transl_cond")
+  end.
+
+Definition cond_for_signed_cmp (cmp: comparison) :=
+  match cmp with
+  | Ceq => TCeq
+  | Cne => TCne
+  | Clt => TClt
+  | Cle => TCle
+  | Cgt => TCgt
+  | Cge => TCge
+  end.
+
+Definition cond_for_unsigned_cmp (cmp: comparison) :=
+  match cmp with
+  | Ceq => TCeq
+  | Cne => TCne
+  | Clt => TClo
+  | Cle => TCls
+  | Cgt => TChi
+  | Cge => TChs
+  end.
+
+Definition cond_for_float_cmp (cmp: comparison) :=
+  match cmp with
+  | Ceq => TCeq
+  | Cne => TCne
+  | Clt => TCmi
+  | Cle => TCls
+  | Cgt => TCgt
+  | Cge => TCge
+  end.
+
+Definition cond_for_float_not_cmp (cmp: comparison) :=
+  match cmp with
+  | Ceq => TCne
+  | Cne => TCeq
+  | Clt => TCpl
+  | Cle => TChi
+  | Cgt => TCle
+  | Cge => TClt
+  end.
+
+Definition cond_for_cond (cond: condition) :=
+  match cond with
+  | Ccomp cmp => cond_for_signed_cmp cmp
+  | Ccompu cmp => cond_for_unsigned_cmp cmp
+  | Ccompshift cmp s a => cond_for_signed_cmp cmp
+  | Ccompushift cmp s a => cond_for_unsigned_cmp cmp
+  | Ccompimm cmp n => cond_for_signed_cmp cmp
+  | Ccompuimm cmp n => cond_for_unsigned_cmp cmp
+  | Cmaskzero n => TCeq
+  | Cmasknotzero n => TCne
+  | Ccompl cmp => cond_for_signed_cmp cmp
+  | Ccomplu cmp => cond_for_unsigned_cmp cmp
+  | Ccomplshift cmp s a => cond_for_signed_cmp cmp
+  | Ccomplushift cmp s a => cond_for_unsigned_cmp cmp
+  | Ccomplimm cmp n => cond_for_signed_cmp cmp
+  | Ccompluimm cmp n => cond_for_unsigned_cmp cmp
+  | Cmasklzero n => TCeq
+  | Cmasklnotzero n => TCne
+  | Ccompf cmp => cond_for_float_cmp cmp
+  | Cnotcompf cmp => cond_for_float_not_cmp cmp
+  | Ccompfzero cmp => cond_for_float_cmp cmp
+  | Cnotcompfzero cmp => cond_for_float_not_cmp cmp
+  | Ccompfs cmp => cond_for_float_cmp cmp
+  | Cnotcompfs cmp => cond_for_float_not_cmp cmp
+  | Ccompfszero cmp => cond_for_float_cmp cmp
+  | Cnotcompfszero cmp => cond_for_float_not_cmp cmp
+  end.
+
+(** Translation of a conditional branch.  Prepends to [k] the instructions
+  that evaluate the condition and ranch to [lbl] if it holds.
+  We recognize some conditional branches that can be implemented
+  without setting then testing condition flags.  *)
+
+Definition transl_cond_branch_default
+              (c: condition) (args: list mreg) (lbl: label) (k: code) :=
+  transl_cond c args (Pbc (cond_for_cond c) lbl :: k).
+ 
+Definition transl_cond_branch
+              (c: condition) (args: list mreg) (lbl: label) (k: code) :=
+  match args, c with
+  | a1 :: nil, (Ccompimm Cne n | Ccompuimm Cne n) =>
+      if Int.eq n Int.zero
+      then (do r1 <- ireg_of a1; OK (Pcbnz W r1 lbl :: k))
+      else transl_cond_branch_default c args lbl k
+  | a1 :: nil, (Ccompimm Ceq n | Ccompuimm Ceq n) =>
+      if Int.eq n Int.zero
+      then (do r1 <- ireg_of a1; OK (Pcbz W r1 lbl :: k))
+      else transl_cond_branch_default c args lbl k
+  | a1 :: nil, (Ccomplimm Cne n | Ccompluimm Cne n) =>
+      if Int64.eq n Int64.zero
+      then (do r1 <- ireg_of a1; OK (Pcbnz X r1 lbl :: k))
+      else transl_cond_branch_default c args lbl k
+  | a1 :: nil, (Ccomplimm Ceq n | Ccompluimm Ceq n) =>
+      if Int64.eq n Int64.zero
+      then (do r1 <- ireg_of a1; OK (Pcbz X r1 lbl :: k))
+      else transl_cond_branch_default c args lbl k
+  | a1 :: nil, Cmaskzero n =>
+      match Int.is_power2 n with
+      | Some bit => do r1 <- ireg_of a1; OK (Ptbz W r1 bit lbl :: k)
+      | None => transl_cond_branch_default c args lbl k
+      end
+  | a1 :: nil, Cmasknotzero n =>
+      match Int.is_power2 n with
+      | Some bit => do r1 <- ireg_of a1; OK (Ptbnz W r1 bit lbl :: k)
+      | None => transl_cond_branch_default c args lbl k
+      end
+  | a1 :: nil, Cmasklzero n =>
+      match Int64.is_power2' n with
+      | Some bit => do r1 <- ireg_of a1; OK (Ptbz X r1 bit lbl :: k)
+      | None => transl_cond_branch_default c args lbl k
+      end
+  | a1 :: nil, Cmasklnotzero n =>
+      match Int64.is_power2' n with
+      | Some bit => do r1 <- ireg_of a1; OK (Ptbnz X r1 bit lbl :: k)
+      | None => transl_cond_branch_default c args lbl k
+      end
+  | _, _ =>
+      transl_cond_branch_default c args lbl k
+  end.
+  
+(** Translation of the arithmetic operation [res <- op(args)].
+    The corresponding instructions are prepended to [k]. *)
+
+Definition transl_op
+              (op: operation) (args: list mreg) (res: mreg) (k: code) :=
+  match op, args with
+  | Omove, a1 :: nil =>
+      match preg_of res, preg_of a1 with
+      | IR r, IR a => OK (Pmov r a :: k)
+      | FR r, FR a => OK (Pfmov r a :: k)
+      |  _  ,  _   => Error(msg "Asmgen.Omove")
+      end
+  | Ointconst n, nil =>
+      do rd <- ireg_of res;
+      OK (loadimm32 rd n k)
+  | Olongconst n, nil =>
+      do rd <- ireg_of res;
+      OK (loadimm64 rd n k)
+  | Ofloatconst f, nil =>
+      do rd <- freg_of res;
+      OK (if Float.eq_dec f Float.zero
+          then Pfmovi D rd XZR :: k
+          else Pfmovimmd rd f :: k)
+  | Osingleconst f, nil =>
+      do rd <- freg_of res;
+      OK (if Float32.eq_dec f Float32.zero
+          then Pfmovi S rd XZR :: k
+          else Pfmovimms rd f :: k)
+  | Oaddrsymbol id ofs, nil =>
+      do rd <- ireg_of res;
+      OK (loadsymbol rd id ofs k)
+  | Oaddrstack ofs, nil =>
+      do rd <- ireg_of res;
+      OK (addimm64 rd XSP (Ptrofs.to_int64 ofs) k)
+(** 32-bit integer arithmetic *)
+  | Oshift s a, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (Porr W rd XZR r1 (transl_shift s a) :: k)
+  | Oadd, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Padd W rd r1 r2 SOnone :: k)
+  | Oaddshift s a, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Padd W rd r1 r2 (transl_shift s a) :: k)
+  | Oaddimm n, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (addimm32 rd r1 n k)
+  | Oneg, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (Psub W rd XZR r1 SOnone :: k)
+  | Onegshift s a, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (Psub W rd XZR r1 (transl_shift s a) :: k)
+  | Osub, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Psub W rd r1 r2 SOnone :: k)
+  | Osubshift s a, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Psub W rd r1 r2 (transl_shift s a) :: k)
+  | Omul, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Pmadd W rd r1 r2 XZR :: k)
+  | Omuladd, a1 :: a2 :: a3 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r3 <- ireg_of a3;
+      OK (Pmadd W rd r2 r3 r1 :: k)
+  | Omulsub, a1 :: a2 :: a3 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r3 <- ireg_of a3;
+      OK (Pmsub W rd r2 r3 r1 :: k)
+  | Odiv, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Psdiv W rd r1 r2 :: k)
+  | Odivu, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Pudiv W rd r1 r2 :: k)
+  | Oand, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Pand W rd r1 r2 SOnone :: k)
+  | Oandshift s a, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Pand W rd r1 r2 (transl_shift s a) :: k)
+  | Oandimm n, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (logicalimm32 (Pandimm W) (Pand W) rd r1 n k)      
+  | Oor, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Porr W rd r1 r2 SOnone :: k)
+  | Oorshift s a, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Porr W rd r1 r2 (transl_shift s a) :: k)
+  | Oorimm n, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (logicalimm32 (Porrimm W) (Porr W) rd r1 n k)      
+  | Oxor, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Peor W rd r1 r2 SOnone :: k)
+  | Oxorshift s a, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Peor W rd r1 r2 (transl_shift s a) :: k)
+  | Oxorimm n, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (logicalimm32 (Peorimm W) (Peor W) rd r1 n k)      
+  | Onot, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (Porn W rd XZR r1 SOnone :: k)
+  | Onotshift s a, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (Porn W rd XZR r1 (transl_shift s a) :: k)
+  | Obic, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Pbic W rd r1 r2 SOnone :: k)
+  | Obicshift s a, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Pbic W rd r1 r2 (transl_shift s a) :: k)
+  | Oorn, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Porn W rd r1 r2 SOnone :: k)
+  | Oornshift s a, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Porn W rd r1 r2 (transl_shift s a) :: k)
+  | Oeqv, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Peon W rd r1 r2 SOnone :: k)
+  | Oeqvshift s a, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Peon W rd r1 r2 (transl_shift s a) :: k)
+  | Oshl, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Plslv W rd r1 r2 :: k)
+  | Oshr, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Pasrv W rd r1 r2 :: k)
+  | Oshru, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Plsrv W rd r1 r2 :: k)
+  | Oshrximm n, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (shrx32 rd r1 n k)
+  | Ozext s, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (Pubfiz W rd r1 Int.zero s :: k)
+  | Osext s, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (Psbfiz W rd r1 Int.zero s :: k)
+  | Oshlzext s a, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (Pubfiz W rd r1 a (Z.min s (Int.zwordsize - Int.unsigned a)) :: k)
+  | Oshlsext s a, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (Psbfiz W rd r1 a (Z.min s (Int.zwordsize - Int.unsigned a)) :: k)
+  | Ozextshr a s, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (Pubfx W rd r1 a (Z.min s (Int.zwordsize - Int.unsigned a)) :: k)
+  | Osextshr a s, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (Psbfx W rd r1 a (Z.min s (Int.zwordsize - Int.unsigned a)) :: k)
+(** 64-bit integer arithmetic *)
+  | Oshiftl s a, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (Porr X rd XZR r1 (transl_shift s a) :: k)
+  | Oextend x a, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (move_extended rd r1 x a k)
+  (* [Omakelong] and [Ohighlong] should not occur *)
+  | Olowlong, a1 :: nil => 
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      assertion (ireg_eq rd r1);
+      OK (Pcvtx2w rd :: k)
+  | Oaddl, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Padd X rd r1 r2 SOnone :: k)
+  | Oaddlshift s a, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Padd X rd r1 r2 (transl_shift s a) :: k)
+  | Oaddlext x a, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (arith_extended Paddext (Padd X) rd r1 r2 x a k)
+  | Oaddlimm n, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (addimm64 rd r1 n k)
+  | Onegl, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (Psub X rd XZR r1 SOnone :: k)
+  | Oneglshift s a, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (Psub X rd XZR r1 (transl_shift s a) :: k)
+  | Osubl, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Psub X rd r1 r2 SOnone :: k)
+  | Osublshift s a, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Psub X rd r1 r2 (transl_shift s a) :: k)
+  | Osublext x a, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (arith_extended Psubext (Psub X) rd r1 r2 x a k)
+  | Omull, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Pmadd X rd r1 r2 XZR :: k)
+  | Omulladd, a1 :: a2 :: a3 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r3 <- ireg_of a3;
+      OK (Pmadd X rd r2 r3 r1 :: k)
+  | Omullsub, a1 :: a2 :: a3 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r3 <- ireg_of a3;
+      OK (Pmsub X rd r2 r3 r1 :: k)
+  | Omullhs, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Psmulh rd r1 r2 :: k)
+  | Omullhu, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Pumulh rd r1 r2 :: k)
+  | Odivl, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Psdiv X rd r1 r2 :: k)
+  | Odivlu, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Pudiv X rd r1 r2 :: k)
+  | Oandl, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Pand X rd r1 r2 SOnone :: k)
+  | Oandlshift s a, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Pand X rd r1 r2 (transl_shift s a) :: k)
+  | Oandlimm n, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (logicalimm64 (Pandimm X) (Pand X) rd r1 n k)      
+  | Oorl, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Porr X rd r1 r2 SOnone :: k)
+  | Oorlshift s a, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Porr X rd r1 r2 (transl_shift s a) :: k)
+  | Oorlimm n, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (logicalimm64 (Porrimm X) (Porr X) rd r1 n k)      
+  | Oxorl, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Peor X rd r1 r2 SOnone :: k)
+  | Oxorlshift s a, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Peor X rd r1 r2 (transl_shift s a) :: k)
+  | Oxorlimm n, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (logicalimm64 (Peorimm X) (Peor X) rd r1 n k)      
+  | Onotl, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (Porn X rd XZR r1 SOnone :: k)
+  | Onotlshift s a, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (Porn X rd XZR r1 (transl_shift s a) :: k)
+  | Obicl, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Pbic X rd r1 r2 SOnone :: k)
+  | Obiclshift s a, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Pbic X rd r1 r2 (transl_shift s a) :: k)
+  | Oornl, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Porn X rd r1 r2 SOnone :: k)
+  | Oornlshift s a, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Porn X rd r1 r2 (transl_shift s a) :: k)
+  | Oeqvl, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Peon X rd r1 r2 SOnone :: k)
+  | Oeqvlshift s a, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Peon X rd r1 r2 (transl_shift s a) :: k)
+  | Oshll, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Plslv X rd r1 r2 :: k)
+  | Oshrl, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Pasrv X rd r1 r2 :: k)
+  | Oshrlu, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Plsrv X rd r1 r2 :: k)
+  | Oshrlximm n, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (shrx64 rd r1 n k)
+  | Ozextl s, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (Pubfiz X rd r1 Int.zero s :: k)
+  | Osextl s, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (Psbfiz X rd r1 Int.zero s :: k)
+  | Oshllzext s a, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (Pubfiz X rd r1 a (Z.min s (Int64.zwordsize - Int.unsigned a)) :: k)
+  | Oshllsext s a, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (Psbfiz X rd r1 a (Z.min s (Int64.zwordsize - Int.unsigned a)) :: k)
+  | Ozextshrl a s, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (Pubfx X rd r1 a (Z.min s (Int64.zwordsize - Int.unsigned a)) :: k)
+  | Osextshrl a s, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (Psbfx X rd r1 a (Z.min s (Int64.zwordsize - Int.unsigned a)) :: k)
+(** 64-bit floating-point arithmetic *)
+  | Onegf, a1 :: nil =>
+      do rd <- freg_of res; do rs <- freg_of a1;
+      OK (Pfneg D rd rs :: k)
+  | Oabsf, a1 :: nil =>
+      do rd <- freg_of res; do rs <- freg_of a1;
+      OK (Pfabs D rd rs :: k)
+  | Oaddf, a1 :: a2 :: nil =>
+      do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
+      OK (Pfadd D rd rs1 rs2 :: k)
+  | Osubf, a1 :: a2 :: nil =>
+      do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
+      OK (Pfsub D rd rs1 rs2 :: k)
+  | Omulf, a1 :: a2 :: nil =>
+      do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
+      OK (Pfmul D rd rs1 rs2 :: k)
+  | Odivf, a1 :: a2 :: nil =>
+      do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
+      OK (Pfdiv D rd rs1 rs2 :: k)
+(** 32-bit floating-point arithmetic *)
+  | Onegfs, a1 :: nil =>
+      do rd <- freg_of res; do rs <- freg_of a1;
+      OK (Pfneg S rd rs :: k)
+  | Oabsfs, a1 :: nil =>
+      do rd <- freg_of res; do rs <- freg_of a1;
+      OK (Pfabs S rd rs :: k)
+  | Oaddfs, a1 :: a2 :: nil =>
+      do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
+      OK (Pfadd S rd rs1 rs2 :: k)
+  | Osubfs, a1 :: a2 :: nil =>
+      do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
+      OK (Pfsub S rd rs1 rs2 :: k)
+  | Omulfs, a1 :: a2 :: nil =>
+      do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
+      OK (Pfmul S rd rs1 rs2 :: k)
+  | Odivfs, a1 :: a2 :: nil =>
+      do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
+      OK (Pfdiv S rd rs1 rs2 :: k)
+  | Osingleoffloat, a1 :: nil =>
+      do rd <- freg_of res; do rs <- freg_of a1;
+      OK (Pfcvtsd rd rs :: k)
+  | Ofloatofsingle, a1 :: nil =>
+      do rd <- freg_of res; do rs <- freg_of a1;
+      OK (Pfcvtds rd rs :: k)
+(** Conversions between int and float *)
+  | Ointoffloat, a1 :: nil =>
+      do rd <- ireg_of res; do rs <- freg_of a1;
+      OK (Pfcvtzs W D rd rs :: k)
+  | Ointuoffloat, a1 :: nil =>
+      do rd <- ireg_of res; do rs <- freg_of a1;
+      OK (Pfcvtzu W D rd rs :: k)
+  | Ofloatofint, a1 :: nil =>
+      do rd <- freg_of res; do rs <- ireg_of a1;
+      OK (Pscvtf D W rd rs :: k)
+  | Ofloatofintu, a1 :: nil =>
+      do rd <- freg_of res; do rs <- ireg_of a1;
+      OK (Pucvtf D W rd rs :: k)
+  | Ointofsingle, a1 :: nil =>
+      do rd <- ireg_of res; do rs <- freg_of a1;
+      OK (Pfcvtzs W S rd rs :: k)
+  | Ointuofsingle, a1 :: nil =>
+      do rd <- ireg_of res; do rs <- freg_of a1;
+      OK (Pfcvtzu W S rd rs :: k)
+  | Osingleofint, a1 :: nil =>
+      do rd <- freg_of res; do rs <- ireg_of a1;
+      OK (Pscvtf S W rd rs :: k)
+  | Osingleofintu, a1 :: nil =>
+      do rd <- freg_of res; do rs <- ireg_of a1;
+      OK (Pucvtf S W rd rs :: k)
+  | Olongoffloat, a1 :: nil =>
+      do rd <- ireg_of res; do rs <- freg_of a1;
+      OK (Pfcvtzs X D rd rs :: k)
+  | Olonguoffloat, a1 :: nil =>
+      do rd <- ireg_of res; do rs <- freg_of a1;
+      OK (Pfcvtzu X D rd rs :: k)
+  | Ofloatoflong, a1 :: nil =>
+      do rd <- freg_of res; do rs <- ireg_of a1;
+      OK (Pscvtf D X rd rs :: k)
+  | Ofloatoflongu, a1 :: nil =>
+      do rd <- freg_of res; do rs <- ireg_of a1;
+      OK (Pucvtf D X rd rs :: k)
+  | Olongofsingle, a1 :: nil =>
+      do rd <- ireg_of res; do rs <- freg_of a1;
+      OK (Pfcvtzs X S rd rs :: k)
+  | Olonguofsingle, a1 :: nil =>
+      do rd <- ireg_of res; do rs <- freg_of a1;
+      OK (Pfcvtzu X S rd rs :: k)
+  | Osingleoflong, a1 :: nil =>
+      do rd <- freg_of res; do rs <- ireg_of a1;
+      OK (Pscvtf S X rd rs :: k)
+  | Osingleoflongu, a1 :: nil =>
+      do rd <- freg_of res; do rs <- ireg_of a1;
+      OK (Pucvtf S X rd rs :: k)
+(** Boolean tests *)
+  | Ocmp c, _ =>
+      do rd <- ireg_of res;
+      transl_cond c args (Pcset rd (cond_for_cond c) :: k)
+(** Conditional move *)
+  | Osel cmp ty, a1 :: a2 :: args =>
+      match preg_of res with
+      | IR r => 
+          do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+          transl_cond cmp args (Pcsel r r1 r2 (cond_for_cond cmp) :: k)
+      | FR r =>
+          do r1 <- freg_of a1; do r2 <- freg_of a2;
+          transl_cond cmp args (Pfsel r r1 r2 (cond_for_cond cmp) :: k)
+      | _ =>
+          Error(msg "Asmgen.Osel")
+      end
+  | _, _ =>
+      Error(msg "Asmgen.transl_op")
+  end.
+
+(** Translation of addressing modes *)
+
+Definition offset_representable (sz: Z) (ofs: int64) : bool :=
+  let isz := Int64.repr sz in
+  (** either unscaled 9-bit signed *)
+  Int64.eq ofs (Int64.sign_ext 9 ofs) ||
+  (** or scaled 12-bit unsigned *)
+  (Int64.eq (Int64.modu ofs isz) Int64.zero
+   && Int64.ltu ofs (Int64.shl isz (Int64.repr 12))).
+ 
+Definition transl_addressing (sz: Z) (addr: Op.addressing) (args: list mreg)
+                             (insn: Asm.addressing -> instruction) (k: code) : res code :=
+  match addr, args with
+  | Aindexed ofs, a1 :: nil =>
+      do r1 <- ireg_of a1;
+       if offset_representable sz ofs then
+        OK (insn (ADimm r1 ofs) :: k)
+      else
+        OK (loadimm64 X16 ofs (insn (ADreg r1 X16) :: k))
+  | Aindexed2, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (insn (ADreg r1 r2) :: k)
+  | Aindexed2shift a, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      if Int.eq a Int.zero then
+        OK (insn (ADreg r1 r2) :: k)
+      else if Int.eq (Int.shl Int.one a) (Int.repr sz) then
+        OK (insn (ADlsl r1 r2 a) :: k)
+      else
+        OK (Padd X X16 r1 r2 (SOlsl a) :: insn (ADimm X16 Int64.zero) :: k)
+  | Aindexed2ext x a, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      if Int.eq a Int.zero || Int.eq (Int.shl Int.one a) (Int.repr sz) then
+        OK (insn (match x with Xsgn32 => ADsxt r1 r2 a
+                             | Xuns32 => ADuxt r1 r2 a end) :: k)
+      else
+        OK (arith_extended Paddext (Padd X) X16 r1 r2 x a
+                           (insn (ADimm X16 Int64.zero) :: k))
+  | Aglobal id ofs, nil =>
+      assertion (negb (Archi.pic_code tt));
+      if Ptrofs.eq (Ptrofs.modu ofs (Ptrofs.repr sz)) Ptrofs.zero && symbol_is_aligned id sz
+      then OK (Padrp X16 id ofs :: insn (ADadr X16 id ofs) :: k)
+      else OK (loadsymbol X16 id ofs (insn (ADimm X16 Int64.zero) :: k))
+  | Ainstack ofs, nil =>
+      let ofs := Ptrofs.to_int64 ofs in
+      if offset_representable sz ofs then
+        OK (insn (ADimm XSP ofs) :: k)
+      else
+        OK (loadimm64 X16 ofs (insn (ADreg XSP X16) :: k))
+  | _, _ =>
+      Error(msg "Asmgen.transl_addressing")
+  end.
+
+(** Translation of loads and stores *)
+
+Definition transl_load (trap: trapping_mode)
+                       (chunk: memory_chunk) (addr: Op.addressing)
+                       (args: list mreg) (dst: mreg) (k: code) : res code :=
+  match trap with
+  | NOTRAP => Error (msg "Asmgen.transl_load non-trapping loads unsupported on aarch64")
+  | TRAP =>
+  match chunk with
+  | Mint8unsigned =>
+      do rd <- ireg_of dst; transl_addressing 1 addr args (Pldrb W rd) k
+  | Mint8signed =>
+      do rd <- ireg_of dst; transl_addressing 1 addr args (Pldrsb W rd) k
+  | Mint16unsigned =>
+      do rd <- ireg_of dst; transl_addressing 2 addr args (Pldrh W rd) k
+  | Mint16signed =>
+      do rd <- ireg_of dst; transl_addressing 2 addr args (Pldrsh W rd) k
+  | Mint32 =>
+      do rd <- ireg_of dst; transl_addressing 4 addr args (Pldrw rd) k
+  | Mint64 =>
+      do rd <- ireg_of dst; transl_addressing 8 addr args (Pldrx rd) k
+  | Mfloat32 =>
+      do rd <- freg_of dst; transl_addressing 4 addr args (Pldrs rd) k
+  | Mfloat64 =>
+      do rd <- freg_of dst; transl_addressing 8 addr args (Pldrd rd) k
+  | Many32 =>
+      do rd <- ireg_of dst; transl_addressing 4 addr args (Pldrw_a rd) k
+  | Many64 =>
+      do rd <- ireg_of dst; transl_addressing 8 addr args (Pldrx_a rd) k
+  end
+  end.
+
+Definition transl_store (chunk: memory_chunk) (addr: Op.addressing)
+                        (args: list mreg) (src: mreg) (k: code) : res code :=
+  match chunk with
+  | Mint8unsigned | Mint8signed =>
+      do r1 <- ireg_of src; transl_addressing 1 addr args (Pstrb r1) k
+  | Mint16unsigned | Mint16signed =>
+      do r1 <- ireg_of src; transl_addressing 2 addr args (Pstrh r1) k
+  | Mint32 =>
+      do r1 <- ireg_of src; transl_addressing 4 addr args (Pstrw r1) k
+  | Mint64 =>
+      do r1 <- ireg_of src; transl_addressing 8 addr args (Pstrx r1) k
+  | Mfloat32 =>
+      do r1 <- freg_of src; transl_addressing 4 addr args (Pstrs r1) k
+  | Mfloat64 =>
+      do r1 <- freg_of src; transl_addressing 8 addr args (Pstrd r1) k
+  | Many32 =>
+      do r1 <- ireg_of src; transl_addressing 4 addr args (Pstrw_a r1) k
+  | Many64 =>
+      do r1 <- ireg_of src; transl_addressing 8 addr args (Pstrx_a r1) k
+  end.
+
+(** Register-indexed loads and stores *)
+
+Definition indexed_memory_access (insn: Asm.addressing -> instruction)
+                                 (sz: Z) (base: iregsp) (ofs: ptrofs) (k: code) :=
+  let ofs := Ptrofs.to_int64 ofs in
+  if offset_representable sz ofs
+  then insn (ADimm base ofs) :: k
+  else loadimm64 X16 ofs (insn (ADreg base X16) :: k).
+
+Definition loadind (base: iregsp) (ofs: ptrofs) (ty: typ) (dst: mreg) (k: code) :=
+  match ty, preg_of dst with
+  | Tint,    IR rd => OK (indexed_memory_access (Pldrw rd) 4 base ofs k)
+  | Tlong,   IR rd => OK (indexed_memory_access (Pldrx rd) 8 base ofs k)
+  | Tsingle, FR rd => OK (indexed_memory_access (Pldrs rd) 4 base ofs k)
+  | Tfloat,  FR rd => OK (indexed_memory_access (Pldrd rd) 8 base ofs k)
+  | Tany32,  IR rd => OK (indexed_memory_access (Pldrw_a rd) 4 base ofs k)
+  | Tany64,  IR rd => OK (indexed_memory_access (Pldrx_a rd) 8 base ofs k)
+  | Tany64,  FR rd => OK (indexed_memory_access (Pldrd_a rd) 8 base ofs k)
+  | _, _           => Error (msg "Asmgen.loadind")
+  end.
+
+Definition storeind (src: mreg) (base: iregsp) (ofs: ptrofs) (ty: typ) (k: code) :=
+  match ty, preg_of src with
+  | Tint,    IR rd => OK (indexed_memory_access (Pstrw rd) 4 base ofs k)
+  | Tlong,   IR rd => OK (indexed_memory_access (Pstrx rd) 8 base ofs k)
+  | Tsingle, FR rd => OK (indexed_memory_access (Pstrs rd) 4 base ofs k)
+  | Tfloat,  FR rd => OK (indexed_memory_access (Pstrd rd) 8 base ofs k)
+  | Tany32,  IR rd => OK (indexed_memory_access (Pstrw_a rd) 4 base ofs k)
+  | Tany64,  IR rd => OK (indexed_memory_access (Pstrx_a rd) 8 base ofs k)
+  | Tany64,  FR rd => OK (indexed_memory_access (Pstrd_a rd) 8 base ofs k)
+  | _, _           => Error (msg "Asmgen.storeind")
+  end.
+
+Definition loadptr (base: iregsp) (ofs: ptrofs) (dst: ireg) (k: code) :=
+  indexed_memory_access (Pldrx dst) 8 base ofs k.
+
+Definition storeptr (src: ireg) (base: iregsp) (ofs: ptrofs) (k: code) :=
+  indexed_memory_access (Pstrx src) 8 base ofs k.
+
+(** Function epilogue *)
+
+Definition make_epilogue (f: Mach.function) (k: code) :=
+  (* FIXME
+     Cannot be used because memcpy destroys X30;
+     issue being discussed with X. Leroy *)
+  (* if is_leaf_function f
+  then Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: k
+  else*) loadptr XSP f.(fn_retaddr_ofs) RA
+         (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: k).
+  
+(** Translation of a Mach instruction. *)
+
+Definition transl_instr (f: Mach.function) (i: Mach.instruction)
+                        (r29_is_parent: bool) (k: code) : res code :=
+  match i with
+  | Mgetstack ofs ty dst =>
+      loadind XSP ofs ty dst k
+  | Msetstack src ofs ty =>
+      storeind src XSP ofs ty k
+  | Mgetparam ofs ty dst =>
+      (* load via the frame pointer if it is valid *)
+      do c <- loadind X29 ofs ty dst k;
+      OK (if r29_is_parent then c else loadptr XSP f.(fn_link_ofs) X29 c)
+  | Mop op args res =>
+      transl_op op args res k
+  | Mload trap chunk addr args dst =>
+      transl_load trap chunk addr args dst k
+  | Mstore chunk addr args src =>
+      transl_store chunk addr args src k
+  | Mcall sig (inl r) =>
+      do r1 <- ireg_of r; OK (Pblr r1 sig :: k)
+  | Mcall sig (inr symb) =>
+      OK (Pbl symb sig :: k)
+  | Mtailcall sig (inl r) =>
+      do r1 <- ireg_of r;
+      OK (make_epilogue f (Pbr r1 sig :: k))
+  | Mtailcall sig (inr symb) =>
+      OK (make_epilogue f (Pbs symb sig :: k))
+  | Mbuiltin ef args res =>
+      OK (Pbuiltin ef (List.map (map_builtin_arg preg_of) args) (map_builtin_res preg_of res) :: k)
+  | Mlabel lbl =>
+      OK (Plabel lbl :: k)
+  | Mgoto lbl =>
+      OK (Pb lbl :: k)
+  | Mcond cond args lbl =>
+      transl_cond_branch cond args lbl k
+  | Mjumptable arg tbl =>
+      do r <- ireg_of arg;
+      OK (Pbtbl r tbl :: k)
+  | Mreturn =>
+      OK (make_epilogue f (Pret RA :: k))
+  end.
+
+(** Translation of a code sequence *)
+
+Definition it1_is_parent (before: bool) (i: Mach.instruction) : bool :=
+  match i with
+  | Msetstack src ofs ty => before
+  | Mgetparam ofs ty dst => negb (mreg_eq dst R29)
+  | Mop op args res => before && negb (mreg_eq res R29)
+  | _ => false
+  end.
+
+(** This is the naive definition that we no longer use because it
+  is not tail-recursive.  It is kept as specification. *)
+
+Fixpoint transl_code (f: Mach.function) (il: list Mach.instruction) (it1p: bool) :=
+  match il with
+  | nil => OK nil
+  | i1 :: il' =>
+      do k <- transl_code f il' (it1_is_parent it1p i1);
+      transl_instr f i1 it1p k
+  end.
+
+(** This is an equivalent definition in continuation-passing style
+  that runs in constant stack space. *)
+
+Fixpoint transl_code_rec (f: Mach.function) (il: list Mach.instruction)
+                         (it1p: bool) (k: code -> res code) :=
+  match il with
+  | nil => k nil
+  | i1 :: il' =>
+      transl_code_rec f il' (it1_is_parent it1p i1)
+        (fun c1 => do c2 <- transl_instr f i1 it1p c1; k c2)
+  end.
+
+Definition transl_code' (f: Mach.function) (il: list Mach.instruction) (it1p: bool) :=
+  transl_code_rec f il it1p (fun c => OK c).
+
+(** Translation of a whole function.  Note that we must check
+  that the generated code contains less than [2^32] instructions,
+  otherwise the offset part of the [PC] code pointer could wrap
+  around, leading to incorrect executions. *)
+
+Definition transl_function (f: Mach.function) :=
+  do c <- transl_code' f f.(Mach.fn_code) true;
+  OK (mkfunction f.(Mach.fn_sig)
+        (Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::
+         storeptr RA XSP f.(fn_retaddr_ofs) c)).
+
+*)
\ No newline at end of file
diff --git a/aarch64/Asmblockgenproof.v b/aarch64/Asmblockgenproof.v
new file mode 100644
index 00000000..bcd4495f
--- /dev/null
+++ b/aarch64/Asmblockgenproof.v
@@ -0,0 +1,1104 @@
+(* ORIGINAL aarch64/Asmgenproof file that needs to be adapted
+
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*         Xavier Leroy, Collège de France and INRIA Paris             *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Correctness proof for AArch64 code generation. *)
+
+Require Import Coqlib Errors.
+Require Import Integers Floats AST Linking.
+Require Import Values Memory Events Globalenvs Smallstep.
+Require Import Op Locations Mach Conventions Asm.
+Require Import Asmgen Asmgenproof0 Asmgenproof1.
+
+Definition match_prog (p: Mach.program) (tp: Asm.program) :=
+  match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp.
+
+Lemma transf_program_match:
+  forall p tp, transf_program p = OK tp -> match_prog p tp.
+Proof.
+  intros. eapply match_transform_partial_program; eauto.
+Qed.
+
+Section PRESERVATION.
+
+Variable prog: Mach.program.
+Variable tprog: Asm.program.
+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).
+
+Lemma functions_transl:
+  forall fb f tf,
+  Genv.find_funct_ptr ge fb = Some (Internal f) ->
+  transf_function f = OK tf ->
+  Genv.find_funct_ptr tge fb = Some (Internal tf).
+Proof.
+  intros. exploit functions_translated; eauto. intros [tf' [A B]].
+  monadInv B. rewrite H0 in EQ; inv EQ; auto.
+Qed.
+
+(** * Properties of control flow *)
+
+Lemma transf_function_no_overflow:
+  forall f tf,
+  transf_function f = OK tf -> list_length_z tf.(fn_code) <= Ptrofs.max_unsigned.
+Proof.
+  intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (list_length_z x.(fn_code))); inv EQ0.
+  omega.
+Qed.
+
+Lemma exec_straight_exec:
+  forall fb f c ep tf tc c' rs m rs' m',
+  transl_code_at_pc ge (rs PC) fb f c ep tf tc ->
+  exec_straight tge tf tc rs m c' rs' m' ->
+  plus step tge (State rs m) E0 (State rs' m').
+Proof.
+  intros. inv H.
+  eapply exec_straight_steps_1; eauto.
+  eapply transf_function_no_overflow; eauto.
+  eapply functions_transl; eauto.
+Qed.
+
+Lemma exec_straight_at:
+  forall fb f c ep tf tc c' ep' tc' rs m rs' m',
+  transl_code_at_pc ge (rs PC) fb f c ep tf tc ->
+  transl_code f c' ep' = OK tc' ->
+  exec_straight tge tf tc rs m tc' rs' m' ->
+  transl_code_at_pc ge (rs' PC) fb f c' ep' tf tc'.
+Proof.
+  intros. inv H.
+  exploit exec_straight_steps_2; eauto.
+  eapply transf_function_no_overflow; eauto.
+  eapply functions_transl; eauto.
+  intros [ofs' [PC' CT']].
+  rewrite PC'. constructor; auto.
+Qed.
+
+(** The following lemmas show that the translation from Mach to Asm
+  preserves labels, in the sense that the following diagram commutes:
+<<
+                          translation
+        Mach code ------------------------ Asm instr sequence
+            |                                          |
+            | Mach.find_label lbl       find_label lbl |
+            |                                          |
+            v                                          v
+        Mach code tail ------------------- Asm instr seq tail
+                          translation
+>>
+  The proof demands many boring lemmas showing that Asm constructor
+  functions do not introduce new labels.
+*)
+
+Section TRANSL_LABEL.
+
+Remark loadimm_z_label: forall sz rd l k, tail_nolabel k (loadimm_z sz rd l k).
+Proof. 
+  intros; destruct l as [ | [n1 p1] l]; simpl; TailNoLabel.
+  induction l as [ | [n p] l]; simpl; TailNoLabel.
+Qed.
+
+Remark loadimm_n_label: forall sz rd l k, tail_nolabel k (loadimm_n sz rd l k).
+Proof. 
+  intros; destruct l as [ | [n1 p1] l]; simpl; TailNoLabel.
+  induction l as [ | [n p] l]; simpl; TailNoLabel.
+Qed.
+
+Remark loadimm_label: forall sz rd n k, tail_nolabel k (loadimm sz rd n k).
+Proof.
+  unfold loadimm; intros. destruct Nat.leb; [apply loadimm_z_label|apply loadimm_n_label].
+Qed.
+Hint Resolve loadimm_label: labels.
+
+Remark loadimm32_label: forall r n k, tail_nolabel k (loadimm32 r n k).
+Proof.
+  unfold loadimm32; intros. destruct (is_logical_imm32 n); TailNoLabel.
+Qed.
+Hint Resolve loadimm32_label: labels.
+
+Remark loadimm64_label: forall r n k, tail_nolabel k (loadimm64 r n k).
+Proof.
+  unfold loadimm64; intros. destruct (is_logical_imm64 n); TailNoLabel.
+Qed.
+Hint Resolve loadimm64_label: labels.
+
+Remark addimm_aux: forall insn rd r1 n k,
+  (forall rd r1 n, nolabel (insn rd r1 n)) ->
+  tail_nolabel k (addimm_aux insn rd r1 n k).
+Proof.
+  unfold addimm_aux; intros. 
+  destruct Z.eqb. TailNoLabel. destruct Z.eqb; TailNoLabel.
+Qed.
+
+Remark addimm32_label: forall rd r1 n k, tail_nolabel k (addimm32 rd r1 n k).
+Proof.
+  unfold addimm32; intros. 
+  destruct Int.eq. apply addimm_aux; intros; red; auto.
+  destruct Int.eq. apply addimm_aux; intros; red; auto.
+  destruct Int.lt; eapply tail_nolabel_trans; TailNoLabel.
+Qed.
+Hint Resolve addimm32_label: labels.
+
+Remark addimm64_label: forall rd r1 n k, tail_nolabel k (addimm64 rd r1 n k).
+Proof.
+  unfold addimm64; intros. 
+  destruct Int64.eq. apply addimm_aux; intros; red; auto.
+  destruct Int64.eq. apply addimm_aux; intros; red; auto.
+  destruct Int64.lt; eapply tail_nolabel_trans; TailNoLabel.
+Qed.
+Hint Resolve addimm64_label: labels.
+
+Remark logicalimm32_label: forall insn1 insn2 rd r1 n k,
+  (forall rd r1 n, nolabel (insn1 rd r1 n)) ->
+  (forall rd r1 r2 s, nolabel (insn2 rd r1 r2 s)) ->
+  tail_nolabel k (logicalimm32 insn1 insn2 rd r1 n k).
+Proof.
+  unfold logicalimm32; intros.
+  destruct (is_logical_imm32 n). TailNoLabel. eapply tail_nolabel_trans; TailNoLabel.
+Qed.
+
+Remark logicalimm64_label: forall insn1 insn2 rd r1 n k,
+  (forall rd r1 n, nolabel (insn1 rd r1 n)) ->
+  (forall rd r1 r2 s, nolabel (insn2 rd r1 r2 s)) ->
+  tail_nolabel k (logicalimm64 insn1 insn2 rd r1 n k).
+Proof.
+  unfold logicalimm64; intros.
+  destruct (is_logical_imm64 n). TailNoLabel. eapply tail_nolabel_trans; TailNoLabel.
+Qed.
+
+Remark move_extended_label: forall rd r1 ex a k, tail_nolabel k (move_extended rd r1 ex a k).
+Proof.
+  unfold move_extended, move_extended_base; intros. destruct Int.eq, ex; TailNoLabel.
+Qed.
+Hint Resolve move_extended_label: labels.
+
+Remark arith_extended_label: forall insnX insnS rd r1 r2 ex a k,
+  (forall rd r1 r2 x, nolabel (insnX rd r1 r2 x)) ->
+  (forall rd r1 r2 s, nolabel (insnS rd r1 r2 s)) ->
+  tail_nolabel k (arith_extended insnX insnS rd r1 r2 ex a k).
+Proof.
+  unfold arith_extended; intros. destruct Int.ltu.
+  TailNoLabel.
+  destruct ex; simpl; TailNoLabel.
+Qed.
+
+Remark loadsymbol_label: forall r id ofs k, tail_nolabel k (loadsymbol r id ofs k).
+Proof.
+  intros; unfold loadsymbol.
+  destruct (Archi.pic_code tt); TailNoLabel. destruct Ptrofs.eq; TailNoLabel.
+Qed. 
+Hint Resolve loadsymbol_label: labels.
+
+Remark transl_cond_label: forall cond args k c,
+  transl_cond cond args k = OK c -> tail_nolabel k c.
+Proof.
+  unfold transl_cond; intros; destruct cond; TailNoLabel.
+- destruct is_arith_imm32; TailNoLabel. destruct is_arith_imm32; TailNoLabel. eapply tail_nolabel_trans; TailNoLabel.
+- destruct is_arith_imm32; TailNoLabel. destruct is_arith_imm32; TailNoLabel. eapply tail_nolabel_trans; TailNoLabel.
+- destruct is_logical_imm32; TailNoLabel. eapply tail_nolabel_trans; TailNoLabel.
+- destruct is_logical_imm32; TailNoLabel. eapply tail_nolabel_trans; TailNoLabel.
+- destruct is_arith_imm64; TailNoLabel. destruct is_arith_imm64; TailNoLabel. eapply tail_nolabel_trans; TailNoLabel.
+- destruct is_arith_imm64; TailNoLabel. destruct is_arith_imm64; TailNoLabel. eapply tail_nolabel_trans; TailNoLabel.
+- destruct is_logical_imm64; TailNoLabel. eapply tail_nolabel_trans; TailNoLabel.
+- destruct is_logical_imm64; TailNoLabel. eapply tail_nolabel_trans; TailNoLabel.
+Qed.
+
+Remark transl_cond_branch_default_label: forall cond args lbl k c,
+  transl_cond_branch_default cond args lbl k = OK c -> tail_nolabel k c.
+Proof.
+  unfold transl_cond_branch_default; intros. 
+  eapply tail_nolabel_trans; [eapply transl_cond_label;eauto|TailNoLabel].
+Qed.
+Hint Resolve transl_cond_branch_default_label: labels.
+
+Remark transl_cond_branch_label: forall cond args lbl k c,
+  transl_cond_branch cond args lbl k = OK c -> tail_nolabel k c.
+Proof.
+  unfold transl_cond_branch; intros; destruct args; TailNoLabel; destruct cond; TailNoLabel.
+- destruct c0; TailNoLabel.
+- destruct c0; TailNoLabel.
+- destruct (Int.is_power2 n); TailNoLabel.
+- destruct (Int.is_power2 n); TailNoLabel.
+- destruct c0; TailNoLabel.
+- destruct c0; TailNoLabel.
+- destruct (Int64.is_power2' n); TailNoLabel.
+- destruct (Int64.is_power2' n); TailNoLabel.
+Qed.
+
+Remark transl_op_label:
+  forall op args r k c,
+  transl_op op args r k = OK c -> tail_nolabel k c.
+Proof.
+  unfold transl_op; intros; destruct op; TailNoLabel.
+- destruct (preg_of r); try discriminate; destruct (preg_of m); inv H; TailNoLabel.
+- destruct (Float.eq_dec n Float.zero); TailNoLabel.
+- destruct (Float32.eq_dec n Float32.zero); TailNoLabel.
+- apply logicalimm32_label; unfold nolabel; auto.
+- apply logicalimm32_label; unfold nolabel; auto.
+- apply logicalimm32_label; unfold nolabel; auto.
+- unfold shrx32. destruct (Int.eq _ _); try destruct (Int.eq _ _); TailNoLabel.
+- apply arith_extended_label; unfold nolabel; auto.
+- apply arith_extended_label; unfold nolabel; auto.
+- apply logicalimm64_label; unfold nolabel; auto.
+- apply logicalimm64_label; unfold nolabel; auto.
+- apply logicalimm64_label; unfold nolabel; auto.
+- unfold shrx64. destruct (Int.eq _ _); try destruct (Int.eq _ _); TailNoLabel.
+- eapply tail_nolabel_trans. eapply transl_cond_label; eauto. TailNoLabel.
+- destruct (preg_of r); try discriminate; TailNoLabel;
+  (eapply tail_nolabel_trans; [eapply transl_cond_label; eauto | TailNoLabel]).
+Qed.
+
+Remark transl_addressing_label:
+  forall sz addr args insn k c,
+  transl_addressing sz addr args insn k = OK c ->
+  (forall ad, nolabel (insn ad)) ->
+  tail_nolabel k c.
+Proof.
+  unfold transl_addressing; intros; destruct addr; TailNoLabel;
+  eapply tail_nolabel_trans; TailNoLabel.
+  eapply tail_nolabel_trans. apply arith_extended_label; unfold nolabel; auto. TailNoLabel.
+Qed.
+
+Remark transl_load_label:
+  forall trap chunk addr args dst k c,
+  transl_load trap chunk addr args dst k = OK c -> tail_nolabel k c.
+Proof.
+  unfold transl_load; intros; destruct trap; try discriminate; destruct chunk; TailNoLabel; eapply transl_addressing_label; eauto; unfold nolabel; auto.
+Qed.
+
+Remark transl_store_label:
+  forall chunk addr args src k c,
+  transl_store chunk addr args src k = OK c -> tail_nolabel k c.
+Proof.
+  unfold transl_store; intros; destruct chunk; TailNoLabel; eapply transl_addressing_label; eauto; unfold nolabel; auto.
+Qed.
+
+Remark indexed_memory_access_label:
+  forall insn sz base ofs k,
+  (forall ad, nolabel (insn ad)) ->
+  tail_nolabel k (indexed_memory_access insn sz base ofs k).
+Proof.
+  unfold indexed_memory_access; intros. destruct offset_representable.
+  TailNoLabel.
+  eapply tail_nolabel_trans; TailNoLabel.
+Qed.
+
+Remark loadind_label:
+  forall base ofs ty dst k c,
+  loadind base ofs ty dst k = OK c -> tail_nolabel k c.
+Proof.
+  unfold loadind; intros.
+  destruct ty, (preg_of dst); inv H; apply indexed_memory_access_label; intros; exact I.
+Qed.
+
+Remark storeind_label:
+  forall src base ofs ty k c,
+  storeind src base ofs ty k = OK c -> tail_nolabel k c.
+Proof.
+  unfold storeind; intros.
+  destruct ty, (preg_of src); inv H; apply indexed_memory_access_label; intros; exact I.
+Qed.
+
+Remark loadptr_label:
+  forall base ofs dst k, tail_nolabel k (loadptr base ofs dst k).
+Proof.
+  intros. apply indexed_memory_access_label. unfold nolabel; auto.
+Qed.
+
+Remark storeptr_label:
+  forall src base ofs k, tail_nolabel k (storeptr src base ofs k).
+Proof.
+  intros. apply indexed_memory_access_label. unfold nolabel; auto.
+Qed.
+
+Remark make_epilogue_label:
+  forall f k, tail_nolabel k (make_epilogue f k).
+Proof.
+  unfold make_epilogue; intros.
+  (* FIXME destruct is_leaf_function.
+  { TailNoLabel. } *)
+  eapply tail_nolabel_trans.
+  apply loadptr_label.
+  TailNoLabel.
+Qed.
+
+Lemma transl_instr_label:
+  forall f i ep k c,
+  transl_instr f i ep k = OK c ->
+  match i with Mlabel lbl => c = Plabel lbl :: k | _ => tail_nolabel k c end.
+Proof.
+  unfold transl_instr; intros; destruct i; TailNoLabel.
+- eapply loadind_label; eauto.
+- eapply storeind_label; eauto.
+- destruct ep. eapply loadind_label; eauto.
+  eapply tail_nolabel_trans. apply loadptr_label. eapply loadind_label; eauto. 
+- eapply transl_op_label; eauto.
+- eapply transl_load_label; eauto. 
+- eapply transl_store_label; eauto.
+- destruct s0; monadInv H; TailNoLabel.
+- destruct s0; monadInv H; (eapply tail_nolabel_trans; [eapply make_epilogue_label|TailNoLabel]).
+- eapply transl_cond_branch_label; eauto.
+- eapply tail_nolabel_trans; [eapply make_epilogue_label|TailNoLabel].
+Qed.
+
+Lemma transl_instr_label':
+  forall lbl f i ep k c,
+  transl_instr f i ep k = OK c ->
+  find_label lbl c = if Mach.is_label lbl i then Some k else find_label lbl k.
+Proof.
+  intros. exploit transl_instr_label; eauto.
+  destruct i; try (intros [A B]; apply B).
+  intros. subst c. simpl. auto.
+Qed.
+
+Lemma transl_code_label:
+  forall lbl f c ep tc,
+  transl_code f c ep = OK tc ->
+  match Mach.find_label lbl c with
+  | None => find_label lbl tc = None
+  | Some c' => exists tc', find_label lbl tc = Some tc' /\ transl_code f c' false = OK tc'
+  end.
+Proof.
+  induction c; simpl; intros.
+  inv H. auto.
+  monadInv H. rewrite (transl_instr_label' lbl _ _ _ _ _ EQ0).
+  generalize (Mach.is_label_correct lbl a).
+  destruct (Mach.is_label lbl a); intros.
+  subst a. simpl in EQ. exists x; auto.
+  eapply IHc; eauto.
+Qed.
+
+Lemma transl_find_label:
+  forall lbl f tf,
+  transf_function f = OK tf ->
+  match Mach.find_label lbl f.(Mach.fn_code) with
+  | None => find_label lbl tf.(fn_code) = None
+  | Some c => exists tc, find_label lbl tf.(fn_code) = Some tc /\ transl_code f c false = OK tc
+  end.
+Proof.
+  intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (list_length_z x.(fn_code))); inv EQ0.
+  monadInv EQ. rewrite transl_code'_transl_code in EQ0. unfold fn_code. 
+  simpl. destruct (storeptr_label X30 XSP (fn_retaddr_ofs f) x) as [A B]; rewrite B. 
+  eapply transl_code_label; eauto.
+Qed.
+
+End TRANSL_LABEL.
+
+(** A valid branch in a piece of Mach code translates to a valid ``go to''
+  transition in the generated Asm code. *)
+
+Lemma find_label_goto_label:
+  forall f tf lbl rs m c' b ofs,
+  Genv.find_funct_ptr ge b = Some (Internal f) ->
+  transf_function f = OK tf ->
+  rs PC = Vptr b ofs ->
+  Mach.find_label lbl f.(Mach.fn_code) = Some c' ->
+  exists tc', exists rs',
+     goto_label tf lbl rs m = Next rs' m
+  /\ transl_code_at_pc ge (rs' PC) b f c' false tf tc'
+  /\ forall r, r <> PC -> rs'#r = rs#r.
+Proof.
+  intros. exploit (transl_find_label lbl f tf); eauto. rewrite H2.
+  intros [tc [A B]].
+  exploit label_pos_code_tail; eauto. instantiate (1 := 0).
+  intros [pos' [P [Q R]]].
+  exists tc; exists (rs#PC <- (Vptr b (Ptrofs.repr pos'))).
+  split. unfold goto_label. rewrite P. rewrite H1. auto.
+  split. rewrite Pregmap.gss. constructor; auto.
+  rewrite Ptrofs.unsigned_repr. replace (pos' - 0) with pos' in Q.
+  auto. omega.
+  generalize (transf_function_no_overflow _ _ H0). omega.
+  intros. apply Pregmap.gso; auto.
+Qed.
+
+(** Existence of return addresses *)
+
+Lemma return_address_exists:
+  forall f sg ros c, is_tail (Mcall sg ros :: c) f.(Mach.fn_code) ->
+  exists ra, return_address_offset f c ra.
+Proof.
+  intros. eapply Asmgenproof0.return_address_exists; eauto.
+- intros. exploit transl_instr_label; eauto.
+  destruct i; try (intros [A B]; apply A). intros. subst c0. repeat constructor.
+- intros. monadInv H0.
+  destruct (zlt Ptrofs.max_unsigned (list_length_z x.(fn_code))); inv EQ0. monadInv EQ.
+  rewrite transl_code'_transl_code in EQ0.
+  exists x; exists true; split; auto. unfold fn_code.
+  constructor. apply (storeptr_label X30 XSP (fn_retaddr_ofs f0) x).
+- exact transf_function_no_overflow.
+Qed.
+
+(** * Proof of semantic preservation *)
+
+(** Semantic preservation is proved using simulation diagrams
+  of the following form.
+<<
+           st1 --------------- st2
+            |                   |
+           t|                  *|t
+            |                   |
+            v                   v
+           st1'--------------- st2'
+>>
+  The invariant is the [match_states] predicate below, which includes:
+- The Asm code pointed by the PC register is the translation of
+  the current Mach code sequence.
+- Mach register values and Asm register values agree.
+*)
+
+Inductive match_states: Mach.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)
+        (LEAF: is_leaf_function f = true -> rs#RA = parent_ra s),
+      match_states (Mach.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 (Mach.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 (Mach.Returnstate s ms m)
+                   (Asm.State rs m').
+
+Lemma exec_straight_steps:
+  forall s fb f rs1 i c ep tf tc m1' m2 m2' sp ms2,
+  match_stack ge s ->
+  Mem.extends m2 m2' ->
+  Genv.find_funct_ptr ge fb = Some (Internal f) ->
+  transl_code_at_pc ge (rs1 PC) fb f (i :: c) ep tf tc ->
+  (forall k c (TR: transl_instr f i ep k = OK c),
+   exists rs2,
+       exec_straight tge tf c rs1 m1' k rs2 m2'
+    /\ agree ms2 sp rs2
+    /\ (it1_is_parent ep i = true -> rs2#X29 = parent_sp s)
+    /\ (is_leaf_function f = true -> rs2#RA = parent_ra s)) ->
+  exists st',
+  plus step tge (State rs1 m1') E0 st' /\
+  match_states (Mach.State s fb sp c ms2 m2) st'.
+Proof.
+  intros. inversion H2. subst. monadInv H7.
+  exploit H3; eauto. intros [rs2 [A [B [C D]]]].
+  exists (State rs2 m2'); split.
+  - eapply exec_straight_exec; eauto.
+  - econstructor; eauto. eapply exec_straight_at; eauto.
+Qed.
+
+Lemma exec_straight_steps_goto:
+  forall s fb f rs1 i c ep tf tc m1' m2 m2' sp ms2 lbl c',
+  match_stack ge s ->
+  Mem.extends m2 m2' ->
+  Genv.find_funct_ptr ge fb = Some (Internal f) ->
+  Mach.find_label lbl f.(Mach.fn_code) = Some c' ->
+  transl_code_at_pc ge (rs1 PC) fb f (i :: c) ep tf tc ->
+  it1_is_parent ep i = false ->
+  (forall k c (TR: transl_instr f i ep k = OK c),
+   exists jmp, exists k', exists rs2,
+       exec_straight tge tf c rs1 m1' (jmp :: k') rs2 m2'
+    /\ agree ms2 sp rs2
+    /\ exec_instr tge tf jmp rs2 m2' = goto_label tf lbl rs2 m2'
+    /\ (is_leaf_function f = true -> rs2#RA = parent_ra s)) ->
+  exists st',
+  plus step tge (State rs1 m1') E0 st' /\
+  match_states (Mach.State s fb sp c' ms2 m2) st'.
+Proof.
+  intros. inversion H3. subst. monadInv H9.
+  exploit H5; eauto. intros [jmp [k' [rs2 [A [B [C D]]]]]].
+  generalize (functions_transl _ _ _ H7 H8); intro FN.
+  generalize (transf_function_no_overflow _ _ H8); intro NOOV.
+  exploit exec_straight_steps_2; eauto.
+  intros [ofs' [PC2 CT2]].
+  exploit find_label_goto_label; eauto.
+  intros [tc' [rs3 [GOTO [AT' OTH]]]].
+  exists (State rs3 m2'); split.
+  eapply plus_right'.
+  eapply exec_straight_steps_1; eauto.
+  econstructor; eauto.
+  eapply find_instr_tail. eauto.
+  rewrite C. eexact GOTO.
+  traceEq.
+  econstructor; eauto.
+  apply agree_exten with rs2; auto with asmgen.
+  congruence.
+  rewrite OTH by congruence; auto.
+Qed.
+
+Lemma exec_straight_opt_steps_goto:
+  forall s fb f rs1 i c ep tf tc m1' m2 m2' sp ms2 lbl c',
+  match_stack ge s ->
+  Mem.extends m2 m2' ->
+  Genv.find_funct_ptr ge fb = Some (Internal f) ->
+  Mach.find_label lbl f.(Mach.fn_code) = Some c' ->
+  transl_code_at_pc ge (rs1 PC) fb f (i :: c) ep tf tc ->
+  it1_is_parent ep i = false ->
+  (forall k c (TR: transl_instr f i ep k = OK c),
+   exists jmp, exists k', exists rs2,
+       exec_straight_opt tge tf c rs1 m1' (jmp :: k') rs2 m2'
+    /\ agree ms2 sp rs2
+    /\ exec_instr tge tf jmp rs2 m2' = goto_label tf lbl rs2 m2'
+    /\ (is_leaf_function f = true -> rs2#RA = parent_ra s)) ->
+  exists st',
+  plus step tge (State rs1 m1') E0 st' /\
+  match_states (Mach.State s fb sp c' ms2 m2) st'.
+Proof.
+  intros. inversion H3. subst. monadInv H9.
+  exploit H5; eauto. intros [jmp [k' [rs2 [A [B [C D]]]]]].
+  generalize (functions_transl _ _ _ H7 H8); intro FN.
+  generalize (transf_function_no_overflow _ _ H8); intro NOOV.
+  inv A.
+- exploit find_label_goto_label; eauto.
+  intros [tc' [rs3 [GOTO [AT' OTH]]]].
+  exists (State rs3 m2'); split.
+  apply plus_one. econstructor; eauto.
+  eapply find_instr_tail. eauto.
+  rewrite C. eexact GOTO.
+  econstructor; eauto.
+  apply agree_exten with rs2; auto with asmgen.
+  congruence.
+  rewrite OTH by congruence; auto.
+- exploit exec_straight_steps_2; eauto.
+  intros [ofs' [PC2 CT2]].
+  exploit find_label_goto_label; eauto.
+  intros [tc' [rs3 [GOTO [AT' OTH]]]].
+  exists (State rs3 m2'); split.
+  eapply plus_right'.
+  eapply exec_straight_steps_1; eauto.
+  econstructor; eauto.
+  eapply find_instr_tail. eauto.
+  rewrite C. eexact GOTO.
+  traceEq.
+  econstructor; eauto.
+  apply agree_exten with rs2; auto with asmgen.
+  congruence.
+  rewrite OTH by congruence; auto.
+Qed.
+
+(** We need to show that, in the simulation diagram, we cannot
+  take infinitely many Mach transitions that correspond to zero
+  transitions on the Asm side.  Actually, all Mach transitions
+  correspond to at least one Asm transition, except the
+  transition from [Machsem.Returnstate] to [Machsem.State].
+  So, the following integer measure will suffice to rule out
+  the unwanted behaviour. *)
+
+Definition measure (s: Mach.state) : nat :=
+  match s with
+  | Mach.State _ _ _ _ _ _ => 0%nat
+  | Mach.Callstate _ _ _ _ => 0%nat
+  | Mach.Returnstate _ _ _ => 1%nat
+  end.
+
+Remark preg_of_not_X29: forall r, negb (mreg_eq r R29) = true -> IR X29 <> preg_of r.
+Proof.
+  intros. change (IR X29) with (preg_of R29). red; intros.
+  exploit preg_of_injective; eauto. intros; subst r; discriminate.
+Qed.
+
+Lemma sp_val': forall ms sp rs, agree ms sp rs -> sp = rs XSP.
+Proof.
+  intros. eapply sp_val; eauto. 
+Qed. 
+
+(** This is the simulation diagram.  We prove it by case analysis on the Mach transition. *)
+
+Theorem step_simulation:
+  forall S1 t S2, Mach.step return_address_offset ge S1 t S2 ->
+  forall S1' (MS: match_states S1 S1')  (WF: wf_state ge S1),
+  (exists S2', plus step tge S1' t S2' /\ match_states S2 S2')
+  \/ (measure S2 < measure S1 /\ t = E0 /\ match_states S2 S1')%nat.
+Proof.
+  induction 1; intros; inv MS.
+
+- (* Mlabel *)
+  left; eapply exec_straight_steps; eauto; intros.
+  monadInv TR. econstructor; split. apply exec_straight_one. simpl; eauto. auto.
+  split. { apply agree_nextinstr; auto. }
+  split. { simpl; congruence. }
+  rewrite nextinstr_inv by congruence; assumption.
+
+- (* Mgetstack *)
+  unfold load_stack in H.
+  exploit Mem.loadv_extends; eauto. intros [v' [A B]].
+  rewrite (sp_val _ _ _ AG) in A.
+  left; eapply exec_straight_steps; eauto. intros. simpl in TR.
+  exploit loadind_correct; eauto with asmgen. intros [rs' [P [Q [R S]]]].
+  exists rs'; split. eauto.
+  split. { eapply agree_set_mreg; eauto with asmgen. congruence. }
+  split. { simpl; congruence. }
+  rewrite S. assumption.
+
+- (* Msetstack *)
+  unfold store_stack in H.
+  assert (Val.lessdef (rs src) (rs0 (preg_of src))) by (eapply preg_val; eauto).
+  exploit Mem.storev_extends; eauto. intros [m2' [A B]].
+  left; eapply exec_straight_steps; eauto.
+  rewrite (sp_val _ _ _ AG) in A. intros. simpl in TR.
+  exploit storeind_correct; eauto with asmgen. intros [rs' [P [Q R]]].
+  exists rs'; split. eauto.
+  split. eapply agree_undef_regs; eauto with asmgen.
+  simpl; intros.
+  split. rewrite Q; auto with asmgen.
+  rewrite R. assumption.
+
+- (* Mgetparam *)
+  assert (f0 = f) by congruence; subst f0.
+  unfold load_stack in *.
+  exploit Mem.loadv_extends. eauto. eexact H0. auto.
+  intros [parent' [A B]]. rewrite (sp_val' _ _ _ AG) in A.
+  exploit lessdef_parent_sp; eauto. clear B; intros B; subst parent'.
+  exploit Mem.loadv_extends. eauto. eexact H1. auto.
+  intros [v' [C D]].
+Opaque loadind.
+  left; eapply exec_straight_steps; eauto; intros. monadInv TR. 
+  destruct ep.
+(* X30 contains parent *)
+  exploit loadind_correct. eexact EQ.
+  instantiate (2 := rs0). simpl; rewrite DXP; eauto. simpl; congruence.
+  intros [rs1 [P [Q [R S]]]].
+  exists rs1; split. eauto.
+  split. eapply agree_set_mreg. eapply agree_set_mreg; eauto. congruence. auto with asmgen.
+  simpl; split; intros.
+  { rewrite R; auto with asmgen.
+    apply preg_of_not_X29; auto.
+  }
+  { rewrite S; auto. }
+    
+(* X30 does not contain parent *)
+  exploit loadptr_correct. eexact A. simpl; congruence. intros [rs1 [P [Q R]]].
+  exploit loadind_correct. eexact EQ. instantiate (2 := rs1). simpl; rewrite Q. eauto. simpl; congruence.
+  intros [rs2 [S [T [U V]]]].
+  exists rs2; split. eapply exec_straight_trans; eauto.
+  split. eapply agree_set_mreg. eapply agree_set_mreg. eauto. eauto.
+  instantiate (1 := rs1#X29 <- (rs2#X29)). intros.
+  rewrite Pregmap.gso; auto with asmgen.
+  congruence.
+  intros. unfold Pregmap.set. destruct (PregEq.eq r' X29). congruence. auto with asmgen.
+  split; simpl; intros. rewrite U; auto with asmgen.
+  apply preg_of_not_X29; auto.
+  rewrite V. rewrite R by congruence. auto.
+  
+- (* Mop *)
+  assert (eval_operation tge sp op (map rs args) m = Some v).
+  { rewrite <- H. apply eval_operation_preserved. exact symbols_preserved. }
+  exploit eval_operation_lessdef. eapply preg_vals; eauto. eauto. eexact H0.
+  intros [v' [A B]]. rewrite (sp_val _ _ _ AG) in A.
+  left; eapply exec_straight_steps; eauto; intros. simpl in TR.
+  exploit transl_op_correct; eauto. intros [rs2 [P [Q [R S]]]].
+  exists rs2; split. eauto. split.
+  apply agree_set_undef_mreg with rs0; auto. 
+  apply Val.lessdef_trans with v'; auto.
+  split; simpl; intros. InvBooleans. 
+  rewrite R; auto. apply preg_of_not_X29; auto.
+Local Transparent destroyed_by_op.
+  destruct op; try exact I; simpl; congruence.
+  rewrite S.
+  auto.
+- (* Mload *)
+  destruct trap.
+  {
+  assert (Op.eval_addressing tge sp addr (map rs args) = Some a).
+  { rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved. }
+  exploit eval_addressing_lessdef. eapply preg_vals; eauto. eexact H1.
+  intros [a' [A B]]. rewrite (sp_val _ _ _ AG) in A.
+  exploit Mem.loadv_extends; eauto. intros [v' [C D]].
+  left; eapply exec_straight_steps; eauto; intros. simpl in TR.
+  exploit transl_load_correct; eauto. intros [rs2 [P [Q [R S]]]].
+  exists rs2; split. eauto.
+  split. eapply agree_set_undef_mreg; eauto. congruence.
+  split. simpl; congruence.
+  rewrite S. assumption.
+  }
+  
+  (* Mload notrap1 *)
+  inv AT. simpl in *. unfold bind in *. destruct (transl_code _ _ _) in *; discriminate.
+
+- (* Mload notrap *)
+  inv AT. simpl in *. unfold bind in *. destruct (transl_code _ _ _) in *; discriminate.
+
+- (* Mload notrap *)
+  inv AT. simpl in *. unfold bind in *. destruct (transl_code _ _ _) in *; discriminate.
+
+- (* Mstore *)
+  assert (Op.eval_addressing tge sp addr (map rs args) = Some a).
+  { rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved. }
+  exploit eval_addressing_lessdef. eapply preg_vals; eauto. eexact H1.
+  intros [a' [A B]]. rewrite (sp_val _ _ _ AG) in A.
+  assert (Val.lessdef (rs src) (rs0 (preg_of src))) by (eapply preg_val; eauto).
+  exploit Mem.storev_extends; eauto. intros [m2' [C D]].
+  left; eapply exec_straight_steps; eauto.
+  intros. simpl in TR. exploit transl_store_correct; eauto. intros [rs2 [P [Q R]]].
+  exists rs2; split. eauto.
+  split. eapply agree_undef_regs; eauto with asmgen.
+  split. simpl; congruence.
+  rewrite R. assumption.
+
+- (* Mcall *)
+  assert (f0 = f) by congruence.  subst f0.
+  inv AT.
+  assert (NOOV: list_length_z tf.(fn_code) <= Ptrofs.max_unsigned).
+  { eapply transf_function_no_overflow; eauto. }
+  destruct ros as [rf|fid]; simpl in H; monadInv H5.
++ (* Indirect call *)
+  assert (rs rf = Vptr f' Ptrofs.zero).
+  { destruct (rs rf); try discriminate.
+    revert H; predSpec Ptrofs.eq Ptrofs.eq_spec i Ptrofs.zero; intros; congruence. }
+  assert (rs0 x0 = Vptr f' Ptrofs.zero).
+  { exploit ireg_val; eauto. rewrite H5; intros LD; inv LD; auto. }
+  generalize (code_tail_next_int _ _ _ _ NOOV H6). intro CT1.
+  assert (TCA: transl_code_at_pc ge (Vptr fb (Ptrofs.add ofs Ptrofs.one)) fb f c false tf x).
+  {  econstructor; eauto. }
+  exploit return_address_offset_correct; eauto. intros; subst ra.
+  left; econstructor; split.
+  apply plus_one. eapply exec_step_internal. Simpl. rewrite <- H2; simpl; eauto.
+  eapply functions_transl; eauto. eapply find_instr_tail; eauto.
+  simpl. eauto.
+  econstructor; eauto.
+  econstructor; eauto.
+  eapply agree_sp_def; eauto.
+  simpl. eapply agree_exten; eauto. intros. Simpl.
+  Simpl. rewrite <- H2. auto.
++ (* Direct call *)
+  generalize (code_tail_next_int _ _ _ _ NOOV H6). intro CT1.
+  assert (TCA: transl_code_at_pc ge (Vptr fb (Ptrofs.add ofs Ptrofs.one)) fb f c false tf x).
+    econstructor; eauto.
+  exploit return_address_offset_correct; eauto. intros; subst ra.
+  left; econstructor; split.
+  apply plus_one. eapply exec_step_internal. eauto.
+  eapply functions_transl; eauto. eapply find_instr_tail; eauto.
+  simpl. unfold Genv.symbol_address. rewrite symbols_preserved. rewrite H. eauto.
+  econstructor; eauto.
+  econstructor; eauto.
+  eapply agree_sp_def; eauto.
+  simpl. eapply agree_exten; eauto. intros. Simpl.
+  Simpl. rewrite <- H2. auto.
+
+- (* Mtailcall *)
+  assert (f0 = f) by congruence.  subst f0.
+  inversion AT; subst.
+  assert (NOOV: list_length_z tf.(fn_code) <= Ptrofs.max_unsigned).
+  { eapply transf_function_no_overflow; eauto. }
+  exploit Mem.loadv_extends. eauto. eexact H1. auto. simpl. intros [parent' [A B]].
+  destruct ros as [rf|fid]; simpl in H; monadInv H7.
++ (* Indirect call *)
+  assert (rs rf = Vptr f' Ptrofs.zero).
+  { destruct (rs rf); try discriminate.
+    revert H; predSpec Ptrofs.eq Ptrofs.eq_spec i Ptrofs.zero; intros; congruence. }
+  assert (rs0 x0 = Vptr f' Ptrofs.zero).
+  { exploit ireg_val; eauto. rewrite H7; intros LD; inv LD; auto. }
+  exploit make_epilogue_correct; eauto. intros (rs1 & m1 & U & V & W & X & Y & Z). 
+  exploit exec_straight_steps_2; eauto using functions_transl.                      
+  intros (ofs' & P & Q).
+  left; econstructor; split.
+  (* execution *)
+  eapply plus_right'. eapply exec_straight_exec; eauto.
+  econstructor. eexact P. eapply functions_transl; eauto. eapply find_instr_tail. eexact Q.
+  simpl. reflexivity.
+  traceEq.
+  (* match states *)
+  econstructor; eauto.
+  apply agree_set_other; auto with asmgen.
+  Simpl. rewrite Z by (rewrite <- (ireg_of_eq _ _ EQ1); eauto with asmgen). assumption. 
++ (* Direct call *)
+  exploit make_epilogue_correct; eauto. intros (rs1 & m1 & U & V & W & X & Y & Z). 
+  exploit exec_straight_steps_2; eauto using functions_transl.                      
+  intros (ofs' & P & Q).
+  left; econstructor; split.
+  (* execution *)
+  eapply plus_right'. eapply exec_straight_exec; eauto.
+  econstructor. eexact P. eapply functions_transl; eauto. eapply find_instr_tail. eexact Q.
+  simpl. reflexivity.
+  traceEq.
+  (* match states *)
+  econstructor; eauto.
+  apply agree_set_other; auto with asmgen.
+  Simpl. unfold Genv.symbol_address. rewrite symbols_preserved. rewrite H. auto.
+
+- (* Mbuiltin *)
+  inv AT. monadInv H4.
+  exploit functions_transl; eauto. intro FN.
+  generalize (transf_function_no_overflow _ _ H3); intro NOOV.
+  exploit builtin_args_match; eauto. intros [vargs' [P Q]].
+  exploit external_call_mem_extends; eauto.
+  intros [vres' [m2' [A [B [C D]]]]].
+  left. econstructor; split. apply plus_one.
+  eapply exec_step_builtin. eauto. eauto.
+  eapply find_instr_tail; eauto.
+  erewrite <- sp_val by eauto.
+  eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved.
+  eapply external_call_symbols_preserved; eauto. apply senv_preserved.
+  eauto.
+  econstructor; eauto.
+  instantiate (2 := tf); instantiate (1 := x).
+  unfold nextinstr. rewrite Pregmap.gss.
+  rewrite set_res_other. rewrite undef_regs_other_2.
+  rewrite <- H1. simpl. econstructor; eauto.
+  eapply code_tail_next_int; eauto.
+  rewrite preg_notin_charact. intros. auto with asmgen.
+  auto with asmgen.
+  apply agree_nextinstr. eapply agree_set_res; auto.
+  eapply agree_undef_regs; eauto. intros. rewrite undef_regs_other_2; auto.
+  congruence.
+
+  Simpl.
+  rewrite set_res_other by trivial.
+  rewrite undef_regs_other.
+  assumption.
+  intro.
+  rewrite in_map_iff.
+  intros (x0 & PREG & IN).
+  subst r'.
+  intro.
+  apply (preg_of_not_RA x0).
+  congruence.
+  
+- (* Mgoto *)
+  assert (f0 = f) by congruence. subst f0.
+  inv AT. monadInv H4.
+  exploit find_label_goto_label; eauto. intros [tc' [rs' [GOTO [AT2 INV]]]].
+  left; exists (State rs' m'); split.
+  apply plus_one. econstructor; eauto.
+  eapply functions_transl; eauto.
+  eapply find_instr_tail; eauto.
+  simpl; eauto.
+  econstructor; eauto.
+  eapply agree_exten; eauto with asmgen.
+  congruence.
+
+  rewrite INV by congruence.
+  assumption.
+  
+- (* Mcond true *)
+  assert (f0 = f) by congruence. subst f0.
+  exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC.
+  left; eapply exec_straight_opt_steps_goto; eauto.
+  intros. simpl in TR.
+  exploit transl_cond_branch_correct; eauto. intros (rs' & jmp & A & B & C & D).
+  exists jmp; exists k; exists rs'.
+  split. eexact A. 
+  split. apply agree_exten with rs0; auto with asmgen.
+  split.
+  exact B.
+  rewrite D. exact LEAF.
+
+- (* Mcond false *)
+  exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC.
+  left; eapply exec_straight_steps; eauto. intros. simpl in TR.
+  exploit transl_cond_branch_correct; eauto. intros (rs' & jmp & A & B & C & D).
+  econstructor; split.
+  eapply exec_straight_opt_right. eexact A. apply exec_straight_one. eexact B. auto.
+  split. apply agree_exten with rs0; auto. intros. Simpl.
+  split.
+  simpl; congruence.
+  Simpl. rewrite D.
+  exact LEAF.
+
+- (* Mjumptable *)
+  assert (f0 = f) by congruence. subst f0.
+  inv AT. monadInv H6.
+  exploit functions_transl; eauto. intro FN.
+  generalize (transf_function_no_overflow _ _ H5); intro NOOV.
+  exploit find_label_goto_label. eauto. eauto.
+  instantiate (2 := rs0#X16 <- Vundef #X17 <- Vundef).
+  Simpl. eauto.
+  eauto.
+  intros [tc' [rs' [A [B C]]]].
+  exploit ireg_val; eauto. rewrite H. intros LD; inv LD.
+  left; econstructor; split.
+  apply plus_one. econstructor; eauto.
+  eapply find_instr_tail; eauto.
+  simpl. Simpl. rewrite <- H9. unfold Mach.label in H0; unfold label; rewrite H0. eexact A.
+  econstructor; eauto.
+  eapply agree_undef_regs; eauto.
+  simpl. intros. rewrite C; auto with asmgen. Simpl.
+  congruence.
+
+  rewrite C by congruence.
+  repeat rewrite Pregmap.gso by congruence.
+  assumption.
+  
+- (* Mreturn *)
+  assert (f0 = f) by congruence. subst f0.
+  inversion AT; subst. simpl in H6; monadInv H6.
+  assert (NOOV: list_length_z tf.(fn_code) <= Ptrofs.max_unsigned).
+    eapply transf_function_no_overflow; eauto.
+  exploit make_epilogue_correct; eauto. intros (rs1 & m1 & U & V & W & X & Y & Z).
+  exploit exec_straight_steps_2; eauto using functions_transl.                      
+  intros (ofs' & P & Q).
+  left; econstructor; split.
+  (* execution *)
+  eapply plus_right'. eapply exec_straight_exec; eauto.
+  econstructor. eexact P. eapply functions_transl; eauto. eapply find_instr_tail. eexact Q.
+  simpl. reflexivity.
+  traceEq.
+  (* match states *)
+  econstructor; eauto.
+  apply agree_set_other; auto with asmgen.
+
+- (* internal function *)
+
+  exploit functions_translated; eauto. intros [tf [A B]]. monadInv B.
+  generalize EQ; intros EQ'. monadInv EQ'.
+  destruct (zlt Ptrofs.max_unsigned (list_length_z x0.(fn_code))); inversion EQ1. clear EQ1. subst x0.
+  unfold 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]].
+  change (chunk_of_type Tptr) with Mint64 in *.
+  (* Execution of function prologue *)
+  monadInv EQ0. rewrite transl_code'_transl_code in EQ1.
+  set (tfbody := Pallocframe (fn_stacksize f) (fn_link_ofs f) ::
+                 storeptr RA XSP (fn_retaddr_ofs f) x0) in *.
+  set (tf := {| fn_sig := Mach.fn_sig f; fn_code := tfbody |}) in *.
+  set (rs2 := nextinstr (rs0#X29 <- (parent_sp s) #SP <- sp #X16 <- Vundef)).
+  exploit (storeptr_correct tge tf XSP (fn_retaddr_ofs f) RA x0 m2' m3' rs2).
+    simpl preg_of_iregsp. change (rs2 X30) with (rs0 X30). rewrite ATLR. 
+    change (rs2 X2) with sp. eexact P. 
+    simpl; congruence. congruence.
+  intros (rs3 & U & V & W).
+  assert (EXEC_PROLOGUE:
+            exec_straight tge tf
+              tf.(fn_code) rs0 m'
+              x0 rs3 m3').
+  { change (fn_code tf) with tfbody; unfold tfbody.
+    apply exec_straight_step with rs2 m2'.
+    unfold exec_instr. rewrite C. fold sp.
+    rewrite <- (sp_val _ _ _ AG). rewrite F. reflexivity.
+    reflexivity. 
+    eexact U. }
+  exploit exec_straight_steps_2; eauto using functions_transl. omega. constructor.
+  intros (ofs' & X & Y).                    
+  left; exists (State rs3 m3'); split.
+  eapply exec_straight_steps_1; eauto. omega. constructor.
+  econstructor; eauto.
+  rewrite X; econstructor; eauto. 
+  apply agree_exten with rs2; eauto with asmgen.
+  unfold rs2. 
+  apply agree_nextinstr. 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.
+  simpl; intros; Simpl.
+  unfold sp; congruence.
+  intros. rewrite V by auto with asmgen. reflexivity.
+
+  rewrite W.
+  unfold rs2.
+  Simpl.
+  
+- (* external function *)
+  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 STACKS. simpl in *.
+  right. split. omega. split. auto.
+  rewrite <- ATPC in H5.
+  econstructor; eauto. congruence.
+  inv WF.
+  inv STACK.
+  inv H1.
+  congruence.
+Qed.
+
+Lemma transf_initial_states:
+  forall st1, Mach.initial_state prog st1 ->
+  exists st2, Asm.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 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 -> Mach.final_state st1 r -> Asm.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.
+
+Theorem transf_program_correct:
+  forward_simulation (Mach.semantics return_address_offset prog) (Asm.semantics tprog).
+Proof.
+  eapply forward_simulation_star with (measure := measure)
+         (match_states := fun S1 S2 => match_states S1 S2 /\ wf_state ge S1).
+  - apply senv_preserved.
+  - simpl; intros. exploit transf_initial_states; eauto.
+    intros (s2 & A & B).
+    exists s2; intuition auto. apply wf_initial; auto.
+  - simpl; intros. destruct H as [MS WF]. eapply transf_final_states; eauto.
+  - simpl; intros. destruct H0 as [MS WF]. 
+    exploit step_simulation; eauto. intros [ (s2' & A & B) | (A & B & C) ].
+    + left; exists s2'; intuition auto. eapply wf_step; eauto. 
+    + right; intuition auto. eapply wf_step; eauto.
+Qed.
+
+End PRESERVATION.
+*)
\ No newline at end of file
diff --git a/aarch64/Asmgenproof1.v b/aarch64/Asmblockgenproof1.v
index 0e36bd05..b42309bc 100644
--- a/aarch64/Asmgenproof1.v
+++ b/aarch64/Asmblockgenproof1.v
@@ -1,3 +1,5 @@
+(* ORIGINAL aarch64/Asmgenproof1 file that needs to be adapted
+
 (* *********************************************************************)
 (*                                                                     *)
 (*              The Compcert verified compiler                         *)
@@ -2136,3 +2138,4 @@ Proof.
 Qed.
 
 End CONSTRUCTORS.
+*)
\ No newline at end of file
diff --git a/aarch64/Asmgen.v b/aarch64/Asmgen.v
index 024c9a17..f81f37d6 100644
--- a/aarch64/Asmgen.v
+++ b/aarch64/Asmgen.v
@@ -1,1172 +1,33 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              The Compcert verified compiler                         *)
-(*                                                                     *)
-(*         Xavier Leroy, Collège de France and INRIA Paris             *)
-(*                                                                     *)
-(*  Copyright Institut National de Recherche en Informatique et en     *)
-(*  Automatique.  All rights reserved.  This file is distributed       *)
-(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-(** Translation from Mach to AArch64. *)
+(* *************************************************************)
+(*                                                             *)
+(*             The Compcert verified compiler                  *)
+(*                                                             *)
+(*           Sylvain Boulmé     Grenoble-INP, VERIMAG          *)
+(*           Justus Fasse       UGA, VERIMAG                   *)
+(*           Xavier Leroy       INRIA Paris-Rocquencourt       *)
+(*           David Monniaux     CNRS, VERIMAG                  *)
+(*           Cyril Six          Kalray                         *)
+(*                                                             *)
+(*  Copyright Kalray. Copyright VERIMAG. All rights reserved.  *)
+(*  This file is distributed under the terms of the INRIA      *)
+(*  Non-Commercial License Agreement.                          *)
+(*                                                             *)
+(* *************************************************************)
 
 Require Import Recdef Coqlib Zwf Zbits.
 Require Import Errors AST Integers Floats Op.
-Require Import Locations Mach Asm.
-
-Local Open Scope string_scope.
-Local Open Scope list_scope.
-Local Open Scope error_monad_scope.
-
-(** Alignment check for symbols *)
-
-Parameter symbol_is_aligned : ident -> Z -> bool.
-(** [symbol_is_aligned id sz] checks whether the symbol [id] is [sz] aligned *)
-
-(** Extracting integer or float registers. *)
-
-Definition ireg_of (r: mreg) : res ireg :=
-  match preg_of r with IR mr => OK mr | _ => Error(msg "Asmgen.ireg_of") end.
-
-Definition freg_of (r: mreg) : res freg :=
-  match preg_of r with FR mr => OK mr | _ => Error(msg "Asmgen.freg_of") end.
-
-(** Recognition of immediate arguments for logical integer operations.*)
-
-(** Valid immediate arguments are repetitions of a bit pattern [B]
-  of length [e] = 2, 4, 8, 16, 32 or 64.
-  The bit pattern [B] must be of the form [0*1*0*] or [1*0*1*]
-  but must not be all zeros or all ones. *)
-
-(** The following automaton recognizes [0*1*0*|1*0*1*].
-<<
-               0          1          0
-              / \        / \        / \
-              \ /        \ /        \ /
-        -0--> [B] --1--> [D] --0--> [F]
-       /
-     [A]
-       \
-        -1--> [C] --0--> [E] --1--> [G]
-              / \        / \        / \
-              \ /        \ /        \ /
-               1          0          1
->>
-*)
-
-Module Automaton.
-
-Inductive state : Type := SA | SB | SC | SD | SE | SF | SG | Sbad.
-
-Definition start := SA.
-
-Definition next (s: state) (b: bool) :=
-  match s, b with
-    | SA,false => SB      | SA,true => SC
-    | SB,false => SB      | SB,true => SD
-    | SC,false => SE      | SC,true => SC
-    | SD,false => SF      | SD,true => SD
-    | SE,false => SE      | SE,true => SG
-    | SF,false => SF      | SF,true => Sbad
-    | SG,false => Sbad    | SG,true => SG
-    | Sbad,_ => Sbad
-  end.
-
-Definition accepting (s: state) :=
-  match s with
-  | SA | SB | SC | SD | SE | SF | SG => true
-  | Sbad => false
-  end.
-
-Fixpoint run (len: nat) (s: state) (x: Z) : bool :=
-  match len with
-  | Datatypes.O => accepting s
-  | Datatypes.S len => run len (next s (Z.odd x)) (Z.div2 x)
-  end.
-
-End Automaton.
-
-(** The following function determines the candidate length [e],
-    ensuring that [x] is a repetition [BB...B] 
-    of a bit pattern [B] of length [e]. *)
-
-Definition logical_imm_length (x: Z) (sixtyfour: bool) : nat :=
-  (** [test n] checks that the low [2n] bits of [x] are of the
-      form [BB], that is, two occurrences of the same [n] bits *)
-  let test (n: Z) : bool :=
-    Z.eqb (Zzero_ext n x) (Zzero_ext n (Z.shiftr x n)) in
-  (** If [test n] fails, we know that the candidate length [e] is
-      at least [2n].  Hence we test with decreasing values of [n]:
-      32, 16, 8, 4, 2. *)
-  if sixtyfour && negb (test 32) then 64%nat
-  else if negb (test 16) then 32%nat
-  else if negb (test 8) then 16%nat
-  else if negb (test 4) then 8%nat
-  else if negb (test 2) then 4%nat
-  else 2%nat.
-
-(** A valid logical immediate is 
-- neither [0] nor [-1];
-- composed of a repetition [BBBBB] of a bit-pattern [B] of length [e]
-- the low [e] bits of the number, that is, [B], match [0*1*0*] or [1*0*1*].
-*)
-
-Definition is_logical_imm32 (x: int) : bool :=
-  negb (Int.eq x Int.zero) && negb (Int.eq x Int.mone) &&
-  Automaton.run (logical_imm_length (Int.unsigned x) false)
-                Automaton.start (Int.unsigned x).
-
-Definition is_logical_imm64 (x: int64) : bool :=
-  negb (Int64.eq x Int64.zero) && negb (Int64.eq x Int64.mone) &&
-  Automaton.run (logical_imm_length (Int64.unsigned x) true)
-                Automaton.start (Int64.unsigned x).
-
-(** Arithmetic immediates are 12-bit unsigned numbers, possibly shifted left 12 bits *)
-
-Definition is_arith_imm32 (x: int) : bool :=
-  Int.eq x (Int.zero_ext 12 x)
-  || Int.eq x (Int.shl (Int.zero_ext 12 (Int.shru x (Int.repr 12))) (Int.repr 12)).
-
-Definition is_arith_imm64 (x: int64) : bool :=
-  Int64.eq x (Int64.zero_ext 12 x)
-  || Int64.eq x (Int64.shl (Int64.zero_ext 12 (Int64.shru x (Int64.repr 12))) (Int64.repr 12)).
-
-(** Decompose integer literals into 16-bit fragments *)
-
-Fixpoint decompose_int (N: nat) (n p: Z) {struct N} : list (Z * Z) :=
-  match N with
-  | Datatypes.O => nil
-  | Datatypes.S N =>
-    let frag := Zzero_ext 16 (Z.shiftr n p) in
-    if Z.eqb frag 0 then
-      decompose_int N n (p + 16)
-    else
-      (frag, p) :: decompose_int N (Z.ldiff n (Z.shiftl 65535 p)) (p + 16)
-  end.
-
-Definition negate_decomposition (l: list (Z * Z)) :=
-  List.map (fun np => (Z.lxor (fst np) 65535, snd np)) l.
-
-Definition loadimm_k (sz: isize) (rd: ireg) (l: list (Z * Z)) (k: code) : code :=
-  List.fold_right (fun np k => Pmovk sz rd (fst np) (snd np) :: k) k l.
-
-Definition loadimm_z (sz: isize) (rd: ireg) (l: list (Z * Z)) (k: code) : code :=
-  match l with
-  | nil => Pmovz sz rd 0 0 :: k
-  | (n1, p1) :: l => Pmovz sz rd n1 p1 :: loadimm_k sz rd l k
-  end.
-
-Definition loadimm_n (sz: isize) (rd: ireg) (l: list (Z * Z)) (k: code) : code :=
-  match l with
-  | nil => Pmovn sz rd 0 0 :: k
-  | (n1, p1) :: l => Pmovn sz rd n1 p1 :: loadimm_k sz rd (negate_decomposition l) k
-  end.
-
-Definition loadimm (sz: isize) (rd: ireg) (n: Z) (k: code) : code :=
-  let N := match sz with W => 2%nat | X => 4%nat end in
-  let dz := decompose_int N n 0 in
-  let dn := decompose_int N (Z.lnot n) 0 in
-  if Nat.leb (List.length dz) (List.length dn)
-  then loadimm_z sz rd dz k
-  else loadimm_n sz rd dn k.
-
-Definition loadimm32 (rd: ireg) (n: int) (k: code) : code :=
-  if is_logical_imm32 n
-  then Porrimm W rd XZR (Int.unsigned n) :: k
-  else loadimm W rd (Int.unsigned n) k.
-
-Definition loadimm64 (rd: ireg) (n: int64) (k: code) : code :=
-  if is_logical_imm64 n
-  then Porrimm X rd XZR (Int64.unsigned n) :: k
-  else loadimm X rd (Int64.unsigned n) k.
-
-(** Add immediate *)
-
-Definition addimm_aux (insn: iregsp -> iregsp -> Z -> instruction)
-                        (rd r1: iregsp) (n: Z) (k: code) :=
-  let nlo := Zzero_ext 12 n in
-  let nhi := n - nlo in
-  if Z.eqb nhi 0 then
-    insn rd r1 nlo :: k
-  else if Z.eqb nlo 0 then
-    insn rd r1 nhi :: k
-  else
-    insn rd r1 nhi :: insn rd rd nlo :: k.
-
-Definition addimm32 (rd r1: ireg) (n: int) (k: code) : code :=
-  let m := Int.neg n in
-  if Int.eq n (Int.zero_ext 24 n) then
-    addimm_aux (Paddimm W) rd r1 (Int.unsigned n) k
-  else if Int.eq m (Int.zero_ext 24 m) then
-    addimm_aux (Psubimm W) rd r1 (Int.unsigned m) k
-  else if Int.lt n Int.zero then
-    loadimm32 X16 m (Psub W rd r1 X16 SOnone :: k)
-  else
-    loadimm32 X16 n (Padd W rd r1 X16 SOnone :: k).
-
-Definition addimm64 (rd r1: iregsp) (n: int64) (k: code) : code :=
-  let m := Int64.neg n in
-  if Int64.eq n (Int64.zero_ext 24 n) then
-    addimm_aux (Paddimm X) rd r1 (Int64.unsigned n) k
-  else if Int64.eq m (Int64.zero_ext 24 m) then
-    addimm_aux (Psubimm X) rd r1 (Int64.unsigned m) k
-  else if Int64.lt n Int64.zero then
-    loadimm64 X16 m (Psubext rd r1 X16 (EOuxtx Int.zero) :: k)
-  else
-    loadimm64 X16 n (Paddext rd r1 X16 (EOuxtx Int.zero) :: k).
-
-(** Logical immediate *)
-
-Definition logicalimm32
-              (insn1: ireg -> ireg0 -> Z -> instruction)
-              (insn2: ireg -> ireg0 -> ireg -> shift_op -> instruction)
-              (rd r1: ireg) (n: int) (k: code) : code :=
-  if is_logical_imm32 n
-  then insn1 rd r1 (Int.unsigned n) :: k
-  else loadimm32 X16 n (insn2 rd r1 X16 SOnone :: k).
-
-Definition logicalimm64
-              (insn1: ireg -> ireg0 -> Z -> instruction)
-              (insn2: ireg -> ireg0 -> ireg -> shift_op -> instruction)
-              (rd r1: ireg) (n: int64) (k: code) : code :=
-  if is_logical_imm64 n
-  then insn1 rd r1 (Int64.unsigned n) :: k
-  else loadimm64 X16 n (insn2 rd r1 X16 SOnone :: k).
-
-(** Sign- or zero-extended arithmetic *)
-
-Definition transl_extension (ex: extension) (a: int) : extend_op :=
-  match ex with Xsgn32 => EOsxtw a | Xuns32 => EOuxtw a end.
-
-Definition move_extended_base
-              (rd: ireg) (r1: ireg) (ex: extension) (k: code) : code :=
-  match ex with
-  | Xsgn32 => Pcvtsw2x rd r1 :: k
-  | Xuns32 => Pcvtuw2x rd r1 :: k
-  end.
-
-Definition move_extended
-              (rd: ireg) (r1: ireg) (ex: extension) (a: int) (k: code) : code :=
-  if Int.eq a Int.zero then
-    move_extended_base rd r1 ex k
-  else
-    move_extended_base rd r1 ex (Padd X rd XZR rd (SOlsl a) :: k).
-
-Definition arith_extended 
-              (insnX: iregsp -> iregsp -> ireg -> extend_op -> instruction)
-              (insnS: ireg -> ireg0 -> ireg -> shift_op -> instruction)
-              (rd r1 r2: ireg) (ex: extension) (a: int) (k: code) : code :=
-  if Int.ltu a (Int.repr 5) then
-    insnX rd r1 r2 (transl_extension ex a) :: k
-  else
-    move_extended_base X16 r2 ex (insnS rd r1 X16 (SOlsl a) :: k).
-
-(** Extended right shift *)
-
-Definition shrx32 (rd r1: ireg) (n: int) (k: code) : code :=
-  if Int.eq n Int.zero then
-    Pmov rd r1 :: k
-  else if Int.eq n Int.one then
-         Padd W X16 r1 r1 (SOlsr (Int.repr 31)) ::
-         Porr W rd XZR X16 (SOasr n) :: k
-       else
-         Porr W X16 XZR r1 (SOasr (Int.repr 31)) ::
-         Padd W X16 r1 X16 (SOlsr (Int.sub Int.iwordsize n)) ::
-         Porr W rd XZR X16 (SOasr n) :: k.
-
-Definition shrx64 (rd r1: ireg) (n: int) (k: code) : code :=
-  if Int.eq n Int.zero then
-    Pmov rd r1 :: k
-  else if Int.eq n Int.one then
-         Padd X X16 r1 r1 (SOlsr (Int.repr 63)) ::
-         Porr X rd XZR X16 (SOasr n) :: k
-       else
-         Porr X X16 XZR r1 (SOasr (Int.repr 63)) ::
-         Padd X X16 r1 X16 (SOlsr (Int.sub Int64.iwordsize' n)) ::
-         Porr X rd XZR X16 (SOasr n) :: k.
-
-(** Load the address [id + ofs] in [rd] *)
-
-Definition loadsymbol (rd: ireg) (id: ident) (ofs: ptrofs) (k: code) : code :=
-  if Archi.pic_code tt then
-    if Ptrofs.eq ofs Ptrofs.zero then
-      Ploadsymbol rd id :: k
-    else
-      Ploadsymbol rd id :: addimm64 rd rd (Ptrofs.to_int64 ofs) k
-  else
-    Padrp rd id ofs :: Paddadr rd rd id ofs :: k.
-
-(** Translate a shifted operand *)
-
-Definition transl_shift (s: Op.shift) (a: int): Asm.shift_op :=
-  match s with
-  | Slsl => SOlsl a
-  | Slsr => SOlsr a
-  | Sasr => SOasr a
-  | Sror => SOror a
-  end.
-
-(** Translation of a condition.  Prepends to [k] the instructions
-  that evaluate the condition and leave its boolean result in one of
-  the bits of the condition register.  The bit in question is
-  determined by the [crbit_for_cond] function. *)
-
-Definition transl_cond
-              (cond: condition) (args: list mreg) (k: code) :=
-  match cond, args with
-  | (Ccomp c | Ccompu c), a1 :: a2 :: nil =>
-      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (Pcmp W r1 r2 SOnone :: k)
-  | (Ccompshift c s a | Ccompushift c s a), a1 :: a2 :: nil =>
-      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (Pcmp W r1 r2 (transl_shift s a) :: k)
-  | (Ccompimm c n | Ccompuimm c n), a1 :: nil =>
-      do r1 <- ireg_of a1;
-      OK (if is_arith_imm32 n then
-            Pcmpimm W r1 (Int.unsigned n) :: k
-          else if is_arith_imm32 (Int.neg n) then
-            Pcmnimm W r1 (Int.unsigned (Int.neg n)) :: k
-          else
-            loadimm32 X16 n (Pcmp W r1 X16 SOnone :: k))
-  | (Cmaskzero n | Cmasknotzero n), a1 :: nil =>
-      do r1 <- ireg_of a1;
-      OK (if is_logical_imm32 n then
-            Ptstimm W r1 (Int.unsigned n) :: k
-          else
-            loadimm32 X16 n (Ptst W r1 X16 SOnone :: k))
-  | (Ccompl c | Ccomplu c), a1 :: a2 :: nil =>
-      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (Pcmp X r1 r2 SOnone :: k)
-  | (Ccomplshift c s a | Ccomplushift c s a), a1 :: a2 :: nil =>
-      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (Pcmp X r1 r2 (transl_shift s a) :: k)
-  | (Ccomplimm c n | Ccompluimm c n), a1 :: nil =>
-      do r1 <- ireg_of a1;
-      OK (if is_arith_imm64 n then
-            Pcmpimm X r1 (Int64.unsigned n) :: k
-          else if is_arith_imm64 (Int64.neg n) then
-            Pcmnimm X r1 (Int64.unsigned (Int64.neg n)) :: k
-          else
-            loadimm64 X16 n (Pcmp X r1 X16 SOnone :: k))
-  | (Cmasklzero n | Cmasklnotzero n), a1 :: nil =>
-      do r1 <- ireg_of a1;
-      OK (if is_logical_imm64 n then
-            Ptstimm X r1 (Int64.unsigned n) :: k
-          else
-            loadimm64 X16 n (Ptst X r1 X16 SOnone :: k))
-  | Ccompf cmp, a1 :: a2 :: nil =>
-      do r1 <- freg_of a1; do r2 <- freg_of a2;
-      OK (Pfcmp D r1 r2 :: k)
-  | Cnotcompf cmp, a1 :: a2 :: nil =>
-      do r1 <- freg_of a1; do r2 <- freg_of a2;
-      OK (Pfcmp D r1 r2 :: k)
-  | Ccompfzero cmp, a1 :: nil =>
-      do r1 <- freg_of a1;
-      OK (Pfcmp0 D r1 :: k)
-  | Cnotcompfzero cmp, a1 :: nil =>
-      do r1 <- freg_of a1;
-      OK (Pfcmp0 D r1 :: k)
-  | Ccompfs cmp, a1 :: a2 :: nil =>
-      do r1 <- freg_of a1; do r2 <- freg_of a2;
-      OK (Pfcmp S r1 r2 :: k)
-  | Cnotcompfs cmp, a1 :: a2 :: nil =>
-      do r1 <- freg_of a1; do r2 <- freg_of a2;
-      OK (Pfcmp S r1 r2 :: k)
-  | Ccompfszero cmp, a1 :: nil =>
-      do r1 <- freg_of a1;
-      OK (Pfcmp0 S r1 :: k)
-  | Cnotcompfszero cmp, a1 :: nil =>
-      do r1 <- freg_of a1;
-      OK (Pfcmp0 S r1 :: k)
-  | _, _ =>
-      Error(msg "Asmgen.transl_cond")
-  end.
-
-Definition cond_for_signed_cmp (cmp: comparison) :=
-  match cmp with
-  | Ceq => TCeq
-  | Cne => TCne
-  | Clt => TClt
-  | Cle => TCle
-  | Cgt => TCgt
-  | Cge => TCge
-  end.
-
-Definition cond_for_unsigned_cmp (cmp: comparison) :=
-  match cmp with
-  | Ceq => TCeq
-  | Cne => TCne
-  | Clt => TClo
-  | Cle => TCls
-  | Cgt => TChi
-  | Cge => TChs
-  end.
-
-Definition cond_for_float_cmp (cmp: comparison) :=
-  match cmp with
-  | Ceq => TCeq
-  | Cne => TCne
-  | Clt => TCmi
-  | Cle => TCls
-  | Cgt => TCgt
-  | Cge => TCge
-  end.
-
-Definition cond_for_float_not_cmp (cmp: comparison) :=
-  match cmp with
-  | Ceq => TCne
-  | Cne => TCeq
-  | Clt => TCpl
-  | Cle => TChi
-  | Cgt => TCle
-  | Cge => TClt
-  end.
-
-Definition cond_for_cond (cond: condition) :=
-  match cond with
-  | Ccomp cmp => cond_for_signed_cmp cmp
-  | Ccompu cmp => cond_for_unsigned_cmp cmp
-  | Ccompshift cmp s a => cond_for_signed_cmp cmp
-  | Ccompushift cmp s a => cond_for_unsigned_cmp cmp
-  | Ccompimm cmp n => cond_for_signed_cmp cmp
-  | Ccompuimm cmp n => cond_for_unsigned_cmp cmp
-  | Cmaskzero n => TCeq
-  | Cmasknotzero n => TCne
-  | Ccompl cmp => cond_for_signed_cmp cmp
-  | Ccomplu cmp => cond_for_unsigned_cmp cmp
-  | Ccomplshift cmp s a => cond_for_signed_cmp cmp
-  | Ccomplushift cmp s a => cond_for_unsigned_cmp cmp
-  | Ccomplimm cmp n => cond_for_signed_cmp cmp
-  | Ccompluimm cmp n => cond_for_unsigned_cmp cmp
-  | Cmasklzero n => TCeq
-  | Cmasklnotzero n => TCne
-  | Ccompf cmp => cond_for_float_cmp cmp
-  | Cnotcompf cmp => cond_for_float_not_cmp cmp
-  | Ccompfzero cmp => cond_for_float_cmp cmp
-  | Cnotcompfzero cmp => cond_for_float_not_cmp cmp
-  | Ccompfs cmp => cond_for_float_cmp cmp
-  | Cnotcompfs cmp => cond_for_float_not_cmp cmp
-  | Ccompfszero cmp => cond_for_float_cmp cmp
-  | Cnotcompfszero cmp => cond_for_float_not_cmp cmp
-  end.
-
-(** Translation of a conditional branch.  Prepends to [k] the instructions
-  that evaluate the condition and ranch to [lbl] if it holds.
-  We recognize some conditional branches that can be implemented
-  without setting then testing condition flags.  *)
-
-Definition transl_cond_branch_default
-              (c: condition) (args: list mreg) (lbl: label) (k: code) :=
-  transl_cond c args (Pbc (cond_for_cond c) lbl :: k).
- 
-Definition transl_cond_branch
-              (c: condition) (args: list mreg) (lbl: label) (k: code) :=
-  match args, c with
-  | a1 :: nil, (Ccompimm Cne n | Ccompuimm Cne n) =>
-      if Int.eq n Int.zero
-      then (do r1 <- ireg_of a1; OK (Pcbnz W r1 lbl :: k))
-      else transl_cond_branch_default c args lbl k
-  | a1 :: nil, (Ccompimm Ceq n | Ccompuimm Ceq n) =>
-      if Int.eq n Int.zero
-      then (do r1 <- ireg_of a1; OK (Pcbz W r1 lbl :: k))
-      else transl_cond_branch_default c args lbl k
-  | a1 :: nil, (Ccomplimm Cne n | Ccompluimm Cne n) =>
-      if Int64.eq n Int64.zero
-      then (do r1 <- ireg_of a1; OK (Pcbnz X r1 lbl :: k))
-      else transl_cond_branch_default c args lbl k
-  | a1 :: nil, (Ccomplimm Ceq n | Ccompluimm Ceq n) =>
-      if Int64.eq n Int64.zero
-      then (do r1 <- ireg_of a1; OK (Pcbz X r1 lbl :: k))
-      else transl_cond_branch_default c args lbl k
-  | a1 :: nil, Cmaskzero n =>
-      match Int.is_power2 n with
-      | Some bit => do r1 <- ireg_of a1; OK (Ptbz W r1 bit lbl :: k)
-      | None => transl_cond_branch_default c args lbl k
-      end
-  | a1 :: nil, Cmasknotzero n =>
-      match Int.is_power2 n with
-      | Some bit => do r1 <- ireg_of a1; OK (Ptbnz W r1 bit lbl :: k)
-      | None => transl_cond_branch_default c args lbl k
-      end
-  | a1 :: nil, Cmasklzero n =>
-      match Int64.is_power2' n with
-      | Some bit => do r1 <- ireg_of a1; OK (Ptbz X r1 bit lbl :: k)
-      | None => transl_cond_branch_default c args lbl k
-      end
-  | a1 :: nil, Cmasklnotzero n =>
-      match Int64.is_power2' n with
-      | Some bit => do r1 <- ireg_of a1; OK (Ptbnz X r1 bit lbl :: k)
-      | None => transl_cond_branch_default c args lbl k
-      end
-  | _, _ =>
-      transl_cond_branch_default c args lbl k
-  end.
-  
-(** Translation of the arithmetic operation [res <- op(args)].
-    The corresponding instructions are prepended to [k]. *)
-
-Definition transl_op
-              (op: operation) (args: list mreg) (res: mreg) (k: code) :=
-  match op, args with
-  | Omove, a1 :: nil =>
-      match preg_of res, preg_of a1 with
-      | IR r, IR a => OK (Pmov r a :: k)
-      | FR r, FR a => OK (Pfmov r a :: k)
-      |  _  ,  _   => Error(msg "Asmgen.Omove")
-      end
-  | Ointconst n, nil =>
-      do rd <- ireg_of res;
-      OK (loadimm32 rd n k)
-  | Olongconst n, nil =>
-      do rd <- ireg_of res;
-      OK (loadimm64 rd n k)
-  | Ofloatconst f, nil =>
-      do rd <- freg_of res;
-      OK (if Float.eq_dec f Float.zero
-          then Pfmovi D rd XZR :: k
-          else Pfmovimmd rd f :: k)
-  | Osingleconst f, nil =>
-      do rd <- freg_of res;
-      OK (if Float32.eq_dec f Float32.zero
-          then Pfmovi S rd XZR :: k
-          else Pfmovimms rd f :: k)
-  | Oaddrsymbol id ofs, nil =>
-      do rd <- ireg_of res;
-      OK (loadsymbol rd id ofs k)
-  | Oaddrstack ofs, nil =>
-      do rd <- ireg_of res;
-      OK (addimm64 rd XSP (Ptrofs.to_int64 ofs) k)
-(** 32-bit integer arithmetic *)
-  | Oshift s a, a1 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1;
-      OK (Porr W rd XZR r1 (transl_shift s a) :: k)
-  | Oadd, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (Padd W rd r1 r2 SOnone :: k)
-  | Oaddshift s a, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (Padd W rd r1 r2 (transl_shift s a) :: k)
-  | Oaddimm n, a1 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1;
-      OK (addimm32 rd r1 n k)
-  | Oneg, a1 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1;
-      OK (Psub W rd XZR r1 SOnone :: k)
-  | Onegshift s a, a1 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1;
-      OK (Psub W rd XZR r1 (transl_shift s a) :: k)
-  | Osub, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (Psub W rd r1 r2 SOnone :: k)
-  | Osubshift s a, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (Psub W rd r1 r2 (transl_shift s a) :: k)
-  | Omul, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (Pmadd W rd r1 r2 XZR :: k)
-  | Omuladd, a1 :: a2 :: a3 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r3 <- ireg_of a3;
-      OK (Pmadd W rd r2 r3 r1 :: k)
-  | Omulsub, a1 :: a2 :: a3 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r3 <- ireg_of a3;
-      OK (Pmsub W rd r2 r3 r1 :: k)
-  | Odiv, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (Psdiv W rd r1 r2 :: k)
-  | Odivu, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (Pudiv W rd r1 r2 :: k)
-  | Oand, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (Pand W rd r1 r2 SOnone :: k)
-  | Oandshift s a, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (Pand W rd r1 r2 (transl_shift s a) :: k)
-  | Oandimm n, a1 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1;
-      OK (logicalimm32 (Pandimm W) (Pand W) rd r1 n k)      
-  | Oor, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (Porr W rd r1 r2 SOnone :: k)
-  | Oorshift s a, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (Porr W rd r1 r2 (transl_shift s a) :: k)
-  | Oorimm n, a1 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1;
-      OK (logicalimm32 (Porrimm W) (Porr W) rd r1 n k)      
-  | Oxor, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (Peor W rd r1 r2 SOnone :: k)
-  | Oxorshift s a, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (Peor W rd r1 r2 (transl_shift s a) :: k)
-  | Oxorimm n, a1 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1;
-      OK (logicalimm32 (Peorimm W) (Peor W) rd r1 n k)      
-  | Onot, a1 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1;
-      OK (Porn W rd XZR r1 SOnone :: k)
-  | Onotshift s a, a1 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1;
-      OK (Porn W rd XZR r1 (transl_shift s a) :: k)
-  | Obic, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (Pbic W rd r1 r2 SOnone :: k)
-  | Obicshift s a, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (Pbic W rd r1 r2 (transl_shift s a) :: k)
-  | Oorn, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (Porn W rd r1 r2 SOnone :: k)
-  | Oornshift s a, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (Porn W rd r1 r2 (transl_shift s a) :: k)
-  | Oeqv, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (Peon W rd r1 r2 SOnone :: k)
-  | Oeqvshift s a, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (Peon W rd r1 r2 (transl_shift s a) :: k)
-  | Oshl, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (Plslv W rd r1 r2 :: k)
-  | Oshr, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (Pasrv W rd r1 r2 :: k)
-  | Oshru, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (Plsrv W rd r1 r2 :: k)
-  | Oshrximm n, a1 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1;
-      OK (shrx32 rd r1 n k)
-  | Ozext s, a1 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1;
-      OK (Pubfiz W rd r1 Int.zero s :: k)
-  | Osext s, a1 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1;
-      OK (Psbfiz W rd r1 Int.zero s :: k)
-  | Oshlzext s a, a1 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1;
-      OK (Pubfiz W rd r1 a (Z.min s (Int.zwordsize - Int.unsigned a)) :: k)
-  | Oshlsext s a, a1 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1;
-      OK (Psbfiz W rd r1 a (Z.min s (Int.zwordsize - Int.unsigned a)) :: k)
-  | Ozextshr a s, a1 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1;
-      OK (Pubfx W rd r1 a (Z.min s (Int.zwordsize - Int.unsigned a)) :: k)
-  | Osextshr a s, a1 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1;
-      OK (Psbfx W rd r1 a (Z.min s (Int.zwordsize - Int.unsigned a)) :: k)
-(** 64-bit integer arithmetic *)
-  | Oshiftl s a, a1 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1;
-      OK (Porr X rd XZR r1 (transl_shift s a) :: k)
-  | Oextend x a, a1 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1;
-      OK (move_extended rd r1 x a k)
-  (* [Omakelong] and [Ohighlong] should not occur *)
-  | Olowlong, a1 :: nil => 
-      do rd <- ireg_of res; do r1 <- ireg_of a1;
-      assertion (ireg_eq rd r1);
-      OK (Pcvtx2w rd :: k)
-  | Oaddl, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (Padd X rd r1 r2 SOnone :: k)
-  | Oaddlshift s a, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (Padd X rd r1 r2 (transl_shift s a) :: k)
-  | Oaddlext x a, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (arith_extended Paddext (Padd X) rd r1 r2 x a k)
-  | Oaddlimm n, a1 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1;
-      OK (addimm64 rd r1 n k)
-  | Onegl, a1 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1;
-      OK (Psub X rd XZR r1 SOnone :: k)
-  | Oneglshift s a, a1 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1;
-      OK (Psub X rd XZR r1 (transl_shift s a) :: k)
-  | Osubl, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (Psub X rd r1 r2 SOnone :: k)
-  | Osublshift s a, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (Psub X rd r1 r2 (transl_shift s a) :: k)
-  | Osublext x a, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (arith_extended Psubext (Psub X) rd r1 r2 x a k)
-  | Omull, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (Pmadd X rd r1 r2 XZR :: k)
-  | Omulladd, a1 :: a2 :: a3 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r3 <- ireg_of a3;
-      OK (Pmadd X rd r2 r3 r1 :: k)
-  | Omullsub, a1 :: a2 :: a3 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r3 <- ireg_of a3;
-      OK (Pmsub X rd r2 r3 r1 :: k)
-  | Omullhs, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (Psmulh rd r1 r2 :: k)
-  | Omullhu, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (Pumulh rd r1 r2 :: k)
-  | Odivl, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (Psdiv X rd r1 r2 :: k)
-  | Odivlu, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (Pudiv X rd r1 r2 :: k)
-  | Oandl, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (Pand X rd r1 r2 SOnone :: k)
-  | Oandlshift s a, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (Pand X rd r1 r2 (transl_shift s a) :: k)
-  | Oandlimm n, a1 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1;
-      OK (logicalimm64 (Pandimm X) (Pand X) rd r1 n k)      
-  | Oorl, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (Porr X rd r1 r2 SOnone :: k)
-  | Oorlshift s a, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (Porr X rd r1 r2 (transl_shift s a) :: k)
-  | Oorlimm n, a1 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1;
-      OK (logicalimm64 (Porrimm X) (Porr X) rd r1 n k)      
-  | Oxorl, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (Peor X rd r1 r2 SOnone :: k)
-  | Oxorlshift s a, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (Peor X rd r1 r2 (transl_shift s a) :: k)
-  | Oxorlimm n, a1 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1;
-      OK (logicalimm64 (Peorimm X) (Peor X) rd r1 n k)      
-  | Onotl, a1 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1;
-      OK (Porn X rd XZR r1 SOnone :: k)
-  | Onotlshift s a, a1 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1;
-      OK (Porn X rd XZR r1 (transl_shift s a) :: k)
-  | Obicl, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (Pbic X rd r1 r2 SOnone :: k)
-  | Obiclshift s a, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (Pbic X rd r1 r2 (transl_shift s a) :: k)
-  | Oornl, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (Porn X rd r1 r2 SOnone :: k)
-  | Oornlshift s a, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (Porn X rd r1 r2 (transl_shift s a) :: k)
-  | Oeqvl, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (Peon X rd r1 r2 SOnone :: k)
-  | Oeqvlshift s a, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (Peon X rd r1 r2 (transl_shift s a) :: k)
-  | Oshll, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (Plslv X rd r1 r2 :: k)
-  | Oshrl, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (Pasrv X rd r1 r2 :: k)
-  | Oshrlu, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (Plsrv X rd r1 r2 :: k)
-  | Oshrlximm n, a1 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1;
-      OK (shrx64 rd r1 n k)
-  | Ozextl s, a1 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1;
-      OK (Pubfiz X rd r1 Int.zero s :: k)
-  | Osextl s, a1 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1;
-      OK (Psbfiz X rd r1 Int.zero s :: k)
-  | Oshllzext s a, a1 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1;
-      OK (Pubfiz X rd r1 a (Z.min s (Int64.zwordsize - Int.unsigned a)) :: k)
-  | Oshllsext s a, a1 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1;
-      OK (Psbfiz X rd r1 a (Z.min s (Int64.zwordsize - Int.unsigned a)) :: k)
-  | Ozextshrl a s, a1 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1;
-      OK (Pubfx X rd r1 a (Z.min s (Int64.zwordsize - Int.unsigned a)) :: k)
-  | Osextshrl a s, a1 :: nil =>
-      do rd <- ireg_of res; do r1 <- ireg_of a1;
-      OK (Psbfx X rd r1 a (Z.min s (Int64.zwordsize - Int.unsigned a)) :: k)
-(** 64-bit floating-point arithmetic *)
-  | Onegf, a1 :: nil =>
-      do rd <- freg_of res; do rs <- freg_of a1;
-      OK (Pfneg D rd rs :: k)
-  | Oabsf, a1 :: nil =>
-      do rd <- freg_of res; do rs <- freg_of a1;
-      OK (Pfabs D rd rs :: k)
-  | Oaddf, a1 :: a2 :: nil =>
-      do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
-      OK (Pfadd D rd rs1 rs2 :: k)
-  | Osubf, a1 :: a2 :: nil =>
-      do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
-      OK (Pfsub D rd rs1 rs2 :: k)
-  | Omulf, a1 :: a2 :: nil =>
-      do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
-      OK (Pfmul D rd rs1 rs2 :: k)
-  | Odivf, a1 :: a2 :: nil =>
-      do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
-      OK (Pfdiv D rd rs1 rs2 :: k)
-(** 32-bit floating-point arithmetic *)
-  | Onegfs, a1 :: nil =>
-      do rd <- freg_of res; do rs <- freg_of a1;
-      OK (Pfneg S rd rs :: k)
-  | Oabsfs, a1 :: nil =>
-      do rd <- freg_of res; do rs <- freg_of a1;
-      OK (Pfabs S rd rs :: k)
-  | Oaddfs, a1 :: a2 :: nil =>
-      do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
-      OK (Pfadd S rd rs1 rs2 :: k)
-  | Osubfs, a1 :: a2 :: nil =>
-      do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
-      OK (Pfsub S rd rs1 rs2 :: k)
-  | Omulfs, a1 :: a2 :: nil =>
-      do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
-      OK (Pfmul S rd rs1 rs2 :: k)
-  | Odivfs, a1 :: a2 :: nil =>
-      do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
-      OK (Pfdiv S rd rs1 rs2 :: k)
-  | Osingleoffloat, a1 :: nil =>
-      do rd <- freg_of res; do rs <- freg_of a1;
-      OK (Pfcvtsd rd rs :: k)
-  | Ofloatofsingle, a1 :: nil =>
-      do rd <- freg_of res; do rs <- freg_of a1;
-      OK (Pfcvtds rd rs :: k)
-(** Conversions between int and float *)
-  | Ointoffloat, a1 :: nil =>
-      do rd <- ireg_of res; do rs <- freg_of a1;
-      OK (Pfcvtzs W D rd rs :: k)
-  | Ointuoffloat, a1 :: nil =>
-      do rd <- ireg_of res; do rs <- freg_of a1;
-      OK (Pfcvtzu W D rd rs :: k)
-  | Ofloatofint, a1 :: nil =>
-      do rd <- freg_of res; do rs <- ireg_of a1;
-      OK (Pscvtf D W rd rs :: k)
-  | Ofloatofintu, a1 :: nil =>
-      do rd <- freg_of res; do rs <- ireg_of a1;
-      OK (Pucvtf D W rd rs :: k)
-  | Ointofsingle, a1 :: nil =>
-      do rd <- ireg_of res; do rs <- freg_of a1;
-      OK (Pfcvtzs W S rd rs :: k)
-  | Ointuofsingle, a1 :: nil =>
-      do rd <- ireg_of res; do rs <- freg_of a1;
-      OK (Pfcvtzu W S rd rs :: k)
-  | Osingleofint, a1 :: nil =>
-      do rd <- freg_of res; do rs <- ireg_of a1;
-      OK (Pscvtf S W rd rs :: k)
-  | Osingleofintu, a1 :: nil =>
-      do rd <- freg_of res; do rs <- ireg_of a1;
-      OK (Pucvtf S W rd rs :: k)
-  | Olongoffloat, a1 :: nil =>
-      do rd <- ireg_of res; do rs <- freg_of a1;
-      OK (Pfcvtzs X D rd rs :: k)
-  | Olonguoffloat, a1 :: nil =>
-      do rd <- ireg_of res; do rs <- freg_of a1;
-      OK (Pfcvtzu X D rd rs :: k)
-  | Ofloatoflong, a1 :: nil =>
-      do rd <- freg_of res; do rs <- ireg_of a1;
-      OK (Pscvtf D X rd rs :: k)
-  | Ofloatoflongu, a1 :: nil =>
-      do rd <- freg_of res; do rs <- ireg_of a1;
-      OK (Pucvtf D X rd rs :: k)
-  | Olongofsingle, a1 :: nil =>
-      do rd <- ireg_of res; do rs <- freg_of a1;
-      OK (Pfcvtzs X S rd rs :: k)
-  | Olonguofsingle, a1 :: nil =>
-      do rd <- ireg_of res; do rs <- freg_of a1;
-      OK (Pfcvtzu X S rd rs :: k)
-  | Osingleoflong, a1 :: nil =>
-      do rd <- freg_of res; do rs <- ireg_of a1;
-      OK (Pscvtf S X rd rs :: k)
-  | Osingleoflongu, a1 :: nil =>
-      do rd <- freg_of res; do rs <- ireg_of a1;
-      OK (Pucvtf S X rd rs :: k)
-(** Boolean tests *)
-  | Ocmp c, _ =>
-      do rd <- ireg_of res;
-      transl_cond c args (Pcset rd (cond_for_cond c) :: k)
-(** Conditional move *)
-  | Osel cmp ty, a1 :: a2 :: args =>
-      match preg_of res with
-      | IR r => 
-          do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-          transl_cond cmp args (Pcsel r r1 r2 (cond_for_cond cmp) :: k)
-      | FR r =>
-          do r1 <- freg_of a1; do r2 <- freg_of a2;
-          transl_cond cmp args (Pfsel r r1 r2 (cond_for_cond cmp) :: k)
-      | _ =>
-          Error(msg "Asmgen.Osel")
-      end
-  | _, _ =>
-      Error(msg "Asmgen.transl_op")
-  end.
-
-(** Translation of addressing modes *)
-
-Definition offset_representable (sz: Z) (ofs: int64) : bool :=
-  let isz := Int64.repr sz in
-  (** either unscaled 9-bit signed *)
-  Int64.eq ofs (Int64.sign_ext 9 ofs) ||
-  (** or scaled 12-bit unsigned *)
-  (Int64.eq (Int64.modu ofs isz) Int64.zero
-   && Int64.ltu ofs (Int64.shl isz (Int64.repr 12))).
- 
-Definition transl_addressing (sz: Z) (addr: Op.addressing) (args: list mreg)
-                             (insn: Asm.addressing -> instruction) (k: code) : res code :=
-  match addr, args with
-  | Aindexed ofs, a1 :: nil =>
-      do r1 <- ireg_of a1;
-       if offset_representable sz ofs then
-        OK (insn (ADimm r1 ofs) :: k)
-      else
-        OK (loadimm64 X16 ofs (insn (ADreg r1 X16) :: k))
-  | Aindexed2, a1 :: a2 :: nil =>
-      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (insn (ADreg r1 r2) :: k)
-  | Aindexed2shift a, a1 :: a2 :: nil =>
-      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      if Int.eq a Int.zero then
-        OK (insn (ADreg r1 r2) :: k)
-      else if Int.eq (Int.shl Int.one a) (Int.repr sz) then
-        OK (insn (ADlsl r1 r2 a) :: k)
-      else
-        OK (Padd X X16 r1 r2 (SOlsl a) :: insn (ADimm X16 Int64.zero) :: k)
-  | Aindexed2ext x a, a1 :: a2 :: nil =>
-      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      if Int.eq a Int.zero || Int.eq (Int.shl Int.one a) (Int.repr sz) then
-        OK (insn (match x with Xsgn32 => ADsxt r1 r2 a
-                             | Xuns32 => ADuxt r1 r2 a end) :: k)
-      else
-        OK (arith_extended Paddext (Padd X) X16 r1 r2 x a
-                           (insn (ADimm X16 Int64.zero) :: k))
-  | Aglobal id ofs, nil =>
-      assertion (negb (Archi.pic_code tt));
-      if Ptrofs.eq (Ptrofs.modu ofs (Ptrofs.repr sz)) Ptrofs.zero && symbol_is_aligned id sz
-      then OK (Padrp X16 id ofs :: insn (ADadr X16 id ofs) :: k)
-      else OK (loadsymbol X16 id ofs (insn (ADimm X16 Int64.zero) :: k))
-  | Ainstack ofs, nil =>
-      let ofs := Ptrofs.to_int64 ofs in
-      if offset_representable sz ofs then
-        OK (insn (ADimm XSP ofs) :: k)
-      else
-        OK (loadimm64 X16 ofs (insn (ADreg XSP X16) :: k))
-  | _, _ =>
-      Error(msg "Asmgen.transl_addressing")
-  end.
-
-(** Translation of loads and stores *)
-
-Definition transl_load (trap: trapping_mode)
-                       (chunk: memory_chunk) (addr: Op.addressing)
-                       (args: list mreg) (dst: mreg) (k: code) : res code :=
-  match trap with
-  | NOTRAP => Error (msg "Asmgen.transl_load non-trapping loads unsupported on aarch64")
-  | TRAP =>
-  match chunk with
-  | Mint8unsigned =>
-      do rd <- ireg_of dst; transl_addressing 1 addr args (Pldrb W rd) k
-  | Mint8signed =>
-      do rd <- ireg_of dst; transl_addressing 1 addr args (Pldrsb W rd) k
-  | Mint16unsigned =>
-      do rd <- ireg_of dst; transl_addressing 2 addr args (Pldrh W rd) k
-  | Mint16signed =>
-      do rd <- ireg_of dst; transl_addressing 2 addr args (Pldrsh W rd) k
-  | Mint32 =>
-      do rd <- ireg_of dst; transl_addressing 4 addr args (Pldrw rd) k
-  | Mint64 =>
-      do rd <- ireg_of dst; transl_addressing 8 addr args (Pldrx rd) k
-  | Mfloat32 =>
-      do rd <- freg_of dst; transl_addressing 4 addr args (Pldrs rd) k
-  | Mfloat64 =>
-      do rd <- freg_of dst; transl_addressing 8 addr args (Pldrd rd) k
-  | Many32 =>
-      do rd <- ireg_of dst; transl_addressing 4 addr args (Pldrw_a rd) k
-  | Many64 =>
-      do rd <- ireg_of dst; transl_addressing 8 addr args (Pldrx_a rd) k
-  end
-  end.
-
-Definition transl_store (chunk: memory_chunk) (addr: Op.addressing)
-                        (args: list mreg) (src: mreg) (k: code) : res code :=
-  match chunk with
-  | Mint8unsigned | Mint8signed =>
-      do r1 <- ireg_of src; transl_addressing 1 addr args (Pstrb r1) k
-  | Mint16unsigned | Mint16signed =>
-      do r1 <- ireg_of src; transl_addressing 2 addr args (Pstrh r1) k
-  | Mint32 =>
-      do r1 <- ireg_of src; transl_addressing 4 addr args (Pstrw r1) k
-  | Mint64 =>
-      do r1 <- ireg_of src; transl_addressing 8 addr args (Pstrx r1) k
-  | Mfloat32 =>
-      do r1 <- freg_of src; transl_addressing 4 addr args (Pstrs r1) k
-  | Mfloat64 =>
-      do r1 <- freg_of src; transl_addressing 8 addr args (Pstrd r1) k
-  | Many32 =>
-      do r1 <- ireg_of src; transl_addressing 4 addr args (Pstrw_a r1) k
-  | Many64 =>
-      do r1 <- ireg_of src; transl_addressing 8 addr args (Pstrx_a r1) k
-  end.
-
-(** Register-indexed loads and stores *)
-
-Definition indexed_memory_access (insn: Asm.addressing -> instruction)
-                                 (sz: Z) (base: iregsp) (ofs: ptrofs) (k: code) :=
-  let ofs := Ptrofs.to_int64 ofs in
-  if offset_representable sz ofs
-  then insn (ADimm base ofs) :: k
-  else loadimm64 X16 ofs (insn (ADreg base X16) :: k).
-
-Definition loadind (base: iregsp) (ofs: ptrofs) (ty: typ) (dst: mreg) (k: code) :=
-  match ty, preg_of dst with
-  | Tint,    IR rd => OK (indexed_memory_access (Pldrw rd) 4 base ofs k)
-  | Tlong,   IR rd => OK (indexed_memory_access (Pldrx rd) 8 base ofs k)
-  | Tsingle, FR rd => OK (indexed_memory_access (Pldrs rd) 4 base ofs k)
-  | Tfloat,  FR rd => OK (indexed_memory_access (Pldrd rd) 8 base ofs k)
-  | Tany32,  IR rd => OK (indexed_memory_access (Pldrw_a rd) 4 base ofs k)
-  | Tany64,  IR rd => OK (indexed_memory_access (Pldrx_a rd) 8 base ofs k)
-  | Tany64,  FR rd => OK (indexed_memory_access (Pldrd_a rd) 8 base ofs k)
-  | _, _           => Error (msg "Asmgen.loadind")
-  end.
-
-Definition storeind (src: mreg) (base: iregsp) (ofs: ptrofs) (ty: typ) (k: code) :=
-  match ty, preg_of src with
-  | Tint,    IR rd => OK (indexed_memory_access (Pstrw rd) 4 base ofs k)
-  | Tlong,   IR rd => OK (indexed_memory_access (Pstrx rd) 8 base ofs k)
-  | Tsingle, FR rd => OK (indexed_memory_access (Pstrs rd) 4 base ofs k)
-  | Tfloat,  FR rd => OK (indexed_memory_access (Pstrd rd) 8 base ofs k)
-  | Tany32,  IR rd => OK (indexed_memory_access (Pstrw_a rd) 4 base ofs k)
-  | Tany64,  IR rd => OK (indexed_memory_access (Pstrx_a rd) 8 base ofs k)
-  | Tany64,  FR rd => OK (indexed_memory_access (Pstrd_a rd) 8 base ofs k)
-  | _, _           => Error (msg "Asmgen.storeind")
-  end.
-
-Definition loadptr (base: iregsp) (ofs: ptrofs) (dst: ireg) (k: code) :=
-  indexed_memory_access (Pldrx dst) 8 base ofs k.
-
-Definition storeptr (src: ireg) (base: iregsp) (ofs: ptrofs) (k: code) :=
-  indexed_memory_access (Pstrx src) 8 base ofs k.
-
-(** Function epilogue *)
-
-Definition make_epilogue (f: Mach.function) (k: code) :=
-  (* FIXME
-     Cannot be used because memcpy destroys X30;
-     issue being discussed with X. Leroy *)
-  (* if is_leaf_function f
-  then Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: k
-  else*) loadptr XSP f.(fn_retaddr_ofs) RA
-         (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: k).
-  
-(** Translation of a Mach instruction. *)
-
-Definition transl_instr (f: Mach.function) (i: Mach.instruction)
-                        (r29_is_parent: bool) (k: code) : res code :=
-  match i with
-  | Mgetstack ofs ty dst =>
-      loadind XSP ofs ty dst k
-  | Msetstack src ofs ty =>
-      storeind src XSP ofs ty k
-  | Mgetparam ofs ty dst =>
-      (* load via the frame pointer if it is valid *)
-      do c <- loadind X29 ofs ty dst k;
-      OK (if r29_is_parent then c else loadptr XSP f.(fn_link_ofs) X29 c)
-  | Mop op args res =>
-      transl_op op args res k
-  | Mload trap chunk addr args dst =>
-      transl_load trap chunk addr args dst k
-  | Mstore chunk addr args src =>
-      transl_store chunk addr args src k
-  | Mcall sig (inl r) =>
-      do r1 <- ireg_of r; OK (Pblr r1 sig :: k)
-  | Mcall sig (inr symb) =>
-      OK (Pbl symb sig :: k)
-  | Mtailcall sig (inl r) =>
-      do r1 <- ireg_of r;
-      OK (make_epilogue f (Pbr r1 sig :: k))
-  | Mtailcall sig (inr symb) =>
-      OK (make_epilogue f (Pbs symb sig :: k))
-  | Mbuiltin ef args res =>
-      OK (Pbuiltin ef (List.map (map_builtin_arg preg_of) args) (map_builtin_res preg_of res) :: k)
-  | Mlabel lbl =>
-      OK (Plabel lbl :: k)
-  | Mgoto lbl =>
-      OK (Pb lbl :: k)
-  | Mcond cond args lbl =>
-      transl_cond_branch cond args lbl k
-  | Mjumptable arg tbl =>
-      do r <- ireg_of arg;
-      OK (Pbtbl r tbl :: k)
-  | Mreturn =>
-      OK (make_epilogue f (Pret RA :: k))
-  end.
-
-(** Translation of a code sequence *)
-
-Definition it1_is_parent (before: bool) (i: Mach.instruction) : bool :=
-  match i with
-  | Msetstack src ofs ty => before
-  | Mgetparam ofs ty dst => negb (mreg_eq dst R29)
-  | Mop op args res => before && negb (mreg_eq res R29)
-  | _ => false
-  end.
-
-(** This is the naive definition that we no longer use because it
-  is not tail-recursive.  It is kept as specification. *)
-
-Fixpoint transl_code (f: Mach.function) (il: list Mach.instruction) (it1p: bool) :=
-  match il with
-  | nil => OK nil
-  | i1 :: il' =>
-      do k <- transl_code f il' (it1_is_parent it1p i1);
-      transl_instr f i1 it1p k
-  end.
-
-(** This is an equivalent definition in continuation-passing style
-  that runs in constant stack space. *)
-
-Fixpoint transl_code_rec (f: Mach.function) (il: list Mach.instruction)
-                         (it1p: bool) (k: code -> res code) :=
-  match il with
-  | nil => k nil
-  | i1 :: il' =>
-      transl_code_rec f il' (it1_is_parent it1p i1)
-        (fun c1 => do c2 <- transl_instr f i1 it1p c1; k c2)
-  end.
-
-Definition transl_code' (f: Mach.function) (il: list Mach.instruction) (it1p: bool) :=
-  transl_code_rec f il it1p (fun c => OK c).
+Require Import Locations Asmblock Asm.
 
-(** Translation of a whole function.  Note that we must check
-  that the generated code contains less than [2^32] instructions,
-  otherwise the offset part of the [PC] code pointer could wrap
-  around, leading to incorrect executions. *)
+(** * Translation from Asmblock to assembly language 
+      Inspired from the KVX backend. *)
 
-Definition transl_function (f: Mach.function) :=
-  do c <- transl_code' f f.(Mach.fn_code) true;
-  OK (mkfunction f.(Mach.fn_sig)
-        (Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::
-         storeptr RA XSP f.(fn_retaddr_ofs) c)).
+(* STUB *)
 
-Definition transf_function (f: Mach.function) : res Asm.function :=
-  do tf <- transl_function f;
-  if zlt Ptrofs.max_unsigned (list_length_z tf.(fn_code))
-  then Error (msg "code size exceeded")
-  else OK tf.
+Definition transf_function (f: Asmblock.function) : res Asm.function :=
+  Error (msg "Asmgen not yet implmented").
 
-Definition transf_fundef (f: Mach.fundef) : res Asm.fundef :=
+Definition transf_fundef (f: Asmblock.fundef) : res Asm.fundef :=
   transf_partial_fundef transf_function f.
 
-Definition transf_program (p: Mach.program) : res Asm.program :=
+Definition transf_program (p: Asmblock.program) : res Asm.program :=
   transform_partial_program transf_fundef p.
diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index 6831509f..e69de29b 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -1,1101 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              The Compcert verified compiler                         *)
-(*                                                                     *)
-(*         Xavier Leroy, Collège de France and INRIA Paris             *)
-(*                                                                     *)
-(*  Copyright Institut National de Recherche en Informatique et en     *)
-(*  Automatique.  All rights reserved.  This file is distributed       *)
-(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-(** Correctness proof for AArch64 code generation. *)
-
-Require Import Coqlib Errors.
-Require Import Integers Floats AST Linking.
-Require Import Values Memory Events Globalenvs Smallstep.
-Require Import Op Locations Mach Conventions Asm.
-Require Import Asmgen Asmgenproof0 Asmgenproof1.
-
-Definition match_prog (p: Mach.program) (tp: Asm.program) :=
-  match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp.
-
-Lemma transf_program_match:
-  forall p tp, transf_program p = OK tp -> match_prog p tp.
-Proof.
-  intros. eapply match_transform_partial_program; eauto.
-Qed.
-
-Section PRESERVATION.
-
-Variable prog: Mach.program.
-Variable tprog: Asm.program.
-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).
-
-Lemma functions_transl:
-  forall fb f tf,
-  Genv.find_funct_ptr ge fb = Some (Internal f) ->
-  transf_function f = OK tf ->
-  Genv.find_funct_ptr tge fb = Some (Internal tf).
-Proof.
-  intros. exploit functions_translated; eauto. intros [tf' [A B]].
-  monadInv B. rewrite H0 in EQ; inv EQ; auto.
-Qed.
-
-(** * Properties of control flow *)
-
-Lemma transf_function_no_overflow:
-  forall f tf,
-  transf_function f = OK tf -> list_length_z tf.(fn_code) <= Ptrofs.max_unsigned.
-Proof.
-  intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (list_length_z x.(fn_code))); inv EQ0.
-  omega.
-Qed.
-
-Lemma exec_straight_exec:
-  forall fb f c ep tf tc c' rs m rs' m',
-  transl_code_at_pc ge (rs PC) fb f c ep tf tc ->
-  exec_straight tge tf tc rs m c' rs' m' ->
-  plus step tge (State rs m) E0 (State rs' m').
-Proof.
-  intros. inv H.
-  eapply exec_straight_steps_1; eauto.
-  eapply transf_function_no_overflow; eauto.
-  eapply functions_transl; eauto.
-Qed.
-
-Lemma exec_straight_at:
-  forall fb f c ep tf tc c' ep' tc' rs m rs' m',
-  transl_code_at_pc ge (rs PC) fb f c ep tf tc ->
-  transl_code f c' ep' = OK tc' ->
-  exec_straight tge tf tc rs m tc' rs' m' ->
-  transl_code_at_pc ge (rs' PC) fb f c' ep' tf tc'.
-Proof.
-  intros. inv H.
-  exploit exec_straight_steps_2; eauto.
-  eapply transf_function_no_overflow; eauto.
-  eapply functions_transl; eauto.
-  intros [ofs' [PC' CT']].
-  rewrite PC'. constructor; auto.
-Qed.
-
-(** The following lemmas show that the translation from Mach to Asm
-  preserves labels, in the sense that the following diagram commutes:
-<<
-                          translation
-        Mach code ------------------------ Asm instr sequence
-            |                                          |
-            | Mach.find_label lbl       find_label lbl |
-            |                                          |
-            v                                          v
-        Mach code tail ------------------- Asm instr seq tail
-                          translation
->>
-  The proof demands many boring lemmas showing that Asm constructor
-  functions do not introduce new labels.
-*)
-
-Section TRANSL_LABEL.
-
-Remark loadimm_z_label: forall sz rd l k, tail_nolabel k (loadimm_z sz rd l k).
-Proof. 
-  intros; destruct l as [ | [n1 p1] l]; simpl; TailNoLabel.
-  induction l as [ | [n p] l]; simpl; TailNoLabel.
-Qed.
-
-Remark loadimm_n_label: forall sz rd l k, tail_nolabel k (loadimm_n sz rd l k).
-Proof. 
-  intros; destruct l as [ | [n1 p1] l]; simpl; TailNoLabel.
-  induction l as [ | [n p] l]; simpl; TailNoLabel.
-Qed.
-
-Remark loadimm_label: forall sz rd n k, tail_nolabel k (loadimm sz rd n k).
-Proof.
-  unfold loadimm; intros. destruct Nat.leb; [apply loadimm_z_label|apply loadimm_n_label].
-Qed.
-Hint Resolve loadimm_label: labels.
-
-Remark loadimm32_label: forall r n k, tail_nolabel k (loadimm32 r n k).
-Proof.
-  unfold loadimm32; intros. destruct (is_logical_imm32 n); TailNoLabel.
-Qed.
-Hint Resolve loadimm32_label: labels.
-
-Remark loadimm64_label: forall r n k, tail_nolabel k (loadimm64 r n k).
-Proof.
-  unfold loadimm64; intros. destruct (is_logical_imm64 n); TailNoLabel.
-Qed.
-Hint Resolve loadimm64_label: labels.
-
-Remark addimm_aux: forall insn rd r1 n k,
-  (forall rd r1 n, nolabel (insn rd r1 n)) ->
-  tail_nolabel k (addimm_aux insn rd r1 n k).
-Proof.
-  unfold addimm_aux; intros. 
-  destruct Z.eqb. TailNoLabel. destruct Z.eqb; TailNoLabel.
-Qed.
-
-Remark addimm32_label: forall rd r1 n k, tail_nolabel k (addimm32 rd r1 n k).
-Proof.
-  unfold addimm32; intros. 
-  destruct Int.eq. apply addimm_aux; intros; red; auto.
-  destruct Int.eq. apply addimm_aux; intros; red; auto.
-  destruct Int.lt; eapply tail_nolabel_trans; TailNoLabel.
-Qed.
-Hint Resolve addimm32_label: labels.
-
-Remark addimm64_label: forall rd r1 n k, tail_nolabel k (addimm64 rd r1 n k).
-Proof.
-  unfold addimm64; intros. 
-  destruct Int64.eq. apply addimm_aux; intros; red; auto.
-  destruct Int64.eq. apply addimm_aux; intros; red; auto.
-  destruct Int64.lt; eapply tail_nolabel_trans; TailNoLabel.
-Qed.
-Hint Resolve addimm64_label: labels.
-
-Remark logicalimm32_label: forall insn1 insn2 rd r1 n k,
-  (forall rd r1 n, nolabel (insn1 rd r1 n)) ->
-  (forall rd r1 r2 s, nolabel (insn2 rd r1 r2 s)) ->
-  tail_nolabel k (logicalimm32 insn1 insn2 rd r1 n k).
-Proof.
-  unfold logicalimm32; intros.
-  destruct (is_logical_imm32 n). TailNoLabel. eapply tail_nolabel_trans; TailNoLabel.
-Qed.
-
-Remark logicalimm64_label: forall insn1 insn2 rd r1 n k,
-  (forall rd r1 n, nolabel (insn1 rd r1 n)) ->
-  (forall rd r1 r2 s, nolabel (insn2 rd r1 r2 s)) ->
-  tail_nolabel k (logicalimm64 insn1 insn2 rd r1 n k).
-Proof.
-  unfold logicalimm64; intros.
-  destruct (is_logical_imm64 n). TailNoLabel. eapply tail_nolabel_trans; TailNoLabel.
-Qed.
-
-Remark move_extended_label: forall rd r1 ex a k, tail_nolabel k (move_extended rd r1 ex a k).
-Proof.
-  unfold move_extended, move_extended_base; intros. destruct Int.eq, ex; TailNoLabel.
-Qed.
-Hint Resolve move_extended_label: labels.
-
-Remark arith_extended_label: forall insnX insnS rd r1 r2 ex a k,
-  (forall rd r1 r2 x, nolabel (insnX rd r1 r2 x)) ->
-  (forall rd r1 r2 s, nolabel (insnS rd r1 r2 s)) ->
-  tail_nolabel k (arith_extended insnX insnS rd r1 r2 ex a k).
-Proof.
-  unfold arith_extended; intros. destruct Int.ltu.
-  TailNoLabel.
-  destruct ex; simpl; TailNoLabel.
-Qed.
-
-Remark loadsymbol_label: forall r id ofs k, tail_nolabel k (loadsymbol r id ofs k).
-Proof.
-  intros; unfold loadsymbol.
-  destruct (Archi.pic_code tt); TailNoLabel. destruct Ptrofs.eq; TailNoLabel.
-Qed. 
-Hint Resolve loadsymbol_label: labels.
-
-Remark transl_cond_label: forall cond args k c,
-  transl_cond cond args k = OK c -> tail_nolabel k c.
-Proof.
-  unfold transl_cond; intros; destruct cond; TailNoLabel.
-- destruct is_arith_imm32; TailNoLabel. destruct is_arith_imm32; TailNoLabel. eapply tail_nolabel_trans; TailNoLabel.
-- destruct is_arith_imm32; TailNoLabel. destruct is_arith_imm32; TailNoLabel. eapply tail_nolabel_trans; TailNoLabel.
-- destruct is_logical_imm32; TailNoLabel. eapply tail_nolabel_trans; TailNoLabel.
-- destruct is_logical_imm32; TailNoLabel. eapply tail_nolabel_trans; TailNoLabel.
-- destruct is_arith_imm64; TailNoLabel. destruct is_arith_imm64; TailNoLabel. eapply tail_nolabel_trans; TailNoLabel.
-- destruct is_arith_imm64; TailNoLabel. destruct is_arith_imm64; TailNoLabel. eapply tail_nolabel_trans; TailNoLabel.
-- destruct is_logical_imm64; TailNoLabel. eapply tail_nolabel_trans; TailNoLabel.
-- destruct is_logical_imm64; TailNoLabel. eapply tail_nolabel_trans; TailNoLabel.
-Qed.
-
-Remark transl_cond_branch_default_label: forall cond args lbl k c,
-  transl_cond_branch_default cond args lbl k = OK c -> tail_nolabel k c.
-Proof.
-  unfold transl_cond_branch_default; intros. 
-  eapply tail_nolabel_trans; [eapply transl_cond_label;eauto|TailNoLabel].
-Qed.
-Hint Resolve transl_cond_branch_default_label: labels.
-
-Remark transl_cond_branch_label: forall cond args lbl k c,
-  transl_cond_branch cond args lbl k = OK c -> tail_nolabel k c.
-Proof.
-  unfold transl_cond_branch; intros; destruct args; TailNoLabel; destruct cond; TailNoLabel.
-- destruct c0; TailNoLabel.
-- destruct c0; TailNoLabel.
-- destruct (Int.is_power2 n); TailNoLabel.
-- destruct (Int.is_power2 n); TailNoLabel.
-- destruct c0; TailNoLabel.
-- destruct c0; TailNoLabel.
-- destruct (Int64.is_power2' n); TailNoLabel.
-- destruct (Int64.is_power2' n); TailNoLabel.
-Qed.
-
-Remark transl_op_label:
-  forall op args r k c,
-  transl_op op args r k = OK c -> tail_nolabel k c.
-Proof.
-  unfold transl_op; intros; destruct op; TailNoLabel.
-- destruct (preg_of r); try discriminate; destruct (preg_of m); inv H; TailNoLabel.
-- destruct (Float.eq_dec n Float.zero); TailNoLabel.
-- destruct (Float32.eq_dec n Float32.zero); TailNoLabel.
-- apply logicalimm32_label; unfold nolabel; auto.
-- apply logicalimm32_label; unfold nolabel; auto.
-- apply logicalimm32_label; unfold nolabel; auto.
-- unfold shrx32. destruct (Int.eq _ _); try destruct (Int.eq _ _); TailNoLabel.
-- apply arith_extended_label; unfold nolabel; auto.
-- apply arith_extended_label; unfold nolabel; auto.
-- apply logicalimm64_label; unfold nolabel; auto.
-- apply logicalimm64_label; unfold nolabel; auto.
-- apply logicalimm64_label; unfold nolabel; auto.
-- unfold shrx64. destruct (Int.eq _ _); try destruct (Int.eq _ _); TailNoLabel.
-- eapply tail_nolabel_trans. eapply transl_cond_label; eauto. TailNoLabel.
-- destruct (preg_of r); try discriminate; TailNoLabel;
-  (eapply tail_nolabel_trans; [eapply transl_cond_label; eauto | TailNoLabel]).
-Qed.
-
-Remark transl_addressing_label:
-  forall sz addr args insn k c,
-  transl_addressing sz addr args insn k = OK c ->
-  (forall ad, nolabel (insn ad)) ->
-  tail_nolabel k c.
-Proof.
-  unfold transl_addressing; intros; destruct addr; TailNoLabel;
-  eapply tail_nolabel_trans; TailNoLabel.
-  eapply tail_nolabel_trans. apply arith_extended_label; unfold nolabel; auto. TailNoLabel.
-Qed.
-
-Remark transl_load_label:
-  forall trap chunk addr args dst k c,
-  transl_load trap chunk addr args dst k = OK c -> tail_nolabel k c.
-Proof.
-  unfold transl_load; intros; destruct trap; try discriminate; destruct chunk; TailNoLabel; eapply transl_addressing_label; eauto; unfold nolabel; auto.
-Qed.
-
-Remark transl_store_label:
-  forall chunk addr args src k c,
-  transl_store chunk addr args src k = OK c -> tail_nolabel k c.
-Proof.
-  unfold transl_store; intros; destruct chunk; TailNoLabel; eapply transl_addressing_label; eauto; unfold nolabel; auto.
-Qed.
-
-Remark indexed_memory_access_label:
-  forall insn sz base ofs k,
-  (forall ad, nolabel (insn ad)) ->
-  tail_nolabel k (indexed_memory_access insn sz base ofs k).
-Proof.
-  unfold indexed_memory_access; intros. destruct offset_representable.
-  TailNoLabel.
-  eapply tail_nolabel_trans; TailNoLabel.
-Qed.
-
-Remark loadind_label:
-  forall base ofs ty dst k c,
-  loadind base ofs ty dst k = OK c -> tail_nolabel k c.
-Proof.
-  unfold loadind; intros.
-  destruct ty, (preg_of dst); inv H; apply indexed_memory_access_label; intros; exact I.
-Qed.
-
-Remark storeind_label:
-  forall src base ofs ty k c,
-  storeind src base ofs ty k = OK c -> tail_nolabel k c.
-Proof.
-  unfold storeind; intros.
-  destruct ty, (preg_of src); inv H; apply indexed_memory_access_label; intros; exact I.
-Qed.
-
-Remark loadptr_label:
-  forall base ofs dst k, tail_nolabel k (loadptr base ofs dst k).
-Proof.
-  intros. apply indexed_memory_access_label. unfold nolabel; auto.
-Qed.
-
-Remark storeptr_label:
-  forall src base ofs k, tail_nolabel k (storeptr src base ofs k).
-Proof.
-  intros. apply indexed_memory_access_label. unfold nolabel; auto.
-Qed.
-
-Remark make_epilogue_label:
-  forall f k, tail_nolabel k (make_epilogue f k).
-Proof.
-  unfold make_epilogue; intros.
-  (* FIXME destruct is_leaf_function.
-  { TailNoLabel. } *)
-  eapply tail_nolabel_trans.
-  apply loadptr_label.
-  TailNoLabel.
-Qed.
-
-Lemma transl_instr_label:
-  forall f i ep k c,
-  transl_instr f i ep k = OK c ->
-  match i with Mlabel lbl => c = Plabel lbl :: k | _ => tail_nolabel k c end.
-Proof.
-  unfold transl_instr; intros; destruct i; TailNoLabel.
-- eapply loadind_label; eauto.
-- eapply storeind_label; eauto.
-- destruct ep. eapply loadind_label; eauto.
-  eapply tail_nolabel_trans. apply loadptr_label. eapply loadind_label; eauto. 
-- eapply transl_op_label; eauto.
-- eapply transl_load_label; eauto. 
-- eapply transl_store_label; eauto.
-- destruct s0; monadInv H; TailNoLabel.
-- destruct s0; monadInv H; (eapply tail_nolabel_trans; [eapply make_epilogue_label|TailNoLabel]).
-- eapply transl_cond_branch_label; eauto.
-- eapply tail_nolabel_trans; [eapply make_epilogue_label|TailNoLabel].
-Qed.
-
-Lemma transl_instr_label':
-  forall lbl f i ep k c,
-  transl_instr f i ep k = OK c ->
-  find_label lbl c = if Mach.is_label lbl i then Some k else find_label lbl k.
-Proof.
-  intros. exploit transl_instr_label; eauto.
-  destruct i; try (intros [A B]; apply B).
-  intros. subst c. simpl. auto.
-Qed.
-
-Lemma transl_code_label:
-  forall lbl f c ep tc,
-  transl_code f c ep = OK tc ->
-  match Mach.find_label lbl c with
-  | None => find_label lbl tc = None
-  | Some c' => exists tc', find_label lbl tc = Some tc' /\ transl_code f c' false = OK tc'
-  end.
-Proof.
-  induction c; simpl; intros.
-  inv H. auto.
-  monadInv H. rewrite (transl_instr_label' lbl _ _ _ _ _ EQ0).
-  generalize (Mach.is_label_correct lbl a).
-  destruct (Mach.is_label lbl a); intros.
-  subst a. simpl in EQ. exists x; auto.
-  eapply IHc; eauto.
-Qed.
-
-Lemma transl_find_label:
-  forall lbl f tf,
-  transf_function f = OK tf ->
-  match Mach.find_label lbl f.(Mach.fn_code) with
-  | None => find_label lbl tf.(fn_code) = None
-  | Some c => exists tc, find_label lbl tf.(fn_code) = Some tc /\ transl_code f c false = OK tc
-  end.
-Proof.
-  intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (list_length_z x.(fn_code))); inv EQ0.
-  monadInv EQ. rewrite transl_code'_transl_code in EQ0. unfold fn_code. 
-  simpl. destruct (storeptr_label X30 XSP (fn_retaddr_ofs f) x) as [A B]; rewrite B. 
-  eapply transl_code_label; eauto.
-Qed.
-
-End TRANSL_LABEL.
-
-(** A valid branch in a piece of Mach code translates to a valid ``go to''
-  transition in the generated Asm code. *)
-
-Lemma find_label_goto_label:
-  forall f tf lbl rs m c' b ofs,
-  Genv.find_funct_ptr ge b = Some (Internal f) ->
-  transf_function f = OK tf ->
-  rs PC = Vptr b ofs ->
-  Mach.find_label lbl f.(Mach.fn_code) = Some c' ->
-  exists tc', exists rs',
-     goto_label tf lbl rs m = Next rs' m
-  /\ transl_code_at_pc ge (rs' PC) b f c' false tf tc'
-  /\ forall r, r <> PC -> rs'#r = rs#r.
-Proof.
-  intros. exploit (transl_find_label lbl f tf); eauto. rewrite H2.
-  intros [tc [A B]].
-  exploit label_pos_code_tail; eauto. instantiate (1 := 0).
-  intros [pos' [P [Q R]]].
-  exists tc; exists (rs#PC <- (Vptr b (Ptrofs.repr pos'))).
-  split. unfold goto_label. rewrite P. rewrite H1. auto.
-  split. rewrite Pregmap.gss. constructor; auto.
-  rewrite Ptrofs.unsigned_repr. replace (pos' - 0) with pos' in Q.
-  auto. omega.
-  generalize (transf_function_no_overflow _ _ H0). omega.
-  intros. apply Pregmap.gso; auto.
-Qed.
-
-(** Existence of return addresses *)
-
-Lemma return_address_exists:
-  forall f sg ros c, is_tail (Mcall sg ros :: c) f.(Mach.fn_code) ->
-  exists ra, return_address_offset f c ra.
-Proof.
-  intros. eapply Asmgenproof0.return_address_exists; eauto.
-- intros. exploit transl_instr_label; eauto.
-  destruct i; try (intros [A B]; apply A). intros. subst c0. repeat constructor.
-- intros. monadInv H0.
-  destruct (zlt Ptrofs.max_unsigned (list_length_z x.(fn_code))); inv EQ0. monadInv EQ.
-  rewrite transl_code'_transl_code in EQ0.
-  exists x; exists true; split; auto. unfold fn_code.
-  constructor. apply (storeptr_label X30 XSP (fn_retaddr_ofs f0) x).
-- exact transf_function_no_overflow.
-Qed.
-
-(** * Proof of semantic preservation *)
-
-(** Semantic preservation is proved using simulation diagrams
-  of the following form.
-<<
-           st1 --------------- st2
-            |                   |
-           t|                  *|t
-            |                   |
-            v                   v
-           st1'--------------- st2'
->>
-  The invariant is the [match_states] predicate below, which includes:
-- The Asm code pointed by the PC register is the translation of
-  the current Mach code sequence.
-- Mach register values and Asm register values agree.
-*)
-
-Inductive match_states: Mach.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)
-        (LEAF: is_leaf_function f = true -> rs#RA = parent_ra s),
-      match_states (Mach.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 (Mach.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 (Mach.Returnstate s ms m)
-                   (Asm.State rs m').
-
-Lemma exec_straight_steps:
-  forall s fb f rs1 i c ep tf tc m1' m2 m2' sp ms2,
-  match_stack ge s ->
-  Mem.extends m2 m2' ->
-  Genv.find_funct_ptr ge fb = Some (Internal f) ->
-  transl_code_at_pc ge (rs1 PC) fb f (i :: c) ep tf tc ->
-  (forall k c (TR: transl_instr f i ep k = OK c),
-   exists rs2,
-       exec_straight tge tf c rs1 m1' k rs2 m2'
-    /\ agree ms2 sp rs2
-    /\ (it1_is_parent ep i = true -> rs2#X29 = parent_sp s)
-    /\ (is_leaf_function f = true -> rs2#RA = parent_ra s)) ->
-  exists st',
-  plus step tge (State rs1 m1') E0 st' /\
-  match_states (Mach.State s fb sp c ms2 m2) st'.
-Proof.
-  intros. inversion H2. subst. monadInv H7.
-  exploit H3; eauto. intros [rs2 [A [B [C D]]]].
-  exists (State rs2 m2'); split.
-  - eapply exec_straight_exec; eauto.
-  - econstructor; eauto. eapply exec_straight_at; eauto.
-Qed.
-
-Lemma exec_straight_steps_goto:
-  forall s fb f rs1 i c ep tf tc m1' m2 m2' sp ms2 lbl c',
-  match_stack ge s ->
-  Mem.extends m2 m2' ->
-  Genv.find_funct_ptr ge fb = Some (Internal f) ->
-  Mach.find_label lbl f.(Mach.fn_code) = Some c' ->
-  transl_code_at_pc ge (rs1 PC) fb f (i :: c) ep tf tc ->
-  it1_is_parent ep i = false ->
-  (forall k c (TR: transl_instr f i ep k = OK c),
-   exists jmp, exists k', exists rs2,
-       exec_straight tge tf c rs1 m1' (jmp :: k') rs2 m2'
-    /\ agree ms2 sp rs2
-    /\ exec_instr tge tf jmp rs2 m2' = goto_label tf lbl rs2 m2'
-    /\ (is_leaf_function f = true -> rs2#RA = parent_ra s)) ->
-  exists st',
-  plus step tge (State rs1 m1') E0 st' /\
-  match_states (Mach.State s fb sp c' ms2 m2) st'.
-Proof.
-  intros. inversion H3. subst. monadInv H9.
-  exploit H5; eauto. intros [jmp [k' [rs2 [A [B [C D]]]]]].
-  generalize (functions_transl _ _ _ H7 H8); intro FN.
-  generalize (transf_function_no_overflow _ _ H8); intro NOOV.
-  exploit exec_straight_steps_2; eauto.
-  intros [ofs' [PC2 CT2]].
-  exploit find_label_goto_label; eauto.
-  intros [tc' [rs3 [GOTO [AT' OTH]]]].
-  exists (State rs3 m2'); split.
-  eapply plus_right'.
-  eapply exec_straight_steps_1; eauto.
-  econstructor; eauto.
-  eapply find_instr_tail. eauto.
-  rewrite C. eexact GOTO.
-  traceEq.
-  econstructor; eauto.
-  apply agree_exten with rs2; auto with asmgen.
-  congruence.
-  rewrite OTH by congruence; auto.
-Qed.
-
-Lemma exec_straight_opt_steps_goto:
-  forall s fb f rs1 i c ep tf tc m1' m2 m2' sp ms2 lbl c',
-  match_stack ge s ->
-  Mem.extends m2 m2' ->
-  Genv.find_funct_ptr ge fb = Some (Internal f) ->
-  Mach.find_label lbl f.(Mach.fn_code) = Some c' ->
-  transl_code_at_pc ge (rs1 PC) fb f (i :: c) ep tf tc ->
-  it1_is_parent ep i = false ->
-  (forall k c (TR: transl_instr f i ep k = OK c),
-   exists jmp, exists k', exists rs2,
-       exec_straight_opt tge tf c rs1 m1' (jmp :: k') rs2 m2'
-    /\ agree ms2 sp rs2
-    /\ exec_instr tge tf jmp rs2 m2' = goto_label tf lbl rs2 m2'
-    /\ (is_leaf_function f = true -> rs2#RA = parent_ra s)) ->
-  exists st',
-  plus step tge (State rs1 m1') E0 st' /\
-  match_states (Mach.State s fb sp c' ms2 m2) st'.
-Proof.
-  intros. inversion H3. subst. monadInv H9.
-  exploit H5; eauto. intros [jmp [k' [rs2 [A [B [C D]]]]]].
-  generalize (functions_transl _ _ _ H7 H8); intro FN.
-  generalize (transf_function_no_overflow _ _ H8); intro NOOV.
-  inv A.
-- exploit find_label_goto_label; eauto.
-  intros [tc' [rs3 [GOTO [AT' OTH]]]].
-  exists (State rs3 m2'); split.
-  apply plus_one. econstructor; eauto.
-  eapply find_instr_tail. eauto.
-  rewrite C. eexact GOTO.
-  econstructor; eauto.
-  apply agree_exten with rs2; auto with asmgen.
-  congruence.
-  rewrite OTH by congruence; auto.
-- exploit exec_straight_steps_2; eauto.
-  intros [ofs' [PC2 CT2]].
-  exploit find_label_goto_label; eauto.
-  intros [tc' [rs3 [GOTO [AT' OTH]]]].
-  exists (State rs3 m2'); split.
-  eapply plus_right'.
-  eapply exec_straight_steps_1; eauto.
-  econstructor; eauto.
-  eapply find_instr_tail. eauto.
-  rewrite C. eexact GOTO.
-  traceEq.
-  econstructor; eauto.
-  apply agree_exten with rs2; auto with asmgen.
-  congruence.
-  rewrite OTH by congruence; auto.
-Qed.
-
-(** We need to show that, in the simulation diagram, we cannot
-  take infinitely many Mach transitions that correspond to zero
-  transitions on the Asm side.  Actually, all Mach transitions
-  correspond to at least one Asm transition, except the
-  transition from [Machsem.Returnstate] to [Machsem.State].
-  So, the following integer measure will suffice to rule out
-  the unwanted behaviour. *)
-
-Definition measure (s: Mach.state) : nat :=
-  match s with
-  | Mach.State _ _ _ _ _ _ => 0%nat
-  | Mach.Callstate _ _ _ _ => 0%nat
-  | Mach.Returnstate _ _ _ => 1%nat
-  end.
-
-Remark preg_of_not_X29: forall r, negb (mreg_eq r R29) = true -> IR X29 <> preg_of r.
-Proof.
-  intros. change (IR X29) with (preg_of R29). red; intros.
-  exploit preg_of_injective; eauto. intros; subst r; discriminate.
-Qed.
-
-Lemma sp_val': forall ms sp rs, agree ms sp rs -> sp = rs XSP.
-Proof.
-  intros. eapply sp_val; eauto. 
-Qed. 
-
-(** This is the simulation diagram.  We prove it by case analysis on the Mach transition. *)
-
-Theorem step_simulation:
-  forall S1 t S2, Mach.step return_address_offset ge S1 t S2 ->
-  forall S1' (MS: match_states S1 S1')  (WF: wf_state ge S1),
-  (exists S2', plus step tge S1' t S2' /\ match_states S2 S2')
-  \/ (measure S2 < measure S1 /\ t = E0 /\ match_states S2 S1')%nat.
-Proof.
-  induction 1; intros; inv MS.
-
-- (* Mlabel *)
-  left; eapply exec_straight_steps; eauto; intros.
-  monadInv TR. econstructor; split. apply exec_straight_one. simpl; eauto. auto.
-  split. { apply agree_nextinstr; auto. }
-  split. { simpl; congruence. }
-  rewrite nextinstr_inv by congruence; assumption.
-
-- (* Mgetstack *)
-  unfold load_stack in H.
-  exploit Mem.loadv_extends; eauto. intros [v' [A B]].
-  rewrite (sp_val _ _ _ AG) in A.
-  left; eapply exec_straight_steps; eauto. intros. simpl in TR.
-  exploit loadind_correct; eauto with asmgen. intros [rs' [P [Q [R S]]]].
-  exists rs'; split. eauto.
-  split. { eapply agree_set_mreg; eauto with asmgen. congruence. }
-  split. { simpl; congruence. }
-  rewrite S. assumption.
-
-- (* Msetstack *)
-  unfold store_stack in H.
-  assert (Val.lessdef (rs src) (rs0 (preg_of src))) by (eapply preg_val; eauto).
-  exploit Mem.storev_extends; eauto. intros [m2' [A B]].
-  left; eapply exec_straight_steps; eauto.
-  rewrite (sp_val _ _ _ AG) in A. intros. simpl in TR.
-  exploit storeind_correct; eauto with asmgen. intros [rs' [P [Q R]]].
-  exists rs'; split. eauto.
-  split. eapply agree_undef_regs; eauto with asmgen.
-  simpl; intros.
-  split. rewrite Q; auto with asmgen.
-  rewrite R. assumption.
-
-- (* Mgetparam *)
-  assert (f0 = f) by congruence; subst f0.
-  unfold load_stack in *.
-  exploit Mem.loadv_extends. eauto. eexact H0. auto.
-  intros [parent' [A B]]. rewrite (sp_val' _ _ _ AG) in A.
-  exploit lessdef_parent_sp; eauto. clear B; intros B; subst parent'.
-  exploit Mem.loadv_extends. eauto. eexact H1. auto.
-  intros [v' [C D]].
-Opaque loadind.
-  left; eapply exec_straight_steps; eauto; intros. monadInv TR. 
-  destruct ep.
-(* X30 contains parent *)
-  exploit loadind_correct. eexact EQ.
-  instantiate (2 := rs0). simpl; rewrite DXP; eauto. simpl; congruence.
-  intros [rs1 [P [Q [R S]]]].
-  exists rs1; split. eauto.
-  split. eapply agree_set_mreg. eapply agree_set_mreg; eauto. congruence. auto with asmgen.
-  simpl; split; intros.
-  { rewrite R; auto with asmgen.
-    apply preg_of_not_X29; auto.
-  }
-  { rewrite S; auto. }
-    
-(* X30 does not contain parent *)
-  exploit loadptr_correct. eexact A. simpl; congruence. intros [rs1 [P [Q R]]].
-  exploit loadind_correct. eexact EQ. instantiate (2 := rs1). simpl; rewrite Q. eauto. simpl; congruence.
-  intros [rs2 [S [T [U V]]]].
-  exists rs2; split. eapply exec_straight_trans; eauto.
-  split. eapply agree_set_mreg. eapply agree_set_mreg. eauto. eauto.
-  instantiate (1 := rs1#X29 <- (rs2#X29)). intros.
-  rewrite Pregmap.gso; auto with asmgen.
-  congruence.
-  intros. unfold Pregmap.set. destruct (PregEq.eq r' X29). congruence. auto with asmgen.
-  split; simpl; intros. rewrite U; auto with asmgen.
-  apply preg_of_not_X29; auto.
-  rewrite V. rewrite R by congruence. auto.
-  
-- (* Mop *)
-  assert (eval_operation tge sp op (map rs args) m = Some v).
-  { rewrite <- H. apply eval_operation_preserved. exact symbols_preserved. }
-  exploit eval_operation_lessdef. eapply preg_vals; eauto. eauto. eexact H0.
-  intros [v' [A B]]. rewrite (sp_val _ _ _ AG) in A.
-  left; eapply exec_straight_steps; eauto; intros. simpl in TR.
-  exploit transl_op_correct; eauto. intros [rs2 [P [Q [R S]]]].
-  exists rs2; split. eauto. split.
-  apply agree_set_undef_mreg with rs0; auto. 
-  apply Val.lessdef_trans with v'; auto.
-  split; simpl; intros. InvBooleans. 
-  rewrite R; auto. apply preg_of_not_X29; auto.
-Local Transparent destroyed_by_op.
-  destruct op; try exact I; simpl; congruence.
-  rewrite S.
-  auto.
-- (* Mload *)
-  destruct trap.
-  {
-  assert (Op.eval_addressing tge sp addr (map rs args) = Some a).
-  { rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved. }
-  exploit eval_addressing_lessdef. eapply preg_vals; eauto. eexact H1.
-  intros [a' [A B]]. rewrite (sp_val _ _ _ AG) in A.
-  exploit Mem.loadv_extends; eauto. intros [v' [C D]].
-  left; eapply exec_straight_steps; eauto; intros. simpl in TR.
-  exploit transl_load_correct; eauto. intros [rs2 [P [Q [R S]]]].
-  exists rs2; split. eauto.
-  split. eapply agree_set_undef_mreg; eauto. congruence.
-  split. simpl; congruence.
-  rewrite S. assumption.
-  }
-  
-  (* Mload notrap1 *)
-  inv AT. simpl in *. unfold bind in *. destruct (transl_code _ _ _) in *; discriminate.
-
-- (* Mload notrap *)
-  inv AT. simpl in *. unfold bind in *. destruct (transl_code _ _ _) in *; discriminate.
-
-- (* Mload notrap *)
-  inv AT. simpl in *. unfold bind in *. destruct (transl_code _ _ _) in *; discriminate.
-
-- (* Mstore *)
-  assert (Op.eval_addressing tge sp addr (map rs args) = Some a).
-  { rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved. }
-  exploit eval_addressing_lessdef. eapply preg_vals; eauto. eexact H1.
-  intros [a' [A B]]. rewrite (sp_val _ _ _ AG) in A.
-  assert (Val.lessdef (rs src) (rs0 (preg_of src))) by (eapply preg_val; eauto).
-  exploit Mem.storev_extends; eauto. intros [m2' [C D]].
-  left; eapply exec_straight_steps; eauto.
-  intros. simpl in TR. exploit transl_store_correct; eauto. intros [rs2 [P [Q R]]].
-  exists rs2; split. eauto.
-  split. eapply agree_undef_regs; eauto with asmgen.
-  split. simpl; congruence.
-  rewrite R. assumption.
-
-- (* Mcall *)
-  assert (f0 = f) by congruence.  subst f0.
-  inv AT.
-  assert (NOOV: list_length_z tf.(fn_code) <= Ptrofs.max_unsigned).
-  { eapply transf_function_no_overflow; eauto. }
-  destruct ros as [rf|fid]; simpl in H; monadInv H5.
-+ (* Indirect call *)
-  assert (rs rf = Vptr f' Ptrofs.zero).
-  { destruct (rs rf); try discriminate.
-    revert H; predSpec Ptrofs.eq Ptrofs.eq_spec i Ptrofs.zero; intros; congruence. }
-  assert (rs0 x0 = Vptr f' Ptrofs.zero).
-  { exploit ireg_val; eauto. rewrite H5; intros LD; inv LD; auto. }
-  generalize (code_tail_next_int _ _ _ _ NOOV H6). intro CT1.
-  assert (TCA: transl_code_at_pc ge (Vptr fb (Ptrofs.add ofs Ptrofs.one)) fb f c false tf x).
-  {  econstructor; eauto. }
-  exploit return_address_offset_correct; eauto. intros; subst ra.
-  left; econstructor; split.
-  apply plus_one. eapply exec_step_internal. Simpl. rewrite <- H2; simpl; eauto.
-  eapply functions_transl; eauto. eapply find_instr_tail; eauto.
-  simpl. eauto.
-  econstructor; eauto.
-  econstructor; eauto.
-  eapply agree_sp_def; eauto.
-  simpl. eapply agree_exten; eauto. intros. Simpl.
-  Simpl. rewrite <- H2. auto.
-+ (* Direct call *)
-  generalize (code_tail_next_int _ _ _ _ NOOV H6). intro CT1.
-  assert (TCA: transl_code_at_pc ge (Vptr fb (Ptrofs.add ofs Ptrofs.one)) fb f c false tf x).
-    econstructor; eauto.
-  exploit return_address_offset_correct; eauto. intros; subst ra.
-  left; econstructor; split.
-  apply plus_one. eapply exec_step_internal. eauto.
-  eapply functions_transl; eauto. eapply find_instr_tail; eauto.
-  simpl. unfold Genv.symbol_address. rewrite symbols_preserved. rewrite H. eauto.
-  econstructor; eauto.
-  econstructor; eauto.
-  eapply agree_sp_def; eauto.
-  simpl. eapply agree_exten; eauto. intros. Simpl.
-  Simpl. rewrite <- H2. auto.
-
-- (* Mtailcall *)
-  assert (f0 = f) by congruence.  subst f0.
-  inversion AT; subst.
-  assert (NOOV: list_length_z tf.(fn_code) <= Ptrofs.max_unsigned).
-  { eapply transf_function_no_overflow; eauto. }
-  exploit Mem.loadv_extends. eauto. eexact H1. auto. simpl. intros [parent' [A B]].
-  destruct ros as [rf|fid]; simpl in H; monadInv H7.
-+ (* Indirect call *)
-  assert (rs rf = Vptr f' Ptrofs.zero).
-  { destruct (rs rf); try discriminate.
-    revert H; predSpec Ptrofs.eq Ptrofs.eq_spec i Ptrofs.zero; intros; congruence. }
-  assert (rs0 x0 = Vptr f' Ptrofs.zero).
-  { exploit ireg_val; eauto. rewrite H7; intros LD; inv LD; auto. }
-  exploit make_epilogue_correct; eauto. intros (rs1 & m1 & U & V & W & X & Y & Z). 
-  exploit exec_straight_steps_2; eauto using functions_transl.                      
-  intros (ofs' & P & Q).
-  left; econstructor; split.
-  (* execution *)
-  eapply plus_right'. eapply exec_straight_exec; eauto.
-  econstructor. eexact P. eapply functions_transl; eauto. eapply find_instr_tail. eexact Q.
-  simpl. reflexivity.
-  traceEq.
-  (* match states *)
-  econstructor; eauto.
-  apply agree_set_other; auto with asmgen.
-  Simpl. rewrite Z by (rewrite <- (ireg_of_eq _ _ EQ1); eauto with asmgen). assumption. 
-+ (* Direct call *)
-  exploit make_epilogue_correct; eauto. intros (rs1 & m1 & U & V & W & X & Y & Z). 
-  exploit exec_straight_steps_2; eauto using functions_transl.                      
-  intros (ofs' & P & Q).
-  left; econstructor; split.
-  (* execution *)
-  eapply plus_right'. eapply exec_straight_exec; eauto.
-  econstructor. eexact P. eapply functions_transl; eauto. eapply find_instr_tail. eexact Q.
-  simpl. reflexivity.
-  traceEq.
-  (* match states *)
-  econstructor; eauto.
-  apply agree_set_other; auto with asmgen.
-  Simpl. unfold Genv.symbol_address. rewrite symbols_preserved. rewrite H. auto.
-
-- (* Mbuiltin *)
-  inv AT. monadInv H4.
-  exploit functions_transl; eauto. intro FN.
-  generalize (transf_function_no_overflow _ _ H3); intro NOOV.
-  exploit builtin_args_match; eauto. intros [vargs' [P Q]].
-  exploit external_call_mem_extends; eauto.
-  intros [vres' [m2' [A [B [C D]]]]].
-  left. econstructor; split. apply plus_one.
-  eapply exec_step_builtin. eauto. eauto.
-  eapply find_instr_tail; eauto.
-  erewrite <- sp_val by eauto.
-  eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved.
-  eapply external_call_symbols_preserved; eauto. apply senv_preserved.
-  eauto.
-  econstructor; eauto.
-  instantiate (2 := tf); instantiate (1 := x).
-  unfold nextinstr. rewrite Pregmap.gss.
-  rewrite set_res_other. rewrite undef_regs_other_2.
-  rewrite <- H1. simpl. econstructor; eauto.
-  eapply code_tail_next_int; eauto.
-  rewrite preg_notin_charact. intros. auto with asmgen.
-  auto with asmgen.
-  apply agree_nextinstr. eapply agree_set_res; auto.
-  eapply agree_undef_regs; eauto. intros. rewrite undef_regs_other_2; auto.
-  congruence.
-
-  Simpl.
-  rewrite set_res_other by trivial.
-  rewrite undef_regs_other.
-  assumption.
-  intro.
-  rewrite in_map_iff.
-  intros (x0 & PREG & IN).
-  subst r'.
-  intro.
-  apply (preg_of_not_RA x0).
-  congruence.
-  
-- (* Mgoto *)
-  assert (f0 = f) by congruence. subst f0.
-  inv AT. monadInv H4.
-  exploit find_label_goto_label; eauto. intros [tc' [rs' [GOTO [AT2 INV]]]].
-  left; exists (State rs' m'); split.
-  apply plus_one. econstructor; eauto.
-  eapply functions_transl; eauto.
-  eapply find_instr_tail; eauto.
-  simpl; eauto.
-  econstructor; eauto.
-  eapply agree_exten; eauto with asmgen.
-  congruence.
-
-  rewrite INV by congruence.
-  assumption.
-  
-- (* Mcond true *)
-  assert (f0 = f) by congruence. subst f0.
-  exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC.
-  left; eapply exec_straight_opt_steps_goto; eauto.
-  intros. simpl in TR.
-  exploit transl_cond_branch_correct; eauto. intros (rs' & jmp & A & B & C & D).
-  exists jmp; exists k; exists rs'.
-  split. eexact A. 
-  split. apply agree_exten with rs0; auto with asmgen.
-  split.
-  exact B.
-  rewrite D. exact LEAF.
-
-- (* Mcond false *)
-  exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC.
-  left; eapply exec_straight_steps; eauto. intros. simpl in TR.
-  exploit transl_cond_branch_correct; eauto. intros (rs' & jmp & A & B & C & D).
-  econstructor; split.
-  eapply exec_straight_opt_right. eexact A. apply exec_straight_one. eexact B. auto.
-  split. apply agree_exten with rs0; auto. intros. Simpl.
-  split.
-  simpl; congruence.
-  Simpl. rewrite D.
-  exact LEAF.
-
-- (* Mjumptable *)
-  assert (f0 = f) by congruence. subst f0.
-  inv AT. monadInv H6.
-  exploit functions_transl; eauto. intro FN.
-  generalize (transf_function_no_overflow _ _ H5); intro NOOV.
-  exploit find_label_goto_label. eauto. eauto.
-  instantiate (2 := rs0#X16 <- Vundef #X17 <- Vundef).
-  Simpl. eauto.
-  eauto.
-  intros [tc' [rs' [A [B C]]]].
-  exploit ireg_val; eauto. rewrite H. intros LD; inv LD.
-  left; econstructor; split.
-  apply plus_one. econstructor; eauto.
-  eapply find_instr_tail; eauto.
-  simpl. Simpl. rewrite <- H9. unfold Mach.label in H0; unfold label; rewrite H0. eexact A.
-  econstructor; eauto.
-  eapply agree_undef_regs; eauto.
-  simpl. intros. rewrite C; auto with asmgen. Simpl.
-  congruence.
-
-  rewrite C by congruence.
-  repeat rewrite Pregmap.gso by congruence.
-  assumption.
-  
-- (* Mreturn *)
-  assert (f0 = f) by congruence. subst f0.
-  inversion AT; subst. simpl in H6; monadInv H6.
-  assert (NOOV: list_length_z tf.(fn_code) <= Ptrofs.max_unsigned).
-    eapply transf_function_no_overflow; eauto.
-  exploit make_epilogue_correct; eauto. intros (rs1 & m1 & U & V & W & X & Y & Z).
-  exploit exec_straight_steps_2; eauto using functions_transl.                      
-  intros (ofs' & P & Q).
-  left; econstructor; split.
-  (* execution *)
-  eapply plus_right'. eapply exec_straight_exec; eauto.
-  econstructor. eexact P. eapply functions_transl; eauto. eapply find_instr_tail. eexact Q.
-  simpl. reflexivity.
-  traceEq.
-  (* match states *)
-  econstructor; eauto.
-  apply agree_set_other; auto with asmgen.
-
-- (* internal function *)
-
-  exploit functions_translated; eauto. intros [tf [A B]]. monadInv B.
-  generalize EQ; intros EQ'. monadInv EQ'.
-  destruct (zlt Ptrofs.max_unsigned (list_length_z x0.(fn_code))); inversion EQ1. clear EQ1. subst x0.
-  unfold 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]].
-  change (chunk_of_type Tptr) with Mint64 in *.
-  (* Execution of function prologue *)
-  monadInv EQ0. rewrite transl_code'_transl_code in EQ1.
-  set (tfbody := Pallocframe (fn_stacksize f) (fn_link_ofs f) ::
-                 storeptr RA XSP (fn_retaddr_ofs f) x0) in *.
-  set (tf := {| fn_sig := Mach.fn_sig f; fn_code := tfbody |}) in *.
-  set (rs2 := nextinstr (rs0#X29 <- (parent_sp s) #SP <- sp #X16 <- Vundef)).
-  exploit (storeptr_correct tge tf XSP (fn_retaddr_ofs f) RA x0 m2' m3' rs2).
-    simpl preg_of_iregsp. change (rs2 X30) with (rs0 X30). rewrite ATLR. 
-    change (rs2 X2) with sp. eexact P. 
-    simpl; congruence. congruence.
-  intros (rs3 & U & V & W).
-  assert (EXEC_PROLOGUE:
-            exec_straight tge tf
-              tf.(fn_code) rs0 m'
-              x0 rs3 m3').
-  { change (fn_code tf) with tfbody; unfold tfbody.
-    apply exec_straight_step with rs2 m2'.
-    unfold exec_instr. rewrite C. fold sp.
-    rewrite <- (sp_val _ _ _ AG). rewrite F. reflexivity.
-    reflexivity. 
-    eexact U. }
-  exploit exec_straight_steps_2; eauto using functions_transl. omega. constructor.
-  intros (ofs' & X & Y).                    
-  left; exists (State rs3 m3'); split.
-  eapply exec_straight_steps_1; eauto. omega. constructor.
-  econstructor; eauto.
-  rewrite X; econstructor; eauto. 
-  apply agree_exten with rs2; eauto with asmgen.
-  unfold rs2. 
-  apply agree_nextinstr. 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.
-  simpl; intros; Simpl.
-  unfold sp; congruence.
-  intros. rewrite V by auto with asmgen. reflexivity.
-
-  rewrite W.
-  unfold rs2.
-  Simpl.
-  
-- (* external function *)
-  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 STACKS. simpl in *.
-  right. split. omega. split. auto.
-  rewrite <- ATPC in H5.
-  econstructor; eauto. congruence.
-  inv WF.
-  inv STACK.
-  inv H1.
-  congruence.
-Qed.
-
-Lemma transf_initial_states:
-  forall st1, Mach.initial_state prog st1 ->
-  exists st2, Asm.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 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 -> Mach.final_state st1 r -> Asm.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.
-
-Theorem transf_program_correct:
-  forward_simulation (Mach.semantics return_address_offset prog) (Asm.semantics tprog).
-Proof.
-  eapply forward_simulation_star with (measure := measure)
-         (match_states := fun S1 S2 => match_states S1 S2 /\ wf_state ge S1).
-  - apply senv_preserved.
-  - simpl; intros. exploit transf_initial_states; eauto.
-    intros (s2 & A & B).
-    exists s2; intuition auto. apply wf_initial; auto.
-  - simpl; intros. destruct H as [MS WF]. eapply transf_final_states; eauto.
-  - simpl; intros. destruct H0 as [MS WF]. 
-    exploit step_simulation; eauto. intros [ (s2' & A & B) | (A & B & C) ].
-    + left; exists s2'; intuition auto. eapply wf_step; eauto. 
-    + right; intuition auto. eapply wf_step; eauto.
-Qed.
-
-End PRESERVATION.
diff --git a/configure b/configure
index 339c9bce..a7c9df9d 100755
--- a/configure
+++ b/configure
@@ -847,8 +847,8 @@ ARCHDIRS=$arch kvx/lib kvx/abstractbb kvx/abstractbb/Impure
 BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v OptionMonad.v IterList.v PseudoAsmblock.v PseudoAsmblockproof.v ForwardSimulationBlock.v\\
     AbstractBasicBlocksDef.v SeqSimuTheory.v ImpSimuTest.v Parallelizability.v\\
     ImpConfig.v ImpCore.v ImpExtern.v ImpHCons.v ImpIO.v ImpLoops.v ImpMonads.v ImpPrelude.v\\
-    Asmblock.v\\
-    Asmgenproof0.v Asmgenproof1.v Asmgenproof.v # TODO: CHANGE THIS
+    Asmblock.v Asmblockgen.v\\
+    Asmgenproof.v # TODO: CHANGE THIS
 EOF
 fi