Merge branch 'mppa-refactor' into mppa-work

12 files changed, 1667 insertions, 1946 deletions

diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index b323a67c..303a624c 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -222,197 +222,197 @@ Inductive instruction : Type :=
 

 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.Picall r)            => Picall r

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

-  | PCtlFlow (Asmblock.Pigoto l)             => Pigoto 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

-  | PCtlFlow (Asmblock.Pjumptable r label)  => Pjumptable r label

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

+  | PCtlFlow Asmvliw.Pret                  => Pret

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

+  | PCtlFlow (Asmvliw.Picall r)            => Picall r

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

+  | PCtlFlow (Asmvliw.Pigoto l)             => Pigoto l

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

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

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

+  | PCtlFlow (Asmvliw.Pjumptable r label)  => Pjumptable r label

   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

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

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

+  | Asmvliw.Pnop               => Pnop

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

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

 

   (** PArith basics *)

   (* R *)

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

+  | PArithR (Asmvliw.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   => Pnegl rd rs

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

-  | PArithRR Asmblock.Psxwd rd rs  => Psxwd rd rs

-  | PArithRR Asmblock.Pzxwd rd rs  => Pzxwd rd rs

-  | PArithRR Asmblock.Pfabsd rd rs => Pfabsd rd rs

-  | PArithRR Asmblock.Pfabsw rd rs => Pfabsw rd rs

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

-  | PArithRR Asmblock.Pfnegw rd rs => Pfnegw rd rs

-  | PArithRR Asmblock.Pfnarrowdw rd rs => Pfnarrowdw rd rs

-  | PArithRR Asmblock.Pfwidenlwd rd rs => Pfwidenlwd rd rs

-  | PArithRR Asmblock.Pfloatuwrnsz rd rs => Pfloatuwrnsz rd rs

-  | PArithRR Asmblock.Pfloatwrnsz rd rs => Pfloatwrnsz rd rs

-  | PArithRR Asmblock.Pfloatudrnsz rd rs => Pfloatudrnsz rd rs

-  | PArithRR Asmblock.Pfloatdrnsz rd rs => Pfloatdrnsz rd rs

-  | PArithRR Asmblock.Pfloatudrnsz_i32 rd rs => Pfloatudrnsz_i32 rd rs

-  | PArithRR Asmblock.Pfloatdrnsz_i32 rd rs => Pfloatdrnsz_i32 rd rs

-  | PArithRR Asmblock.Pfixedwrzz rd rs => Pfixedwrzz rd rs

-  | PArithRR Asmblock.Pfixeduwrzz rd rs => Pfixeduwrzz rd rs

-  | PArithRR Asmblock.Pfixeddrzz rd rs => Pfixeddrzz rd rs

-  | PArithRR Asmblock.Pfixedudrzz rd rs => Pfixedudrzz rd rs

-  | PArithRR Asmblock.Pfixeddrzz_i32 rd rs => Pfixeddrzz_i32 rd rs

-  | PArithRR Asmblock.Pfixedudrzz_i32 rd rs => Pfixedudrzz_i32 rd rs

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

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

+  | PArithRR Asmvliw.Pnegl rd rs   => Pnegl rd rs

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

+  | PArithRR Asmvliw.Psxwd rd rs  => Psxwd rd rs

+  | PArithRR Asmvliw.Pzxwd rd rs  => Pzxwd rd rs

+  | PArithRR Asmvliw.Pfabsd rd rs => Pfabsd rd rs

+  | PArithRR Asmvliw.Pfabsw rd rs => Pfabsw rd rs

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

+  | PArithRR Asmvliw.Pfnegw rd rs => Pfnegw rd rs

+  | PArithRR Asmvliw.Pfnarrowdw rd rs => Pfnarrowdw rd rs

+  | PArithRR Asmvliw.Pfwidenlwd rd rs => Pfwidenlwd rd rs

+  | PArithRR Asmvliw.Pfloatuwrnsz rd rs => Pfloatuwrnsz rd rs

+  | PArithRR Asmvliw.Pfloatwrnsz rd rs => Pfloatwrnsz rd rs

+  | PArithRR Asmvliw.Pfloatudrnsz rd rs => Pfloatudrnsz rd rs

+  | PArithRR Asmvliw.Pfloatdrnsz rd rs => Pfloatdrnsz rd rs

+  | PArithRR Asmvliw.Pfloatudrnsz_i32 rd rs => Pfloatudrnsz_i32 rd rs

+  | PArithRR Asmvliw.Pfloatdrnsz_i32 rd rs => Pfloatdrnsz_i32 rd rs

+  | PArithRR Asmvliw.Pfixedwrzz rd rs => Pfixedwrzz rd rs

+  | PArithRR Asmvliw.Pfixeduwrzz rd rs => Pfixeduwrzz rd rs

+  | PArithRR Asmvliw.Pfixeddrzz rd rs => Pfixeddrzz rd rs

+  | PArithRR Asmvliw.Pfixedudrzz rd rs => Pfixedudrzz rd rs

+  | PArithRR Asmvliw.Pfixeddrzz_i32 rd rs => Pfixeddrzz_i32 rd rs

+  | PArithRR Asmvliw.Pfixedudrzz_i32 rd rs => Pfixedudrzz_i32 rd rs

 

   (* RI32 *)

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

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

 

   (* RI64 *)

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

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

 

   (* RF32 *)

-  | PArithRF32 Asmblock.Pmakefs rd imm => Pmakefs rd imm

+  | PArithRF32 Asmvliw.Pmakefs rd imm => Pmakefs rd imm

 

   (* RF64 *)

-  | PArithRF64 Asmblock.Pmakef rd imm => Pmakef rd imm

+  | PArithRF64 Asmvliw.Pmakef rd imm => Pmakef 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.Pfcompw ft) rd rs1 rs2 => Pfcompw ft rd rs1 rs2

-  | PArithRRR (Asmblock.Pfcompl ft) rd rs1 rs2 => Pfcompl ft 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.Pnandw rd rs1 rs2      => Pnandw rd rs1 rs2

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

-  | PArithRRR Asmblock.Pnorw rd rs1 rs2       => Pnorw rd rs1 rs2

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

-  | PArithRRR Asmblock.Pnxorw rd rs1 rs2      => Pnxorw rd rs1 rs2

-  | PArithRRR Asmblock.Pandnw rd rs1 rs2      => Pandnw rd rs1 rs2

-  | PArithRRR Asmblock.Pornw rd rs1 rs2       => Pornw 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.Pnandl rd rs1 rs2      => Pnandl rd rs1 rs2

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

-  | PArithRRR Asmblock.Pnorl rd rs1 rs2       => Pnorl rd rs1 rs2

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

-  | PArithRRR Asmblock.Pnxorl rd rs1 rs2      => Pnxorl rd rs1 rs2

-  | PArithRRR Asmblock.Pandnl rd rs1 rs2      => Pandnl rd rs1 rs2

-  | PArithRRR Asmblock.Pornl rd rs1 rs2       => Pornl 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

-

-  | PArithRRR Asmblock.Pfaddd rd rs1 rs2      => Pfaddd rd rs1 rs2

-  | PArithRRR Asmblock.Pfaddw rd rs1 rs2      => Pfaddw rd rs1 rs2

-  | PArithRRR Asmblock.Pfsbfd rd rs1 rs2      => Pfsbfd rd rs1 rs2

-  | PArithRRR Asmblock.Pfsbfw rd rs1 rs2      => Pfsbfw rd rs1 rs2

-  | PArithRRR Asmblock.Pfmuld rd rs1 rs2      => Pfmuld rd rs1 rs2

-  | PArithRRR Asmblock.Pfmulw rd rs1 rs2      => Pfmulw rd rs1 rs2

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

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

+  | PArithRRR (Asmvliw.Pfcompw ft) rd rs1 rs2 => Pfcompw ft rd rs1 rs2

+  | PArithRRR (Asmvliw.Pfcompl ft) rd rs1 rs2 => Pfcompl ft rd rs1 rs2

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

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

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

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

+  | PArithRRR Asmvliw.Pnandw rd rs1 rs2      => Pnandw rd rs1 rs2

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

+  | PArithRRR Asmvliw.Pnorw rd rs1 rs2       => Pnorw rd rs1 rs2

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

+  | PArithRRR Asmvliw.Pnxorw rd rs1 rs2      => Pnxorw rd rs1 rs2

+  | PArithRRR Asmvliw.Pandnw rd rs1 rs2      => Pandnw rd rs1 rs2

+  | PArithRRR Asmvliw.Pornw rd rs1 rs2       => Pornw rd rs1 rs2

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

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

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

+

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

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

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

+  | PArithRRR Asmvliw.Pnandl rd rs1 rs2      => Pnandl rd rs1 rs2

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

+  | PArithRRR Asmvliw.Pnorl rd rs1 rs2       => Pnorl rd rs1 rs2

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

+  | PArithRRR Asmvliw.Pnxorl rd rs1 rs2      => Pnxorl rd rs1 rs2

+  | PArithRRR Asmvliw.Pandnl rd rs1 rs2      => Pandnl rd rs1 rs2

+  | PArithRRR Asmvliw.Pornl rd rs1 rs2       => Pornl rd rs1 rs2

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

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

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

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

+

+  | PArithRRR Asmvliw.Pfaddd rd rs1 rs2      => Pfaddd rd rs1 rs2

+  | PArithRRR Asmvliw.Pfaddw rd rs1 rs2      => Pfaddw rd rs1 rs2

+  | PArithRRR Asmvliw.Pfsbfd rd rs1 rs2      => Pfsbfd rd rs1 rs2

+  | PArithRRR Asmvliw.Pfsbfw rd rs1 rs2      => Pfsbfw rd rs1 rs2

+  | PArithRRR Asmvliw.Pfmuld rd rs1 rs2      => Pfmuld rd rs1 rs2

+  | PArithRRR Asmvliw.Pfmulw rd rs1 rs2      => Pfmulw 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.Pmuliw rd rs imm       => Pmuliw rd rs imm

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

-  | PArithRRI32 Asmblock.Pnandiw rd rs imm      => Pnandiw rd rs imm

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

-  | PArithRRI32 Asmblock.Pnoriw rd rs imm       => Pnoriw rd rs imm

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

-  | PArithRRI32 Asmblock.Pnxoriw rd rs imm      => Pnxoriw rd rs imm

-  | PArithRRI32 Asmblock.Pandniw rd rs imm      => Pandniw rd rs imm

-  | PArithRRI32 Asmblock.Porniw rd rs imm       => Porniw 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.Proriw rd rs imm       => Proriw 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

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

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

+  | PArithRRI32 Asmvliw.Pmuliw rd rs imm       => Pmuliw rd rs imm

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

+  | PArithRRI32 Asmvliw.Pnandiw rd rs imm      => Pnandiw rd rs imm

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

+  | PArithRRI32 Asmvliw.Pnoriw rd rs imm       => Pnoriw rd rs imm

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

+  | PArithRRI32 Asmvliw.Pnxoriw rd rs imm      => Pnxoriw rd rs imm

+  | PArithRRI32 Asmvliw.Pandniw rd rs imm      => Pandniw rd rs imm

+  | PArithRRI32 Asmvliw.Porniw rd rs imm       => Porniw rd rs imm

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

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

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

+  | PArithRRI32 Asmvliw.Proriw rd rs imm       => Proriw rd rs imm

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

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

+  | PArithRRI32 Asmvliw.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.Pmulil rd rs imm       => Pmulil rd rs imm

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

-  | PArithRRI64 Asmblock.Pnandil rd rs imm      => Pnandil rd rs imm

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

-  | PArithRRI64 Asmblock.Pnoril rd rs imm       => Pnoril rd rs imm

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

-  | PArithRRI64 Asmblock.Pnxoril rd rs imm      => Pnxoril rd rs imm

-  | PArithRRI64 Asmblock.Pandnil rd rs imm      => Pandnil rd rs imm

-  | PArithRRI64 Asmblock.Pornil rd rs imm       => Pornil rd rs imm

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

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

+  | PArithRRI64 Asmvliw.Pmulil rd rs imm       => Pmulil rd rs imm

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

+  | PArithRRI64 Asmvliw.Pnandil rd rs imm      => Pnandil rd rs imm

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

+  | PArithRRI64 Asmvliw.Pnoril rd rs imm       => Pnoril rd rs imm

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

+  | PArithRRI64 Asmvliw.Pnxoril rd rs imm      => Pnxoril rd rs imm

+  | PArithRRI64 Asmvliw.Pandnil rd rs imm      => Pandnil rd rs imm

+  | PArithRRI64 Asmvliw.Pornil rd rs imm       => Pornil rd rs imm

 

   (** ARRR *)

-  | PArithARRR Asmblock.Pmaddw rd rs1 rs2       => Pmaddw rd rs1 rs2

-  | PArithARRR Asmblock.Pmaddl rd rs1 rs2       => Pmaddl rd rs1 rs2

-  | PArithARRR (Asmblock.Pcmove cond) rd rs1 rs2=> Pcmove cond rd rs1 rs2

-  | PArithARRR (Asmblock.Pcmoveu cond) rd rs1 rs2=> Pcmoveu cond rd rs1 rs2

+  | PArithARRR Asmvliw.Pmaddw rd rs1 rs2       => Pmaddw rd rs1 rs2

+  | PArithARRR Asmvliw.Pmaddl rd rs1 rs2       => Pmaddl rd rs1 rs2

+  | PArithARRR (Asmvliw.Pcmove cond) rd rs1 rs2=> Pcmove cond rd rs1 rs2

+  | PArithARRR (Asmvliw.Pcmoveu cond) rd rs1 rs2=> Pcmoveu cond rd rs1 rs2

 

   (** ARRI32 *)

-  | PArithARRI32 Asmblock.Pmaddiw rd rs1 imm    => Pmaddiw rd rs1 imm

+  | PArithARRI32 Asmvliw.Pmaddiw rd rs1 imm    => Pmaddiw rd rs1 imm

 

   (** ARRI64 *)

-  | PArithARRI64 Asmblock.Pmaddil rd rs1 imm    => Pmaddil rd rs1 imm

+  | PArithARRI64 Asmvliw.Pmaddil rd rs1 imm    => Pmaddil rd rs1 imm

                                                           

   (** Load *)

-  | PLoadRRO Asmblock.Plb rd ra ofs   => Plb rd ra (AOff ofs)

-  | PLoadRRO Asmblock.Plbu rd ra ofs  => Plbu rd ra (AOff ofs)

-  | PLoadRRO Asmblock.Plh rd ra ofs   => Plh rd ra (AOff ofs)

-  | PLoadRRO Asmblock.Plhu rd ra ofs  => Plhu rd ra (AOff ofs)

-  | PLoadRRO Asmblock.Plw rd ra ofs   => Plw rd ra (AOff ofs)

-  | PLoadRRO Asmblock.Plw_a rd ra ofs => Plw_a rd ra (AOff ofs)

-  | PLoadRRO Asmblock.Pld rd ra ofs   => Pld rd ra (AOff ofs)

-  | PLoadRRO Asmblock.Pld_a rd ra ofs => Pld_a rd ra (AOff ofs)

-  | PLoadRRO Asmblock.Pfls rd ra ofs  => Pfls rd ra (AOff ofs)

-  | PLoadRRO Asmblock.Pfld rd ra ofs  => Pfld rd ra (AOff ofs)

-

-  | PLoadRRR Asmblock.Plb rd ra ro   => Plb rd ra (AReg ro)

-  | PLoadRRR Asmblock.Plbu rd ra ro  => Plbu rd ra (AReg ro)

-  | PLoadRRR Asmblock.Plh rd ra ro   => Plh rd ra (AReg ro)

-  | PLoadRRR Asmblock.Plhu rd ra ro  => Plhu rd ra (AReg ro)

-  | PLoadRRR Asmblock.Plw rd ra ro   => Plw rd ra (AReg ro)

-  | PLoadRRR Asmblock.Plw_a rd ra ro => Plw_a rd ra (AReg ro)

-  | PLoadRRR Asmblock.Pld rd ra ro   => Pld rd ra (AReg ro)

-  | PLoadRRR Asmblock.Pld_a rd ra ro => Pld_a rd ra (AReg ro)

-  | PLoadRRR Asmblock.Pfls rd ra ro  => Pfls rd ra (AReg ro)

-  | PLoadRRR Asmblock.Pfld rd ra ro  => Pfld rd ra (AReg ro)

+  | PLoadRRO Asmvliw.Plb rd ra ofs   => Plb rd ra (AOff ofs)

+  | PLoadRRO Asmvliw.Plbu rd ra ofs  => Plbu rd ra (AOff ofs)

+  | PLoadRRO Asmvliw.Plh rd ra ofs   => Plh rd ra (AOff ofs)

+  | PLoadRRO Asmvliw.Plhu rd ra ofs  => Plhu rd ra (AOff ofs)

+  | PLoadRRO Asmvliw.Plw rd ra ofs   => Plw rd ra (AOff ofs)

+  | PLoadRRO Asmvliw.Plw_a rd ra ofs => Plw_a rd ra (AOff ofs)

+  | PLoadRRO Asmvliw.Pld rd ra ofs   => Pld rd ra (AOff ofs)

+  | PLoadRRO Asmvliw.Pld_a rd ra ofs => Pld_a rd ra (AOff ofs)

+  | PLoadRRO Asmvliw.Pfls rd ra ofs  => Pfls rd ra (AOff ofs)

+  | PLoadRRO Asmvliw.Pfld rd ra ofs  => Pfld rd ra (AOff ofs)

+

+  | PLoadRRR Asmvliw.Plb rd ra ro   => Plb rd ra (AReg ro)

+  | PLoadRRR Asmvliw.Plbu rd ra ro  => Plbu rd ra (AReg ro)

+  | PLoadRRR Asmvliw.Plh rd ra ro   => Plh rd ra (AReg ro)

+  | PLoadRRR Asmvliw.Plhu rd ra ro  => Plhu rd ra (AReg ro)

+  | PLoadRRR Asmvliw.Plw rd ra ro   => Plw rd ra (AReg ro)

+  | PLoadRRR Asmvliw.Plw_a rd ra ro => Plw_a rd ra (AReg ro)

+  | PLoadRRR Asmvliw.Pld rd ra ro   => Pld rd ra (AReg ro)

+  | PLoadRRR Asmvliw.Pld_a rd ra ro => Pld_a rd ra (AReg ro)

+  | PLoadRRR Asmvliw.Pfls rd ra ro  => Pfls rd ra (AReg ro)

+  | PLoadRRR Asmvliw.Pfld rd ra ro  => Pfld rd ra (AReg ro)

 

   (** Store *)

-  | PStoreRRO Asmblock.Psb rd ra ofs  => Psb rd ra (AOff ofs)

-  | PStoreRRO Asmblock.Psh rd ra ofs => Psh rd ra (AOff ofs)

-  | PStoreRRO Asmblock.Psw rd ra ofs => Psw rd ra (AOff ofs)

-  | PStoreRRO Asmblock.Psw_a rd ra ofs => Psw_a rd ra (AOff ofs)

-  | PStoreRRO Asmblock.Psd rd ra ofs => Psd rd ra (AOff ofs)

-  | PStoreRRO Asmblock.Psd_a rd ra ofs => Psd_a rd ra (AOff ofs)

-  | PStoreRRO Asmblock.Pfss rd ra ofs => Pfss rd ra (AOff ofs)

-  | PStoreRRO Asmblock.Pfsd rd ra ofs => Pfsd rd ra (AOff ofs)

-

-  | PStoreRRR Asmblock.Psb rd ra ro  => Psb rd ra (AReg ro)

-  | PStoreRRR Asmblock.Psh rd ra ro => Psh rd ra (AReg ro)

-  | PStoreRRR Asmblock.Psw rd ra ro => Psw rd ra (AReg ro)

-  | PStoreRRR Asmblock.Psw_a rd ra ro => Psw_a rd ra (AReg ro)

-  | PStoreRRR Asmblock.Psd rd ra ro => Psd rd ra (AReg ro)

-  | PStoreRRR Asmblock.Psd_a rd ra ro => Psd_a rd ra (AReg ro)

-  | PStoreRRR Asmblock.Pfss rd ra ro => Pfss rd ra (AReg ro)

-  | PStoreRRR Asmblock.Pfsd rd ra ro => Pfsd rd ra (AReg ro)

+  | PStoreRRO Asmvliw.Psb rd ra ofs  => Psb rd ra (AOff ofs)

+  | PStoreRRO Asmvliw.Psh rd ra ofs => Psh rd ra (AOff ofs)

+  | PStoreRRO Asmvliw.Psw rd ra ofs => Psw rd ra (AOff ofs)

+  | PStoreRRO Asmvliw.Psw_a rd ra ofs => Psw_a rd ra (AOff ofs)

+  | PStoreRRO Asmvliw.Psd rd ra ofs => Psd rd ra (AOff ofs)

+  | PStoreRRO Asmvliw.Psd_a rd ra ofs => Psd_a rd ra (AOff ofs)

+  | PStoreRRO Asmvliw.Pfss rd ra ofs => Pfss rd ra (AOff ofs)

+  | PStoreRRO Asmvliw.Pfsd rd ra ofs => Pfsd rd ra (AOff ofs)

+

+  | PStoreRRR Asmvliw.Psb rd ra ro  => Psb rd ra (AReg ro)

+  | PStoreRRR Asmvliw.Psh rd ra ro => Psh rd ra (AReg ro)

+  | PStoreRRR Asmvliw.Psw rd ra ro => Psw rd ra (AReg ro)

+  | PStoreRRR Asmvliw.Psw_a rd ra ro => Psw_a rd ra (AReg ro)

+  | PStoreRRR Asmvliw.Psd rd ra ro => Psd rd ra (AReg ro)

+  | PStoreRRR Asmvliw.Psd_a rd ra ro => Psd_a rd ra (AReg ro)

+  | PStoreRRR Asmvliw.Pfss rd ra ro => Pfss rd ra (AReg ro)

+  | PStoreRRR Asmvliw.Pfsd rd ra ro => Pfsd rd ra (AReg ro)

 

   end.

 

@@ -453,7 +453,7 @@ 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 function_proj (f: function) := Asmvliw.mkfunction (fn_sig f) (fn_blocks f).

 

 (* 

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

@@ -461,19 +461,19 @@ Definition fundef_proj (fu: fundef) : Asmblock.fundef := transf_fundef function_
 Definition program_proj (p: program) : Asmblock.program := transform_program fundef_proj p.

  *)

 

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

+Definition fundef_proj (fu: fundef) : Asmvliw.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 :=

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

   match gd with

   | Gfun f => Gfun (fundef_proj f)

   | Gvar gu => Gvar gu

   end.

 

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

+Program Definition genv_trans (ge: genv) : Asmvliw.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);

@@ -492,13 +492,13 @@ Qed. Next Obligation.
 Qed.

 

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

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

+                          : list (ident * globdef Asmvliw.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 :=

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

   {|  prog_defs := prog_defs_proj (prog_defs p);

       prog_public := prog_public p;

       prog_main := prog_main p

@@ -517,16 +517,16 @@ 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) |}.

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

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

+        fn_code := unfold (Asmvliw.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 : Asmblock.fundef -> fundef := AST.transf_fundef transf_function.

+Definition transf_fundef : Asmvliw.fundef -> fundef := AST.transf_fundef transf_function.

 

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

 Proof.

@@ -563,7 +563,7 @@ Proof.
 Qed.

  *)

 

-Definition transf_program : Asmblock.program -> program := transform_program transf_fundef.

+Definition transf_program : Asmvliw.program -> program := transform_program transf_fundef.

 

 Lemma program_equals {A B: Type} : forall (p1 p2: AST.program A B),

   prog_defs p1 = prog_defs p2 ->

@@ -586,7 +586,7 @@ Proof.
     rewrite transf_fundef_proj. auto.

 Qed.

 

-Definition match_prog (p: Asmblock.program) (tp: program) :=

+Definition match_prog (p: Asmvliw.program) (tp: program) :=

   match_program (fun _ f tf => tf = transf_fundef f) eq p tp.

 

 Lemma transf_program_match:

@@ -619,7 +619,7 @@ Qed.
 

 Section PRESERVATION.

 

-Variable prog: Asmblock.program.

+Variable prog: Asmvliw.program.

 Variable tprog: program.

 Hypothesis TRANSF: match_prog prog tprog.

 Let ge := Genv.globalenv prog.

diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v
index 339b44c6..ed145f21 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -31,458 +31,81 @@ Require Import Locations.
 Require Stacklayout.
 Require Import Conventions.
 Require Import Errors.
