Changeset 1071


Ignore:
Timestamp:
Jul 15, 2011, 2:40:40 PM (8 years ago)
Author:
mulligan
Message:

changes the specific form that the added proofs take to use None, not Some, hence removing the exitential

Location:
src
Files:
7 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/I8051.ma

    r1066 r1071  
    137137
    138138(* dpm: registers for stack manipulation *)
    139 definition RegisterSST ≝ Register03.
    140 definition RegisterST0 ≝ Register04.
    141 definition RegisterST1 ≝ Register05.
     139definition RegisterSST ≝ Register10.
     140definition RegisterST0 ≝ Register02.
     141definition RegisterST1 ≝ Register03.
     142definition RegisterST2 ≝ Register04.
     143definition RegisterST3 ≝ Register05.
     144definition RegisterSTS ≝ [RegisterST0; RegisterST1; RegisterST2; RegisterST3].
    142145definition RegisterSPL ≝ Register06.
    143146definition RegisterSPH ≝ Register07.
     147definition RegisterRets ≝ [RegisterDPL; RegisterDPH; Register00; Register01].
    144148
    145149definition register_address: Register → [[ acc_a; direct; registr ]] ≝
  • src/ASM/Util.ma

    r1064 r1071  
    215215
    216216let rec reduce
    217   (A: Type[0]) (left: list A) (right: list A) on left ≝
     217  (A: Type[0]) (B: Type[0]) (left: list A) (right: list B) on left ≝
    218218  match left with
    219219  [ nil ⇒ 〈〈[ ], [ ]〉, 〈[ ], right〉〉
     
    222222    [ nil ⇒ 〈〈[ ], left〉, 〈[ ], [ ]〉〉
    223223    | cons hd' tl' ⇒
    224       let 〈cleft, cright〉 ≝ reduce A tl tl' in
     224      let 〈cleft, cright〉 ≝ reduce A B tl tl' in
    225225      let 〈commonl, restl〉 ≝ cleft in
    226226      let 〈commonr, restr〉 ≝ cright in
     
    238238
    239239let rec reduce_strong
    240   (A: Type[0]) (left: list A) (right: list A)
    241     on left : Σret: ((list A) × (list A)) × ((list A) × (list A)). |\fst (\fst ret)| = |\fst (\snd ret)|  ≝
     240  (A: Type[0]) (B: Type[0]) (left: list A) (right: list B)
     241    on left : Σret: ((list A) × (list A)) × ((list B) × (list B)). |\fst (\fst ret)| = |\fst (\snd ret)|  ≝
    242242  match left with
    243243  [ nil ⇒ 〈〈[ ], [ ]〉, 〈[ ], right〉〉
     
    246246    [ nil ⇒ 〈〈[ ], left〉, 〈[ ], [ ]〉〉
    247247    | cons hd' tl' ⇒
    248       let 〈cleft, cright〉 ≝ reduce_strong A tl tl' in
     248      let 〈cleft, cright〉 ≝ reduce_strong A B tl tl' in
    249249      let 〈commonl, restl〉 ≝ cleft in
    250250      let 〈commonr, restr〉 ≝ cright in
     
    255255  | 2: normalize %
    256256  | 3: normalize
    257        generalize in match (sig2 … (reduce_strong A tl tl1));
     257       generalize in match (sig2 … (reduce_strong A B tl tl1));
    258258       >p2 >p3 >p4 normalize in ⊢ (% → ?)
    259259       #HYP //
     
    464464    mapi_internal A B 0 f l.
    465465
     466let rec zip_pottier
     467  (A: Type[0]) (B: Type[0]) (left: list A) (right: list B)
     468    on left ≝
     469  match left with
     470  [ nil ⇒ [ ]
     471  | cons hd tl ⇒
     472    match right with
     473    [ nil ⇒ [ ]
     474    | cons hd' tl' ⇒ 〈hd, hd'〉 :: zip_pottier A B tl tl'
     475    ]
     476  ].
     477
     478let rec zip_safe
     479  (A: Type[0]) (B: Type[0]) (left: list A) (right: list B) (prf: |left| = |right|)
     480    on left ≝
     481  match left return λx. |x| = |right| → list (A × B) with
     482  [ nil ⇒ λnil_prf.
     483    match right return λx. |[ ]| = |x| → list (A × B) with
     484    [ nil ⇒ λnil_nil_prf. [ ]
     485    | cons hd tl ⇒ λnil_cons_absrd. ?
     486    ] nil_prf
     487  | cons hd tl ⇒ λcons_prf.
     488    match right return λx. |hd::tl| = |x| → list (A × B) with
     489    [ nil ⇒ λcons_nil_absrd. ?
     490    | cons hd' tl' ⇒ λcons_cons_prf. 〈hd, hd'〉 :: zip_safe A B tl tl' ?
     491    ] cons_prf
     492  ] prf.
     493  [ 1: normalize in nil_cons_absrd;
     494       destruct(nil_cons_absrd)
     495  | 2: normalize in cons_nil_absrd;
     496       destruct(cons_nil_absrd)
     497  | 3: normalize in cons_cons_prf;
     498       @injective_S
     499       assumption
     500  ]
     501qed.
     502
    466503let rec zip (A: Type[0]) (B: Type[0]) (l: list A) (r: list B) on l: option (list (A × B)) ≝
    467504  match l with
  • src/ERTL/ERTL.ma

    r878 r1071  
    2525  | ertl_st_int: register → Byte → label → ertl_statement
    2626  | ertl_st_move: register → register → label → ertl_statement
    27   | ertl_st_opaccs: OpAccs → register → register → register → label → ertl_statement
     27  | ertl_st_opaccs_a: OpAccs → register → register → register → label → ertl_statement
     28  | ertl_st_opaccs_b: OpAccs → register → register → register → label → ertl_statement
    2829  | ertl_st_op1: Op1 → register → register → label → ertl_statement
    2930  | ertl_st_op2: Op2 → register → register → register → label → ertl_statement
    3031  | ertl_st_clear_carry: label → ertl_statement
     32  | ertl_st_set_carry: label → ertl_statement
    3133  | ertl_st_load: register → register → register → label → ertl_statement
    3234  | ertl_st_store: register → register → register → label → ertl_statement
    3335  | ertl_st_call_id: ident → Byte → label → ertl_statement
    34   | ertl_st_cond_acc: register → label → label → ertl_statement
    35   | ertl_st_return: registers → ertl_statement.
     36  | ertl_st_cond: register → label → label → ertl_statement
     37  | ertl_st_return: ertl_statement. (* XXX: change from o'caml *)
    3638
    3739definition ertl_statement_graph ≝ graph ertl_statement.
     
    4951}.
    5052
    51 inductive ertl_function: Type[0] ≝
    52   | ertl_f_internal: ertl_internal_function → ertl_function
    53   | ertl_f_external: external_function → ertl_function.
     53definition ertl_function ≝ fundef ertl_internal_function.
    5454 
    5555record ertl_program: Type[0] ≝
  • src/RTL/RTL.ma

    r1068 r1071  
    3535  rtl_if_runiverse: universe RegisterTag;
    3636(*  rtl_if_sig: signature;  -- dropped in front end *)
    37   rtl_if_result: registers;
    38   rtl_if_params: registers;
    39   rtl_if_locals: registers;
     37  rtl_if_result   : registers;
     38  rtl_if_params   : registers;
     39  rtl_if_locals   : registers;
    4040  rtl_if_stacksize: nat;
    41   rtl_if_graph: rtl_statement_graph;
    42   rtl_if_entry: label;
    43   rtl_if_exit: label
     41  rtl_if_graph    : rtl_statement_graph;
     42  rtl_if_entry    : Σl: label. lookup ? ? rtl_if_graph l ≠ None ?;
     43  rtl_if_exit     : Σl: label. lookup ? ? rtl_if_graph l ≠ None ?
    4444}.
    4545
  • src/RTL/RTLtoERTL.ma

    r783 r1071  
    11include "RTL/RTL.ma".
    2 include "RTL/RTLTailcall.ma".
     2(* include "RTL/RTLTailcall.ma". *)
    33include "ERTL/ERTL.ma".
    4 include "utilities/RegisterSet.ma".
    54
    65definition change_exit_label ≝
     
    5251definition fresh_label ≝
    5352  λdef.
    54     match fresh LabelTag (ertl_if_luniverse def) with
    55     [ OK lbl_univ ⇒ Some ? (\fst … lbl_univ)
    56     | Error ⇒ None ?
    57     ].
     53    fresh LabelTag (ertl_if_luniverse def).
    5854   
    5955definition change_label ≝
     
    7672  | ertl_st_int r i _ ⇒ ertl_st_int r i l
    7773  | ertl_st_move r1 r2 _ ⇒ ertl_st_move r1 r2 l
    78   | ertl_st_opaccs opaccs d s1 s2 _ ⇒ ertl_st_opaccs opaccs d s1 s2 l
     74  | ertl_st_opaccs_a opaccs d s1 s2 _ ⇒ ertl_st_opaccs_a opaccs d s1 s2 l
     75  | ertl_st_opaccs_b opaccs d s1 s2 _ ⇒ ertl_st_opaccs_b opaccs d s1 s2 l
    7976  | ertl_st_op1 op1 d s1 _ ⇒ ertl_st_op1 op1 d s1 l
    8077  | ertl_st_op2 op2 d s1 s2 _ ⇒ ertl_st_op2 op2 d s1 s2 l
    8178  | ertl_st_clear_carry _ ⇒ ertl_st_clear_carry l
     79  | ertl_st_set_carry _ ⇒ ertl_st_set_carry l
    8280  | ertl_st_load d a1 a2 _ ⇒ ertl_st_load d a1 a2 l
    8381  | ertl_st_store a1 a2 s _ ⇒ ertl_st_store a1 a2 s l
    8482  | ertl_st_call_id f args _ ⇒ ertl_st_call_id f args l
    85   | ertl_st_cond_acc a i1 i2 ⇒ ertl_st_cond_acc a i1 i2
    86   | ertl_st_return a ⇒ ertl_st_return a
    87   ].
    88  
    89 let rec adds_graph (stmt_list: list ertl_statement) (start_lbl: label) (dest_lbl: label) (def: ertl_internal_function): option ertl_internal_function ≝
     83  | ertl_st_cond a i1 i2 ⇒ ertl_st_cond a i1 i2
     84  | ertl_st_return ⇒ ertl_st_return
     85  ].
     86 
     87let rec adds_graph
     88  (stmt_list: list ertl_statement) (start_lbl: label)
     89  (dest_lbl: label) (def: ertl_internal_function)
     90    on stmt_list ≝
    9091  match stmt_list with
    91   [ nil ⇒ Some ? def
    92   | cons hd tl
    93     match tl with
    94     [ nil ⇒ Some ? (add_graph start_lbl (change_label dest_lbl hd) def)
     92  [ nil ⇒ add_graph start_lbl (ertl_st_skip dest_lbl) def
     93  | cons stmt stmt_list
     94    match stmt_list with
     95    [ nil ⇒ add_graph start_lbl (change_label dest_lbl stmt) def
    9596    | _ ⇒
    96       let tmp_lbl ≝ fresh_label def in
    97       match tmp_lbl with
    98       [ Some tmp_lbl ⇒
    99         let stmt ≝ change_label tmp_lbl hd in
    100         let def ≝ add_graph start_lbl hd def in
    101           adds_graph tl tmp_lbl dest_lbl def
    102       | None ⇒ None ?
    103       ]
    104     ]
    105   ].
    106 
    107 let rec add_translates (translate_list: list (label → label → ertl_internal_function → option ertl_internal_function))
    108                        (start_lbl: label) (dest_lbl: label)
    109                        (def: ertl_internal_function): option ertl_internal_function ≝
     97      let 〈tmp_lbl, nuniv〉 ≝ fresh_label def in
     98      let stmt ≝ change_label tmp_lbl stmt in
     99      let def ≝ add_graph start_lbl stmt def in
     100        adds_graph stmt_list tmp_lbl dest_lbl def
     101    ]
     102  ].
     103
     104let rec add_translates
     105  (translate_list: list ?) (start_lbl: label) (dest_lbl: label)
     106  (def: ertl_internal_function)
     107    on translate_list ≝
    110108  match translate_list with
    111   [ nil ⇒ Some ? def
    112   | cons hd tl
    113     match tl with
    114     [ nil ⇒ hd start_lbl dest_lbl def
     109  [ nil ⇒ add_graph start_lbl (ertl_st_skip dest_lbl) def
     110  | cons trans translate_list
     111    match translate_list with
     112    [ nil ⇒ trans start_lbl dest_lbl def
    115113    | _ ⇒
    116       let tmp_lbl ≝ fresh_label def in
    117       match tmp_lbl with
    118       [ Some tmp_lbl ⇒
    119         match hd start_lbl tmp_lbl def with
    120         [ Some def ⇒ add_translates tl tmp_lbl dest_lbl def
    121         | None ⇒ None ?
    122         ]
    123       | None ⇒ None ?
    124       ]
    125     ]
    126   ].
    127  
    128 axiom fresh_reg: ertl_internal_function → ertl_internal_function × register.
    129 
    130 let rec fresh_regs (def: ertl_internal_function) (n: nat) on n ≝
     114      let 〈tmp_lbl, nuniv〉 ≝ fresh_label def in
     115      let def ≝ trans start_lbl tmp_lbl def in
     116        add_translates translate_list tmp_lbl dest_lbl def
     117    ]
     118  ].
     119
     120axiom register_fresh: universe RegisterTag → register.
     121
     122definition fresh_reg: ertl_internal_function → ertl_internal_function × register ≝
     123  λdef.
     124    let r ≝ register_fresh (ertl_if_runiverse def) in
     125    let locals ≝ r :: ertl_if_locals def in
     126    let ertl_if_luniverse' ≝ ertl_if_luniverse def in
     127    let ertl_if_runiverse' ≝ ertl_if_runiverse def in
     128    let ertl_if_params' ≝ ertl_if_params def in
     129    let ertl_if_locals' ≝ locals in
     130    let ertl_if_stacksize' ≝ ertl_if_stacksize def in
     131    let ertl_if_graph' ≝ ertl_if_graph def in
     132    let ertl_if_entry' ≝ ertl_if_entry def in
     133    let ertl_if_exit' ≝ ertl_if_exit def in
     134      〈mk_ertl_internal_function
     135        ertl_if_luniverse' ertl_if_runiverse' ertl_if_params'
     136        ertl_if_locals' ertl_if_stacksize' ertl_if_graph'
     137        ertl_if_entry' ertl_if_exit', r〉.
     138
     139let rec fresh_regs
     140  (def: ertl_internal_function) (n: nat)
     141    on n ≝
    131142  match n with
    132143  [ O ⇒ 〈def, [ ]〉
     
    169180definition get_params_hdw ≝
    170181  λparams: list register.
    171   match length ? params with
    172   [ O ⇒ Some ? [ get_params_hdw_internal ]
     182  match params with
     183  [ nil ⇒ [get_params_hdw_internal]
    173184  | _ ⇒
    174     match zip ? ? params parameters with
    175     [ None ⇒ None ?
    176     | Some l ⇒ Some ? (save_hdws l)
    177     ]
     185    let l ≝ zip_pottier ? ? params parameters in
     186      save_hdws l
    178187  ].
    179188
     
    186195  let 〈def, addr2〉 ≝ fresh_reg def in
    187196  let 〈def, tmpr〉 ≝ fresh_reg def in
    188   let 〈int_offset, ignore〉 ≝ add_8_with_carry (bitvector_of_nat ? off) int_size false in
     197  let 〈carry, int_offset〉 ≝ half_add ? (bitvector_of_nat ? off) int_size in
    189198  adds_graph [
    190199    ertl_st_frame_size addr1 start_lbl;
     
    199208  ] start_lbl dest_lbl def.
    200209 
    201 definition get_params_stack_internal ≝
    202   λi.
    203   λr.
    204     get_param_stack i r.
    205  
    206210definition get_params_stack ≝
    207211  λparams.
    208   match length ? params with
    209   [ O ⇒ [ get_params_hdw_internal ]
    210   | _ ⇒ mapi ? ? get_params_stack_internal params
     212  match params with
     213  [ nil ⇒ [ λstart_lbl. adds_graph [ertl_st_skip start_lbl] start_lbl ]
     214  | _ ⇒
     215    let f ≝ λi. λr. get_param_stack i r in
     216      mapi ? ? f params
    211217  ].
    212218
     
    215221  let n ≝ min (length ? params) (length ? parameters) in
    216222  let 〈hdw_params, stack_params〉 ≝ list_split ? n params in
    217   match get_params_hdw hdw_params with
    218   [ None ⇒ None ?
    219   | Some hdw_params ⇒ Some ? (hdw_params @ (get_params_stack stack_params))
    220   ].
     223  let hdw_params ≝ get_params_hdw hdw_params in
     224    hdw_params @ (get_params_stack stack_params).
    221225 
    222226definition add_prologue ≝
    223   λparams.
     227  λparams: list register.
    224228  λsral.
    225229  λsrah.
     
    227231  λdef.
    228232  let start_lbl ≝ ertl_if_entry def in
    229   let tmp_lbl ≝ fresh_label def in
    230   match tmp_lbl with
    231   [ None ⇒ None ?
    232   | Some tmp_lbl ⇒
    233     let last_stmt ≝ lookup ? ? (ertl_if_graph def) start_lbl in
    234     let params ≝
    235       match get_params params with
    236       [ Some params ⇒ params
    237       | None ⇒ [ ] (* dpm: is this ok? *)
    238       ] in
     233  let 〈tmp_lbl, nuniv〉 ≝ fresh_label def in
     234  match lookup ? ? (ertl_if_graph def) start_lbl with
     235  [ None ⇒ ?
     236  | Some last_stmt ⇒
    239237    let def ≝
    240       add_translates (
    241         adds_graph [ ertl_st_new_frame start_lbl ] ::
    242         adds_graph [ ertl_st_pop sral start_lbl; ertl_st_pop srah start_lbl ] ::
    243         save_hdws sregs @
    244         params) start_lbl tmp_lbl def in
    245     match def with
    246     [ Some def ⇒
    247       match last_stmt with
    248       [ Some last_stmt ⇒ Some ? (add_graph tmp_lbl last_stmt def)
    249       | None ⇒ None ?
    250       ]
    251     | None ⇒ None ?
    252     ]
    253   ].
     238      add_translates
     239         ((adds_graph [
     240                     ertl_st_new_frame start_lbl
     241                   ]) ::
     242         (adds_graph [
     243                      ertl_st_pop sral start_lbl;
     244                      ertl_st_pop srah start_lbl
     245                   ]) ::
     246         (save_hdws sregs) @
     247         (get_params params))
     248        start_lbl tmp_lbl def
     249    in
     250      add_graph tmp_lbl last_stmt def
     251  ].
     252  cases not_implemented (* until Brian gives goahead for dep. types *)
     253qed.
     254
     255definition save_return ≝
     256  λret_regs.
     257  λstart_lbl: label.
     258  λdest_lbl: label.
     259  λdef: ertl_internal_function.
     260  let 〈def, tmpr〉 ≝ fresh_reg def in
     261  match reduce_strong ? RegisterSTS ret_regs with
     262  [ dp crl crl_proof ⇒
     263    let commonl ≝ \fst (\fst crl) in
     264    let commonr ≝ \fst (\snd crl) in
     265    let restl ≝ \snd (\fst crl) in
     266    let restr ≝ \snd (\snd crl) in
     267    let init_tmpr ≝ ertl_st_int tmpr (zero ?) start_lbl in
     268    let f_save ≝ λst. λr. ertl_st_set_hdw st r start_lbl in
     269    let saves ≝ map2 ? ? ? f_save commonl commonr ? in
     270    let f_default ≝ λst. ertl_st_set_hdw st tmpr start_lbl in
     271    let defaults ≝ map ? ? f_default restl in
     272      adds_graph (init_tmpr :: saves @ defaults) start_lbl dest_lbl def
     273  ].
     274
     275let save_return ret_regs start_lbl dest_lbl def =
     276  let (def, tmpr) = fresh_reg def in
     277  let ((common1, rest1), (common2, _)) =
     278    MiscPottier.reduce I8051.sts ret_regs in
     279  let init_tmpr = ERTL.St_int (tmpr, 0, start_lbl) in
     280  let f_save st r = ERTL.St_set_hdw (st, r, start_lbl) in
     281  let saves = List.map2 f_save common1 common2 in
     282  let f_default st = ERTL.St_set_hdw (st, tmpr, start_lbl) in
     283  let defaults = List.map f_default rest1 in
     284  adds_graph (init_tmpr :: saves @ defaults) start_lbl dest_lbl def
    254285 
    255286definition allocate_regs_internal ≝
  • src/RTLabs/RTLAbstoRTL.ma

    r1068 r1071  
    22include "RTL/RTL.ma".
    33include "common/AssocList.ma".
     4include "common/FrontEndOps.ma".
    45include "common/Graphs.ma".
    5 include "common/FrontEndOps.ma".
     6
     7axiom graph_add_lookup:
     8  ∀g: graph rtl_statement.
     9  ∀l: label.
     10  ∀s: rtl_statement.
     11  ∀to_insert: label.
     12    lookup ? ? g l ≠ None ? → lookup ? ? (add ? ? g to_insert s) l ≠ None ?.
    613
    714definition add_graph ≝
     
    2027    mk_rtl_internal_function rtl_if_luniverse' rtl_if_runiverse'
    2128                             rtl_if_params' rtl_if_params' rtl_if_locals'
    22                              rtl_if_stacksize' rtl_if_graph' rtl_if_entry'
    23                              rtl_if_exit'.
     29                             rtl_if_stacksize' rtl_if_graph' ? ?.
     30  [1: cases(rtl_if_entry')
     31      #LABEL #HYP
     32      %
     33      [1: @LABEL
     34      |2: cases(HYP)
     35          #STMT
     36          #FRST_PRF
     37          %
     38          [1: @STMT
     39          |2: <FRST_PRF @(graph_add_lookup (rtl_if_graph p) LABEL stmt)
     40          ]
     41      ]
     42 
    2443     
    2544definition fresh_label: rtl_internal_function → rtl_internal_function × label ≝
     
    316335  λsrcrs: list register.
    317336  λstart_lbl: label.
    318     match reduce_strong register destrs srcrs with
     337    match reduce_strong register register destrs srcrs with
    319338    [ dp crl_crr len_proof ⇒
    320339      let commonl ≝ \fst (\fst crl_crr) in
     
    399418      translate_move destrs srcrs
    400419    else
    401       match reduce_strong ? destrs srcrs with
     420      match reduce_strong register register destrs srcrs with
    402421      [ dp crl len_proof ⇒
    403422        let commonl ≝ \fst (\fst crl) in
     
    510529  λdest_lbl.
    511530  λdef.
    512   match reduce_strong ? srcrs1 srcrs2 with
     531  match reduce_strong register register srcrs1 srcrs2 with
    513532  [ dp reduced first_reduced_proof ⇒
    514533    let srcrsl_common ≝ \fst (\fst reduced) in
     
    517536    let srcrsr_rest ≝ \snd (\snd reduced) in
    518537    let srcrs_rest ≝ choose_rest ? srcrsl_rest srcrsr_rest ? ? in
    519     match reduce_strong ? destrs srcrsl_common with
     538    match reduce_strong register register destrs srcrsl_common with
    520539    [ dp reduced second_reduced_proof ⇒
    521540      let destrs_common ≝ \fst (\fst reduced) in
    522541      let destrs_rest ≝ \snd (\fst reduced) in
    523       match reduce_strong ? destrs_rest srcrs_rest with
     542      match reduce_strong register register destrs_rest srcrs_rest with
    524543      [ dp reduced third_reduced_proof ⇒
    525544        let destrs_cted ≝ \fst (\fst reduced) in
     
    704723    let 〈def, tmp_srcrs2〉 ≝ fresh_regs def (|srcrs2|) in
    705724    let save_srcrs2 ≝ translate_move tmp_srcrs2 srcrs2 in
    706     match reduce_strong ? tmp_srcrs1 tmp_srcrs2 with
     725    match reduce_strong register register tmp_srcrs1 tmp_srcrs2 with
    707726    [ dp crl their_proof ⇒
    708727      let commonl ≝ \fst (\fst crl) in
  • src/RTLabs/syntax.ma

    r1070 r1071  
    3535; f_stacksize : nat
    3636; f_graph     : graph statement
    37 ; f_entry     : Σl:label. ∃s. lookup ?? f_graph l = Some ? s
    38 ; f_exit      : Σl:label. ∃s. lookup ?? f_graph l = Some ? s
     37; f_entry     : Σl:label. lookup ?? f_graph l ≠ None ?
     38; f_exit      : Σl:label. lookup ?? f_graph l ≠ None ?
    3939}.
    4040
Note: See TracChangeset for help on using the changeset viewer.