Changeset 1556


Ignore:
Timestamp:
Nov 24, 2011, 5:24:10 PM (8 years ago)
Author:
mulligan
Message:

submitting to avoid conflicts

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r1555 r1556  
    13071307 λl:list labelled_instruction.
    13081308 λacc.
    1309   foldl ??
     1309  foldl
    13101310   (λt,i.
    13111311       match t with
    1312        [ None ⇒ None ?
     1312       [ None ⇒ None
    13131313       | Some ppc_pc_map ⇒
    13141314         let 〈ppc,pc_map〉 ≝ ppc_pc_map in
     
    13191319           | Some pc_ignore ⇒
    13201320              let 〈pc,ignore〉 ≝ pc_ignore in
    1321               Some … 〈S ppc,〈pc, insert ? ? (bitvector_of_nat ? ppc) (bitvector_of_nat ? pc) sigma_map〉〉 ]
     1321                Some … 〈S ppc, 〈pc, insert ?? (bitvector_of_nat 16 ppc) (bitvector_of_nat 16 pc) sigma_map〉〉 ]
    13221322       ]) acc l.
    13231323
    1324 definition sigma0: pseudo_assembly_program → policy_type → option (nat × (nat × (BitVectorTrie Word 16)))
    1325  ≝ λprog.λjump_expansion.sigma00 prog jump_expansion (\snd prog) (Some ? 〈0, 〈0, (Stub ? ?)〉〉).
     1324definition sigma0: pseudo_assembly_program → policy_type → option (nat × (nat × (BitVectorTrie Word 16))) ≝
     1325  λprog.
     1326  λjump_expansion.
     1327    sigma00 prog jump_expansion (\snd prog) (Some ? 〈0, 〈0, Stub …〉〉).
    13261328
    13271329definition tech_pc_sigma00: pseudo_assembly_program → policy_type → list labelled_instruction → option (nat × nat) ≝
     
    13441346        None ?
    13451347      else
    1346         Some ? (λx.lookup ?? x sigma_map (zero …)) ].
     1348        Some ? (λx. lookup … x sigma_map (zero …)) ].
    13471349
    13481350(* stuff about policy *)
     
    14271429  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pc.
    14281430  lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
    1429   lookup_datalabels = (λx. lookup ?? x (construct_datalabels (\fst program)) (zero ?)) →
     1431  lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
    14301432  let pi ≝ \fst (fetch_pseudo_instruction (\snd program) ppc) in
    14311433  pc = sigma program pol ppc →
     
    14361438    | Some res ⇒ res ].
    14371439 [ @⊥ whd in p:(??%??);
    1438    generalize in match (sig2 ?? pol) whd in ⊢ (% → ?)
    1439    whd in ⊢ (?(??%?) → ?) change in ⊢ (?(??(match % with [_ ⇒ ? | _ ⇒ ?])?) → ?) with (sigma00 ????)
    1440    generalize in match (refl … (sigma00 program pol (\snd program) (Some ? 〈O,〈O,Stub (BitVector 16) 16〉〉)))
    1441    cases (sigma00 ????) in ⊢ (??%? → %) normalize nodelta [#_ * #abs @abs %]
     1440   generalize in match (sig2 ?? pol); whd in ⊢ (% → ?);
     1441   whd in ⊢ (?(??%?) → ?); change with (sigma00 ????) in ⊢ (?(??(match % with [_ ⇒ ? | _ ⇒ ?])?) → ?);
     1442   generalize in match (refl … (sigma00 program pol (\snd program) (Some ? 〈O,〈O,Stub (BitVector 16) 16〉〉)));
     1443   cases (sigma00 ????) in ⊢ (??%? → %); normalize nodelta [#_ * #abs @abs %]
    14421444   #res #K
    14431445   cases (fetch_pseudo_instruction_split (\snd program) ppc) #pre * #suff * #lbl #EQ1
    1444    generalize in match (policy_ok_prefix_hd_ok program pol … EQ1 ?) in ⊢ ?
     1446   generalize in match (policy_ok_prefix_hd_ok program pol … EQ1 ?) in ⊢ ?;
    14451447   cases daemon (* CSC: XXXXXXXX Ero qui
    14461448   
     
    14611463  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.
    14621464  lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
    1463   lookup_datalabels = (λx. lookup ?? x (construct_datalabels (\fst program)) (zero ?)) →
     1465  lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
    14641466  \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
    14651467  Σres:(nat × (list Byte)).
     
    14781480    [ None ⇒ let dummy ≝ 〈0,[ ]〉 in dummy
    14791481    | Some res ⇒ res ].
    1480  [ @⊥ elim pi in p [*]
     1482 [ @⊥ elim pi in p; [*]
    14811483   try (#ARG1 #ARG2 #ARG3 #abs) try (#ARG1 #ARG2 #abs) try (#ARG1 #abs) try #abs
    1482    generalize in match (jmeq_to_eq ??? abs) -abs; #abs whd in abs:(??%?); try destruct(abs)
     1484   generalize in match (jmeq_to_eq ??? abs); -abs; #abs whd in abs:(??%?); try destruct(abs)
    14831485   whd in abs:(??match % with [_ ⇒ ? | _ ⇒ ?]?);
    14841486   (* WRONG HERE, NEEDS LEMMA SAYING THAT THE POLICY DOES NOT RETURN MEDIUM! *)
     
    14941496  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.
    14951497  lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
    1496   lookup_datalabels = (λx. lookup ?? x (construct_datalabels (\fst program)) (zero ?)) →
     1498  lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
    14971499  \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
    14981500   nat × (list Byte)
     
    15051507  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.
    15061508  ∀prf1:lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)).
    1507   ∀prf2:lookup_datalabels = (λx. lookup ?? x (construct_datalabels (\fst program)) (zero ?)).
     1509  ∀prf2:lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)).
    15081510  ∀prf3:\fst (fetch_pseudo_instruction (\snd program) ppc) = pi.
    15091511     Some … (assembly_1_pseudoinstruction program pol ppc lookup_labels lookup_datalabels pi prf1 prf2 prf3)
     
    15171519definition construct_costs':
    15181520 ∀program. ∀pol:policy program. ∀ppc,pc,costs,i.
    1519   Σres:(nat × (BitVectorTrie Word 16)). Some … res = construct_costs_safe program pol ppc pc costs i
     1521  Σres:(nat × (BitVectorTrie costlabel 16)). Some … res = construct_costs_safe program pol ppc pc costs i
    15201522
    15211523  λprogram.λpol: policy program.λppc,pc,costs,i.
    15221524   match construct_costs_safe program pol ppc pc costs i with
    1523     [ None ⇒ let dummy ≝ 〈0, Stub ??〉 in dummy
     1525    [ None ⇒ let dummy ≝ 〈0, Stub costlabel 16〉 in dummy
    15241526    | Some res ⇒ res ].
    15251527 [ cases daemon
     
    16131615   tech_pc_sigma00 program pol (prefix@[〈label,i〉]) = Some … 〈S ppc,\fst (construct_costs program pol … ppc pc costs i)〉.
    16141616
     1617lemma eq_identifier_eq:
     1618  ∀tag: String.
     1619  ∀l.
     1620  ∀r.
     1621    eq_identifier tag l r = true → l = r.
     1622  #tag #l #r cases l cases r #posl #posr
     1623  cases daemon
     1624qed.
     1625
    16151626definition build_maps:
    16161627 ∀pseudo_program.∀pol:policy pseudo_program.
    1617   Σres:((BitVectorTrie Word 16) × (BitVectorTrie Word 16)).
     1628  Σres:((identifier_map ASMTag Word) × (BitVectorTrie costlabel 16)).
     1629   let 〈labels, costs〉 ≝ res in
     1630    ∀id. occurs_exactly_once id (\snd pseudo_program) →
     1631     lookup_def … labels id (zero ?) = sigma pseudo_program pol (address_of_word_labels_code_mem (\snd pseudo_program) id) ≝
     1632  λpseudo_program.
     1633  λpol:policy pseudo_program.
     1634    let result ≝
     1635      foldl_strong
     1636        (option Identifier × pseudo_instruction)
     1637          (λpre. Σres:((identifier_map ASMTag Word) × (nat × (nat × (BitVectorTrie costlabel 16)))).
     1638            let 〈labels,ppc_pc_costs〉 ≝ res in
     1639            let 〈ppc',pc_costs〉 ≝ ppc_pc_costs in
     1640            let 〈pc',costs〉 ≝ pc_costs in
     1641              And ( And (
     1642              And (bitvector_of_nat ? pc' = sigma pseudo_program pol (bitvector_of_nat ? ppc')) (*∧*)
     1643                (ppc' = length … pre)) (*∧ *)
     1644                (tech_pc_sigma00 pseudo_program (eject … pol) pre = Some ? 〈ppc',pc'〉)) (*∧*)
     1645                (∀id. occurs_exactly_once id pre →
     1646                  lookup_def … labels id (zero …) = sigma pseudo_program pol (address_of_word_labels_code_mem pre id)))
     1647                (\snd pseudo_program)
     1648        (λprefix,i,tl,prf,t.
     1649          let 〈labels, ppc_pc_costs〉 ≝ t in
     1650          let 〈ppc, pc_costs〉 ≝ ppc_pc_costs in
     1651          let 〈pc,costs〉 ≝ pc_costs in
     1652          let 〈label, i'〉 ≝ i in
     1653          let labels ≝
     1654            match label with
     1655            [ None ⇒ labels
     1656            | Some label ⇒
     1657                let program_counter_bv ≝ bitvector_of_nat ? pc in
     1658                  add ? ? labels label program_counter_bv
     1659            ]
     1660          in
     1661            let construct ≝ construct_costs pseudo_program pol ppc pc costs i' in
     1662              〈labels, 〈S ppc,construct〉〉) 〈empty_map …, 〈0, 〈0, Stub ? ?〉〉〉
     1663    in
     1664      let 〈labels, ppc_pc_costs〉 ≝ result in
     1665      let 〈ppc,pc_costs〉 ≝ ppc_pc_costs in
     1666      let 〈pc, costs〉 ≝ pc_costs in
     1667        〈labels, costs〉.
     1668 [2: whd generalize in match (sig2 … t); >p >p1 >p2 >p3 * * * #IHn1 #IH0 #IH1 #IH2
     1669   generalize in match (refl … construct); cases construct in ⊢ (???% → %); #PC #CODE #JMEQ % [% [%]]
     1670   [ <(construct_costs_sigma … costs i1 IHn1) change with (? = ?(\fst construct)) >JMEQ %
     1671   | >append_length <IH0 normalize; -IHn1; (*CSC: otherwise it diverges!*) //
     1672   | >(tech_pc_sigma00_append_Some … costs … IH1) change with (Some … 〈S ppc,\fst construct〉 = ?) >JMEQ %
     1673   | #id normalize nodelta; -labels1; cases label; normalize nodelta
     1674     [ #K <address_of_word_labels_code_mem_None [2:@K] @IH2 -IHn1; (*CSC: otherwise it diverges!*) //
     1675     | #l #H generalize in match (occurs_exactly_once_Some ???? H) in ⊢ ?;
     1676       generalize in match (refl … (eq_identifier ? l id)); cases (eq_identifier … l id) in ⊢ (???% → %);
     1677        [ #EQ #_ <(eq_identifier_eq … EQ) check lookup_add_hit. >lookup_insert_hit >address_of_word_labels_code_mem_Some_hit
     1678          <IH0 [@IHn1 | <(eq_bv_eq … EQ) in H #H @H]
     1679        | #EQ change with (occurs_exactly_once ?? → ?) #K >lookup_insert_miss [2: -IHn1; (*Andrea:XXXX used to work /2/*)>eq_bv_sym >EQ // ]
     1680          <(address_of_word_labels_code_mem_Some_miss … EQ … H) @IH2 -IHn1; //]]]
     1681 |3: whd % [% [%]] // [>sigma_0//] #id normalize in ⊢ (% → ?); #abs @⊥ //
     1682 | generalize in match (sig2 … result) in ⊢ ?;
     1683   normalize nodelta in p ⊢ %; -result; >p in ⊢ (match % with [_ ⇒ ?] → ?);
     1684   normalize nodelta; >p1 normalize nodelta; >p2; normalize nodelta; * #_; #H @H]
     1685qed.
     1686
     1687definition build_maps:
     1688 ∀pseudo_program.∀pol:policy pseudo_program.
     1689  Σres:((BitVectorTrie Identifier 16) × (BitVectorTrie costlabel 16)).
    16181690   let 〈labels,costs〉 ≝ res in
    16191691    ∀id. occurs_exactly_once id (\snd pseudo_program) →
    1620      lookup ?? id labels (zero …) = sigma pseudo_program pol (address_of_word_labels_code_mem (\snd pseudo_program) id)
    1621 
     1692     lookup ? ? id labels (zero …) = ? (* sigma pseudo_program pol (address_of_word_labels_code_mem (\snd pseudo_program) id) *)
     1693 ?.
    16221694  λpseudo_program.λpol:policy pseudo_program.
    16231695  let result ≝
    16241696   foldl_strong
    16251697    (option Identifier × pseudo_instruction)
    1626     (λpre. Σres:((BitVectorTrie Word 16) × (nat × (nat × (BitVectorTrie Word 16)))).
     1698    (λpre. Σres:((BitVectorTrie Word 16) × (nat × (nat × (BitVectorTrie costlabel 16)))).
    16271699      let 〈labels,ppc_pc_costs〉 ≝ res in
    16281700      let 〈ppc',pc_costs〉 ≝ ppc_pc_costs in
  • src/ASM/CostsProof.ma

    r1554 r1556  
    290290include alias "arithmetics/nat.ma".
    291291
    292 (*Useless now?
     292(*
    293293lemma minus_m_n_minus_minus_plus_1:
    294294  ∀m, n: nat.
     
    297297 /3 by lt_plus_to_minus_r, plus_minus/
    298298qed.
     299*)
    299300
    300301lemma plus_minus_rearrangement_1:
     
    313314    (m - n) + (n - o) = m - o.
    314315 /2 by plus_minus_rearrangement_1/
    315 qed.*)
     316qed.
    316317
    317318(*
     
    344345    normalize @compute_max_trace_any_label_cost_is_ok
    345346  |2:
     347    cases the_trace
     348    [1:
     349      #start_status #final_status #is_next #is_not_return #is_costed
     350      normalize nodelta;
     351      change with (
     352        let current_instruction_cost ≝ current_instruction_cost start_status in 
     353        let call_trace_cost ≝ compute_max_trace_label_return_cost cost_labels start_fun_call after_fun_call call_trace in 
     354        let final_trace_cost ≝ compute_max_trace_any_label_cost cost_labels end_flag after_fun_call final final_trace in 
     355        call_trace_cost+current_instruction_cost+final_trace_cost
     356      ) in ⊢ (??%?);
     357    |2:
     358      #start_status #final_status #is_next #is_return
     359    |3:
     360      #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
     361      #status_final #is_next #is_call #is_after_return #fun_call_trace #after_fun_call_trace
     362      change with (
     363        let current_instruction_cost ≝ current_instruction_cost status_pre_fun_call in 
     364        let call_trace_cost ≝ compute_max_trace_label_return_cost cost_labels status_start_fun_call status_after_fun_call fun_call_trace in 
     365        let final_trace_cost ≝ compute_max_trace_any_label_cost cost_labels end_flag status_after_fun_call status_final after_fun_call_trace in 
     366          call_trace_cost+current_instruction_cost+final_trace_cost) in ⊢ (??%?);
     367      normalize nodelta;
     368      >compute_max_trace_label_return_cost_is_ok
     369      >compute_max_trace_any_label_cost_is_ok
     370    |4:
     371    ]
    346372  |3:
    347373    cases the_trace
     
    353379      normalize >compute_max_trace_label_label_cost_is_ok
    354380      >compute_max_trace_label_return_cost_is_ok
     381      >plus_minus_rearrangement_1
     382      [1: %
     383      |2:
     384      |3:
     385      ]
    355386    ]
    356387  ].
Note: See TracChangeset for help on using the changeset viewer.