+Require Export Asmvliw.
 
-(** * 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. *)
-
-(** basic register *)
-Inductive preg: Type :=
-  | IR: gpreg -> preg                   (**r integer general purpose registers *)
-  | RA: preg
-  | PC: preg
-  .
-
-Coercion IR: gpreg >-> preg.
-
-Lemma preg_eq: forall (x y: preg), {x=y} + {x<>y}.
-Proof. decide equality. apply ireg_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'" := GPR17 (only parsing) : asm.
-Notation "'MFP'" := R17 (only parsing) : asm.
-Notation "'GPRA'" := GPR16 (only parsing) : asm.
-Notation "'RTMP'" := GPR32 (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 *)
-  .
-
-Inductive ftest: Type :=
-  | FTone                               (**r Ordered and Not Equal *)
-  | FTueq                               (**r Unordered or Equal *)
-  | FToeq                               (**r Ordered and Equal *)
-  | FTune                               (**r Unordered or Not Equal *)
-  | FTolt                               (**r Ordered and Less Than *)
-  | FTuge                               (**r Unordered or Greater Than or Equal *)
-  | FToge                               (**r Ordered and Greater Than or Equal *)
-  | FTult                               (**r Unordered or Less Than *)
-  .
-
-(** 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.
-*)
-
-(** * Instructions *)
-
-Definition label := positive.
-
-(* FIXME - rewrite the comment *)
-(** 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 in control-flow 
-*)
-Inductive ex_instruction : Type :=
-  (* Pseudo-instructions *)
-(*| Ploadsymbol_high (rd: ireg) (id: ident) (ofs: ptrofs) (**r load the high part of the address of a symbol *)
-  | 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) *)
-.
-
-(** FIXME: comment not up to date !
-
-
- The pseudo-instructions are the following:
-
-- [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.
-
-- [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.
-*)
+(** * Auxiliary utilies on basic blocks *)
 
-(** Control Flow instructions *)
-Inductive cf_instruction : Type :=
-  | Pret                                            (**r return *)
-  | Pcall   (l: label)                              (**r function call *)
-  | Picall  (r: ireg)                               (**r function call on register value *)
-  | Pjumptable (r: ireg) (labels: list label) (**r N-way branch through a jump table (pseudo) *)
-
-  (* Pgoto is for tailcalls, Pj_l is for jumping to a particular label *)
-  | Pgoto   (l: label)                              (**r goto *)
-  | Pigoto  (r: ireg)                               (**r goto from register *)
-  | 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 load_name : Type :=
-  | Plb                                             (**r load byte *)
-  | Plbu                                            (**r load byte unsigned *)
-  | Plh                                             (**r load half word *)
-  | Plhu                                            (**r load half word unsigned *)
-  | Plw                                             (**r load int32 *)
-  | Plw_a                                           (**r load any32 *)
-  | Pld                                             (**r load int64 *)
-  | Pld_a                                           (**r load any64 *)
-  | Pfls                                            (**r load float *)
-  | Pfld                                            (**r load 64-bit float *)
-.
-
-Inductive ld_instruction : Type :=
-  | PLoadRRO   (i: load_name) (rd: ireg) (ra: ireg) (ofs: offset)
-  | PLoadRRR   (i: load_name) (rd: ireg) (ra: ireg) (rofs: ireg)
-.
-
-Coercion PLoadRRO:       load_name        >-> Funclass.
-Coercion PLoadRRR:       load_name        >-> Funclass.
-
-(** Stores **)
-Inductive store_name : Type :=
-  | Psb                                             (**r store byte *)
-  | Psh                                             (**r store half byte *)
-  | Psw                                             (**r store int32 *)
-  | Psw_a                                           (**r store any32 *)
-  | Psd                                             (**r store int64 *)
-  | Psd_a                                           (**r store any64 *)
-  | Pfss                                            (**r store float *)
-  | Pfsd                                            (**r store 64-bit float *)
-.
+(** ** A unified view of Kalray instructions *)
 
-Inductive st_instruction : Type :=
-  | PStoreRRO  (i: store_name) (rs: ireg) (ra: ireg) (ofs: offset)
-  | PStoreRRR  (i: store_name) (rs: ireg) (ra: ireg) (rofs: ireg)
-.
-
-Coercion PStoreRRO:       store_name        >-> Funclass.
-Coercion PStoreRRR:       store_name        >-> Funclass.
-
-(** Arithmetic instructions **)
-Inductive arith_name_r : Type :=
-  | Ploadsymbol (id: ident) (ofs: ptrofs)           (**r load the address of a symbol *)
-.
-
-Inductive arith_name_rr : Type :=
-  | Pmv                                             (**r register move *)
-  | Pnegw                                           (**r negate word *)
-  | Pnegl                                           (**r negate long *)
-  | Pcvtl2w                                         (**r Convert Long to Word *)
-  | Psxwd                                           (**r Sign Extend Word to Double Word *)
-  | Pzxwd                                           (**r Zero Extend Word to Double Word *)
-
-  | Pfabsd                                          (**r float absolute double *)
-  | Pfabsw                                          (**r float absolute word *)
-  | Pfnegd                                          (**r float negate double *)
-  | Pfnegw                                          (**r float negate word *)
-  | Pfnarrowdw                                      (**r float narrow 64 -> 32 bits *)
-  | Pfwidenlwd                                      (**r Floating Point widen from 32 bits to 64 bits *)
-  | Pfloatwrnsz                                     (**r Floating Point conversion from integer (int -> SINGLE) *)
-  | Pfloatuwrnsz                                    (**r Floating Point conversion from integer (unsigned int -> SINGLE) *)
-  | Pfloatudrnsz                                    (**r Floating Point Conversion from integer (unsigned long -> float) *)
-  | Pfloatudrnsz_i32                                (**r Floating Point Conversion from integer (unsigned int -> float) *)
-  | Pfloatdrnsz                                     (**r Floating Point Conversion from integer (long -> float) *)
-  | Pfloatdrnsz_i32                                 (**r Floating Point Conversion from integer (int -> float) *)
-  | Pfixedwrzz                                      (**r Integer conversion from floating point (single -> int) *)
-  | Pfixeduwrzz                                     (**r Integer conversion from floating point (single -> unsigned int) *)
-  | Pfixeddrzz                                      (**r Integer conversion from floating point (float -> long) *)
-  | Pfixedudrzz                                      (**r Integer conversion from floating point (float -> unsigned long) *)
-  | Pfixeddrzz_i32                                  (**r Integer conversion from floating point (float -> int) *)
-  | Pfixedudrzz_i32                                  (**r Integer conversion from floating point (float -> unsigned int) *)
-.
-
-Inductive arith_name_ri32 : Type :=
-  | Pmake                                           (**r load immediate *)
-.
-
-Inductive arith_name_ri64 : Type :=
-  | Pmakel                                          (**r load immediate long *)
-.
-
-Inductive arith_name_rf32 : Type :=
-  | Pmakefs                                         (**r load immediate single *)
-.
-
-Inductive arith_name_rf64 : Type :=
-  | Pmakef                                          (**r load immediate float *)
-.
-
-Inductive arith_name_rrr : Type :=
-  | Pcompw  (it: itest)                             (**r comparison word *)
-  | Pcompl  (it: itest)                             (**r comparison long *)
-  | Pfcompw (ft: ftest)                             (**r comparison float32 *)
-  | Pfcompl (ft: ftest)                             (**r comparison float64 *)
-
-  | Paddw                                           (**r add word *)
-  | Psubw                                           (**r sub word *)
-  | Pmulw                                           (**r mul word *)
-  | Pandw                                           (**r and word *)
-  | Pnandw                                          (**r nand word *)
-  | Porw                                            (**r or word *)
-  | Pnorw                                           (**r nor word *)
-  | Pxorw                                           (**r xor word *)
-  | Pnxorw                                          (**r nxor word *)
-  | Pandnw                                          (**r andn word *)
-  | Pornw                                           (**r orn 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 *)
-  | Pnandl                                          (**r nand long *)
-  | Porl                                            (**r or long *)
-  | Pnorl                                           (**r nor long *)
-  | Pxorl                                           (**r xor long *)
-  | Pnxorl                                          (**r nxor long *)
-  | Pandnl                                          (**r andn long *)
-  | Pornl                                           (**r orn 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 *)
-
-  | Pfaddd                                          (**r float add double *)
-  | Pfaddw                                          (**r float add word *)
-  | Pfsbfd                                          (**r float sub double *)
-  | Pfsbfw                                          (**r float sub word *)
-  | Pfmuld                                          (**r float multiply double *)
-  | Pfmulw                                          (**r float multiply word *)
-.
-
-Inductive arith_name_rri32 : Type :=
-  | Pcompiw (it: itest)                             (**r comparison imm word *)
-
-  | Paddiw                                          (**r add imm word *)
-  | Pmuliw                                          (**r add imm word *)
-  | Pandiw                                          (**r and imm word *)
-  | Pnandiw                                         (**r nand imm word *)
-  | Poriw                                           (**r or imm word *)
-  | Pnoriw                                          (**r nor imm word *)
-  | Pxoriw                                          (**r xor imm word *)
-  | Pnxoriw                                         (**r nxor imm word *)
-  | Pandniw                                         (**r andn word *)
-  | Porniw                                          (**r orn word *)
-  | Psraiw                                          (**r shift right arithmetic imm word *)
-  | Psrliw                                          (**r shift right logical imm word *)
-  | Pslliw                                          (**r shift left logical imm word *)
-  | Proriw                                          (**r rotate right 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 *) 
-  | Pmulil                                          (**r mul immediate long *) 
-  | Pandil                                          (**r and immediate long *) 
-  | Pnandil                                         (**r nand immediate long *) 
-  | Poril                                           (**r or immediate long *) 
-  | Pnoril                                          (**r nor immediate long *) 
-  | Pxoril                                          (**r xor immediate long *) 
-  | Pnxoril                                         (**r nxor immediate long *) 
-  | Pandnil                                         (**r andn immediate long *)
-  | Pornil                                          (**r orn immediate long *)
-.
-
-Inductive arith_name_arrr : Type :=
-  | Pmaddw                                           (**r multiply add word *)
-  | Pmaddl                                           (**r multiply add long *)
-  | Pcmove (bt: btest)                               (**r conditional move *)
-  | Pcmoveu (bt: btest)                              (**r conditional move, test on unsigned semantics *)
+Inductive instruction : Type :=
+  | PBasic    (i: basic)
+  | PControl  (i: control)
 .
 
-Inductive arith_name_arri32 : Type :=
-  | Pmaddiw                                           (**r multiply add word *)
-.
+Coercion PBasic:    basic >-> instruction.
+Coercion PControl:  control >-> instruction.
 
-Inductive arith_name_arri64 : Type :=
-  | Pmaddil                                           (**r multiply add long *)
-.
+Definition code := list instruction.
+Definition bcode := list basic.
 
-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)
-  | PArithRF32  (i: arith_name_rf32)  (rd: ireg) (imm: float32)
-  | PArithRF64  (i: arith_name_rf64)  (rd: ireg) (imm: float)
-  | 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)
-  | PArithARRR   (i: arith_name_arrr)   (rd rs1 rs2: ireg)
-  | PArithARRI32 (i: arith_name_arri32) (rd rs: ireg) (imm: int)
-  | PArithARRI64 (i: arith_name_arri64) (rd rs: ireg) (imm: int64)
-.
+Fixpoint basics_to_code (l: list basic) :=
+  match l with
+  | nil => nil
+  | bi::l => (PBasic bi)::(basics_to_code l)
+  end.
 
-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 PArithRF32:    arith_name_rf32     >-> Funclass.
-Coercion PArithRF64:    arith_name_rf64     >-> Funclass.
-Coercion PArithRRR:     arith_name_rrr      >-> Funclass.
-Coercion PArithRRI32:   arith_name_rri32    >-> Funclass.
-Coercion PArithRRI64:   arith_name_rri64    >-> Funclass.
-Coercion PArithARRR:     arith_name_arrr      >-> Funclass.
-Coercion PArithARRI32:   arith_name_arri32    >-> Funclass.
-Coercion PArithARRI64:   arith_name_arri64    >-> Funclass.
-
-Inductive basic : Type :=
-  | PArith          (i: ar_instruction)
-  | PLoad           (i: ld_instruction)
-  | PStore          (i: st_instruction)
-  | Pallocframe (sz: Z) (pos: ptrofs)               (**r allocate new stack frame *)
-  | Pfreeframe  (sz: Z) (pos: ptrofs)               (**r deallocate stack frame and restore previous frame *)
-  | Pget    (rd: ireg) (rs: preg)                   (**r get system register *)
-  | Pset    (rd: preg) (rs: ireg)                   (**r set system register *)
-  | Pnop                                            (**r virtual instruction that does nothing *)
-.
+Fixpoint code_to_basics (c: code) :=
+  match c with
+  | (PBasic i)::c =>
+    match code_to_basics c with
+    | None => None
+    | Some l => Some (i::l)
+    end
+  | _::c => None
+  | nil => Some nil
+  end.
 
-Coercion PLoad:         ld_instruction >-> basic.
-Coercion PStore:        st_instruction >-> basic.
-Coercion PArith:        ar_instruction >-> basic.
+Lemma code_to_basics_id: forall c, code_to_basics (basics_to_code c) = Some c.
+Proof.
+  intros. induction c as [|i c]; simpl; auto.
+  rewrite IHc. auto.
+Qed.
 
+Lemma code_to_basics_dist:
+  forall c c' l l',
+  code_to_basics c = Some l ->
+  code_to_basics c' = Some l' ->
+  code_to_basics (c ++ c') = Some (l ++ l').
+Proof.
+  induction c as [|i c]; simpl; auto.
+  - intros. inv H. simpl. auto.
+  - intros. destruct i; try discriminate. destruct (code_to_basics c) eqn:CTB; try discriminate.
+    inv H. erewrite IHc; eauto. auto.
+Qed.
 
-Inductive control : Type :=
-  | PExpand         (i: ex_instruction)
-  | PCtlFlow        (i: cf_instruction)
-.
+(** 
+  Asmblockgen will have to translate a Mach control into a list of instructions of the form
+   i1 :: i2 :: i3 :: ctl :: nil ; where i1..i3 are basic instructions, ctl is a control instruction
+  These functions provide way to extract the basic / control instructions
+*)
 
-Coercion PExpand:   ex_instruction >-> control.
-Coercion PCtlFlow:  cf_instruction >-> control.
+Fixpoint extract_basic (c: code) :=
+  match c with
+  | nil => nil
+  | PBasic i :: c => i :: (extract_basic c)
+  | PControl i :: c => nil
+  end.
 
