Asmblock -> Asm presque fini.. erreur sur driver/Compiler.v

8 files changed, 753 insertions, 3391 deletions

diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index df394ecf..d71304fa 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -1,1244 +1,451 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              The Compcert verified compiler                         *)
-(*                                                                     *)
-(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
-(*           Prashanth Mundkur, SRI International                      *)
-(*                                                                     *)
-(*  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.     *)
-(*                                                                     *)
-(*  The contributions by Prashanth Mundkur are reused and adapted      *)
-(*  under the terms of a Contributor License Agreement between         *)
-(*  SRI International and INRIA.                                       *)
-(*                                                                     *)
-(* *********************************************************************)
-
-(** Abstract syntax and semantics for K1c assembly language. *)
-
-Require Import Coqlib.
-Require Import Maps.
-Require Import AST.
-Require Import Integers.
-Require Import Floats.
-Require Import Values.
-Require Import Memory.
-Require Import Events.
-Require Import Globalenvs.
-Require Import Smallstep.
-Require Import Locations.
-Require Stacklayout.
-Require Import Conventions.
-
-(** * Abstract syntax *)
-
-(** General Purpose registers. *)
-
-Inductive gpreg: Type :=
-  | GPR0:  gpreg | GPR1:  gpreg | GPR2:  gpreg | GPR3:  gpreg | GPR4:  gpreg
-  | GPR5:  gpreg | GPR6:  gpreg | GPR7:  gpreg | GPR8:  gpreg | GPR9:  gpreg
-  | GPR10: gpreg | GPR11: gpreg | GPR12: gpreg | GPR13: gpreg | GPR14: gpreg
-  | GPR15: gpreg | GPR16: gpreg | GPR17: gpreg | GPR18: gpreg | GPR19: gpreg
-  | GPR20: gpreg | GPR21: gpreg | GPR22: gpreg | GPR23: gpreg | GPR24: gpreg
-  | GPR25: gpreg | GPR26: gpreg | GPR27: gpreg | GPR28: gpreg | GPR29: gpreg
-  | GPR30: gpreg | GPR31: gpreg | GPR32: gpreg | GPR33: gpreg | GPR34: gpreg
-  | GPR35: gpreg | GPR36: gpreg | GPR37: gpreg | GPR38: gpreg | GPR39: gpreg
-  | GPR40: gpreg | GPR41: gpreg | GPR42: gpreg | GPR43: gpreg | GPR44: gpreg
-  | GPR45: gpreg | GPR46: gpreg | GPR47: gpreg | GPR48: gpreg | GPR49: gpreg
-  | GPR50: gpreg | GPR51: gpreg | GPR52: gpreg | GPR53: gpreg | GPR54: gpreg
-  | GPR55: gpreg | GPR56: gpreg | GPR57: gpreg | GPR58: gpreg | GPR59: gpreg
-  | GPR60: gpreg | GPR61: gpreg | GPR62: gpreg | GPR63: gpreg.
-
-Definition ireg := gpreg.
-Definition freg := gpreg.
-
-Lemma ireg_eq: forall (x y: ireg), {x=y} + {x<>y}.
-Proof. decide equality. Defined.
-
-Lemma freg_eq: forall (x y: freg), {x=y} + {x<>y}.
-Proof. decide equality. Defined.
-
-(** We model the following registers of the RISC-V architecture. *)
-
-Inductive preg: Type :=
-  | IR: gpreg -> preg                   (**r integer registers *)
-  | FR: gpreg -> preg                   (**r float registers   *)
-  | RA: preg                            (**r return address    *)
-  | PC: preg.                           (**r program counter   *)
-
-Coercion IR: gpreg >-> preg.
-Coercion FR: gpreg >-> preg.
-
-Lemma preg_eq: forall (x y: preg), {x=y} + {x<>y}.
-Proof. decide equality. apply ireg_eq. apply freg_eq. Defined.
-
-Module PregEq.
-  Definition t  := preg.
-  Definition eq := preg_eq.
-End PregEq.
-
-Module Pregmap := EMap(PregEq).
-
-(** Conventional names for stack pointer ([SP]) and return address ([RA]). *)
-
-Notation "'SP'" := GPR12 (only parsing) : asm.
-Notation "'FP'" := GPR10 (only parsing) : asm.
-Notation "'RTMP'" := GPR31 (only parsing) : asm.
-
-Inductive btest: Type :=
-  | BTdnez                              (**r Double Not Equal to Zero *)
-  | BTdeqz                              (**r Double Equal to Zero *)
-  | BTdltz                              (**r Double Less Than Zero *)
-  | BTdgez                              (**r Double Greater Than or Equal to Zero *)
-  | BTdlez                              (**r Double Less Than or Equal to Zero *)
-  | BTdgtz                              (**r Double Greater Than Zero *)
-(*| BTodd                               (**r Odd (LSB Set) *)
-  | BTeven                              (**r Even (LSB Clear) *)
-*)| BTwnez                              (**r Word Not Equal to Zero *)
-  | BTweqz                              (**r Word Equal to Zero *)
-  | BTwltz                              (**r Word Less Than Zero *)
-  | BTwgez                              (**r Word Greater Than or Equal to Zero *)
-  | BTwlez                              (**r Word Less Than or Equal to Zero *)
-  | BTwgtz                              (**r Word Greater Than Zero *)
-  .
-
-Inductive itest: Type :=
-  | ITne                                (**r Not Equal *)
-  | ITeq                                (**r Equal *)
-  | ITlt                                (**r Less Than *)
-  | ITge                                (**r Greater Than or Equal *)
-  | ITle                                (**r Less Than or Equal *)
-  | ITgt                                (**r Greater Than *)
-  | ITneu                               (**r Unsigned Not Equal *)
-  | ITequ                               (**r Unsigned Equal *)
-  | ITltu                               (**r Less Than Unsigned *)
-  | ITgeu                               (**r Greater Than or Equal Unsigned *)
-  | ITleu                               (**r Less Than or Equal Unsigned *)
-  | ITgtu                               (**r Greater Than Unsigned *)
-  (* Not used yet *)
-  | ITall                               (**r All Bits Set in Mask *)
-  | ITnall                              (**r Not All Bits Set in Mask *)
-  | ITany                               (**r Any Bits Set in Mask *)
-  | ITnone                              (**r Not Any Bits Set in Mask *)
-  .
-
-(** Offsets for load and store instructions.  An offset is either an
-  immediate integer or the low part of a symbol. *)
-
-Inductive offset : Type :=
-  | Ofsimm (ofs: ptrofs)
-  | Ofslow (id: ident) (ofs: ptrofs).
-
-(** We model a subset of the K1c instruction set. In particular, we do not
-  support floats yet.
-
-  Although it is possible to use the 32-bits mode, for now we don't support it.
-
-  We follow a design close to the one used for the Risc-V port: one set of
-  pseudo-instructions for 32-bit integer arithmetic, with suffix W, another
-  set for 64-bit integer arithmetic, with suffix L.
-
-  When mapping to actual instructions, the OCaml code in TargetPrinter.ml
-  throws an error if we are not in 64-bits mode.
-*)
-
-Definition label := positive.
-
-(** A note on immediates: there are various constraints on immediate
-  operands to K1c instructions.  We do not attempt to capture these
-  restrictions in the abstract syntax nor in the semantics.  The
-  assembler will emit an error if immediate operands exceed the
-  representable range.  Of course, our K1c generator (file
-  [Asmgen]) is careful to respect this range. *)
-
-(** Instructions to be expanded *)
-Inductive ex_instruction : Type :=
-  (* Pseudo-instructions *)
-  | Pallocframe (sz: Z) (pos: ptrofs)               (**r allocate new stack frame *)
-  | Pfreeframe  (sz: Z) (pos: ptrofs)               (**r deallocate stack frame and restore previous frame *)
-  | Plabel  (lbl: label)                            (**r define a code label *)
-  | Ploadsymbol (rd: ireg) (id: ident) (ofs: ptrofs) (**r load the address of a symbol *)
-(*| Ploadsymbol_high (rd: ireg) (id: ident) (ofs: ptrofs) (**r load the high part of the address of a symbol *)
-  | Ploadli (rd: ireg) (i: int64)                   (**r load an immediate int64 *)
-  | Ploadfi (rd: freg) (f: float)                   (**r load an immediate float *)
-  | Ploadsi (rd: freg) (f: float32)                 (**r load an immediate single *)
-  | Pbtbl   (r: ireg)  (tbl: list label)            (**r N-way branch through a jump table *) *)
-  | Pbuiltin: external_function -> list (builtin_arg preg)
-              -> builtin_res preg -> ex_instruction   (**r built-in function (pseudo) *)
-  (* Instructions not generated by Asmgen (most likely result of AsmExpand) *)
-  | Pclzll (rd rs: ireg)
-  | Pstsud (rd rs1 rs2: ireg)
-.
-
-(** The pseudo-instructions are the following:
-
-- [Plabel]: define a code label at the current program point.
-
-- [Ploadsymbol]: load the address of a symbol in an integer register.
-  Expands to the [la] assembler pseudo-instruction, which does the right
-  thing even if we are in PIC mode.
-
-- [Ploadli rd ival]: load an immediate 64-bit integer into an integer
-  register rd.  Expands to a load from an address in the constant data section,
-  using the integer register x31 as temporary:
-<<
-        lui x31, %hi(lbl)
-        ld rd, %lo(lbl)(x31)
-lbl:
-        .quad ival
->>
-
-- [Ploadfi rd fval]: similar to [Ploadli] but loads a double FP constant fval
-  into a float register rd.
-
-- [Ploadsi rd fval]: similar to [Ploadli] but loads a singe FP constant fval
-  into a float register rd.
-
-- [Pallocframe sz pos]: in the formal semantics, this
-  pseudo-instruction allocates a memory block with bounds [0] and
-  [sz], stores the value of the stack pointer at offset [pos] in this
-  block, and sets the stack pointer to the address of the bottom of
-  this block.
-  In the printed ASM assembly code, this allocation is:
-<<
-        mv      x30, sp
-        sub     sp,  sp, #sz
-        sw      x30, #pos(sp)
->>
-  This cannot be expressed in our memory model, which does not reflect
-  the fact that stack frames are adjacent and allocated/freed
-  following a stack discipline.
-
-- [Pfreeframe sz pos]: in the formal semantics, this pseudo-instruction
-  reads the word at [pos] of the block pointed by the stack pointer,
-  frees this block, and sets the stack pointer to the value read.
-  In the printed ASM assembly code, this freeing is just an increment of [sp]:
-<<
-        add     sp,  sp, #sz
->>
-  Again, our memory model cannot comprehend that this operation
-  frees (logically) the current stack frame.
-
-- [Pbtbl reg table]: this is a N-way branch, implemented via a jump table
-  as follows:
-<<
-        la      x31, table
-        add     x31, x31, reg
-        jr      x31
-table:  .long   table[0], table[1], ...
->>
-  Note that [reg] contains 4 times the index of the desired table entry.
-
-- [Pseq rd rs1 rs2]: since unsigned comparisons have particular
-  semantics for pointers, we cannot encode equality directly using
-  xor/sub etc, which have only integer semantics.
-<<
-        xor     rd, rs1, rs2
-        sltiu   rd, rd, 1
->>
-  The [xor] is omitted if one of [rs1] and [rs2] is [x0].
-
-- [Psne rd rs1 rs2]: similarly for unsigned inequality.
-<<
-        xor     rd, rs1, rs2
-        sltu    rd, x0, rd
->>
-*)
-
-(** Control Flow instructions *)
-Inductive cf_instruction : Type :=
-  | Pget    (rd: ireg) (rs: preg)                   (**r get system register *)
-  | Pset    (rd: preg) (rs: ireg)                   (**r set system register *)
-  | Pret                                            (**r return *)
-  | Pcall   (l: label)                              (**r function call *)
-  (* Pgoto is for tailcalls, Pj_l is for jumping to a particular label *)
-  | Pgoto   (l: label)                              (**r goto *)
-  | Pj_l    (l: label)                              (**r jump to label *)
-  (* Conditional branches *)
-  | Pcb     (bt: btest) (r: ireg) (l: label)        (**r branch based on btest *)
-  | Pcbu    (bt: btest) (r: ireg) (l: label)        (**r branch based on btest with unsigned semantics *)
-.
-
-(** Loads **)
-Inductive ld_instruction : Type :=
-  | Plb     (rd: ireg) (ra: ireg) (ofs: offset)     (**r load byte *)
-  | Plbu    (rd: ireg) (ra: ireg) (ofs: offset)     (**r load byte unsigned *)
-  | Plh     (rd: ireg) (ra: ireg) (ofs: offset)     (**r load half word *)
-  | Plhu    (rd: ireg) (ra: ireg) (ofs: offset)     (**r load half word unsigned *)
-  | Plw     (rd: ireg) (ra: ireg) (ofs: offset)     (**r load int32 *)
-  | Plw_a   (rd: ireg) (ra: ireg) (ofs: offset)     (**r load any32 *)
-  | Pld     (rd: ireg) (ra: ireg) (ofs: offset)     (**r load int64 *)
-  | Pld_a   (rd: ireg) (ra: ireg) (ofs: offset)     (**r load any64 *)
-  | Pfls    (rd: freg) (ra: ireg) (ofs: offset)     (**r load float *)
-  | Pfld     (rd: freg) (ra: ireg) (ofs: offset)    (**r load 64-bit float *)
-.
-
-(** Stores **)
-Inductive st_instruction : Type :=
-  | Psb     (rs: ireg) (ra: ireg) (ofs: offset)     (**r store byte *)
-  | Psh     (rs: ireg) (ra: ireg) (ofs: offset)     (**r store half byte *)
-  | Psw     (rs: ireg) (ra: ireg) (ofs: offset)     (**r store int32 *)
-  | Psw_a   (rs: ireg) (ra: ireg) (ofs: offset)     (**r store any32 *)
-  | Psd     (rs: ireg) (ra: ireg) (ofs: offset)     (**r store int64 *)
-  | Psd_a   (rs: ireg) (ra: ireg) (ofs: offset)     (**r store any64 *)
-  | Pfss    (rs: freg) (ra: ireg) (ofs: offset)     (**r store float *)
-  | Pfsd     (rd: freg) (ra: ireg) (ofs: offset)    (**r store 64-bit float *)
-.
-
-(** Arithmetic instructions **)
-Inductive arith_name_r : Type :=
-  | Pcvtw2l                                         (**r Convert Word to Long *)
-.
-
-Inductive arith_name_rr : Type :=
-  | Pmv                                             (**r register move *)
-  | Pnegw                                           (**r negate word *)
-  | Pnegl                                           (**r negate long *)
-  | Pfnegd                                          (**r float negate double *)
-  | Pcvtl2w                                         (**r Convert Long to Word *)
-  | Pmvw2l                                          (**r Move Convert Word to Long *)
-.
-
-Inductive arith_name_ri32 : Type :=
-  | Pmake                                           (**r load immediate *)
-.
-
-Inductive arith_name_ri64 : Type :=
-  | Pmakel                                          (**r load immediate long *)
-.
-
-Inductive arith_name_rrr : Type :=
-  | Pcompw  (it: itest)                             (**r comparison word *)
-  | Pcompl  (it: itest)                             (**r comparison long *)
-
-  | Paddw                                           (**r add word *)
-  | Psubw                                           (**r sub word *)
-  | Pmulw                                           (**r mul word *)
-  | Pandw                                           (**r and word *)
-  | Porw                                            (**r or word *)
-  | Pxorw                                           (**r xor word *)
-  | Psraw                                           (**r shift right arithmetic word *)
-  | Psrlw                                           (**r shift right logical word *)
-  | Psllw                                           (**r shift left logical word *)
-
-  | Paddl                                           (**r add long *)
-  | Psubl                                           (**r sub long *)
-  | Pandl                                           (**r and long *)
-  | Porl                                            (**r or long *)
-  | Pxorl                                           (**r xor long *)
-  | Pmull                                           (**r mul long (low part) *)
-  | Pslll                                           (**r shift left logical long *)
-  | Psrll                                           (**r shift right logical long *)
-  | Psral                                           (**r shift right arithmetic long *)
-.
-
-Inductive arith_name_rri32 : Type :=
-  | Pcompiw (it: itest)                             (**r comparison imm word *)
-
-  | Paddiw                                          (**r add imm word *)
-  | Pandiw                                          (**r and imm word *)
-  | Poriw                                           (**r or imm word *)
-  | Pxoriw                                          (**r xor imm word *)
-  | Psraiw                                          (**r shift right arithmetic imm word *)
-  | Psrliw                                          (**r shift right logical imm word *)
-  | Pslliw                                          (**r shift left logical imm word *)
-
-  | Psllil                                          (**r shift left logical immediate long *)
-  | Psrlil                                          (**r shift right logical immediate long *)
-  | Psrail                                          (**r shift right arithmetic immediate long *)
-.
-
-Inductive arith_name_rri64 : Type :=
-  | Pcompil (it: itest)                             (**r comparison imm long *)
-  | Paddil                                          (**r add immediate long *) 
-  | Pandil                                          (**r and immediate long *) 
-  | Poril                                           (**r or immediate long *) 
-  | Pxoril                                          (**r xor immediate long *) 
-.
-
-Inductive ar_instruction : Type :=
-  | PArithR     (i: arith_name_r)     (rd: ireg)
-  | PArithRR    (i: arith_name_rr)    (rd rs: ireg)
-  | PArithRI32  (i: arith_name_ri32)  (rd: ireg) (imm: int)
-  | PArithRI64  (i: arith_name_ri64)  (rd: ireg) (imm: int64)
-  | PArithRRR   (i: arith_name_rrr)   (rd rs1 rs2: ireg)
-  | PArithRRI32 (i: arith_name_rri32) (rd rs: ireg) (imm: int)
-  | PArithRRI64 (i: arith_name_rri64) (rd rs: ireg) (imm: int64)
-.
-
-Coercion PArithR:       arith_name_r        >-> Funclass.
-Coercion PArithRR:      arith_name_rr       >-> Funclass.
-Coercion PArithRI32:    arith_name_ri32     >-> Funclass.
-Coercion PArithRI64:    arith_name_ri64     >-> Funclass.
-Coercion PArithRRR:     arith_name_rrr      >-> Funclass.
-Coercion PArithRRI32:   arith_name_rri32    >-> Funclass.
-Coercion PArithRRI64:   arith_name_rri64    >-> Funclass.
-
-(*| Pfence                                          (**r fence *)
-
-  (* floating point register move *)
-  | Pfmv     (rd: freg) (rs: freg)                  (**r move *)
-  | Pfmvxs   (rd: ireg) (rs: freg)                  (**r move FP single to integer register *)
-  | Pfmvxd   (rd: ireg) (rs: freg)                  (**r move FP double to integer register *)
-
-*)(* 32-bit (single-precision) floating point *)
-
-(*| Pfnegs   (rd: freg) (rs: freg)                  (**r negation *)
-  | Pfabss   (rd: freg) (rs: freg)                  (**r absolute value *)
-
-  | Pfadds   (rd: freg) (rs1 rs2: freg)             (**r addition *)
-  | Pfsubs   (rd: freg) (rs1 rs2: freg)             (**r subtraction *)
-  | Pfmuls   (rd: freg) (rs1 rs2: freg)             (**r multiplication *)
-  | Pfdivs   (rd: freg) (rs1 rs2: freg)             (**r division *)
-  | Pfmins   (rd: freg) (rs1 rs2: freg)             (**r minimum *)
-  | Pfmaxs   (rd: freg) (rs1 rs2: freg)             (**r maximum *)
-
-  | Pfeqs    (rd: ireg) (rs1 rs2: freg)             (**r compare equal *)
-  | Pflts    (rd: ireg) (rs1 rs2: freg)             (**r compare less-than *)
-  | Pfles    (rd: ireg) (rs1 rs2: freg)             (**r compare less-than/equal *)
-
-  | Pfsqrts  (rd: freg) (rs: freg)                  (**r square-root *)
-
-  | Pfmadds  (rd: freg) (rs1 rs2 rs3: freg)         (**r fused multiply-add *)
-  | Pfmsubs  (rd: freg) (rs1 rs2 rs3: freg)         (**r fused multiply-sub *)
-  | Pfnmadds (rd: freg) (rs1 rs2 rs3: freg)         (**r fused negated multiply-add *)
-  | Pfnmsubs (rd: freg) (rs1 rs2 rs3: freg)         (**r fused negated multiply-sub *)
-
-  | Pfcvtws  (rd: ireg) (rs: freg)                  (**r float32 -> int32 conversion *)
-  | Pfcvtwus (rd: ireg) (rs: freg)                  (**r float32 -> unsigned int32 conversion *)
-  | Pfcvtsw  (rd: freg) (rs: ireg)                 (**r int32 -> float32 conversion *)
-  | Pfcvtswu (rd: freg) (rs: ireg)                 (**r unsigned int32 -> float32 conversion *)
-
-  | Pfcvtls  (rd: ireg) (rs: freg)                  (**r float32 -> int64 conversion *)
-  | Pfcvtlus (rd: ireg) (rs: freg)                  (**r float32 -> unsigned int64 conversion *)
-  | Pfcvtsl  (rd: freg) (rs: ireg)                 (**r int64 -> float32 conversion *)
-  | Pfcvtslu (rd: freg) (rs: ireg)                 (**r unsigned int 64-> float32 conversion *)
-
-*)(* 64-bit (double-precision) floating point *)
-(*| Pfld_a   (rd: freg) (ra: ireg) (ofs: offset)    (**r load any64 *)
-  | Pfsd_a   (rd: freg) (ra: ireg) (ofs: offset)    (**r store any64 *)
-
-  | Pfabsd   (rd: freg) (rs: freg)                  (**r absolute value *)
-
-  | Pfaddd   (rd: freg) (rs1 rs2: freg)             (**r addition *)
-  | Pfsubd   (rd: freg) (rs1 rs2: freg)             (**r subtraction *)
-  | Pfmuld   (rd: freg) (rs1 rs2: freg)             (**r multiplication *)
-  | Pfdivd   (rd: freg) (rs1 rs2: freg)             (**r division *)
-  | Pfmind   (rd: freg) (rs1 rs2: freg)             (**r minimum *)
-  | Pfmaxd   (rd: freg) (rs1 rs2: freg)             (**r maximum *)
-
-  | Pfeqd    (rd: ireg) (rs1 rs2: freg)             (**r compare equal *)
-  | Pfltd    (rd: ireg) (rs1 rs2: freg)             (**r compare less-than *)
-  | Pfled    (rd: ireg) (rs1 rs2: freg)             (**r compare less-than/equal *)
-
-  | Pfsqrtd  (rd: freg) (rs: freg)                  (**r square-root *)
-
-  | Pfmaddd  (rd: freg) (rs1 rs2 rs3: freg)         (**r fused multiply-add *)
-  | Pfmsubd  (rd: freg) (rs1 rs2 rs3: freg)         (**r fused multiply-sub *)
-  | Pfnmaddd (rd: freg) (rs1 rs2 rs3: freg)         (**r fused negated multiply-add *)
-  | Pfnmsubd (rd: freg) (rs1 rs2 rs3: freg)         (**r fused negated multiply-sub *)
-
-  | Pfcvtwd  (rd: ireg) (rs: freg)                  (**r float -> int32 conversion *)
-  | Pfcvtwud (rd: ireg) (rs: freg)                  (**r float -> unsigned int32 conversion *)
-  | Pfcvtdw  (rd: freg) (rs: ireg)                 (**r int32 -> float conversion *)
-  | Pfcvtdwu (rd: freg) (rs: ireg)                 (**r unsigned int32 -> float conversion *)
-
-  | Pfcvtld  (rd: ireg) (rs: freg)                  (**r float -> int64 conversion *)
-  | Pfcvtlud (rd: ireg) (rs: freg)                  (**r float -> unsigned int64 conversion *)
-  | Pfcvtdl  (rd: freg) (rs: ireg)                 (**r int64 -> float conversion *)
-  | Pfcvtdlu (rd: freg) (rs: ireg)                 (**r unsigned int64 -> float conversion *)
-
-  | Pfcvtds  (rd: freg) (rs: freg)                  (**r float32 -> float   *)
-  | Pfcvtsd  (rd: freg) (rs: freg)                  (**r float   -> float32 *)
-*)
-
-Inductive instruction : Type :=
-  | PExpand         (i: ex_instruction)
-  | PControlFlow    (i: cf_instruction)
-  | PLoad           (i: ld_instruction)
-  | PStore          (i: st_instruction)
-  | PArith          (i: ar_instruction)
-.
-
-Coercion PExpand:       ex_instruction >-> instruction.
-Coercion PControlFlow:  cf_instruction >-> instruction.
-Coercion PLoad:         ld_instruction >-> instruction.
-Coercion PStore:        st_instruction >-> instruction.
-Coercion PArith:        ar_instruction >-> instruction.
-
-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
-  the convention that integer registers are mapped to values of
-  type [Tint] or [Tlong] (in 64 bit mode),
-  and float registers to values of type [Tsingle] or [Tfloat]. *)
-
-Definition regset := Pregmap.t val.
-Definition genv := Genv.t fundef unit.
-
-Definition getw (rs: regset) (r: ireg) : val :=
-  match r with
-  | _ => rs r
-  end.
-
-Definition getl (rs: regset) (r: ireg) : val :=
-  match r with
-  | _ => rs r
-  end.
-
-Notation "a # b" := (a b) (at level 1, only parsing) : asm.
-Notation "a ## b" := (getw a b) (at level 1) : asm.
-Notation "a ### b" := (getl a b) (at level 1) : asm.
-Notation "a # b <- c" := (Pregmap.set b c a) (at level 1, b at next level) : 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.
-
-(** 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 multiple registers *)
-
-Fixpoint set_regs (rl: list preg) (vl: list val) (rs: regset) : regset :=
-  match rl, vl with
-  | r1 :: rl', v1 :: vl' => set_regs rl' vl' (rs#r1 <- v1)
-  | _, _ => rs
-  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.
-
-Section RELSEM.
-
-(** Looking up instructions in a code sequence by position. *)
-
-Fixpoint find_instr (pos: Z) (c: code) {struct c} : option instruction :=
-  match c with
-  | nil => None
-  | i :: il => if zeq pos 0 then Some i else find_instr (pos - 1) il
-  end.
-
-(** Position corresponding to a label *)
-
-Definition is_label (lbl: label) (instr: instruction) : bool :=
-  match instr with
-  | Plabel lbl' => if peq lbl lbl' then true else false
-  | _ => false
-  end.
-
-Lemma is_label_correct:
-  forall lbl instr,
-  if is_label lbl instr then instr = Plabel lbl else instr <> Plabel lbl.
-Proof.
-  intros.  destruct instr; simpl; try discriminate.
-  destruct i; simpl; try discriminate.
-  case (peq lbl lbl0); intro; congruence.
-Qed.
-
-Fixpoint label_pos (lbl: label) (pos: Z) (c: code) {struct c} : option Z :=
-  match c with
-  | nil => None
-  | instr :: c' =>
-      if is_label lbl instr then Some (pos + 1) else label_pos lbl (pos + 1) c'
-  end.
-
-Variable ge: genv.
-
-(** The two functions below axiomatize how the linker processes
-  symbolic references [symbol + offset)] and splits their
-  actual values into a 20-bit high part [%hi(symbol + offset)] and 
-  a 12-bit low part [%lo(symbol + offset)]. *)
-
-Parameter low_half: genv -> ident -> ptrofs -> ptrofs.
-Parameter high_half: genv -> ident -> ptrofs -> val.
-
-(** The fundamental property of these operations is that, when applied
-  to the address of a symbol, their results can be recombined by
-  addition, rebuilding the original address. *)
-
-Axiom low_high_half:
-  forall id ofs,
-  Val.offset_ptr (high_half ge id ofs) (low_half ge id ofs) = Genv.symbol_address ge id ofs.
-
-(** 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).
-
-Definition goto_label (f: function) (lbl: label) (rs: regset) (m: mem) :=
-  match label_pos lbl 0 (fn_code f) with
-  | None => Stuck
-  | Some pos =>
-      match rs#PC with
-      | Vptr b ofs => Next (rs#PC <- (Vptr b (Ptrofs.repr pos))) m
-      | _          => Stuck
-      end
-  end.
-
-(** Auxiliaries for memory accesses *)
-
-Definition eval_offset (ofs: offset) : ptrofs :=
-  match ofs with
-  | Ofsimm n => n
-  | Ofslow id delta => low_half ge id delta
-  end.
-
-Definition exec_load (chunk: memory_chunk) (rs: regset) (m: mem)
-                     (d: preg) (a: ireg) (ofs: offset) :=
-  match Mem.loadv chunk m (Val.offset_ptr (rs a) (eval_offset ofs)) with
-  | None => Stuck
-  | Some v => Next (nextinstr (rs#d <- v)) m
-  end.
-
-Definition exec_store (chunk: memory_chunk) (rs: regset) (m: mem)
-                      (s: preg) (a: ireg) (ofs: offset) :=
-  match Mem.storev chunk m (Val.offset_ptr (rs a) (eval_offset ofs)) (rs s) with
-  | None => Stuck
-  | Some m' => Next (nextinstr rs) m'
-  end.
-
-(** Evaluating a branch *)
-
-Definition eval_branch (f: function) (l: label) (rs: regset) (m: mem) (res: option bool) : outcome :=
-  match res with
-    | Some true  => goto_label f l rs m
-    | Some false => Next (nextinstr rs) m
-    | None => Stuck
-  end.
-
-Inductive signedness: Type := Signed | Unsigned.
-
-Inductive intsize: Type := Int | Long.
-
-Definition itest_for_cmp (c: comparison) (s: signedness) :=
-  match c, s with
-  | Cne, Signed => ITne
-  | Ceq, Signed => ITeq
-  | Clt, Signed => ITlt
-  | Cge, Signed => ITge
-  | Cle, Signed => ITle
-  | Cgt, Signed => ITgt
-  | Cne, Unsigned => ITneu
-  | Ceq, Unsigned => ITequ
-  | Clt, Unsigned => ITltu
-  | Cge, Unsigned => ITgeu
-  | Cle, Unsigned => ITleu
-  | Cgt, Unsigned => ITgtu
-  end.
-
-(* CoMPare Signed Words to Zero *)
-Definition btest_for_cmpswz (c: comparison) :=
-  match c with
-  | Cne => BTwnez
-  | Ceq => BTweqz
-  | Clt => BTwltz
-  | Cge => BTwgez
-  | Cle => BTwlez
-  | Cgt => BTwgtz
-  end.
-
-(* CoMPare Signed Doubles to Zero *)
-Definition btest_for_cmpsdz (c: comparison) :=
-  match c with
-  | Cne => BTdnez
-  | Ceq => BTdeqz
-  | Clt => BTdltz
-  | Cge => BTdgez
-  | Cle => BTdlez
-  | Cgt => BTdgtz
-  end.
-
-Definition cmp_for_btest (bt: btest) :=
-  match bt with
-  | BTwnez => (Some Cne, Int)
-  | BTweqz => (Some Ceq, Int)
-  | BTwltz => (Some Clt, Int)
-  | BTwgez => (Some Cge, Int)
-  | BTwlez => (Some Cle, Int)
-  | BTwgtz => (Some Cgt, Int)
-
-  | BTdnez => (Some Cne, Long)
-  | BTdeqz => (Some Ceq, Long)
-  | BTdltz => (Some Clt, Long)
-  | BTdgez => (Some Cge, Long)
-  | BTdlez => (Some Cle, Long)
-  | BTdgtz => (Some Cgt, Long)
-  end.
-
-Definition cmpu_for_btest (bt: btest) :=
-  match bt with
-  | BTwnez => (Some Cne, Int)
-  | BTweqz => (Some Ceq, Int)
-  | BTdnez => (Some Cne, Long)
-  | BTdeqz => (Some Ceq, Long)
-  | _ => (None, Int)
-  end.
-
-(** Comparing integers *)
-Definition compare_int (t: itest) (v1 v2: val) (m: mem): val :=
-  match t with
-  | ITne  => Val.cmp Cne v1 v2
-  | ITeq  => Val.cmp Ceq v1 v2
-  | ITlt  => Val.cmp Clt v1 v2
-  | ITge  => Val.cmp Cge v1 v2
-  | ITle  => Val.cmp Cle v1 v2
-  | ITgt  => Val.cmp Cgt v1 v2
-  | ITneu => Val.cmpu (Mem.valid_pointer m) Cne v1 v2
-  | ITequ => Val.cmpu (Mem.valid_pointer m) Ceq v1 v2
-  | ITltu => Val.cmpu (Mem.valid_pointer m) Clt v1 v2
-  | ITgeu => Val.cmpu (Mem.valid_pointer m) Cge v1 v2
-  | ITleu => Val.cmpu (Mem.valid_pointer m) Cle v1 v2
-  | ITgtu => Val.cmpu (Mem.valid_pointer m) Cgt v1 v2
-  | ITall
-  | ITnall
-  | ITany
-  | ITnone => Vundef
-  end.
-
-Definition compare_long (t: itest) (v1 v2: val) (m: mem): val :=
-  let res := match t with
-  | ITne  => Val.cmpl Cne v1 v2
-  | ITeq  => Val.cmpl Ceq v1 v2
-  | ITlt  => Val.cmpl Clt v1 v2
-  | ITge  => Val.cmpl Cge v1 v2
-  | ITle  => Val.cmpl Cle v1 v2
-  | ITgt  => Val.cmpl Cgt v1 v2
-  | ITneu => Val.cmplu (Mem.valid_pointer m) Cne v1 v2
-  | ITequ => Val.cmplu (Mem.valid_pointer m) Ceq v1 v2
-  | ITltu => Val.cmplu (Mem.valid_pointer m) Clt v1 v2
-  | ITgeu => Val.cmplu (Mem.valid_pointer m) Cge v1 v2
-  | ITleu => Val.cmplu (Mem.valid_pointer m) Cle v1 v2
-  | ITgtu => Val.cmplu (Mem.valid_pointer m) Cgt v1 v2
-  | ITall
-  | ITnall
-  | ITany
-  | ITnone => Some Vundef
-  end in 
-  match res with
-  | Some v => v
-  | None => Vundef
-  end
-  .
-
-(** Execution of a single instruction [i] in initial state [rs] and
-    [m].  Return updated state.  For instructions that correspond to
-    actual RISC-V instructions, the cases are straightforward
-    transliterations of the informal descriptions given in the RISC-V
-    user-mode specification.  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 RISC-V 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 :=
-(** Get/Set system registers *)
-  match i with
-  | Pget rd ra =>
-    match ra with
-    | RA => Next (nextinstr (rs#rd <- (rs#ra))) m
-    | _  => Stuck
-    end
-  | Pset ra rd =>
-    match ra with
-    | RA => Next (nextinstr (rs#ra <- (rs#rd))) m
-    | _  => Stuck
-    end
-
-(** Branch Control Unit instructions *)
-  | Pret =>
-      Next (rs#PC <- (rs#RA)) m
-  | Pcall s =>
-      Next (rs#RA <- (Val.offset_ptr (rs#PC) Ptrofs.one)#PC <- (Genv.symbol_address ge s Ptrofs.zero)) m
-  | Pgoto s =>
-      Next (rs#PC <- (Genv.symbol_address ge s Ptrofs.zero)) m
-  | Pj_l l =>
-      goto_label f l rs m
-  | Pcb bt r l =>
-      match cmp_for_btest bt with
-      | (Some c, Int)  => eval_branch f l rs m (Val.cmp_bool c rs##r (Vint (Int.repr 0)))
-      | (Some c, Long) => eval_branch f l rs m (Val.cmpl_bool c rs###r (Vlong (Int64.repr 0)))
-      | (None, _) => Stuck
-      end
-  | Pcbu bt r l => 
-      match cmpu_for_btest bt with
-      | (Some c, Int) => eval_branch f l rs m (Val.cmpu_bool (Mem.valid_pointer m) c rs##r (Vint (Int.repr 0)))
-      | (Some c, Long) => eval_branch f l rs m (Val.cmplu_bool (Mem.valid_pointer m) c rs###r (Vlong (Int64.repr 0)))
-      | (None, _) => Stuck
-      end
-
-(** Arithmetic Instructions *)
-  | PArithR n d =>
-      match n with
-      | Pcvtw2l => Next (nextinstr (rs#d <- (Val.longofint rs#d))) m
-      end
-  
-  | PArithRR n d s =>
-      match n with
-      | Pmv => Next (nextinstr (rs#d <- (rs#s))) m
-      | Pnegw => Next (nextinstr (rs#d <- (Val.neg rs###s))) m
-      | Pnegl => Next (nextinstr (rs#d <- (Val.negl rs###s))) m
-      | Pfnegd => Next (nextinstr (rs#d <- (Val.negf rs#s))) m
-      | Pcvtl2w => Next (nextinstr (rs#d <- (Val.loword rs###s))) m
-      | Pmvw2l => Next (nextinstr (rs#d <- (Val.longofint rs#s))) m
-      end
-
-  | PArithRI32 n d i =>
-      match n with
-      | Pmake => Next (nextinstr (rs#d <- (Vint i))) m
-      end
-
-  | PArithRI64 n d i =>
-      match n with
-      | Pmakel => Next (nextinstr (rs#d <- (Vlong i))) m
-      end
-
-  | PArithRRR n d s1 s2 =>
-      match n with
-      | Pcompw c => Next (nextinstr (rs#d <- (compare_int c rs##s1 rs##s2 m))) m
-      | Pcompl c => Next (nextinstr (rs#d <- (compare_long c rs###s1 rs###s2 m))) m
-      | Paddw  => Next (nextinstr (rs#d <- (Val.add  rs##s1 rs##s2))) m
-      | Psubw  => Next (nextinstr (rs#d <- (Val.sub  rs##s1 rs##s2))) m
-      | Pmulw  => Next (nextinstr (rs#d <- (Val.mul  rs##s1 rs##s2))) m
-      | Pandw  => Next (nextinstr (rs#d <- (Val.and  rs##s1 rs##s2))) m
-      | Porw   => Next (nextinstr (rs#d <- (Val.or   rs##s1 rs##s2))) m
-      | Pxorw  => Next (nextinstr (rs#d <- (Val.xor  rs##s1 rs##s2))) m
-      | Psrlw  => Next (nextinstr (rs#d <- (Val.shru rs##s1 rs##s2))) m
-      | Psraw  => Next (nextinstr (rs#d <- (Val.shr  rs##s1 rs##s2))) m
-      | Psllw  => Next (nextinstr (rs#d <- (Val.shl  rs##s1 rs##s2))) m
-
-      | Paddl => Next (nextinstr (rs#d <- (Val.addl rs###s1 rs###s2))) m
-      | Psubl => Next (nextinstr (rs#d <- (Val.subl rs###s1 rs###s2))) m
-      | Pandl => Next (nextinstr (rs#d <- (Val.andl rs###s1 rs###s2))) m
-      | Porl  => Next (nextinstr (rs#d <- (Val.orl  rs###s1 rs###s2))) m
-      | Pxorl  => Next (nextinstr (rs#d <- (Val.xorl  rs###s1 rs###s2))) m
-      | Pmull => Next (nextinstr (rs#d <- (Val.mull rs###s1 rs###s2))) m
-      | Pslll => Next (nextinstr (rs#d <- (Val.shll rs###s1 rs###s2))) m
-      | Psrll => Next (nextinstr (rs#d <- (Val.shrlu rs###s1 rs###s2))) m
-      | Psral => Next (nextinstr (rs#d <- (Val.shrl rs###s1 rs###s2))) m
-      end
-
-  | PArithRRI32 n d s i =>
-      match n with
-      | Pcompiw c => Next (nextinstr (rs#d <- (compare_int c rs##s (Vint i) m))) m
-      | Paddiw  => Next (nextinstr (rs#d <- (Val.add   rs##s (Vint i)))) m
-      | Pandiw  => Next (nextinstr (rs#d <- (Val.and   rs##s (Vint i)))) m
-      | Poriw   => Next (nextinstr (rs#d <- (Val.or    rs##s (Vint i)))) m
-      | Pxoriw  => Next (nextinstr (rs#d <- (Val.xor   rs##s (Vint i)))) m
-      | Psraiw  => Next (nextinstr (rs#d <- (Val.shr   rs##s (Vint i)))) m
-      | Psrliw  => Next (nextinstr (rs#d <- (Val.shru  rs##s (Vint i)))) m
-      | Pslliw  => Next (nextinstr (rs#d <- (Val.shl   rs##s (Vint i)))) m
-
-      | Psllil  => Next (nextinstr (rs#d <- (Val.shll  rs###s (Vint i)))) m
-      | Psrlil  => Next (nextinstr (rs#d <- (Val.shrlu rs###s (Vint i)))) m
-      | Psrail  => Next (nextinstr (rs#d <- (Val.shrl  rs###s (Vint i)))) m
-      end
-
-  | PArithRRI64 n d s i =>
-      match n with
-      | Pcompil c => Next (nextinstr (rs#d <- (compare_long c rs###s (Vlong i) m))) m
-      | Paddil  => Next (nextinstr (rs#d <- (Val.addl rs###s (Vlong i)))) m
-      | Pandil  => Next (nextinstr (rs#d <- (Val.andl rs###s (Vlong i)))) m
-      | Poril   => Next (nextinstr (rs#d <- (Val.orl  rs###s (Vlong i)))) m
-      | Pxoril  => Next (nextinstr (rs#d <- (Val.xorl  rs###s (Vlong i)))) m
-      end
-
-(** Loads and stores *)
-  | Plb d a ofs =>
-      exec_load Mint8signed rs m d a ofs
-  | Plbu d a ofs =>
-      exec_load Mint8unsigned rs m d a ofs
-  | Plh d a ofs =>
-      exec_load Mint16signed rs m d a ofs
-  | Plhu d a ofs =>
-      exec_load Mint16unsigned rs m d a ofs
-  | Plw d a ofs =>
-      exec_load Mint32 rs m d a ofs
-  | Plw_a d a ofs =>
-      exec_load Many32 rs m d a ofs
-  | Pld d a ofs =>
-      exec_load Mint64 rs m d a ofs
-  | Pld_a d a ofs =>
-      exec_load Many64 rs m d a ofs
-  | Psb s a ofs =>
-      exec_store Mint8unsigned rs m s a ofs
-  | Psh s a ofs =>
-      exec_store Mint16unsigned rs m s a ofs
-  | Psw s a ofs =>
-      exec_store Mint32 rs m s a ofs
-  | Psw_a s a ofs =>
-      exec_store Many32 rs m s a ofs
-  | Psd s a ofs =>
-      exec_store Mint64 rs m s a ofs
-  | Psd_a s a ofs =>
-      exec_store Many64 rs m s a ofs
-
-(** Floating point register move *)
-(*| Pfmv d s =>
-      Next (nextinstr (rs#d <- (rs#s))) m
-
-(** 32-bit (single-precision) floating point *)
-*)| Pfls d a ofs =>
-      exec_load Mfloat32 rs m d a ofs
-  | Pfss s a ofs =>
-      exec_store Mfloat32 rs m s a ofs
-
-(*| Pfnegs d s =>
-      Next (nextinstr (rs#d <- (Val.negfs rs#s))) m
-  | Pfabss d s =>
-      Next (nextinstr (rs#d <- (Val.absfs rs#s))) m
-
-  | Pfadds d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.addfs rs#s1 rs#s2))) m
-  | Pfsubs d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.subfs rs#s1 rs#s2))) m
-  | Pfmuls d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.mulfs rs#s1 rs#s2))) m
-  | Pfdivs d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.divfs rs#s1 rs#s2))) m
-  | Pfeqs d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.cmpfs Ceq rs#s1 rs#s2))) m
-  | Pflts d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.cmpfs Clt rs#s1 rs#s2))) m
-  | Pfles d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.cmpfs Cle rs#s1 rs#s2))) m
-
-  | Pfcvtws d s =>
-      Next (nextinstr (rs#d <- (Val.maketotal (Val.intofsingle rs#s)))) m
-  | Pfcvtwus d s =>
-      Next (nextinstr (rs#d <- (Val.maketotal (Val.intuofsingle rs#s)))) m
-  | Pfcvtsw d s =>
-      Next (nextinstr (rs#d <- (Val.maketotal (Val.singleofint rs##s)))) m
-  | Pfcvtswu d s =>
-      Next (nextinstr (rs#d <- (Val.maketotal (Val.singleofintu rs##s)))) m
-
-  | Pfcvtls d s =>
-      Next (nextinstr (rs#d <- (Val.maketotal (Val.longofsingle rs#s)))) m
-  | Pfcvtlus d s =>
-      Next (nextinstr (rs#d <- (Val.maketotal (Val.longuofsingle rs#s)))) m
-  | Pfcvtsl d s =>
-      Next (nextinstr (rs#d <- (Val.maketotal (Val.singleoflong rs###s)))) m
-  | Pfcvtslu d s =>
-      Next (nextinstr (rs#d <- (Val.maketotal (Val.singleoflongu rs###s)))) m
-
-(** 64-bit (double-precision) floating point *)
-*)| Pfld d a ofs =>
-      exec_load Mfloat64 rs m d a ofs
-(*| Pfld_a d a ofs =>
-      exec_load Many64 rs m d a ofs
-*)| Pfsd s a ofs =>
-      exec_store Mfloat64 rs m s a ofs
-(*| Pfsd_a s a ofs =>
-      exec_store Many64 rs m s a ofs
-
-  | Pfabsd d s =>
-      Next (nextinstr (rs#d <- (Val.absf rs#s))) m
-
-  | Pfaddd d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.addf rs#s1 rs#s2))) m
-  | Pfsubd d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.subf rs#s1 rs#s2))) m
-  | Pfmuld d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.mulf rs#s1 rs#s2))) m
-  | Pfdivd d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.divf rs#s1 rs#s2))) m
-  | Pfeqd d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.cmpf Ceq rs#s1 rs#s2))) m
-  | Pfltd d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.cmpf Clt rs#s1 rs#s2))) m
-  | Pfled d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.cmpf Cle rs#s1 rs#s2))) m
-
-  | Pfcvtwd d s =>
-      Next (nextinstr (rs#d <- (Val.maketotal (Val.intoffloat rs#s)))) m
-  | Pfcvtwud d s =>
-      Next (nextinstr (rs#d <- (Val.maketotal (Val.intuoffloat rs#s)))) m
-  | Pfcvtdw d s =>
-      Next (nextinstr (rs#d <- (Val.maketotal (Val.floatofint rs##s)))) m
-  | Pfcvtdwu d s =>
-      Next (nextinstr (rs#d <- (Val.maketotal (Val.floatofintu rs##s)))) m
-
-  | Pfcvtld d s =>
-      Next (nextinstr (rs#d <- (Val.maketotal (Val.longoffloat rs#s)))) m
-  | Pfcvtlud d s =>
-      Next (nextinstr (rs#d <- (Val.maketotal (Val.longuoffloat rs#s)))) m
-  | Pfcvtdl d s =>
-      Next (nextinstr (rs#d <- (Val.maketotal (Val.floatoflong rs###s)))) m
-  | Pfcvtdlu d s =>
-      Next (nextinstr (rs#d <- (Val.maketotal (Val.floatoflongu rs###s)))) m
-
-  | Pfcvtds d s =>
-      Next (nextinstr (rs#d <- (Val.floatofsingle rs#s))) m
-  | Pfcvtsd d s =>
-      Next (nextinstr (rs#d <- (Val.singleoffloat rs#s))) 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 Mptr m1 (Val.offset_ptr sp pos) rs#SP with
-      | None => Stuck
-      | Some m2 => Next (nextinstr (rs #FP <- (rs SP) #SP <- sp #GPR31 <- Vundef)) m2
-      end
-  | Pfreeframe sz pos =>
-      match Mem.loadv Mptr 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 #GPR31 <- Vundef)) m'
-              end
-          | _ => Stuck
-          end
-      end
-  | Plabel lbl =>
-      Next (nextinstr rs) m
-  | Ploadsymbol rd s ofs =>
-      Next (nextinstr (rs#rd <- (Genv.symbol_address ge s ofs))) m
-(*| Ploadsymbol_high rd s ofs =>
-      Next (nextinstr (rs#rd <- (high_half ge s ofs))) m
-  | Ploadli rd i =>
-      Next (nextinstr (rs#GPR31 <- Vundef #rd <- (Vlong i))) m
-  | Ploadfi rd f =>
-      Next (nextinstr (rs#GPR31 <- Vundef #rd <- (Vfloat f))) m
-  | Ploadsi rd f =>
-      Next (nextinstr (rs#GPR31 <- Vundef #rd <- (Vsingle f))) m
-  | Pbtbl r tbl =>
-      match rs r with
-      | Vint n =>
-          match list_nth_z tbl (Int.unsigned n) with
-          | None => Stuck
-          | Some lbl => goto_label f lbl (rs#GPR5 <- Vundef #GPR31 <- 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. *)
-  | Pclzll _ _
-  | Pstsud _ _ _
-    => Stuck
-  end.
-
-(** Translation of the LTL/Linear/Mach view of machine registers to
-  the RISC-V view.  Note that no LTL register maps to [X31].  This
-  register is reserved as temporary, to be used by the generated RV32G
-  code.  *)
-
-  (* FIXME - R31 is not there *)
-Definition preg_of (r: mreg) : preg :=
-  match r with
-  | R0  => GPR0  | R1  => GPR1  | R2  => GPR2  | R3  => GPR3  | R4  => GPR4
-  | R5  => GPR5  | R6  => GPR6  | R7  => GPR7                 | R9  => GPR9
-  | R10 => GPR10 (*| R11 => GPR11 | R12 => GPR12 | R13 => GPR13 | R14  => GPR14 *)
-  | R15 => GPR15 | R16 => GPR16 | R17 => GPR17 | R18 => GPR18 | R19  => GPR19
-  | R20 => GPR20 | R21 => GPR21 | R22 => GPR22 | R23 => GPR23 | R24  => GPR24
-  | R25 => GPR25 | R26 => GPR26 | R27 => GPR27 | R28 => GPR28 | R29  => GPR29
-  | R30 => GPR30 |                R32 => GPR32 | R33 => GPR33 | R34  => GPR34
-  | R35 => GPR35 | R36 => GPR36 | R37 => GPR37 | R38 => GPR38 | R39  => GPR39
-  | R40 => GPR40 | R41 => GPR41 | R42 => GPR42 | R43 => GPR43 | R44  => GPR44
-  | R45 => GPR45 | R46 => GPR46 | R47 => GPR47 | R48 => GPR48 | R49  => GPR49
-  | R50 => GPR50 | R51 => GPR51 | R52 => GPR52 | R53 => GPR53 | R54  => GPR54
-  | R55 => GPR55 | R56 => GPR56 | R57 => GPR57 | R58 => GPR58 | R59  => GPR59
-  | R60 => GPR60 | R61 => GPR61 | R62 => GPR62 | R63 => GPR63
-  end.
-
-(** Extract the values of the arguments of an external call.
-    We exploit the calling conventions from module [Conventions], except that
-    we use RISC-V 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 (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',
-      rs PC = Vptr b ofs ->
-      Genv.find_funct_ptr ge b = Some (Internal f) ->
-      find_instr (Ptrofs.unsigned ofs) (fn_code f) = Some i ->
-      exec_instr f i rs m = Next rs' m' ->
-      step (State rs m) E0 (State rs' m')
-  | exec_step_builtin:
-      forall b ofs f ef args res rs m vargs t vres 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 (A:=instruction) (Pbuiltin ef args res) ->
-      eval_builtin_args ge rs (rs SP) m args vargs ->
-      external_call ef ge vargs m t vres m' ->
-      rs' = nextinstr
-              (set_res res vres
-                (undef_regs (map preg_of (destroyed_by_builtin ef))
-                   (rs#GPR31 <- Vundef))) ->
-      step (State rs m) t (State rs' m')
-  | exec_step_external:
-      forall b ef args res rs m t rs' m',
-      rs PC = Vptr b Ptrofs.zero ->
-      Genv.find_funct_ptr ge b = Some (External ef) ->
-      external_call ef ge args m t res m' ->
-      extcall_arguments rs m (ef_sig ef) args ->
-      rs' = (set_pair (loc_external_result (ef_sig ef) ) res rs)#PC <- (rs RA) ->
-      step (State rs m) t (State rs' m').
-
-End RELSEM.
-
-(** Execution of whole programs. *)
-
-Inductive initial_state (p: program): state -> Prop :=
-  | initial_state_intro: forall m0,
-      let ge := Genv.globalenv p in
-      let rs0 :=
-        (Pregmap.init Vundef)
-        # PC <- (Genv.symbol_address ge p.(prog_main) Ptrofs.zero)
-        # SP <- Vnullptr
-        # RA <- Vnullptr in
-      Genv.init_mem p = Some m0 ->
-      initial_state p (State rs0 m0).
-
-Inductive final_state: state -> int -> Prop :=
-  | final_state_intro: forall rs m r,
-      rs PC = Vnullptr ->
-      rs GPR0 = Vint r ->
-      final_state (State rs m) r.
-
-Definition semantics (p: program) :=
-  Semantics step (initial_state p) final_state (Genv.globalenv p).
-
-(** Determinacy of the [Asm] semantics. *)
-
-Remark extcall_arguments_determ:
-  forall rs m sg args1 args2,
-  extcall_arguments rs m sg args1 -> extcall_arguments rs m sg args2 -> args1 = args2.
-Proof.
-  intros until m.
-  assert (A: forall l v1 v2,
-             extcall_arg rs m l v1 -> extcall_arg rs m l v2 -> v1 = v2).
-  { intros. inv H; inv H0; congruence. }
-  assert (B: forall p v1 v2,
-             extcall_arg_pair rs m p v1 -> extcall_arg_pair rs m p v2 -> v1 = v2).
-  { intros. inv H; inv H0. 
-    eapply A; eauto.
-    f_equal; eapply A; eauto. }
-  assert (C: forall ll vl1, list_forall2 (extcall_arg_pair rs m) ll vl1 ->
-             forall vl2, list_forall2 (extcall_arg_pair rs m) ll vl2 -> vl1 = vl2).
-  {
-    induction 1; intros vl2 EA; inv EA.
-    auto.
-    f_equal; eauto. }
-  intros. eapply C; eauto.
-Qed.
-
-Lemma semantics_determinate: forall p, determinate (semantics p).
-Proof.
-Ltac Equalities :=
-  match goal with
-  | [ H1: ?a = ?b, H2: ?a = ?c |- _ ] =>
-      rewrite H1 in H2; inv H2; Equalities
-  | _ => idtac
-  end.
-  intros; constructor; simpl; intros.
-- (* determ *)
-  inv H; inv H0; Equalities.
-  split. constructor. auto.
-  discriminate.
-  discriminate.
-  assert (vargs0 = vargs) by (eapply eval_builtin_args_determ; eauto). subst vargs0.
-  exploit external_call_determ. eexact H5. eexact H11. intros [A B].
-  split. auto. intros. destruct B; auto. subst. auto.
-  assert (args0 = args) by (eapply extcall_arguments_determ; eauto). subst args0.
-  exploit external_call_determ. eexact H3. eexact H8. intros [A B].
-  split. auto. intros. destruct B; auto. subst. auto.
-- (* trace length *)
-  red; intros. inv H; simpl.
-  omega.
-  eapply external_call_trace_length; eauto.
-  eapply external_call_trace_length; eauto.
-- (* initial states *)
-  inv H; inv H0. f_equal. congruence.
-- (* final no step *)
-  assert (NOTNULL: forall b ofs, Vnullptr <> Vptr b ofs).
-  { intros; unfold Vnullptr; destruct Archi.ptr64; congruence. }
-  inv H. unfold Vzero in H0. red; intros; red; intros.
-  inv H; rewrite H0 in *; eelim NOTNULL; eauto.
-- (* final states *)
-  inv H; inv H0. congruence.
-Qed.
-
-(** Classification functions for processor registers (used in Asmgenproof). *)
-
-Definition data_preg (r: preg) : bool :=
-  match r with
-  | RA  => false
-  | IR GPR31 => false
-  | IR GPR8 => false
-  | IR _   => true
-  | FR _   => true
-  | PC     => false
-  end.
+(* *********************************************************************)

+(*                                                                     *)

+(*              The Compcert verified compiler                         *)

+(*                                                                     *)

+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)

+(*           Prashanth Mundkur, SRI International                      *)

+(*                                                                     *)

+(*  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.     *)

+(*                                                                     *)

+(*  The contributions by Prashanth Mundkur are reused and adapted      *)

+(*  under the terms of a Contributor License Agreement between         *)

+(*  SRI International and INRIA.                                       *)

+(*                                                                     *)

+(* *********************************************************************)

+

+(** Abstract syntax and semantics for K1c assembly language. *)

+

+Require Import Coqlib.

+Require Import Maps.

+Require Import AST.

+Require Import Integers.

+Require Import Floats.

+Require Import Values.

+Require Import Memory.

+Require Import Events.

+Require Import Globalenvs.

+Require Import Smallstep.

+Require Import Locations.

+Require Stacklayout.

+Require Import Conventions.

+Require Import Asmblock.

+Require Import Linking.

+Require Import Errors.

+

+Inductive instruction : Type :=

+  (** pseudo instructions *)

+  | Pallocframe (sz: Z) (pos: ptrofs)               (**r allocate new stack frame *)

+  | Pfreeframe  (sz: Z) (pos: ptrofs)               (**r deallocate stack frame and restore previous frame *)

+  | Plabel  (lbl: label)                            (**r define a code label *)

+  | Ploadsymbol (rd: ireg) (id: ident) (ofs: ptrofs) (**r load the address of a symbol *)

+  | Pbuiltin: external_function -> list (builtin_arg preg)

+              -> builtin_res preg -> instruction   (**r built-in function (pseudo) *)

+  | Pnop                                            (**r instruction that does nothing *)

+

+  (** Control flow instructions *)

+  | Pget    (rd: ireg) (rs: preg)                   (**r get system register *)

+  | Pset    (rd: preg) (rs: ireg)                   (**r set system register *)

+  | Pret                                            (**r return *)

+  | Pcall   (l: label)                              (**r function call *)

+  (* Pgoto is for tailcalls, Pj_l is for jumping to a particular label *)

+  | Pgoto   (l: label)                              (**r goto *)

+  | Pj_l    (l: label)                              (**r jump to label *)

+  | Pcb     (bt: btest) (r: ireg) (l: label)        (**r branch based on btest *)

+  | Pcbu    (bt: btest) (r: ireg) (l: label)        (**r branch based on btest with unsigned semantics *)

+

+  (** Loads **)

+  | Plb     (rd: ireg) (ra: ireg) (ofs: offset)     (**r load byte *)

+  | Plbu    (rd: ireg) (ra: ireg) (ofs: offset)     (**r load byte unsigned *)

+  | Plh     (rd: ireg) (ra: ireg) (ofs: offset)     (**r load half word *)

+  | Plhu    (rd: ireg) (ra: ireg) (ofs: offset)     (**r load half word unsigned *)

+  | Plw     (rd: ireg) (ra: ireg) (ofs: offset)     (**r load int32 *)

+  | Plw_a   (rd: ireg) (ra: ireg) (ofs: offset)     (**r load any32 *)

+  | Pld     (rd: ireg) (ra: ireg) (ofs: offset)     (**r load int64 *)

+  | Pld_a   (rd: ireg) (ra: ireg) (ofs: offset)     (**r load any64 *)

+  | Pfls    (rd: freg) (ra: ireg) (ofs: offset)     (**r load float *)

+  | Pfld     (rd: freg) (ra: ireg) (ofs: offset)    (**r load 64-bit float *)

+

+  (** Stores **)

+  | Psb     (rs: ireg) (ra: ireg) (ofs: offset)     (**r store byte *)

+  | Psh     (rs: ireg) (ra: ireg) (ofs: offset)     (**r store half byte *)

+  | Psw     (rs: ireg) (ra: ireg) (ofs: offset)     (**r store int32 *)

+  | Psw_a   (rs: ireg) (ra: ireg) (ofs: offset)     (**r store any32 *)

+  | Psd     (rs: ireg) (ra: ireg) (ofs: offset)     (**r store int64 *)

+  | Psd_a   (rs: ireg) (ra: ireg) (ofs: offset)     (**r store any64 *)

+  | Pfss    (rs: freg) (ra: ireg) (ofs: offset)     (**r store float *)

+  | Pfsd     (rd: freg) (ra: ireg) (ofs: offset)    (**r store 64-bit float *)

+

+  (** Arith R *)

+  | Pcvtw2l (rd: ireg)                              (**r Convert Word to Long *)

+

+  (** Arith RR *)

+  | Pmv     (rd rs: ireg)                           (**r register move *)

+  | Pnegw   (rd rs: ireg)                           (**r negate word *)

+  | Pnegl   (rd rs: ireg)                           (**r negate long *)

+  | Pfnegd  (rd rs: ireg)                           (**r float negate double *)

+  | Pcvtl2w (rd rs: ireg)                           (**r Convert Long to Word *)

+  | Pmvw2l  (rd rs: ireg)                           (**r Move Convert Word to Long *)

+

+  (** Arith RI32 *)

+  | Pmake   (rd: ireg) (imm: int)                   (**r load immediate *)

+

+  (** Arith RI64 *)

+  | Pmakel  (rd: ireg) (imm: int64)                 (**r load immediate long *)

+

+  (** Arith RRR *)

+  | Pcompw  (it: itest) (rd rs1 rs2: ireg)          (**r comparison word *)

+  | Pcompl  (it: itest) (rd rs1 rs2: ireg)          (**r comparison long *)

+

+  | Paddw               (rd rs1 rs2: ireg)          (**r add word *)

+  | Psubw               (rd rs1 rs2: ireg)          (**r sub word *)

+  | Pmulw               (rd rs1 rs2: ireg)          (**r mul word *)

+  | Pandw               (rd rs1 rs2: ireg)          (**r and word *)

+  | Porw                (rd rs1 rs2: ireg)          (**r or word *)

+  | Pxorw               (rd rs1 rs2: ireg)          (**r xor word *)

+  | Psraw               (rd rs1 rs2: ireg)          (**r shift right arithmetic word *)

+  | Psrlw               (rd rs1 rs2: ireg)          (**r shift right logical word *)

+  | Psllw               (rd rs1 rs2: ireg)          (**r shift left logical word *)

+

+  | Paddl               (rd rs1 rs2: ireg)          (**r add long *)

+  | Psubl               (rd rs1 rs2: ireg)          (**r sub long *)

+  | Pandl               (rd rs1 rs2: ireg)          (**r and long *)

+  | Porl                (rd rs1 rs2: ireg)          (**r or long *)

+  | Pxorl               (rd rs1 rs2: ireg)          (**r xor long *)

+  | Pmull               (rd rs1 rs2: ireg)          (**r mul long (low part) *)

+  | Pslll               (rd rs1 rs2: ireg)          (**r shift left logical long *)

+  | Psrll               (rd rs1 rs2: ireg)          (**r shift right logical long *)

+  | Psral               (rd rs1 rs2: ireg)          (**r shift right arithmetic long *)

+

+  (** Arith RRI32 *)

+  | Pcompiw (it: itest) (rd rs: ireg) (imm: int)    (**r comparison imm word *)

+

+  | Paddiw              (rd rs: ireg) (imm: int)    (**r add imm word *)

+  | Pandiw              (rd rs: ireg) (imm: int)    (**r and imm word *)

+  | Poriw               (rd rs: ireg) (imm: int)    (**r or imm word *)

+  | Pxoriw              (rd rs: ireg) (imm: int)    (**r xor imm word *)

+  | Psraiw              (rd rs: ireg) (imm: int)    (**r shift right arithmetic imm word *)

+  | Psrliw              (rd rs: ireg) (imm: int)    (**r shift right logical imm word *)

+  | Pslliw              (rd rs: ireg) (imm: int)    (**r shift left logical imm word *)

+

+  | Psllil              (rd rs: ireg) (imm: int)    (**r shift left logical immediate long *)

+  | Psrlil              (rd rs: ireg) (imm: int)    (**r shift right logical immediate long *)

+  | Psrail              (rd rs: ireg) (imm: int)    (**r shift right arithmetic immediate long *)

+

+  (** Arith RRI64 *)

+  | Pcompil (it: itest) (rd rs: ireg) (imm: int64)  (**r comparison imm long *)

+  | Paddil              (rd rs: ireg) (imm: int64)  (**r add immediate long *) 

+  | Pandil              (rd rs: ireg) (imm: int64)  (**r and immediate long *) 

+  | Poril               (rd rs: ireg) (imm: int64)  (**r or immediate long *) 

+  | Pxoril              (rd rs: ireg) (imm: int64)  (**r xor immediate long *) 

+  .

+

+(** Correspondance between Asmblock and Asm *)

+

+Definition control_to_instruction (c: control) :=

+  match c with

+  | PExpand (Asmblock.Pbuiltin ef args res) => Pbuiltin ef args res

+  | PCtlFlow Asmblock.Pret                  => Pret

+  | PCtlFlow (Asmblock.Pcall l)             => Pcall l

+  | PCtlFlow (Asmblock.Pgoto l)             => Pgoto l

+  | PCtlFlow (Asmblock.Pj_l l)              => Pj_l l

+  | PCtlFlow (Asmblock.Pcb bt r l)          => Pcb bt r l

+  | PCtlFlow (Asmblock.Pcbu bt r l)         => Pcbu bt r l

+  end.

+

+Definition basic_to_instruction (b: basic) :=

+  match b with

+  (** Special basics *)

+  | Asmblock.Pget rd rs         => Pget rd rs

+  | Asmblock.Pset rd rs         => Pset rd rs

+  | Asmblock.Pnop               => Pnop

+  | Asmblock.Pallocframe sz pos => Pallocframe sz pos

+  | Asmblock.Pfreeframe sz pos  => Pfreeframe sz pos

+

+  (** PArith basics *)

+  (* R *)

+  | PArithR Asmblock.Pcvtw2l r              => Pcvtw2l r

+  | PArithR (Asmblock.Ploadsymbol id ofs) r => Ploadsymbol r id ofs

+

+  (* RR *)

+  | PArithRR Asmblock.Pmv rd rs     => Pmv rd rs

+  | PArithRR Asmblock.Pnegw rd rs   => Pnegw rd rs

+  | PArithRR Asmblock.Pnegl rd rs   => Pfnegd rd rs

+  | PArithRR Asmblock.Pcvtl2w rd rs => Pcvtl2w rd rs

+  | PArithRR Asmblock.Pmvw2l rd rs  => Pmvw2l rd rs

+  | PArithRR Asmblock.Pfnegd rd rs  => Pfnegd rd rs

+

+  (* RI32 *)

+  | PArithRI32 Asmblock.Pmake rd imm  => Pmake rd imm

+

+  (* RI64 *)

+  | PArithRI64 Asmblock.Pmakel rd imm => Pmakel rd imm

+

+  (* RRR *)

+  | PArithRRR (Asmblock.Pcompw it) rd rs1 rs2 => Pcompw it rd rs1 rs2

+  | PArithRRR (Asmblock.Pcompl it) rd rs1 rs2 => Pcompl it rd rs1 rs2

+  | PArithRRR Asmblock.Paddw rd rs1 rs2       => Paddw rd rs1 rs2

+  | PArithRRR Asmblock.Psubw rd rs1 rs2       => Psubw rd rs1 rs2

+  | PArithRRR Asmblock.Pmulw rd rs1 rs2       => Pmulw rd rs1 rs2

+  | PArithRRR Asmblock.Pandw rd rs1 rs2       => Pandw rd rs1 rs2

+  | PArithRRR Asmblock.Porw rd rs1 rs2        => Porw rd rs1 rs2

+  | PArithRRR Asmblock.Pxorw rd rs1 rs2       => Pxorw rd rs1 rs2

+  | PArithRRR Asmblock.Psraw rd rs1 rs2       => Psraw rd rs1 rs2

+  | PArithRRR Asmblock.Psrlw rd rs1 rs2       => Psrlw rd rs1 rs2

+  | PArithRRR Asmblock.Psllw rd rs1 rs2       => Psllw rd rs1 rs2

+

+  | PArithRRR Asmblock.Paddl rd rs1 rs2       => Paddl rd rs1 rs2

+  | PArithRRR Asmblock.Psubl rd rs1 rs2       => Psubl rd rs1 rs2

+  | PArithRRR Asmblock.Pandl rd rs1 rs2       => Pandl rd rs1 rs2

+  | PArithRRR Asmblock.Porl rd rs1 rs2        => Porl rd rs1 rs2

+  | PArithRRR Asmblock.Pxorl rd rs1 rs2       => Pxorl rd rs1 rs2

+  | PArithRRR Asmblock.Pmull rd rs1 rs2       => Pmull rd rs1 rs2

+  | PArithRRR Asmblock.Pslll rd rs1 rs2       => Pslll rd rs1 rs2

+  | PArithRRR Asmblock.Psrll rd rs1 rs2       => Psrll rd rs1 rs2

+  | PArithRRR Asmblock.Psral rd rs1 rs2       => Psral rd rs1 rs2

+

+  (* RRI32 *)

+  | PArithRRI32 (Asmblock.Pcompiw it) rd rs imm => Pcompiw it rd rs imm

+  | PArithRRI32 Asmblock.Paddiw rd rs imm       => Paddiw rd rs imm

+  | PArithRRI32 Asmblock.Pandiw rd rs imm       => Pandiw rd rs imm

+  | PArithRRI32 Asmblock.Poriw rd rs imm        => Poriw rd rs imm

+  | PArithRRI32 Asmblock.Pxoriw rd rs imm       => Pxoriw rd rs imm

+  | PArithRRI32 Asmblock.Psraiw rd rs imm       => Psraiw rd rs imm

+  | PArithRRI32 Asmblock.Psrliw rd rs imm       => Psrliw rd rs imm

+  | PArithRRI32 Asmblock.Pslliw rd rs imm       => Pslliw rd rs imm

+  | PArithRRI32 Asmblock.Psllil rd rs imm       => Psllil rd rs imm

+  | PArithRRI32 Asmblock.Psrlil rd rs imm       => Psrlil rd rs imm

+  | PArithRRI32 Asmblock.Psrail rd rs imm       => Psrail rd rs imm

+

+  (* RRI64 *)

+  | PArithRRI64 (Asmblock.Pcompil it) rd rs imm => Pcompil it rd rs imm

+  | PArithRRI64 Asmblock.Paddil rd rs imm       => Paddil rd rs imm

+  | PArithRRI64 Asmblock.Pandil rd rs imm       => Pandil rd rs imm

+  | PArithRRI64 Asmblock.Poril rd rs imm        => Poril rd rs imm

+  | PArithRRI64 Asmblock.Pxoril rd rs imm       => Pxoril rd rs imm

+

+  (** Load *)

+  | PLoadRRO Asmblock.Plb rd ra ofs   => Plb rd ra ofs

+  | PLoadRRO Asmblock.Plbu rd ra ofs  => Plbu rd ra ofs

+  | PLoadRRO Asmblock.Plh rd ra ofs   => Plh rd ra ofs

+  | PLoadRRO Asmblock.Plhu rd ra ofs  => Plhu rd ra ofs

+  | PLoadRRO Asmblock.Plw rd ra ofs   => Plw rd ra ofs

+  | PLoadRRO Asmblock.Plw_a rd ra ofs => Plw_a rd ra ofs

+  | PLoadRRO Asmblock.Pld rd ra ofs   => Pld rd ra ofs

+  | PLoadRRO Asmblock.Pld_a rd ra ofs => Pld_a rd ra ofs

+  | PLoadRRO Asmblock.Pfls rd ra ofs  => Pfls rd ra ofs

+  | PLoadRRO Asmblock.Pfld rd ra ofs  => Pfld rd ra ofs

+

+  (** Store *)

+  | PStoreRRO Asmblock.Psb rd ra ofs  => Psb rd ra ofs

+  | PStoreRRO Asmblock.Psh rd ra ofs => Psh rd ra ofs

+  | PStoreRRO Asmblock.Psw rd ra ofs => Psw rd ra ofs

+  | PStoreRRO Asmblock.Psw_a rd ra ofs => Psw_a rd ra ofs

+  | PStoreRRO Asmblock.Psd rd ra ofs => Psd rd ra ofs

+  | PStoreRRO Asmblock.Psd_a rd ra ofs => Psd_a rd ra ofs

+  | PStoreRRO Asmblock.Pfss rd ra ofs => Pfss rd ra ofs

+  | PStoreRRO Asmblock.Pfsd rd ra ofs => Pfss rd ra ofs

+

+  end.

+

+Section RELSEM.

+

+Definition code := list instruction.

+

+Fixpoint unfold_label (ll: list label) :=

+  match ll with

+  | nil => nil

+  | l :: ll => Plabel l :: unfold_label ll

+  end.

+

+Fixpoint unfold_body (lb: list basic) :=

+  match lb with

+  | nil => nil

+  | b :: lb => basic_to_instruction b :: unfold_body lb

+  end.

+

+Definition unfold_exit (oc: option control) :=

+  match oc with

+  | None => nil

+  | Some c => control_to_instruction c :: nil

+  end.

+

+Definition unfold_bblock (b: bblock) := unfold_label (header b) ++ unfold_body (body b) ++ unfold_exit (exit b).

+

+Fixpoint unfold (lb: bblocks) :=

+  match lb with

+  | nil => nil

+  | b :: lb => (unfold_bblock b) ++ unfold lb

+  end.

+

+Record function : Type := mkfunction { fn_sig: signature; fn_blocks: bblocks; fn_code: code; 

+                                       correct: unfold fn_blocks = fn_code }.

+

+Definition fundef := AST.fundef function.

+Definition program := AST.program fundef unit.

+Definition genv := Genv.t fundef unit.

+

+Definition function_proj (f: function) := Asmblock.mkfunction (fn_sig f) (fn_blocks f).

+

+(* 

+Definition fundef_proj (fu: fundef) : Asmblock.fundef := transf_fundef function_proj fu.

+

+Definition program_proj (p: program) : Asmblock.program := transform_program fundef_proj p.

+ *)

+

+Definition fundef_proj (fu: fundef) : Asmblock.fundef := 

+  match fu with

+  | Internal f => Internal (function_proj f)

+  | External ef => External ef

+  end.

+

+Definition globdef_proj (gd: globdef fundef unit) : globdef Asmblock.fundef unit :=

+  match gd with

+  | Gfun f => Gfun (fundef_proj f)

+  | Gvar gu => Gvar gu

+  end.

+

+Program Definition genv_trans (ge: genv) : Asmblock.genv :=

+  {|  Genv.genv_public := Genv.genv_public ge;

+      Genv.genv_symb := Genv.genv_symb ge;

+      Genv.genv_defs := PTree.map1 globdef_proj (Genv.genv_defs ge);

+      Genv.genv_next := Genv.genv_next ge |}.

+Next Obligation.

+  destruct ge. simpl in *. eauto.

+Qed. Next Obligation.

+  destruct ge; simpl in *.

+  rewrite PTree.gmap1 in H.

+  destruct (genv_defs ! b) eqn:GEN.

+  - eauto.

+  - discriminate.

+Qed. Next Obligation.

+  destruct ge; simpl in *.

+  eauto.

+Qed.

+

+Fixpoint prog_defs_proj (l: list (ident * globdef fundef unit))

+                          : list (ident * globdef Asmblock.fundef unit) :=

+  match l with

+  | nil => nil

+  | (i, gd) :: l => (i, globdef_proj gd) :: prog_defs_proj l

+  end.

+

+Definition program_proj (p: program) : Asmblock.program :=

+  {|  prog_defs := prog_defs_proj (prog_defs p);

+      prog_public := prog_public p;

+      prog_main := prog_main p

+  |}.

+

+End RELSEM.

+

+Definition semantics (p: program) := Asmblock.semantics (program_proj p).

+

+(** Determinacy of the [Asm] semantics. *)

+

+Lemma semantics_determinate: forall p, determinate (semantics p).

+Proof.

+  intros. apply semantics_determinate.

+Qed.

+

+(** transf_program *)

+

+Program Definition transf_function (f: Asmblock.function) : function :=

+     {| fn_sig := Asmblock.fn_sig f; fn_blocks := Asmblock.fn_blocks f; 

+        fn_code := unfold (Asmblock.fn_blocks f) |}.

+

+Lemma transf_function_proj: forall f, function_proj (transf_function f) = f.

+Proof.

+  intros f. destruct f as [sig blks]. unfold function_proj. simpl. auto.

+Qed.

+

+Definition transf_fundef (f: Asmblock.fundef) : fundef := 

+  match f with

+  | Internal f => Internal (transf_function f)

+  | External ef => External ef

+  end.

+

+Lemma transf_fundef_proj: forall f, fundef_proj (transf_fundef f) = f.

+Proof.

+  intros f. destruct f as [f|e]; simpl; auto.

+  rewrite transf_function_proj. auto.

+Qed.

+

+Definition transf_globdef (gd: globdef Asmblock.fundef unit) : globdef fundef unit :=

+  match gd with

+  | Gfun f => Gfun (transf_fundef f)

+  | Gvar gu => Gvar gu

+  end.

+

+Lemma transf_globdef_proj: forall gd, globdef_proj (transf_globdef gd) = gd.

+Proof.

+  intros gd. destruct gd as [f|v]; simpl; auto.

+  rewrite transf_fundef_proj; auto.

+Qed.

+

+Fixpoint transf_prog_defs (l: list (ident * globdef Asmblock.fundef unit))

+                            : list (ident * globdef fundef unit) :=

+  match l with

+  | nil => nil

+  | (i, gd) :: l => (i, transf_globdef gd) :: transf_prog_defs l

+  end.

+

+Lemma transf_prog_proj: forall p, prog_defs p = prog_defs_proj (transf_prog_defs (prog_defs p)).

+Proof.

+  intros p. destruct p as [defs pub main]. simpl.

+  induction defs; simpl; auto.

+  destruct a as [i gd]. simpl.

+  rewrite transf_globdef_proj.

+  congruence.

+Qed.

+

+Definition transf_program (p: Asmblock.program) : program :=

+  {|  prog_defs := transf_prog_defs (prog_defs p);

+      prog_public := prog_public p;

+      prog_main := prog_main p

+  |}.

+

+Definition match_prog (p: Asmblock.program) (tp: program) := (p = program_proj tp).

+

+Lemma asmblock_program_equals: forall (p1 p2: Asmblock.program),

+  prog_defs p1 = prog_defs p2 ->

+  prog_public p1 = prog_public p2 ->

+  prog_main p1 = prog_main p2 ->

+  p1 = p2.

+Proof.

+  intros. destruct p1. destruct p2. simpl in *. subst. auto.

+Qed.

+

+Lemma transf_program_match:

+  forall p tp, transf_program p = tp -> match_prog p tp.

+Proof.

+  intros p tp H. unfold match_prog.

+  unfold transf_program in H.

+  destruct tp as [tdefs tpub tmain]. inv H.

+  unfold program_proj. simpl. apply asmblock_program_equals; simpl; auto.

+  apply transf_prog_proj.

+Qed.

+

+Section PRESERVATION.

+

+Variable prog: Asmblock.program.

+Variable tprog: program.

+Hypothesis TRANSF: match_prog prog tprog.

+Let ge := Genv.globalenv prog.

+Let tge := Genv.globalenv tprog.

+

+Definition match_states (s1 s2: state) := s1 = s2.

+

+Theorem transf_program_correct:

+  forward_simulation (Asmblock.semantics prog) (semantics tprog).

+Proof.

+  inversion TRANSF. (* inv H0. *)

+  eapply forward_simulation_step with (match_states := match_states).

+  all: try (simpl; congruence).

+  - simpl. intros s1 H1. exists s1. split; auto. congruence.

+  - simpl. intros s1 t s1' H1 s2 H2. exists s1'. split.

+    + congruence.

+    + unfold match_states. auto.

+Qed.

+

+End PRESERVATION.
\ No newline at end of file
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v
index 253ae05d..58cc0f2c 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -1161,253 +1161,263 @@ Definition semantics (p: program) :=
 
 Axiom semantics_determinate: forall p, determinate (semantics p).
 
-(** Determinacy of the [Asm] semantics. *)
-
-(* TODO.
-
-Remark extcall_arguments_determ:
-  forall rs m sg args1 args2,
-  extcall_arguments rs m sg args1 -> extcall_arguments rs m sg args2 -> args1 = args2.
-Proof.
-  intros until m.
-  assert (A: forall l v1 v2,
-             extcall_arg rs m l v1 -> extcall_arg rs m l v2 -> v1 = v2).
-  { intros. inv H; inv H0; congruence. }
-  assert (B: forall p v1 v2,
-             extcall_arg_pair rs m p v1 -> extcall_arg_pair rs m p v2 -> v1 = v2).
-  { intros. inv H; inv H0. 
-    eapply A; eauto.
-    f_equal; eapply A; eauto. }
-  assert (C: forall ll vl1, list_forall2 (extcall_arg_pair rs m) ll vl1 ->
-             forall vl2, list_forall2 (extcall_arg_pair rs m) ll vl2 -> vl1 = vl2).
-  {
-    induction 1; intros vl2 EA; inv EA.
-    auto.
-    f_equal; eauto. }
-  intros. eapply C; eauto.
-Qed.
-
-Lemma semantics_determinate: forall p, determinate (semantics p).
-Proof.
-Ltac Equalities :=
-  match goal with
-  | [ H1: ?a = ?b, H2: ?a = ?c |- _ ] =>
-      rewrite H1 in H2; inv H2; Equalities
-  | _ => idtac
-  end.
-  intros; constructor; simpl; intros.
-- (* determ *)
-  inv H; inv H0; Equalities.
-  split. constructor. auto.
-  discriminate.
-  discriminate.
-  assert (vargs0 = vargs) by (eapply eval_builtin_args_determ; eauto). subst vargs0.
-  exploit external_call_determ. eexact H5. eexact H11. intros [A B].
-  split. auto. intros. destruct B; auto. subst. auto.
-  assert (args0 = args) by (eapply extcall_arguments_determ; eauto). subst args0.
-  exploit external_call_determ. eexact H3. eexact H8. intros [A B].
-  split. auto. intros. destruct B; auto. subst. auto.
-- (* trace length *)
-  red; intros. inv H; simpl.
-  omega.
-  eapply external_call_trace_length; eauto.
-  eapply external_call_trace_length; eauto.
-- (* initial states *)
-  inv H; inv H0. f_equal. congruence.
-- (* final no step *)
-  assert (NOTNULL: forall b ofs, Vnullptr <> Vptr b ofs).
-  { intros; unfold Vnullptr; destruct Archi.ptr64; congruence. }
-  inv H. unfold Vzero in H0. red; intros; red; intros.
-  inv H; rewrite H0 in *; eelim NOTNULL; eauto.
-- (* final states *)
-  inv H; inv H0. congruence.
-Qed.
-*)
-
-
-(*
-
-(** * Instruction dependencies, definition of a bundle 
-
-NOTE: this would be better to do this in an other file, e.g. Asmbundle ?
-
-*)
-
-(** NOTE: in all of these dependencies definitions, we do *not* consider PC.
-          PC dependencies are fullfilled by the above separation in bblocks
- *)
-
-(* (writereg i rd) holds if an instruction writes to a single register rd *)
-Inductive writereg: instruction -> preg -> Prop :=
-  | writereg_set:         forall rd rs,         writereg (Pset rd rs) rd
-  | writereg_get:         forall rd rs,         writereg (Pget rd rs) rd
-  | writereg_load:        forall i rd ra o,     writereg (PLoadRRO i rd ra o) rd
-  | writereg_arith_r:     forall i rd,          writereg (PArithR i rd) rd
-  | writereg_arith_rr:    forall i rd rs,       writereg (PArithRR i rd rs) rd
-  | writereg_arith_ri32:  forall i rd imm,      writereg (PArithRI32 i rd imm) rd
-  | writereg_arith_ri64:  forall i rd imm,      writereg (PArithRI64 i rd imm) rd
-  | writereg_arith_rrr:   forall i rd rs1 rs2,  writereg (PArithRRR i rd rs1 rs2) rd
-  | writereg_arith_rri32: forall i rd rs imm,   writereg (PArithRRI32 i rd rs imm) rd
-  | writereg_arith_rri64: forall i rd rs imm,   writereg (PArithRRI64 i rd rs imm) rd
-  .
-
-(* (nowrite i) holds if an instruction doesn't write to any register *)
-Inductive nowrite: instruction -> Prop :=
-  | nowrite_ret:                      nowrite Pret
-  | nowrite_call:   forall l,         nowrite (Pcall l)
-  | nowrite_goto:   forall l,         nowrite (Pgoto l)
-  | nowrite_jl:     forall l,         nowrite (Pj_l l)
-  | nowrite_cb:     forall bt r l,    nowrite (Pcb bt r l)
-  | nowrite_cbu:    forall bt r l,    nowrite (Pcbu bt r l)
-  | nowrite_store:  forall i rs ra o, nowrite (PStoreRRO i rs ra o)
-  | nowrite_label:  forall l,         nowrite (Plabel l)
-  .
-
-(* (readregs i lr) holds if an instruction reads from the register list lr, and only from it *)
-Inductive readregs: instruction -> list preg -> Prop :=
-  | readregs_set:         forall rd rs,         readregs (Pset rd rs) (IR rs::nil)
-  | readregs_get:         forall rd rs,         readregs (Pget rd rs) (rs::nil)
-  | readregs_cb:          forall bt r l,        readregs (Pcb bt r l) (IR r::nil)
-  | readregs_cbu:         forall bt r l,        readregs (Pcbu bt r l) (IR r::nil)
-  | readregs_load:        forall i rd ra o,     readregs (PLoadRRO i rd ra o) (IR ra::nil)
-  | readregs_store:       forall i rs ra o,     readregs (PStoreRRO i rs ra o) (IR rs::IR ra::nil)
-  | readregs_arith_rr:    forall i rd rs,       readregs (PArithRR i rd rs) (IR rs::nil)
-  | readregs_arith_rrr:   forall i rd rs1 rs2,  readregs (PArithRRR i rd rs1 rs2) (IR rs1::IR rs2::nil)
-  | readregs_arith_rri32: forall i rd rs imm,   readregs (PArithRRI32 i rd rs imm) (IR rs::nil)
-  | readregs_arith_rri64: forall i rd rs imm,   readregs (PArithRRI64 i rd rs imm) (IR rs::nil)
-  .
-
-(* (noread i) holds if an instruction doesn't read any register *)
-Inductive noread: instruction -> Prop :=
-  | noread_ret:                           noread Pret
-  | noread_call:        forall l,         noread (Pcall l)
-  | noread_goto:        forall l,         noread (Pgoto l)
-  | noread_jl:          forall l,         noread (Pj_l l)
-  | noread_arith_r:     forall i rd,      noread (PArithR i rd)
-  | noread_arith_ri32:  forall i rd imm,  noread (PArithRI32 i rd imm)
-  | noread_arith_ri64:  forall i rd imm,  noread (PArithRI64 i rd imm)
-  | noread_label:       forall l,         noread (Plabel l)
-  .
-
-(* (wawfree i i') holds if i::i' has no WAW dependency *)
-Inductive wawfree: instruction -> instruction -> Prop :=
-  | wawfree_write: forall i rs i' rs',
-      writereg i rs -> writereg i' rs' -> rs <> rs' -> wawfree i i'
-  | wawfree_free1: forall i i',
-      nowrite i -> wawfree i i'
-  | wawfree_free2: forall i i',
-      nowrite i' -> wawfree i i'
-  .
-
-(* (rawfree i i') holds if i::i' has no RAW dependency *)
-Inductive rawfree: instruction -> instruction -> Prop :=
-  | rawfree_single: forall i rd i' rs,
-      writereg i rd -> readregs i' (rs::nil) -> rd <> rs -> rawfree i i'
-  | rawfree_double: forall i rd i' rs rs',
-      writereg i rd -> readregs i' (rs::rs'::nil) -> rd <> rs -> rd <> rs' -> rawfree i i'
-  | rawfree_free1: forall i i',
-      nowrite i -> rawfree i i'
-  | rawfree_free2: forall i i',
-      noread i' -> rawfree i i'
-  .
-
-(* (depfree i i') holds if i::i' has no RAW or WAW dependency *)
-Inductive depfree: instruction -> instruction -> Prop :=
-  | mk_depfree: forall i i', rawfree i i' -> wawfree i i' -> depfree i i'.
-
-(* (depfreelist i c) holds if i::c has no RAW or WAW dependency _in regards to i_ *)
-Inductive depfreelist: instruction -> list instruction -> Prop :=
-  | depfreelist_nil:  forall i,
-      depfreelist i nil
-  | depfreelist_cons: forall i i' l,
-      depfreelist i l -> depfree i i' -> depfreelist i (i'::l)
-  .
-
-(* (depfreeall c) holds if c has no RAW or WAW dependency within itself *)
-Inductive depfreeall: list instruction -> Prop :=
-  | depfreeall_nil:
-      depfreeall nil
-  | depfreeall_cons: forall i l,
-      depfreeall l -> depfreelist i l -> depfreeall (i::l)
-  .
-
-(** NOTE: we do not verify the resource constraints of the bundles,
-          since not meeting them causes a failure when invoking the assembler *)
-
-(* A bundle is well formed if his body and exit do not have RAW or WAW dependencies *)
-Inductive wf_bundle: bblock -> Prop := 
-  | mk_wf_bundle: forall b, depfreeall (body b ++ unfold_exit (exit b)) -> wf_bundle b.
-
-Hint Constructors writereg nowrite readregs noread wawfree rawfree depfree depfreelist depfreeall wf_bundle.
-
-Record bundle := mk_bundle {
-  bd_block: bblock;
-  bd_correct: wf_bundle bd_block
-}.
-
-Definition bundles := list bundle.
-
-Definition unbundlize (lb: list bundle) := map bd_block lb.
-Definition unfold_bd (lb: list bundle) := unfold (map bd_block lb).
-
-Lemma unfold_bd_app: forall l l', unfold_bd (l ++ l') = unfold_bd l ++ unfold_bd l'.
-Proof.
-  intros l l'. unfold unfold_bd. rewrite map_app. rewrite unfold_app. auto.
-Qed.
-
-(** Some theorems on bundles construction *)
-Lemma bundle_empty_correct: wf_bundle empty_bblock.
-Proof.
-  constructor. auto.
-Qed.
-
-Definition empty_bundle := {| bd_block := empty_bblock; bd_correct := bundle_empty_correct |}.
-
-(** Bundlization. For now, we restrict ourselves to bundles containing 1 instruction *)
-
-Definition single_inst_block (i: instruction) := acc_block i empty_bblock.
-
-Fact single_inst_block_correct: forall i, wf_bundle (hd empty_bblock (single_inst_block i)).
-Proof.
-  intros i. unfold single_inst_block. unfold acc_block. destruct i.
-  all:  simpl; constructor; simpl; auto.
-Qed.
-
-Definition bundlize_inst (i: instruction) :=
-  {| bd_block := hd empty_bblock (single_inst_block i); bd_correct := single_inst_block_correct i |}.
-
-Lemma bundlize_inst_conserv: forall c, unfold (unbundlize (map bundlize_inst c)) = c.
-Proof.
-  induction c as [|i c]; simpl; auto.
-  rewrite IHc. destruct i; simpl; auto.
-Qed.
-
-Definition split_bblock (b: bblock) := map bundlize_inst (unfold_block b).
-
-Fixpoint bundlize (lb: list bblock) :=
-  match lb with
-  | nil => nil
-  | b :: lb => split_bblock b ++ bundlize lb
-  end.
-
-Lemma unfold_split_bblock: forall b, unfold_bd (split_bblock b) = unfold_block b.
-Proof.
-  intros b. unfold unfold_bd. unfold split_bblock. apply bundlize_inst_conserv.
-Qed.
-
-Theorem unfold_bundlize: forall lb, unfold_bd (bundlize lb) = unfold lb.
-Proof.
-  induction lb as [|b lb]; simpl; auto.
-  rewrite unfold_bd_app. rewrite IHlb. rewrite unfold_split_bblock. auto.
-Qed.
-
-Theorem unfold_bundlize_fold: forall c, unfold_bd (bundlize (fold c)) = c.
-Proof.
-  intros. rewrite unfold_bundlize. rewrite unfold_fold. auto.
-Qed.
-
-Record function : Type := mkfunction { fn_sig: signature; fn_bundles: bundles }.
-Definition fn_code := (fun (f: function) => unfold_bd (fn_bundles f)).
-Definition fundef := AST.fundef function.
-Definition program := AST.program fundef unit.
+Definition data_preg (r: preg) : bool :=

+  match r with

+  | RA  => false

+  | IR GPR31 => false

+  | IR GPR8 => false

+  | IR _   => true

+  | FR _   => true

+  | PC     => false

+  end.

+

+(** Determinacy of the [Asm] semantics. *)

+

+(* TODO.

+

+Remark extcall_arguments_determ:

+  forall rs m sg args1 args2,

+  extcall_arguments rs m sg args1 -> extcall_arguments rs m sg args2 -> args1 = args2.

+Proof.

+  intros until m.

+  assert (A: forall l v1 v2,

+             extcall_arg rs m l v1 -> extcall_arg rs m l v2 -> v1 = v2).

+  { intros. inv H; inv H0; congruence. }

+  assert (B: forall p v1 v2,

+             extcall_arg_pair rs m p v1 -> extcall_arg_pair rs m p v2 -> v1 = v2).

+  { intros. inv H; inv H0. 

+    eapply A; eauto.

+    f_equal; eapply A; eauto. }

+  assert (C: forall ll vl1, list_forall2 (extcall_arg_pair rs m) ll vl1 ->

+             forall vl2, list_forall2 (extcall_arg_pair rs m) ll vl2 -> vl1 = vl2).

+  {

+    induction 1; intros vl2 EA; inv EA.

+    auto.

+    f_equal; eauto. }

+  intros. eapply C; eauto.

+Qed.

+

+Lemma semantics_determinate: forall p, determinate (semantics p).

+Proof.

+Ltac Equalities :=

+  match goal with

+  | [ H1: ?a = ?b, H2: ?a = ?c |- _ ] =>

+      rewrite H1 in H2; inv H2; Equalities

+  | _ => idtac

+  end.

+  intros; constructor; simpl; intros.

+- (* determ *)

+  inv H; inv H0; Equalities.

+  split. constructor. auto.

+  discriminate.

+  discriminate.

+  assert (vargs0 = vargs) by (eapply eval_builtin_args_determ; eauto). subst vargs0.

+  exploit external_call_determ. eexact H5. eexact H11. intros [A B].

+  split. auto. intros. destruct B; auto. subst. auto.

+  assert (args0 = args) by (eapply extcall_arguments_determ; eauto). subst args0.

+  exploit external_call_determ. eexact H3. eexact H8. intros [A B].

+  split. auto. intros. destruct B; auto. subst. auto.

+- (* trace length *)

+  red; intros. inv H; simpl.

+  omega.

+  eapply external_call_trace_length; eauto.

+  eapply external_call_trace_length; eauto.

+- (* initial states *)

+  inv H; inv H0. f_equal. congruence.

+- (* final no step *)

+  assert (NOTNULL: forall b ofs, Vnullptr <> Vptr b ofs).

+  { intros; unfold Vnullptr; destruct Archi.ptr64; congruence. }

+  inv H. unfold Vzero in H0. red; intros; red; intros.

+  inv H; rewrite H0 in *; eelim NOTNULL; eauto.

+- (* final states *)

+  inv H; inv H0. congruence.

+Qed.

+*)

+

+

+(*

+

+(** * Instruction dependencies, definition of a bundle 

+

+NOTE: this would be better to do this in an other file, e.g. Asmbundle ?

+

+*)

+

+(** NOTE: in all of these dependencies definitions, we do *not* consider PC.

+          PC dependencies are fullfilled by the above separation in bblocks

+ *)

+

+(* (writereg i rd) holds if an instruction writes to a single register rd *)

+Inductive writereg: instruction -> preg -> Prop :=

+  | writereg_set:         forall rd rs,         writereg (Pset rd rs) rd

+  | writereg_get:         forall rd rs,         writereg (Pget rd rs) rd

+  | writereg_load:        forall i rd ra o,     writereg (PLoadRRO i rd ra o) rd

+  | writereg_arith_r:     forall i rd,          writereg (PArithR i rd) rd

+  | writereg_arith_rr:    forall i rd rs,       writereg (PArithRR i rd rs) rd

+  | writereg_arith_ri32:  forall i rd imm,      writereg (PArithRI32 i rd imm) rd

+  | writereg_arith_ri64:  forall i rd imm,      writereg (PArithRI64 i rd imm) rd

+  | writereg_arith_rrr:   forall i rd rs1 rs2,  writereg (PArithRRR i rd rs1 rs2) rd

+  | writereg_arith_rri32: forall i rd rs imm,   writereg (PArithRRI32 i rd rs imm) rd

+  | writereg_arith_rri64: forall i rd rs imm,   writereg (PArithRRI64 i rd rs imm) rd

+  .

+

+(* (nowrite i) holds if an instruction doesn't write to any register *)

+Inductive nowrite: instruction -> Prop :=

+  | nowrite_ret:                      nowrite Pret

+  | nowrite_call:   forall l,         nowrite (Pcall l)

+  | nowrite_goto:   forall l,         nowrite (Pgoto l)

+  | nowrite_jl:     forall l,         nowrite (Pj_l l)

+  | nowrite_cb:     forall bt r l,    nowrite (Pcb bt r l)

+  | nowrite_cbu:    forall bt r l,    nowrite (Pcbu bt r l)

+  | nowrite_store:  forall i rs ra o, nowrite (PStoreRRO i rs ra o)

+  | nowrite_label:  forall l,         nowrite (Plabel l)

+  .

+

+(* (readregs i lr) holds if an instruction reads from the register list lr, and only from it *)

+Inductive readregs: instruction -> list preg -> Prop :=

+  | readregs_set:         forall rd rs,         readregs (Pset rd rs) (IR rs::nil)

+  | readregs_get:         forall rd rs,         readregs (Pget rd rs) (rs::nil)

+  | readregs_cb:          forall bt r l,        readregs (Pcb bt r l) (IR r::nil)

+  | readregs_cbu:         forall bt r l,        readregs (Pcbu bt r l) (IR r::nil)

+  | readregs_load:        forall i rd ra o,     readregs (PLoadRRO i rd ra o) (IR ra::nil)

+  | readregs_store:       forall i rs ra o,     readregs (PStoreRRO i rs ra o) (IR rs::IR ra::nil)

+  | readregs_arith_rr:    forall i rd rs,       readregs (PArithRR i rd rs) (IR rs::nil)

+  | readregs_arith_rrr:   forall i rd rs1 rs2,  readregs (PArithRRR i rd rs1 rs2) (IR rs1::IR rs2::nil)

+  | readregs_arith_rri32: forall i rd rs imm,   readregs (PArithRRI32 i rd rs imm) (IR rs::nil)

+  | readregs_arith_rri64: forall i rd rs imm,   readregs (PArithRRI64 i rd rs imm) (IR rs::nil)

+  .

+

+(* (noread i) holds if an instruction doesn't read any register *)

+Inductive noread: instruction -> Prop :=

+  | noread_ret:                           noread Pret

+  | noread_call:        forall l,         noread (Pcall l)

+  | noread_goto:        forall l,         noread (Pgoto l)

+  | noread_jl:          forall l,         noread (Pj_l l)

+  | noread_arith_r:     forall i rd,      noread (PArithR i rd)

+  | noread_arith_ri32:  forall i rd imm,  noread (PArithRI32 i rd imm)

+  | noread_arith_ri64:  forall i rd imm,  noread (PArithRI64 i rd imm)

+  | noread_label:       forall l,         noread (Plabel l)

+  .

+

+(* (wawfree i i') holds if i::i' has no WAW dependency *)

+Inductive wawfree: instruction -> instruction -> Prop :=

+  | wawfree_write: forall i rs i' rs',

+      writereg i rs -> writereg i' rs' -> rs <> rs' -> wawfree i i'

+  | wawfree_free1: forall i i',

+      nowrite i -> wawfree i i'

+  | wawfree_free2: forall i i',

+      nowrite i' -> wawfree i i'

+  .

+

+(* (rawfree i i') holds if i::i' has no RAW dependency *)

+Inductive rawfree: instruction -> instruction -> Prop :=

+  | rawfree_single: forall i rd i' rs,

+      writereg i rd -> readregs i' (rs::nil) -> rd <> rs -> rawfree i i'

+  | rawfree_double: forall i rd i' rs rs',

+      writereg i rd -> readregs i' (rs::rs'::nil) -> rd <> rs -> rd <> rs' -> rawfree i i'

+  | rawfree_free1: forall i i',

+      nowrite i -> rawfree i i'

+  | rawfree_free2: forall i i',

+      noread i' -> rawfree i i'

+  .

+

+(* (depfree i i') holds if i::i' has no RAW or WAW dependency *)

+Inductive depfree: instruction -> instruction -> Prop :=

+  | mk_depfree: forall i i', rawfree i i' -> wawfree i i' -> depfree i i'.

+

+(* (depfreelist i c) holds if i::c has no RAW or WAW dependency _in regards to i_ *)

+Inductive depfreelist: instruction -> list instruction -> Prop :=

+  | depfreelist_nil:  forall i,

+      depfreelist i nil

+  | depfreelist_cons: forall i i' l,

+      depfreelist i l -> depfree i i' -> depfreelist i (i'::l)

+  .

+

+(* (depfreeall c) holds if c has no RAW or WAW dependency within itself *)

+Inductive depfreeall: list instruction -> Prop :=

+  | depfreeall_nil:

+      depfreeall nil

+  | depfreeall_cons: forall i l,

+      depfreeall l -> depfreelist i l -> depfreeall (i::l)

+  .

+

+(** NOTE: we do not verify the resource constraints of the bundles,

+          since not meeting them causes a failure when invoking the assembler *)

+

+(* A bundle is well formed if his body and exit do not have RAW or WAW dependencies *)

+Inductive wf_bundle: bblock -> Prop := 

+  | mk_wf_bundle: forall b, depfreeall (body b ++ unfold_exit (exit b)) -> wf_bundle b.

+

+Hint Constructors writereg nowrite readregs noread wawfree rawfree depfree depfreelist depfreeall wf_bundle.

+

+Record bundle := mk_bundle {

+  bd_block: bblock;

+  bd_correct: wf_bundle bd_block

+}.

+

+Definition bundles := list bundle.

+

+Definition unbundlize (lb: list bundle) := map bd_block lb.

+Definition unfold_bd (lb: list bundle) := unfold (map bd_block lb).

+

+Lemma unfold_bd_app: forall l l', unfold_bd (l ++ l') = unfold_bd l ++ unfold_bd l'.

+Proof.

+  intros l l'. unfold unfold_bd. rewrite map_app. rewrite unfold_app. auto.

+Qed.

+

+(** Some theorems on bundles construction *)

+Lemma bundle_empty_correct: wf_bundle empty_bblock.

+Proof.

+  constructor. auto.

+Qed.

+

+Definition empty_bundle := {| bd_block := empty_bblock; bd_correct := bundle_empty_correct |}.

+

+(** Bundlization. For now, we restrict ourselves to bundles containing 1 instruction *)

+

+Definition single_inst_block (i: instruction) := acc_block i empty_bblock.

+

+Fact single_inst_block_correct: forall i, wf_bundle (hd empty_bblock (single_inst_block i)).

+Proof.

+  intros i. unfold single_inst_block. unfold acc_block. destruct i.

+  all:  simpl; constructor; simpl; auto.

+Qed.

+

+Definition bundlize_inst (i: instruction) :=

+  {| bd_block := hd empty_bblock (single_inst_block i); bd_correct := single_inst_block_correct i |}.

+

+Lemma bundlize_inst_conserv: forall c, unfold (unbundlize (map bundlize_inst c)) = c.

+Proof.

+  induction c as [|i c]; simpl; auto.

+  rewrite IHc. destruct i; simpl; auto.

+Qed.

+

+Definition split_bblock (b: bblock) := map bundlize_inst (unfold_block b).

+

+Fixpoint bundlize (lb: list bblock) :=

+  match lb with

+  | nil => nil

+  | b :: lb => split_bblock b ++ bundlize lb

+  end.

+

+Lemma unfold_split_bblock: forall b, unfold_bd (split_bblock b) = unfold_block b.

+Proof.

+  intros b. unfold unfold_bd. unfold split_bblock. apply bundlize_inst_conserv.

+Qed.

+

+Theorem unfold_bundlize: forall lb, unfold_bd (bundlize lb) = unfold lb.

+Proof.

+  induction lb as [|b lb]; simpl; auto.

+  rewrite unfold_bd_app. rewrite IHlb. rewrite unfold_split_bblock. auto.

+Qed.

+

+Theorem unfold_bundlize_fold: forall c, unfold_bd (bundlize (fold c)) = c.

+Proof.

+  intros. rewrite unfold_bundlize. rewrite unfold_fold. auto.

+Qed.

+

+Record function : Type := mkfunction { fn_sig: signature; fn_bundles: bundles }.

+Definition fn_code := (fun (f: function) => unfold_bd (fn_bundles f)).

+Definition fundef := AST.fundef function.

+Definition program := AST.program fundef unit.

 *)
\ No newline at end of file
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index f9f38b18..4bb23e8e 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -838,7 +838,7 @@ Definition transl_basic_code' (f: Machblock.function) (il: list Machblock.basic_
   otherwise the offset part of the [PC] code pointer could wrap
   around, leading to incorrect executions. *)
 
-Obligation Tactic := bblock_auto_correct.
+Local Obligation Tactic := bblock_auto_correct.
 
 Program Definition gen_bblock_noctl (hd: list label) (c: list basic) :=
   match c with
diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v
index d98e4cd3..de00218e 100644
--- a/mppa_k1c/Asmblockgenproof.v
+++ b/mppa_k1c/Asmblockgenproof.v
@@ -22,12 +22,11 @@ Require Import Asmblockgen.
 Definition match_prog (p: Machblock.program) (tp: Asmblock.program) :=
   match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp.
 
-(* Lemma transf_program_match:
+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.
 
diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v
index 6b6531c3..7b753506 100644
--- a/mppa_k1c/Asmgen.v
+++ b/mppa_k1c/Asmgen.v
@@ -15,826 +15,12 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-(** Translation from Mach to RISC-V assembly language *)
+Require Import Mach Asm Asmblockgen Machblockgen.
+Require Import Errors.
 
-Require Archi.
-Require Import Coqlib Errors.
-Require Import AST Integers Floats Memdata.
-Require Import Op Locations Mach Asm.
-
-Local Open Scope string_scope.
 Local Open Scope error_monad_scope.
 
-(** The code generation functions take advantage of several
-  characteristics of the [Mach] code generated by earlier passes of the
-  compiler, mostly that argument and result registers are of the correct
-  types.  These properties are true by construction, but it's easier to
-  recheck them during code generation and fail if they do not hold. *)
-
-(** 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 IR mr => OK mr | _ => Error(msg "Asmgen.freg_of") end.
-
-(*
-(** Decomposition of 32-bit integer constants.  They are split into either
-  small signed immediates that fit in 12-bits, or, if they do not fit,
-  into a (20-bit hi, 12-bit lo) pair where lo is sign-extended. *)
-
-*)
-Inductive immed32 : Type :=
-  | Imm32_single (imm: int).
-
-Definition make_immed32 (val: int) := Imm32_single val.
-
-(** Likewise, for 64-bit integer constants. *)
-Inductive immed64 : Type :=
-  | Imm64_single (imm: int64)
-.
-
-(* For now, let's suppose all instructions of K1c can handle 64-bits immediate *)
-Definition make_immed64 (val: int64) := Imm64_single val.
-
-Notation "a ::i b" := (cons (A:=instruction) a b) (at level 49, right associativity).
-
-(** Smart constructors for arithmetic operations involving
-  a 32-bit or 64-bit integer constant.  Depending on whether the
-  constant fits in 12 bits or not, one or several instructions
-  are generated as required to perform the operation
-  and prepended to the given instruction sequence [k]. *)
-
-Definition loadimm32 (r: ireg) (n: int) (k: code) :=
-  match make_immed32 n with
-  | Imm32_single imm => Pmake r imm ::i k
-  end.
-
-Definition opimm32 (op: arith_name_rrr)
-                   (opimm: arith_name_rri32)
-                   (rd rs: ireg) (n: int) (k: code) :=
-  match make_immed32 n with
-  | Imm32_single imm => opimm rd rs imm ::i k
-  end.
-
-Definition addimm32 := opimm32 Paddw Paddiw.
-Definition andimm32 := opimm32 Pandw Pandiw.
-Definition orimm32  := opimm32 Porw Poriw.
-Definition xorimm32 := opimm32 Pxorw Pxoriw.
-(*
-Definition sltimm32 := opimm32 Psltw Psltiw.
-Definition sltuimm32 := opimm32 Psltuw Psltiuw.
-*)
-
-Definition loadimm64 (r: ireg) (n: int64) (k: code) :=
-  match make_immed64 n with
-  | Imm64_single imm => Pmakel r imm ::i k
-  end.
-
-Definition opimm64 (op: arith_name_rrr)
-                   (opimm: arith_name_rri64)
-                   (rd rs: ireg) (n: int64) (k: code) :=
-  match make_immed64 n with
-  | Imm64_single imm => opimm rd rs imm ::i k
-end.
-
-Definition addimm64 := opimm64 Paddl Paddil.
-Definition orimm64  := opimm64 Porl  Poril.
-Definition andimm64 := opimm64 Pandl Pandil.
-Definition xorimm64 := opimm64 Pxorl  Pxoril.
-
-(*
-Definition sltimm64 := opimm64 Psltl Psltil.
-Definition sltuimm64 := opimm64 Psltul Psltiul.
-*)
-
-Definition cast32signed (rd rs: ireg) (k: code) := 
-  if (ireg_eq rd rs)
-    then Pcvtw2l rd ::i k
-    else Pmvw2l rd rs ::i k
-  .
-
-Definition addptrofs (rd rs: ireg) (n: ptrofs) (k: code) :=
-  if Ptrofs.eq_dec n Ptrofs.zero then
-    Pmv rd rs ::i k
-  else
-    addimm64 rd rs (Ptrofs.to_int64 n) k.
-
-(** Translation of conditional branches. *)
-
-Definition transl_comp
-    (c: comparison) (s: signedness) (r1 r2: ireg) (lbl: label) (k: code) : list instruction :=
-  Pcompw (itest_for_cmp c s) RTMP r1 r2 ::i Pcb BTwnez RTMP lbl ::i k.
-
-Definition transl_compl
-    (c: comparison) (s: signedness) (r1 r2: ireg) (lbl: label) (k: code) : list instruction :=
-  Pcompl (itest_for_cmp c s) RTMP r1 r2 ::i Pcb BTwnez RTMP lbl ::i k.
-
-Definition select_comp (n: int) (c: comparison) : option comparison :=
-  if Int.eq n Int.zero then
-    match c with
-    | Ceq => Some Ceq
-    | Cne => Some Cne
-    | _   => None
-    end
-  else
-    None
-  .
-
-Definition transl_opt_compuimm
-    (n: int) (c: comparison) (r1: ireg) (lbl: label) (k: code) : list instruction :=
-  match select_comp n c with
-  | Some Ceq => Pcbu BTweqz r1 lbl ::i k
-  | Some Cne => Pcbu BTwnez r1 lbl ::i k
-  | Some _   => nil (* Never happens *)
-  | None     => loadimm32 RTMP n (transl_comp c Unsigned r1 RTMP lbl k)
-  end
-  .
-
-Definition select_compl (n: int64) (c: comparison) : option comparison :=
-  if Int64.eq n Int64.zero then
-    match c with
-    | Ceq => Some Ceq
-    | Cne => Some Cne
-    | _   => None
-    end
-  else
-    None
-  .
-
-Definition transl_opt_compluimm
-    (n: int64) (c: comparison) (r1: ireg) (lbl: label) (k: code) : list instruction :=
-  match select_compl n c with
-  | Some Ceq => Pcbu BTdeqz r1 lbl ::i k
-  | Some Cne => Pcbu BTdnez r1 lbl ::i k
-  | Some _   => nil (* Never happens *)
-  | None     => loadimm64 RTMP n (transl_compl c Unsigned r1 RTMP lbl k)
-  end
-  .
-
-Definition transl_cbranch
-    (cond: condition) (args: list mreg) (lbl: label) (k: code) : res (list instruction ) :=
-  match cond, args with
-  | Ccompuimm c n, a1 :: nil =>
-      do r1 <- ireg_of a1;
-      OK (transl_opt_compuimm n c r1 lbl k)
-  | Ccomp c, a1 :: a2 :: nil =>
-      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (transl_comp c Signed r1 r2 lbl k)
-  | Ccompu c, a1 :: a2 :: nil =>
-      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (transl_comp c Unsigned r1 r2 lbl k)
-  | Ccompimm c n, a1 :: nil =>
-      do r1 <- ireg_of a1;
-      OK (if Int.eq n Int.zero then
-            Pcb (btest_for_cmpswz c) r1 lbl ::i k
-          else
-            loadimm32 RTMP n (transl_comp c Signed r1 RTMP lbl k)
-         )
-  | Ccompluimm c n, a1 :: nil =>
-      do r1 <- ireg_of a1;
-      OK (transl_opt_compluimm n c r1 lbl k)
-  | Ccompl c, a1 :: a2 :: nil =>
-      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (transl_compl c Signed r1 r2 lbl k)
-  | Ccomplu c, a1 :: a2 :: nil =>
-      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (transl_compl c Unsigned r1 r2 lbl k)
-  | Ccomplimm c n, a1 :: nil =>
-      do r1 <- ireg_of a1;
-      OK (if Int64.eq n Int64.zero then
-            Pcb (btest_for_cmpsdz c) r1 lbl ::i k
-          else
-            loadimm64 RTMP n (transl_compl c Signed r1 RTMP lbl k)
-         )
-(*| Ccompf c, f1 :: f2 :: nil =>
-      do r1 <- freg_of f1; do r2 <- freg_of f2;
-      let (insn, normal) := transl_cond_float c rd r1 r2 in
-      OK (insn :: if normal then k else Pxoriw rd rd Int.one :: k)
-  | Cnotcompf c, f1 :: f2 :: nil =>
-      do r1 <- freg_of f1; do r2 <- freg_of f2;
-      let (insn, normal) := transl_cond_float c rd r1 r2 in
-      OK (insn :: if normal then Pxoriw rd rd Int.one :: k else k)
-  | Ccompfs c, f1 :: f2 :: nil =>
-      do r1 <- freg_of f1; do r2 <- freg_of f2;
-      let (insn, normal) := transl_cond_single c rd r1 r2 in
-      OK (insn :: if normal then k else Pxoriw rd rd Int.one :: k)
-  | Cnotcompfs c, f1 :: f2 :: nil =>
-      do r1 <- freg_of f1; do r2 <- freg_of f2;
-      let (insn, normal) := transl_cond_single c rd r1 r2 in
-      OK (insn :: if normal then Pxoriw rd rd Int.one :: k else k)
-*)| _, _ =>
-      Error(msg "Asmgen.transl_cbranch")
-  end.
-
-(** Translation of a condition operator.  The generated code sets the
-  [rd] target register to 0 or 1 depending on the truth value of the
-  condition. *)
-
-Definition transl_cond_int32s (cmp: comparison) (rd r1 r2: ireg) (k: code) :=
-  Pcompw (itest_for_cmp cmp Signed) rd r1 r2 ::i k.
-
-Definition transl_cond_int32u (cmp: comparison) (rd r1 r2: ireg) (k: code) :=
-  Pcompw (itest_for_cmp cmp Unsigned) rd r1 r2 ::i k.
-
-Definition transl_cond_int64s (cmp: comparison) (rd r1 r2: ireg) (k: code) :=
-  Pcompl (itest_for_cmp cmp Signed) rd r1 r2 ::i k.
-
-Definition transl_cond_int64u (cmp: comparison) (rd r1 r2: ireg) (k: code) :=
-  Pcompl (itest_for_cmp cmp Unsigned) rd r1 r2 ::i k.
-
-Definition transl_condimm_int32s (cmp: comparison) (rd r1: ireg) (n: int) (k: code) :=
-  Pcompiw (itest_for_cmp cmp Signed) rd r1 n ::i k.
-
-Definition transl_condimm_int32u (cmp: comparison) (rd r1: ireg) (n: int) (k: code) :=
-  Pcompiw (itest_for_cmp cmp Unsigned) rd r1 n ::i k.
-
-Definition transl_condimm_int64s (cmp: comparison) (rd r1: ireg) (n: int64) (k: code) :=
-  Pcompil (itest_for_cmp cmp Signed) rd r1 n ::i k.
-
-Definition transl_condimm_int64u (cmp: comparison) (rd r1: ireg) (n: int64) (k: code) :=
-  Pcompil (itest_for_cmp cmp Unsigned) rd r1 n ::i k.
-
-Definition transl_cond_op
-           (cond: condition) (rd: ireg) (args: list mreg) (k: code) :=
-  match cond, args with
-  | Ccomp c, a1 :: a2 :: nil =>
-      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (transl_cond_int32s c rd r1 r2 k)
-  | Ccompu c, a1 :: a2 :: nil =>
-      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (transl_cond_int32u c rd r1 r2 k)
-  | Ccompimm c n, a1 :: nil =>
-      do r1 <- ireg_of a1;
-      OK (transl_condimm_int32s c rd r1 n k)
-  | Ccompuimm c n, a1 :: nil =>
-      do r1 <- ireg_of a1;
-      OK (transl_condimm_int32u c rd r1 n k)
-  | Ccompl c, a1 :: a2 :: nil =>
-      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (transl_cond_int64s c rd r1 r2 k)
-  | Ccomplu c, a1 :: a2 :: nil =>
-      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (transl_cond_int64u c rd r1 r2 k)
-  | Ccomplimm c n, a1 :: nil =>
-      do r1 <- ireg_of a1;
-      OK (transl_condimm_int64s c rd r1 n k)
-  | Ccompluimm c n, a1 :: nil =>
-      do r1 <- ireg_of a1;
-      OK (transl_condimm_int64u c rd r1 n k)
-(*| Ccompf c, f1 :: f2 :: nil =>
-      do r1 <- freg_of f1; do r2 <- freg_of f2;
-      let (insn, normal) := transl_cond_float c rd r1 r2 in
-      OK (insn :: if normal then k else Pxoriw rd rd Int.one :: k)
-  | Cnotcompf c, f1 :: f2 :: nil =>
-      do r1 <- freg_of f1; do r2 <- freg_of f2;
-      let (insn, normal) := transl_cond_float c rd r1 r2 in
-      OK (insn :: if normal then Pxoriw rd rd Int.one :: k else k)
-  | Ccompfs c, f1 :: f2 :: nil =>
-      do r1 <- freg_of f1; do r2 <- freg_of f2;
-      let (insn, normal) := transl_cond_single c rd r1 r2 in
-      OK (insn :: if normal then k else Pxoriw rd rd Int.one :: k)
-  | Cnotcompfs c, f1 :: f2 :: nil =>
-      do r1 <- freg_of f1; do r2 <- freg_of f2;
-      let (insn, normal) := transl_cond_single c rd r1 r2 in
-      OK (insn :: if normal then Pxoriw rd rd Int.one :: k else k)
-*)| _, _ =>
-      Error(msg "Asmgen.transl_cond_op")
-end.
-
-(** Translation of the arithmetic operation [r <- 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 (Pmv r a ::i 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 Pfcvtdw rd GPR0 :: k
-          else Ploadfi rd f :: k)
-  | Osingleconst f, nil =>
-      do rd <- freg_of res;
-      OK (if Float32.eq_dec f Float32.zero
-          then Pfcvtsw rd GPR0 :: k
-          else Ploadsi rd f :: k)
-*)| Oaddrsymbol s ofs, nil =>
-      do rd <- ireg_of res;
-      OK (if Archi.pic_code tt && negb (Ptrofs.eq ofs Ptrofs.zero)
-          then Ploadsymbol rd s Ptrofs.zero ::i addptrofs rd rd ofs k
-          else Ploadsymbol rd s ofs ::i k)
-  | Oaddrstack n, nil =>
-      do rd <- ireg_of res;
-      OK (addptrofs rd SP n k)
-
-  | Ocast8signed, a1 :: nil =>
-      do rd <- ireg_of res; do rs <- ireg_of a1;
-      OK (Pslliw rd rs (Int.repr 24) ::i Psraiw rd rd (Int.repr 24) ::i k)
-  | Ocast16signed, a1 :: nil =>
-      do rd <- ireg_of res; do rs <- ireg_of a1;
-      OK (Pslliw rd rs (Int.repr 16) ::i Psraiw rd rd (Int.repr 16) ::i k)
-  | Oadd, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Paddw rd rs1 rs2 ::i k)
-  | Oaddimm n, a1 :: nil =>
-      do rd  <- ireg_of res; do rs <- ireg_of a1;
-      OK (addimm32 rd rs n k)
-  | Oneg, a1 :: nil =>
-      do rd  <- ireg_of res; do rs <- ireg_of a1;
-      OK (Pnegw rd rs ::i k)
-  | Osub, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Psubw rd rs1 rs2 ::i k)
-  | Omul, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Pmulw rd rs1 rs2 ::i k)
-(*| Omulhs, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Pmulhw rd rs1 rs2 :: k)
-  | Omulhu, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Pmulhuw rd rs1 rs2 :: k)
-  | Odiv, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Pdivw rd rs1 rs2 :: k)
-  | Odivu, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Pdivuw rd rs1 rs2 :: k)
-  | Omod, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Premw rd rs1 rs2 :: k)
-  | Omodu, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Premuw rd rs1 rs2 :: k)
-*)| Oand, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Pandw rd rs1 rs2 ::i k)
-  | Oandimm n, a1 :: nil =>
-      do rd  <- ireg_of res; do rs <- ireg_of a1;
-      OK (andimm32 rd rs n k)
-  | Oor, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Porw rd rs1 rs2 ::i k)
-  | Oorimm n, a1 :: nil =>
-      do rd  <- ireg_of res; do rs <- ireg_of a1;
-      OK (orimm32 rd rs n k)
-  | Oxor, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Pxorw rd rs1 rs2 ::i k)
-  | Oxorimm n, a1 :: nil =>
-      do rd  <- ireg_of res; do rs <- ireg_of a1;
-      OK (xorimm32 rd rs n k)
-  | Oshl, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Psllw rd rs1 rs2 ::i k)
-  | Oshlimm n, a1 :: nil =>
-      do rd <- ireg_of res; do rs <- ireg_of a1;
-      OK (Pslliw rd rs n ::i k)
-  | Oshr, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Psraw rd rs1 rs2 ::i k)
-  | Oshrimm n, a1 :: nil =>
-      do rd <- ireg_of res; do rs <- ireg_of a1;
-      OK (Psraiw rd rs n ::i k)
-  | Oshru, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Psrlw rd rs1 rs2 ::i k)
-  | Oshruimm n, a1 :: nil =>
-      do rd <- ireg_of res; do rs <- ireg_of a1;
-      OK (Psrliw rd rs n ::i k)
-  | Oshrximm n, a1 :: nil =>
-      do rd <- ireg_of res; do rs <- ireg_of a1;
-      OK (if Int.eq n Int.zero then Pmv rd rs ::i k else
-          Psraiw GPR31 rs (Int.repr 31) ::i
-          Psrliw GPR31 GPR31 (Int.sub Int.iwordsize n) ::i
-          Paddw GPR31 rs GPR31 ::i
-          Psraiw rd GPR31 n ::i k)
-
-  (* [Omakelong], [Ohighlong]  should not occur *)
-  | Olowlong, a1 :: nil =>
-      do rd <- ireg_of res; do rs <- ireg_of a1;
-      OK (Pcvtl2w rd rs ::i k)  
-  | Ocast32signed, a1 :: nil =>
-      do rd <- ireg_of res; do rs <- ireg_of a1;
-      OK (cast32signed rd rs k)
-  | Ocast32unsigned, a1 :: nil =>
-      do rd <- ireg_of res; do rs <- ireg_of a1;
-      assertion (ireg_eq rd rs);
-      OK (Pcvtw2l rd ::i Psllil rd rd (Int.repr 32) ::i Psrlil rd rd (Int.repr 32) ::i k)
-  | Oaddl, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Paddl rd rs1 rs2 ::i k)
-  | Oaddlimm n, a1 :: nil =>
-      do rd  <- ireg_of res; do rs <- ireg_of a1;
-      OK (addimm64 rd rs n k)
-  | Onegl, a1 :: nil =>
-      do rd  <- ireg_of res; do rs <- ireg_of a1;
-      OK (Pnegl rd rs ::i k)
-  | Osubl, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Psubl rd rs1 rs2 ::i k)
-  | Omull, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Pmull rd rs1 rs2 ::i k)
-(*| Omullhs, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Pmulhl rd rs1 rs2 :: k)
-  | Omullhu, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Pmulhul rd rs1 rs2 :: k)
-  | Odivl, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Pdivl rd rs1 rs2 :: k)
-  | Odivlu, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Pdivul rd rs1 rs2 :: k)
-  | Omodl, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Preml rd rs1 rs2 :: k)
-  | Omodlu, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Premul rd rs1 rs2 :: k)
-*)| Oandl, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Pandl rd rs1 rs2 ::i k)
-  | Oandlimm n, a1 :: nil =>
-      do rd  <- ireg_of res; do rs <- ireg_of a1;
-      OK (andimm64 rd rs n k)
-  | Oorl, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Porl rd rs1 rs2 ::i k)
-  | Oorlimm n, a1 :: nil =>
-      do rd  <- ireg_of res; do rs <- ireg_of a1;
-      OK (orimm64 rd rs n k)
-  | Oxorl, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Pxorl rd rs1 rs2 ::i k)
-  | Oxorlimm n, a1 :: nil =>
-      do rd  <- ireg_of res; do rs <- ireg_of a1;
-      OK (xorimm64 rd rs n k)
-  | Oshll, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Pslll rd rs1 rs2 ::i k)
-  | Oshllimm n, a1 :: nil =>
-      do rd <- ireg_of res; do rs <- ireg_of a1;
-      OK (Psllil rd rs n ::i k)
-  | Oshrl, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Psral rd rs1 rs2 ::i k)
-  | Oshrlimm n, a1 :: nil =>
-      do rd <- ireg_of res; do rs <- ireg_of a1;
-      OK (Psrail rd rs n ::i k)
-  | Oshrlu, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Psrll rd rs1 rs2 ::i k)
-  | Oshrluimm n, a1 :: nil =>
-      do rd <- ireg_of res; do rs <- ireg_of a1;
-      OK (Psrlil rd rs n ::i k)
-(*| Oshrxlimm n, a1 :: nil =>
-      do rd <- ireg_of res; do rs <- ireg_of a1;
-      OK (if Int.eq n Int.zero then Pmv rd rs :: k else
-          Psrail GPR31 rs (Int.repr 63) ::
-          Psrlil GPR31 GPR31 (Int.sub Int64.iwordsize' n) ::
-          Paddl GPR31 rs GPR31 ::
-          Psrail rd GPR31 n :: k)
-
-*)| Onegf, a1 :: nil =>
-      do rd <- freg_of res; do rs <- freg_of a1;
-      OK (Pfnegd rd rs ::i k)
-(*| Oabsf, a1 :: nil =>
-      do rd <- freg_of res; do rs <- freg_of a1;
-      OK (Pfabsd rd rs :: k)
-  | Oaddf, a1 :: a2 :: nil =>
-      do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
-      OK (Pfaddd rd rs1 rs2 :: k)
-  | Osubf, a1 :: a2 :: nil =>
-      do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
-      OK (Pfsubd rd rs1 rs2 :: k)
-  | Omulf, a1 :: a2 :: nil =>
-      do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
-      OK (Pfmuld rd rs1 rs2 :: k)
-  | Odivf, a1 :: a2 :: nil =>
-      do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
-      OK (Pfdivd rd rs1 rs2 :: k)
-
-  | Onegfs, a1 :: nil =>
-      do rd <- freg_of res; do rs <- freg_of a1;
-      OK (Pfnegs rd rs :: k)
-  | Oabsfs, a1 :: nil =>
-      do rd <- freg_of res; do rs <- freg_of a1;
-      OK (Pfabss rd rs :: k)
-  | Oaddfs, a1 :: a2 :: nil =>
-      do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
-      OK (Pfadds rd rs1 rs2 :: k)
-  | Osubfs, a1 :: a2 :: nil =>
-      do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
-      OK (Pfsubs rd rs1 rs2 :: k)
-  | Omulfs, a1 :: a2 :: nil =>
-      do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
-      OK (Pfmuls rd rs1 rs2 :: k)
-  | Odivfs, a1 :: a2 :: nil =>
-      do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
-      OK (Pfdivs 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)
-
-  | Ointoffloat, a1 :: nil =>
-      do rd <- ireg_of res; do rs <- freg_of a1;
-      OK (Pfcvtwd rd rs :: k)
-  | Ointuoffloat, a1 :: nil =>
-      do rd <- ireg_of res; do rs <- freg_of a1;
-      OK (Pfcvtwud rd rs :: k)
-  | Ofloatofint, a1 :: nil =>
-      do rd <- freg_of res; do rs <- ireg_of a1;
-      OK (Pfcvtdw rd rs :: k)
-  | Ofloatofintu, a1 :: nil =>
-      do rd <- freg_of res; do rs <- ireg_of a1;
-      OK (Pfcvtdwu rd rs :: k)
-  | Ointofsingle, a1 :: nil =>
-      do rd <- ireg_of res; do rs <- freg_of a1;
-      OK (Pfcvtws rd rs :: k)
-  | Ointuofsingle, a1 :: nil =>
-      do rd <- ireg_of res; do rs <- freg_of a1;
-      OK (Pfcvtwus rd rs :: k)
-  | Osingleofint, a1 :: nil =>
-      do rd <- freg_of res; do rs <- ireg_of a1;
-      OK (Pfcvtsw rd rs :: k)
-  | Osingleofintu, a1 :: nil =>
-      do rd <- freg_of res; do rs <- ireg_of a1;
-      OK (Pfcvtswu rd rs :: k)
-
-  | Olongoffloat, a1 :: nil =>
-      do rd <- ireg_of res; do rs <- freg_of a1;
-      OK (Pfcvtld rd rs :: k)
-  | Olonguoffloat, a1 :: nil =>
-      do rd <- ireg_of res; do rs <- freg_of a1;
-      OK (Pfcvtlud rd rs :: k)
-  | Ofloatoflong, a1 :: nil =>
-      do rd <- freg_of res; do rs <- ireg_of a1;
-      OK (Pfcvtdl rd rs :: k)
-  | Ofloatoflongu, a1 :: nil =>
-      do rd <- freg_of res; do rs <- ireg_of a1;
-      OK (Pfcvtdlu rd rs :: k)
-  | Olongofsingle, a1 :: nil =>
-      do rd <- ireg_of res; do rs <- freg_of a1;
-      OK (Pfcvtls rd rs :: k)
-  | Olonguofsingle, a1 :: nil =>
-      do rd <- ireg_of res; do rs <- freg_of a1;
-      OK (Pfcvtlus rd rs :: k)
-  | Osingleoflong, a1 :: nil =>
-      do rd <- freg_of res; do rs <- ireg_of a1;
-      OK (Pfcvtsl rd rs :: k)
-  | Osingleoflongu, a1 :: nil =>
-      do rd <- freg_of res; do rs <- ireg_of a1;
-      OK (Pfcvtslu rd rs :: k)
-
-*)| Ocmp cmp, _ =>
-      do rd <- ireg_of res;
-      transl_cond_op cmp rd args k
-  
-  | _, _ =>
-      Error(msg "Asmgen.transl_op")
-  end.
-
-(** Accessing data in the stack frame. *)
-
-Definition indexed_memory_access
-        (mk_instr: ireg -> offset -> instruction)
-        (base: ireg) (ofs: ptrofs) (k: code) :=
-  match make_immed64 (Ptrofs.to_int64 ofs) with
-  | Imm64_single imm =>
-      mk_instr base (Ofsimm (Ptrofs.of_int64 imm)) ::i k
-(*| Imm64_pair hi lo =>
-      Pluil GPR31 hi :: Paddl GPR31 base GPR31 :: mk_instr GPR31 (Ofsimm (Ptrofs.of_int64 lo)) :: k
-  | Imm64_large imm =>
-      Pmake GPR31 imm :: Paddl GPR31 base GPR31 :: mk_instr GPR31 (Ofsimm Ptrofs.zero) :: k
-*)end.
-
-Definition loadind (base: ireg) (ofs: ptrofs) (ty: typ) (dst: mreg) (k: code) :=
-  match ty, preg_of dst with
-  | Tint,    IR rd => OK (indexed_memory_access (Plw rd) base ofs k)
-  | Tlong,   IR rd => OK (indexed_memory_access (Pld rd) base ofs k)
-  | Tsingle, IR rd => OK (indexed_memory_access (Pfls rd) base ofs k)
-  | Tfloat,  IR rd => OK (indexed_memory_access (Pfld rd) base ofs k)
-  | Tany32,  IR rd => OK (indexed_memory_access (Plw_a rd) base ofs k)
-  | Tany64,  IR rd => OK (indexed_memory_access (Pld_a rd) base ofs k)
-  | _, _           => Error (msg "Asmgen.loadind")
-  end.
-
-Definition storeind (src: mreg) (base: ireg) (ofs: ptrofs) (ty: typ) (k: code) :=
-  match ty, preg_of src with
-  | Tint,    IR rd => OK (indexed_memory_access (Psw rd) base ofs k)
-  | Tlong,   IR rd => OK (indexed_memory_access (Psd rd) base ofs k)
-  | Tsingle, IR rd => OK (indexed_memory_access (Pfss rd) base ofs k)
-  | Tfloat,  IR rd => OK (indexed_memory_access (Pfsd rd) base ofs k)
-  | Tany32,  IR rd => OK (indexed_memory_access (Psw_a rd) base ofs k)
-  | Tany64,  IR rd => OK (indexed_memory_access (Psd_a rd) base ofs k)
-  | _, _           => Error (msg "Asmgen.storeind")
-  end.
-
-Definition loadind_ptr (base: ireg) (ofs: ptrofs) (dst: ireg) (k: code) :=
-  indexed_memory_access (Pld dst) base ofs k.
-
-Definition storeind_ptr (src: ireg) (base: ireg) (ofs: ptrofs) (k: code) :=
-  indexed_memory_access (Psd src) base ofs k.
-
-(** Translation of memory accesses: loads, and stores. *)
-
-Definition transl_memory_access
-     (mk_instr: ireg -> offset -> instruction)
-     (addr: addressing) (args: list mreg) (k: code) : res (list instruction) :=
-  match addr, args with
-  | Aindexed ofs, a1 :: nil =>
-      do rs <- ireg_of a1;
-      OK (indexed_memory_access mk_instr rs ofs k)
-  | Aglobal id ofs, nil =>
-      OK (Ploadsymbol GPR31 id ofs ::i (mk_instr GPR31 (Ofsimm Ptrofs.zero) ::i k))
-  | Ainstack ofs, nil =>
-      OK (indexed_memory_access mk_instr SP ofs k)
-  | _, _ =>
-      Error(msg "Asmgen.transl_memory_access")
-  end.
-
-Definition transl_load (chunk: memory_chunk) (addr: addressing)
-           (args: list mreg) (dst: mreg) (k: code) : res (list instruction) :=
-  match chunk with
-  | Mint8signed =>
-      do r <- ireg_of dst;
-      transl_memory_access (Plb r)  addr args k
-  | Mint8unsigned =>
-      do r <- ireg_of dst;
-      transl_memory_access (Plbu r) addr args k
-  | Mint16signed =>
-      do r <- ireg_of dst;
-      transl_memory_access (Plh r)  addr args k
-  | Mint16unsigned =>
-      do r <- ireg_of dst;
-      transl_memory_access (Plhu r) addr args k
-  | Mint32 =>
-      do r <- ireg_of dst;
-      transl_memory_access (Plw r)  addr args k
-  | Mint64 =>
-      do r <- ireg_of dst;
-      transl_memory_access (Pld r)  addr args k
-  | Mfloat32 =>
-      do r <- freg_of dst;
-      transl_memory_access (Pfls r) addr args k
-  | Mfloat64 =>
-      do r <- freg_of dst;
-      transl_memory_access (Pfld r) addr args k
-  | _ =>
-      Error (msg "Asmgen.transl_load")
-  end.
-
-Definition transl_store (chunk: memory_chunk) (addr: addressing)
-           (args: list mreg) (src: mreg) (k: code) : res (list instruction) :=
-  match chunk with
-  | Mint8signed | Mint8unsigned =>
-      do r <- ireg_of src;
-      transl_memory_access (Psb r)  addr args k
-  | Mint16signed | Mint16unsigned =>
-      do r <- ireg_of src;
-      transl_memory_access (Psh r)  addr args k
-  | Mint32 =>
-      do r <- ireg_of src;
-      transl_memory_access (Psw r)  addr args k
-  | Mint64 =>
-      do r <- ireg_of src;
-      transl_memory_access (Psd r)  addr args k
-  | Mfloat32 =>
-      do r <- freg_of src;
-      transl_memory_access (Pfss r) addr args k
-  | Mfloat64 =>
-      do r <- freg_of src;
-      transl_memory_access (Pfsd r) addr args k
-  | _ =>
-      Error (msg "Asmgen.transl_store")
-  end.
-
-(** Function epilogue *)
-
-Definition make_epilogue (f: Mach.function) (k: code) :=
-  loadind_ptr SP f.(fn_retaddr_ofs) GPR8 
-  (Pset RA GPR8 ::i Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) ::i k).
-
-(** Translation of a Mach instruction. *)
-
-Definition transl_instr (f: Mach.function) (i: Mach.instruction)
-                        (ep: bool) (k: code) :=
-  match i with
-  | Mgetstack ofs ty dst =>
-      loadind SP ofs ty dst k
-  | Msetstack src ofs ty =>
-      storeind src SP ofs ty k
-  | Mgetparam ofs ty dst =>
-      (* load via the frame pointer if it is valid *)
-      do c <- loadind FP ofs ty dst k;
-      OK (if ep then c
-                else loadind_ptr SP f.(fn_link_ofs) FP c)
-  | Mop op args res =>
-      transl_op op args res k
-  | Mload chunk addr args dst =>
-      transl_load 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 (Pjal_r r1 sig :: k)
-*)| Mcall sig (inr symb) =>
-      OK ((Pcall symb) ::i k)
-(*| Mtailcall sig (inl r) =>
-      do r1 <- ireg_of r;
-      OK (make_epilogue f (Pcall :: k))
-*)| Mtailcall sig (inr symb) =>
-      OK (make_epilogue f ((Pgoto symb) ::i k))
-  | Mbuiltin ef args res =>
-      OK (Pbuiltin ef (List.map (map_builtin_arg preg_of) args) (map_builtin_res preg_of res) ::i k)
-  | Mlabel lbl =>
-      OK (Plabel lbl ::i k)
-  | Mgoto lbl =>
-      OK (Pj_l lbl ::i k)
-  | Mcond cond args lbl =>
-      transl_cbranch cond args lbl k
-(*| Mjumptable arg tbl => do r <- ireg_of arg; OK (Pbtbl r tbl :: k)
-*)| Mreturn =>
-      OK (make_epilogue f (Pret ::i k))
-      (*OK (make_epilogue f (Pj_r RA f.(Mach.fn_sig) :: k))*)
-  | _ =>
-      Error (msg "Asmgen.transl_instr")
-  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 R10)
-  | Mop op args res => before && negb (mreg_eq res R10)
-  | _ => 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) ::i
-         Pget GPR8 RA ::i
-         storeind_ptr GPR8 SP f.(fn_retaddr_ofs) c)).
-
-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_fundef (f: Mach.fundef) : res Asm.fundef :=
-  transf_partial_fundef transf_function f.
-
 Definition transf_program (p: Mach.program) : res Asm.program :=
-  transform_partial_program transf_fundef p.
+  let mbp := Machblockgen.transf_program p in
+  do abp <- Asmblockgen.transf_program mbp;
+  OK (Asm.transf_program abp).
\ No newline at end of file
diff --git a/mppa_k1c/Asmgenproof.v b/mppa_k1c/Asmgenproof.v
index 896e9ce9..87c4184b 100644
--- a/mppa_k1c/Asmgenproof.v
+++ b/mppa_k1c/Asmgenproof.v
@@ -15,1092 +15,52 @@
 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.
+Require Import Op Locations Mach Conventions Asm Asmgen Machblockgen Asmblockgen.
+Require Import Machblockgenproof Asmblockgenproof.
 
-Definition match_prog (p: Mach.program) (tp: Asm.program) :=
-  match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp.
+(* Local Open Scope linking_scope.
+
+Definition block_passes :=
+      mkpass Machblockgenproof.match_prog
+  ::: mkpass Asmblockgenproof.match_prog
+  ::: mkpass Asm.match_prog
+  ::: pass_nil _.
+ *)
+
+Inductive match_prog : Mach.program -> Asm.program -> Prop :=
+  | mk_match_prog: forall p mbp abp tp,
+      Machblockgen.transf_program p = mbp -> Machblockgenproof.match_prog p mbp ->
+      Asmblockgen.transf_program mbp = OK abp -> Asmblockgenproof.match_prog mbp abp ->
+      Asm.match_prog abp tp ->
+      match_prog p tp.
 
 Lemma transf_program_match:
-  forall p tp, transf_program p = OK tp -> match_prog p tp.
+  forall p tp, Asmgen.transf_program p = OK tp -> match_prog p tp.
 Proof.
-  intros. eapply match_transform_partial_program; eauto.
+  intros p tp H.
+  unfold Asmgen.transf_program in H. apply bind_inversion in H. destruct H.
+  inversion_clear H. inversion_clear H1. remember (Machblockgen.transf_program p) as mbp.
+  constructor 1 with (mbp:=mbp) (abp:=x); auto.
+  subst. apply Machblockgenproof.transf_program_match.
+  apply Asmblockgenproof.transf_program_match. auto.
+  apply Asm.transf_program_match. auto.
 Qed.
 
 Section PRESERVATION.
 
 Variable prog: Mach.program.
-Variable tprog: Asm.program.
+Variable tprog: 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 loadimm32_label:
-  forall r n k, tail_nolabel k (loadimm32 r n k).
-Proof.
-  intros; unfold loadimm32. destruct (make_immed32 n); TailNoLabel.
-(*unfold load_hilo32. destruct (Int.eq lo Int.zero); TailNoLabel.*)
-Qed.
-Hint Resolve loadimm32_label: labels.
-
-Remark opimm32_label:
-  forall (op: arith_name_rrr) (opimm: arith_name_rri32) r1 r2 n k,
-  (forall r1 r2 r3, nolabel (op r1 r2 r3)) ->
-  (forall r1 r2 n, nolabel (opimm r1 r2 n)) ->
-  tail_nolabel k (opimm32 op opimm r1 r2 n k).
-Proof.
-  intros; unfold opimm32. destruct (make_immed32 n); TailNoLabel.
-(*unfold load_hilo32. destruct (Int.eq lo Int.zero); TailNoLabel.*)
-Qed.
-Hint Resolve opimm32_label: labels.
-
-Remark loadimm64_label:
-  forall r n k, tail_nolabel k (loadimm64 r n k).
-Proof.
-  intros; unfold loadimm64. destruct (make_immed64 n); TailNoLabel.
-(*unfold load_hilo64. destruct (Int64.eq lo Int64.zero); TailNoLabel.*)
-Qed.
-Hint Resolve loadimm64_label: labels.
-
-Remark cast32signed_label:
-  forall rd rs k, tail_nolabel k (cast32signed rd rs k).
-Proof.
-  intros; unfold cast32signed. destruct (ireg_eq rd rs); TailNoLabel.
-Qed.
-Hint Resolve cast32signed_label: labels.
-
-Remark opimm64_label:
-  forall (op: arith_name_rrr) (opimm: arith_name_rri64) r1 r2 n k,
-  (forall r1 r2 r3, nolabel (op r1 r2 r3)) ->
-  (forall r1 r2 n, nolabel (opimm r1 r2 n)) ->
-  tail_nolabel k (opimm64 op opimm r1 r2 n k).
-Proof.
-  intros; unfold opimm64. destruct (make_immed64 n); TailNoLabel.
-(*unfold load_hilo64. destruct (Int64.eq lo Int64.zero); TailNoLabel.*)
-Qed.
-Hint Resolve opimm64_label: labels.
-
-Remark addptrofs_label:
-  forall r1 r2 n k, tail_nolabel k (addptrofs r1 r2 n k).
-Proof.
-  unfold addptrofs; intros. destruct (Ptrofs.eq_dec n Ptrofs.zero). TailNoLabel.
-  apply opimm64_label; TailNoLabel.
-Qed.
-Hint Resolve addptrofs_label: labels.
-(*
-Remark transl_cond_float_nolabel:
-  forall c r1 r2 r3 insn normal,
-  transl_cond_float c r1 r2 r3 = (insn, normal) -> nolabel insn.
-Proof.
-  unfold transl_cond_float; intros. destruct c; inv H; exact I.
-Qed.
-
-Remark transl_cond_single_nolabel:
-  forall c r1 r2 r3 insn normal,
-  transl_cond_single c r1 r2 r3 = (insn, normal) -> nolabel insn.
-Proof.
-  unfold transl_cond_single; intros. destruct c; inv H; exact I.
-Qed.
-*)
-Remark transl_cbranch_label:
-  forall cond args lbl k c,
-  transl_cbranch cond args lbl k = OK c -> tail_nolabel k c.
-Proof.
-  intros. unfold transl_cbranch in H. destruct cond; TailNoLabel.
-(* Ccomp *)
-  - unfold transl_comp; TailNoLabel.
-(* Ccompu *)
-  - unfold transl_comp; TailNoLabel.
-(* Ccompimm *)
-  - destruct (Int.eq n Int.zero); TailNoLabel.
-    unfold loadimm32. destruct (make_immed32 n); TailNoLabel. unfold transl_comp; TailNoLabel.
-(* Ccompuimm *)
-  - unfold transl_opt_compuimm.
-    remember (select_comp n c0) as selcomp; destruct selcomp.
-    + destruct c; TailNoLabel; contradict Heqselcomp; unfold select_comp;
-      destruct (Int.eq n Int.zero); destruct c0; discriminate.
-    + unfold loadimm32;
-      destruct (make_immed32 n); TailNoLabel; unfold transl_comp; TailNoLabel.
-(* Ccompl *)
-  - unfold transl_compl; TailNoLabel.
-(* Ccomplu *)
-  - unfold transl_compl; TailNoLabel.
-(* Ccomplimm *)
-  - destruct (Int64.eq n Int64.zero); TailNoLabel.
-    unfold loadimm64. destruct (make_immed64 n); TailNoLabel. unfold transl_compl; TailNoLabel.
-(* Ccompluimm *)
-  - unfold transl_opt_compluimm.
-    remember (select_compl n c0) as selcomp; destruct selcomp.
-    + destruct c; TailNoLabel; contradict Heqselcomp; unfold select_compl;
-      destruct (Int64.eq n Int64.zero); destruct c0; discriminate.
-    + unfold loadimm64;
-      destruct (make_immed64 n); TailNoLabel; unfold transl_compl; TailNoLabel.
-Qed.
-
-(*
-- destruct c0; simpl; TailNoLabel.
-- destruct c0; simpl; TailNoLabel.
-- destruct (Int.eq n Int.zero).
-  destruct c0; simpl; TailNoLabel.
-  apply tail_nolabel_trans with (transl_cbranch_int32s c0 x X31 lbl :: k).
-  auto with labels. destruct c0; simpl; TailNoLabel.
-- destruct (Int.eq n Int.zero).
-  destruct c0; simpl; TailNoLabel.
-  apply tail_nolabel_trans with (transl_cbranch_int32u c0 x X31 lbl :: k).
-  auto with labels. destruct c0; simpl; TailNoLabel.
-- destruct c0; simpl; TailNoLabel.
-- destruct c0; simpl; TailNoLabel.
-- destruct (Int64.eq n Int64.zero).
-  destruct c0; simpl; TailNoLabel.
-  apply tail_nolabel_trans with (transl_cbranch_int64s c0 x X31 lbl :: k).
-  auto with labels. destruct c0; simpl; TailNoLabel.
-- destruct (Int64.eq n Int64.zero).
-  destruct c0; simpl; TailNoLabel.
-  apply tail_nolabel_trans with (transl_cbranch_int64u c0 x X31 lbl :: k).
-  auto with labels. destruct c0; simpl; TailNoLabel.
-- destruct (transl_cond_float c0 X31 x x0) as [insn normal] eqn:F; inv EQ2.
-  apply tail_nolabel_cons. eapply transl_cond_float_nolabel; eauto. 
-  destruct normal; TailNoLabel.
-- destruct (transl_cond_float c0 X31 x x0) as [insn normal] eqn:F; inv EQ2.
-  apply tail_nolabel_cons. eapply transl_cond_float_nolabel; eauto. 
-  destruct normal; TailNoLabel.
-- destruct (transl_cond_single c0 X31 x x0) as [insn normal] eqn:F; inv EQ2.
-  apply tail_nolabel_cons. eapply transl_cond_single_nolabel; eauto. 
-  destruct normal; TailNoLabel.
-- destruct (transl_cond_single c0 X31 x x0) as [insn normal] eqn:F; inv EQ2.
-  apply tail_nolabel_cons. eapply transl_cond_single_nolabel; eauto. 
-  destruct normal; TailNoLabel.
-*)
-
-Remark transl_cond_op_label:
-  forall cond args r k c,
-  transl_cond_op cond r args k = OK c -> tail_nolabel k c.
-Proof.
-  intros. unfold transl_cond_op in H; destruct cond; TailNoLabel.
-- unfold transl_cond_int32s; destruct c0; simpl; TailNoLabel.
-- unfold transl_cond_int32u; destruct c0; simpl; TailNoLabel. 
-- unfold transl_condimm_int32s; destruct c0; simpl; TailNoLabel.
-- unfold transl_condimm_int32u; destruct c0; simpl; TailNoLabel.
-- unfold transl_cond_int64s; destruct c0; simpl; TailNoLabel.
-- unfold transl_cond_int64u; destruct c0; simpl; TailNoLabel. 
-- unfold transl_condimm_int64s; destruct c0; simpl; TailNoLabel.
-- unfold transl_condimm_int64u; destruct c0; simpl; 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.
-Opaque Int.eq.
-  unfold transl_op; intros; destruct op; TailNoLabel.
-(* Omove *)
-- destruct (preg_of r); try discriminate; destruct (preg_of m); inv H; TailNoLabel.
-(* Oaddrsymbol *)
-- destruct (Archi.pic_code tt && negb (Ptrofs.eq ofs Ptrofs.zero)); TailNoLabel.
-(* Oaddimm32 *)
-- apply opimm32_label; intros; exact I.
-(* Oandimm32 *)
-- apply opimm32_label; intros; exact I.
-(* Oorimm32 *)
-- apply opimm32_label; intros; exact I.
-(* Oxorimm32 *)
-- apply opimm32_label; intros; exact I.
-(* Oshrximm *)
-- destruct (Int.eq n Int.zero); TailNoLabel.
-(* Oaddimm64 *)
-- apply opimm64_label; intros; exact I.
-(* Oandimm64  *)
-- apply opimm64_label; intros; exact I.
-(* Oorimm64  *)
-- apply opimm64_label; intros; exact I.
-(* Oxorimm64  *)
-- apply opimm64_label; intros; exact I.
-(* Ocmp *)
-- eapply transl_cond_op_label; eauto.
-Qed.
-
-(*
-- 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.
-- destruct (Archi.pic_code tt && negb (Ptrofs.eq ofs Ptrofs.zero)).
-+ eapply tail_nolabel_trans; [|apply addptrofs_label]. TailNoLabel.
-+ TailNoLabel. 
-- apply opimm32_label; intros; exact I.
-- apply opimm32_label; intros; exact I.
-- apply opimm32_label; intros; exact I.
-- apply opimm32_label; intros; exact I.
-- destruct (Int.eq n Int.zero); TailNoLabel.
-- apply opimm64_label; intros; exact I.
-- apply opimm64_label; intros; exact I.
-- apply opimm64_label; intros; exact I.
-- apply opimm64_label; intros; exact I.
-- destruct (Int.eq n Int.zero); TailNoLabel.
-- eapply transl_cond_op_label; eauto.
-*)
-
-Remark indexed_memory_access_label:
-  forall (mk_instr: ireg -> offset -> instruction) base ofs k,
-  (forall r o, nolabel (mk_instr r o)) ->
-  tail_nolabel k (indexed_memory_access mk_instr base ofs k).
-Proof.
-  unfold indexed_memory_access; intros. 
-  (* destruct Archi.ptr64. *)
-  destruct (make_immed64 (Ptrofs.to_int64 ofs)); TailNoLabel.
-  (* destruct (make_immed32 (Ptrofs.to_int ofs)); 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 loadind_ptr_label:
-  forall base ofs dst k, tail_nolabel k (loadind_ptr base ofs dst k).
-Proof.
-  intros. apply indexed_memory_access_label. intros; destruct Archi.ptr64; exact I.
-Qed.
-
-Remark storeind_ptr_label:
-  forall src base ofs k, tail_nolabel k (storeind_ptr src base ofs k).
-Proof.
-  intros. apply indexed_memory_access_label. intros; destruct Archi.ptr64; exact I.
-Qed.
-
-Remark transl_memory_access_label:
-  forall (mk_instr: ireg -> offset -> instruction) addr args k c,
-  (forall r o, nolabel (mk_instr r o)) ->
-  transl_memory_access mk_instr addr args k = OK c ->
-  tail_nolabel k c.
-Proof.
-  unfold transl_memory_access; intros; destruct addr; TailNoLabel; apply indexed_memory_access_label; auto. 
-Qed.
-
-Remark make_epilogue_label:
-  forall f k, tail_nolabel k (make_epilogue f k).
-Proof.
-  unfold make_epilogue; intros. eapply tail_nolabel_trans. apply loadind_ptr_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 ::i k | _ => tail_nolabel k c end.
-Proof.
-  unfold transl_instr; intros; destruct i; TailNoLabel.
-(* loadind *)
-- eapply loadind_label; eauto.
-(* storeind *)
-- eapply storeind_label; eauto.
-(* Mgetparam *)
-- destruct ep. eapply loadind_label; eauto.
-  eapply tail_nolabel_trans. apply loadind_ptr_label. eapply loadind_label; eauto. 
-(* transl_op *)
-- eapply transl_op_label; eauto.
-(* transl_load *)
-- destruct m; monadInv H; eapply transl_memory_access_label; eauto; intros; exact I.
-(* transl store *)
-- destruct m; monadInv H; eapply transl_memory_access_label; eauto; intros; exact I.
-- destruct s0; monadInv H; TailNoLabel.
-- destruct s0; monadInv H; eapply tail_nolabel_trans
-  ; [eapply make_epilogue_label|TailNoLabel].
-- eapply transl_cbranch_label; eauto.
-- eapply tail_nolabel_trans; [eapply make_epilogue_label|TailNoLabel].
-Qed.
-(*
-
-
-- eapply transl_op_label; eauto.
-- destruct m; monadInv H; eapply transl_memory_access_label; eauto; intros; exact I.
-- destruct m; monadInv H; eapply transl_memory_access_label; eauto; intros; exact I.
-- destruct s0; monadInv H; (eapply tail_nolabel_trans; [eapply make_epilogue_label|TailNoLabel]).
-- eapply tail_nolabel_trans; [eapply make_epilogue_label|TailNoLabel].
-*)
-
-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 (storeind_ptr_label GPR8 GPR12 (fn_retaddr_ofs f) x) as [A B]. 
-  (* destruct 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 is_tail_cons. apply (storeind_ptr_label GPR8 GPR12 (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#FP = parent_sp 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#FP = parent_sp 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]]].
-  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') ->
-  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]]]]].
-  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.
-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') ->
-  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]]]]].
-  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.
-- 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.
-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_FP: forall r, negb (mreg_eq r R10) = true -> IR FP <> preg_of r.
-Proof.
-  intros. change (IR FP) with (preg_of R10). red; intros.
-  exploit preg_of_injective; eauto. intros; subst r; discriminate.
-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'),
-  (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. simpl; congruence.
-
-- (* 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]]].
-  exists rs'; split. eauto.
-  split. eapply agree_set_mreg; eauto with asmgen. congruence.
-  simpl; congruence.
-
-
-- (* Msetstack *)
-  unfold store_stack in H.
-  assert (Val.lessdef (rs src) (rs0 (preg_of src))). 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.
-  inversion TR.
-  exploit storeind_correct; eauto with asmgen. intros [rs' [P Q]].
-  exists rs'; split. eauto.
-  split. eapply agree_undef_regs; eauto with asmgen.
-  simpl; intros. rewrite Q; auto with asmgen.
-
-- (* 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.
-(* GPR31 contains parent *)
-  exploit loadind_correct. eexact EQ.
-  instantiate (2 := rs0). rewrite DXP; eauto. congruence.
-  intros [rs1 [P [Q R]]].
-  exists rs1; split. eauto.
-  split. eapply agree_set_mreg. eapply agree_set_mreg; eauto. congruence. auto with asmgen.
-  simpl; intros. rewrite R; auto with asmgen.
-  apply preg_of_not_FP; auto.
-(* GPR11 does not contain parent *)
-  rewrite chunk_of_Tptr in A. 
-  exploit loadind_ptr_correct. eexact A. congruence. intros [rs1 [P [Q R]]].
-  exploit loadind_correct. eexact EQ. instantiate (2 := rs1). rewrite Q. eauto. congruence.
-  intros [rs2 [S [T U]]].
-  exists rs2; split. eapply exec_straight_trans; eauto.
-  split. eapply agree_set_mreg. eapply agree_set_mreg. eauto. eauto.
-  instantiate (1 := rs1#FP <- (rs2#FP)). intros.
-  rewrite Pregmap.gso; auto with asmgen.
-  congruence.
-  intros. unfold Pregmap.set. destruct (PregEq.eq r' FP). congruence. auto with asmgen.
-  simpl; intros. rewrite U; auto with asmgen.
-  apply preg_of_not_FP; 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]]].
-  exists rs2; split. eauto. split. auto.
-  apply agree_set_undef_mreg with rs0; auto. 
-  apply Val.lessdef_trans with v'; auto.
-  simpl; intros. destruct (andb_prop _ _ H1); clear H1.
-  rewrite R; auto. apply preg_of_not_FP; auto.
-Local Transparent destroyed_by_op.
-  destruct op; simpl; auto; congruence.
-
-- (* Mload *)
-  assert (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.
-  inversion TR.
-  exploit transl_load_correct; eauto.
-  intros [rs2 [P [Q R]]].
-  exists rs2; split. eauto.
-  split. eapply agree_set_undef_mreg; eauto. congruence.
-  intros; auto with asmgen.
-  simpl; congruence.
-
-
-- (* Mstore *)
-  assert (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))). eapply preg_val; eauto.
-  exploit Mem.storev_extends; eauto. intros [m2' [C D]].
-  left; eapply exec_straight_steps; eauto.
-  intros. simpl in TR.
-  inversion TR.
-  exploit transl_store_correct; eauto. intros [rs2 [P Q]].
-  exists rs2; split. eauto.
-  split. eapply agree_undef_regs; eauto with asmgen.
-  simpl; congruence.
-
-- (* 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.
-    - econstructor; auto with asmgen.
-      + apply V.
-      + intro r. destruct r; apply V; auto.
-    - eauto 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 Pregmap.gso by congruence. 
-  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. apply Pregmap.gso; auto with asmgen.
-  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.
-- (* 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.
-  inversion TR.
-  exploit transl_cbranch_correct_true; eauto. intros (rs' & jmp & A & B & C).
-  exists jmp; exists k; exists rs'.
-  split. eexact A. 
-  split. apply agree_exten with rs0; auto with asmgen.
-  exact B. 
-- (* Mcond false *)
-  exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC.
-  left; eapply exec_straight_steps; eauto. intros. simpl in TR.
-  inversion TR.
-  exploit transl_cbranch_correct_false; eauto. intros (rs' & A & B).
-  exists rs'.
-  split. eexact A.
-  split. apply agree_exten with rs0; auto with asmgen.
-  simpl. congruence.
-- (* 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#X5 <- Vundef #X31 <- 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. 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.
-*)
-- (* 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]].
-  (* Execution of function prologue *)
-  monadInv EQ0. rewrite transl_code'_transl_code in EQ1.
-  set (tfbody := Pallocframe (fn_stacksize f) (fn_link_ofs f) ::i
-                 Pget GPR8 RA ::i
-                 storeind_ptr GPR8 SP (fn_retaddr_ofs f) x0) in *.
-  set (tf := {| fn_sig := Mach.fn_sig f; fn_code := tfbody |}) in *.
-  set (rs2 := nextinstr (rs0#FP <- (parent_sp s) #SP <- sp #GPR31 <- Vundef)).
-  exploit (Pget_correct tge tf GPR8 RA (storeind_ptr GPR8 SP (fn_retaddr_ofs f) x0) rs2 m2'); auto.
-  intros (rs' & U' & V').
-  exploit (storeind_ptr_correct tge tf SP (fn_retaddr_ofs f) GPR8 x0 rs' m2').
-    rewrite chunk_of_Tptr in P.
-    assert (rs' GPR8 = rs0 RA). { apply V'. }
-    assert (rs' GPR12 = rs2 GPR12). { apply V'; discriminate. }
-    rewrite H3. rewrite H4.
-    (* change (rs' GPR8) with (rs0 RA). *)
-    rewrite ATLR.
-    change (rs2 GPR12) with sp. eexact P.
-    congruence. congruence.
-  intros (rs3 & U & V).
-  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 chunk_of_Tptr in F. rewrite F. reflexivity.
-    reflexivity.
-    eapply exec_straight_trans.
-    - eexact U'.
-    - 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; intros; Simpl.
-  unfold sp; congruence.
-
-  intros.
-  assert (r <> GPR31). { contradict H3; rewrite H3; unfold data_preg; auto. }
-  rewrite V.
-  assert (r <> GPR8). { contradict H3; rewrite H3; unfold data_preg; auto. }
-  assert (forall r : preg, r <> PC -> r <> GPR8 -> rs' r = rs2 r). { apply V'. }
-  rewrite H6; auto.
-  contradict H3; rewrite H3; unfold data_preg; auto.
-  contradict H3; rewrite H3; unfold data_preg; auto.
-  contradict H3; rewrite H3; unfold data_preg; auto.
-  intros. rewrite V by auto with asmgen.
-  assert (forall r : preg, r <> PC -> r <> GPR8 -> rs' r = rs2 r). { apply V'. }
-  rewrite H4 by auto with asmgen. reflexivity.
-
-- (* 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.
-
-- (* return *)
-  inv STACKS. simpl in *.
-  right. split. omega. split. auto.
-  rewrite <- ATPC in H5.
-  econstructor; eauto. 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).
+  forward_simulation (Mach.semantics (inv_trans_rao return_address_offset) prog) (Asm.semantics tprog).
 Proof.
-  eapply forward_simulation_star with (measure := measure).
-  apply senv_preserved.
-  eexact transf_initial_states.
-  eexact transf_final_states.
-  exact step_simulation.
+  inv TRANSF.
+  eapply compose_forward_simulations. apply Machblockgenproof.transf_program_correct; eauto.
+  eapply compose_forward_simulations. apply Asmblockgenproof.transf_program_correct; eauto.
+  apply Asm.transf_program_correct. eauto.
 Qed.
 
 End PRESERVATION.
diff --git a/mppa_k1c/Machblockgen.v b/mppa_k1c/Machblockgen.v
index aa54e8a2..c20889b7 100644
--- a/mppa_k1c/Machblockgen.v
+++ b/mppa_k1c/Machblockgen.v
@@ -574,5 +574,5 @@ Definition trans_function (f: Mach.function) : function :=
 Definition trans_fundef (f: Mach.fundef) : fundef :=
   transf_fundef trans_function f.
 
-Definition trans_prog (src: Mach.program) : program :=
+Definition transf_program (src: Mach.program) : program :=
   transform_program trans_fundef src.
diff --git a/mppa_k1c/Machblockgenproof.v b/mppa_k1c/Machblockgenproof.v
index 62391792..ff9c29d3 100644
--- a/mppa_k1c/Machblockgenproof.v
+++ b/mppa_k1c/Machblockgenproof.v
@@ -23,7 +23,7 @@ Definition inv_trans_rao (rao: function -> code -> ptrofs -> Prop) (f: Mach.func
 Definition match_prog (p: Mach.program) (tp: Machblock.program) :=
   match_program (fun _ f tf => tf = trans_fundef f) eq p tp.
 
-Lemma trans_program_match: forall p, match_prog p (trans_prog p).
+Lemma transf_program_match: forall p, match_prog p (transf_program p).
 Proof.
   intros. eapply match_transform_program; eauto.
 Qed.
@@ -461,8 +461,7 @@ Proof.
   destruct ei; (contradict Hexit; discriminate) || (
     inversion Hexit; subst; inversion Hstep; subst; simpl
   ).
-  * unfold inv_trans_rao in H11.
-    eapply ex_intro; constructor 1; [ idtac | eapply match_states_trans_state ]; eauto.
+  * eapply ex_intro; constructor 1; [ idtac | eapply match_states_trans_state ]; eauto.
     apply exec_MBcall with (f := (trans_function f0)); auto.
     rewrite find_function_ptr_same in H9; auto.
   * eapply ex_intro; constructor 1; [ idtac | eapply match_states_trans_state ]; eauto.
@@ -600,7 +599,8 @@ Proof.
     eapply exec_return.
 Qed.
 
-Theorem simulation: forward_simulation (Mach.semantics (inv_trans_rao rao) prog) (Machblock.semantics rao tprog).
+Theorem transf_program_correct: 
+    forward_simulation (Mach.semantics (inv_trans_rao rao) prog) (Machblock.semantics rao tprog).
 Proof.
   apply forward_simulation_block_trans with (dist_end_block := dist_end_block) (trans_state := trans_state).
 (* simu_mid_block *)