Some cleanup in todos

4 files changed, 13 insertions, 624 deletions

diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v
index 16f8e0c0..f12e8922 100644
--- a/aarch64/Asmblock.v
+++ b/aarch64/Asmblock.v
@@ -82,8 +82,6 @@ Inductive control: Type :=
              (args: list (builtin_arg dreg)) (res: builtin_res dreg)  (**r built-in function (pseudo) *)
   .
 
-Coercion PCtlFlow: cf_instruction >-> control.
-
 (** Basic instructions *)
 
 (* Loads waiting for (rd: dreg) (a: addressing)
@@ -319,7 +317,7 @@ Inductive ar_instruction : Type :=
 .
 
 Inductive basic : Type :=
-  | PArith (i: ar_instruction)                                        (**r TODO *)
+  | PArith (i: ar_instruction)
   | PLoad (ld: ld_instruction)
   | PStore (st: st_instruction)
   | Pallocframe (sz: Z) (linkofs: ptrofs)                             (**r allocate new stack frame *)
@@ -335,8 +333,20 @@ Inductive basic : Type :=
 *)
 .
 
+Coercion PCtlFlow: cf_instruction >-> control.
 Coercion PLoad: ld_instruction >-> basic.
 Coercion PStore : st_instruction >-> basic.
+Coercion PArithP: arith_p >-> Funclass.
+Coercion PArithPP: arith_pp >-> Funclass.
+Coercion PArithPPP: arith_ppp >-> Funclass.
+Coercion PArithRR0: arith_rr0 >-> Funclass.
+Coercion PArithRR0R: arith_rr0r >-> Funclass.
+Coercion PArithARRRR0: arith_arrrr0 >-> Funclass.
+Coercion PArithComparisonP: arith_comparison_p >-> Funclass.
+Coercion PArithComparisonPP: arith_comparison_pp >-> Funclass.
+Coercion PArithComparisonR0R: arith_comparison_r0r >-> Funclass.
+Coercion PArith: ar_instruction >-> basic.
+
 
 (* Not used in Coq, declared in ocaml directly in PostpassSchedulingOracle.ml
 Inductive instruction : Type :=
@@ -414,160 +424,6 @@ Record function : Type := mkfunction { fn_sig: signature; fn_blocks: bblocks }.
 Definition fundef := AST.fundef function.
 Definition program := AST.program fundef unit.
 
-(* TODO: ORIGINAL ABSTRACT SYNTAX OF INSTRUCTIONS THAT NEEDS TO BE ADAPTED !
-
-Inductive instruction: Type :=
-  (** Branches *)
-  | Pb (lbl: label)                                                   (**r branch *)
-  | Pbc (c: testcond) (lbl: label)                                    (**r conditional branch *)
-  | Pbl (id: ident) (sg: signature)                                   (**r jump to function and link *)
-  | Pbs (id: ident) (sg: signature)                                   (**r jump to function *)
-  | Pblr (r: ireg) (sg: signature)                                    (**r indirect jump and link *)
-  | Pbr (r: ireg) (sg: signature)                                     (**r indirect jump *)
-  | Pret (r: ireg)                                                    (**r return *)
-  | Pcbnz (sz: isize) (r: ireg) (lbl: label)                          (**r branch if not zero *)
-  | Pcbz (sz: isize) (r: ireg) (lbl: label)                           (**r branch if zero *)
-  | Ptbnz (sz: isize) (r: ireg) (n: int) (lbl: label)                 (**r branch if bit n is not zero *)
-  | Ptbz (sz: isize) (r: ireg) (n: int) (lbl: label)                  (**r branch if bit n is zero *)
-  (** Memory loads and stores *)
-  | Pldrw (rd: ireg) (a: addressing)                                  (**r load int32 *)
-  | Pldrw_a (rd: ireg) (a: addressing)                                (**r load int32 as any32 *)
-  | Pldrx (rd: ireg) (a: addressing)                                  (**r load int64 *)
-  | Pldrx_a (rd: ireg) (a: addressing)                                (**r load int64 as any64 *)
-  | Pldrb (sz: isize) (rd: ireg) (a: addressing)                      (**r load int8, zero-extend *)
-  | Pldrsb (sz: isize) (rd: ireg) (a: addressing)                     (**r load int8, sign-extend *)
-  | Pldrh (sz: isize) (rd: ireg) (a: addressing)                      (**r load int16, zero-extend *)
-  | Pldrsh (sz: isize) (rd: ireg) (a: addressing)                     (**r load int16, sign-extend *)
-  | Pldrzw (rd: ireg) (a: addressing)                                 (**r load int32, zero-extend to int64 *)
-  | Pldrsw (rd: ireg) (a: addressing)                                 (**r load int32, sign-extend to int64 *)
-  | Pldp (rd1 rd2: ireg) (a: addressing)                              (**r load two int64 *)
-  | Pstrw (rs: ireg) (a: addressing)                                  (**r store int32 *)
-  | Pstrw_a (rs: ireg) (a: addressing)                                (**r store int32 as any32 *)
-  | Pstrx (rs: ireg) (a: addressing)                                  (**r store int64 *)
-  | Pstrx_a (rs: ireg) (a: addressing)                                (**r store int64 as any64 *)
-  | Pstrb (rs: ireg) (a: addressing)                                  (**r store int8 *)
-  | Pstrh (rs: ireg) (a: addressing)                                  (**r store int16 *)
-  | Pstp (rs1 rs2: ireg) (a: addressing)                              (**r store two int64 *)
-  (** Integer arithmetic, immediate *)
-  | Paddimm (sz: isize) (rd: iregsp) (r1: iregsp) (n: Z)              (**r addition *)
-  | Psubimm (sz: isize) (rd: iregsp) (r1: iregsp) (n: Z)              (**r subtraction *)
-  | Pcmpimm (sz: isize) (r1: ireg) (n: Z)                             (**r compare *)
-  | Pcmnimm (sz: isize) (r1: ireg) (n: Z)                             (**r compare negative *)
-  (** Move integer register *)
-  | Pmov (rd: iregsp) (r1: iregsp)
-  (** Logical, immediate *)
-  | Pandimm (sz: isize) (rd: ireg) (r1: ireg0) (n: Z)                 (**r and *)
-  | Peorimm (sz: isize) (rd: ireg) (r1: ireg0) (n: Z)                 (**r xor *)
-  | Porrimm (sz: isize) (rd: ireg) (r1: ireg0) (n: Z)                 (**r or *)
-  | Ptstimm (sz: isize) (r1: ireg) (n: Z)                             (**r and, then set flags *)
-  (** Move wide immediate *)
-  | Pmovz (sz: isize) (rd: ireg) (n: Z) (pos: Z)                      (**r move [n << pos] to [rd] *)
-  | Pmovn (sz: isize) (rd: ireg) (n: Z) (pos: Z)                      (**r move [NOT(n << pos)] to [rd] *)
-  | Pmovk (sz: isize) (rd: ireg) (n: Z) (pos: Z)                      (**r insert 16 bits of [n] at [pos] in rd *)
-  (** PC-relative addressing *)
-  | Padrp (rd: ireg) (id: ident) (ofs: ptrofs)                        (**r set [rd] to high address of [id + ofs] *)
-  | Paddadr (rd: ireg) (r1: ireg) (id: ident) (ofs: ptrofs)           (**r add the low address of [id + ofs] *)
-  (** Bit-field operations *)
-  | Psbfiz (sz: isize) (rd: ireg) (r1: ireg) (r: int) (s: Z)          (**r sign extend and shift left *)
-  | Psbfx (sz: isize) (rd: ireg) (r1: ireg) (r: int) (s: Z)           (**r shift right and sign extend *)
-  | Pubfiz (sz: isize) (rd: ireg) (r1: ireg) (r: int) (s: Z)          (**r zero extend and shift left *)
-  | Pubfx (sz: isize) (rd: ireg) (r1: ireg) (r: int) (s: Z)           (**r shift right and zero extend *)
-  (** Integer arithmetic, shifted register *)
-  | Padd (sz: isize) (rd: ireg) (r1: ireg0) (r2: ireg) (s: shift_op)  (**r addition *)
-  | Psub (sz: isize) (rd: ireg) (r1: ireg0) (r2: ireg) (s: shift_op)  (**r subtraction *)
-  | Pcmp (sz: isize) (r1: ireg0) (r2: ireg) (s: shift_op)             (**r compare *)
-  | Pcmn (sz: isize) (r1: ireg0) (r2: ireg) (s: shift_op)             (**r compare negative *)
-  (** Integer arithmetic, extending register *)
-  | Paddext (rd: iregsp) (r1: iregsp) (r2: ireg) (x: extend_op)       (**r int64-int32 add *)
-  | Psubext (rd: iregsp) (r1: iregsp) (r2: ireg) (x: extend_op)       (**r int64-int32 sub *)
-  | Pcmpext (r1: ireg) (r2: ireg) (x: extend_op)                      (**r int64-int32 cmp *)
-  | Pcmnext (r1: ireg) (r2: ireg) (x: extend_op)                      (**r int64-int32 cmn *)
-  (** Logical, shifted register *)
-  | Pand (sz: isize) (rd: ireg) (r1: ireg0) (r2: ireg) (s: shift_op)  (**r and *)
-  | Pbic (sz: isize) (rd: ireg) (r1: ireg0) (r2: ireg) (s: shift_op)  (**r and-not *)
-  | Peon (sz: isize) (rd: ireg) (r1: ireg0) (r2: ireg) (s: shift_op)  (**r xor-not *)
-  | Peor (sz: isize) (rd: ireg) (r1: ireg0) (r2: ireg) (s: shift_op)  (**r xor *)
-  | Porr (sz: isize) (rd: ireg) (r1: ireg0) (r2: ireg) (s: shift_op)  (**r or *)
-  | Porn (sz: isize) (rd: ireg) (r1: ireg0) (r2: ireg) (s: shift_op)  (**r or-not *)
-  | Ptst (sz: isize) (r1: ireg0) (r2: ireg) (s: shift_op)             (**r and, then set flags *)
-  (** Variable shifts *)
-  | Pasrv (sz: isize) (rd: ireg) (r1 r2: ireg)                        (**r arithmetic right shift *)
-  | Plslv (sz: isize) (rd: ireg) (r1 r2: ireg)                        (**r left shift *)
-  | Plsrv (sz: isize) (rd: ireg) (r1 r2: ireg)                        (**r logical right shift *)
-  | Prorv (sz: isize) (rd: ireg) (r1 r2: ireg)                        (**r rotate right *)
-  (** Bit operations *)
-  | Pcls (sz: isize) (rd r1: ireg)                                    (**r count leading sign bits *)
-  | Pclz (sz: isize) (rd r1: ireg)                                    (**r count leading zero bits *)
-  | Prev (sz: isize) (rd r1: ireg)                                    (**r reverse bytes *)
-  | Prev16 (sz: isize) (rd r1: ireg)                                  (**r reverse bytes in each 16-bit word *)
-  (** Conditional data processing *)
-  | Pcsel (rd: ireg) (r1 r2: ireg) (c: testcond)                      (**r int conditional move *)
-  | Pcset (rd: ireg) (c: testcond)                                    (**r set to 1/0 if cond is true/false *)
-(*
-  | Pcsetm (rd: ireg) (c: testcond)                                   (**r set to -1/0 if cond is true/false *)
-*)
-  (** Integer multiply/divide *)
-  | Pmadd (sz: isize) (rd: ireg) (r1 r2: ireg) (r3: ireg0)            (**r multiply-add *)
-  | Pmsub (sz: isize) (rd: ireg) (r1 r2: ireg) (r3: ireg0)            (**r multiply-sub *)
-  | Psmulh (rd: ireg) (r1 r2: ireg)                                   (**r signed multiply high *)
-  | Pumulh (rd: ireg) (r1 r2: ireg)                                   (**r unsigned multiply high *)
-  | Psdiv (sz: isize) (rd: ireg) (r1 r2: ireg)                        (**r signed division *)
-  | Pudiv (sz: isize) (rd: ireg) (r1 r2: ireg)                        (**r unsigned division *)
-  (** Floating-point loads and stores *)
-  | Pldrs (rd: freg) (a: addressing)                                  (**r load float32 (single precision) *)
-  | Pldrd (rd: freg) (a: addressing)                                  (**r load float64 (double precision) *)
-  | Pldrd_a (rd: freg) (a: addressing)                                (**r load float64 as any64 *)
-  | Pstrs (rs: freg) (a: addressing)                                  (**r store float32 *)
-  | Pstrd (rs: freg) (a: addressing)                                  (**r store float64 *)
-  | Pstrd_a (rs: freg) (a: addressing)                                (**r store float64 as any64 *)
-  (** Floating-point move *)
-  | Pfmov (rd r1: freg)
-  | Pfmovimms (rd: freg) (f: float32)                                 (**r load float32 constant *)
-  | Pfmovimmd (rd: freg) (f: float)                                   (**r load float64 constant *)
-  | Pfmovi (fsz: fsize) (rd: freg) (r1: ireg0)                        (**r copy int reg to FP reg *)
-  (** Floating-point conversions *)
-  | Pfcvtds (rd r1: freg)                                             (**r convert float32 to float64 *)
-  | Pfcvtsd (rd r1: freg)                                             (**r convert float64 to float32 *)
-  | Pfcvtzs (isz: isize) (fsz: fsize) (rd: ireg) (r1: freg)           (**r convert float to signed int *)
-  | Pfcvtzu (isz: isize) (fsz: fsize) (rd: ireg) (r1: freg)           (**r convert float to unsigned int *)
-  | Pscvtf (fsz: fsize) (isz: isize) (rd: freg) (r1: ireg)            (**r convert signed int to float *)
-  | Pucvtf (fsz: fsize) (isz: isize) (rd: freg) (r1: ireg)            (**r convert unsigned int to float *)
-  (** Floating-point arithmetic *)
-  | Pfabs (sz: fsize) (rd r1: freg)                                   (**r absolute value *)
-  | Pfneg (sz: fsize) (rd r1: freg)                                   (**r negation *)
-  | Pfsqrt (sz: fsize) (rd r1: freg)                                  (**r square root *)
-  | Pfadd (sz: fsize) (rd r1 r2: freg)                                (**r addition *)
-  | Pfdiv (sz: fsize) (rd r1 r2: freg)                                (**r division *)
-  | Pfmul (sz: fsize) (rd r1 r2: freg)                                (**r multiplication *)
-  | Pfnmul (sz: fsize) (rd r1 r2: freg)                               (**r multiply-negate *)
-  | Pfsub (sz: fsize) (rd r1 r2: freg)                                (**r subtraction *)
-  | Pfmadd (sz: fsize) (rd r1 r2 r3: freg)                            (**r [rd = r3 + r1 * r2] *)
-  | Pfmsub (sz: fsize) (rd r1 r2 r3: freg)                            (**r [rd = r3 - r1 * r2] *)
-  | Pfnmadd (sz: fsize) (rd r1 r2 r3: freg)                           (**r [rd = - r3 - r1 * r2] *)
-  | Pfnmsub (sz: fsize) (rd r1 r2 r3: freg)                           (**r [rd = - r3 + r1 * r2] *)
-  (** Floating-point comparison *)
-  | Pfcmp (sz: fsize) (r1 r2: freg)                                   (**r compare [r1] and [r2] *)
-  | Pfcmp0 (sz: fsize) (r1: freg)                                     (**r compare [r1] and [+0.0] *)
-  (** Floating-point conditional select *)
-  | Pfsel (rd r1 r2: freg) (cond: testcond)
-  (** Pseudo-instructions *)
-  | Pallocframe (sz: Z) (linkofs: ptrofs)                             (**r allocate new stack frame *)
-  | Pfreeframe (sz: Z) (linkofs: ptrofs)                              (**r deallocate stack frame and restore previous frame *)
-  | Plabel (lbl: label)                                               (**r define a code label *)
-  | Ploadsymbol (rd: ireg) (id: ident)                                (**r load the address of [id] *)
-  | Pcvtsw2x (rd: ireg) (r1: ireg)                                    (**r sign-extend 32-bit int to 64-bit *)
-  | Pcvtuw2x (rd: ireg) (r1: ireg)                                    (**r zero-extend 32-bit int to 64-bit *)
-  | Pcvtx2w (rd: ireg)                                                (**r retype a 64-bit int as a 32-bit int *)
-  | Pbtbl (r1: ireg) (tbl: list label)                                (**r N-way branch through a jump table *)
-  | Pbuiltin (ef: external_function)
-             (args: list (builtin_arg preg)) (res: builtin_res preg)  (**r built-in function (pseudo) *)
-  | Pnop                                                              (**r no operation *)
-  | Pcfi_adjust (ofs: int)                                            (**r .cfi_adjust debug directive *)
-  | Pcfi_rel_offset (ofs: int)                                        (**r .cfi_rel_offset debug directive *)
-.
-*)
-
-
 (** * Operational semantics *)
 
 (** See "Parameters" of the same names in Asm.v *)
@@ -1069,458 +925,6 @@ Definition exec_basic (b: basic) (rs: regset) (m: mem): outcome :=
   | Pnop => Next rs m
   end.
 
-(* TODO: ORIGINAL EXECUTION OF INSTRUCTIONS THAT NEEDS TO BE ADAPTED !
-
-(** 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
-  (** Branches *)
-  | Pb lbl =>
-      goto_label f lbl rs m
-  | Pbc cond lbl =>
-      match eval_testcond cond rs with
-      | Some true => goto_label f lbl rs m
-      | Some false => Next (nextinstr rs) m
-      | None => Stuck
-      end
-  | Pbl id sg =>
-      Next (rs#RA <- (Val.offset_ptr rs#PC Ptrofs.one) #PC <- (Genv.symbol_address ge id Ptrofs.zero)) m
-  | Pbs id sg =>
-      Next (rs#PC <- (Genv.symbol_address ge id Ptrofs.zero)) m
-  | Pblr r sg =>
-      Next (rs#RA <- (Val.offset_ptr rs#PC Ptrofs.one) #PC <- (rs#r)) m
-  | Pbr r sg =>
-      Next (rs#PC <- (rs#r)) m
-  | Pret r =>
-      Next (rs#PC <- (rs#r)) m
-  | Pcbnz sz r lbl =>
-      match eval_testzero sz rs#r m 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
-      | Some true => goto_label f lbl rs m
-      | Some false => Next (nextinstr rs) m
-      | None => Stuck
-      end
-  | Ptbnz sz r n lbl =>
-      match eval_testbit sz rs#r n with
-      | Some true => goto_label f lbl rs m
-      | Some false => Next (nextinstr rs) m
-      | None => Stuck
-      end
-  | Ptbz sz r n lbl =>
-      match eval_testbit sz rs#r n with
-      | Some true => Next (nextinstr rs) m
-      | Some false => goto_label f lbl rs m
-      | None => Stuck
-      end
-  (** Memory loads and stores *)
-  | Pldrw rd a =>
-      exec_load Mint32 (fun v => v) a rd rs m
-  | Pldrw_a rd a =>
-      exec_load Many32 (fun v => v) a rd rs m
-  | Pldrx rd a =>
-      exec_load Mint64 (fun v => v) a rd rs m
-  | Pldrx_a rd a =>
-      exec_load Many64 (fun v => v) a rd rs m
-  | Pldrb W rd a =>
-      exec_load Mint8unsigned (fun v => v) a rd rs m
-  | Pldrb X rd a =>
-      exec_load Mint8unsigned Val.longofintu a rd rs m
-  | Pldrsb W rd a =>
-      exec_load Mint8signed (fun v => v) a rd rs m
-  | Pldrsb X rd a =>
-      exec_load Mint8signed Val.longofint a rd rs m
-  | Pldrh W rd a =>
-      exec_load Mint16unsigned (fun v => v) a rd rs m
-  | Pldrh X rd a =>
-      exec_load Mint16unsigned Val.longofintu a rd rs m
-  | Pldrsh W rd a =>
-      exec_load Mint16signed (fun v => v) a rd rs m
-  | Pldrsh X rd a =>
-      exec_load Mint16signed Val.longofint a rd rs m
-  | Pldrzw rd a =>
-      exec_load Mint32 Val.longofintu a rd rs m
-  | Pldrsw rd a =>
-      exec_load Mint32 Val.longofint a rd rs m
-  | Pstrw r a =>
-      exec_store Mint32 a rs#r rs m
-  | Pstrw_a r a =>
-      exec_store Many32 a rs#r rs m
-  | Pstrx r a =>
-      exec_store Mint64 a rs#r rs m
-  | Pstrx_a r a =>
-      exec_store Many64 a rs#r rs m
-  | Pstrb r a =>
-      exec_store Mint8unsigned a rs#r rs m
-  | Pstrh r a =>
-      exec_store Mint16unsigned a rs#r rs m
-  (** Integer arithmetic, immediate *)
-  | Paddimm W rd r1 n =>
-      Next (nextinstr (rs#rd <- (Val.add rs#r1 (Vint (Int.repr n))))) m
-  | Paddimm X rd r1 n =>
-      Next (nextinstr (rs#rd <- (Val.addl rs#r1 (Vlong (Int64.repr n))))) m
-  | Psubimm W rd r1 n =>
-      Next (nextinstr (rs#rd <- (Val.sub rs#r1 (Vint (Int.repr n))))) m
-  | 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
-  | Pcmpimm X r1 n =>
-      Next (nextinstr (compare_long rs rs#r1 (Vlong (Int64.repr n)) m)) m
-  | Pcmnimm W r1 n =>
-      Next (nextinstr (compare_int rs rs#r1 (Vint (Int.neg (Int.repr n))) m)) m
-  | Pcmnimm X r1 n =>
-      Next (nextinstr (compare_long rs rs#r1 (Vlong (Int64.neg (Int64.repr n))) m)) m
-  (** Move integer register *)
-  | Pmov rd r1 =>
-      Next (nextinstr (rs#rd <- (rs#r1))) m
-  (** Logical, immediate *)
-  | Pandimm W rd r1 n =>
-      Next (nextinstr (rs#rd <- (Val.and rs##r1 (Vint (Int.repr n))))) m
-  | Pandimm X rd r1 n =>
-      Next (nextinstr (rs#rd <- (Val.andl rs###r1 (Vlong (Int64.repr n))))) m
-  | Peorimm W rd r1 n =>
-      Next (nextinstr (rs#rd <- (Val.xor rs##r1 (Vint (Int.repr n))))) m
-  | Peorimm X rd r1 n =>
-      Next (nextinstr (rs#rd <- (Val.xorl rs###r1 (Vlong (Int64.repr n))))) m
-  | Porrimm W rd r1 n =>
-      Next (nextinstr (rs#rd <- (Val.or rs##r1 (Vint (Int.repr n))))) m
-  | 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
-  | Ptstimm X r1 n =>
-      Next (nextinstr (compare_long rs (Val.andl rs#r1 (Vlong (Int64.repr n))) (Vlong Int64.zero) m)) m
-  (** Move wide immediate *)
-  | Pmovz W rd n pos =>
-      Next (nextinstr (rs#rd <- (Vint (Int.repr (Z.shiftl n pos))))) m
-  | Pmovz X rd n pos =>
-      Next (nextinstr (rs#rd <- (Vlong (Int64.repr (Z.shiftl n pos))))) m
-  | Pmovn W rd n pos =>
-      Next (nextinstr (rs#rd <- (Vint (Int.repr (Z.lnot (Z.shiftl n pos)))))) m
-  | Pmovn X rd n pos =>
-      Next (nextinstr (rs#rd <- (Vlong (Int64.repr (Z.lnot (Z.shiftl n pos)))))) m
-  | Pmovk W rd n pos =>
-      Next (nextinstr (rs#rd <- (insert_in_int rs#rd n pos 16))) m
-  | Pmovk X rd n pos =>
-      Next (nextinstr (rs#rd <- (insert_in_long rs#rd n pos 16))) m
-  (** PC-relative addressing *)
-  | Padrp rd id ofs =>
-      Next (nextinstr (rs#rd <- (symbol_high ge id ofs))) m
-  | Paddadr rd r1 id ofs =>
-      Next (nextinstr (rs#rd <- (Val.addl rs#r1 (symbol_low ge id ofs)))) m
-  (** Bit-field operations *)
-  | Psbfiz W rd r1 r s =>
-      Next (nextinstr (rs#rd <- (Val.shl (Val.sign_ext s rs#r1) (Vint r)))) m
-  | Psbfiz X rd r1 r s =>
-      Next (nextinstr (rs#rd <- (Val.shll (Val.sign_ext_l s rs#r1) (Vint r)))) m
-  | Psbfx W rd r1 r s =>
-      Next (nextinstr (rs#rd <- (Val.sign_ext s (Val.shr rs#r1 (Vint r))))) m
-  | Psbfx X rd r1 r s =>
-      Next (nextinstr (rs#rd <- (Val.sign_ext_l s (Val.shrl rs#r1 (Vint r))))) m
-  | Pubfiz W rd r1 r s =>
-      Next (nextinstr (rs#rd <- (Val.shl (Val.zero_ext s rs#r1) (Vint r)))) m
-  | Pubfiz X rd r1 r s =>
-      Next (nextinstr (rs#rd <- (Val.shll (Val.zero_ext_l s rs#r1) (Vint r)))) m
-  | Pubfx W rd r1 r s =>
-      Next (nextinstr (rs#rd <- (Val.zero_ext s (Val.shru rs#r1 (Vint r))))) m
-  | Pubfx X rd r1 r s =>
-      Next (nextinstr (rs#rd <- (Val.zero_ext_l s (Val.shrlu rs#r1 (Vint r))))) m
-  (** Integer arithmetic, shifted register *)
-  | Padd W rd r1 r2 s =>
-      Next (nextinstr (rs#rd <- (Val.add rs##r1 (eval_shift_op_int rs#r2 s)))) m
-  | Padd X rd r1 r2 s =>
-      Next (nextinstr (rs#rd <- (Val.addl rs###r1 (eval_shift_op_long rs#r2 s)))) m
-  | Psub W rd r1 r2 s =>
-      Next (nextinstr (rs#rd <- (Val.sub rs##r1 (eval_shift_op_int rs#r2 s)))) m
-  | 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
-  | Pcmp X r1 r2 s =>
-      Next (nextinstr (compare_long rs rs###r1 (eval_shift_op_long rs#r2 s) m)) m
-  | Pcmn W r1 r2 s =>
-      Next (nextinstr (compare_int rs rs##r1 (Val.neg (eval_shift_op_int rs#r2 s)) m)) m
-  | Pcmn X r1 r2 s =>
-      Next (nextinstr (compare_long rs rs###r1 (Val.negl (eval_shift_op_long rs#r2 s)) m)) 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
-  | Pcmnext r1 r2 x =>
-      Next (nextinstr (compare_long rs rs#r1 (Val.negl (eval_extend rs#r2 x)) m)) 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
-  | Pand X rd r1 r2 s =>
-      Next (nextinstr (rs#rd <- (Val.andl rs###r1 (eval_shift_op_long rs#r2 s)))) m
-  | Pbic W rd r1 r2 s =>
-      Next (nextinstr (rs#rd <- (Val.and rs##r1 (Val.notint (eval_shift_op_int rs#r2 s))))) m
-  | Pbic X rd r1 r2 s =>
-      Next (nextinstr (rs#rd <- (Val.andl rs###r1 (Val.notl (eval_shift_op_long rs#r2 s))))) m
-  | Peon W rd r1 r2 s =>
-      Next (nextinstr (rs#rd <- (Val.xor rs##r1 (Val.notint (eval_shift_op_int rs#r2 s))))) m
-  | Peon X rd r1 r2 s =>
-      Next (nextinstr (rs#rd <- (Val.xorl rs###r1 (Val.notl (eval_shift_op_long rs#r2 s))))) m
-  | Peor W rd r1 r2 s =>
-      Next (nextinstr (rs#rd <- (Val.xor rs##r1 (eval_shift_op_int rs#r2 s)))) m
-  | Peor X rd r1 r2 s =>
-      Next (nextinstr (rs#rd <- (Val.xorl rs###r1 (eval_shift_op_long rs#r2 s)))) m
-  | Porr W rd r1 r2 s =>
-      Next (nextinstr (rs#rd <- (Val.or rs##r1 (eval_shift_op_int rs#r2 s)))) m
-  | Porr X rd r1 r2 s =>
-      Next (nextinstr (rs#rd <- (Val.orl rs###r1 (eval_shift_op_long rs#r2 s)))) m
-  | Porn W rd r1 r2 s =>
-      Next (nextinstr (rs#rd <- (Val.or rs##r1 (Val.notint (eval_shift_op_int rs#r2 s))))) m
-  | 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
-  | 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
-  (** Variable shifts *)
-  | Pasrv W rd r1 r2 =>
-      Next (nextinstr (rs#rd <- (Val.shr rs#r1 rs#r2))) m
-  | Pasrv X rd r1 r2 =>
-      Next (nextinstr (rs#rd <- (Val.shrl rs#r1 rs#r2))) m
-  | Plslv W rd r1 r2 =>
-      Next (nextinstr (rs#rd <- (Val.shl rs#r1 rs#r2))) m
-  | Plslv X rd r1 r2 =>
-      Next (nextinstr (rs#rd <- (Val.shll rs#r1 rs#r2))) m
-  | Plsrv W rd r1 r2 =>
-      Next (nextinstr (rs#rd <- (Val.shru rs#r1 rs#r2))) m
-  | Plsrv X rd r1 r2 =>
-      Next (nextinstr (rs#rd <- (Val.shrlu rs#r1 rs#r2))) m
-  | Prorv W rd r1 r2 =>
-      Next (nextinstr (rs#rd <- (Val.ror rs#r1 rs#r2))) m
-  | Prorv X rd r1 r2 =>
-      Next (nextinstr (rs#rd <- (Val.rorl rs#r1 rs#r2))) m
-  (** Conditional data processing *)
-  | Pcsel rd r1 r2 cond =>
-      let v :=
-        match eval_testcond cond rs with
-        | Some true => rs#r1
-        | Some false => rs#r2
-        | None => Vundef
-        end in
-      Next (nextinstr (rs#rd <- v)) m
-  | Pcset rd cond =>
-      let v :=
-        match cond rs with
-        | Some true => Vint Int.one
-        | Some false => Vint Int.zero
-        | None => Vundef
-        end in
-      Next (nextinstr (rs#rd <- v)) m
-  (** Integer multiply/divide *)
-  | Pmadd W rd r1 r2 r3 =>
-      Next (nextinstr (rs#rd <- (Val.add rs##r3 (Val.mul rs#r1 rs#r2)))) m
-  | Pmadd X rd r1 r2 r3 =>
-      Next (nextinstr (rs#rd <- (Val.addl rs###r3 (Val.mull rs#r1 rs#r2)))) m
-  | Pmsub W rd r1 r2 r3 =>
-      Next (nextinstr (rs#rd <- (Val.sub rs##r3 (Val.mul rs#r1 rs#r2)))) m
-  | Pmsub X rd r1 r2 r3 =>
-      Next (nextinstr (rs#rd <- (Val.subl rs###r3 (Val.mull rs#r1 rs#r2)))) m
-  | Psmulh rd r1 r2 =>
-      Next (nextinstr (rs#rd <- (Val.mullhs rs#r1 rs#r2))) m
-  | Pumulh rd r1 r2 =>
-      Next (nextinstr (rs#rd <- (Val.mullhu rs#r1 rs#r2))) m
-  | Psdiv W rd r1 r2 =>
-      Next (nextinstr (rs#rd <- (Val.maketotal (Val.divs rs#r1 rs#r2)))) m
-  | Psdiv X rd r1 r2 =>
-      Next (nextinstr (rs#rd <- (Val.maketotal (Val.divls rs#r1 rs#r2)))) m
-  | Pudiv W rd r1 r2 =>
-      Next (nextinstr (rs#rd <- (Val.maketotal (Val.divu rs#r1 rs#r2)))) m
-  | Pudiv X rd r1 r2 =>
-      Next (nextinstr (rs#rd <- (Val.maketotal (Val.divlu rs#r1 rs#r2)))) m
-  (** Floating-point loads and stores *)
-  | Pldrs rd a =>
-      exec_load Mfloat32 (fun v => v) a rd rs m
-  | Pldrd rd a =>
-      exec_load Mfloat64 (fun v => v) a rd rs m
-  | Pldrd_a rd a =>
-      exec_load Many64 (fun v => v) a rd rs m
-  | Pstrs r a =>
-      exec_store Mfloat32 a rs#r rs m
-  | Pstrd r a =>
-      exec_store Mfloat64 a rs#r rs m
-  | Pstrd_a r a =>
-      exec_store Many64 a rs#r rs m
-  (** Floating-point move *)
-  | Pfmov rd r1 =>
-      Next (nextinstr (rs#rd <- (rs#r1))) m
-  | Pfmovimms rd f =>
-      Next (nextinstr (rs#rd <- (Vsingle f))) m
-  | Pfmovimmd rd f =>
-      Next (nextinstr (rs#rd <- (Vfloat f))) m
-  | Pfmovi S rd r1 =>
-      Next (nextinstr (rs#rd <- (float32_of_bits rs##r1))) m
-  | Pfmovi D rd r1 =>
-      Next (nextinstr (rs#rd <- (float64_of_bits rs###r1))) m
-  (** Floating-point conversions *)
-  | Pfcvtds rd r1 =>
-      Next (nextinstr (rs#rd <- (Val.floatofsingle rs#r1))) m
-  | Pfcvtsd rd r1 =>
-      Next (nextinstr (rs#rd <- (Val.singleoffloat rs#r1))) m
-  | Pfcvtzs W S rd r1 =>
-      Next (nextinstr (rs#rd <- (Val.maketotal (Val.intofsingle rs#r1)))) m
-  | Pfcvtzs W D rd r1 =>
-      Next (nextinstr (rs#rd <- (Val.maketotal (Val.intoffloat rs#r1)))) m
-  | Pfcvtzs X S rd r1 =>
-      Next (nextinstr (rs#rd <- (Val.maketotal (Val.longofsingle rs#r1)))) m
-  | Pfcvtzs X D rd r1 =>
-      Next (nextinstr (rs#rd <- (Val.maketotal (Val.longoffloat rs#r1)))) m
-  | Pfcvtzu W S rd r1 =>
-      Next (nextinstr (rs#rd <- (Val.maketotal (Val.intuofsingle rs#r1)))) m
-  | Pfcvtzu W D rd r1 =>
-      Next (nextinstr (rs#rd <- (Val.maketotal (Val.intuoffloat rs#r1)))) m
-  | Pfcvtzu X S rd r1 =>
-      Next (nextinstr (rs#rd <- (Val.maketotal (Val.longuofsingle rs#r1)))) m
-  | Pfcvtzu X D rd r1 =>
-      Next (nextinstr (rs#rd <- (Val.maketotal (Val.longuoffloat rs#r1)))) m
-  | Pscvtf S W rd r1 =>
-      Next (nextinstr (rs#rd <- (Val.maketotal (Val.singleofint rs#r1)))) m
-  | Pscvtf D W rd r1 =>
-      Next (nextinstr (rs#rd <- (Val.maketotal (Val.floatofint rs#r1)))) m
-  | Pscvtf S X rd r1 =>
-      Next (nextinstr (rs#rd <- (Val.maketotal (Val.singleoflong rs#r1)))) m
-  | Pscvtf D X rd r1 =>
-      Next (nextinstr (rs#rd <- (Val.maketotal (Val.floatoflong rs#r1)))) m
-  | Pucvtf S W rd r1 =>
-      Next (nextinstr (rs#rd <- (Val.maketotal (Val.singleofintu rs#r1)))) m
-  | Pucvtf D W rd r1 =>
-      Next (nextinstr (rs#rd <- (Val.maketotal (Val.floatofintu rs#r1)))) m
-  | Pucvtf S X rd r1 =>
-      Next (nextinstr (rs#rd <- (Val.maketotal (Val.singleoflongu rs#r1)))) m
-  | Pucvtf D X rd r1 =>
-      Next (nextinstr (rs#rd <- (Val.maketotal (Val.floatoflongu rs#r1)))) m
-  (** Floating-point arithmetic *)
-  | Pfabs S rd r1 =>
-      Next (nextinstr (rs#rd <- (Val.absfs rs#r1))) m
-  | Pfabs D rd r1 =>
-      Next (nextinstr (rs#rd <- (Val.absf rs#r1))) m
-  | Pfneg S rd r1 =>
-      Next (nextinstr (rs#rd <- (Val.negfs rs#r1))) m
-  | Pfneg D rd r1 =>
-      Next (nextinstr (rs#rd <- (Val.negf rs#r1))) m
-  | Pfadd S rd r1 r2 =>
-      Next (nextinstr (rs#rd <- (Val.addfs rs#r1 rs#r2))) m
-  | Pfadd D rd r1 r2 =>
-      Next (nextinstr (rs#rd <- (Val.addf rs#r1 rs#r2))) m
-  | Pfdiv S rd r1 r2 =>
-      Next (nextinstr (rs#rd <- (Val.divfs rs#r1 rs#r2))) m
-  | Pfdiv D rd r1 r2 =>
-      Next (nextinstr (rs#rd <- (Val.divf rs#r1 rs#r2))) m
-  | Pfmul S rd r1 r2 =>
-      Next (nextinstr (rs#rd <- (Val.mulfs rs#r1 rs#r2))) m
-  | Pfmul D rd r1 r2 =>
-      Next (nextinstr (rs#rd <- (Val.mulf rs#r1 rs#r2))) m
-  | Pfnmul S rd r1 r2 =>
-      Next (nextinstr (rs#rd <- (Val.negfs (Val.mulfs rs#r1 rs#r2)))) m
-  | Pfnmul D rd r1 r2 =>
-      Next (nextinstr (rs#rd <- (Val.negf (Val.mulf rs#r1 rs#r2)))) m
-  | Pfsub S rd r1 r2 =>
-      Next (nextinstr (rs#rd <- (Val.subfs rs#r1 rs#r2))) m
-  | Pfsub D rd r1 r2 =>
-      Next (nextinstr (rs#rd <- (Val.subf rs#r1 rs#r2))) m
-  (** Floating-point comparison *)
-  | Pfcmp S r1 r2 =>
-      Next (nextinstr (compare_single rs rs#r1 rs#r2)) m
-  | Pfcmp D r1 r2 =>
-      Next (nextinstr (compare_float rs rs#r1 rs#r2)) m
-  | Pfcmp0 S r1 =>
-      Next (nextinstr (compare_single rs rs#r1 (Vsingle Float32.zero))) m
-  | Pfcmp0 D r1 =>
-      Next (nextinstr (compare_float rs rs#r1 (Vfloat Float.zero))) m
-  (** Floating-point conditional select *)
-  | Pfsel rd r1 r2 cond =>
-      let v :=
-        match eval_testcond cond rs with
-        | Some true => rs#r1
-        | Some false => rs#r2
-        | None => Vundef
-        end in
-      Next (nextinstr (rs#rd <- v)) m
-  (** Pseudo-instructions *)
-  | Pallocframe sz pos =>
-      let (m1, stk) := Mem.alloc m 0 sz in
-      let sp := (Vptr stk Ptrofs.zero) in
-      match Mem.storev Mint64 m1 (Val.offset_ptr sp pos) rs#SP with
-      | None => Stuck
-      | Some m2 => Next (nextinstr (rs #X29 <- (rs#SP) #SP <- sp #X16 <- Vundef)) m2
-      end
-  | Pfreeframe sz pos =>
-      match Mem.loadv Mint64 m (Val.offset_ptr rs#SP pos) with
-      | None => Stuck
-      | Some v =>
-          match rs#SP with
-          | Vptr stk ofs =>
-              match Mem.free m stk 0 sz with
-              | None => Stuck
-              | Some m' => Next (nextinstr (rs#SP <- v #X16 <- Vundef)) m'
-              end
-          | _ => Stuck
-          end
-      end
-  | Plabel lbl =>
-      Next (nextinstr rs) m
-  | Ploadsymbol rd id =>
-      Next (nextinstr (rs#rd <- (Genv.symbol_address ge id Ptrofs.zero))) m
-  | Pcvtsw2x rd r1 =>
-      Next (nextinstr (rs#rd <- (Val.longofint rs#r1))) m
-  | Pcvtuw2x rd r1 =>
-      Next (nextinstr (rs#rd <- (Val.longofintu rs#r1))) m
-  | Pcvtx2w rd =>
-      Next (nextinstr (rs#rd <- (Val.loword rs#rd))) m
-  | Pbtbl r tbl =>
-      match (rs#X16 <- Vundef)#r with
-      | Vint n =>
-          match list_nth_z tbl (Int.unsigned n) with
-          | None => Stuck
-          | Some lbl => goto_label f lbl (rs#X16 <- Vundef #X17 <- Vundef) m
-          end
-      | _ => Stuck
-      end
-  | Pbuiltin ef args res => Stuck    (**r treated specially below *)
-  (** The following instructions and directives are not generated directly
-      by Asmgen, so we do not model them. *)
-  | Pldp _ _ _
-  | Pstp _ _ _
-  | Pcls _ _ _
-  | Pclz _ _ _
-  | Prev _ _ _
-  | Prev16 _ _ _
-  | Pfsqrt _ _ _
-  | Pfmadd _ _ _ _ _
-  | Pfmsub _ _ _ _ _
-  | Pfnmadd _ _ _ _ _
-  | Pfnmsub _ _ _ _ _
-  | Pnop
-  | Pcfi_adjust _
-  | Pcfi_rel_offset _ =>
-      Stuck
-  end.
-*)
-
 (**  execution of the body of a bblock *)
 Fixpoint exec_body (body: list basic) (rs: regset) (m: mem): outcome :=
   match body with
diff --git a/aarch64/Asmblockgen.v b/aarch64/Asmblockgen.v
index 137b5871..fbbf7507 100644
--- a/aarch64/Asmblockgen.v
+++ b/aarch64/Asmblockgen.v
@@ -157,18 +157,6 @@ Program Definition insert_basic (bi: basic) (k:bblocks): bblocks :=
 
 Notation "bi ::b k" := (insert_basic bi k) (at level 49, right associativity).
 
-(* TODO: Coercions to move in Asmblock ? *)
-Coercion PArithP: arith_p >-> Funclass.
-Coercion PArithPP: arith_pp >-> Funclass.
-Coercion PArithPPP: arith_ppp >-> Funclass.
-Coercion PArithRR0: arith_rr0 >-> Funclass.
-Coercion PArithRR0R: arith_rr0r >-> Funclass.
-Coercion PArithARRRR0: arith_arrrr0 >-> Funclass.
-Coercion PArithComparisonP: arith_comparison_p >-> Funclass.
-Coercion PArithComparisonPP: arith_comparison_pp >-> Funclass.
-Coercion PArithComparisonR0R: arith_comparison_r0r >-> Funclass.
-Coercion PArith: ar_instruction >-> basic.
-
 (* NB: this notation helps the Coq typechecker to infer coercion [PArith] in [bcode] expressions *)
 (** Alignment check for symbols *)
 Notation "i ::bi k" := (cons (A:=basic) i k) (at level 49, right associativity).
diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index eac406a1..793d94f9 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -807,7 +807,6 @@ Proof.
   - destruct fsz; rewrite <- BASIC; rewrite Pregmap.gso; try (discriminate || reflexivity).
 Qed.
 
-(* TODO *)
 Lemma exec_basic_dont_move_PC bi rs m rs' m': forall
   (BASIC: exec_basic lk ge bi rs m = Next rs' m'),
   rs PC = rs' PC.
@@ -1660,7 +1659,6 @@ Proof.
     + destruct H.
 Qed.
 
-(* TODO *)
 Lemma no_label_in_basic_inst: forall a lbl x,
   basic_to_instruction a = OK x -> Asm.is_label lbl x = false.
 Proof.
diff --git a/aarch64/Peephole.v b/aarch64/Peephole.v
index a1bb6c6c..54670708 100644
--- a/aarch64/Peephole.v
+++ b/aarch64/Peephole.v
@@ -160,7 +160,6 @@ Fixpoint pair_rep (insns : list basic) : list basic :=
   end.
 
 Definition optimize_body (insns : list basic) :=
-  (* TODO ADD A FLAG TO ENABLE PEEPHOLE *)
   if Compopts.optim_coalesce_mem tt
   then (pair_rep insns)
   else insns.