Changeset 2286 for src/RTLabs


Ignore:
Timestamp:
Aug 2, 2012, 3:18:11 PM (7 years ago)
Author:
tranquil
Message:

Big update!

  • merge of all _paolo variants
  • reorganised some depends (in particular, Register and thus back-end laguages no longer have fake ASM dependency)
  • split I8051.ma spawning new BackEndOps?.ma

compiler.ma broken at the moment, but not by these changes as far as I can tell

Location:
src/RTLabs
Files:
1 deleted
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabsToRTL.ma

    r2176 r2286  
    55include "common/Graphs.ma".
    66include "joint/TranslateUtils.ma".
     7include "utilities/bindLists.ma".
    78include alias "ASM/BitVector.ma".
    89include alias "arithmetics/nat.ma".
    910
    10 let rec register_freshes (runiverse: universe RegisterTag) (n: nat) on n ≝
    11   match n with
    12   [ O ⇒ 〈[],runiverse〉
    13   | S n' ⇒
    14      let 〈r,runiverse〉 ≝ fresh … runiverse in
    15      let 〈res,runiverse〉 ≝ register_freshes runiverse n' in
    16       〈r::res,runiverse〉 ].
    17 
    18 definition complete_regs ≝
    19   λglobals.
    20   λdef.
    21   λsrcrs1.
    22   λsrcrs2.
    23   if leb (length … srcrs2) (length … srcrs1) then
    24    let 〈def, added_regs〉 ≝ fresh_regs rtl_params0 globals def (minus (length ? srcrs1) (length ? srcrs2)) in
    25     〈〈srcrs1, srcrs2 @ added_regs〉, added_regs〉
    26   else
    27    let 〈def, added_regs〉 ≝ fresh_regs rtl_params0 globals def (minus (length ? srcrs2) (length ? srcrs1)) in
    28     〈〈srcrs1 @ added_regs, srcrs2〉, added_regs〉.
    29 
    30 lemma complete_regs_length:
    31   ∀globals,def,left,right.
    32    |\fst (\fst (complete_regs globals def left right))| = |\snd (\fst (complete_regs globals def left right))|.
    33  #globals #def #left #right
    34  whd in match complete_regs; normalize nodelta
    35  @leb_elim normalize nodelta #H
    36  [ generalize in match (fresh_regs_length rtl_params0 globals def (minus (length … left) (length … right)));
    37  | generalize in match (fresh_regs_length rtl_params0 globals def (minus (length … right) (length … left)));]
    38  cases (fresh_regs ????) #def' #fresh normalize >append_length
    39  generalize in match H; -H;
    40  generalize in match (length … left); generalize in match (length … right); generalize in match (length … fresh);
    41  [ /2/ | #x #y #z #H generalize in match (not_le_to_lt … H); -H #H #E >E >commutative_plus
    42          <plus_minus_m_m /2/ ]
    43 qed.
     11definition rtl_fresh_reg:
     12 ∀globals.freshT RTL globals register ≝
     13  λglobals,def.
     14    let 〈r, runiverse〉 ≝ fresh … (joint_if_runiverse … def) in
     15    〈set_locals ?? (set_runiverse ?? def runiverse)(r::joint_if_locals ?? def), r〉.
     16
     17definition rtl_fresh_reg_no_local :
     18 ∀globals.freshT RTL globals register ≝
     19  λglobals,def.
     20    let 〈r, runiverse〉 ≝ fresh … (joint_if_runiverse … def) in
     21    〈set_runiverse ?? def runiverse, r〉.
    4422
    4523definition size_of_sig_type ≝
     
    4725  match sig with
    4826  [ ASTint isize sign ⇒
    49     let isize' ≝ match isize with [ I8 ⇒ 8 | I16 ⇒ 16 | I32 ⇒ 32 ] in
    50       isize' ÷ (nat_of_bitvector ? int_size)
     27    match isize with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4 ]
    5128  | ASTfloat _ ⇒ ? (* dpm: not implemented *)
    52   | ASTptr ⇒ nat_of_bitvector ? ptr_size
    53   ].
    54   cases not_implemented;
     29  | ASTptr ⇒ 2 (* rgn ⇒ nat_of_bitvector ? ptr_size *)
     30  ].
     31  cases not_implemented
    5532qed.
    5633
     
    6138definition local_env ≝ identifier_map RegisterTag (list register).
    6239
    63 definition mem_local_env : register → local_env → bool ≝
    64   λr,e. member … e r.
    65 
    66 definition add_local_env : register → list register → local_env → local_env ≝
    67   λr,v,e. add … e r v.
    68 
    69 definition find_local_env : register → local_env → list register ≝
    70   λr: register.λenv. lookup_def … env r [].
    71 
    72 definition initialize_local_env_internal ≝
    73   λlenv_runiverse.
    74   λr_sig.
    75   let 〈lenv,runiverse〉 ≝ lenv_runiverse in
     40definition local_env_typed :
     41  list (register × typ) → local_env → Prop ≝
     42  λl,env.All ?
     43    (λp.let 〈r, ty〉 ≝ p in ∃regs.lookup … env r = Some ? regs ∧
     44                                 |regs| = size_of_sig_type ty) l.
     45
     46definition find_local_env ≝ λr.λlenv : local_env.
     47  λprf : r ∈ lenv.opt_safe … (lookup … lenv r) ?.
     48lapply (in_map_domain … lenv r)
     49>prf * #x #lookup_eq >lookup_eq % #ABS destruct(ABS)
     50qed.
     51
     52lemma find_local_env_elim : ∀P : list register → Prop.∀r. ∀lenv: local_env.∀prf.
     53  (∀x.lookup … lenv r = Some ? x → P x) → P (find_local_env r lenv prf).
     54#P#r#lenv#prf #H
     55change with (P (opt_safe ???))
     56@opt_safe_elim assumption
     57qed.
     58
     59definition find_local_env_arg : register → local_env → ? → list psd_argument ≝
     60  λr,lenv,prf. map … (Reg ?) (find_local_env r lenv prf).
     61
     62definition initialize_local_env_internal :
     63  ∀globals.
     64  ((joint_internal_function RTL globals) × local_env) → (register×typ) →
     65  ((joint_internal_function RTL globals) × local_env) ≝
     66  λglobals,def_env,r_sig.
     67  let 〈def,lenv〉 ≝ def_env in
    7668  let 〈r, sig〉 ≝ r_sig in
    7769  let size ≝ size_of_sig_type sig in
    78   let 〈rs,runiverse〉 ≝ register_freshes runiverse size in
    79     〈add_local_env r rs lenv,runiverse〉.
    80 
    81 definition initialize_local_env ≝
    82   λruniverse.
    83   λregisters.
    84   λresult.
    85   let registers ≝ registers @
    86     match result with
    87     [ None ⇒ [ ]
    88     | Some rt ⇒ [ rt ]
     70  let 〈def,rs〉 ≝ repeat_fresh … (rtl_fresh_reg_no_local globals) size def in
     71    〈def,add … lenv r rs〉.
     72
     73include alias "common/Identifiers.ma".
     74let rec map_list_local_env
     75  lenv (regs : list (register×typ)) on regs :
     76  All ? (λpr.bool_to_Prop (\fst pr ∈ lenv)) regs → list register ≝
     77  match regs return λx.All ?? x → ? with
     78  [ nil ⇒ λ_.[ ]
     79  | cons hd tl ⇒ λprf.find_local_env (\fst hd) lenv ? @ map_list_local_env lenv tl ?
     80  ].cases prf #A #B assumption qed.
     81
     82definition initialize_local_env :
     83  ∀globals.
     84  list (register×typ) →
     85  freshT RTL globals local_env ≝
     86  λglobals,registers,def.
     87  foldl ?? (initialize_local_env_internal globals) 〈def,empty_map …〉 registers.
     88
     89lemma initialize_local_env_in : ∀globals,l,def,r.
     90  Exists ? (λx.\fst x = r) l → r ∈ \snd (initialize_local_env globals l def).
     91#globals #l #U #r @(list_elim_left … l)
     92[ *
     93| * #tl #sig #hd #IH #G elim (Exists_append … G) -G
     94  whd in match initialize_local_env; normalize nodelta
     95  >foldl_step change with (initialize_local_env ???) in match (foldl ?????);
     96  [ #H lapply (IH H)
     97  | * [2: *] #EQ destruct(EQ)
     98  ] 
     99  cases (initialize_local_env ???)
     100  #U' #env' [#G] whd in match initialize_local_env_internal; normalize nodelta
     101  elim (repeat_fresh ??????) #U'' #rs
     102  [ >mem_set_add @orb_Prop_r assumption
     103  | @mem_set_add_id
     104  ]
     105qed.
     106
     107example proj1_rewrite : ∀A,B,a,b.∀pr : A×B.〈a,b〉 = pr → a = \fst pr.
     108// qed-.
     109example proj2_rewrite : ∀A,B,a,b.∀pr : A×B.〈a,b〉 = pr → b = \snd pr.
     110// qed-.
     111
     112definition initialize_locals_params_ret :
     113  ∀globals.
     114  (* locals *) list (register×typ) →
     115  (* params *) list (register×typ) →
     116  (* return *) option (register×typ) →
     117  freshT RTL globals local_env ≝
     118  λglobals,locals,params,ret,def.
     119  let 〈def',lenv〉 as EQ ≝
     120    initialize_local_env globals
     121    ((match ret with
     122     [ Some r_sig ⇒ [r_sig]
     123     | None ⇒ [ ]
     124     ]) @ locals @ params) def in
     125  let locals' ≝ map_list_local_env lenv locals ? in
     126  let params' ≝ map_list_local_env lenv params ? in
     127  let ret' ≝ match ret return λx.ret = x → ? with
     128    [ Some r_sig ⇒ λprf.find_local_env (\fst r_sig) lenv ?
     129    | None ⇒ λ_.[ ]
     130    ] (refl …) in
     131  let def'' ≝
     132    mk_joint_internal_function RTL globals
     133      (joint_if_luniverse … def') (joint_if_runiverse … def') ret'
     134      params' locals' (joint_if_stacksize … def')
     135      (joint_if_code … def') (joint_if_entry … def') (joint_if_exit … def') in
     136   〈def'', lenv〉. @hide_prf
     137[ >(proj2_rewrite ????? EQ)
     138  @initialize_local_env_in >prf %1 %
     139|*: >(proj2_rewrite ????? EQ)
     140  @(All_mp ??? (λpr.initialize_local_env_in ??? (\fst pr)))
     141  [ @(All_mp … (λpr.Exists ? (λx.\fst x = \fst pr) params))
     142    [ #a #H @Exists_append_r @Exists_append_r @H
     143    | generalize in match params;
    89144    ]
    90   in
    91     foldl … initialize_local_env_internal 〈empty_map …,runiverse〉 registers.
    92 
    93 definition map_list_local_env_internal ≝
    94   λlenv,res,r. res @ (find_local_env r lenv).
    95    
    96 definition map_list_local_env ≝
    97   λlenv,regs. foldl … (map_list_local_env_internal lenv) [ ] regs.
     145  | @(All_mp … (λpr.Exists ? (λx.\fst x = \fst pr) locals))
     146    [ #a #H @Exists_append_r @Exists_append_l @H
     147    | generalize in match locals;
     148    ]
     149  ]
     150  #l elim l [1,3: %] #hd #tl #IH % [1,3: %1 %] @(All_mp … IH) #x #G %2{G}
     151]
     152qed.
    98153
    99154definition make_addr ≝
    100155  λA.
    101156  λlst: list A.
    102   λprf: 2 = length A lst.
    103   match lst return λx. 2 = |x| → A × A with
    104   [ nil ⇒ λlst_nil_prf. ?
    105   | cons hd tl ⇒ λprf.
    106     match tl return λx. 1 = |x| → A × A with
    107     [ nil ⇒ λtl_nil_prf. ?
    108     | cons hd' tl' ⇒ λtl_cons_prf. 〈hd, hd'〉
    109     ] ?
    110   ] prf.
    111   [1: normalize in lst_nil_prf;
    112       destruct(lst_nil_prf)
    113   |2: normalize in prf;
    114       @injective_S
    115       assumption
    116   |3: normalize in tl_nil_prf;
    117       destruct(tl_nil_prf)
    118   ]
    119 qed.
     157  λprf: 2 = length A lst.〈nth_safe … 0 lst ?, nth_safe … 1 lst ?〉. <prf //
     158  qed.
    120159
    121160definition find_and_addr ≝
    122   λr,lenv. make_addr ? (find_local_env r lenv).
    123 
    124 definition rtl_args ≝
    125   λregs_list,lenv. flatten … (map … (λr. find_local_env r lenv) regs_list).
    126 
    127 definition translate_cst_int_internal ≝
    128   λglobals,dest_lbl,r,i. sequential rtl_params_ globals (INT … r i) dest_lbl.
     161  λr,lenv,prf. make_addr ? (find_local_env r lenv prf).
     162
     163include alias "common/Identifiers.ma".
     164let rec rtl_args (args : list register) (env : local_env) on args :
     165  All ? (λr.bool_to_Prop (r∈env)) args → list psd_argument ≝
     166  match args return λx.All ?? x → ? with
     167  [ nil ⇒ λ_.[ ]
     168  | cons hd tl ⇒ λprf.find_local_env_arg hd env ? @ rtl_args tl env ?
     169  ].
     170  cases prf #H #G assumption
     171  qed.
     172
     173include alias "basics/lists/list.ma".
     174let rec vrsplit A (m,n : nat)
     175  on m : Vector A (m*n) → Σs : list (Vector A n).|s| = m ≝
     176  match m return λx.Vector A (x*n) → Sig (list ?) ? with
     177  [ O ⇒ λv.[ ]
     178  | S k ⇒ λv.let spl ≝ vsplit ? n … v in \fst spl :: vrsplit ? k n (\snd spl)
     179  ].
     180  [ %
     181  | cases (vrsplit ????) #lst #EQ normalize >EQ %
     182  ] qed.
    129183
    130184definition split_into_bytes:
    131185  ∀size. ∀int: bvint size. Σbytes: list Byte. |bytes| = size_intsize size ≝
    132 λsize.
    133  match size return λsize.∀int: bvint size. Σbytes. |bytes| = size_intsize size with
    134   [ I8 ⇒ λint. ? | I16 ⇒ λint. ? | I32 ⇒ λint. ? ].
    135 [ %[@[int]] //
    136 | %[@(let 〈h,l〉 ≝ vsplit ? 8 … int in [l;h])] cases (vsplit ????) //
    137 | %[@(let 〈h1,l〉 ≝ vsplit ? 8 … int in
    138       let 〈h2,l〉 ≝ vsplit ? 8 … l in
    139       let 〈h3,l〉 ≝ vsplit ? 8 … l in
    140        [l;h3;h2;h1])]
    141   cases (vsplit ????) #h1 #l normalize
    142   cases (vsplit ????) #h2 #l normalize
    143   cases (vsplit ????) // ]
    144 qed.
    145 
    146 lemma eqb_implies_eq:
    147   ∀m, n: nat.
    148     eqb m n = true → m = n.
    149   #M
    150   elim M
    151   [1: #N normalize
    152       cases N
    153       [1: normalize //
    154       |2: #M' normalize #HYP destruct(HYP)
    155       ]
    156   |2: #M' #IND_HYP #N
    157       normalize
    158       cases N
    159       [1: normalize #HYP destruct(HYP)
    160       |2: #M'' normalize #HYP
    161           @eq_f @(IND_HYP M'')
    162           assumption
    163       ]
    164    ]
    165 qed.
    166 
    167 definition translate_op: ∀globals. ? → list register → list register → list register →
    168   label → label → rtl_internal_function globals → rtl_internal_function globals ≝
     186λsize.vrsplit ? (size_intsize size) 8.
     187
     188let rec list_inject_All_aux A P (l : list A) on l : All A P l → list (Σx.P x) ≝
     189match l return λx.All A P x → ? with
     190[ nil ⇒ λ_.[ ]
     191| cons hd tl ⇒ λprf.«hd, ?» :: list_inject_All_aux A P tl ?
     192]. cases prf #H1 #H2 [@H1 | @H2]
     193qed.
     194
     195include alias "basics/lists/list.ma".
     196definition translate_op:
     197  ∀globals. Op2 →
     198  ∀dests : list register.
     199  ∀srcrs1 : list psd_argument.
     200  ∀srcrs2 : list psd_argument.
     201  |dests| = |srcrs1| → |srcrs1| = |srcrs2| →
     202  list (joint_seq RTL globals)
     203  ≝
    169204  λglobals: list ident.
    170205  λop.
    171   λdestrs: list register.
    172   λsrcrs1: list register.
    173   λsrcrs2: list register.
    174   λstart_lbl: label.
    175   λdest_lbl: label.
    176   λdef: rtl_internal_function globals.
    177   match reduce_strong register register srcrs1 srcrs2 with
    178   [ mk_Sig reduced first_reduced_proof ⇒
    179     let srcrsl_common ≝ \fst (\fst reduced) in
    180     let srcrsr_common ≝ \fst (\snd reduced) in
    181     let srcrsl_rest ≝ \snd (\fst reduced) in
    182     let srcrsr_rest ≝ \snd (\snd reduced) in
    183     let srcrs_rest ≝ srcrsl_rest @ srcrsr_rest in
    184     match reduce_strong register register destrs srcrsl_common with
    185     [ mk_Sig reduced second_reduced_proof ⇒
    186       let destrs_common ≝ \fst (\fst reduced) in
    187       let destrs_rest ≝ \snd (\fst reduced) in
    188       match reduce_strong register register destrs_rest srcrs_rest with
    189       [ mk_Sig reduced third_reduced_proof ⇒
    190         let destrs_cted ≝ \fst (\fst reduced) in
    191         let destrs_rest ≝ \snd (\fst reduced) in
    192         let srcrs_cted ≝ \fst (\snd reduced) in
    193         let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
    194         let insts_init ≝ [
    195           sequential … (CLEAR_CARRY …);
    196           sequential … (INT rtl_params_ globals tmpr (zero …))
    197         ] in
    198         let f_add ≝ λdestr. λsrcr1. λsrcr2. sequential … (OP2 rtl_params_ globals op destr srcr1 srcr2) in
    199         let insts_add ≝ map3 ? ? ? ? f_add destrs_common srcrsl_common srcrsr_common ? ? in
    200         let f_add_cted ≝ λdestr. λsrcr. sequential … (OP2 rtl_params_ globals op destr srcr tmpr) in
    201         let insts_add_cted ≝ map2 … f_add_cted destrs_cted srcrs_cted ? in
    202         let f_rest ≝ λdestr. sequential … (OP2 rtl_params_ globals op destr tmpr tmpr) in
    203         let insts_rest ≝ map … f_rest destrs_rest in
    204           adds_graph rtl_params1 globals (insts_init @ insts_add @ insts_add_cted @ insts_rest) start_lbl dest_lbl def
    205       ]
    206     ]
    207   ].
    208   [1: @third_reduced_proof
    209   |3: @first_reduced_proof
    210   |*: cases daemon (* XXX: some of these look like they may be false *)
    211   ]
    212 qed.
    213 
    214 (* Type safety in RTLabs has broken this for the moment...
    215 let rec translate_cst
    216   (globals: list ident) (cst: constant) (destrs: list register)
    217     (start_lbl: label) (dest_lbl: label) (def: rtl_internal_function globals)
    218       on cst: rtl_internal_function globals ≝
    219   match cst with
    220   [ Ointconst size const ⇒
    221     match destrs with
    222     [ nil ⇒ add_graph … start_lbl (GOTO … dest_lbl) def
    223     | _   ⇒
    224       let size' ≝ size_intsize size in
    225         match eqb size' (|destrs|) return λx. (eqb size' (|destrs|)) = x → rtl_internal_function globals with
    226         [ true  ⇒ λgood_case.
    227           match split_into_bytes size const with
    228           [ mk_Sig bytes bytes_length_proof ⇒
    229             let mapped ≝ map2 … (λd. λb. (sequential … (INT rtl_params_ globals d b))) destrs bytes ? in
    230               adds_graph rtl_params1 globals mapped start_lbl dest_lbl def
    231           ]
    232         | false ⇒ λbad_case. ?
    233         ] (refl … (eqb size' (|destrs|)))
    234     ]
    235   | Ofloatconst float ⇒ ⊥
    236   | Oaddrsymbol id offset ⇒
    237     let 〈r1, r2〉 ≝ make_addr … destrs ? in
    238     let def ≝ add_graph rtl_params1 globals start_lbl (sequential … (ADDRESS rtl_params_ globals id ? r1 r2) dest_lbl) def in
    239     let def ≝ translate_op globals Addc [r1] [r1] [r2] start_lbl dest_lbl def in
    240       def
    241   | Oaddrstack offset ⇒
    242     let 〈r1, r2〉 ≝ make_addr … destrs ? in
    243     let def ≝ add_graph rtl_params1 globals start_lbl (sequential … (extension rtl_params_ globals (rtl_st_ext_stack_address r1 r2)) dest_lbl) def in
    244     let def ≝ translate_op globals Addc [r1] [r1] [r2] start_lbl dest_lbl def in
    245       def
    246   ].
    247   [1: >bytes_length_proof
    248       cut(size' = |destrs|)
    249       [1: @eqb_implies_eq
    250           assumption
    251       |2: #EQ_HYP
    252           <EQ_HYP %
    253       ]
    254   |2: cases daemon (* XXX: bad case where destrs is of the wrong length *)
    255   |3: cases not_implemented (* XXX: float, error_float in o'caml *)
    256   |*: cases daemon (* XXX: various proofs to be filled in *)
    257   ].
    258 qed.
    259  
    260 definition translate_move_internal ≝
    261   λglobals.
    262   λdestr: register.
    263   λsrcr: register.
    264     sequential rtl_params_ globals (MOVE … 〈destr,srcr〉).
    265 
    266 definition translate_move ≝
    267   λglobals.
    268   λdestrs: list register.
    269   λsrcrs: list register.
    270   λstart_lbl: label.
    271     match reduce_strong register register destrs srcrs with
    272     [ mk_Sig crl_crr len_proof ⇒
    273       let commonl ≝ \fst (\fst crl_crr) in
    274       let commonr ≝ \fst (\snd crl_crr) in
    275       let restl ≝ \snd (\fst crl_crr) in
    276       let restr ≝ \snd (\snd crl_crr) in
    277       let f_common ≝ translate_move_internal globals in
    278       let translate1 ≝ adds_graph rtl_params1 … (map2 … f_common commonl commonr ?) in
    279       let translate2 ≝ translate_cst … (Ointconst ? (repr I8 0)) restl in (* should this be 8? *)
    280         add_translates … [ translate1 ; translate2 ] start_lbl
    281     ].
    282     @len_proof
    283 qed.
    284 
    285 let rec make
    286   (A: Type[0]) (elt: A) (n: nat) on n ≝
    287   match n with
    288   [ O ⇒ [ ]
    289   | S n' ⇒ elt :: make A elt n'
    290   ].
    291  
    292 lemma make_length:
     206  λdestrs.
     207  λsrcrs1.
     208  λsrcrs2.
     209  λprf1,prf2.
     210  (* first, clear carry if op relies on it *)
     211  match op with
     212  [ Addc ⇒ [CLEAR_CARRY ??]
     213  | Sub ⇒ [CLEAR_CARRY ??]
     214  | _ ⇒ [ ]
     215  ] @ map3 ???? (OP2 RTL globals op) destrs srcrs1 srcrs2 prf1 prf2.
     216
     217definition cast_list : ∀A.A → ℕ → list A → list A ≝
     218λA,deflt,new_length,l.
     219  if leb (|l|) new_length then
     220    l @ make_list ? deflt (new_length - |l|)
     221  else
     222    lhd … l new_length.
     223
     224lemma length_make_list:
    293225  ∀A: Type[0].
    294226  ∀elt: A.
    295227  ∀n: nat.
    296     n = length ? (make A elt n).
     228    length ? (make_list A elt n) = n.
    297229  #A #ELT #N
    298   elim N
    299   [ normalize %
    300   | #N #IH
    301     normalize <IH %
     230  elim N normalize // qed.
     231
     232lemma length_lhd : ∀A,l,n.|lhd A l n| = min (|l|) n.
     233#A #l elim l -l
     234[ * //
     235| #hd #tl #IH * normalize [%]
     236  #n >IH normalize elim (leb ??) %
     237]
     238qed.
     239
     240lemma length_cast_list : ∀A,dflt,n,l.|cast_list A dflt n l| = n.
     241#A #dflt #n #l
     242normalize @leb_elim #H normalize
     243[ >length_append >length_make_list
     244  @sym_eq @minus_to_plus //
     245| >length_lhd normalize @leb_elim
     246  [ #abs elim (absurd ? abs H) ]
     247  #_ %
     248]
     249qed.
     250
     251definition translate_op_asym_unsigned :
     252  ∀globals.Op2 → list register → list psd_argument → list psd_argument →
     253  list (joint_seq RTL globals) ≝
     254  λglobals,op,destrs,srcrs1,srcrs2.
     255  let l ≝ |destrs| in
     256  let srcrs1' ≝ cast_list ? (zero_byte : psd_argument) l srcrs1 in
     257  let srcrs2' ≝ cast_list ? (zero_byte : psd_argument) l srcrs2 in
     258  translate_op globals op destrs srcrs1' srcrs2' ??.
     259  normalize nodelta
     260  >length_cast_list [2: >length_cast_list ] %
     261qed.
     262
     263let rec nat_to_args (size : nat) (k : nat) on size : Σl : list psd_argument.|l| = size ≝
     264match size with
     265[ O ⇒ [ ]
     266| S size' ⇒
     267  (byte_of_nat k : psd_argument) :: nat_to_args size' (k ÷ 8)
     268]. [ % | cases (nat_to_args ??) #res #EQ  normalize >EQ % ] qed.
     269
     270definition size_of_cst ≝ λtyp.λcst : constant typ.match cst with
     271  [ Ointconst size _ _ ⇒ size_intsize size
     272  | Ofloatconst _ _ ⇒ ? (* not implemented *)
     273  | _ ⇒ 2
     274  ].
     275  cases not_implemented qed.
     276
     277definition cst_well_defd : ∀ty.list ident → constant ty → Prop ≝ λty,globals,cst.
     278  match cst with
     279  [ Oaddrsymbol id _ ⇒ member id (eq_identifier ?) globals
     280  | _ ⇒ True
     281  ].
     282
     283definition translate_cst :
     284  ∀ty.
     285  ∀globals: list ident.
     286  ∀cst_sig: Σcst : constant ty.cst_well_defd ty globals cst.
     287  ∀destrs: list register.
     288  |destrs| = size_of_cst ? cst_sig →
     289  list (joint_seq RTL globals)
     290 ≝
     291  λty,globals,cst_sig,destrs.
     292  match pi1 … cst_sig in constant return λty'.λx : constant ty'.
     293      cst_well_defd ty' ? x → |destrs| = size_of_cst ty' x → ?
     294  with
     295  [ Ointconst size sign const ⇒ λcst_prf,prf.
     296      map2 … (λr.λb : Byte.r ← b) destrs
     297        (split_into_bytes size const) ?
     298  | Ofloatconst _ _ ⇒ ?
     299  | Oaddrsymbol id offset ⇒ λcst_prf,prf.
     300    let 〈r1, r2〉 ≝ make_addr … destrs ? in
     301    [ADDRESS RTL globals id ? r1 r2]
     302  | Oaddrstack offset ⇒ λcst_prf,prf.
     303    let 〈r1, r2〉 ≝ make_addr … destrs ? in
     304    [(rtl_stack_address r1 r2 : joint_seq RTL globals)]
     305  ] (pi2 … cst_sig).
     306  [2: cases not_implemented
     307  |1: cases (split_into_bytes ??) #lst
     308    #EQ >EQ >prf whd in ⊢ (??%?); cases size %
     309  |3: @cst_prf
     310  |*: >prf %
    302311  ]
    303312qed.
    304 
    305 definition translate_cast_unsigned ≝
    306   λglobals.
    307   λdestrs.
    308   λstart_lbl.
    309   λdest_lbl.
    310   λdef: joint_internal_function … (rtl_params globals).
    311   let 〈def, tmp_zero〉 ≝ fresh_reg … def in
    312   let zeros ≝ make … tmp_zero (length … destrs) in
    313     add_translates … [
    314       adds_graph rtl_params1 … [
    315         sequential rtl_params_ … (INT rtl_params_ ? tmp_zero (bitvector_of_nat ? 0))
    316         ];
    317       translate_move globals destrs zeros
    318     ] start_lbl dest_lbl def.
    319 
    320 definition translate_cast_signed:
    321     ∀globals: list ident. list register → ? → label → label → rtl_internal_function globals → rtl_internal_function globals ≝
    322   λglobals: list ident.
    323   λdestrs.
    324   λsrcr.
    325   λstart_lbl.
    326   λdest_lbl.
    327   λdef.
    328   let 〈def, tmp_128〉 ≝ fresh_reg … def in
    329   let 〈def, tmp_255〉 ≝ fresh_reg … def in
    330   let 〈def, tmpr〉 ≝ fresh_reg … def in
    331   let 〈def, dummy〉 ≝ fresh_reg … def in
    332   let insts ≝ [
    333     sequential  … (INT rtl_params_ globals tmp_128 (bitvector_of_nat ? 128));
    334     sequential … (OP2 rtl_params_ globals And tmpr tmp_128 srcr);
    335     sequential … (OPACCS rtl_params_ globals DivuModu tmpr dummy tmpr tmp_128);
    336     sequential … (INT rtl_params_ globals tmp_255 (bitvector_of_nat ? 255));
    337     sequential … (OPACCS rtl_params_ globals Mul tmpr dummy tmpr tmp_255)
     313 
     314definition translate_move :
     315  ∀globals.
     316  ∀destrs: list register.
     317  ∀srcrs: list psd_argument.
     318  |destrs| = |srcrs| → list (joint_seq RTL globals) ≝
     319  λglobals,destrs,srcrs,length_eq.
     320  map2 … (λdst,src.dst ← src) destrs srcrs length_eq.
     321
     322definition sign_mask : ∀globals.register → psd_argument →
     323  list (joint_seq RTL globals) ≝
     324    (* this sets destr to 0xFF if s is neg, 0x00 o.w. Done like that:
     325       byte in destr if srcr is: neg   |  pos
     326       destr ← srcr | 127       11...1 | 01...1
     327       destr ← destr <rot< 1    1...11 | 1...10
     328       destr ← INC destr        0....0 | 1....1
     329       destr ← CPL destr        1....1 | 0....0
     330     *)
     331  λglobals,destr,srca.
     332  match srca with
     333  [ Reg srcr ⇒
     334    let byte_127 : Byte ≝ false ::: maximum ? in
     335    [destr ← srcr .Or. byte_127 ;
     336     destr ← .Rl. destr ;
     337     destr ← .Inc. destr ;
     338     destr ← .Cmpl. destr ]
     339  | Imm by ⇒
     340    match by with
     341    [ BVByte b ⇒
     342      if sign_bit … b then
     343        [ destr ← (maximum … : Byte) ]
     344      else
     345        [ destr ← zero_byte ]
     346    | _ ⇒ (* should not happend ... *) [ ]
     347    ]
     348  ].
     349
     350definition translate_cast_signed :
     351  ∀globals : list ident.
     352  list register → psd_argument →
     353  bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
     354  λglobals,destrs,srca.
     355  ν tmp in
     356  (sign_mask ? tmp srca @
     357  translate_move ? destrs (make_list ? (Reg ? tmp) (|destrs|)) ?).
     358 >length_make_list % qed.
     359
     360definition translate_fill_with_zero :
     361  ∀globals : list ident.
     362  list register → list (joint_seq RTL globals) ≝
     363  λglobals,destrs.
     364  match nat_to_args (|destrs|) 0 with
     365  [ mk_Sig res prf ⇒ translate_move ? destrs res ?].
     366  // qed.
     367
     368let rec last A (l : list A) on l : option A ≝
     369match l with
     370[ nil ⇒ None ?
     371| cons hd tl ⇒
     372  match tl with
     373  [ nil ⇒ Some ? hd
     374  | _ ⇒ last A tl
    338375  ]
    339   in
    340   let srcrs ≝ make … tmpr (length … destrs) in
    341     add_translates rtl_params1 globals [
    342       adds_graph rtl_params1 globals insts;
    343       translate_move globals destrs srcrs
    344     ] start_lbl dest_lbl def.
    345 
    346 definition translate_cast ≝
    347   λglobals: list ident.
    348   λsrc_size: nat.
    349   λsrc_sign: signedness.
    350   λdest_size: nat.
    351   λdestrs: list register.
    352   λsrcrs: list register.
    353   match |srcrs| return λx. |srcrs| = x → ? with
    354   [ O ⇒ λzero_prf. adds_graph rtl_params1 globals [ ]
    355   | S n' ⇒ λsucc_prf.
    356     if ltb dest_size src_size then
    357       translate_move globals destrs srcrs
     376].
     377
     378lemma last_not_empty : ∀A,l.
     379  match l with [ nil ⇒ False | _ ⇒ True ] →
     380  match last A l with
     381  [ None ⇒ False
     382  | _ ⇒ True ].
     383#A #l elim l [ * ]
     384#hd * [ #_ * % ]
     385#hd' #tl #IH * @(IH I)
     386qed.
     387
     388definition translate_op_asym_signed :
     389  ∀globals.Op2 → list register → list psd_argument → list psd_argument →
     390  bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
     391  λglobals,op,destrs,srcrs1,srcrs2.
     392  νtmp1,tmp2 in
     393  let l ≝ |destrs| in
     394  let f ≝ λsrcrs,tmp.
     395    let srcrs_l ≝ |srcrs| in
     396    if leb srcrs_l l then
     397      match last … srcrs with
     398      [ Some last ⇒
     399        〈srcrs @ make_list … (Reg ? tmp) (l - srcrs_l),
     400         sign_mask … tmp last〉
     401      | None ⇒
     402        〈make_list … (zero_byte : psd_argument) l, [ ]〉
     403      ]
    358404    else
    359       match reduce_strong register register destrs srcrs with
    360       [ mk_Sig crl len_proof ⇒
    361         let commonl ≝ \fst (\fst crl) in
    362         let commonr ≝ \fst (\snd crl) in
    363         let restl ≝ \snd (\fst crl) in
    364         let restr ≝ \snd (\snd crl) in
    365         let insts_common ≝ translate_move globals commonl commonr in
    366         let sign_reg ≝ last_safe ? srcrs ? in
    367         let insts_sign ≝
    368           match src_sign with
    369           [ Unsigned ⇒ translate_cast_unsigned globals restl
    370           | Signed ⇒ translate_cast_signed globals restl sign_reg
    371           ]
    372         in
    373           add_translates rtl_params1 globals [ insts_common; insts_sign ]
     405      〈lhd … srcrs l, [ ]〉 in
     406  let prf : ∀srcrs,tmp.|destrs| = |\fst (f srcrs tmp)| ≝ ? in
     407  let srcrs1init ≝ f srcrs1 tmp1 in
     408  let srcrs2init ≝ f srcrs2 tmp2 in
     409  \snd srcrs1init @ \snd srcrs2init @
     410  translate_op globals op destrs (\fst srcrs1init) (\fst srcrs2init) ??.
     411  [ @prf | <prf @prf ]
     412  #srcrs #tmp normalize nodelta
     413  @leb_elim #H normalize nodelta
     414  [ lapply (last_not_empty … srcrs)
     415    cases (last ??)
     416    [ cases srcrs
     417      [ #_ normalize >length_make_list %
     418      | #hd #tl #abs elim(abs I)
    374419      ]
    375   ] (refl ? (|srcrs|)).
    376   >succ_prf //
    377 qed.
    378 
    379 definition translate_negint ≝
     420    | #last #_ normalize nodelta
     421      >length_append >length_make_list
     422      @minus_to_plus //
     423    ]
     424  | >length_lhd normalize @leb_elim
     425    [ #G elim (absurd … G H)
     426    | #_ %
     427    ]
     428  ]
     429qed.
     430
     431(* using size of lists as size of ints *)
     432definition translate_cast :
     433  ∀globals: list ident.
     434  signedness → list register → list register →
     435    bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
     436  λglobals,src_sign,destrs,srcrs.
     437  match reduce_strong ?? destrs srcrs with
     438  [ mk_Sig t prf ⇒
     439    let src_common ≝ \fst (\fst t) in
     440    let src_rest   ≝ \snd (\fst t) in
     441    let dst_common ≝ \fst (\snd t) in
     442    let dst_rest   ≝ \snd (\snd t) in
     443    (* first, move the common part *)
     444    translate_move ? src_common (map … (Reg ?) dst_common) ? @@
     445    match src_rest return λ_.bind_new ?? with
     446    [ nil ⇒ (* upcast *)
     447      match src_sign return λ_.bind_new ?? with
     448      [ Unsigned ⇒ translate_fill_with_zero ? dst_rest
     449      | Signed ⇒
     450        match last … srcrs (* = src_common *) with
     451        [ Some src_last ⇒ translate_cast_signed ? dst_rest src_last
     452        | None ⇒ (* srcrs is empty *) translate_fill_with_zero ? dst_rest
     453        ]
     454      ]
     455    | _ ⇒ (* downcast, nothing else to do *) [ ]
     456    ]
     457  ].
     458  >length_map @prf qed.
     459 
     460definition translate_notint :
     461  ∀globals : list ident.
     462  ∀destrs : list register.
     463  ∀srcrs_arg : list register.
     464  |destrs| = |srcrs_arg| → list (joint_seq RTL globals) ≝
     465  λglobals, destrs, srcrs, prf.
     466  map2 ??? (OP1 RTL globals Cmpl) destrs srcrs prf.
     467
     468definition translate_negint : ∀globals.? → ? → ? → bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
    380469  λglobals: list ident.
    381470  λdestrs: list register.
    382471  λsrcrs: list register.
    383   λstart_lbl: label.
    384   λdest_lbl: label.
    385   λdef: rtl_internal_function globals.
    386472  λprf: |destrs| = |srcrs|. (* assert in caml code *)
    387   let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
    388   let f_cmpl ≝ λdestr. λsrcr. sequential rtl_params_ globals (OP1 rtl_params1 globals Cmpl destr srcr) in
    389   let insts_cmpl ≝ map2 … f_cmpl destrs srcrs prf in
    390   let insts_init ≝ [
    391     sequential … (SET_CARRY …);
    392     sequential … (INT rtl_params_ globals tmpr (zero ?))
    393   ] in
    394   let f_add ≝ λdestr. sequential … (OP2 rtl_params_ globals Addc destr destr tmpr) in
    395   let insts_add ≝ map … f_add destrs in
    396     adds_graph rtl_params1 globals (insts_cmpl @ insts_init @ insts_add) start_lbl dest_lbl def.
    397 
    398 definition translate_notbool: ∀globals. list register → list register → label → label → rtl_internal_function globals → rtl_internal_function globals ≝
    399   λglobals: list ident.
    400   λdestrs: list register.
    401   λsrcrs: list register.
    402   λstart_lbl: label.
    403   λdest_lbl: label.
    404   λdef: rtl_internal_function globals.
     473  translate_notint … destrs srcrs prf @
     474  match nat_to_args (|destrs|) 1 with
     475  [ mk_Sig res prf' ⇒
     476    translate_op ? Add destrs (map … (Reg ?) destrs) res ??
     477  ].
     478>length_map // qed.
     479
     480definition translate_notbool:
     481  ∀globals : list ident.
     482  list register → list register →
     483    bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
     484  λglobals,destrs,srcrs.
    405485  match destrs with
    406   [ nil ⇒ add_graph rtl_params1 globals start_lbl (GOTO … start_lbl) def
    407   | cons destr destrs ⇒
    408     let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
    409     let 〈def, tmp_srcrs〉 ≝ fresh_regs rtl_params0 globals def (length ? srcrs) in
    410     let save_srcrs ≝ translate_move globals tmp_srcrs srcrs in
    411     let init_destr ≝ sequential … (INT rtl_params_ globals destr (bitvector_of_nat ? 1)) in
    412     let f ≝ λtmp_srcr. [
    413       sequential … (CLEAR_CARRY rtl_params_ globals);
    414       sequential … (INT rtl_params_ globals tmpr (zero ?));
    415       sequential … (OP2 rtl_params_ globals Sub tmpr tmpr tmp_srcr);
    416       sequential … (INT rtl_params_ globals tmpr (zero ?));
    417       sequential … (OP2 rtl_params_ globals Addc tmpr tmpr tmpr);
    418       sequential … (OP2 rtl_params_ globals Xor destr destr tmpr)
    419     ] in
    420     let insts ≝ init_destr :: (flatten … (map … f tmp_srcrs)) in
    421     let epilogue ≝ translate_cst globals (Ointconst I8 (zero …)) destrs in
    422       add_translates rtl_params1 globals [
    423         save_srcrs; adds_graph rtl_params1 globals insts; epilogue
    424       ] start_lbl dest_lbl def
    425   ].
    426 
    427 (* TODO: examine this properly.  This is a change from the O'caml code due
    428    to us dropping the explicit use of a cast destination size field.  We
    429    instead infer the size of the cast's destination from the context.  Is
    430    this correct?
    431 *)
    432 definition translate_op1 ≝
    433   λglobals: list ident.
     486  [ nil ⇒ [ ]
     487  | cons destr destrs' ⇒
     488    translate_fill_with_zero ? destrs' @@
     489    match srcrs return λ_.bind_new ?? with
     490    [ nil ⇒ [destr ← zero_byte]
     491    | cons srcr srcrs' ⇒
     492      (destr ← srcr) :::
     493      map register (joint_seq RTL globals) (λr. destr ← destr .Or. r) srcrs' @@
     494      (* now destr is non-null iff srcrs was non-null *)
     495      CLEAR_CARRY ?? :::
     496      (* many uses of 0, better not use immediates *)
     497      ν tmp in
     498      [tmp ← zero_byte ;
     499       destr ← tmp .Sub. tmp ;
     500       (* now carry bit is set iff destr was non-null *)
     501       destr ← tmp .Addc. tmp]
     502     ]
     503   ].
     504
     505definition translate_op1 : ∀globals.? → ? → ? → ? → ? → ? → ? →
     506  bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
     507  λglobals.
    434508  λty, ty'.
    435509  λop1: unary_operation ty ty'.
    436510  λdestrs: list register.
    437511  λsrcrs: list register.
    438   λprf: |destrs| = |srcrs|.
    439   λstart_lbl: label.
    440   λdest_lbl: label.
    441   λdef: rtl_internal_function globals.
    442   match op1 with
    443   [ Ocastint src_size src_sign _ _ ⇒
    444     let dest_size ≝ |destrs| * 8 in
    445     let src_size ≝ bitsize_of_intsize src_size in
    446       translate_cast globals src_size src_sign dest_size destrs srcrs start_lbl dest_lbl def
    447   | Onegint _ _ ⇒
    448       translate_negint globals destrs srcrs start_lbl dest_lbl def prf
    449   | Onotbool _ _ _ _ ⇒
    450       translate_notbool globals destrs srcrs start_lbl dest_lbl def
    451   | Onotint _ _ ⇒
    452     let f ≝ λdestr. λsrcr. sequential rtl_params_ globals (OP1 … Cmpl destr srcr) in
    453     let l ≝ map2 … f destrs srcrs prf in
    454       adds_graph rtl_params1 globals l start_lbl dest_lbl def
    455   | Optrofint _ _ r ⇒
    456       translate_move globals destrs srcrs start_lbl dest_lbl def
    457   | Ointofptr _ _ r ⇒
    458       translate_move globals destrs srcrs start_lbl dest_lbl def
    459   | Oid _ ⇒
    460       translate_move globals destrs srcrs start_lbl dest_lbl def
    461   | _ ⇒ ? (* float operations implemented in runtime *)
    462   ].
    463   cases not_implemented
    464 qed.
    465 
    466 let rec translate_mul1
    467   (globals: list ident) (dummy: register) (tmpr: register)
    468     (destrs: list register) (srcrs1: list register) (srcr2: register)
    469       (start_lbl: label)
    470         on srcrs1 ≝
    471   match destrs with
    472   [ nil ⇒ adds_graph rtl_params1 globals [ GOTO … ] start_lbl
    473   | cons destr tl ⇒
    474     match tl with
     512  λprf1: |destrs| = size_of_sig_type ty'.
     513  λprf2: |srcrs| = size_of_sig_type ty.
     514  match op1
     515  return λty'',ty'''.λx : unary_operation ty'' ty'''.ty'' = ty → ty''' = ty' →
     516    bind_new (localsT RTL) (list (joint_seq RTL globals)) with
     517  [ Ocastint _ src_sign _ _ ⇒ λeq1,eq2.
     518    translate_cast globals src_sign destrs srcrs
     519  | Onegint sz sg ⇒ λeq1,eq2.
     520    translate_negint globals destrs srcrs ?
     521  | Onotbool _ _ _ _ ⇒ λeq1,eq2.
     522    translate_notbool globals destrs srcrs
     523  | Onotint sz sg ⇒ λeq1,eq2.
     524    translate_notint globals destrs srcrs ?
     525  | Optrofint sz sg ⇒ λeq1,eq2.
     526    translate_cast globals Unsigned destrs srcrs
     527  | Ointofptr sz sg ⇒ λeq1,eq2.
     528    translate_cast globals Unsigned destrs srcrs
     529  | Oid t ⇒ λeq1,eq2.
     530      translate_move globals destrs (map … (Reg ?) srcrs) ?
     531  | _ ⇒ λeq1,eq2.? (* float operations implemented in runtime *)
     532  ] (refl …) (refl …).
     533  [3,4,5,6,7,8,9: (* floats *)  cases not_implemented
     534  |*: destruct >prf1 >prf2 [3: >length_map ] //
     535  ]
     536qed.
     537
     538include alias "arithmetics/nat.ma".
     539
     540let rec range_strong_internal (start : ℕ) (count : ℕ)
     541  (* Paolo: no notation to avoid ambiguity *)
     542  on count : list (Σn : ℕ.lt n (plus start count)) ≝
     543match count return λx.count = x → list (Σn : ℕ. n < start + count)
     544  with
     545[ O ⇒ λ_.[ ]
     546| S count' ⇒ λEQ.
     547  let f : (Σn : ℕ. lt n (S start + count')) → Σn : ℕ. lt n (start + count) ≝
     548    λsig.match sig with [mk_Sig n prf ⇒ n] in
     549  start :: map … f (range_strong_internal (S start) count')
     550] (refl …).
     551destruct(EQ) // qed.
     552
     553definition range_strong : ∀end : ℕ. list (Σn.n<end) ≝
     554  λend.range_strong_internal 0 end.
     555
     556definition translate_mul_i :
     557  ∀globals.
     558  register → register →
     559  (* size of destination and sources *)
     560  ∀n : ℕ.
     561  (* the temporary destination, with a dummy register at the end *)
     562  ∀tmp_destrs_dummy : list register.
     563  ∀srcrs1,srcrs2 : list psd_argument.
     564  |tmp_destrs_dummy| = S n →
     565  n = |srcrs1| →
     566  |srcrs1| = |srcrs2| →
     567  (* the position of the least significant byte of the result we compute at
     568     this stage (goes from 0 to n in the main function) *)
     569  ∀k : ℕ.
     570  lt k n →
     571  (* the position of the byte in the first source we will use in this stage.
     572     the position in the other source will be k - i *)
     573  (Σi.i<S k) →
     574  (* the accumulator *)
     575  list (joint_seq RTL globals) →
     576    list (joint_seq RTL globals) ≝
     577  λglobals,a,b,n,tmp_destrs_dummy,srcrs1,srcrs2,
     578    tmp_destrs_dummy_prf,srcrs1_prf,srcrs2_prf,k,k_prf,i_sig,acc.
     579  (* the following will expand to
     580     a, b ← srcrs1[i] * srcrs2[k-i]
     581     tmp_destrs_dummy[k]   ← tmp_destrs_dummy[k] + a
     582     tmp_destrs_dummy[k+1] ← tmp_destrs_dummy[k+1] + b + C
     583     tmp_destrs_dummy[k+2] ← tmp_destrs_dummy[k+2] + 0 + C
     584     ...
     585     tmp_destrs_dummy[n]   ← tmp_destrs_dummy[n] + 0 + C
     586     ( all calculations on tmp_destrs_dummy[n] will be eliminated with
     587     liveness analysis) *)
     588  match i_sig with
     589    [ mk_Sig i i_prf ⇒
     590      (* we pad the result of a byte multiplication with zeros in order
     591         for the bit to be carried. Redundant calculations will be eliminated
     592         by constant propagation. *)
     593      let args : list psd_argument ≝
     594        [Reg ? a;Reg ? b] @ make_list ? (zero_byte : psd_argument) (n - 1 - k) in
     595      let tmp_destrs_view : list register ≝
     596        ltl ? tmp_destrs_dummy k in
     597      ❮a, b❯ ← (nth_safe ? i srcrs1 ?) .Mul. (nth_safe ? (k - i) srcrs2 ?) ::
     598      translate_op … Add tmp_destrs_view (map … (Reg ?) tmp_destrs_view) args ?? @
     599      acc
     600    ].
     601[ @lt_plus_to_minus [ @le_S_S_to_le assumption | <srcrs2_prf <srcrs1_prf
     602  whd >(plus_n_O (S k)) @le_plus // ]
     603| <srcrs1_prf
     604  @(transitive_le … i_prf k_prf)
     605| >length_map //
     606| >length_map
     607  >length_ltl
     608  >tmp_destrs_dummy_prf >length_append
     609  >length_make_list
     610  normalize in ⊢ (???(?%?));
     611  >plus_minus_commutative
     612    [2: @le_plus_to_minus_r <plus_n_Sm <plus_n_O assumption]
     613  cut (S n = 2 + (n - 1))
     614    [2: #EQ >EQ %]
     615  >plus_minus_commutative
     616    [2: @(transitive_le … k_prf) //]
     617  @sym_eq
     618  @plus_to_minus %
     619] qed.
     620
     621definition translate_mul : ∀globals.?→?→?→?→?→bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
     622λglobals : list ident.
     623λdestrs : list register.
     624λsrcrs1 : list psd_argument.
     625λsrcrs2 : list psd_argument.
     626λsrcrs1_prf : |destrs| = |srcrs1|.
     627λsrcrs2_prf : |srcrs1| = |srcrs2|.
     628(* needed fresh registers *)
     629νa in
     630νb in
     631(* temporary registers for the result are created, so to avoid overwriting
     632   sources *)
     633νν |destrs| as tmp_destrs with tmp_destrs_prf in
     634νdummy in
     635(* the step calculating all products with least significant byte going in the
     636   k-th position of the result *)
     637let translate_mul_k : (Σk.k<|destrs|) → list (joint_seq RTL globals) →
     638  list (joint_seq RTL globals) ≝
     639  λk_sig,acc.match k_sig with
     640  [ mk_Sig k k_prf ⇒
     641    foldr … (translate_mul_i ? a b (|destrs|)
     642      (tmp_destrs @ [dummy]) srcrs1 srcrs2
     643      ? srcrs1_prf srcrs2_prf k k_prf) acc (range_strong (S k))
     644  ] in
     645(* initializing tmp_destrs to zero
     646   dummy is intentionally uninitialized *)
     647translate_fill_with_zero … tmp_destrs @
     648(* the main body, roughly:
     649   for k in 0 ... n-1 do
     650     for i in 0 ... k do
     651       translate_mul_i … k … i *)
     652foldr … translate_mul_k [ ] (range_strong (|destrs|)) @
     653(* epilogue: saving the result *)
     654translate_move … destrs (map … (Reg ?) tmp_destrs) ?.
     655[ >length_map >tmp_destrs_prf //
     656| >length_append <plus_n_Sm <plus_n_O //
     657]
     658qed.
     659
     660definition translate_divumodu8 : ∀globals.?→?→?→?→?→?→
     661    bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
     662  λglobals: list ident.
     663  λdiv_not_mod: bool.
     664  λdestrs: list register.
     665  λsrcrs1: list psd_argument.
     666  λsrcrs2: list psd_argument.
     667  λsrcrs1_prf : |destrs| = |srcrs1|.
     668  λsrcrs2_prf : |srcrs1| = |srcrs2|.
     669  match destrs return λx.x = destrs → bind_new ?? with
     670  [ nil ⇒ λ_.[ ]
     671  | cons destr destrs' ⇒ λeq_destrs.
     672    match destrs' with
    475673    [ nil ⇒
    476       match srcrs1 with
    477       [ nil ⇒
    478         adds_graph rtl_params1 globals [
    479           sequential … (INT rtl_params_ globals tmpr (zero …));
    480           sequential … (OP2 rtl_params_ globals Addc destr destr tmpr)
    481         ] start_lbl
    482       | cons srcr1 tl' ⇒
    483         adds_graph rtl_params1 globals [
    484           sequential … (OPACCS rtl_params_ globals Mul tmpr dummy srcr2 srcr1);
    485           sequential … (OP2 rtl_params_ globals Addc destr destr tmpr)
    486         ] start_lbl
    487       ]
    488     | cons destr2 destrs ⇒
    489       match srcrs1 with
    490       [ nil ⇒
    491         add_translates rtl_params1 globals [
    492           adds_graph rtl_params1 globals [
    493             sequential … (INT rtl_params_ globals tmpr (zero …));
    494             sequential … (OP2 rtl_params_ globals Addc destr destr tmpr);
    495             sequential … (OP2 rtl_params_ globals Addc destr2 tmpr tmpr)
    496           ];
    497           translate_cst globals (Ointconst I8 (zero …)) destrs
    498         ] start_lbl
    499       | cons srcr1 srcrs1 ⇒
    500         match destrs with
    501         [ nil ⇒
    502           add_translates rtl_params1 globals [
    503             adds_graph rtl_params1 globals [
    504               sequential … (INT rtl_params_ globals tmpr (zero …));
    505               sequential … (OP2 rtl_params_ globals Addc destr destr tmpr);
    506               sequential … (OP2 rtl_params_ globals Addc destr2 tmpr tmpr)
    507             ];
    508             translate_cst globals (Ointconst I8 (zero ?)) destrs
    509           ] start_lbl
    510         | cons destr2 destrs ⇒
    511           add_translates rtl_params1 globals [
    512             adds_graph rtl_params1 globals [
    513               sequential … (OPACCS rtl_params_ globals Mul tmpr destr2 srcr2 srcr1);
    514               sequential … (OP2 rtl_params_ globals Addc destr destr tmpr)
    515             ];
    516             translate_mul1 globals dummy tmpr (destr2 :: destrs) srcrs1 srcr2
    517           ] start_lbl
    518         ]
    519       ]
     674      match srcrs1 return λx.x = srcrs1 → bind_new ??  with
     675      [ nil ⇒ λeq_srcrs1.⊥
     676      | cons srcr1 srcrs1' ⇒ λeq_srcrs1.
     677        match srcrs2 return λx.x = srcrs2 → bind_new ??  with
     678        [ nil ⇒ λeq_srcrs2.⊥
     679        | cons srcr2 srcrs2' ⇒ λeq_srcrs2.
     680          νdummy in
     681          let 〈destr1, destr2〉 ≝
     682            if div_not_mod then 〈destr, dummy〉 else 〈dummy, destr〉 in
     683          [❮destr1, destr2❯ ← srcr1 .DivuModu. srcr2]
     684        ] (refl …)
     685      ] (refl …)
     686    | _ ⇒ ? (* not implemented *)
    520687    ]
    521   ].
    522 
    523 definition translate_muli ≝
    524   λglobals: list ident.
    525   λdummy: register.
    526   λtmpr: register.
    527   λdestrs: list register.
    528   λtmp_destrs: list register.
    529   λsrcrs1: list register.
    530   λdummy_lbl: label.
    531   λi: nat.
    532   λi_prf: i ≤ |tmp_destrs|.
    533   λtranslates: list ?.
    534   λsrcr2i: register.
    535   let 〈tmp_destrs1, tmp_destrs2〉 ≝ vsplit … tmp_destrs i i_prf in
    536   let tmp_destrs2' ≝
    537     match tmp_destrs2 with
    538     [ nil ⇒ [ ]
    539     | cons tmp_destr2 tmp_destrs2 ⇒ [
    540         adds_graph rtl_params1 globals [
    541           sequential rtl_params_ globals (CLEAR_CARRY …);
    542           sequential … (INT rtl_params_ globals tmp_destr2 (zero …))
    543         ];
    544         translate_mul1 globals dummy tmpr tmp_destrs2 srcrs1 srcr2i;
    545         translate_cst globals (Ointconst I8 (zero …)) tmp_destrs1;
    546         adds_graph rtl_params1 globals [
    547           sequential rtl_params_ globals (CLEAR_CARRY …)
    548         ];
    549         translate_op globals Addc destrs destrs tmp_destrs
    550       ]
    551     ]
    552   in
    553     translates @ tmp_destrs2'.
    554    
    555 let rec remove_n_first_internal
    556   (b: Type[0]) (n: nat) (the_list: list b) (i: nat)
    557     on the_list ≝
    558   match the_list with
    559   [ nil        ⇒ [ ]
    560   | cons hd tl ⇒
    561     match eqb i n with
    562     [ true  ⇒ the_list
    563     | false ⇒ remove_n_first_internal b n tl (S i)
    564     ]
    565   ].
    566    
    567 definition remove_n_first ≝
    568   λb: Type[0].
    569   λn: nat.
    570   λthe_list: list b.
    571     remove_n_first_internal b n the_list 0.
    572 
    573 axiom plus_m_n_eq_o_to_lt_m_o:
    574   ∀m, n, o: nat.
    575     m + n = o → m ≤ o.
    576 
    577 include alias "arithmetics/nat.ma".
    578 
    579 axiom minus_m_n_Sp_to_minus_m_Sn_p:
    580   ∀m, n, p: nat.
    581     minus m n = S p → minus m (S n) = p.
    582    
    583 let rec foldi_strong_internal
    584   (a: Type[0]) (b: Type[0]) (reference: nat) (the_list: list b)
    585     (f: ∀j: nat. ∀proof: lt j (|the_list|). a → b → a) (seed: a)
    586       (counter: nat) (counter_proof: minus reference counter = |the_list|)
    587         on the_list: a ≝
    588   match the_list return λx. the_list = x → (minus reference counter = |x|) → a with
    589   [ nil        ⇒ λidentity. λbase_case. seed
    590   | cons hd tl ⇒ λidentity. λstep_case.
    591     let f' ≝ λj: nat. λproof: j < |tl|. f j ? in
    592       foldi_strong_internal a b reference tl f' (f counter ? seed hd) (S counter) ?
    593   ] (refl … the_list) counter_proof.
    594   [1: cases daemon (* XXX: to do *)
    595   |2: generalize in match counter_proof;
    596       >identity
    597       #HYP
    598       normalize in HYP:(???%);
    599       generalize in match (minus_m_n_Sp_to_minus_m_Sn_p reference counter (|tl|) HYP);
    600       #ASSM assumption
    601   |3: >identity
    602       normalize
    603       normalize in proof;
    604       generalize in match(le_S … proof);
    605       #HYP assumption
    606   ]
    607 qed.
    608  
    609 definition foldi_strong ≝
    610   λa: Type[0].
    611   λb: Type[0].
    612   λthe_list: list b.
    613   λf: (∀i: nat. ∀proof: i < |the_list|. a → b → a).
    614   λseed: a.
    615     foldi_strong_internal a b (|the_list|) the_list f seed 0 ?.
    616   //
    617 qed.
    618  
    619 definition translate_mul ≝
     688  ] (refl …).
     689[3: elim not_implemented]
     690destruct normalize in srcrs1_prf; normalize in srcrs2_prf; destruct qed.
     691
     692(* Paolo: to be moved elsewhere *)
     693let rec foldr2 (A : Type[0]) (B : Type[0]) (C : Type[0]) (f : A→B→C→C) (init : C) (l1 : list A) (l2 : list B)
     694  (prf : |l1| = |l2|) on l1 : C ≝
     695  match l1 return λx.x = l1 → C with 
     696  [ nil ⇒ λ_.init
     697  | cons a l1' ⇒ λeq_l1.
     698    match l2 return λy.y = l2 → C with
     699    [ nil ⇒ λeq_l2.⊥
     700    | cons b l2' ⇒ λeq_l2.
     701      f a b (foldr2 A B C f init l1' l2' ?)
     702    ] (refl …)
     703  ] (refl …).
     704destruct normalize in prf;  [destruct|//]
     705qed.
     706
     707definition translate_ne: ∀globals: list ident.?→?→?→?→
     708  bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
    620709  λglobals: list ident.
    621710  λdestrs: list register.
    622   λsrcrs1: list register.
    623   λsrcrs2: list register.
    624   λregs_proof: |destrs| = |srcrs2|.
    625   λstart_lbl: label.
    626   λdest_lbl: label.
    627   λdef: rtl_internal_function globals.
    628   let 〈def, dummy〉 ≝ fresh_reg rtl_params0 globals def in
    629   let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
    630     match fresh_regs_strong rtl_params0 globals def (|destrs|) with
    631     [ mk_Sig def_tmp_destrs tmp_destrs_prf ⇒
    632       let def ≝ \fst def_tmp_destrs in
    633       let tmp_destrs ≝ \snd def_tmp_destrs in
    634       let 〈def, fresh_srcrs1〉 ≝ fresh_regs rtl_params0 globals def (|srcrs1|) in
    635       let 〈def, fresh_srcrs2〉 ≝ fresh_regs rtl_params0 globals def (|srcrs2|) in
    636       let insts_init ≝ [
    637         translate_move globals fresh_srcrs1 srcrs1;
    638         translate_move globals fresh_srcrs2 srcrs2;
    639         translate_cst globals (Ointconst I8 (zero …)) destrs
    640       ]
    641       in
    642         let f ≝ translate_muli globals dummy tmpr destrs tmp_destrs fresh_srcrs1 start_lbl in
    643         let f' ≝ λi. λi_proof: i < |srcrs2|. f i ? in
    644         let insts_mul ≝ foldi_strong … srcrs2 f' [ ] in
    645           add_translates rtl_params1 globals (insts_init @ insts_mul) start_lbl dest_lbl def
    646     ].
    647   >tmp_destrs_prf
    648   >regs_proof
    649   /2/
    650 qed.
    651 
    652 definition translate_divumodu8 ≝
    653   λglobals: list ident.
    654   λorder: bool.
    655   λdestrs: list register.
    656   λsrcr1: register.
    657   λsrcr2: register.
    658   λstart_lbl: label.
    659   λdest_lbl: label.
    660   λdef: rtl_internal_function globals.
    661   match destrs with
    662   [ nil ⇒ add_graph rtl_params1 globals start_lbl (GOTO … dest_lbl) def
    663   | cons destr destrs ⇒
    664     let 〈def, dummy〉 ≝ fresh_reg rtl_params0 globals def in
    665     let 〈destr1, destr2〉 ≝ match order with [ true ⇒ 〈destr, dummy〉 | _ ⇒ 〈dummy, destr〉 ] in
    666     let inst_div ≝ adds_graph rtl_params1 globals [
    667       sequential rtl_params_ globals (OPACCS … DivuModu destr1 destr2 srcr1 srcr2)
    668     ]
    669     in
    670     let insts_rest ≝ translate_cst globals (Ointconst I8 (zero ?)) destrs in
    671       add_translates rtl_params1 globals [ inst_div; insts_rest ] start_lbl dest_lbl def
    672   ].
    673 
    674 definition translate_ne: ∀globals: list ident. ? → ? → ? → ? → ? → ? → rtl_internal_function globals ≝
     711  λsrcrs1: list psd_argument.
     712  λsrcrs2: list psd_argument.
     713  match destrs return λ_.|srcrs1| = |srcrs2| → bind_new ?? with
     714  [ nil ⇒ λ_.[ ]
     715  | cons destr destrs' ⇒ λEQ.
     716    translate_fill_with_zero … destrs' @@
     717    match srcrs1 return λx.|x| = |srcrs2| → bind_new ?? with
     718    [ nil ⇒ λ_.[destr ← zero_byte]
     719    | cons srcr1 srcrs1' ⇒
     720      match srcrs2 return λx.S (|srcrs1'|) = |x| → bind_new ?? with
     721      [ nil ⇒ λEQ.⊥
     722      | cons srcr2 srcrs2' ⇒ λEQ.
     723        νtmpr in
     724        let f : psd_argument → psd_argument → list (joint_seq RTL globals) → list (joint_seq RTL globals) ≝
     725          λs1,s2,acc.
     726          tmpr  ← s1 .Xor. s2 ::
     727          destr ← destr .Or. tmpr ::
     728          acc in
     729        let epilogue : list (joint_seq RTL globals) ≝
     730          [ CLEAR_CARRY ?? ;
     731            tmpr ← zero_byte .Sub. destr ;
     732            (* now carry bit is 1 iff destrs != 0 *)
     733            destr ← zero_byte .Addc. zero_byte ] in
     734         destr ← srcr1 .Xor. srcr2 ::
     735         foldr2 ??? f epilogue srcrs1' srcrs2' ?
     736       ]
     737     ] EQ
     738   ]. normalize in EQ; destruct(EQ) assumption qed.
     739
     740(* if destrs is 0 or 1, it inverses it. To be used after operations that
     741   ensure this. *)
     742definition translate_toggle_bool : ∀globals.?→list (joint_seq RTL globals) ≝
    675743  λglobals: list ident.
    676744  λdestrs: list register.
    677   λsrcrs1: list register.
    678   λsrcrs2: list register.
    679   λstart_lbl: label.
    680   λdest_lbl: label.
    681   λdef: rtl_internal_function globals.
    682745  match destrs with
    683   [ nil ⇒ add_graph rtl_params1 globals start_lbl (GOTO … dest_lbl) def
    684   | cons destr destrs ⇒
    685     let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
    686     let 〈def, tmp_zero〉 ≝ fresh_reg rtl_params0 globals def in
    687     let 〈def, tmp_srcrs1〉 ≝ fresh_regs rtl_params0 globals def (|srcrs1|) in
    688     let save_srcrs1 ≝ translate_move globals tmp_srcrs1 srcrs1 in
    689     let 〈def, tmp_srcrs2〉 ≝ fresh_regs rtl_params0 globals def (|srcrs2|) in
    690     let save_srcrs2 ≝ translate_move globals tmp_srcrs2 srcrs2 in
    691     match reduce_strong register register tmp_srcrs1 tmp_srcrs2 with
    692     [ mk_Sig crl their_proof ⇒
    693       let commonl ≝ \fst (\fst crl) in
    694       let commonr ≝ \fst (\snd crl) in
    695       let restl ≝ \snd (\snd crl) in
    696       let restr ≝ \snd (\snd crl) in
    697       let rest ≝ restl @ restr in
    698       let inits ≝ [
    699         sequential … (INT rtl_params_ globals destr (zero …));
    700         sequential … (INT rtl_params_ globals tmp_zero (zero …))
    701       ]
    702       in
    703       let f_common ≝ λtmp_srcr1. λtmp_srcr2. [
    704         sequential … (CLEAR_CARRY …);
    705         sequential … (OP2 rtl_params_ globals Sub tmpr tmp_srcr1 tmp_srcr2);
    706         sequential … (OP2 rtl_params_ globals Or destr destr tmpr)
    707       ]
    708       in
    709       let insts_common ≝ flatten … (map2 … f_common commonl commonr ?) in
    710       let f_rest ≝ λtmp_srcr. [
    711         sequential … (CLEAR_CARRY …);
    712         sequential … (OP2 rtl_params_ globals Sub tmpr tmp_zero tmp_srcr);
    713         sequential … (OP2 rtl_params_ globals Or destr destr tmpr)
    714       ]
    715       in
    716       let insts_rest ≝ flatten … (map … f_rest rest) in
    717       let insts ≝ inits @ insts_common @ insts_rest in
    718       let epilogue ≝ translate_cst globals (Ointconst I8 (zero …)) destrs in
    719         add_translates rtl_params1 globals [
    720           save_srcrs1; save_srcrs2; adds_graph rtl_params1 globals insts; epilogue
    721         ] start_lbl dest_lbl def
     746  [ nil ⇒ [ ]
     747  | cons destr _ ⇒ [destr ← .Cmpl. destr]
     748  ].
     749 
     750definition translate_lt_unsigned :
     751  ∀globals.
     752  ∀destrs: list register.
     753  ∀srcrs1: list psd_argument.
     754  ∀srcrs2: list psd_argument.
     755  |srcrs1| = |srcrs2| →
     756  bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
     757  λglobals,destrs,srcrs1,srcrs2,srcrs_prf.
     758  match destrs with
     759  [ nil ⇒ [ ]
     760  | cons destr destrs' ⇒
     761    ν tmpr in
     762    (translate_fill_with_zero … destrs' @
     763    (* I perform a subtraction, but the only interest is in the carry bit *)
     764    translate_op ? Sub (make_list … tmpr (|srcrs1|)) srcrs1 srcrs2 ? srcrs_prf @
     765    [ destr ← zero_byte .Addc. zero_byte ])
     766  ].
     767>length_make_list % qed.
     768
     769(* shifts signed integers by adding 128 to the most significant byte
     770   it replaces it with a fresh register which must be provided *)
     771let rec shift_signed globals
     772  (tmp : register)
     773  (srcrs : list psd_argument) on srcrs :
     774  Σt : (list psd_argument) × (list (joint_seq RTL globals)).|\fst t| = |srcrs| ≝
     775  let byte_128 : Byte ≝ true ::: bv_zero ? in
     776  match srcrs with
     777  [ nil ⇒ 〈[ ],[ ]〉
     778  | cons srcr srcrs' ⇒
     779    match srcrs' with
     780    [ nil ⇒ 〈[ Reg ? tmp ], [ tmp ← srcr .Add. byte_128 ]〉
     781    | _ ⇒
     782      let re ≝ shift_signed globals tmp srcrs' in
     783      〈srcr :: \fst re, \snd re〉
    722784    ]
    723785  ].
    724   @their_proof
    725 qed.
    726 
    727 definition translate_eq_reg ≝
    728   λglobals: list ident.
    729   λtmp_zero: register.
    730   λtmp_one: register.
    731   λtmpr1: register.
    732   λtmpr2: register.
    733   λdestr: register.
    734   λdummy_lbl: label.
    735   λsrcr12: register × register.
    736   let 〈srcr1, srcr2〉 ≝ srcr12 in
    737   [ sequential … (CLEAR_CARRY …);
    738     sequential rtl_params_ globals (OP2 rtl_params_ globals Sub tmpr1 srcr1 srcr2);
    739     sequential … (OP2 rtl_params_ globals Addc tmpr1 tmp_zero tmp_zero);
    740     sequential … (OP2 rtl_params_ globals Sub tmpr2 srcr2 srcr1);
    741     sequential … (OP2 rtl_params_ globals Addc tmpr2 tmp_zero tmp_zero);
    742     sequential … (OP2 rtl_params_ globals Or tmpr1 tmpr1 tmpr2);
    743     sequential … (OP2 rtl_params_ globals Xor tmpr1 tmpr1 tmp_one);
    744     sequential … (OP2 rtl_params_ globals And destr destr tmpr1) ].
    745 
    746 definition translate_eq_list ≝
    747   λglobals: list ident.
    748   λtmp_zero: register.
    749   λtmp_one: register.
    750   λtmpr1: register.
    751   λtmpr2: register.
    752   λdestr: register.
    753   λleq: list (register × register).
    754   λdummy_lbl: label.
    755   let f ≝ translate_eq_reg globals tmp_zero tmp_one tmpr1 tmpr2 destr dummy_lbl in
    756     (sequential … (INT rtl_params_ globals destr (bitvector_of_nat ? 1))) ::
    757       flatten … (map … f leq).
    758 
    759 definition translate_atom ≝
    760   λglobals: list ident.
    761   λtmp_zero: register.
    762   λtmp_one: register.
    763   λtmpr1: register.
    764   λtmpr2: register.
    765   λtmpr3: register.
    766   λdestr: register.
    767   λdummy_lbl: label.
    768   λleq: list (register × register).
    769   λsrcr1: register.
    770   λsrcr2: register.
    771     translate_eq_list globals tmp_zero tmp_one tmpr1 tmpr2 tmpr3 leq dummy_lbl @
    772     [ sequential … (CLEAR_CARRY …);
    773       sequential … (OP2 rtl_params_ globals Sub tmpr1 srcr1 srcr2);
    774       sequential … (OP2 rtl_params_ globals Addc tmpr1 tmp_zero tmp_zero);
    775       sequential … (OP2 rtl_params_ globals And tmpr3 tmpr3 tmpr1);
    776       sequential … (OP2 rtl_params_ globals Or destr destr tmpr3) ].
    777 
    778 definition translate_lt_main ≝
    779   λglobals: list ident.
    780   λtmp_zero: register.
    781   λtmp_one: register.
    782   λtmpr1: register.
    783   λtmpr2: register.
    784   λtmpr3: register.
    785   λdestr: register.
    786   λdummy_lbl: label.
    787   λsrcrs1: list register.
    788   λsrcrs2: list register.
    789   λproof: |srcrs1| = |srcrs2|.
    790   let f ≝ λinsts_leq. λsrcr1. λsrcr2.
    791     let 〈insts, leq〉 ≝ insts_leq in
    792     let added_insts ≝ translate_atom globals tmp_zero tmp_one tmpr1 tmpr2 tmpr3 destr dummy_lbl leq srcr1 srcr2 in
    793       〈insts @ added_insts, leq @ [〈srcr1, srcr2〉]〉
    794   in
    795     \fst (fold_left2 … f 〈[ ], [ ]〉 srcrs1 srcrs2 proof).
    796 
    797 definition fresh_regs_strong:
    798   ∀globals. rtl_internal_function globals → ∀n: nat. Σfresh: (rtl_internal_function globals) × (list register). |\snd fresh| = n ≝
    799   λglobals: list ident.
    800   λdef.
    801   λn.
    802     fresh_regs rtl_params0 globals def n.
    803   @fresh_regs_length
    804 qed.
    805 
    806 definition complete_regs_strong:
    807   ∀globals: list ident. rtl_internal_function globals → list register → list register → Σcomplete: (list register) × (list register) × (list register). |\fst (\fst complete)| = |\snd (\fst complete)| ≝
    808   λglobals: list ident.
    809   λdef.
    810   λleft.
    811   λright.
    812     complete_regs globals def left right.
    813   @complete_regs_length
    814 qed.
    815 
    816 definition translate_lt ≝
    817   λglobals: list ident.
    818   λdestrs: list register.
    819   λprf_destrs: 0 < |destrs|.
    820   λsrcrs1: list register.
    821   λsrcrs2: list register.
    822   λstart_lbl: label.
    823   λdest_lbl: label.
    824   λdef: rtl_internal_function globals.
    825   match destrs with
    826   [ nil ⇒ add_graph rtl_params1 globals start_lbl (GOTO … dest_lbl) def
    827   | _ ⇒
    828     match fresh_regs_strong globals def (|destrs|) with
    829     [ mk_Sig def_tmp_destrs tmp_destrs_proof ⇒
    830       let def ≝ \fst def_tmp_destrs in
    831       let tmp_destrs ≝ \snd def_tmp_destrs in
    832       let tmp_destr ≝ hd_safe ? tmp_destrs ? in
    833       let 〈def, tmp_zero〉 ≝ fresh_reg rtl_params1 globals def in
    834       let 〈def, tmp_one〉 ≝ fresh_reg rtl_params1 globals def in
    835       let 〈def, tmpr1〉 ≝ fresh_reg rtl_params1 globals def in
    836       let 〈def, tmpr2〉 ≝ fresh_reg rtl_params1 globals def in
    837       let 〈def, tmpr3〉 ≝ fresh_reg rtl_params1 globals def in
    838       match complete_regs_strong globals def srcrs1 srcrs2 with
    839       [ mk_Sig srcrs12_added srcrs12_proof ⇒
    840         let srcrs1 ≝ \fst (\fst srcrs12_added) in
    841         let srcrs2 ≝ \snd (\fst srcrs12_added) in
    842         let added ≝ \snd srcrs12_added in
    843         let srcrs1' ≝ rev … srcrs1 in
    844         let srcrs2' ≝ rev … srcrs2 in
    845         let insts_init ≝ [
    846           translate_cst globals (Ointconst I8 (zero ?)) tmp_destrs;
    847           translate_cst globals (Ointconst I8 (zero ?)) added;
    848           adds_graph rtl_params1 globals [
    849             sequential rtl_params_ globals (INT rtl_params_ globals tmp_zero (zero …));
    850             sequential rtl_params_ globals (INT rtl_params_ globals tmp_one (bitvector_of_nat … 1))
    851           ]
    852         ]
    853         in
    854         let insts_main ≝
    855           translate_lt_main globals tmp_zero tmp_one tmpr1 tmpr2 tmpr3 tmp_destr start_lbl srcrs1' srcrs2' ? in
    856           let insts_main ≝ [ adds_graph rtl_params1 globals insts_main ] in
    857           let insts_exit ≝ [ translate_move globals destrs tmp_destrs ] in
    858             add_translates rtl_params1 globals (insts_init @ insts_main @ insts_exit) start_lbl dest_lbl def
    859       ]
    860     ]
    861   ].
    862   [2: >tmp_destrs_proof @prf_destrs
    863   |1: normalize nodelta
    864       generalize in match srcrs12_proof;
    865       #HYP >rev_length >rev_length @HYP
    866   ]
    867 qed.
    868 
    869 definition add_128_to_last ≝
    870   λglobals: list ident.
    871   λtmp_128: register.
    872   λrs.
    873   λprf: 0 < |rs|.
    874   λstart_lbl: label.
    875   match rs with
    876   [ nil ⇒ adds_graph rtl_params1 globals [ ] start_lbl
    877   | _ ⇒
    878     let r ≝ last_safe … rs prf in
    879       adds_graph rtl_params1 globals [
    880         sequential rtl_params_ globals (OP2 rtl_params_ globals Add r r tmp_128)
    881       ] start_lbl
    882   ].
    883 
    884 definition translate_lts ≝
    885   λglobals: list ident.
    886   λdestrs: list register.
    887   λdestrs_prf: 0 < |destrs|.
    888   λsrcrs1: list register.
    889   λsrcrs2: list register.
    890   λsrcrs1_lt_prf: 0 < |srcrs1|.
    891   λsrcrs2_lt_prf: 0 < |srcrs2|.
    892   λstart_lbl: label.
    893   λdest_lbl: label.
    894   λdef: rtl_internal_function globals.
    895   match fresh_regs_strong globals def (|srcrs1|) with
    896   [ mk_Sig def_tmp_srcrs1 srcrs1_prf ⇒
    897     let def ≝ \fst def_tmp_srcrs1 in
    898     let tmp_srcrs1 ≝ \snd def_tmp_srcrs1 in
    899     match fresh_regs_strong globals def (|srcrs2|) with
    900     [ mk_Sig def_tmp_srcrs2 srcrs2_prf ⇒
    901       let def ≝ \fst def_tmp_srcrs2 in
    902       let tmp_srcrs2 ≝ \snd def_tmp_srcrs2 in
    903       let 〈def, tmp_128〉 ≝ fresh_reg rtl_params0 globals def in
    904         add_translates rtl_params1 globals [
    905           translate_move globals tmp_srcrs1 srcrs1;
    906           translate_move globals tmp_srcrs2 srcrs2;
    907           adds_graph rtl_params1 globals [
    908             sequential rtl_params_ globals (INT rtl_params_ globals tmp_128 (bitvector_of_nat ? 128))
    909           ];
    910           add_128_to_last globals tmp_128 tmp_srcrs1 ?;
    911           add_128_to_last globals tmp_128 tmp_srcrs2 ?;
    912           translate_lt globals destrs destrs_prf tmp_srcrs1 tmp_srcrs2
    913         ] start_lbl dest_lbl def
    914     ]
    915   ].
    916   [1: >srcrs1_prf @srcrs1_lt_prf
    917   |2: >srcrs2_prf @srcrs2_lt_prf
    918   ]
    919 qed.
    920 
    921 definition translate_op2 ≝
    922   λglobals: list ident.
    923   λop2.
    924   λdestrs: list register.
    925   λdestrs_prf: 0 < |destrs|.
    926   λsrcrs1: list register.
    927   λsrcrs2: list register.
    928   λsrcrs2_destrs_prf: |srcrs2| = |destrs|.
    929   λsrcrs1_destrs_prf: |srcrs1| = |destrs|.
    930   λstart_lbl: label.
    931   λdest_lbl: label.
    932   λdef: rtl_internal_function globals.
    933   match op2 with
    934   [ Oadd ⇒
    935     translate_op globals Addc destrs srcrs1 srcrs2 start_lbl dest_lbl def
    936   | Oaddp ⇒
    937     translate_op globals Addc destrs srcrs1 srcrs2 start_lbl dest_lbl def
    938   | Osub ⇒
    939     translate_op globals Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
    940   | Osubpi ⇒
    941     translate_op globals Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
    942   | Osubpp sz ⇒
    943     translate_op globals Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
    944   | Omul ⇒
    945     translate_mul globals destrs srcrs1 srcrs2 ? start_lbl dest_lbl def
    946   | Odivu ⇒
    947     match srcrs1 return λx. 0 < |x| → rtl_internal_function globals with
    948     [ cons hd tl ⇒ λcons_prf.
    949       match tl with
    950       [ nil ⇒ translate_divumodu8 globals true destrs hd (hd_safe register srcrs2 ?) start_lbl dest_lbl def
    951       | _ ⇒ ? (* not implemented *)
    952       ]
    953     | nil ⇒ λnil_absrd. ?
    954     ] ?
    955   | Omodu ⇒
    956     match srcrs1 return λx. 0 < |x| → rtl_internal_function globals with
    957     [ cons hd tl ⇒ λcons_prf.
    958       match tl with
    959       [ nil ⇒ translate_divumodu8 globals false destrs hd (hd_safe register srcrs2 ?) start_lbl dest_lbl def
    960       | _ ⇒ ? (* not implemented *)
    961       ]
    962     | nil ⇒ λnil_absrd. ?
    963     ] ?
    964   | Oand ⇒
    965     translate_op globals And destrs srcrs1 srcrs2 start_lbl dest_lbl def
    966   | Oor ⇒
    967     translate_op globals Or destrs srcrs1 srcrs2 start_lbl dest_lbl def
    968   | Oxor ⇒
    969     translate_op globals Xor destrs srcrs1 srcrs2 start_lbl dest_lbl def
    970   | Ocmp c ⇒
    971     match c with
    972     [ Ceq ⇒
    973       add_translates rtl_params1 globals [
    974         translate_ne globals destrs srcrs1 srcrs2;
    975         translate_op1 globals ?? (Onotbool (ASTint I8 Unsigned) I8 Unsigned I) destrs destrs (refl ? (|destrs|))
    976       ] start_lbl dest_lbl def
    977     | Cne ⇒ translate_ne globals destrs srcrs1 srcrs2 start_lbl dest_lbl def
    978     | Clt ⇒ translate_lts globals destrs destrs_prf srcrs1 srcrs2 ? ? start_lbl dest_lbl def
    979     | Cgt ⇒ translate_lts globals destrs destrs_prf srcrs2 srcrs1 ? ? start_lbl dest_lbl def
    980     | Cle ⇒
    981       add_translates rtl_params1 globals [
    982         translate_lts globals destrs destrs_prf srcrs2 srcrs1 ? ?;
    983         translate_op1 globals ?? (Onotbool (ASTint I8 Unsigned) I8 Unsigned I) destrs destrs (refl ? (|destrs|))
    984       ] start_lbl dest_lbl def
    985     | Cge ⇒
    986       add_translates rtl_params1 globals [
    987         translate_lts globals destrs destrs_prf srcrs1 srcrs2 ? ?;
    988         translate_op1 globals ?? (Onotbool (ASTint I8 Unsigned) I8 Unsigned I) destrs destrs (refl ? (|destrs|))
    989       ] start_lbl dest_lbl def
    990     ]
    991   | Ocmpu c ⇒
    992     match c with
    993     [ Ceq ⇒
    994       add_translates rtl_params1 globals [
    995         translate_ne globals destrs srcrs1 srcrs2;
    996         translate_op1 globals ?? (Onotbool (ASTint I8 Unsigned) I8 Unsigned I) destrs destrs (refl ? (|destrs|))
    997       ] start_lbl dest_lbl def
    998     | Cne ⇒ translate_ne globals destrs srcrs1 srcrs2 start_lbl dest_lbl def
    999     | Clt ⇒ translate_lt globals destrs destrs_prf srcrs1 srcrs2 start_lbl dest_lbl def
    1000     | Cgt ⇒ translate_lt globals destrs destrs_prf srcrs2 srcrs1 start_lbl dest_lbl def
    1001     | Cle ⇒
    1002       add_translates rtl_params1 globals [
    1003         translate_lt globals destrs destrs_prf srcrs2 srcrs1;
    1004         translate_op1 globals ?? (Onotbool (ASTint I8 Unsigned) I8 Unsigned I) destrs destrs (refl ? (|destrs|))
    1005       ] start_lbl dest_lbl def
    1006     | Cge ⇒
    1007       add_translates rtl_params1 globals [
    1008         translate_lt globals destrs destrs_prf srcrs1 srcrs2;
    1009         translate_op1 globals ?? (Onotbool (ASTint I8 Unsigned) I8 Unsigned I) destrs destrs (refl ? (|destrs|))
    1010       ] start_lbl dest_lbl def
    1011     ]
    1012   | Ocmpp c ⇒
    1013     match c with
    1014     [ Ceq ⇒
    1015       add_translates rtl_params1 globals [
    1016         translate_ne globals destrs srcrs1 srcrs2;
    1017         translate_op1 globals ?? (Onotbool (ASTint I8 Unsigned) I8 Unsigned I) destrs destrs (refl ? (|destrs|))
    1018       ] start_lbl dest_lbl def
    1019     | Cne ⇒ translate_ne globals destrs srcrs1 srcrs2 start_lbl dest_lbl def
    1020     | Clt ⇒ translate_lt globals destrs destrs_prf srcrs1 srcrs2 start_lbl dest_lbl def
    1021     | Cgt ⇒ translate_lt globals destrs destrs_prf srcrs2 srcrs1 start_lbl dest_lbl def
    1022     | Cle ⇒
    1023       add_translates rtl_params1 globals [
    1024         translate_lt globals destrs destrs_prf srcrs2 srcrs1;
    1025         translate_op1 globals ?? (Onotbool (ASTint I8 Unsigned) I8 Unsigned I) destrs destrs (refl ? (|destrs|))
    1026       ] start_lbl dest_lbl def
    1027     | Cge ⇒
    1028       add_translates rtl_params1 globals [
    1029         translate_lt globals destrs destrs_prf srcrs1 srcrs2;
    1030         translate_op1 globals ?? (Onotbool (ASTint I8 Unsigned) I8 Unsigned I) destrs destrs (refl ? (|destrs|))
    1031       ] start_lbl dest_lbl def
    1032     ]
    1033   | _ ⇒ ? (* assert false, implemented in run time or float op *)
    1034   ].
    1035   [1:
    1036     @sym_eq
    1037     assumption
    1038   |3,8,19,22,24,25:
    1039     >srcrs1_destrs_prf
    1040     assumption
    1041   |4,9:
    1042     normalize in nil_absrd;
    1043     cases(not_le_Sn_O 0)
    1044     #HYP cases(HYP nil_absrd)
    1045   |5,10,20,21,23,26:
    1046     >srcrs2_destrs_prf
    1047     assumption
    1048   |*:
    1049     cases not_implemented (* XXX: yes, really *)
    1050   ]
    1051 qed.
    1052 
    1053 definition translate_cond: ∀globals: list ident. list register → label → label → label → rtl_internal_function globals → rtl_internal_function globals ≝
     786[1,2: %
     787|*: cases re * #a #b >p1 normalize #EQ >EQ %
     788] qed.
     789
     790definition translate_lt_signed :
     791  ∀globals.
     792  ∀destrs: list register.
     793  ∀srcrs1: list psd_argument.
     794  ∀srcrs2: list psd_argument.
     795  |srcrs1| = |srcrs2| →
     796  bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
     797  λglobals,destrs,srcrs1,srcrs2,srcrs_prf.
     798  νtmp_last_s1 in
     799  νtmp_last_s2 in
     800  let p1 ≝ shift_signed globals tmp_last_s1 srcrs1 in
     801  let new_srcrs1 ≝ \fst p1 in
     802  let shift_srcrs1 ≝ \snd p1 in
     803  let p2 ≝ shift_signed globals tmp_last_s2 srcrs2 in
     804  let new_srcrs2 ≝ \fst p2 in
     805  let shift_srcrs2 ≝ \snd p2 in
     806  shift_srcrs1 @@ shift_srcrs2 @@
     807  translate_lt_unsigned globals destrs new_srcrs1 new_srcrs2 ?.
     808whd in match new_srcrs1; whd in match new_srcrs2;
     809cases p1
     810cases p2
     811//
     812qed.
     813
     814definition translate_lt : bool→∀globals.?→?→?→?→bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
     815  λis_unsigned,globals,destrs,srcrs1,srcrs2,srcrs_prf.
     816  if is_unsigned then
     817    translate_lt_unsigned globals destrs srcrs1 srcrs2 srcrs_prf
     818  else
     819    translate_lt_signed globals destrs srcrs1 srcrs2 srcrs_prf.
     820
     821definition translate_cmp ≝
     822  λis_unsigned,globals,cmp,destrs,srcrs1,srcrs2,srcrs_prf.
     823  match cmp with
     824  [ Ceq ⇒
     825    translate_ne globals destrs srcrs1 srcrs2 srcrs_prf @@
     826    translate_toggle_bool globals destrs
     827  | Cne ⇒
     828    translate_ne globals destrs srcrs1 srcrs2 srcrs_prf
     829  | Clt ⇒
     830    translate_lt is_unsigned globals destrs srcrs1 srcrs2 srcrs_prf
     831  | Cgt ⇒
     832    translate_lt is_unsigned globals destrs srcrs2 srcrs1 ?
     833  | Cle ⇒
     834    translate_lt is_unsigned globals destrs srcrs2 srcrs1 ? @@
     835    translate_toggle_bool globals destrs
     836  | Cge ⇒
     837    translate_lt is_unsigned globals destrs srcrs1 srcrs2 srcrs_prf @@
     838    translate_toggle_bool globals destrs
     839  ].
     840// qed.
     841
     842definition translate_op2 :
     843  ∀globals.∀ty1,ty2,ty3.∀op : binary_operation ty1 ty2 ty3.
     844  ∀destrs : list register.
     845  ∀srcrs1,srcrs2 : list psd_argument.
     846  |destrs| = size_of_sig_type ty3 →
     847  |srcrs1| = size_of_sig_type ty1 →
     848  |srcrs2| = size_of_sig_type ty2 →
     849  bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
     850  λglobals,ty1,ty2,ty3,op2,destrs,srcrs1,srcrs2.
     851  match op2 return λty1,ty2,ty3.λx : binary_operation ty1 ty2 ty3.
     852    ? = size_of_sig_type ty3 → ? = size_of_sig_type ty1 → ? = size_of_sig_type ty2 →
     853    bind_new ?? with
     854  [ Oadd sz sg ⇒ λprf1,prf2,prf3.
     855    translate_op globals Add destrs srcrs1 srcrs2 ??
     856  | Oaddp sz ⇒ λprf1,prf2,prf3.
     857    translate_op_asym_signed globals Add destrs srcrs1 srcrs2
     858  | Osub sz sg ⇒ λprf1,prf2,prf2.
     859    translate_op globals Sub destrs srcrs1 srcrs2 ??
     860  | Osubpi sz ⇒ λprf1,prf2,prf3.
     861    translate_op_asym_signed globals Add destrs srcrs1 srcrs2
     862  | Osubpp sz ⇒ λprf1,prf2,prf3.
     863    translate_op_asym_unsigned globals Sub destrs srcrs1 srcrs2
     864  | Omul sz sg ⇒ λprf1,prf2,prf3.
     865    translate_mul globals destrs srcrs1 srcrs2 ??
     866  | Odivu sz ⇒ λprf1,prf2,prf3.
     867    translate_divumodu8 globals true destrs srcrs1 srcrs2 ??
     868  | Omodu sz ⇒ λprf1,prf2,prf3.
     869    translate_divumodu8 globals false destrs srcrs1 srcrs2 ??
     870  | Oand sz sg ⇒ λprf1,prf2,prf3.
     871    translate_op globals And destrs srcrs1 srcrs2 ??
     872  | Oor sz sg ⇒ λprf1,prf2,prf3.
     873    translate_op globals Or destrs srcrs1 srcrs2 ??
     874  | Oxor sz sg ⇒ λprf1,prf2,prf3.
     875    translate_op globals Xor destrs srcrs1 srcrs2 ??
     876  | Ocmp sz sg1 sg2 c ⇒ λprf1,prf2,prf3.
     877    translate_cmp false globals c destrs srcrs1 srcrs2 ?
     878  | Ocmpu sz sg c ⇒ λprf1,prf2,prf3.
     879    translate_cmp true globals c destrs srcrs1 srcrs2 ?
     880  | Ocmpp sg c ⇒ λprf1,prf2,prf3.
     881    let is_Ocmpp ≝ 0 in
     882    translate_cmp true globals c destrs srcrs1 srcrs2 ?
     883  | _ ⇒ ⊥ (* assert false, implemented in run time or float op *)
     884  ]. try @not_implemented //
     885  qed.
     886
     887definition translate_cond: ∀globals: list ident. list register → label →
     888  bind_seq_block RTL globals (joint_step RTL globals) ≝
    1054889  λglobals: list ident.
    1055890  λsrcrs: list register.
    1056   λstart_lbl: label.
    1057891  λlbl_true: label.
    1058   λlbl_false: label.
    1059   λdef: rtl_internal_function globals.
    1060   let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
    1061   let 〈tmp_lbl, def〉 ≝ fresh_label rtl_params1 globals def in
    1062   let init ≝ sequential rtl_params_ globals (INT rtl_params_ globals tmpr (zero …)) in
    1063   let f ≝ λsrcr. sequential rtl_params_ globals (OP2 rtl_params_ globals Or tmpr tmpr srcr) in
    1064   let def ≝ adds_graph rtl_params1 globals (init :: (map ? ? f srcrs)) start_lbl tmp_lbl def in
    1065     add_graph rtl_params1 globals tmp_lbl (sequential rtl_params_ globals (COND rtl_params_ globals tmpr lbl_true) lbl_false) def.
    1066 
    1067 definition translate_load ≝
     892  match srcrs return λ_.bind_seq_block RTL ? (joint_step ??) with
     893  [ nil ⇒ bret … 〈[ ], NOOP ??〉
     894  | cons srcr srcrs' ⇒
     895    ν tmpr in
     896    let f : register → joint_seq RTL globals ≝
     897      λr. tmpr ← tmpr .Or. r in
     898    bret … 〈MOVE RTL globals 〈tmpr,srcr〉 ::
     899    map ?? f srcrs', (COND … tmpr lbl_true : joint_step ??) 〉
     900  ].
     901
     902(* Paolo: to be controlled (original seemed overly complex) *)
     903definition translate_load : ∀globals.?→?→?→bind_new (localsT RTL) ? ≝
    1068904  λglobals: list ident.
    1069   λaddr.
     905  λaddr : list psd_argument.
    1070906  λaddr_prf: 2 = |addr|.
    1071907  λdestrs: list register.
    1072   λstart_lbl: label.
    1073   λdest_lbl: label.
    1074   λdef: rtl_internal_function globals.
    1075   match fresh_regs_strong rtl_params0 globals def (|addr|) with
    1076   [ mk_Sig def_save_addr save_addr_prf ⇒
    1077     let def ≝ \fst def_save_addr in
    1078     let save_addr ≝ \snd def_save_addr in
    1079     match fresh_regs_strong rtl_params0 globals def (|addr|) with
    1080     [ mk_Sig def_tmp_addr tmp_addr_prf ⇒
    1081       let def ≝ \fst def_tmp_addr in
    1082       let tmp_addr ≝ \snd def_tmp_addr in
    1083       let 〈tmp_addr1, tmp_addr2〉 ≝ make_addr … tmp_addr ? in
    1084       let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
    1085       let 〈def, dummy〉 ≝ fresh_reg rtl_params0 globals def in
    1086       let insts_save_addr ≝ translate_move globals save_addr addr in
    1087       let f ≝ λtranslates_off. λr.
    1088         let 〈translates, off〉 ≝ translates_off in
    1089         let translates ≝ translates @ [
    1090           adds_graph rtl_params1 globals [
    1091             sequential rtl_params_ globals (INT rtl_params_ globals tmpr off)
    1092           ];
    1093           translate_op2 globals Oaddp tmp_addr ? save_addr [dummy; tmpr] ? ?;
    1094           adds_graph rtl_params1 globals [
    1095             sequential rtl_params_ globals (LOAD rtl_params_ globals r tmp_addr1 tmp_addr2)
    1096           ]
    1097         ]
    1098         in
    1099         let 〈carry, result〉 ≝ half_add … off int_size in
    1100           〈translates, result〉
    1101       in
    1102       let 〈translates, ignore〉 ≝ foldl … f 〈[ ], (zero ?)〉 destrs in
    1103         add_translates rtl_params1 globals (insts_save_addr :: translates) start_lbl dest_lbl def
     908  ν tmp_addr_l in
     909  ν tmp_addr_h in
     910  let f ≝ λdestr : register.λacc : list (joint_seq RTL globals).
     911    LOAD RTL globals destr (Reg ? tmp_addr_l) (Reg ? tmp_addr_h) ::
     912    translate_op ? Add
     913      [tmp_addr_l ; tmp_addr_h]
     914      [tmp_addr_l ; tmp_addr_h]
     915      [zero_byte ; (int_size : Byte)] ? ? @ acc in
     916  translate_move … [tmp_addr_l ; tmp_addr_h] addr ? @@
     917  foldr … f [ ] destrs.
     918[1: <addr_prf
     919] // qed.
     920 
     921definition translate_store : ∀globals.?→?→?→bind_new (localsT RTL) ? ≝
     922  λglobals: list ident.
     923  λaddr : list psd_argument.
     924  λaddr_prf: 2 = |addr|.
     925  λsrcrs: list psd_argument.
     926  ν tmp_addr_l in
     927  ν tmp_addr_h in
     928  let f ≝ λsrcr : psd_argument.λacc : list (joint_seq RTL globals).
     929    STORE RTL globals (Reg ? tmp_addr_l) (Reg ? tmp_addr_h) srcr ::
     930    translate_op … Add
     931      [tmp_addr_l ; tmp_addr_h]
     932      [tmp_addr_l ; tmp_addr_h]
     933      [zero_byte ; (int_size : Byte)] ? ? @ acc in
     934  translate_move … [tmp_addr_l ; tmp_addr_h] addr ? @@
     935  foldr … f [ ] srcrs.
     936[1: <addr_prf] // qed.
     937
     938lemma lenv_typed_reg_typed_ok1 :
     939  ∀locals,env,r,ty.
     940  local_env_typed locals env →
     941  Exists ? (λx:register×typ.〈r,ty〉=x) locals →
     942  ∀prf.
     943  |find_local_env r env prf| = size_of_sig_type ty.
     944#locals #env #r #ty #env_typed #r_ok
     945elim (Exists_All … r_ok env_typed)
     946* #r' #ty' * #EQ destruct(EQ) * #rs * #EQ1 #EQ2 #prf
     947whd in match find_local_env; normalize nodelta
     948@opt_safe_elim #rs' >EQ1 #EQ' destruct assumption
     949qed.
     950
     951lemma lenv_typed_arg_typed_ok1 :
     952  ∀locals,env,r,ty.
     953  local_env_typed locals env →
     954  Exists ? (λx:register×typ.〈r,ty〉=x) locals →
     955  ∀prf.
     956  |find_local_env_arg r env prf| = size_of_sig_type ty.
     957#locals #env #r #ty #env_typed #r_ok #prf
     958whd in match find_local_env_arg; normalize nodelta
     959>length_map @lenv_typed_reg_typed_ok1 assumption
     960qed.
     961
     962lemma lenv_typed_reg_typed_ok2 :
     963  ∀locals,env,r,ty.
     964  local_env_typed locals env →
     965  Exists ? (λx:register×typ.〈r,ty〉=x) locals →
     966  r ∈ env.
     967#locals #env #r #ty #env_typed #r_ok
     968elim (Exists_All … r_ok env_typed)
     969* #r' #ty' * #EQ destruct(EQ) * #rs * #EQ1 #EQ2
     970whd in ⊢ (?%);
     971>EQ1 %
     972qed.
     973
     974lemma cst_size_ok : ∀ty,cst.size_of_sig_type ty=size_of_cst ty cst.
     975#ty * -ty [*] //
     976qed.
     977
     978definition translate_statement : ∀globals, locals.∀env.
     979  local_env_typed locals env →
     980  ∀stmt : statement.statement_typed locals stmt →
     981  𝚺b :
     982  bind_seq_block RTL globals (joint_step RTL globals) +
     983  bind_seq_block RTL globals (joint_fin_step RTL).
     984  if is_inl … b then label else unit ≝
     985  λglobals,locals,lenv,lenv_typed,stmt.
     986  match stmt return λstmt.statement_typed locals stmt → 𝚺b:bind_seq_block ???+bind_seq_block ???.if is_inl … b then label else unit with
     987  [ St_skip lbl' ⇒ λstmt_typed.
     988    ❬NOOP ??, lbl'❭
     989  | St_cost cost_lbl lbl' ⇒ λstmt_typed.
     990    ❬COST_LABEL … cost_lbl, lbl'❭
     991  | St_const ty destr cst lbl' ⇒ λstmt_typed.
     992    ❬translate_cst ty globals cst (find_local_env destr lenv ?) ?, lbl'❭
     993  | St_op1 ty ty' op1 destr srcr lbl' ⇒ λstmt_typed.
     994    ❬translate_op1 globals ty' ty op1
     995      (find_local_env destr lenv ?)
     996      (find_local_env srcr lenv ?) ??, lbl'❭
     997  | St_op2 ty1 ty2 ty3 op2 destr srcr1 srcr2 lbl' ⇒ λstmt_typed.
     998    ❬translate_op2 globals … op2
     999      (find_local_env destr lenv ?)
     1000      (find_local_env_arg srcr1 lenv ?)
     1001      (find_local_env_arg srcr2 lenv ?) ???, lbl'❭
     1002    (* XXX: should we be ignoring this? *)
     1003  | St_load ignore addr destr lbl' ⇒ λstmt_typed.
     1004    ❬translate_load globals
     1005      (find_local_env_arg addr lenv ?) ? (find_local_env destr lenv ?), lbl'❭
     1006    (* XXX: should we be ignoring this? *)
     1007  | St_store ignore addr srcr lbl' ⇒ λstmt_typed.
     1008    ❬translate_store globals (find_local_env_arg addr lenv ?) ?
     1009      (find_local_env_arg srcr lenv ?), lbl'❭
     1010  | St_call_id f args retr lbl' ⇒ λstmt_typed.
     1011    ❬(match retr with
     1012      [ Some retr ⇒
     1013        CALL_ID RTL ? f (rtl_args args lenv ?) (find_local_env retr lenv ?)
     1014      | None ⇒
     1015        CALL_ID RTL ? f (rtl_args args lenv ?) [ ]
     1016      ] : bind_seq_block ???), lbl'❭
     1017  | St_call_ptr f args retr lbl' ⇒ λstmt_typed.
     1018    let fs ≝ find_and_addr f lenv ?? in
     1019    ❬(rtl_call_ptr (\fst fs) (\snd fs) (rtl_args args lenv ?)
     1020      (match retr with
     1021       [ Some retr ⇒
     1022         find_local_env retr lenv ?
     1023       | None ⇒ [ ]
     1024       ]) : joint_step ??), lbl'❭
     1025  | St_cond r lbl_true lbl_false ⇒ λstmt_typed.
     1026    ❬translate_cond globals (find_local_env r lenv ?) lbl_true, lbl_false❭
     1027  | St_jumptable r l ⇒ ⊥ (* assert false: not implemented yet *)
     1028  | St_return ⇒ λ_. ❬inr … (RETURN ?),it❭
     1029  ].
     1030  [ >(lenv_typed_reg_typed_ok1 … lenv_typed stmt_typed)
     1031    @cst_size_ok
     1032  | @(lenv_typed_reg_typed_ok2 … lenv_typed stmt_typed)
     1033  | cases daemon (* needs more hypotheses *)
     1034  |4,5,6,7: cases stmt_typed #dstr_typed #srcr_typed
     1035    [1,2: @(lenv_typed_reg_typed_ok1 … lenv_typed) assumption
     1036    | @(lenv_typed_reg_typed_ok2 … lenv_typed srcr_typed)
     1037    | @(lenv_typed_reg_typed_ok2 … lenv_typed dstr_typed)
    11041038    ]
    1105   ].
    1106   [1: >tmp_addr_prf >save_addr_prf %
    1107   |2: >save_addr_prf >tmp_addr_prf
    1108       @addr_prf
    1109   |3: >tmp_addr_prf normalize
    1110       <addr_prf //
    1111   |4: >tmp_addr_prf assumption
    1112   ]
    1113 qed.
    1114 
    1115 definition translate_store ≝
    1116   λglobals: list ident.
    1117   λaddr.
    1118   λaddr_prf: 2 = |addr|.
    1119   λsrcrs: list register.
    1120   λstart_lbl: label.
    1121   λdest_lbl: label.
    1122   λdef: rtl_internal_function globals.
    1123   match fresh_regs_strong rtl_params0 globals def (|addr|) with
    1124   [ mk_Sig def_tmp_addr tmp_addr_prf ⇒
    1125     let def ≝ \fst def_tmp_addr in
    1126     let tmp_addr ≝ \snd def_tmp_addr in
    1127     let 〈tmp_addr1, tmp_addr2〉 ≝ make_addr … tmp_addr ? in
    1128     let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
    1129     let 〈def, dummy〉 ≝ fresh_reg rtl_params0 globals def in
    1130     let f ≝ λtranslate_off. λsrcr.
    1131       let 〈translates, off〉 ≝ translate_off in
    1132       let translates ≝ translates @ [
    1133         adds_graph rtl_params1 globals [
    1134           sequential rtl_params_ globals (INT rtl_params_ globals tmpr off)
    1135         ];
    1136         translate_op2 globals Oaddp tmp_addr … addr [dummy; tmpr] ? ?;
    1137         adds_graph rtl_params1 globals [
    1138           sequential rtl_params_ globals (STORE rtl_params_ globals tmp_addr1 tmp_addr2 srcr)
    1139         ]
    1140       ]
    1141       in
    1142         let 〈carry, result〉 ≝ half_add … off int_size in
    1143           〈translates, result〉
    1144     in
    1145     let 〈translates, ignore〉 ≝ foldl … f 〈[ ], zero …〉 srcrs in
    1146       add_translates rtl_params1 globals translates start_lbl dest_lbl def
    1147   ].
    1148   [1: >tmp_addr_prf %
    1149   |2: >tmp_addr_prf normalize
    1150       <addr_prf //
    1151   |3: >tmp_addr_prf <addr_prf //
    1152   |4: >tmp_addr_prf @addr_prf
    1153   ]
    1154 qed.
    1155 
    1156 axiom fake_label: label.
    1157 
    1158 (* XXX: following conversation with CSC about the mix up in extension statements
    1159         and extension instructions in RTL, use fake_label in calls to
    1160         tailcall_* instructions. *)
    1161 definition translate_stmt ≝
    1162   λglobals: list ident.
    1163   λlenv: local_env.
    1164   λlbl: label.
    1165   λstmt.
    1166   λdef: rtl_internal_function globals.
    1167   match stmt with
    1168   [ St_skip lbl' ⇒ add_graph … lbl (GOTO … lbl') def
    1169   | St_cost cost_lbl lbl' ⇒ add_graph rtl_params1 globals lbl (sequential rtl_params_ globals (COST_LABEL rtl_params_ globals cost_lbl) lbl') def
    1170   | St_const destr cst lbl' ⇒
    1171     translate_cst globals cst (find_local_env destr lenv) lbl lbl' def
    1172   | St_op1 ty ty' op1 destr srcr lbl' ⇒
    1173     translate_op1 globals ty ty' op1 (find_local_env destr lenv) (find_local_env srcr lenv) … lbl lbl' def
    1174   | St_op2 op2 destr srcr1 srcr2 lbl' ⇒
    1175     translate_op2 globals op2 (find_local_env destr lenv) ? (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) ? ? lbl lbl' def
    1176     (* XXX: should we be ignoring this? *)
    1177   | St_load ignore addr destr lbl' ⇒
    1178     translate_load globals (find_local_env addr lenv) ? (find_local_env destr lenv) lbl lbl' def
    1179     (* XXX: should we be ignoring this? *)
    1180   | St_store ignore addr srcr lbl' ⇒
    1181     translate_store globals (find_local_env addr lenv) ? (find_local_env srcr lenv) lbl lbl' def
    1182   | St_call_id f args retr lbl' ⇒
    1183     match retr with
    1184     [ Some retr ⇒
    1185       add_graph rtl_params1 globals lbl (sequential … (CALL_ID rtl_params1 globals f (rtl_args args lenv) (find_local_env retr lenv)) lbl') def
    1186     | None ⇒ add_graph rtl_params1 globals lbl (sequential … (CALL_ID rtl_params1 globals f (rtl_args args lenv) [ ]) lbl') def
     1039  |8,9,10,11,12,13:
     1040    cases stmt_typed * #srcrs1_prf #srcrs2_prf #dstr_prf
     1041    [1,2: @(lenv_typed_arg_typed_ok1 … lenv_typed) assumption
     1042    | @(lenv_typed_reg_typed_ok1 … lenv_typed) assumption
     1043    | @(lenv_typed_reg_typed_ok2 … lenv_typed srcrs2_prf)
     1044    | @(lenv_typed_reg_typed_ok2 … lenv_typed srcrs1_prf)
     1045    | @(lenv_typed_reg_typed_ok2 … lenv_typed dstr_prf)
    11871046    ]
    1188   | St_call_ptr f args retr lbl' ⇒
    1189     match retr with
    1190     [ None ⇒
    1191       let 〈f1, f2〉 ≝ find_and_addr f lenv ? in
    1192         add_graph rtl_params1 globals lbl (sequential … (extension … (rtl_st_ext_call_ptr f1 f2 (rtl_args args lenv) [ ])) lbl') def
    1193     | Some retr ⇒
    1194       let 〈f1, f2〉 ≝ find_and_addr f lenv ? in
    1195         add_graph rtl_params1 globals lbl (sequential … (extension … (rtl_st_ext_call_ptr f1 f2 (rtl_args args lenv) (find_local_env retr lenv))) lbl') def
    1196     ]
    1197   | St_tailcall_id f args ⇒
    1198     add_graph rtl_params1 globals lbl (sequential rtl_params_ globals (extension rtl_params_ globals (rtl_st_ext_tailcall_id f (rtl_args args lenv))) fake_label) def
    1199   | St_tailcall_ptr f args ⇒
    1200     let 〈f1, f2〉 ≝ find_and_addr f lenv ? in
    1201       add_graph rtl_params1 globals lbl (sequential rtl_params_ globals (extension rtl_params1 globals (rtl_st_ext_tailcall_ptr f1 f2 (rtl_args args lenv))) fake_label) def
    1202   | St_cond r lbl_true lbl_false ⇒
    1203     translate_cond globals (find_local_env r lenv) lbl lbl_true lbl_false def
    1204   | St_jumptable r l ⇒ ? (* assert false: not implemented yet *)
    1205   | St_return ⇒ add_graph rtl_params1 globals lbl (RETURN …) def
    1206   ].
    1207   [10: cases not_implemented (* jtable case *)
    1208   |*: cases daemon (* TODO: proofs regarding lengths of lists, examine! *)
     1047  |*: whd in stmt_typed; cases daemon (* TODO need more stringent statement_typed *)
    12091048  ]
    12101049qed.
     
    12171056  λglobals: list ident.
    12181057  λdef.
    1219   let runiverse ≝ f_reggen def in
    1220   let 〈lenv,runiverse〉 ≝ initialize_local_env runiverse
    1221     (f_params def @ f_locals def) (f_result def) in
    1222   let params ≝ map_list_local_env lenv (map … \fst (f_params def)) in
    1223   let locals ≝ map_list_local_env lenv (map … \fst (f_locals def)) in
    1224   let result ≝
    1225     match (f_result def) with
    1226     [ None ⇒ [ ]
    1227     | Some r_typ ⇒
    1228       let 〈r, typ〉 ≝ r_typ in
    1229         find_local_env r lenv
    1230     ]
    1231   in
     1058  let runiverse' ≝ f_reggen def in
    12321059  let luniverse' ≝ f_labgen def in
    1233   let runiverse' ≝ runiverse in
    1234   let result' ≝ result in
    1235   let params' ≝ params in
    1236   let locals' ≝ locals in
    12371060  let stack_size' ≝ f_stacksize def in
    12381061  let entry' ≝ f_entry def in
    12391062  let exit' ≝ f_exit def in
    1240   let graph' ≝ add LabelTag ? (empty_map LabelTag ?) entry' (GOTO rtl_params_ globals entry') in
    1241   let graph' ≝ add LabelTag ? graph' exit' (GOTO rtl_params_ globals exit') in
    1242   let res ≝
    1243     mk_joint_internal_function … (rtl_params globals) luniverse' runiverse' result' params'
    1244      locals' stack_size' graph' ? ? in
    1245     foldi … (translate_stmt globals … lenv) (f_graph def) res.
    1246 [ % [@entry' | @graph_add_lookup @graph_add]
    1247 | % [@exit'  | @graph_add]]
     1063  let init ≝ init_graph_if RTL globals luniverse' runiverse' [ ] [ ]
     1064     [ ] stack_size' (pi1 … entry') (pi1 … exit') in
     1065  let 〈init',lenv〉 as pr_eq ≝ initialize_locals_params_ret globals
     1066    (f_locals def) (f_params def) (f_result def) init in
     1067  let vars ≝ (f_locals def) @ (f_params def) @
     1068    match f_result def with [ Some x ⇒ [x] | _ ⇒ [ ] ] in
     1069  let f_trans ≝ λlbl,stmt,def.
     1070    let pr ≝ translate_statement … vars lenv ? stmt ? in
     1071    b_adds_graph … (rtl_fresh_reg …) (dpi1 … pr) lbl (dpi2 … pr) def in
     1072  foldi … f_trans (f_graph def) init'. (* TODO *) cases daemon
    12481073qed.
    12491074
     
    12521077definition rtlabs_to_rtl: RTLabs_program → rtl_program ≝
    12531078 λp. transform_program … p (λvarnames. transf_fundef … (translate_internal varnames)).
    1254 
    1255 *)
    1256 axiom rtlabs_to_rtl: RTLabs_program → rtl_program.
    1257 
Note: See TracChangeset for help on using the changeset viewer.