+Fixpoint extract_ctl (c: code) :=
+  match c with
+  | nil => None
+  | PBasic i :: c => extract_ctl c
+  | PControl i :: nil => Some i
+  | PControl i :: _ => None (* if the first found control instruction isn't the last *)
+  end.
 
-(** * Definition of a bblock *)
+(** ** Wellformness of basic blocks *)
 
 Ltac exploreInst :=
   repeat match goal with
@@ -498,20 +121,6 @@ Ltac exploreInst :=
 Definition non_empty_bblock (body: list basic) (exit: option control): Prop
  := body <> nil \/ exit <> None.
 
-Definition non_empty_body (body: list basic): bool :=
-  match body with
-  | nil => false
-  | _ => true
-  end.
-
-Definition non_empty_exit (exit: option control): bool :=
-  match exit with
-  | None => false
-  | _ => true
-  end.
-
-Definition non_empty_bblockb (body: list basic) (exit: option control): bool := non_empty_body body || non_empty_exit exit.
-
 Lemma non_empty_bblock_refl:
   forall body exit,
   non_empty_bblock body exit <->
@@ -529,15 +138,6 @@ Qed.
 Definition builtin_alone (body: list basic) (exit: option control) := forall ef args res,
   exit = Some (PExpand (Pbuiltin ef args res)) -> body = nil.
 
-Definition builtin_aloneb (body: list basic) (exit: option control) :=
-  match exit with
-  | Some (PExpand (Pbuiltin _ _ _)) =>
-    match body with
-    | nil => true
-    | _ => false
-    end
-  | _ => true
-  end.
 
 Lemma builtin_alone_refl:
   forall body exit,
@@ -556,9 +156,6 @@ Proof.
     + intros. discriminate.
 Qed.
 
-Definition wf_bblockb (body: list basic) (exit: option control) :=
-  (non_empty_bblockb body exit) && (builtin_aloneb body exit).
-
 Definition wf_bblock (body: list basic) (exit: option control) :=
   non_empty_bblock body exit /\ builtin_alone body exit.
 
@@ -574,16 +171,6 @@ Proof.
     unfold wf_bblock. split; auto.
 Qed.
 
-(** A bblock is well-formed if he contains at least one instruction,
-    and if there is a builtin then it must be alone in this bblock. *)
-
-Record bblock := mk_bblock {
-  header: list label;
-  body: list basic;
-  exit: option control;
-  correct: Is_true (wf_bblockb body exit)
-}.
-
 Ltac bblock_auto_correct := (apply non_empty_bblock_refl; try discriminate; try (left; discriminate); try (right; discriminate)).
 (* Local Obligation Tactic := bblock_auto_correct. *)
 
@@ -602,24 +189,16 @@ Proof.
   auto.
 Qed.
 
-
-(* FIXME: redundant with definition in Machblock *)
-Definition length_opt {A} (o: option A) : nat :=
-  match o with
-  | Some o => 1
-  | None => 0
-  end.
-
-(* WARNING: the notion of size is not the same than in Machblock !
-   We ignore labels here...
-   The result is in Z to be compatible with operations on PC
-*)
-Definition size (b:bblock): Z := Z.of_nat (length (body b) + length_opt (exit b)).
-(*   match (body b, exit b) with
-  | (nil, None) => 1
-  | _ => 
+Program Definition bblock_single_inst (i: instruction) :=
+  match i with
+  | PBasic b => {| header:=nil; body:=(b::nil); exit:=None |}
+  | PControl ctl => {| header:=nil; body:=nil; exit:=(Some ctl) |}
   end.
- *)
+Next Obligation.
+  apply wf_bblock_refl. constructor.
+    right. discriminate.
+    constructor.
+Qed.
 
 Lemma length_nonil {A: Type} : forall l:(list A), l <> nil -> (length l > 0)%nat.
 Proof.
@@ -640,11 +219,7 @@ Proof.
   unfold size. destruct b as [hd bdy ex cor]. simpl.
   destruct ex; destruct bdy; try (apply to_nat_pos; rewrite Nat2Z.id; simpl; omega).
   inversion cor; contradict H; simpl; auto.
-(*     rewrite eq. (* inversion COR. *) (* inversion H. *)
-  - assert ((length b > 0)%nat). apply length_nonil. auto.
-    omega.
-  - destruct e; simpl; try omega. contradict H; simpl; auto.
- *)Qed.
+Qed.
 
 
 Program Definition no_header (bb : bblock) := {| header := nil; body := body bb; exit := exit bb |}.
@@ -676,727 +251,30 @@ Proof.
 Qed.
 
 
-Definition bblocks := list bblock.
-
-Fixpoint size_blocks (l: bblocks): Z :=
-  match l with
-  | nil => 0
-  | b :: l =>
-     (size b) + (size_blocks l)
-  end
-  .
-
-Record function : Type := mkfunction { fn_sig: signature; fn_blocks: bblocks }.
-Definition fundef := AST.fundef function.
-Definition program := AST.program fundef unit.
-
-Inductive instruction : Type :=
-  | PBasic    (i: basic)
-  | PControl  (i: control)
-.
-
-Coercion PBasic:    basic >-> instruction.
-Coercion PControl:  control >-> instruction.
-
-Definition code := list instruction.
-Definition bcode := list basic.
 
-Fixpoint basics_to_code (l: list basic) :=
-  match l with
-  | nil => nil
-  | bi::l => (PBasic bi)::(basics_to_code l)
-  end.
-
-Fixpoint code_to_basics (c: code) :=
-  match c with
-  | (PBasic i)::c =>
-    match code_to_basics c with
-    | None => None
-    | Some l => Some (i::l)
-    end
-  | _::c => None
-  | nil => Some nil
-  end.
-
-Lemma code_to_basics_id: forall c, code_to_basics (basics_to_code c) = Some c.
-Proof.
-  intros. induction c as [|i c]; simpl; auto.
-  rewrite IHc. auto.
-Qed.
-
-Lemma code_to_basics_dist:
-  forall c c' l l',
-  code_to_basics c = Some l ->
-  code_to_basics c' = Some l' ->
-  code_to_basics (c ++ c') = Some (l ++ l').
-Proof.
-  induction c as [|i c]; simpl; auto.
-  - intros. inv H. simpl. auto.
-  - intros. destruct i; try discriminate. destruct (code_to_basics c) eqn:CTB; try discriminate.
-    inv H. erewrite IHc; eauto. auto.
-Qed.
-
-(** 
-  Asmblockgen will have to translate a Mach control into a list of instructions of the form
-   i1 :: i2 :: i3 :: ctl :: nil ; where i1..i3 are basic instructions, ctl is a control instruction
-  These functions provide way to extract the basic / control instructions
-*)
-
-Fixpoint extract_basic (c: code) :=
-  match c with
-  | nil => nil
-  | PBasic i :: c => i :: (extract_basic c)
-  | PControl i :: c => nil
-  end.
-
-Fixpoint extract_ctl (c: code) :=
-  match c with
-  | nil => None
-  | PBasic i :: c => extract_ctl c
-  | PControl i :: nil => Some i
-  | PControl i :: _ => None (* if the first found control instruction isn't the last *)
-  end.
-
-(** * Utility for Asmblockgen *)
-
-Program Definition bblock_single_inst (i: instruction) :=
-  match i with
-  | PBasic b => {| header:=nil; body:=(b::nil); exit:=None |}
-  | PControl ctl => {| header:=nil; body:=nil; exit:=(Some ctl) |}
-  end.
-Next Obligation.
-  apply wf_bblock_refl. constructor.
-    right. discriminate.
-    constructor.
-Qed.
-
-(** This definition is not used anymore *)
-(* Program Definition bblock_basic_ctl (c: list basic) (i: option control) :=
-  match i with
-  | Some i => {| header:=nil; body:=c; exit:=Some i |}
-  | None =>
-    match c with
-    | _::_ => {| header:=nil; body:=c; exit:=None |}
-    | nil => {| header:=nil; body:=Pnop::nil; exit:=None |}
-    end
-  end.
-Next Obligation.
-  bblock_auto_correct.
-Qed. Next Obligation.
-  bblock_auto_correct.
-Qed. *)
-
-
-(** * 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.
-
-Notation "a # b" := (a b) (at level 1, only parsing) : asm.
-Notation "a # b <- c" := (Pregmap.set b c a) (at level 1, b at next level) : asm.
-
-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.
-
-(* TODO: Is it still useful ?? *)
-
-
-(** 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.
 
+(** * Sequential Semantics of basic blocks *)
 Section RELSEM.
 
-
-(** 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 (rs:regset) (m:mem)
-  | Stuck.
-(* Arguments outcome: clear implicits. *)
-
-
-(** ** Arithmetic Expressions (including comparisons) *)
-
-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.
-
-Inductive oporder_ftest :=
-  | Normal (ft: ftest)
-  | Reversed (ft: ftest)
-.
-
-Definition ftest_for_cmp (c: comparison) :=
-  match c with
-  | Ceq => Normal FToeq
-  | Cne => Normal FTune
-  | Clt => Normal FTolt
-  | Cle => Reversed FToge
-  | Cgt => Reversed FTolt
-  | Cge => Normal FToge
-  end.
-
-Definition notftest_for_cmp (c: comparison) :=
-  match c with
-  | Ceq => Normal FTune
-  | Cne => Normal FToeq
-  | Clt => Normal FTuge
-  | Cle => Reversed FTult
-  | Cgt => Reversed FTuge
-  | Cge => Normal FTult
-  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.
-
-
-(* a few lemma on comparisons of unsigned (e.g. pointers) *)
-
-Definition Val_cmpu_bool cmp v1 v2: option bool :=
-  Val.cmpu_bool (fun _ _ => true) cmp v1 v2.
-
-Lemma Val_cmpu_bool_correct (m:mem) (cmp: comparison) (v1 v2: val) b:
-   (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) = Some b
-   -> (Val_cmpu_bool cmp v1 v2) = Some b.
-Proof.
-  intros; eapply Val.cmpu_bool_lessdef; (econstructor 1 || eauto).
-Qed.
-
-Definition Val_cmpu cmp v1 v2 := Val.of_optbool (Val_cmpu_bool cmp v1 v2).
-
-Lemma Val_cmpu_correct (m:mem) (cmp: comparison) (v1 v2: val):
-   Val.lessdef (Val.cmpu (Mem.valid_pointer m) cmp v1 v2)
-               (Val_cmpu cmp v1 v2).
-Proof.
-  unfold Val.cmpu, Val_cmpu.
-  remember (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) as ob.
-  destruct ob; simpl.
-  - erewrite Val_cmpu_bool_correct; eauto.
-    econstructor.
-  - econstructor.
-Qed.
-
-Definition Val_cmplu_bool (cmp: comparison) (v1 v2: val)
- := (Val.cmplu_bool (fun _ _ => true) cmp v1 v2).
-
-Lemma Val_cmplu_bool_correct (m:mem) (cmp: comparison) (v1 v2: val) b:
-   (Val.cmplu_bool (Mem.valid_pointer m) cmp v1 v2) = Some b
-   -> (Val_cmplu_bool cmp v1 v2) = Some b.
-Proof.
-  intros; eapply Val.cmplu_bool_lessdef; (econstructor 1 || eauto).
-Qed.
-
-Definition Val_cmplu cmp v1 v2 := Val.of_optbool (Val_cmplu_bool cmp v1 v2).
-
-Lemma Val_cmplu_correct (m:mem) (cmp: comparison) (v1 v2: val):
-   Val.lessdef (Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp v1 v2))
-               (Val_cmplu cmp v1 v2).
-Proof.
-  unfold Val.cmplu, Val_cmplu.
-  remember (Val.cmplu_bool (Mem.valid_pointer m) cmp v1 v2) as ob.
-  destruct ob as [b|]; simpl.
-  - erewrite Val_cmplu_bool_correct; eauto.
-    simpl. econstructor.
-  - econstructor.
-Qed.
-
-
-(** Comparing integers *)
-Definition compare_int (t: itest) (v1 v2: val): 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 Cne v1 v2
-  | ITequ => Val_cmpu Ceq v1 v2
-  | ITltu => Val_cmpu Clt v1 v2
-  | ITgeu => Val_cmpu Cge v1 v2
-  | ITleu => Val_cmpu Cle v1 v2
-  | ITgtu => Val_cmpu Cgt v1 v2
-  | ITall
-  | ITnall
-  | ITany
-  | ITnone => Vundef
-  end.
-
-Definition compare_long (t: itest) (v1 v2: val): 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 => Some (Val_cmplu Cne v1 v2)
-  | ITequ => Some (Val_cmplu Ceq v1 v2)
-  | ITltu => Some (Val_cmplu Clt v1 v2)
-  | ITgeu => Some (Val_cmplu Cge v1 v2)
-  | ITleu => Some (Val_cmplu Cle v1 v2)
-  | ITgtu => Some (Val_cmplu Cgt v1 v2)
-  | ITall
-  | ITnall
-  | ITany
-  | ITnone => Some Vundef
-  end in 
-  match res with
-  | Some v => v
-  | None => Vundef
-  end
-  .
-
-Definition compare_single (t: ftest) (v1 v2: val): val :=
-  match t with
-  | FTone | FTueq => Vundef (* unused *)
-  | FToeq => Val.cmpfs Ceq v1 v2
-  | FTune => Val.cmpfs Cne v1 v2
-  | FTolt => Val.cmpfs Clt v1 v2
-  | FTuge => Val.notbool (Val.cmpfs Clt v1 v2)
-  | FToge => Val.cmpfs Cge v1 v2
-  | FTult => Val.notbool (Val.cmpfs Cge v1 v2)
-  end.
-
-Definition compare_float (t: ftest) (v1 v2: val): val :=
-  match t with
-  | FTone | FTueq => Vundef (* unused *)
-  | FToeq => Val.cmpf Ceq v1 v2
-  | FTune => Val.cmpf Cne v1 v2
-  | FTolt => Val.cmpf Clt v1 v2
-  | FTuge => Val.notbool (Val.cmpf Clt v1 v2)
-  | FToge => Val.cmpf Cge v1 v2
-  | FTult => Val.notbool (Val.cmpf Cge v1 v2)
-  end.
-
 (** Execution of arith instructions *)
 
 Variable ge: genv.
 
-Definition arith_eval_r n :=
-  match n with
-  | Ploadsymbol s ofs => Genv.symbol_address ge s ofs
-  end
-.
-
-Definition arith_eval_rr n v :=
-  match n with
-  | Pmv => v
-  | Pnegw => Val.neg v
-  | Pnegl => Val.negl v
-  | Pcvtl2w => Val.loword v
-  | Psxwd => Val.longofint v
-  | Pzxwd => Val.longofintu v
-  | Pfnegd => Val.negf v
-  | Pfnegw => Val.negfs v
-  | Pfabsd => Val.absf v
-  | Pfabsw => Val.absfs v
-  | Pfnarrowdw => Val.singleoffloat v
-  | Pfwidenlwd => Val.floatofsingle v
-  | Pfloatwrnsz => match Val.singleofint v with Some f => f | _ => Vundef end
-  | Pfloatuwrnsz => match Val.singleofintu v with Some f => f | _ => Vundef end
-  | Pfloatudrnsz => match Val.floatoflongu v with Some f => f | _ => Vundef end
-  | Pfloatdrnsz => match Val.floatoflong v with Some f => f | _ => Vundef end
-  | Pfloatudrnsz_i32 => match Val.floatofintu v with Some f => f | _ => Vundef end
-  | Pfloatdrnsz_i32 => match Val.floatofint v with Some f => f | _ => Vundef end
-  | Pfixedwrzz => match Val.intofsingle v with Some i => i | _ => Vundef end
-  | Pfixeduwrzz => match Val.intuofsingle v with Some i => i | _ => Vundef end
-  | Pfixeddrzz => match Val.longoffloat v with Some i => i | _ => Vundef end
-  | Pfixedudrzz => match Val.longuoffloat v with Some i => i | _ => Vundef end
-  | Pfixeddrzz_i32 => match Val.intoffloat v with Some i => i | _ => Vundef end
-  | Pfixedudrzz_i32 => match Val.intuoffloat v with Some i => i | _ => Vundef end
-  end.
-
-Definition arith_eval_ri32 n i :=
-  match n with
-  | Pmake => Vint i
-  end.
-
-Definition arith_eval_ri64 n i :=
-  match n with
-  | Pmakel => Vlong i
-  end.
-
-Definition arith_eval_rf32 n i :=
-  match n with
-  | Pmakefs => Vsingle i
-  end.
-
-Definition arith_eval_rf64 n i :=
-  match n with
-  | Pmakef => Vfloat i
-  end.
-
-Definition arith_eval_rrr n v1 v2 :=
-  match n with
-  | Pcompw c => compare_int c v1 v2
-  | Pcompl c => compare_long c v1 v2
-  | Pfcompw c => compare_single c v1 v2
-  | Pfcompl c => compare_float c v1 v2
-
-  | Paddw  => Val.add  v1 v2
-  | Psubw  => Val.sub  v1 v2
-  | Pmulw  => Val.mul  v1 v2
-  | Pandw  => Val.and  v1 v2
-  | Pnandw => Val.notint (Val.and v1 v2)
-  | Porw   => Val.or   v1 v2
-  | Pnorw  => Val.notint (Val.or v1 v2)
-  | Pxorw  => Val.xor  v1 v2
-  | Pnxorw => Val.notint (Val.xor v1 v2)
-  | Pandnw => Val.and (Val.notint v1) v2
-  | Pornw  => Val.or (Val.notint v1) v2
-  | Psrlw  => Val.shru v1 v2
-  | Psraw  => Val.shr  v1 v2
-  | Psllw  => Val.shl  v1 v2
-
-  | Paddl => Val.addl v1 v2
-  | Psubl => Val.subl v1 v2
-  | Pandl => Val.andl v1 v2
-  | Pnandl => Val.notl (Val.andl v1 v2)
-  | Porl  => Val.orl  v1 v2
-  | Pnorl  => Val.notl (Val.orl  v1 v2)
-  | Pxorl  => Val.xorl  v1 v2
-  | Pnxorl  => Val.notl (Val.xorl  v1 v2)
-  | Pandnl => Val.andl (Val.notl v1) v2
-  | Pornl  => Val.orl (Val.notl v1) v2
-  | Pmull => Val.mull v1 v2
-  | Pslll => Val.shll v1 v2
-  | Psrll => Val.shrlu v1 v2
-  | Psral => Val.shrl v1 v2
-
-  | Pfaddd => Val.addf v1 v2
-  | Pfaddw => Val.addfs v1 v2
-  | Pfsbfd => Val.subf v1 v2
-  | Pfsbfw => Val.subfs v1 v2
-  | Pfmuld => Val.mulf v1 v2
-  | Pfmulw => Val.mulfs v1 v2
-  end.
-
-Definition arith_eval_rri32 n v i :=
-  match n with
-  | Pcompiw c => compare_int c v (Vint i)
-  | Paddiw  => Val.add   v (Vint i)
-  | Pmuliw  => Val.mul   v (Vint i)
-  | Pandiw  => Val.and   v (Vint i)
-  | Pnandiw => Val.notint (Val.and  v (Vint i))
-  | Poriw   => Val.or    v (Vint i)
-  | Pnoriw  => Val.notint (Val.or v (Vint i))
-  | Pxoriw  => Val.xor   v (Vint i)
-  | Pnxoriw => Val.notint (Val.xor v (Vint i))
-  | Pandniw => Val.and (Val.notint v) (Vint i)
-  | Porniw  => Val.or (Val.notint v) (Vint i)
-  | Psraiw  => Val.shr   v (Vint i)
-  | Psrliw  => Val.shru  v (Vint i)
-  | Pslliw  => Val.shl   v (Vint i)
-  | Proriw  => Val.ror   v (Vint i)
-  | Psllil  => Val.shll  v (Vint i)
-  | Psrlil  => Val.shrlu v (Vint i)
-  | Psrail  => Val.shrl  v (Vint i)
-  end.
-
-Definition arith_eval_rri64 n v i :=
-  match n with
-  | Pcompil c => compare_long c v (Vlong i)
-  | Paddil  => Val.addl v (Vlong i)
-  | Pmulil  => Val.mull v (Vlong i)
-  | Pandil  => Val.andl v (Vlong i)
-  | Pnandil  => Val.notl (Val.andl v (Vlong i))
-  | Poril   => Val.orl  v (Vlong i)
-  | Pnoril   => Val.notl (Val.orl  v (Vlong i))
-  | Pxoril  => Val.xorl  v (Vlong i)
-  | Pnxoril  => Val.notl (Val.xorl  v (Vlong i))
-  | Pandnil => Val.andl (Val.notl v) (Vlong i)
-  | Pornil  => Val.orl (Val.notl v) (Vlong i)
-  end.
-
-Definition arith_eval_arrr n v1 v2 v3 :=
-  match n with
-  | Pmaddw => Val.add v1 (Val.mul v2 v3)
-  | Pmaddl => Val.addl v1 (Val.mull v2 v3)
-  | Pcmove bt =>
-    match cmp_for_btest bt with
-    | (Some c, Int)  =>
-      match Val.cmp_bool c v2 (Vint Int.zero) with
-      | None => Vundef
-      | Some true => v3
-      | Some false => v1
-      end
-    | (Some c, Long) =>
-      match Val.cmpl_bool c v2 (Vlong Int64.zero) with
-      | None => Vundef
-      | Some true => v3
-      | Some false => v1
-      end
-    | (None, _) => Vundef
-    end
-  | Pcmoveu bt =>
-    match cmpu_for_btest bt with
-    | (Some c, Int)  =>
-      match Val_cmpu_bool c v2 (Vint Int.zero) with
-      | None => Vundef
-      | Some true => v3
-      | Some false => v1
-      end
-    | (Some c, Long) =>
-      match Val_cmplu_bool c v2 (Vlong Int64.zero) with
-      | None => Vundef
-      | Some true => v3
-      | Some false => v1
-      end
-    | (None, _) => Vundef
-    end
-  end.                    
-
-Definition arith_eval_arri32 n v1 v2 v3 :=
-  match n with
-  | Pmaddiw => Val.add v1 (Val.mul v2 (Vint v3))
-  end.                    
-
-Definition arith_eval_arri64 n v1 v2 v3 :=
-  match n with
-  | Pmaddil => Val.addl v1 (Val.mull v2 (Vlong v3))
-  end.                    
-
-Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset :=
-  match ai with
-  | PArithR n d => rs#d <- (arith_eval_r n)
-
-  | PArithRR n d s => rs#d <- (arith_eval_rr n rs#s)
-
-  | PArithRI32 n d i => rs#d <- (arith_eval_ri32 n i)
-  | PArithRI64 n d i => rs#d <- (arith_eval_ri64 n i)
-  | PArithRF32 n d i => rs#d <- (arith_eval_rf32 n i)
-  | PArithRF64 n d i => rs#d <- (arith_eval_rf64 n i)
-
-  | PArithRRR n d s1 s2 => rs#d <- (arith_eval_rrr n rs#s1 rs#s2)
-
-  | PArithRRI32 n d s i => rs#d <- (arith_eval_rri32 n rs#s i)
-
-  | PArithRRI64 n d s i => rs#d <- (arith_eval_rri64 n rs#s i)
-
-  | PArithARRR n d s1 s2 => rs#d <- (arith_eval_arrr n rs#d rs#s1 rs#s2)
-
-  | PArithARRI32 n d s i => rs#d <- (arith_eval_arri32 n rs#d rs#s i)
-
-  | PArithARRI64 n d s i => rs#d <- (arith_eval_arri64 n rs#d rs#s i)
-  end.
-
-(** * load/store *)
+Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset := parexec_arith_instr ge ai rs rs.
 
 (** Auxiliaries for memory accesses *)
 
-Definition eval_offset (ofs: offset) : res ptrofs :=
-  match ofs with
-  | Ofsimm n => OK n
-  | Ofslow id delta => 
-      match (Genv.symbol_address ge id delta) with
-      | Vptr b ofs => OK ofs
-      | _ => Error (msg "Asmblock.eval_offset")
-      end
-  end.
-
-Definition exec_load_offset (chunk: memory_chunk) (rs: regset) (m: mem) (d a: ireg) (ofs: offset) :=
-  match (eval_offset ofs) with
-  | OK ptr => match Mem.loadv chunk m (Val.offset_ptr (rs a) ptr) with
-              | None => Stuck
-              | Some v => Next (rs#d <- v) m
-              end
-  | _ => Stuck
-  end.
-
-Definition exec_load_reg (chunk: memory_chunk) (rs: regset) (m: mem) (d a ro: ireg) :=
-  match Mem.loadv chunk m (Val.addl (rs a) (rs ro)) with
-  | None => Stuck
-  | Some v => Next (rs#d <- v) m
-  end.
-
-Definition exec_store_offset (chunk: memory_chunk) (rs: regset) (m: mem) (s a: ireg) (ofs: offset) :=
-  match (eval_offset ofs) with
-  | OK ptr => match Mem.storev chunk m (Val.offset_ptr (rs a) ptr) (rs s) with
-              | None => Stuck
-              | Some m' => Next rs m'
-              end
-  | _ => Stuck
-  end.
+Definition exec_load_offset (chunk: memory_chunk) (rs: regset) (m: mem) (d a: ireg) (ofs: offset) := parexec_load_offset ge chunk rs rs m m d a ofs.
 
-Definition exec_store_reg (chunk: memory_chunk) (rs: regset) (m: mem) (s a ro: ireg) :=
-  match Mem.storev chunk m (Val.addl (rs a) (rs ro)) (rs s) with
-  | None => Stuck
-  | Some m' => Next rs m'
-  end.
+Definition exec_load_reg (chunk: memory_chunk) (rs: regset) (m: mem) (d a ro: ireg) := parexec_load_reg chunk rs rs m m d a ro.
 
-Definition load_chunk n :=
-  match n with
-  | Plb => Mint8signed
-  | Plbu => Mint8unsigned
-  | Plh => Mint16signed
-  | Plhu => Mint16unsigned
-  | Plw => Mint32
-  | Plw_a => Many32
-  | Pld => Mint64
-  | Pld_a => Many64
-  | Pfls => Mfloat32
-  | Pfld => Mfloat64
-  end.
+Definition exec_store_offset (chunk: memory_chunk) (rs: regset) (m: mem) (s a: ireg) (ofs: offset) := parexec_store_offset ge chunk rs rs m m s a ofs.
 
-Definition store_chunk n :=
-  match n with
-  | Psb => Mint8unsigned
-  | Psh => Mint16unsigned
-  | Psw => Mint32
-  | Psw_a => Many32
-  | Psd => Mint64
-  | Psd_a => Many64
-  | Pfss => Mfloat32
-  | Pfsd => Mfloat64
-  end.
+Definition exec_store_reg (chunk: memory_chunk) (rs: regset) (m: mem) (s a ro: ireg) := parexec_store_reg chunk rs rs m m s a ro.
 
 (** * basic instructions *)
 
-Definition exec_basic_instr (bi: basic) (rs: regset) (m: mem) : outcome :=
-  match bi with
-  | PArith ai => Next (exec_arith_instr ai rs) m
-
-  | PLoadRRO n d a ofs => exec_load_offset (load_chunk n) rs m d a ofs
-  | PLoadRRR n d a ro => exec_load_reg (load_chunk n) rs m d a ro
-
-  | PStoreRRO n s a ofs => exec_store_offset (store_chunk n) rs m s a ofs
-  | PStoreRRR n s a ro => exec_store_reg (store_chunk n) rs m s a ro
-
-  | 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 (rs #FP <- (rs SP) #SP <- sp #RTMP <- 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 (rs#SP <- v #RTMP <- Vundef) m'
-              end
-          | _ => Stuck
-          end
-      end
-  | Pget rd ra =>
-    match ra with
-    | RA => Next (rs#rd <- (rs#ra)) m
-    | _  => Stuck
-    end
-  | Pset ra rd =>
-    match ra with
-    | RA => Next (rs#ra <- (rs#rd)) m
-    | _  => Stuck
-    end
-  | Pnop => Next rs m
-end.
+Definition exec_basic_instr (bi: basic) (rs: regset) (m: mem) : outcome := parexec_basic_instr ge bi rs rs m m.
 
 Fixpoint exec_body (body: list basic) (rs: regset) (m: mem): outcome :=
   match body with
@@ -1408,78 +286,16 @@ Fixpoint exec_body (body: list basic) (rs: regset) (m: mem): outcome :=
      end
   end.
 
-(** Manipulations over the [PC] register: continuing with the next
-  instruction ([nextblock]) or branching to a label ([goto_label]). *)
-
-Definition nextblock (b:bblock) (rs: regset) :=
-  rs#PC <- (Val.offset_ptr rs#PC (Ptrofs.repr (size b))).
-
-(** Looking up bblocks in a code sequence by position. *)
-Fixpoint find_bblock (pos: Z) (lb: bblocks) {struct lb} : option bblock :=
-  match lb with
-  | nil => None
-  | b :: il => 
-    if zlt pos 0 then None  (* NOTE: It is impossible to branch inside a block *)
-    else if zeq pos 0 then Some b
-    else find_bblock (pos - (size b)) il
-  end.
-
-
 (** Position corresponding to a label *)
 
-(** TODO: redundant w.r.t Machblock *)
-Lemma in_dec (lbl: label) (l: list label):  { List.In lbl l } + { ~(List.In lbl l) }.
-Proof.
-  apply List.in_dec.
-  apply Pos.eq_dec.
-Qed.
-
-
-(** Note: copy-paste from Machblock *)
-Definition is_label (lbl: label) (bb: bblock) : bool :=
-  if in_dec lbl (header bb) then true else false.
-
-Lemma is_label_correct_true lbl bb:
-  List.In lbl (header bb) <-> is_label lbl bb = true. 
-Proof.
-  unfold is_label; destruct (in_dec lbl (header bb)); simpl; intuition.
-Qed.
-
-Lemma is_label_correct_false lbl bb:
-  ~(List.In lbl (header bb)) <-> is_label lbl bb = false. 
-Proof.
-  unfold is_label; destruct (in_dec lbl (header bb)); simpl; intuition.
-Qed.
-
-(** convert a label into a position in the code *)
-Fixpoint label_pos (lbl: label) (pos: Z) (lb: bblocks) {struct lb} : option Z :=
-  match lb with
-  | nil => None
-  | b :: lb' => if is_label lbl b then Some pos else label_pos lbl (pos + (size b)) lb'
-  end.
-
-Definition goto_label (f: function) (lbl: label) (rs: regset) (m: mem) : outcome :=
-  match label_pos lbl 0 (fn_blocks 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.
+Definition goto_label (f: function) (lbl: label) (rs: regset) (m: mem) : outcome := par_goto_label f lbl rs rs m.
 
 (** Evaluating a branch 
 
 Warning: in m PC is assumed to be already pointing on the next instruction !
 
 *)
-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 rs m
-    | None => Stuck
-  end.
-
+Definition eval_branch (f: function) (l: label) (rs: regset) (m: mem) (res: option bool) : outcome := par_eval_branch f l rs rs m res.
 
 (** Execution of a single control-flow instruction [i] in initial state [rs] and
     [m].  Return updated state.
@@ -1497,55 +313,7 @@ Definition eval_branch (f: function) (l: label) (rs: regset) (m: mem) (res: opti
     we generate cannot use those registers to hold values that must
     survive the execution of the pseudo-instruction. *)
 
-Definition exec_control (f: function) (oc: option control) (rs: regset) (m: mem) : outcome :=
-  match oc with
-  | Some ic =>
-(** Get/Set system registers *)
-  match ic with
-
-
-(** Branch Control Unit instructions *)
-  | Pret =>
-      Next (rs#PC <- (rs#RA)) m
-  | Pcall s =>
-      Next (rs#RA <- (rs#PC) #PC <- (Genv.symbol_address ge s Ptrofs.zero)) m
-  | Picall r =>
-      Next (rs#RA <- (rs#PC) #PC <- (rs#r)) m
-  | Pgoto s =>
-      Next (rs#PC <- (Genv.symbol_address ge s Ptrofs.zero)) m
-  | Pigoto r =>
-      Next (rs#PC <- (rs#r)) m
-  | Pj_l l =>
-      goto_label f l rs m
-  | Pjumptable 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 #GPR62 <- Vundef #GPR63 <- Vundef) m
-          end
-      | _ => Stuck
-      end
-      
-  | 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 c rs#r (Vint (Int.repr 0)))
-      | (Some c, Long) => eval_branch f l rs m (Val_cmplu_bool c rs#r (Vlong (Int64.repr 0)))
-      | (None, _) => Stuck
-      end
-
-(** Pseudo-instructions *)
-  | Pbuiltin ef args res =>
-      Stuck (**r treated specially below *)
-  end
-  | None => Next rs m
-end.
+Definition exec_control (f: function) (oc: option control) (rs: regset) (m: mem) : outcome := parexec_control ge f oc rs rs m.
 
 Definition exec_bblock (f: function) (b: bblock) (rs0: regset) (m: mem) : outcome :=
   match exec_body (body b) rs0 m with
@@ -1554,79 +322,9 @@ Definition exec_bblock (f: function) (b: bblock) (rs0: regset) (m: mem) : outcom
   | Stuck => 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 - R16 and R32 are excluded *)
-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  | R8  => GPR8  | 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 | R31 => GPR31 (* | 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.
-
-(** Undefine all registers except SP and callee-save registers *)
-
-Definition undef_caller_save_regs (rs: regset) : regset :=
-  fun r =>
-    if preg_eq r SP
-    || In_dec preg_eq r (List.map preg_of (List.filter is_callee_save all_mregs))
-    then rs r
-    else Vundef.
-
-
-(** Extract the values of the arguments of an external call.
-    We exploit the calling conventions from module [Conventions], except that
-    we use 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.
-
-
-(** TODO
- * For now, we consider a builtin is alone in a basic block.
- * Perhaps there is a way to avoid that ?
- *)
-
 Inductive step: state -> trace -> state -> Prop :=
   | exec_step_internal:
       forall b ofs f bi rs m rs' m',
@@ -1662,90 +360,11 @@ Inductive step: state -> trace -> state -> Prop :=
 
 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).
 
-(* Useless
-
-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.
-  + unfold exec_bblock in H4. destruct (exec_body _ _ _ _); try discriminate.
-    rewrite H9 in H4. discriminate.
-  + unfold exec_bblock in H13. destruct (exec_body _ _ _ _); try discriminate.
-    rewrite H4 in H13. discriminate.
-  + assert (vargs0 = vargs) by (eapply eval_builtin_args_determ; eauto). subst vargs0.
-    exploit external_call_determ. eexact H6. eexact H13. 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.
-*)
 
 Definition data_preg (r: preg) : bool :=
   match r with
@@ -1756,65 +375,3 @@ Definition data_preg (r: preg) : bool :=
   | PC     => false
   end.
 
-(** Determinacy of the [Asm] semantics. *)
-
-(* Useless.
-
-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.
-*)
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index 96547342..18aeafac 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -633,7 +633,7 @@ Fixpoint trans_body (b: list basic) : list L.inst :=
 
 Definition trans_pcincr (sz: Z) (k: L.inst) := (#PC, Op (Control (OIncremPC sz)) (PReg(#PC) @ Enil)) :: k.
 
-Definition trans_block (b: Asmblock.bblock) : L.bblock :=
+Definition trans_block (b: Asmvliw.bblock) : L.bblock :=
   trans_body (body b) ++ (trans_pcincr (size b) (trans_exit (exit b)) :: nil).
 
 Theorem trans_block_noheader_inv: forall bb, trans_block (no_header bb) = trans_block bb.
@@ -649,7 +649,7 @@ Qed.
 Definition state := L.mem.
 Definition exec := L.run.
 
-Definition match_states (s: Asmblock.state) (s': state) :=
+Definition match_states (s: Asmvliw.state) (s': state) :=
   let (rs, m) := s in
      s' pmem = Memstate m
   /\ forall r, s' (#r) = Val (rs r).
@@ -662,7 +662,7 @@ Definition match_outcome (o:outcome) (s: option state) :=
  
 Notation "a <[ b <- c ]>" := (assign a b c) (at level 102, right associativity).
 
-Definition trans_state (s: Asmblock.state) : state :=
+Definition trans_state (s: Asmvliw.state) : state :=
   let (rs, m) := s in
   fun x => if (Pos.eq_dec x pmem) then Memstate m
            else match (inv_ppos x) with
@@ -729,7 +729,7 @@ Lemma trans_arith_correct:
      inst_run (Genv ge fn) (trans_arith i) s s = Some s'
   /\ match_states (State rs' m) s'.
 Proof.
-  intros. unfold exec_arith_instr in H. destruct i.
+  intros. unfold exec_arith_instr in H. unfold parexec_arith_instr in H. destruct i.
 (* Ploadsymbol *)
   - inv H; inv H0. eexists; split; try split.
     * Simpl.
@@ -816,16 +816,16 @@ Theorem forward_simu_basic_gen ge fn b rs m s:
 Proof.
   intros. destruct b; inversion H; simpl.
 (* Arith *)
-  - eapply trans_arith_correct; eauto.
+  - eapply trans_arith_correct; eauto. destruct i; simpl; reflexivity.
 (* Load *)
   - destruct i.
   (* Load Offset *)
     + destruct i; simpl;
-      unfold exec_load_offset; rewrite (H1 ra); rewrite H0;
+      unfold parexec_load_offset; rewrite (H1 ra); rewrite H0;
       destruct (eval_offset _ _); simpl; auto; destruct (Mem.loadv _ _); simpl; auto;
       eexists; split; try split; Simpl; intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl.
     + destruct i; simpl;
-      unfold exec_load_reg; rewrite (H1 ra); rewrite (H1 rofs); rewrite H0; unfold exec_load_deps_reg;
+      unfold parexec_load_reg; rewrite (H1 ra); rewrite (H1 rofs); rewrite H0; unfold exec_load_deps_reg;
       destruct (Mem.loadv _ _); simpl; auto;
       eexists; split; try split; Simpl; intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl.
 
@@ -833,12 +833,12 @@ Proof.
   - destruct i.
   (* Store Offset *)
     + destruct i; simpl;
-      rewrite (H1 rs0); rewrite (H1 ra); rewrite H0; unfold exec_store_offset; destruct (eval_offset _ _); simpl; auto;
+      rewrite (H1 rs0); rewrite (H1 ra); rewrite H0; unfold parexec_store_offset; destruct (eval_offset _ _); simpl; auto;
       destruct (Mem.storev _ _ _ _); simpl; auto;
       eexists; split; try split; Simpl; intros rr; destruct rr; Simpl.
 
     + destruct i; simpl;
-      rewrite (H1 rs0); rewrite (H1 ra); rewrite (H1 rofs); rewrite H0; unfold exec_store_reg; unfold exec_store_deps_reg;
+      rewrite (H1 rs0); rewrite (H1 ra); rewrite (H1 rofs); rewrite H0; unfold parexec_store_reg; unfold exec_store_deps_reg;
       destruct (Mem.storev _ _ _ _); simpl; auto; eexists; split; try split; Simpl; intros rr; destruct rr; Simpl.
 
 (* Allocframe *)
@@ -910,43 +910,43 @@ Theorem forward_simu_control_gen ge fn ex b rs m s:
 Proof.
   intros. destruct ex; simpl; inv H0.
   - destruct c; destruct i; simpl; rewrite (H2 PC); auto.
-    all: try (eexists; split; try split; Simpl; intros rr; destruct rr; unfold nextblock; Simpl).
+    all: try (eexists; split; try split; Simpl; intros rr; destruct rr; unfold nextblock, incrPC; Simpl).
 
     (* Pjumptable *)
     + Simpl. rewrite (H2 r). destruct (rs r); simpl; auto. destruct (list_nth_z _ _); simpl; auto.
-      unfold goto_label; unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. Simpl.
+      unfold par_goto_label; unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. Simpl.
       destruct (Val.offset_ptr _ _); simpl; auto.
       eexists; split; try split; Simpl. intros rr; destruct rr; Simpl.
       destruct (preg_eq GPR62 g). rewrite e. Simpl.
       destruct (preg_eq GPR63 g). rewrite e. Simpl. Simpl.
 
     (* Pj_l *)
-    + Simpl. unfold goto_label; unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto.
-      unfold nextblock. Simpl. destruct (Val.offset_ptr _ _); simpl; auto.
+    + Simpl. unfold par_goto_label; unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto.
+      unfold nextblock, incrPC. Simpl. destruct (Val.offset_ptr _ _); simpl; auto.
       eexists; split; try split; Simpl. intros rr; destruct rr; Simpl.
 
     (* Pcb *)
-    + Simpl. destruct (cmp_for_btest _); simpl; auto. rewrite (H2 r). destruct o; simpl; auto. destruct i; unfold eval_branch; unfold eval_branch_deps.
+    + Simpl. destruct (cmp_for_btest _); simpl; auto. rewrite (H2 r). destruct o; simpl; auto. destruct i; unfold par_eval_branch; unfold eval_branch_deps.
       ++ destruct (Val.cmp_bool _ _ _); simpl; auto. destruct b0.
-         +++ unfold goto_label; unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. unfold nextblock; Simpl.
+         +++ unfold par_goto_label; unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. unfold nextblock, incrPC; Simpl.
              destruct (Val.offset_ptr _ _); simpl; auto.
              eexists; split; try split; Simpl. intros rr; destruct rr; Simpl.
          +++ simpl. eexists; split; try split; Simpl. intros rr; destruct rr; Simpl.
       ++ destruct (Val.cmpl_bool _ _ _); simpl; auto. destruct b0.
-         +++ unfold goto_label; unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. unfold nextblock; Simpl.
+         +++ unfold par_goto_label; unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. unfold nextblock, incrPC; Simpl.
              destruct (Val.offset_ptr _ _); simpl; auto.
              eexists; split; try split; Simpl. intros rr; destruct rr; Simpl.
          +++ simpl. eexists; split; try split; Simpl. intros rr; destruct rr; Simpl.
 
     (* Pcbu *)
-    + Simpl. destruct (cmpu_for_btest _); simpl; auto. rewrite (H2 r). destruct o; simpl; auto. destruct i; unfold eval_branch; unfold eval_branch_deps.
+    + Simpl. destruct (cmpu_for_btest _); simpl; auto. rewrite (H2 r). destruct o; simpl; auto. destruct i; unfold par_eval_branch; unfold eval_branch_deps.
       ++ destruct (Val_cmpu_bool _ _ _); simpl; auto. destruct b0.
-         +++ unfold goto_label; unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. unfold nextblock; Simpl.
+         +++ unfold par_goto_label; unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. unfold nextblock, incrPC; Simpl.
              destruct (Val.offset_ptr _ _); simpl; auto.
              eexists; split; try split; Simpl. intros rr; destruct rr; Simpl.
          +++ simpl. eexists; split; try split; Simpl. intros rr; destruct rr; Simpl.
       ++ destruct (Val_cmplu_bool _ _ _); simpl; auto. destruct b0.
-         +++ unfold goto_label; unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. unfold nextblock; Simpl.
+         +++ unfold par_goto_label; unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. unfold nextblock, incrPC; Simpl.
              destruct (Val.offset_ptr _ _); simpl; auto.
              eexists; split; try split; Simpl. intros rr; destruct rr; Simpl.
          +++ simpl. eexists; split; try split; Simpl. intros rr; destruct rr; Simpl.
@@ -1090,41 +1090,41 @@ Proof.
 (* Pjumptable *)
   - simpl in *. repeat (rewrite H3 in H1).
     destruct (rs r); try discriminate; auto. destruct (list_nth_z _ _); try discriminate; auto.
-    unfold goto_label_deps in H1. unfold goto_label. Simpl.
+    unfold goto_label_deps in H1. unfold par_goto_label. Simpl.
     destruct (label_pos _ _ _); auto. destruct (rs PC); auto. discriminate.
 (* Pj_l *)
   - simpl in *. pose (H3 PC); simpl in e; rewrite e in H1. clear e.
-    unfold goto_label_deps in H1. unfold goto_label.
+    unfold goto_label_deps in H1. unfold par_goto_label.
     destruct (label_pos _ _ _); auto. destruct (rs PC); auto. discriminate.
 (* Pcb *)
   - simpl in *. destruct (cmp_for_btest bt). destruct i.
     + pose (H3 PC); simpl in e; rewrite e in H1; clear e.
       destruct o; auto. pose (H3 r); simpl in e; rewrite e in H1; clear e.
-      unfold eval_branch_deps in H1; unfold eval_branch.
+      unfold eval_branch_deps in H1; unfold par_eval_branch.
       destruct (Val.cmp_bool _ _ _); auto. destruct b; try discriminate.
-      unfold goto_label_deps in H1; unfold goto_label. destruct (label_pos _ _ _); auto.
+      unfold goto_label_deps in H1; unfold par_goto_label. destruct (label_pos _ _ _); auto.
       destruct (rs PC); auto. discriminate.
     + pose (H3 PC); simpl in e; rewrite e in H1; clear e.
       destruct o; auto. pose (H3 r); simpl in e; rewrite e in H1; clear e.
-      unfold eval_branch_deps in H1; unfold eval_branch.
+      unfold eval_branch_deps in H1; unfold par_eval_branch.
       destruct (Val.cmpl_bool _ _ _); auto. destruct b; try discriminate.
-      unfold goto_label_deps in H1; unfold goto_label. destruct (label_pos _ _ _); auto.
+      unfold goto_label_deps in H1; unfold par_goto_label. destruct (label_pos _ _ _); auto.
       destruct (rs PC); auto. discriminate.
 (* Pcbu *)
   - simpl in *. destruct (cmpu_for_btest bt). destruct i.
     + pose (H3 PC); simpl in e; rewrite e in H1; clear e.
       destruct o; auto.
       pose (H3 r); simpl in e; rewrite e in H1; clear e.
-      unfold eval_branch_deps in H1; unfold eval_branch.
+      unfold eval_branch_deps in H1; unfold par_eval_branch.
       destruct (Val_cmpu_bool _ _ _); auto. destruct b; try discriminate.
-      unfold goto_label_deps in H1; unfold goto_label. destruct (label_pos _ _ _); auto.
+      unfold goto_label_deps in H1; unfold par_goto_label. destruct (label_pos _ _ _); auto.
       destruct (rs PC); auto. discriminate.
     + pose (H3 PC); simpl in e; rewrite e in H1; clear e.
       destruct o; auto.
       pose (H3 r); simpl in e; rewrite e in H1; clear e.
-      unfold eval_branch_deps in H1; unfold eval_branch.
+      unfold eval_branch_deps in H1; unfold par_eval_branch.
       destruct (Val_cmplu_bool _ _); auto. destruct b; try discriminate.
-      unfold goto_label_deps in H1; unfold goto_label. destruct (label_pos _ _ _); auto.
+      unfold goto_label_deps in H1; unfold par_goto_label. destruct (label_pos _ _ _); auto.
       destruct (rs PC); auto. discriminate.
 Qed.
 
@@ -1173,37 +1173,37 @@ Proof.
   destruct ctl; destruct i; try discriminate; try (simpl; reflexivity).
   (* Pjumptable *)
   - simpl in *. repeat (rewrite H3). destruct (rs r); try discriminate; auto. destruct (list_nth_z _ _); try discriminate; auto.
-    unfold goto_label_deps. unfold goto_label in H0.
+    unfold goto_label_deps. unfold par_goto_label in H0.
     destruct (label_pos _ _ _); auto. repeat (rewrite Pregmap.gso in H0; try discriminate). destruct (rs PC); auto. discriminate.
 (* Pj_l *)
-  - simpl in *. pose (H3 PC); simpl in e; rewrite e. unfold goto_label_deps. unfold goto_label in H0.
+  - simpl in *. pose (H3 PC); simpl in e; rewrite e. unfold goto_label_deps. unfold par_goto_label in H0.
     destruct (label_pos _ _ _); auto. clear e. destruct (rs PC); auto. discriminate.
 (* Pcb *)
   - simpl in *. destruct (cmp_for_btest bt). destruct i.
     -- destruct o.
-      + unfold eval_branch in H0; unfold eval_branch_deps.
+      + unfold par_eval_branch in H0; unfold eval_branch_deps.
         pose (H3 r); simpl in e; rewrite e. pose (H3 PC); simpl in e0; rewrite e0. destruct (Val.cmp_bool _ _ _); auto.
-        destruct b; try discriminate. unfold goto_label_deps; unfold goto_label in H0. clear e0.
+        destruct b; try discriminate. unfold goto_label_deps; unfold par_goto_label in H0. clear e0.
         destruct (label_pos _ _ _); auto. destruct (rs PC); auto. discriminate.
       + pose (H3 r); simpl in e; rewrite e. pose (H3 PC); simpl in e0; rewrite e0. reflexivity.
     -- destruct o.
-      + unfold eval_branch in H0; unfold eval_branch_deps.
+      + unfold par_eval_branch in H0; unfold eval_branch_deps.
         pose (H3 r); simpl in e; rewrite e. pose (H3 PC); simpl in e0; rewrite e0. destruct (Val.cmpl_bool _ _ _); auto.
-        destruct b; try discriminate. unfold goto_label_deps; unfold goto_label in H0. clear e0.
+        destruct b; try discriminate. unfold goto_label_deps; unfold par_goto_label in H0. clear e0.
         destruct (label_pos _ _ _); auto. destruct (rs PC); auto. discriminate.
       + pose (H3 r); simpl in e; rewrite e. pose (H3 PC); simpl in e0; rewrite e0. reflexivity.
 (* Pcbu *)
   - simpl in *. destruct (cmpu_for_btest bt). destruct i.
     -- destruct o.
-      + unfold eval_branch in H0; unfold eval_branch_deps.
+      + unfold par_eval_branch in H0; unfold eval_branch_deps.
         pose (H3 r); simpl in e; rewrite e. pose (H3 PC); simpl in e0; rewrite e0. destruct (Val_cmpu_bool _ _); auto.
-        destruct b; try discriminate. unfold goto_label_deps; unfold goto_label in H0. clear e0.
+        destruct b; try discriminate. unfold goto_label_deps; unfold par_goto_label in H0. clear e0.
         destruct (label_pos _ _ _); auto. destruct (rs PC); auto. discriminate.
       + pose (H3 r); simpl in e; rewrite e. pose (H3 PC); simpl in e0; rewrite e0. reflexivity.
     -- destruct o.
-      + unfold eval_branch in H0; unfold eval_branch_deps.
+      + unfold par_eval_branch in H0; unfold eval_branch_deps.
         pose (H3 r); simpl in e; rewrite e. pose (H3 PC); simpl in e0; rewrite e0. destruct (Val_cmplu_bool _ _); auto.
-        destruct b; try discriminate. unfold goto_label_deps; unfold goto_label in H0. clear e0.
+        destruct b; try discriminate. unfold goto_label_deps; unfold par_goto_label in H0. clear e0.
         destruct (label_pos _ _ _); auto. destruct (rs PC); auto. discriminate.
       + pose (H3 r); simpl in e; rewrite e. pose (H3 PC); simpl in e0; rewrite e0. reflexivity.
 Qed.
@@ -1539,7 +1539,7 @@ Definition string_of_op (op: P.op): ?? pstring :=
   | Fail => RET (Str "Fail")
   end.
 
-Definition bblock_eq_test (verb: bool) (p1 p2: Asmblock.bblock) : ?? bool :=
+Definition bblock_eq_test (verb: bool) (p1 p2: Asmvliw.bblock) : ?? bool :=
   if verb then
     IDT.verb_bblock_eq_test string_of_name string_of_op (trans_block p1) (trans_block p2)
   else
@@ -1558,7 +1558,7 @@ Hint Resolve bblock_eq_test_correct: wlp.
 
 Import UnsafeImpure.
 
-Definition pure_bblock_eq_test (verb: bool) (p1 p2: Asmblock.bblock): bool := unsafe_coerce (bblock_eq_test verb p1 p2).
+Definition pure_bblock_eq_test (verb: bool) (p1 p2: Asmvliw.bblock): bool := unsafe_coerce (bblock_eq_test verb p1 p2).
 
 Theorem pure_bblock_eq_test_correct verb p1 p2:
   forall ge fn, Ge = Genv ge fn ->
@@ -1568,7 +1568,7 @@ Proof.
    apply unsafe_coerce_not_really_correct; eauto.
 Qed.
 
-Definition bblock_equivb: Asmblock.bblock -> Asmblock.bblock -> bool := pure_bblock_eq_test true.
+Definition bblock_equivb: Asmvliw.bblock -> Asmvliw.bblock -> bool := pure_bblock_eq_test true.
 
 Definition bblock_equiv_eq := pure_bblock_eq_test_correct true.
 
@@ -1578,7 +1578,7 @@ End SECT.
 
 Module PChk := ParallelChecks L PosPseudoRegSet.
 
-Definition bblock_para_check (p: Asmblock.bblock) : bool :=
+Definition bblock_para_check (p: Asmvliw.bblock) : bool :=
   PChk.is_parallelizable (trans_block p).
 
 Require Import Asmvliw Permutation.
@@ -1815,31 +1815,31 @@ Theorem forward_simu_par_control_gen ge fn rsr rsw mr mw sr sw sz ex:
   Ge = Genv ge fn ->
   match_states (State rsr mr) sr ->
   match_states (State rsw mw) sw ->
-  match_outcome (parexec_control ge fn ex (par_nextblock (Ptrofs.repr sz) rsr) rsw mw) (inst_prun Ge (trans_pcincr sz (trans_exit ex)) sw sr sr).
+  match_outcome (parexec_control ge fn ex (incrPC (Ptrofs.repr sz) rsr) rsw mw) (inst_prun Ge (trans_pcincr sz (trans_exit ex)) sw sr sr).
 Proof.
   intros GENV MSR MSW.
   simpl in *. inv MSR. inv MSW.
   destruct ex.
   - destruct c; destruct i; try discriminate; simpl.
-    all: try (rewrite (H0 PC); eexists; split; try split; Simpl; intros rr; destruct rr; unfold par_nextblock; Simpl).
+    all: try (rewrite (H0 PC); eexists; split; try split; Simpl; intros rr; destruct rr; unfold incrPC; Simpl).
 
     (* Pjumptable *)
-    + rewrite (H0 PC). Simpl. rewrite (H0 r). unfold par_nextblock. Simpl.
+    + rewrite (H0 PC). Simpl. rewrite (H0 r). unfold incrPC. Simpl.
       destruct (rsr r); simpl; auto. destruct (list_nth_z _ _); simpl; auto.
       unfold par_goto_label. unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. Simpl.
       destruct (Val.offset_ptr _ _); simpl; auto.
-      eexists; split; try split; Simpl. intros rr; destruct rr; unfold par_nextblock; Simpl.
+      eexists; split; try split; Simpl. intros rr; destruct rr; unfold incrPC; Simpl.
       destruct (preg_eq g GPR62). rewrite e. Simpl.
       destruct (preg_eq g GPR63). rewrite e. Simpl. Simpl.
 
     (* Pj_l *)
     + rewrite (H0 PC). Simpl. unfold par_goto_label. unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto.
-      unfold par_nextblock. Simpl. destruct (Val.offset_ptr _ _); simpl; auto.
-      eexists; split; try split; Simpl. intros rr; destruct rr; unfold par_nextblock; Simpl.
+      unfold incrPC. Simpl. destruct (Val.offset_ptr _ _); simpl; auto.
+      eexists; split; try split; Simpl. intros rr; destruct rr; unfold incrPC; Simpl.
 
     (* Pcb *)
     + rewrite (H0 PC). Simpl. rewrite (H0 r). destruct (cmp_for_btest _); simpl; auto. destruct o; simpl; auto.
-      unfold par_eval_branch. unfold eval_branch_deps. unfold par_nextblock. Simpl. destruct i.
+      unfold par_eval_branch. unfold eval_branch_deps. unfold incrPC. Simpl. destruct i.
       ++ destruct (Val.cmp_bool _ _ _); simpl; auto. destruct b.
          +++ unfold par_goto_label. unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. Simpl.
              destruct (Val.offset_ptr _ _); simpl; auto. eexists; split; try split; Simpl.
@@ -1853,7 +1853,7 @@ Proof.
 
     (* Pcbu *)
     + rewrite (H0 PC). Simpl. rewrite (H0 r). destruct (cmpu_for_btest _); simpl; auto. destruct o; simpl; auto.
-      unfold par_eval_branch. unfold eval_branch_deps. unfold par_nextblock. Simpl. destruct i.
+      unfold par_eval_branch. unfold eval_branch_deps. unfold incrPC. Simpl. destruct i.
       ++ destruct (Val_cmpu_bool _ _ _); simpl; auto. destruct b.
          +++ unfold par_goto_label. unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. Simpl.
              destruct (Val.offset_ptr _ _); simpl; auto. eexists; split; try split; Simpl.
@@ -1866,14 +1866,14 @@ Proof.
          +++ repeat (econstructor; eauto). intros rr; destruct rr; Simpl.
 
   - simpl in *. rewrite (H0 PC). eexists; split; try split; Simpl.
-    intros rr; destruct rr; unfold par_nextblock; Simpl.
+    intros rr; destruct rr; unfold incrPC; Simpl.
 Qed.
 
 Theorem forward_simu_par_control ge fn rsr rsw mr mw sr sw sz rs' ex m':
   Ge = Genv ge fn ->
   match_states (State rsr mr) sr ->
   match_states (State rsw mw) sw ->
-  parexec_control ge fn ex (par_nextblock (Ptrofs.repr sz) rsr) rsw mw = Next rs' m' ->
+  parexec_control ge fn ex (incrPC (Ptrofs.repr sz) rsr) rsw mw = Next rs' m' ->
   exists s',
      inst_prun Ge (trans_pcincr sz (trans_exit ex)) sw sr sr = Some s'
   /\ match_states (State rs' m') s'.
@@ -1887,7 +1887,7 @@ Lemma forward_simu_par_control_Stuck ge fn rsr rsw mr mw sr sw sz ex:
   Ge = Genv ge fn ->
   match_states (State rsr mr) sr ->
   match_states (State rsw mw) sw ->
-  parexec_control ge fn ex (par_nextblock (Ptrofs.repr sz) rsr) rsw mw = Stuck ->
+  parexec_control ge fn ex (incrPC (Ptrofs.repr sz) rsr) rsw mw = Stuck ->
   inst_prun Ge (trans_pcincr sz (trans_exit ex)) sw sr sr = None.
 Proof.
   intros. exploit forward_simu_par_control_gen. 3: eapply H1. 2: eapply H0. all: eauto. 
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index 392b7953..bf466c4e 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -1067,14 +1067,14 @@ Definition transl_function (f: Machblock.function) :=
          Pget GPRA RA ::b
          storeind_ptr GPRA SP f.(fn_retaddr_ofs) ::b lb)).
 
-Definition transf_function (f: Machblock.function) : res Asmblock.function :=
+Definition transf_function (f: Machblock.function) : res Asmvliw.function :=
   do tf <- transl_function f;
   if zlt Ptrofs.max_unsigned (size_blocks tf.(fn_blocks))
   then Error (msg "code size exceeded")
   else OK tf.
 
-Definition transf_fundef (f: Machblock.fundef) : res Asmblock.fundef :=
+Definition transf_fundef (f: Machblock.fundef) : res Asmvliw.fundef :=
   transf_partial_fundef transf_function f.
 
-Definition transf_program (p: Machblock.program) : res Asmblock.program :=
+Definition transf_program (p: Machblock.program) : res Asmvliw.program :=
   transform_partial_program transf_fundef p.
diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v
index 70f188ec..e3be258a 100644
--- a/mppa_k1c/Asmblockgenproof.v
+++ b/mppa_k1c/Asmblockgenproof.v
@@ -19,9 +19,9 @@ Require Import Op Locations Machblock Conventions Asmblock.
 Require Import Asmblockgen Asmblockgenproof0 Asmblockgenproof1.

 

 Module MB := Machblock.

-Module AB := Asmblock.

+Module AB := Asmvliw.

 

-Definition match_prog (p: Machblock.program) (tp: Asmblock.program) :=

+Definition match_prog (p: Machblock.program) (tp: Asmvliw.program) :=

   match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp.

 

 Lemma transf_program_match:

@@ -33,7 +33,7 @@ Qed.
 Section PRESERVATION.

 

 Variable prog: Machblock.program.

-Variable tprog: Asmblock.program.

+Variable tprog: Asmvliw.program.

 Hypothesis TRANSF: match_prog prog tprog.

 Let ge := Genv.globalenv prog.

 Let tge := Genv.globalenv tprog.

@@ -259,7 +259,7 @@ Proof.
   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. unfold goto_label. unfold par_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.

@@ -318,7 +318,7 @@ Proof.
   exploit preg_of_injective; eauto. intros; subst r; discriminate.

 Qed.

 

-Inductive match_states: Machblock.state -> Asmblock.state -> Prop :=

+Inductive match_states: Machblock.state -> Asmvliw.state -> Prop :=

   | match_states_intro:

       forall s fb sp c ep ms m m' rs f tf tc

         (STACKS: match_stack ge s)

@@ -328,7 +328,7 @@ Inductive match_states: Machblock.state -> Asmblock.state -> Prop :=
         (AG: agree ms sp rs)

         (DXP: ep = true -> rs#FP = parent_sp s),

       match_states (Machblock.State s fb sp c ms m)

-                   (Asmblock.State rs m')

+                   (Asmvliw.State rs m')

   | match_states_call:

       forall s fb ms m m' rs

         (STACKS: match_stack ge s)

@@ -337,7 +337,7 @@ Inductive match_states: Machblock.state -> Asmblock.state -> Prop :=
         (ATPC: rs PC = Vptr fb Ptrofs.zero)

         (ATLR: rs RA = parent_ra s),

       match_states (Machblock.Callstate s fb ms m)

-                   (Asmblock.State rs m')

+                   (Asmvliw.State rs m')

   | match_states_return:

       forall s ms m m' rs

         (STACKS: match_stack ge s)

@@ -345,7 +345,7 @@ Inductive match_states: Machblock.state -> Asmblock.state -> Prop :=
         (AG: agree ms (parent_sp s) rs)

         (ATPC: rs PC = parent_ra s),

       match_states (Machblock.Returnstate s ms m)

-                   (Asmblock.State rs m').

+                   (Asmvliw.State rs m').

 

 Record codestate :=

   Codestate {     pstate: state;

@@ -373,7 +373,7 @@ Inductive match_codestate fb: Machblock.state -> codestate -> Prop :=
         (DXP: (if MB.header bb then ep else false) = true -> rs0#FP = parent_sp s)

         ,

       match_codestate fb (Machblock.State s fb sp (bb::c) ms m)

-        {|  pstate := (Asmblock.State rs0 m0);

+        {|  pstate := (Asmvliw.State rs0 m0);

             pheader := (MB.header bb);

             pbody1 := tbc;

             pbody2 := (extract_basic tbi);

@@ -384,7 +384,7 @@ Inductive match_codestate fb: Machblock.state -> codestate -> Prop :=
         |}

 .

 

-Inductive match_asmstate fb: codestate -> Asmblock.state -> Prop :=

+Inductive match_asmstate fb: codestate -> Asmvliw.state -> Prop :=

   | match_asmstate_some:

       forall rs f tf tc m tbb ofs ep tbdy tex lhd

         (FIND: Genv.find_funct_ptr ge fb = Some (Internal f))

@@ -394,7 +394,7 @@ Inductive match_asmstate fb: codestate -> Asmblock.state -> Prop :=
 (*         (HDROK: header tbb = lhd) *)

         ,

       match_asmstate fb 

-        {|  pstate := (Asmblock.State rs m);

+        {|  pstate := (Asmvliw.State rs m);

             pheader := lhd;

             pbody1 := tbdy;

             pbody2 := extract_basic tex;

@@ -402,7 +402,7 @@ Inductive match_asmstate fb: codestate -> Asmblock.state -> Prop :=
             fpok := ep;

             rem := tc;

             cur := Some tbb |}

-        (Asmblock.State rs m)

+        (Asmvliw.State rs m)

 .

 

 Ltac exploreInst :=

@@ -716,11 +716,11 @@ Theorem step_simu_control:
   MB.body bb' = nil ->

   (forall ef args res, MB.exit bb' <> Some (MBbuiltin ef args res)) ->

   Genv.find_funct_ptr tge fb = Some (Internal fn) ->

-  pstate cs2 = (Asmblock.State rs2 m2) ->

+  pstate cs2 = (Asmvliw.State rs2 m2) ->

   pbody1 cs2 = nil -> pbody2 cs2 = tbdy2 -> pctl cs2 = tex ->

   cur cs2 = Some tbb ->

   match_codestate fb (MB.State s fb sp (bb'::c) ms' m') cs2 ->

-  match_asmstate fb cs2 (Asmblock.State rs1 m1) ->

+  match_asmstate fb cs2 (Asmvliw.State rs1 m1) ->

   exit_step return_address_offset ge (MB.exit bb') (MB.State s fb sp (bb'::c) ms' m') E0 S'' ->

   (exists rs3 m3 rs4 m4,

       exec_body tge tbdy2 rs2 m2 = Next rs3 m3

@@ -839,7 +839,7 @@ Proof.
       exploit find_label_goto_label.

         eauto. eauto.

         instantiate (2 := rs2').

-        { subst. unfold nextblock. Simpl. unfold Val.offset_ptr. rewrite PCeq. eauto. }

+        { subst. unfold nextblock, incrPC. Simpl. unfold Val.offset_ptr. rewrite PCeq. eauto. }

         eauto.

       intros (tc' & rs' & GOTO & AT2 & INV).

 

@@ -847,7 +847,7 @@ Proof.
         rewrite H6. simpl extract_basic. simpl. eauto.

         rewrite H7. simpl extract_ctl. simpl. rewrite <- Heqrs2'. eauto.

       econstructor; eauto.

-        rewrite Heqrs2' in INV. unfold nextblock in INV.

+        rewrite Heqrs2' in INV. unfold nextblock, incrPC in INV.

         eapply agree_exten; eauto with asmgen.

         assert (forall r : preg, r <> PC -> rs' r = rs2 r).

         { intros. destruct r.

@@ -886,7 +886,7 @@ Proof.
         econstructor; eauto.

           eapply agree_exten with rs2; eauto with asmgen.

           { intros. destruct r; try destruct g; try discriminate.

-            all: rewrite Hrs3; try discriminate; unfold nextblock; Simpl. }

+            all: rewrite Hrs3; try discriminate; unfold nextblock, incrPC; Simpl. }

         intros. discriminate.

 

       * (* MBcond false *)

@@ -912,10 +912,10 @@ Proof.
           rewrite H7. rewrite <- BTC. rewrite extract_ctl_basics_to_code. simpl extract_ctl. rewrite B. eauto.

 

         econstructor; eauto.

-          unfold nextblock. Simpl. unfold Val.offset_ptr. rewrite PCeq. econstructor; eauto.

+          unfold nextblock, incrPC. Simpl. unfold Val.offset_ptr. rewrite PCeq. econstructor; eauto.

           eapply agree_exten with rs2; eauto with asmgen.

           { intros. destruct r; try destruct g; try discriminate.

-            all: rewrite <- C; try discriminate; unfold nextblock; Simpl. }

+            all: rewrite <- C; try discriminate; unfold nextblock, incrPC; Simpl. }

         intros. discriminate.

     + (* MBjumptable *)

       destruct bb' as [mhd' mbdy' mex']; simpl in *. subst.

@@ -926,7 +926,7 @@ Proof.
       generalize (transf_function_no_overflow _ _ TRANSF0); intro NOOV.

       assert (f1 = f) by congruence. subst f1.

       exploit find_label_goto_label. 4: eapply H16. 1-2: eauto. instantiate (2 := (nextblock tbb rs2) # GPR62 <- Vundef # GPR63 <- Vundef).

-        unfold nextblock. Simpl. unfold Val.offset_ptr. rewrite PCeq. reflexivity.

+        unfold nextblock, incrPC. Simpl. unfold Val.offset_ptr. rewrite PCeq. reflexivity.

       exploit functions_transl. eapply FIND0. eapply TRANSF0. intros FIND3. assert (fn = tf) by congruence. subst fn.

 

       intros [tc' [rs' [A [B C]]]].

@@ -959,7 +959,7 @@ Proof.
         rewrite H6. simpl extract_basic. eauto.

         rewrite H7. simpl extract_ctl. simpl. reflexivity.

       econstructor; eauto.

-        unfold nextblock. repeat apply agree_set_other; auto with asmgen.

+        unfold nextblock, incrPC. repeat apply agree_set_other; auto with asmgen.

 

   - inv MCS. inv MAS. simpl in *. subst. inv Hpstate. inv Hcur.

 (*     exploit transl_blocks_distrib; eauto. (* rewrite <- H2. discriminate. *)

@@ -969,7 +969,7 @@ Proof.
     monadInv TBC. monadInv TIC. simpl in *. rewrite H5. rewrite H6.

     simpl. repeat eexists.

     econstructor. 4: instantiate (3 := false). all:eauto.

-      unfold nextblock. Simpl. unfold Val.offset_ptr. rewrite PCeq.

+      unfold nextblock, incrPC. Simpl. unfold Val.offset_ptr. rewrite PCeq.

       assert (NOOV: size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned).

         eapply transf_function_no_overflow; eauto.

       assert (f = f0) by congruence. subst f0. econstructor; eauto.

@@ -1398,7 +1398,7 @@ Proof.
     eapply exec_step_internal; eauto. eapply find_bblock_tail; eauto.

     unfold exec_bblock. simpl. eauto.

     econstructor. eauto. eauto. eauto.

-    unfold nextblock. Simpl. unfold Val.offset_ptr. rewrite <- H.

+    unfold nextblock, incrPC. Simpl. unfold Val.offset_ptr. rewrite <- H.

     assert (NOOV: size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned).

       eapply transf_function_no_overflow; eauto.

     econstructor; eauto.

@@ -1581,7 +1581,7 @@ Proof.
     eauto.

   econstructor; eauto.

     instantiate (2 := tf); instantiate (1 := x0).

-    unfold nextblock. rewrite Pregmap.gss.

+    unfold nextblock, incrPC. rewrite Pregmap.gss.

     rewrite set_res_other. rewrite undef_regs_other_2. rewrite Pregmap.gso by congruence. 

     rewrite <- H. simpl. econstructor; eauto.

     eapply code_tail_next_int; eauto.

@@ -1680,7 +1680,7 @@ Proof.
   { change (fn_blocks tf) with tfbody; unfold tfbody.

     apply exec_straight_blocks_step with rs2 m2'.

     unfold exec_bblock. simpl exec_body. rewrite C. fold sp. simpl exec_control.

-    rewrite <- (sp_val _ _ _ AG). rewrite chunk_of_Tptr in F. simpl in F. rewrite F. reflexivity.

+    rewrite <- (sp_val _ _ _ AG). rewrite chunk_of_Tptr in F. simpl in F. rewrite F. rewrite regset_same_assign. reflexivity.

     reflexivity.

     eapply exec_straight_blocks_trans.

     - eexact W'.

@@ -1775,7 +1775,7 @@ Definition return_address_offset : Machblock.function -> Machblock.code -> ptrof
   Asmblockgenproof0.return_address_offset.

 

 Theorem transf_program_correct:

-  forward_simulation (MB.semantics return_address_offset prog) (AB.semantics tprog).

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

 Proof.

   eapply forward_simulation_star with (measure := measure).

   - apply senv_preserved.

diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v
index 6cf5c60c..bbcffbe2 100644
--- a/mppa_k1c/Asmblockgenproof1.v
+++ b/mppa_k1c/Asmblockgenproof1.v
@@ -745,7 +745,7 @@ Proof.
     * constructor.
     * split; auto. simpl. intros.
       assert (rs r1 = (nextblock tbb rs) r1).
-        unfold nextblock. Simpl. rewrite H1 in H0.
+        unfold nextblock, incrPC. Simpl. rewrite H1 in H0.
       (*assert (Val.cmp_bool Ceq (rs r1) (Vint (Int.repr 0)) = Some b) as EVAL'S.
       { rewrite <- H2. rewrite <- H0. rewrite <- H1. auto. }*)
       auto;
@@ -772,7 +772,7 @@ Proof.
     * constructor.
     * split; auto. simpl. intros.
       assert (rs r1 = (nextblock tbb rs) r1).
-        unfold nextblock. Simpl. rewrite H1 in H0.
+        unfold nextblock, incrPC. Simpl. rewrite H1 in H0.
       auto;
       unfold eval_branch. rewrite H0. auto.
   - (* c = Clt *) contradict H; unfold select_comp; destruct (Int.eq n Int.zero);
@@ -821,7 +821,7 @@ Proof.
     * constructor.
     * split; auto. simpl. intros.
       assert (rs r1 = (nextblock tbb rs) r1).
-        unfold nextblock. Simpl. rewrite H1 in H0.
+        unfold nextblock, incrPC. Simpl. rewrite H1 in H0.
       auto;
       unfold eval_branch. rewrite H0; auto.
   - (* c = Cne *)
@@ -846,7 +846,7 @@ Proof.
     * constructor.
     * split; auto. simpl. intros.
       assert (rs r1 = (nextblock tbb rs) r1).
-        unfold nextblock. Simpl. rewrite H1 in H0.
+        unfold nextblock, incrPC. Simpl. rewrite H1 in H0.
       auto;
       unfold eval_branch. rewrite H0; auto.
   - (* c = Clt *) contradict H; unfold select_compl; destruct (Int64.eq n Int64.zero);
@@ -903,7 +903,7 @@ Proof.
     * constructor.
     * split; auto.
       assert (rs x = (nextblock tbb rs) x).
-        unfold nextblock. Simpl. rewrite H0 in EVAL'. clear H0.
+        unfold nextblock, incrPC. Simpl. rewrite H0 in EVAL'. clear H0.
       destruct c0; simpl; auto;
       unfold eval_branch; rewrite <- H; rewrite EVAL'; auto.
   + exploit (loadimm32_correct RTMP n); eauto. intros (rs' & A & B & C).
@@ -966,7 +966,7 @@ Proof.
     * constructor.
     * split; auto.
       assert (rs x = (nextblock tbb rs) x).
-        unfold nextblock. Simpl. rewrite H0 in EVAL'. clear H0.
+        unfold nextblock, incrPC. Simpl. rewrite H0 in EVAL'. clear H0.
       destruct c0; simpl; auto;
       unfold eval_branch; rewrite <- H; rewrite EVAL'; auto.
   + exploit (loadimm64_correct RTMP n); eauto. intros (rs' & A & B & C).
@@ -1060,13 +1060,10 @@ Lemma transl_cbranch_correct_false:
   /\ exec_control ge fn (Some insn) (nextblock tbb rs') m' = Next (nextblock tbb rs') m'
   /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r.
 Proof.
-  intros. exploit transl_cbranch_correct_1; eauto.
+  intros. exploit transl_cbranch_correct_1. all: eauto. simpl eval_branch. instantiate (1 := tbb).
+  intros (rs' & insn & A & B & C). rewrite regset_same_assign in B.
+  eexists; eexists. split; try split. all: eassumption.
 Qed.
-(*   intros (rs' & insn & A & B & C).
-  exists rs'.
-  split. eapply exec_straight_opt_right; eauto. apply exec_straight_one; auto.
-  intros; Simpl. 
- *)
 
 (** Translation of condition operators *)
 
@@ -1950,7 +1947,7 @@ Proof.
   intros (base' & ofs' & rs' & ptr' & A & PtrEq & B & C).
   econstructor; split.
   eapply exec_straight_opt_right. eexact A. apply exec_straight_one. rewrite EXEC.
-  unfold exec_load_offset. rewrite PtrEq. rewrite B, LOAD. eauto. Simpl. 
+  unfold exec_load_offset. unfold parexec_load_offset. rewrite PtrEq. rewrite B, LOAD. eauto. Simpl. 
   split; intros; Simpl. auto.
 Qed.
 
@@ -1970,7 +1967,7 @@ Proof.
   intros (base' & ofs' & rs' & ptr' & A & PtrEq & B & C).
   econstructor; split.
   eapply exec_straight_opt_right. eapply A. apply exec_straight_one. rewrite EXEC.
-  unfold exec_store_offset. rewrite PtrEq. rewrite B, C, STORE.
+  unfold exec_store_offset. unfold parexec_store_offset. rewrite PtrEq. rewrite B, C, STORE.
     eauto.
     discriminate.
     { intro. inv H. contradiction. }
@@ -2149,7 +2146,7 @@ Proof.
   intros (base & ro2 & mro2 & mr2 & rs' & ARGSS & IREGEQ & A & B & C). rewrite ARGSS in ARGS. inversion ARGS. subst mr2 mro2. clear ARGS.
   econstructor; split.
   eapply exec_straight_opt_right. eexact A. apply exec_straight_one. assert (ro = ro2) by congruence. subst ro2.
-  rewrite INSTR. unfold exec_load_reg. rewrite B, LOAD. reflexivity. Simpl. 
+  rewrite INSTR. unfold exec_load_reg. unfold parexec_load_reg. rewrite B, LOAD. reflexivity. Simpl. 
   split; intros; Simpl. auto.
 Qed.
 
@@ -2170,7 +2167,7 @@ Proof.
   intros (base & ofs & rs' & ptr & A & PtrEq & B & C).
   econstructor; split.
   eapply exec_straight_opt_right. eexact A. apply exec_straight_one. 
-  rewrite INSTR. unfold exec_load_offset. rewrite PtrEq, B, LOAD. reflexivity. Simpl. 
+  rewrite INSTR. unfold exec_load_offset. unfold parexec_load_offset. rewrite PtrEq, B, LOAD. reflexivity. Simpl. 
   split; intros; Simpl. auto.
 Qed.
 
@@ -2256,7 +2253,7 @@ Proof.
   intros (base & ro2 & mr2 & mro2 & rs' & ARGSS & IREGG & A & B & C). rewrite ARGSS in ARGS. inversion ARGS. subst mro2 mr2. clear ARGS.
   econstructor; split.
   eapply exec_straight_opt_right. eexact A. apply exec_straight_one. assert (ro = ro2) by congruence. subst ro2.
-  rewrite INSTR. unfold exec_store_reg. rewrite B. rewrite C; try discriminate. rewrite STORE. auto.
+  rewrite INSTR. unfold exec_store_reg. unfold parexec_store_reg. rewrite B. rewrite C; try discriminate. rewrite STORE. auto.
   intro. inv H. contradiction.
   auto.
 Qed.
@@ -2278,7 +2275,7 @@ Proof.
   intros (base & ofs & rs' & ptr & A & PtrEq & B & C).
   econstructor; split.
   eapply exec_straight_opt_right. eexact A. apply exec_straight_one. 
-  rewrite INSTR. unfold exec_store_offset. rewrite PtrEq, B. rewrite C; try discriminate. rewrite STORE. auto.
+  rewrite INSTR. unfold exec_store_offset. unfold parexec_store_offset. rewrite PtrEq, B. rewrite C; try discriminate. rewrite STORE. auto.
   intro. inv H. contradiction.
   auto.
 Qed.
@@ -2287,14 +2284,14 @@ Qed.
 Remark exec_store_offset_8_sign rs m x base ofs:
   exec_store_offset ge Mint8unsigned rs m x base ofs = exec_store_offset ge Mint8signed rs m x base ofs.
 Proof.
-  unfold exec_store_offset. destruct (eval_offset _ _); auto. unfold Mem.storev.
+  unfold exec_store_offset. unfold parexec_store_offset. destruct (eval_offset _ _); auto. unfold Mem.storev.
   destruct (Val.offset_ptr _ _); auto. erewrite <- Mem.store_signed_unsigned_8. reflexivity.
 Qed.
 
 Remark exec_store_offset_16_sign rs m x base ofs:
   exec_store_offset ge Mint16unsigned rs m x base ofs = exec_store_offset ge Mint16signed rs m x base ofs.
 Proof.
-  unfold exec_store_offset. destruct (eval_offset _ _); auto. unfold Mem.storev.
+  unfold exec_store_offset. unfold parexec_store_offset. destruct (eval_offset _ _); auto. unfold Mem.storev.
   destruct (Val.offset_ptr _ _); auto. erewrite <- Mem.store_signed_unsigned_16. reflexivity.
 Qed.
 
@@ -2336,14 +2333,14 @@ Qed.
 Remark exec_store_reg_8_sign rs m x base ofs:
   exec_store_reg Mint8unsigned rs m x base ofs = exec_store_reg Mint8signed rs m x base ofs.
 Proof.
-  unfold exec_store_reg. unfold Mem.storev. destruct (Val.addl _ _); auto.
+  unfold exec_store_reg. unfold parexec_store_reg. unfold Mem.storev. destruct (Val.addl _ _); auto.
   erewrite <- Mem.store_signed_unsigned_8. reflexivity.
 Qed.
 
 Remark exec_store_reg_16_sign rs m x base ofs:
   exec_store_reg Mint16unsigned rs m x base ofs = exec_store_reg Mint16signed rs m x base ofs.
 Proof.
-  unfold exec_store_reg. unfold Mem.storev. destruct (Val.addl _ _); auto.
+  unfold exec_store_reg. unfold parexec_store_reg. unfold Mem.storev. destruct (Val.addl _ _); auto.
   erewrite <- Mem.store_signed_unsigned_16. reflexivity.
 Qed.
 
diff --git a/mppa_k1c/Asmexpand.ml b/mppa_k1c/Asmexpand.ml
index a9f17f33..6310b8ae 100644
--- a/mppa_k1c/Asmexpand.ml
+++ b/mppa_k1c/Asmexpand.ml
@@ -41,7 +41,7 @@ let wordsize = if Archi.ptr64 then 8 else 4
 
 let align n a = (n + a - 1) land (-a)
 
-let stack_pointer = Asmblock.GPR12
+let stack_pointer = Asmvliw.GPR12
                   
 (* Emit instruction sequences that set or offset a register by a constant. *)
 (*
@@ -49,7 +49,7 @@ let stack_pointer = Asmblock.GPR12
   List.iter emit (Asmgen.loadimm32 dst n [])
 *)
 let expand_addptrofs dst src n =
-  List.iter emit (basic_to_instruction (Asmblock.PArith (Asmblockgen.addptrofs dst src n)) :: [])
+  List.iter emit (basic_to_instruction (Asmvliw.PArith (Asmblockgen.addptrofs dst src n)) :: [])
 let expand_storeind_ptr src base ofs =
   List.iter emit (basic_to_instruction (Asmblockgen.storeind_ptr src base ofs) :: [])
 let expand_loadind_ptr dst base ofs =
@@ -65,7 +65,7 @@ let expand_loadind_ptr dst base ofs =
 (* Fix-up code around calls to variadic functions.  Floating-point arguments
    residing in FP registers need to be moved to integer registers. *)
 
-let int_param_regs   = let open Asmblock in [| GPR0; GPR1; GPR2; GPR3; GPR4; GPR5; GPR6; GPR7; GPR8; GPR9; GPR10; GPR11 |]
+let int_param_regs   = let open Asmvliw in [| GPR0; GPR1; GPR2; GPR3; GPR4; GPR5; GPR6; GPR7; GPR8; GPR9; GPR10; GPR11 |]
 (* let float_param_regs = [| F10; F11; F12; F13; F14; F15; F16; F17 |] *)
 let float_param_regs = [| |]
 
@@ -131,7 +131,7 @@ let emit_move dst r =
 (* FIXME DMonniaux this is probably not complete *)
 let get_builtin_arg dst arg =
   match arg with
-  | BA (Asmblock.IR reg) -> emit_move dst reg
+  | BA (Asmvliw.IR reg) -> emit_move dst reg
   | BA (ireg) ->  failwith "get_builtin_arg: BA_int(not ireg)"
   | BA_int _ -> failwith "get_builtin_arg: BA_int"
   | BA_long _ -> failwith "get_builtin_arg: BA_long"
@@ -147,9 +147,9 @@ let get_builtin_arg dst arg =
 (* FIXME DMonniaux this is really suboptimal (byte per byte) *)
 let expand_builtin_memcpy_big sz al src dst =
   assert (sz > Z.zero);
-  let dstptr = Asmblock.GPR62
-  and srcptr = Asmblock.GPR63
-  and tmpbuf = Asmblock.GPR61 in
+  let dstptr = Asmvliw.GPR62
+  and srcptr = Asmvliw.GPR63
+  and tmpbuf = Asmvliw.GPR61 in
   get_builtin_arg dstptr dst;
   get_builtin_arg srcptr src;
   emit (Pmake (tmpbuf, sz));
@@ -157,10 +157,10 @@ let expand_builtin_memcpy_big sz al src dst =
   let lbl = new_label() in
   emit (Ploopdo (tmpbuf, lbl));
   emit Psemi;
-  emit (Plb (tmpbuf, srcptr, AOff (Asmblock.Ofsimm Z.zero)));
+  emit (Plb (tmpbuf, srcptr, AOff (Asmvliw.Ofsimm Z.zero)));
   emit (Paddil (srcptr, srcptr, Z.one));
   emit Psemi;
-  emit (Psb (tmpbuf, dstptr, AOff (Asmblock.Ofsimm Z.zero)));
+  emit (Psb (tmpbuf, dstptr, AOff (Asmvliw.Ofsimm Z.zero)));
   emit (Paddil (dstptr, dstptr, Z.one));
   emit Psemi;
   emit (Plabel lbl);;
@@ -175,41 +175,41 @@ let expand_builtin_memcpy  sz al args =
 (* FIXME probably need to check for size of displacement *)
 let expand_builtin_vload_common chunk base ofs res =
   match chunk, res with
-  | Mint8unsigned, BR(Asmblock.IR res) ->
-     emit (Plbu (res, base, AOff (Asmblock.Ofsimm ofs)))
-  | Mint8signed, BR(Asmblock.IR res) ->
-     emit (Plb  (res, base, AOff (Asmblock.Ofsimm ofs)))
-  | Mint16unsigned, BR(Asmblock.IR res) ->
-     emit (Plhu (res, base, AOff (Asmblock.Ofsimm ofs)))
-  | Mint16signed, BR(Asmblock.IR res) ->
-     emit (Plh  (res, base, AOff (Asmblock.Ofsimm ofs)))
-  | Mint32, BR(Asmblock.IR res) ->
-     emit (Plw  (res, base, AOff (Asmblock.Ofsimm ofs)))
-  | Mint64, BR(Asmblock.IR res) ->
-     emit (Pld  (res, base, AOff (Asmblock.Ofsimm ofs)))
-  | Mint64, BR_splitlong(BR(Asmblock.IR res1), BR(Asmblock.IR res2)) ->
+  | Mint8unsigned, BR(Asmvliw.IR res) ->
+     emit (Plbu (res, base, AOff (Asmvliw.Ofsimm ofs)))
+  | Mint8signed, BR(Asmvliw.IR res) ->
+     emit (Plb  (res, base, AOff (Asmvliw.Ofsimm ofs)))
+  | Mint16unsigned, BR(Asmvliw.IR res) ->
+     emit (Plhu (res, base, AOff (Asmvliw.Ofsimm ofs)))
+  | Mint16signed, BR(Asmvliw.IR res) ->
+     emit (Plh  (res, base, AOff (Asmvliw.Ofsimm ofs)))
+  | Mint32, BR(Asmvliw.IR res) ->
+     emit (Plw  (res, base, AOff (Asmvliw.Ofsimm ofs)))
+  | Mint64, BR(Asmvliw.IR res) ->
+     emit (Pld  (res, base, AOff (Asmvliw.Ofsimm ofs)))
+  | Mint64, BR_splitlong(BR(Asmvliw.IR res1), BR(Asmvliw.IR res2)) ->
      let ofs' = Ptrofs.add ofs _4 in
      if base <> res2 then begin
-         emit (Plw (res2, base, AOff (Asmblock.Ofsimm ofs)));
-         emit (Plw (res1, base, AOff (Asmblock.Ofsimm ofs')))
+         emit (Plw (res2, base, AOff (Asmvliw.Ofsimm ofs)));
+         emit (Plw (res1, base, AOff (Asmvliw.Ofsimm ofs')))
        end else begin
-         emit (Plw (res1, base, AOff (Asmblock.Ofsimm ofs')));
-         emit (Plw (res2, base, AOff (Asmblock.Ofsimm ofs)))
+         emit (Plw (res1, base, AOff (Asmvliw.Ofsimm ofs')));
+         emit (Plw (res2, base, AOff (Asmvliw.Ofsimm ofs)))
        end
-  | Mfloat32, BR(Asmblock.IR res) ->
-     emit (Pfls (res, base, AOff (Asmblock.Ofsimm ofs)))
-  | Mfloat64, BR(Asmblock.IR res) ->
-     emit (Pfld (res, base, AOff (Asmblock.Ofsimm ofs)))
+  | Mfloat32, BR(Asmvliw.IR res) ->
+     emit (Pfls (res, base, AOff (Asmvliw.Ofsimm ofs)))
+  | Mfloat64, BR(Asmvliw.IR res) ->
+     emit (Pfld (res, base, AOff (Asmvliw.Ofsimm ofs)))
   | _ ->
      assert false
 
 let expand_builtin_vload chunk args res =
   match args with
-  | [BA(Asmblock.IR addr)] ->
+  | [BA(Asmvliw.IR addr)] ->
       expand_builtin_vload_common chunk addr _0 res
   | [BA_addrstack ofs] ->
      expand_builtin_vload_common chunk stack_pointer ofs res
-  | [BA_addptr(BA(Asmblock.IR addr), (BA_int ofs | BA_long ofs))] ->
+  | [BA_addptr(BA(Asmvliw.IR addr), (BA_int ofs | BA_long ofs))] ->
      expand_builtin_vload_common chunk addr ofs res
   | _ ->
       assert false
@@ -217,32 +217,32 @@ let expand_builtin_vload chunk args res =
 
 let expand_builtin_vstore_common chunk base ofs src =
   match chunk, src with
-  | (Mint8signed | Mint8unsigned), BA(Asmblock.IR src) ->
-     emit (Psb (src, base, AOff (Asmblock.Ofsimm ofs)))
-  | (Mint16signed | Mint16unsigned), BA(Asmblock.IR src) ->
-     emit (Psh (src, base, AOff (Asmblock.Ofsimm ofs)))
-  | Mint32, BA(Asmblock.IR src) ->
-     emit (Psw (src, base, AOff (Asmblock.Ofsimm ofs)))
-  | Mint64, BA(Asmblock.IR src) ->
-     emit (Psd (src, base, AOff (Asmblock.Ofsimm ofs)))
-  | Mint64, BA_splitlong(BA(Asmblock.IR src1), BA(Asmblock.IR src2)) ->
+  | (Mint8signed | Mint8unsigned), BA(Asmvliw.IR src) ->
+     emit (Psb (src, base, AOff (Asmvliw.Ofsimm ofs)))
+  | (Mint16signed | Mint16unsigned), BA(Asmvliw.IR src) ->
+     emit (Psh (src, base, AOff (Asmvliw.Ofsimm ofs)))
+  | Mint32, BA(Asmvliw.IR src) ->
+     emit (Psw (src, base, AOff (Asmvliw.Ofsimm ofs)))
+  | Mint64, BA(Asmvliw.IR src) ->
+     emit (Psd (src, base, AOff (Asmvliw.Ofsimm ofs)))
+  | Mint64, BA_splitlong(BA(Asmvliw.IR src1), BA(Asmvliw.IR src2)) ->
      let ofs' = Ptrofs.add ofs _4 in
-     emit (Psw (src2, base, AOff (Asmblock.Ofsimm ofs)));
-     emit (Psw (src1, base, AOff (Asmblock.Ofsimm ofs')))
-  | Mfloat32, BA(Asmblock.IR src) ->
-     emit (Pfss (src, base, AOff (Asmblock.Ofsimm ofs)))
-  | Mfloat64, BA(Asmblock.IR src) ->
-     emit (Pfsd (src, base, AOff (Asmblock.Ofsimm ofs)))
+     emit (Psw (src2, base, AOff (Asmvliw.Ofsimm ofs)));
+     emit (Psw (src1, base, AOff (Asmvliw.Ofsimm ofs')))
+  | Mfloat32, BA(Asmvliw.IR src) ->
+     emit (Pfss (src, base, AOff (Asmvliw.Ofsimm ofs)))
+  | Mfloat64, BA(Asmvliw.IR src) ->
+     emit (Pfsd (src, base, AOff (Asmvliw.Ofsimm ofs)))
   | _ ->
      assert false
 
 let expand_builtin_vstore chunk args =
   match args with
-  | [BA(Asmblock.IR addr); src] ->
+  | [BA(Asmvliw.IR addr); src] ->
       expand_builtin_vstore_common chunk addr _0 src
   | [BA_addrstack ofs; src] ->
      expand_builtin_vstore_common chunk stack_pointer ofs src
-  | [BA_addptr(BA(Asmblock.IR addr), (BA_int ofs | BA_long ofs)); src] ->
+  | [BA_addptr(BA(Asmvliw.IR addr), (BA_int ofs | BA_long ofs)); src] ->
      expand_builtin_vstore_common chunk addr ofs src
   | _ ->
       assert false
@@ -265,7 +265,7 @@ let arguments_size sg =
 let _nbregargs_ = 12
 let _alignment_ = 8
 
-let save_arguments first_reg base_ofs = let open Asmblock in
+let save_arguments first_reg base_ofs = let open Asmvliw in
   for i = first_reg to (_nbregargs_ - 1) do begin
     expand_storeind_ptr
       int_param_regs.(i)
@@ -281,9 +281,9 @@ match !vararg_start_ofs with
   | None ->
       invalid_arg "Fatal error: va_start used in non-vararg function"
   | Some ofs ->
-      expand_addptrofs Asmblock.GPR32 stack_pointer (Ptrofs.repr ofs);
+      expand_addptrofs Asmvliw.GPR32 stack_pointer (Ptrofs.repr ofs);
       emit Psemi;
-      expand_storeind_ptr Asmblock.GPR32 r Ptrofs.zero
+      expand_storeind_ptr Asmvliw.GPR32 r Ptrofs.zero
 
 (* Auxiliary for 64-bit integer arithmetic built-ins.  They expand to
    two instructions, one computing the low 32 bits of the result,
@@ -348,7 +348,7 @@ let expand_bswap64 d s = assert false
 
 (* Handling of compiler-inlined builtins *)
 
-let expand_builtin_inline name args res = let open Asmblock in
+let expand_builtin_inline name args res = let open Asmvliw in
   match name, args, res with
   (* Synchronization *)
   | "__builtin_membar", [], _ ->
@@ -376,14 +376,14 @@ let expand_instruction instr =
   match instr with
   | Pallocframe (sz, ofs) ->
       let sg = get_current_function_sig() in
-      emit (Pmv (Asmblock.GPR17, stack_pointer));
+      emit (Pmv (Asmvliw.GPR17, stack_pointer));
       if sg.sig_cc.cc_vararg then begin
         let n = arguments_size sg in
         let extra_sz = if n >= _nbregargs_ then 0 else (* align _alignment_ *) ((_nbregargs_ - n) * wordsize) in
         let full_sz = Z.add sz (Z.of_uint extra_sz) in
         expand_addptrofs stack_pointer stack_pointer (Ptrofs.repr (Z.neg full_sz));
         emit Psemi;
-        expand_storeind_ptr Asmblock.GPR17 stack_pointer ofs;
+        expand_storeind_ptr Asmvliw.GPR17 stack_pointer ofs;
         emit Psemi;
         let va_ofs =
             sz in
@@ -393,7 +393,7 @@ let expand_instruction instr =
       end else begin
         expand_addptrofs stack_pointer stack_pointer (Ptrofs.repr (Z.neg sz));
         emit Psemi;
-        expand_storeind_ptr Asmblock.GPR17 stack_pointer ofs;
+        expand_storeind_ptr Asmvliw.GPR17 stack_pointer ofs;
         emit Psemi;
         vararg_start_ofs := None
       end
@@ -476,7 +476,7 @@ let expand_instruction instr =
 
 (* NOTE: Dwarf register maps for RV32G are not yet specified
    officially.  This is just a placeholder.  *)
-let int_reg_to_dwarf = let open Asmblock in function
+let int_reg_to_dwarf = let open Asmvliw in function
    | GPR0  -> 1   | GPR1  -> 2   | GPR2  -> 3   | GPR3  -> 4   | GPR4  -> 5
    | GPR5  -> 6   | GPR6  -> 7   | GPR7  -> 8   | GPR8  -> 9   | GPR9  -> 10
    | GPR10 -> 11  | GPR11 -> 12  | GPR12 -> 13  | GPR13 -> 14  | GPR14 -> 15
@@ -491,7 +491,7 @@ let int_reg_to_dwarf = let open Asmblock in function
    | GPR55 -> 56  | GPR56 -> 57  | GPR57 -> 58  | GPR58 -> 59  | GPR59 -> 60
    | GPR60 -> 61  | GPR61 -> 62  | GPR62 -> 63  | GPR63 -> 64
 
-let preg_to_dwarf = let open Asmblock in function
+let preg_to_dwarf = let open Asmvliw in function
    | IR r -> int_reg_to_dwarf r
    | RA   -> 65 (* FIXME - No idea what is $ra DWARF number in k1-gdb *)
    | _ -> assert false
diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v
index c15a33af..8620326f 100644
--- a/mppa_k1c/Asmvliw.v
+++ b/mppa_k1c/Asmvliw.v
@@ -15,7 +15,9 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-(** Abstract syntax and semantics for K1c assembly language. *)
+(** Abstract syntax and semantics for VLIW semantics of K1c assembly language. *)
+
+(* FIXME: develop/fix the comments in this file *)
 
 Require Import Coqlib.
 Require Import Maps.
@@ -31,24 +33,1012 @@ Require Import Locations.
 Require Stacklayout.
 Require Import Conventions.
 Require Import Errors.
-Require Export Asmblock.
 Require Import Sorting.Permutation.
 
+(** * Abstract syntax *)
+
+(** A K1c program is syntactically given as a list of functions. 
+    Each function is associated to a list of bundles of type [bblock] below.
+    Hence, syntactically, we view each bundle as a basic block:
+    this view induces our sequential semantics of bundles defined in [Asmblock].
+*)
+
+(** 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. *)
+
+(** basic register *)
+Inductive preg: Type :=
+  | IR: gpreg -> preg                   (**r integer general purpose registers *)
+  | RA: preg
+  | PC: preg
+  .
+
+Coercion IR: gpreg >-> preg.
+
+Lemma preg_eq: forall (x y: preg), {x=y} + {x<>y}.
+Proof. decide equality. apply ireg_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'" := GPR17 (only parsing) : asm.
+Notation "'MFP'" := R17 (only parsing) : asm.
+Notation "'GPRA'" := GPR16 (only parsing) : asm.
+Notation "'RTMP'" := GPR32 (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 *)
+  .
+
+Inductive ftest: Type :=
+  | FTone                               (**r Ordered and Not Equal *)
+  | FTueq                               (**r Unordered or Equal *)
+  | FToeq                               (**r Ordered and Equal *)
+  | FTune                               (**r Unordered or Not Equal *)
+  | FTolt                               (**r Ordered and Less Than *)
+  | FTuge                               (**r Unordered or Greater Than or Equal *)
+  | FToge                               (**r Ordered and Greater Than or Equal *)
+  | FTult                               (**r Unordered or Less Than *)
+  .
+
+(** 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.
+*)
+
+(** * Instructions *)
+
+Definition label := positive.
+
+(* FIXME - rewrite the comment *)
+(** 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 in control-flow 
+*)
+Inductive ex_instruction : Type :=
+  (* Pseudo-instructions *)
+(*| Ploadsymbol_high (rd: ireg) (id: ident) (ofs: ptrofs) (**r load the high part of the address of a symbol *)
+  | 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) *)
+.
+
+(** FIXME: comment not up to date !
+
+
+ The pseudo-instructions are the following:
+
+- [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.
+
+- [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.
+*)
+
+(** Control Flow instructions *)
+Inductive cf_instruction : Type :=
+  | Pret                                            (**r return *)
+  | Pcall   (l: label)                              (**r function call *)
+  | Picall  (r: ireg)                               (**r function call on register value *)
+  | Pjumptable (r: ireg) (labels: list label) (**r N-way branch through a jump table (pseudo) *)
+
+  (* Pgoto is for tailcalls, Pj_l is for jumping to a particular label *)
+  | Pgoto   (l: label)                              (**r goto *)
+  | Pigoto  (r: ireg)                               (**r goto from register *)
+  | 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 load_name : Type :=
+  | Plb                                             (**r load byte *)
+  | Plbu                                            (**r load byte unsigned *)
+  | Plh                                             (**r load half word *)
+  | Plhu                                            (**r load half word unsigned *)
+  | Plw                                             (**r load int32 *)
+  | Plw_a                                           (**r load any32 *)
+  | Pld                                             (**r load int64 *)
+  | Pld_a                                           (**r load any64 *)
+  | Pfls                                            (**r load float *)
+  | Pfld                                            (**r load 64-bit float *)
+.
+
+Inductive ld_instruction : Type :=
+  | PLoadRRO   (i: load_name) (rd: ireg) (ra: ireg) (ofs: offset)
+  | PLoadRRR   (i: load_name) (rd: ireg) (ra: ireg) (rofs: ireg)
+.
+
+Coercion PLoadRRO:       load_name        >-> Funclass.
+Coercion PLoadRRR:       load_name        >-> Funclass.
+
+(** Stores **)
+Inductive store_name : Type :=
+  | Psb                                             (**r store byte *)
+  | Psh                                             (**r store half byte *)
+  | Psw                                             (**r store int32 *)
+  | Psw_a                                           (**r store any32 *)
+  | Psd                                             (**r store int64 *)
+  | Psd_a                                           (**r store any64 *)
+  | Pfss                                            (**r store float *)
+  | Pfsd                                            (**r store 64-bit float *)
+.
+
+Inductive st_instruction : Type :=
+  | PStoreRRO  (i: store_name) (rs: ireg) (ra: ireg) (ofs: offset)
+  | PStoreRRR  (i: store_name) (rs: ireg) (ra: ireg) (rofs: ireg)
+.
+
+Coercion PStoreRRO:       store_name        >-> Funclass.
+Coercion PStoreRRR:       store_name        >-> Funclass.
+
+(** Arithmetic instructions **)
+Inductive arith_name_r : Type :=
+  | Ploadsymbol (id: ident) (ofs: ptrofs)           (**r load the address of a symbol *)
+.
+
+Inductive arith_name_rr : Type :=
+  | Pmv                                             (**r register move *)
+  | Pnegw                                           (**r negate word *)
+  | Pnegl                                           (**r negate long *)
+  | Pcvtl2w                                         (**r Convert Long to Word *)
+  | Psxwd                                           (**r Sign Extend Word to Double Word *)
+  | Pzxwd                                           (**r Zero Extend Word to Double Word *)
+
+  | Pfabsd                                          (**r float absolute double *)
+  | Pfabsw                                          (**r float absolute word *)
+  | Pfnegd                                          (**r float negate double *)
+  | Pfnegw                                          (**r float negate word *)
+  | Pfnarrowdw                                      (**r float narrow 64 -> 32 bits *)
+  | Pfwidenlwd                                      (**r Floating Point widen from 32 bits to 64 bits *)
+  | Pfloatwrnsz                                     (**r Floating Point conversion from integer (int -> SINGLE) *)
+  | Pfloatuwrnsz                                    (**r Floating Point conversion from integer (unsigned int -> SINGLE) *)
+  | Pfloatudrnsz                                    (**r Floating Point Conversion from integer (unsigned long -> float) *)
+  | Pfloatudrnsz_i32                                (**r Floating Point Conversion from integer (unsigned int -> float) *)
+  | Pfloatdrnsz                                     (**r Floating Point Conversion from integer (long -> float) *)
+  | Pfloatdrnsz_i32                                 (**r Floating Point Conversion from integer (int -> float) *)
+  | Pfixedwrzz                                      (**r Integer conversion from floating point (single -> int) *)
+  | Pfixeduwrzz                                     (**r Integer conversion from floating point (single -> unsigned int) *)
+  | Pfixeddrzz                                      (**r Integer conversion from floating point (float -> long) *)
+  | Pfixedudrzz                                      (**r Integer conversion from floating point (float -> unsigned long) *)
+  | Pfixeddrzz_i32                                  (**r Integer conversion from floating point (float -> int) *)
+  | Pfixedudrzz_i32                                  (**r Integer conversion from floating point (float -> unsigned int) *)
+.
+
+Inductive arith_name_ri32 : Type :=
+  | Pmake                                           (**r load immediate *)
+.
+
+Inductive arith_name_ri64 : Type :=
+  | Pmakel                                          (**r load immediate long *)
+.
+
+Inductive arith_name_rf32 : Type :=
+  | Pmakefs                                         (**r load immediate single *)
+.
+
+Inductive arith_name_rf64 : Type :=
+  | Pmakef                                          (**r load immediate float *)
+.
+
+Inductive arith_name_rrr : Type :=
+  | Pcompw  (it: itest)                             (**r comparison word *)
+  | Pcompl  (it: itest)                             (**r comparison long *)
+  | Pfcompw (ft: ftest)                             (**r comparison float32 *)
+  | Pfcompl (ft: ftest)                             (**r comparison float64 *)
+
+  | Paddw                                           (**r add word *)
+  | Psubw                                           (**r sub word *)
+  | Pmulw                                           (**r mul word *)
+  | Pandw                                           (**r and word *)
+  | Pnandw                                          (**r nand word *)
+  | Porw                                            (**r or word *)
+  | Pnorw                                           (**r nor word *)
+  | Pxorw                                           (**r xor word *)
+  | Pnxorw                                          (**r nxor word *)
+  | Pandnw                                          (**r andn word *)
+  | Pornw                                           (**r orn 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 *)
+  | Pnandl                                          (**r nand long *)
+  | Porl                                            (**r or long *)
+  | Pnorl                                           (**r nor long *)
+  | Pxorl                                           (**r xor long *)
+  | Pnxorl                                          (**r nxor long *)
+  | Pandnl                                          (**r andn long *)
+  | Pornl                                           (**r orn 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 *)
+
+  | Pfaddd                                          (**r float add double *)
+  | Pfaddw                                          (**r float add word *)
+  | Pfsbfd                                          (**r float sub double *)
+  | Pfsbfw                                          (**r float sub word *)
+  | Pfmuld                                          (**r float multiply double *)
+  | Pfmulw                                          (**r float multiply word *)
+.
+
+Inductive arith_name_rri32 : Type :=
+  | Pcompiw (it: itest)                             (**r comparison imm word *)
+
+  | Paddiw                                          (**r add imm word *)
+  | Pmuliw                                          (**r add imm word *)
+  | Pandiw                                          (**r and imm word *)
+  | Pnandiw                                         (**r nand imm word *)
+  | Poriw                                           (**r or imm word *)
+  | Pnoriw                                          (**r nor imm word *)
+  | Pxoriw                                          (**r xor imm word *)
+  | Pnxoriw                                         (**r nxor imm word *)
+  | Pandniw                                         (**r andn word *)
+  | Porniw                                          (**r orn word *)
+  | Psraiw                                          (**r shift right arithmetic imm word *)
+  | Psrliw                                          (**r shift right logical imm word *)
+  | Pslliw                                          (**r shift left logical imm word *)
+  | Proriw                                          (**r rotate right 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 *) 
+  | Pmulil                                          (**r mul immediate long *) 
+  | Pandil                                          (**r and immediate long *) 
+  | Pnandil                                         (**r nand immediate long *) 
+  | Poril                                           (**r or immediate long *) 
+  | Pnoril                                          (**r nor immediate long *) 
+  | Pxoril                                          (**r xor immediate long *) 
+  | Pnxoril                                         (**r nxor immediate long *) 
+  | Pandnil                                         (**r andn immediate long *)
+  | Pornil                                          (**r orn immediate long *)
+.
+
+Inductive arith_name_arrr : Type :=
+  | Pmaddw                                           (**r multiply add word *)
+  | Pmaddl                                           (**r multiply add long *)
+  | Pcmove (bt: btest)                               (**r conditional move *)
+  | Pcmoveu (bt: btest)                              (**r conditional move, test on unsigned semantics *)
+.
+
+Inductive arith_name_arri32 : Type :=
+  | Pmaddiw                                           (**r multiply add word *)
+.
+
+Inductive arith_name_arri64 : Type :=
+  | Pmaddil                                           (**r multiply add 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)
+  | PArithRF32  (i: arith_name_rf32)  (rd: ireg) (imm: float32)
+  | PArithRF64  (i: arith_name_rf64)  (rd: ireg) (imm: float)
+  | 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)
+  | PArithARRR   (i: arith_name_arrr)   (rd rs1 rs2: ireg)
+  | PArithARRI32 (i: arith_name_arri32) (rd rs: ireg) (imm: int)
+  | PArithARRI64 (i: arith_name_arri64) (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 PArithRF32:    arith_name_rf32     >-> Funclass.
+Coercion PArithRF64:    arith_name_rf64     >-> Funclass.
+Coercion PArithRRR:     arith_name_rrr      >-> Funclass.
+Coercion PArithRRI32:   arith_name_rri32    >-> Funclass.
+Coercion PArithRRI64:   arith_name_rri64    >-> Funclass.
+Coercion PArithARRR:     arith_name_arrr      >-> Funclass.
+Coercion PArithARRI32:   arith_name_arri32    >-> Funclass.
+Coercion PArithARRI64:   arith_name_arri64    >-> Funclass.
+
+Inductive basic : Type :=
+  | PArith          (i: ar_instruction)
+  | PLoad           (i: ld_instruction)
+  | PStore          (i: st_instruction)
+  | Pallocframe (sz: Z) (pos: ptrofs)               (**r allocate new stack frame *)
+  | Pfreeframe  (sz: Z) (pos: ptrofs)               (**r deallocate stack frame and restore previous frame *)
+  | Pget    (rd: ireg) (rs: preg)                   (**r get system register *)
+  | Pset    (rd: preg) (rs: ireg)                   (**r set system register *)
+  | Pnop                                            (**r virtual instruction that does nothing *)
+.
+
+Coercion PLoad:         ld_instruction >-> basic.
+Coercion PStore:        st_instruction >-> basic.
+Coercion PArith:        ar_instruction >-> basic.
+
+
+Inductive control : Type :=
+  | PExpand         (i: ex_instruction)
+  | PCtlFlow        (i: cf_instruction)
+.
+
+Coercion PExpand:   ex_instruction >-> control.
+Coercion PCtlFlow:  cf_instruction >-> control.
+
+
+(** * Definition of a bblock (ie a bundle) *)
+
+Definition non_empty_body (body: list basic): bool :=
+  match body with
+  | nil => false
+  | _ => true
+  end.
+
+Definition non_empty_exit (exit: option control): bool :=
+  match exit with
+  | None => false
+  | _ => true
+  end.
+
+Definition non_empty_bblockb (body: list basic) (exit: option control): bool := non_empty_body body || non_empty_exit exit.
+
+
+(** TODO
+ * For now, we consider a builtin is alone in a bundle (and a basic block).
+ * Is there a way to avoid that ?
+ *)
+Definition builtin_aloneb (body: list basic) (exit: option control) :=
+  match exit with
+  | Some (PExpand (Pbuiltin _ _ _)) =>
+    match body with
+    | nil => true
+    | _ => false
+    end
+  | _ => true
+  end.
+
+Definition wf_bblockb (body: list basic) (exit: option control) :=
+  (non_empty_bblockb body exit) && (builtin_aloneb body exit).
+
+(** A bblock is well-formed if he contains at least one instruction,
+    and if there is a builtin then it must be alone in this bblock. *)
+
+Record bblock := mk_bblock {
+  header: list label;
+  body: list basic;
+  exit: option control;
+  correct: Is_true (wf_bblockb body exit)
+}.
+
+(* FIXME? redundant with definition in Machblock *)
+Definition length_opt {A} (o: option A) : nat :=
+  match o with
+  | Some o => 1
+  | None => 0
+  end.
+
+(* WARNING: the notion of size is not the same than in Machblock !
+   We ignore labels here...
+   The result is in Z to be compatible with operations on PC
+*)
+Definition size (b:bblock): Z := Z.of_nat (length (body b) + length_opt (exit b)).
+
+Definition bblocks := list bblock.
+
+Fixpoint size_blocks (l: bblocks): Z :=
+  match l with
+  | nil => 0
+  | b :: l =>
+     (size b) + (size_blocks l)
+  end
+  .
+
+Record function : Type := mkfunction { fn_sig: signature; fn_blocks: bblocks }.
+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.
+
+Notation "a # b" := (a b) (at level 1, only parsing) : asm.
+Notation "a # b <- c" := (Pregmap.set b c a) (at level 1, b at next level) : asm.
+
+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.
+
+(* TODO: Is it still useful ?? *)
+
+
+(** 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.
+
 Local Open Scope asm.
 
+(** * Parallel Semantics of bundles *)
+
 Section RELSEM.
 
 (** Execution of arith instructions *)
 
 Variable ge: genv.
 
-(* TODO: on pourrait mettre ça dans Asmblock pour factoriser le code
-   en définissant 
-    exec_arith_instr ai rs := parexec_arith_instr ai rs rs
-*)
+(** 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 (rs:regset) (m:mem)
+  | Stuck
+.
+
+(** ** Arithmetic Expressions (including comparisons) *)
+
+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.
+
+Inductive oporder_ftest :=
+  | Normal (ft: ftest)
+  | Reversed (ft: ftest)
+.
+
+Definition ftest_for_cmp (c: comparison) :=
+  match c with
+  | Ceq => Normal FToeq
+  | Cne => Normal FTune
+  | Clt => Normal FTolt
+  | Cle => Reversed FToge
+  | Cgt => Reversed FTolt
+  | Cge => Normal FToge
+  end.
+
+Definition notftest_for_cmp (c: comparison) :=
+  match c with
+  | Ceq => Normal FTune
+  | Cne => Normal FToeq
+  | Clt => Normal FTuge
+  | Cle => Reversed FTult
+  | Cgt => Reversed FTuge
+  | Cge => Normal FTult
+  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.
+
+
+(* a few lemma on comparisons of unsigned (e.g. pointers) *)
+
+Definition Val_cmpu_bool cmp v1 v2: option bool :=
+  Val.cmpu_bool (fun _ _ => true) cmp v1 v2.
+
+Lemma Val_cmpu_bool_correct (m:mem) (cmp: comparison) (v1 v2: val) b:
+   (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) = Some b
+   -> (Val_cmpu_bool cmp v1 v2) = Some b.
+Proof.
+  intros; eapply Val.cmpu_bool_lessdef; (econstructor 1 || eauto).
+Qed.
+
+Definition Val_cmpu cmp v1 v2 := Val.of_optbool (Val_cmpu_bool cmp v1 v2).
+
+Lemma Val_cmpu_correct (m:mem) (cmp: comparison) (v1 v2: val):
+   Val.lessdef (Val.cmpu (Mem.valid_pointer m) cmp v1 v2)
+               (Val_cmpu cmp v1 v2).
+Proof.
+  unfold Val.cmpu, Val_cmpu.
+  remember (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) as ob.
+  destruct ob; simpl.
+  - erewrite Val_cmpu_bool_correct; eauto.
+    econstructor.
+  - econstructor.
+Qed.
+
+Definition Val_cmplu_bool (cmp: comparison) (v1 v2: val)
+ := (Val.cmplu_bool (fun _ _ => true) cmp v1 v2).
+
+Lemma Val_cmplu_bool_correct (m:mem) (cmp: comparison) (v1 v2: val) b:
+   (Val.cmplu_bool (Mem.valid_pointer m) cmp v1 v2) = Some b
+   -> (Val_cmplu_bool cmp v1 v2) = Some b.
+Proof.
+  intros; eapply Val.cmplu_bool_lessdef; (econstructor 1 || eauto).
+Qed.
+
+Definition Val_cmplu cmp v1 v2 := Val.of_optbool (Val_cmplu_bool cmp v1 v2).
+
+Lemma Val_cmplu_correct (m:mem) (cmp: comparison) (v1 v2: val):
+   Val.lessdef (Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp v1 v2))
+               (Val_cmplu cmp v1 v2).
+Proof.
+  unfold Val.cmplu, Val_cmplu.
+  remember (Val.cmplu_bool (Mem.valid_pointer m) cmp v1 v2) as ob.
+  destruct ob as [b|]; simpl.
+  - erewrite Val_cmplu_bool_correct; eauto.
+    simpl. econstructor.
+  - econstructor.
+Qed.
+
+
+
+(** Comparing integers *)
+Definition compare_int (t: itest) (v1 v2: val): 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 Cne v1 v2
+  | ITequ => Val_cmpu Ceq v1 v2
+  | ITltu => Val_cmpu Clt v1 v2
+  | ITgeu => Val_cmpu Cge v1 v2
+  | ITleu => Val_cmpu Cle v1 v2
+  | ITgtu => Val_cmpu Cgt v1 v2
+  | ITall
+  | ITnall
+  | ITany
+  | ITnone => Vundef
+  end.
+
+Definition compare_long (t: itest) (v1 v2: val): 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 => Some (Val_cmplu Cne v1 v2)
+  | ITequ => Some (Val_cmplu Ceq v1 v2)
+  | ITltu => Some (Val_cmplu Clt v1 v2)
+  | ITgeu => Some (Val_cmplu Cge v1 v2)
+  | ITleu => Some (Val_cmplu Cle v1 v2)
+  | ITgtu => Some (Val_cmplu Cgt v1 v2)
+  | ITall
+  | ITnall
+  | ITany
+  | ITnone => Some Vundef
+  end in 
+  match res with
+  | Some v => v
+  | None => Vundef
+  end
+  .
+
+Definition compare_single (t: ftest) (v1 v2: val): val :=
+  match t with
+  | FTone | FTueq => Vundef (* unused *)
+  | FToeq => Val.cmpfs Ceq v1 v2
+  | FTune => Val.cmpfs Cne v1 v2
+  | FTolt => Val.cmpfs Clt v1 v2
+  | FTuge => Val.notbool (Val.cmpfs Clt v1 v2)
+  | FToge => Val.cmpfs Cge v1 v2
+  | FTult => Val.notbool (Val.cmpfs Cge v1 v2)
+  end.
+
+Definition compare_float (t: ftest) (v1 v2: val): val :=
+  match t with
+  | FTone | FTueq => Vundef (* unused *)
+  | FToeq => Val.cmpf Ceq v1 v2
+  | FTune => Val.cmpf Cne v1 v2
+  | FTolt => Val.cmpf Clt v1 v2
+  | FTuge => Val.notbool (Val.cmpf Clt v1 v2)
+  | FToge => Val.cmpf Cge v1 v2
+  | FTult => Val.notbool (Val.cmpf Cge v1 v2)
+  end.
+
+Definition arith_eval_r n :=
+  match n with
+  | Ploadsymbol s ofs => Genv.symbol_address ge s ofs
+  end
+.
+
+Definition arith_eval_rr n v :=
+  match n with
+  | Pmv => v
+  | Pnegw => Val.neg v
+  | Pnegl => Val.negl v
+  | Pcvtl2w => Val.loword v
+  | Psxwd => Val.longofint v
+  | Pzxwd => Val.longofintu v
+  | Pfnegd => Val.negf v
+  | Pfnegw => Val.negfs v
+  | Pfabsd => Val.absf v
+  | Pfabsw => Val.absfs v
+  | Pfnarrowdw => Val.singleoffloat v
+  | Pfwidenlwd => Val.floatofsingle v
+  | Pfloatwrnsz => match Val.singleofint v with Some f => f | _ => Vundef end
+  | Pfloatuwrnsz => match Val.singleofintu v with Some f => f | _ => Vundef end
+  | Pfloatudrnsz => match Val.floatoflongu v with Some f => f | _ => Vundef end
+  | Pfloatdrnsz => match Val.floatoflong v with Some f => f | _ => Vundef end
+  | Pfloatudrnsz_i32 => match Val.floatofintu v with Some f => f | _ => Vundef end
+  | Pfloatdrnsz_i32 => match Val.floatofint v with Some f => f | _ => Vundef end
+  | Pfixedwrzz => match Val.intofsingle v with Some i => i | _ => Vundef end
+  | Pfixeduwrzz => match Val.intuofsingle v with Some i => i | _ => Vundef end
+  | Pfixeddrzz => match Val.longoffloat v with Some i => i | _ => Vundef end
+  | Pfixedudrzz => match Val.longuoffloat v with Some i => i | _ => Vundef end
+  | Pfixeddrzz_i32 => match Val.intoffloat v with Some i => i | _ => Vundef end
+  | Pfixedudrzz_i32 => match Val.intuoffloat v with Some i => i | _ => Vundef end
+  end.
+
+Definition arith_eval_ri32 n i :=
+  match n with
+  | Pmake => Vint i
+  end.
+
+Definition arith_eval_ri64 n i :=
+  match n with
+  | Pmakel => Vlong i
+  end.
+
+Definition arith_eval_rf32 n i :=
+  match n with
+  | Pmakefs => Vsingle i
+  end.
+
+Definition arith_eval_rf64 n i :=
+  match n with
+  | Pmakef => Vfloat i
+  end.
+
+Definition arith_eval_rrr n v1 v2 :=
+  match n with
+  | Pcompw c => compare_int c v1 v2
+  | Pcompl c => compare_long c v1 v2
+  | Pfcompw c => compare_single c v1 v2
+  | Pfcompl c => compare_float c v1 v2
+
+  | Paddw  => Val.add  v1 v2
+  | Psubw  => Val.sub  v1 v2
+  | Pmulw  => Val.mul  v1 v2
+  | Pandw  => Val.and  v1 v2
+  | Pnandw => Val.notint (Val.and v1 v2)
+  | Porw   => Val.or   v1 v2
+  | Pnorw  => Val.notint (Val.or v1 v2)
+  | Pxorw  => Val.xor  v1 v2
+  | Pnxorw => Val.notint (Val.xor v1 v2)
+  | Pandnw => Val.and (Val.notint v1) v2
+  | Pornw  => Val.or (Val.notint v1) v2
+  | Psrlw  => Val.shru v1 v2
+  | Psraw  => Val.shr  v1 v2
+  | Psllw  => Val.shl  v1 v2
+
+  | Paddl => Val.addl v1 v2
+  | Psubl => Val.subl v1 v2
+  | Pandl => Val.andl v1 v2
+  | Pnandl => Val.notl (Val.andl v1 v2)
+  | Porl  => Val.orl  v1 v2
+  | Pnorl  => Val.notl (Val.orl  v1 v2)
+  | Pxorl  => Val.xorl  v1 v2
+  | Pnxorl  => Val.notl (Val.xorl  v1 v2)
+  | Pandnl => Val.andl (Val.notl v1) v2
+  | Pornl  => Val.orl (Val.notl v1) v2
+  | Pmull => Val.mull v1 v2
+  | Pslll => Val.shll v1 v2
+  | Psrll => Val.shrlu v1 v2
+  | Psral => Val.shrl v1 v2
+
+  | Pfaddd => Val.addf v1 v2
+  | Pfaddw => Val.addfs v1 v2
+  | Pfsbfd => Val.subf v1 v2
+  | Pfsbfw => Val.subfs v1 v2
+  | Pfmuld => Val.mulf v1 v2
+  | Pfmulw => Val.mulfs v1 v2
+  end.
+
+Definition arith_eval_rri32 n v i :=
+  match n with
+  | Pcompiw c => compare_int c v (Vint i)
+  | Paddiw  => Val.add   v (Vint i)
+  | Pmuliw  => Val.mul   v (Vint i)
+  | Pandiw  => Val.and   v (Vint i)
+  | Pnandiw => Val.notint (Val.and  v (Vint i))
+  | Poriw   => Val.or    v (Vint i)
+  | Pnoriw  => Val.notint (Val.or v (Vint i))
+  | Pxoriw  => Val.xor   v (Vint i)
+  | Pnxoriw => Val.notint (Val.xor v (Vint i))
+  | Pandniw => Val.and (Val.notint v) (Vint i)
+  | Porniw  => Val.or (Val.notint v) (Vint i)
+  | Psraiw  => Val.shr   v (Vint i)
+  | Psrliw  => Val.shru  v (Vint i)
+  | Pslliw  => Val.shl   v (Vint i)
+  | Proriw  => Val.ror   v (Vint i)
+  | Psllil  => Val.shll  v (Vint i)
+  | Psrlil  => Val.shrlu v (Vint i)
+  | Psrail  => Val.shrl  v (Vint i)
+  end.
+
+Definition arith_eval_rri64 n v i :=
+  match n with
+  | Pcompil c => compare_long c v (Vlong i)
+  | Paddil  => Val.addl v (Vlong i)
+  | Pmulil  => Val.mull v (Vlong i)
+  | Pandil  => Val.andl v (Vlong i)
+  | Pnandil  => Val.notl (Val.andl v (Vlong i))
+  | Poril   => Val.orl  v (Vlong i)
+  | Pnoril   => Val.notl (Val.orl  v (Vlong i))
+  | Pxoril  => Val.xorl  v (Vlong i)
+  | Pnxoril  => Val.notl (Val.xorl  v (Vlong i))
+  | Pandnil => Val.andl (Val.notl v) (Vlong i)
+  | Pornil  => Val.orl (Val.notl v) (Vlong i)
+  end.
+
+Definition arith_eval_arrr n v1 v2 v3 :=
+  match n with
+  | Pmaddw => Val.add v1 (Val.mul v2 v3)
+  | Pmaddl => Val.addl v1 (Val.mull v2 v3)
+  | Pcmove bt =>
+    match cmp_for_btest bt with
+    | (Some c, Int)  =>
+      match Val.cmp_bool c v2 (Vint Int.zero) with
+      | None => Vundef
+      | Some true => v3
+      | Some false => v1
+      end
+    | (Some c, Long) =>
+      match Val.cmpl_bool c v2 (Vlong Int64.zero) with
+      | None => Vundef
+      | Some true => v3
+      | Some false => v1
+      end
+    | (None, _) => Vundef
+    end
+  | Pcmoveu bt =>
+    match cmpu_for_btest bt with
+    | (Some c, Int)  =>
+      match Val_cmpu_bool c v2 (Vint Int.zero) with
+      | None => Vundef
+      | Some true => v3
+      | Some false => v1
+      end
+    | (Some c, Long) =>
+      match Val_cmplu_bool c v2 (Vlong Int64.zero) with
+      | None => Vundef
+      | Some true => v3
+      | Some false => v1
+      end
+    | (None, _) => Vundef
+    end
+  end.
+
+Definition arith_eval_arri32 n v1 v2 v3 :=
+  match n with
+  | Pmaddiw => Val.add v1 (Val.mul v2 (Vint v3))
+  end.
+
+Definition arith_eval_arri64 n v1 v2 v3 :=
+  match n with
+  | Pmaddil => Val.addl v1 (Val.mull v2 (Vlong v3))
+  end.
+
 Definition parexec_arith_instr (ai: ar_instruction) (rsr rsw: regset): regset :=
   match ai with
-  | PArithR n d => rsw#d <- (arith_eval_r ge n)
+  | PArithR n d => rsw#d <- (arith_eval_r n)
 
   | PArithRR n d s => rsw#d <- (arith_eval_rr n rsr#s)
 
@@ -66,11 +1056,20 @@ Definition parexec_arith_instr (ai: ar_instruction) (rsr rsw: regset): regset :=
   | PArithARRI64 n d s i => rsw#d <- (arith_eval_arri64 n rsr#d rsr#s i)
   end.
 
+Definition eval_offset (ofs: offset) : res ptrofs :=
+  match ofs with
+  | Ofsimm n => OK n
+  | Ofslow id delta => 
+      match (Genv.symbol_address ge id delta) with
+      | Vptr b ofs => OK ofs
+      | _ => Error (msg "Asmblock.eval_offset")
+      end
+  end.
+
 (** * load/store *)
 
-(* TODO: factoriser ? *)
 Definition parexec_load_offset (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (d a: ireg) (ofs: offset) :=
-  match (eval_offset ge ofs) with
+  match (eval_offset ofs) with
   | OK ptr => match Mem.loadv chunk mr (Val.offset_ptr (rsr a) ptr) with
               | None => Stuck
               | Some v => Next (rsw#d <- v) mw
@@ -85,7 +1084,7 @@ Definition parexec_load_reg (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem)
   end.
 
 Definition parexec_store_offset (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (s a: ireg) (ofs: offset) :=
-  match (eval_offset ge ofs) with
+  match (eval_offset ofs) with
   | OK ptr => match Mem.storev chunk mr (Val.offset_ptr (rsr a) ptr) (rsr s) with
               | None => Stuck
               | Some m' => Next rsw m'
@@ -99,11 +1098,34 @@ Definition parexec_store_reg (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem
   | Some m' => Next rsw m'
   end.
 
-(* rem: parexec_store = exec_store *)
+Definition load_chunk n :=
+  match n with
+  | Plb => Mint8signed
+  | Plbu => Mint8unsigned
+  | Plh => Mint16signed
+  | Plhu => Mint16unsigned
+  | Plw => Mint32
+  | Plw_a => Many32
+  | Pld => Mint64
+  | Pld_a => Many64
+  | Pfls => Mfloat32
+  | Pfld => Mfloat64
+  end.
+
+Definition store_chunk n :=
+  match n with
+  | Psb => Mint8unsigned
+  | Psh => Mint16unsigned
+  | Psw => Mint32
+  | Psw_a => Many32
+  | Psd => Mint64
+  | Psd_a => Many64
+  | Pfss => Mfloat32
+  | Pfsd => Mfloat64
+  end.
 
 (** * basic instructions *)
 
-(* TODO: factoriser ? *)
 Definition parexec_basic_instr (bi: basic) (rsr rsw: regset) (mr mw: mem) :=
   match bi with
   | PArith ai => Next (parexec_arith_instr ai rsr rsw) mw
@@ -159,14 +1181,40 @@ Fixpoint parexec_wio_body (body: list basic) (rsr rsw: regset) (mr mw: mem) :=
      end
   end.
 
-(** Manipulations over the [PC] register: continuing with the next
-  instruction ([nextblock]) or branching to a label ([goto_label]). *)
+(** TODO: redundant w.r.t Machblock ?? *)
+Lemma in_dec (lbl: label) (l: list label):  { List.In lbl l } + { ~(List.In lbl l) }.
+Proof.
+  apply List.in_dec.
+  apply Pos.eq_dec.
+Qed.
+
 
-(* TODO: factoriser ? *)
-Definition par_nextblock size_b (rs: regset) :=
-  rs#PC <- (Val.offset_ptr rs#PC size_b).
 
-(* TODO: factoriser ? *)
+(** Note: copy-paste from Machblock *)
+Definition is_label (lbl: label) (bb: bblock) : bool :=
+  if in_dec lbl (header bb) then true else false.
+
+Lemma is_label_correct_true lbl bb:
+  List.In lbl (header bb) <-> is_label lbl bb = true. 
+Proof.
+  unfold is_label; destruct (in_dec lbl (header bb)); simpl; intuition.
+Qed.
+
+Lemma is_label_correct_false lbl bb:
+  ~(List.In lbl (header bb)) <-> is_label lbl bb = false. 
+Proof.
+  unfold is_label; destruct (in_dec lbl (header bb)); simpl; intuition.
+Qed.
+
+
+
+(** convert a label into a position in the code *)
+Fixpoint label_pos (lbl: label) (pos: Z) (lb: bblocks) {struct lb} : option Z :=
+  match lb with
+  | nil => None
+  | b :: lb' => if is_label lbl b then Some pos else label_pos lbl (pos + (size b)) lb'
+  end.
+
 Definition par_goto_label (f: function) (lbl: label) (rsr rsw: regset) (mw: mem) :=
   match label_pos lbl 0 (fn_blocks f) with
   | None => Stuck
@@ -182,7 +1230,7 @@ Definition par_goto_label (f: function) (lbl: label) (rsr rsw: regset) (mw: mem)
 Warning: in m PC is assumed to be already pointing on the next instruction !
 
 *)
-(* TODO: factoriser ? *)
+
 Definition par_eval_branch (f: function) (l: label) (rsr rsw: regset) (mw: mem) (res: option bool) :=
   match res with
     | Some true  => par_goto_label f l rsr rsw mw
@@ -191,6 +1239,8 @@ Definition par_eval_branch (f: function) (l: label) (rsr rsw: regset) (mw: mem)
   end.
 
 
+(* FIXME: comment not up-to-date for parallel semantics *)
+
 (** Execution of a single control-flow instruction [i] in initial state [rs] and
     [m].  Return updated state.
 
@@ -257,18 +1307,19 @@ Definition parexec_control (f: function) (oc: option control) (rsr rsw: regset)
 end.
 
 
-Definition parexec_wio_bblock_aux (f: function) bdy ext size_b (rsr rsw: regset) (mr mw: mem): outcome :=
+Definition incrPC size_b (rs: regset) :=
+  rs#PC <- (Val.offset_ptr rs#PC size_b).
+
+(** parallel execution of the exit instruction of a bundle *)
+Definition parexec_exit (f: function) ext size_b (rsr rsw: regset) (mw: mem) 
+  := parexec_control f ext (incrPC size_b rsr) rsw mw.
+
+Definition parexec_wio_bblock_aux f bdy ext size_b (rsr rsw: regset) (mr mw: mem): outcome :=
   match parexec_wio_body bdy rsr rsw mr mw with
-  | Next rsw mw =>
-    let rsr := par_nextblock size_b rsr in 
-    parexec_control f ext rsr rsw mw
+  | Next rsw mw => parexec_exit f ext size_b rsr rsw mw
   | Stuck => Stuck
   end.
 
-(** parallel in-order writes execution of bundles *)
-Definition parexec_wio_bblock (f: function) (b: bblock) (rs: regset) (m: mem): outcome :=
-  parexec_wio_bblock_aux f (body b) (exit b) (Ptrofs.repr (size b)) rs rs m m.
-
 (** non-deterministic (out-of-order writes) parallel execution of bundles *)
 Definition parexec_bblock (f: function) (bundle: bblock) (rs: regset) (m: mem) (o: outcome): Prop :=
    exists bdy1 bdy2, Permutation (bdy1++bdy2) (body bundle) /\ 
@@ -277,28 +1328,93 @@ Definition parexec_bblock (f: function) (bundle: bblock) (rs: regset) (m: mem) (
       | Stuck => Stuck
       end.
 
-Lemma parexec_bblock_write_in_order f b rs m:
-   parexec_bblock f b rs m (parexec_wio_bblock f b rs m).
-Proof.
-   exists (body b). exists nil.
-   constructor 1.
-   - rewrite app_nil_r; auto.
-   - unfold parexec_wio_bblock.
-     destruct (parexec_wio_bblock_aux f _ _ _ _ _); simpl; auto.
-Qed.
-
 (** deterministic parallel (out-of-order writes) execution of bundles *)
 Definition det_parexec (f: function) (bundle: bblock) (rs: regset) (m: mem) rs' m': Prop :=
    forall o, parexec_bblock f bundle rs m o -> o = Next rs' m'.
 
 
-Local Hint Resolve parexec_bblock_write_in_order.
+(* FIXME: comment not up-to-date *)
+(** 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 - R16 and R32 are excluded *)
+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  | R8  => GPR8  | 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 | R31 => GPR31 (* | 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.
+
+(** Undefine all registers except SP and callee-save registers *)
+
+Definition undef_caller_save_regs (rs: regset) : regset :=
+  fun r =>
+    if preg_eq r SP
+    || In_dec preg_eq r (List.map preg_of (List.filter is_callee_save all_mregs))
+    then rs r
+    else Vundef.
+
+(* FIXME: comment not up-to-date *)
+(** 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.
 
-Lemma det_parexec_write_in_order f b rs m rs' m':
-   det_parexec f b rs m rs' m' -> parexec_wio_bblock f b rs m = Next rs' m'.
-Proof.
-   unfold det_parexec; auto.
-Qed.
+
+Definition loc_external_result (sg: signature) : rpair preg :=
+  map_rpair preg_of (loc_result sg).
+
+
+(** Looking up bblocks in a code sequence by position. *)
+Fixpoint find_bblock (pos: Z) (lb: bblocks) {struct lb} : option bblock :=
+  match lb with
+  | nil => None
+  | b :: il => 
+    if zlt pos 0 then None  (* NOTE: It is impossible to branch inside a block *)
+    else if zeq pos 0 then Some b
+    else find_bblock (pos - (size b)) il
+  end.
+
+
+Inductive state: Type :=
+  | State: regset -> mem -> state.
+
+Definition nextblock (b:bblock) (rs: regset) :=
+  incrPC (Ptrofs.repr (size b)) rs.
 
 Inductive step: state -> trace -> state -> Prop :=
   | exec_step_internal:
@@ -331,10 +1447,54 @@ Inductive step: state -> trace -> state -> Prop :=
       step (State rs m) t (State rs' m')
   .
 
+
+(** parallel in-order writes execution of bundles *)
+Definition parexec_wio_bblock (f: function) (b: bblock) (rs: regset) (m: mem): outcome :=
+  parexec_wio_bblock_aux f (body b) (exit b) (Ptrofs.repr (size b)) rs rs m m.
+
+
+Lemma parexec_bblock_write_in_order f b rs m:
+   parexec_bblock f b rs m (parexec_wio_bblock f b rs m).
+Proof.
+   exists (body b). exists nil.
+   constructor 1.
+   - rewrite app_nil_r; auto.
+   - unfold parexec_wio_bblock.
+     destruct (parexec_wio_bblock_aux f _ _ _ _ _); simpl; auto.
+Qed.
+
+
+Local Hint Resolve parexec_bblock_write_in_order.
+
+Lemma det_parexec_write_in_order f b rs m rs' m':
+   det_parexec f b rs m rs' m' -> parexec_wio_bblock f b rs m = Next rs' m'.
+Proof.
+   unfold det_parexec; auto.
+Qed.
+
 End RELSEM.
 
 (** Execution of whole programs. *)
 
+(** 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).
 
@@ -402,4 +1562,4 @@ Ltac Det_WIO X :=
   inv H; rewrite H0 in *; eelim NOTNULL; eauto.
 - (* final states *)
   intros s r1 r2 H H0; inv H; inv H0. congruence.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml
index c4d8cd8d..9a26425a 100644
--- a/mppa_k1c/PostpassSchedulingOracle.ml
+++ b/mppa_k1c/PostpassSchedulingOracle.ml
@@ -1,3 +1,4 @@
+open Asmvliw
 open Asmblock
 open Printf
 open Camlcoq
@@ -7,7 +8,7 @@ open TargetPrinter.Target
 let debug = false
 
 (**
- * Extracting infos from Asmblock instructions
+ * Extracting infos from Asmvliw instructions
  *)
 
 type immediate = I32 of Integers.Int.int | I64 of Integers.Int64.int | Off of offset
@@ -22,7 +23,7 @@ type ab_inst_rec = {
   is_control : bool;
 }
 
-(** Asmblock constructor to string functions *)
+(** Asmvliw constructor to string functions *)
 
 exception OpaqueInstruction
 
diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v
index e0890a09..bc90dd4c 100644
--- a/mppa_k1c/PostpassSchedulingproof.v
+++ b/mppa_k1c/PostpassSchedulingproof.v
@@ -21,7 +21,7 @@ Require Import Axioms.
 
 Local Open Scope error_monad_scope.
 
-Definition match_prog (p tp: Asmblock.program) :=
+Definition match_prog (p tp: Asmvliw.program) :=
   match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp.
 
 Lemma transf_program_match:
@@ -100,7 +100,7 @@ Lemma exec_load_offset_pc_var:
   exec_load_offset ge t rs m rd ra ofs = Next rs' m' ->
   exec_load_offset ge t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'.
 Proof.
-  intros. unfold exec_load_offset in *. rewrite Pregmap.gso; try discriminate. destruct (eval_offset ge ofs); try discriminate.
+  intros. unfold exec_load_offset in *. unfold parexec_load_offset in *. rewrite Pregmap.gso; try discriminate. destruct (eval_offset ge ofs); try discriminate.
   destruct (Mem.loadv _ _ _).
   - inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate.
   - discriminate.
@@ -111,7 +111,7 @@ Lemma exec_load_reg_pc_var:
   exec_load_reg t rs m rd ra ro = Next rs' m' ->
   exec_load_reg t rs # PC <- v m rd ra ro = Next rs' # PC <- v m'.
 Proof.
-  intros. unfold exec_load_reg in *. rewrite Pregmap.gso; try discriminate.
+  intros. unfold exec_load_reg in *. unfold parexec_load_reg in *. rewrite Pregmap.gso; try discriminate.
   destruct (Mem.loadv _ _ _).
   - inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate.
   - discriminate.
@@ -122,7 +122,7 @@ Lemma exec_store_offset_pc_var:
   exec_store_offset ge t rs m rd ra ofs = Next rs' m' ->
   exec_store_offset ge t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'.
 Proof.
-  intros. unfold exec_store_offset in *. rewrite Pregmap.gso; try discriminate.
+  intros. unfold exec_store_offset in *. unfold parexec_store_offset in *. rewrite Pregmap.gso; try discriminate.
   destruct (eval_offset ge ofs); try discriminate.
   destruct (Mem.storev _ _ _).
   - inv H. apply next_eq; auto.
@@ -134,7 +134,7 @@ Lemma exec_store_reg_pc_var:
   exec_store_reg t rs m rd ra ro = Next rs' m' ->
   exec_store_reg t rs # PC <- v m rd ra ro = Next rs' # PC <- v m'.
 Proof.
-  intros. unfold exec_store_reg in *. rewrite Pregmap.gso; try discriminate.
+  intros. unfold exec_store_reg in *. unfold parexec_store_reg in *. rewrite Pregmap.gso; try discriminate.
   destruct (Mem.storev _ _ _).
   - inv H. apply next_eq; auto.
   - discriminate.
@@ -145,13 +145,13 @@ Lemma exec_basic_instr_pc_var:
   exec_basic_instr ge i rs m = Next rs' m' ->
   exec_basic_instr ge i (rs # PC <- v) m = Next (rs' # PC <- v) m'.
 Proof.
-  intros. unfold exec_basic_instr in *. destruct i.
+  intros. unfold exec_basic_instr in *. unfold parexec_basic_instr in *. destruct i.
   - unfold exec_arith_instr in *. destruct i; destruct i.
       all: try (exploreInst; inv H; apply next_eq; auto;
       apply functional_extensionality; intros; rewrite regset_double_set; auto; discriminate).
-
+(* 
       (* Some cases treated seperately because exploreInst destructs too much *)
-      all: try (inv H; apply next_eq; auto; apply functional_extensionality; intros; rewrite regset_double_set; auto; discriminate).
+      all: try (inv H; apply next_eq; auto; apply functional_extensionality; intros; rewrite regset_double_set; auto; discriminate). *)
   - destruct i.
     + exploreInst; apply exec_load_offset_pc_var; auto.
     + exploreInst; apply exec_load_reg_pc_var; auto.
@@ -223,10 +223,11 @@ Proof.
   exploit concat2_decomp; eauto. intros. inv H.
   unfold exec_bblock in EXEB. destruct (exec_body ge (body bb) rs m) eqn:EXEB'; try discriminate.
   rewrite H0 in EXEB'. apply exec_body_app in EXEB'. destruct EXEB' as (rs1 & m1 & EXEB1 & EXEB2).
-  repeat eexists.
+  eexists; eexists. split.
     unfold exec_bblock. rewrite EXEB1. rewrite EXA. simpl. eauto.
+  split.
     exploit exec_body_pc. eapply EXEB1. intros. rewrite <- H. auto.
-    unfold exec_bblock. unfold nextblock. erewrite exec_body_pc_var; eauto.
+    unfold exec_bblock. unfold nextblock, incrPC. rewrite regset_same_assign. erewrite exec_body_pc_var; eauto.
     rewrite <- H1. unfold nextblock in EXEB. rewrite regset_double_set_id.
     assert (size bb = size a + size b).
     { unfold size. rewrite H0. rewrite H1. rewrite app_length. rewrite EXA. simpl. rewrite Nat.add_0_r.
@@ -234,8 +235,8 @@ Proof.
     clear EXA H0 H1. rewrite H in EXEB.
     assert (rs1 PC = rs0 PC). { apply exec_body_pc in EXEB2. auto. }
     rewrite H0. rewrite <- pc_set_add; auto.
-    exploit AB.size_positive. instantiate (1 := a). intro. omega.
-    exploit AB.size_positive. instantiate (1 := b). intro. omega.
+    exploit size_positive. instantiate (1 := a). intro. omega.
+    exploit size_positive. instantiate (1 := b). intro. omega.
 Qed.
 
 Lemma concat_all_exec_bblock (ge: Genv.t fundef unit) (f: function) :
@@ -571,13 +572,8 @@ Proof.
   assert (ge = Genv.globalenv prog). auto.
   assert (tge = Genv.globalenv tprog). auto.
   pose symbol_address_preserved.
-  exploreInst; simpl; auto; try congruence.
-  - unfold goto_label. erewrite label_pos_preserved_blocks; eauto.
-  - unfold eval_branch. unfold goto_label. erewrite label_pos_preserved_blocks; eauto.
-  - unfold eval_branch. unfold goto_label. erewrite label_pos_preserved_blocks; eauto.
-  - unfold eval_branch. unfold goto_label. erewrite label_pos_preserved_blocks; eauto.
-  - unfold eval_branch. unfold goto_label. erewrite label_pos_preserved_blocks; eauto.
-  - unfold eval_branch. unfold goto_label. erewrite label_pos_preserved_blocks; eauto.
+  exploreInst; simpl; auto; try congruence;
+    unfold par_goto_label; unfold par_eval_branch; unfold par_goto_label; erewrite label_pos_preserved_blocks; eauto.
 Qed.
 
 Lemma eval_offset_preserved:
@@ -589,21 +585,21 @@ Qed.
 Lemma transf_exec_load_offset:
   forall t rs m rd ra ofs, exec_load_offset ge t rs m rd ra ofs = exec_load_offset tge t rs m rd ra ofs.
 Proof.
-  intros. unfold exec_load_offset. rewrite eval_offset_preserved. reflexivity.
+  intros. unfold exec_load_offset. unfold parexec_load_offset. rewrite eval_offset_preserved. reflexivity.
 Qed.
 
 Lemma transf_exec_store_offset:
   forall t rs m rs0 ra ofs, exec_store_offset ge t rs m rs0 ra ofs = exec_store_offset tge t rs m rs0 ra ofs.
 Proof.
-  intros. unfold exec_store_offset. rewrite eval_offset_preserved. reflexivity.
+  intros. unfold exec_store_offset. unfold parexec_store_offset. rewrite eval_offset_preserved. reflexivity.
 Qed.
 
 Lemma transf_exec_basic_instr:
   forall i rs m, exec_basic_instr ge i rs m = exec_basic_instr tge i rs m.
 Proof.
   intros. pose symbol_address_preserved.
-  unfold exec_basic_instr. exploreInst; simpl; auto; try congruence.
-  - unfold exec_arith_instr; unfold arith_eval_r; exploreInst; simpl; auto; try congruence.
+  unfold exec_basic_instr. unfold parexec_basic_instr. exploreInst; simpl; auto; try congruence.
+  - unfold parexec_arith_instr; unfold arith_eval_r; exploreInst; simpl; auto; try congruence.
   - apply transf_exec_load_offset.
   - apply transf_exec_store_offset.
 Qed.
@@ -731,9 +727,9 @@ Proof.
   destruct bb as [h bdy ext H]; simpl.
   intros; subst. destruct i.
   generalize H.
-  rewrite <- AB.wf_bblock_refl in H.
+  rewrite <- wf_bblock_refl in H.
   destruct H as [H H0].
-  unfold AB.builtin_alone in H0. erewrite H0; eauto.
+  unfold builtin_alone in H0. erewrite H0; eauto.
 Qed.
 
 Local Hint Resolve verified_schedule_nob_checks_alls_bundles.
@@ -826,7 +822,7 @@ Qed.
 Theorem transf_program_correct_Asmvliw: 
   forward_simulation (Asmblock.semantics tprog) (Asmvliw.semantics tprog).
 Proof.
-  eapply forward_simulation_step with (match_states:=fun (s1:Asmblock.state) s2 => s1=s2); eauto.
+  eapply forward_simulation_step with (match_states:=fun (s1:Asmvliw.state) s2 => s1=s2); eauto.
   - intros; subst; auto.
   - intros s1 t s1' H s2 H0; subst; inversion H; clear H; subst; eexists; split; eauto.
     + eapply exec_step_internal; eauto.
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index 6f292460..3aa6b319 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -40,7 +40,7 @@ module Target (*: TARGET*) =
 
     let print_label oc lbl = label oc (transl_label lbl)
 
-    let int_reg_name = let open Asmblock in function
+    let int_reg_name = let open Asmvliw in function
       | GPR0  -> "$r0"  | GPR1  -> "$r1"  | GPR2  -> "$r2"  | GPR3  -> "$r3"
       | GPR4  -> "$r4"  | GPR5  -> "$r5"  | GPR6  -> "$r6"  | GPR7  -> "$r7"
       | GPR8  -> "$r8"  | GPR9  -> "$r9"  | GPR10 -> "$r10" | GPR11 -> "$r11"
@@ -62,12 +62,12 @@ module Target (*: TARGET*) =
 
     let ireg = ireg
 
-    let preg oc = let open Asmblock in function
+    let preg oc = let open Asmvliw in function
       | IR r -> ireg oc r
       | RA   -> output_string oc "$ra"
       | _ -> assert false
 
-    let preg_annot = let open Asmblock in function
+    let preg_annot = let open Asmvliw in function
       | IR r -> int_reg_name r
       | RA   -> "$ra"
       | _ -> assert false
@@ -160,7 +160,7 @@ module Target (*: TARGET*) =
   *)
 (* Offset part of a load or store *)
 
-    let offset oc = let open Asmblock in function
+    let offset oc = let open Asmvliw in function
     | Ofsimm n -> ptrofs oc n
     | Ofslow(id, ofs) -> fprintf oc "%%lo(%a)" symbol_offset (id, ofs)
 
@@ -168,7 +168,7 @@ module Target (*: TARGET*) =
     | AOff ofs -> offset oc ofs
     | AReg ro -> ireg oc ro
 
-    let icond_name = let open Asmblock in function
+    let icond_name = let open Asmvliw in function
       | ITne | ITneu -> "ne"
       | ITeq | ITequ -> "eq"
       | ITlt   -> "lt"
@@ -186,7 +186,7 @@ module Target (*: TARGET*) =
 
     let icond oc c = fprintf oc "%s" (icond_name c)
 
-    let fcond_name = let open Asmblock in function
+    let fcond_name = let open Asmvliw in function
       | FTone -> "one"
       | FTueq -> "ueq"
       | FToeq -> "oeq"
@@ -198,7 +198,7 @@ module Target (*: TARGET*) =
 
     let fcond oc c = fprintf oc "%s" (fcond_name c)
   
-    let bcond_name = let open Asmblock in function
+    let bcond_name = let open Asmvliw in function
       | BTwnez -> "wnez"
       | BTweqz -> "weqz"
       | BTwltz -> "wltz"
@@ -279,7 +279,7 @@ module Target (*: TARGET*) =
       | Pjumptable (idx_reg, tbl) ->
          let lbl = new_label() in
          (* jumptables := (lbl, tbl) :: !jumptables; *)
-         let base_reg = if idx_reg=Asmblock.GPR63 then Asmblock.GPR62 else Asmblock.GPR63 in
+         let base_reg = if idx_reg=Asmvliw.GPR63 then Asmvliw.GPR62 else Asmvliw.GPR63 in
          fprintf oc "%s jumptable [ " comment;
          List.iter (fun l -> fprintf oc "%a " print_label l) tbl;
          fprintf oc "]\n";
diff --git a/mppa_k1c/lib/Asmblockgenproof0.v b/mppa_k1c/lib/Asmblockgenproof0.v
index d0e05389..eb336edc 100644
--- a/mppa_k1c/lib/Asmblockgenproof0.v
+++ b/mppa_k1c/lib/Asmblockgenproof0.v
@@ -14,9 +14,10 @@ Require Import Machblock.
 Require Import Asmblock.
 Require Import Asmblockgen.
 Require Import Conventions1.
+Require Import Axioms.
 
 Module MB:=Machblock.
-Module AB:=Asmblock.
+Module AB:=Asmvliw.
 
 Hint Extern 2 (_ <> _) => congruence: asmgen.
 
@@ -311,9 +312,9 @@ Qed.
 Lemma agree_undef_caller_save_regs:
   forall ms sp rs,
   agree ms sp rs ->
-  agree (Mach.undef_caller_save_regs ms) sp (Asmblock.undef_caller_save_regs rs).
+  agree (Mach.undef_caller_save_regs ms) sp (Asmvliw.undef_caller_save_regs rs).
 Proof.
-  intros. destruct H. unfold Mach.undef_caller_save_regs, Asmblock.undef_caller_save_regs; split.
+  intros. destruct H. unfold Mach.undef_caller_save_regs, Asmvliw.undef_caller_save_regs; split.
 - unfold proj_sumbool; rewrite dec_eq_true. auto.
 - auto.
 - intros. unfold proj_sumbool. rewrite dec_eq_false by (apply preg_of_not_SP). 
@@ -943,10 +944,10 @@ Lemma exec_basic_instr_pc:
 Proof.
   intros. destruct b; try destruct i; try destruct i.
   all: try (inv H; Simpl).
-  1-10: try (unfold exec_load_offset in H1; destruct (eval_offset ge ofs); try discriminate; destruct (Mem.loadv _ _ _); [inv H1; Simpl | discriminate]).
-  1-10: try (unfold exec_load_reg in H1; destruct (Mem.loadv _ _ _); [inv H1; Simpl | discriminate]).
-  1-10: try (unfold exec_store_offset in H1; destruct (eval_offset ge ofs); try discriminate; destruct (Mem.storev _ _ _); [inv H1; auto | discriminate]).
-  1-10: try (unfold exec_store_reg in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]); auto.
+  1-10: try (unfold parexec_load_offset in H1; destruct (eval_offset ge ofs); try discriminate; destruct (Mem.loadv _ _ _); [inv H1; Simpl | discriminate]).
+  1-10: try (unfold parexec_load_reg in H1; destruct (Mem.loadv _ _ _); [inv H1; Simpl | discriminate]).
+  1-10: try (unfold parexec_store_offset in H1; destruct (eval_offset ge ofs); try discriminate; destruct (Mem.storev _ _ _); [inv H1; auto | discriminate]).
+  1-10: try (unfold parexec_store_reg in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]); auto.
   - destruct (Mem.alloc _ _ _). destruct (Mem.store _ _ _ _ _). inv H1. Simpl. discriminate.
   - destruct (Mem.loadv _ _ _); try discriminate. destruct (rs1 _); try discriminate.
     destruct (Mem.free _ _ _ _). inv H1. Simpl. discriminate.
@@ -997,6 +998,13 @@ Proof.
     + rewrite <- (exec_straight_pc (i ::i c) nil rs1 m1 rs2 m2'); auto.
 Qed.
  *)
+
+Lemma regset_same_assign (rs: regset) r:
+  rs # r <- (rs r) = rs.
+Proof.
+  apply functional_extensionality. intros x. destruct (preg_eq x r); subst; Simpl.
+Qed.
+
 Lemma exec_straight_through_singleinst:
   forall a b rs1 m1 rs2 m2 rs2' m2' lb,
   bblock_single_inst (PBasic a) = b ->
@@ -1005,10 +1013,12 @@ Lemma exec_straight_through_singleinst:
   exec_straight_blocks (b::lb) rs1 m1 lb rs2' m2'.
 Proof.
   intros. subst. constructor 1. unfold exec_bblock. simpl body. erewrite exec_straight_body; eauto.
-  simpl. auto.
-  simpl; auto. unfold nextblock; simpl. Simpl. erewrite exec_straight_pc; eauto.
+  simpl. rewrite regset_same_assign. auto.
+  simpl; auto. unfold nextblock, incrPC; simpl. Simpl. erewrite exec_straight_pc; eauto.
 Qed.
 
+
+
 (** The following lemmas show that straight-line executions
   (predicate [exec_straight_blocks]) correspond to correct Asm executions. *)