Changeset 1556 for src/ASM

Timestamp:

Nov 24, 2011, 5:24:10 PM (9 years ago)

Author:

mulligan

Message:

submitting to avoid conflicts

Location:

src/ASM

Files:

• Assembly.ma (modified) (11 diffs)
• CostsProof.ma (modified) (5 diffs)

src/ASM/Assembly.ma

@@ -1307 +1307 @@
  λl:list labelled_instruction.
  λacc.
-  foldl ??
+  foldl …
    (λt,i.
        match t with
-       [ None ⇒ None ?
+       [ None ⇒ None …
        | Some ppc_pc_map ⇒
          let 〈ppc,pc_map〉 ≝ ppc_pc_map in
@@ -1319 +1319 @@
            | Some pc_ignore ⇒
               let 〈pc,ignore〉 ≝ pc_ignore in
-              Some … 〈S ppc,〈pc, insert ? ? (bitvector_of_nat ? ppc) (bitvector_of_nat ? pc) sigma_map〉〉 ]
+                Some … 〈S ppc, 〈pc, insert ?? (bitvector_of_nat 16 ppc) (bitvector_of_nat 16 pc) sigma_map〉〉 ]
        ]) acc l.
 
-definition sigma0: pseudo_assembly_program → policy_type → option (nat × (nat × (BitVectorTrie Word 16)))
- ≝ λprog.λjump_expansion.sigma00 prog jump_expansion (\snd prog) (Some ? 〈0, 〈0, (Stub ? ?)〉〉).
+definition sigma0: pseudo_assembly_program → policy_type → option (nat × (nat × (BitVectorTrie Word 16))) ≝
+  λprog.
+  λjump_expansion.
+    sigma00 prog jump_expansion (\snd prog) (Some ? 〈0, 〈0, Stub …〉〉).
 
 definition tech_pc_sigma00: pseudo_assembly_program → policy_type → list labelled_instruction → option (nat × nat) ≝
@@ -1344 +1346 @@
         None ?
       else
-        Some ? (λx.lookup ?? x sigma_map (zero …)) ].
+        Some ? (λx. lookup … x sigma_map (zero …)) ].
 
 (* stuff about policy *)
@@ -1427 +1429 @@
   ∀ppc:Word.∀lookup_labels,lookup_datalabels,pc.
   lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
-  lookup_datalabels = (λx. lookup ?? x (construct_datalabels (\fst program)) (zero ?)) →
+  lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
   let pi ≝ \fst (fetch_pseudo_instruction (\snd program) ppc) in
   pc = sigma program pol ppc →
@@ -1436 +1438 @@
     | Some res ⇒ res ].
  [ @⊥ whd in p:(??%??);
-   generalize in match (sig2 ?? pol) whd in ⊢ (% → ?)
-   whd in ⊢ (?(??%?) → ?) change in ⊢ (?(??(match % with [_ ⇒ ? | _ ⇒ ?])?) → ?) with (sigma00 ????)
-   generalize in match (refl … (sigma00 program pol (\snd program) (Some ? 〈O,〈O,Stub (BitVector 16) 16〉〉)))
-   cases (sigma00 ????) in ⊢ (??%? → %) normalize nodelta [#_ * #abs @abs %]
+   generalize in match (sig2 ?? pol); whd in ⊢ (% → ?);
+   whd in ⊢ (?(??%?) → ?); change with (sigma00 ????) in ⊢ (?(??(match % with [_ ⇒ ? | _ ⇒ ?])?) → ?);
+   generalize in match (refl … (sigma00 program pol (\snd program) (Some ? 〈O,〈O,Stub (BitVector 16) 16〉〉)));
+   cases (sigma00 ????) in ⊢ (??%? → %); normalize nodelta [#_ * #abs @abs %]
    #res #K
    cases (fetch_pseudo_instruction_split (\snd program) ppc) #pre * #suff * #lbl #EQ1
-   generalize in match (policy_ok_prefix_hd_ok program pol … EQ1 ?) in ⊢ ?
+   generalize in match (policy_ok_prefix_hd_ok program pol … EQ1 ?) in ⊢ ?;
    cases daemon (* CSC: XXXXXXXX Ero qui
    
@@ -1461 +1463 @@
   ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.
   lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
-  lookup_datalabels = (λx. lookup ?? x (construct_datalabels (\fst program)) (zero ?)) →
+  lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
   \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
   Σres:(nat × (list Byte)).
@@ -1478 +1480 @@
     [ None ⇒ let dummy ≝ 〈0,[ ]〉 in dummy 
     | Some res ⇒ res ].
- [ @⊥ elim pi in p [*]
+ [ @⊥ elim pi in p; [*]
    try (#ARG1 #ARG2 #ARG3 #abs) try (#ARG1 #ARG2 #abs) try (#ARG1 #abs) try #abs
-   generalize in match (jmeq_to_eq ??? abs) -abs; #abs whd in abs:(??%?); try destruct(abs)
+   generalize in match (jmeq_to_eq ??? abs); -abs; #abs whd in abs:(??%?); try destruct(abs)
    whd in abs:(??match % with [_ ⇒ ? | _ ⇒ ?]?);
    (* WRONG HERE, NEEDS LEMMA SAYING THAT THE POLICY DOES NOT RETURN MEDIUM! *)
@@ -1494 +1496 @@
   ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.
   lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
-  lookup_datalabels = (λx. lookup ?? x (construct_datalabels (\fst program)) (zero ?)) →
+  lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
   \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
    nat × (list Byte)
@@ -1505 +1507 @@
   ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.
   ∀prf1:lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)).
-  ∀prf2:lookup_datalabels = (λx. lookup ?? x (construct_datalabels (\fst program)) (zero ?)).
+  ∀prf2:lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)).
   ∀prf3:\fst (fetch_pseudo_instruction (\snd program) ppc) = pi.
      Some … (assembly_1_pseudoinstruction program pol ppc lookup_labels lookup_datalabels pi prf1 prf2 prf3)
@@ -1517 +1519 @@
 definition construct_costs':
  ∀program. ∀pol:policy program. ∀ppc,pc,costs,i.
-  Σres:(nat × (BitVectorTrie Word 16)). Some … res = construct_costs_safe program pol ppc pc costs i
+  Σres:(nat × (BitVectorTrie costlabel 16)). Some … res = construct_costs_safe program pol ppc pc costs i
 ≝
   λprogram.λpol: policy program.λppc,pc,costs,i.
    match construct_costs_safe program pol ppc pc costs i with
-    [ None ⇒ let dummy ≝ 〈0, Stub ??〉 in dummy
+    [ None ⇒ let dummy ≝ 〈0, Stub costlabel 16〉 in dummy
     | Some res ⇒ res ].
  [ cases daemon
@@ -1613 +1615 @@
    tech_pc_sigma00 program pol (prefix@[〈label,i〉]) = Some … 〈S ppc,\fst (construct_costs program pol … ppc pc costs i)〉.
 
+lemma eq_identifier_eq:
+  ∀tag: String.
+  ∀l.
+  ∀r.
+    eq_identifier tag l r = true → l = r.
+  #tag #l #r cases l cases r #posl #posr
+  cases daemon
+qed.
+
 definition build_maps:
  ∀pseudo_program.∀pol:policy pseudo_program.
-  Σres:((BitVectorTrie Word 16) × (BitVectorTrie Word 16)).
+  Σres:((identifier_map ASMTag Word) × (BitVectorTrie costlabel 16)).
+   let 〈labels, costs〉 ≝ res in
+    ∀id. occurs_exactly_once id (\snd pseudo_program) →
+     lookup_def … labels id (zero ?) = sigma pseudo_program pol (address_of_word_labels_code_mem (\snd pseudo_program) id) ≝
+  λpseudo_program.
+  λpol:policy pseudo_program.
+    let result ≝
+      foldl_strong
+        (option Identifier × pseudo_instruction)
+          (λpre. Σres:((identifier_map ASMTag Word) × (nat × (nat × (BitVectorTrie costlabel 16)))).
+            let 〈labels,ppc_pc_costs〉 ≝ res in
+            let 〈ppc',pc_costs〉 ≝ ppc_pc_costs in
+            let 〈pc',costs〉 ≝ pc_costs in
+              And ( And (
+              And (bitvector_of_nat ? pc' = sigma pseudo_program pol (bitvector_of_nat ? ppc')) (*∧*)
+                (ppc' = length … pre)) (*∧ *)
+                (tech_pc_sigma00 pseudo_program (eject … pol) pre = Some ? 〈ppc',pc'〉)) (*∧*)
+                (∀id. occurs_exactly_once id pre →
+                  lookup_def … labels id (zero …) = sigma pseudo_program pol (address_of_word_labels_code_mem pre id)))
+                (\snd pseudo_program)
+        (λprefix,i,tl,prf,t.
+          let 〈labels, ppc_pc_costs〉 ≝ t in
+          let 〈ppc, pc_costs〉 ≝ ppc_pc_costs in
+          let 〈pc,costs〉 ≝ pc_costs in
+          let 〈label, i'〉 ≝ i in
+          let labels ≝
+            match label with
+            [ None ⇒ labels
+            | Some label ⇒
+                let program_counter_bv ≝ bitvector_of_nat ? pc in
+                  add ? ? labels label program_counter_bv
+            ]
+          in
+            let construct ≝ construct_costs pseudo_program pol ppc pc costs i' in
+              〈labels, 〈S ppc,construct〉〉) 〈empty_map …, 〈0, 〈0, Stub ? ?〉〉〉
+    in
+      let 〈labels, ppc_pc_costs〉 ≝ result in
+      let 〈ppc,pc_costs〉 ≝ ppc_pc_costs in
+      let 〈pc, costs〉 ≝ pc_costs in
+        〈labels, costs〉.
+ [2: whd generalize in match (sig2 … t); >p >p1 >p2 >p3 * * * #IHn1 #IH0 #IH1 #IH2
+   generalize in match (refl … construct); cases construct in ⊢ (???% → %); #PC #CODE #JMEQ % [% [%]]
+   [ <(construct_costs_sigma … costs i1 IHn1) change with (? = ?(\fst construct)) >JMEQ %
+   | >append_length <IH0 normalize; -IHn1; (*CSC: otherwise it diverges!*) //
+   | >(tech_pc_sigma00_append_Some … costs … IH1) change with (Some … 〈S ppc,\fst construct〉 = ?) >JMEQ %
+   | #id normalize nodelta; -labels1; cases label; normalize nodelta
+     [ #K <address_of_word_labels_code_mem_None [2:@K] @IH2 -IHn1; (*CSC: otherwise it diverges!*) //
+     | #l #H generalize in match (occurs_exactly_once_Some ???? H) in ⊢ ?;
+       generalize in match (refl … (eq_identifier ? l id)); cases (eq_identifier … l id) in ⊢ (???% → %);
+        [ #EQ #_ <(eq_identifier_eq … EQ) check lookup_add_hit. >lookup_insert_hit >address_of_word_labels_code_mem_Some_hit
+          <IH0 [@IHn1 | <(eq_bv_eq … EQ) in H #H @H]
+        | #EQ change with (occurs_exactly_once ?? → ?) #K >lookup_insert_miss [2: -IHn1; (*Andrea:XXXX used to work /2/*)>eq_bv_sym >EQ // ]
+          <(address_of_word_labels_code_mem_Some_miss … EQ … H) @IH2 -IHn1; //]]]
+ |3: whd % [% [%]] // [>sigma_0//] #id normalize in ⊢ (% → ?); #abs @⊥ //
+ | generalize in match (sig2 … result) in ⊢ ?;
+   normalize nodelta in p ⊢ %; -result; >p in ⊢ (match % with [_ ⇒ ?] → ?);
+   normalize nodelta; >p1 normalize nodelta; >p2; normalize nodelta; * #_; #H @H]
+qed.
+
+definition build_maps:
+ ∀pseudo_program.∀pol:policy pseudo_program.
+  Σres:((BitVectorTrie Identifier 16) × (BitVectorTrie costlabel 16)).
    let 〈labels,costs〉 ≝ res in
     ∀id. occurs_exactly_once id (\snd pseudo_program) →
-     lookup ?? id labels (zero …) = sigma pseudo_program pol (address_of_word_labels_code_mem (\snd pseudo_program) id)
-≝
+     lookup ? ? id labels (zero …) = ? (* sigma pseudo_program pol (address_of_word_labels_code_mem (\snd pseudo_program) id) *)
+≝ ?.
   λpseudo_program.λpol:policy pseudo_program.
   let result ≝
    foldl_strong
     (option Identifier × pseudo_instruction)
-    (λpre. Σres:((BitVectorTrie Word 16) × (nat × (nat × (BitVectorTrie Word 16)))).
+    (λpre. Σres:((BitVectorTrie Word 16) × (nat × (nat × (BitVectorTrie costlabel 16)))).
       let 〈labels,ppc_pc_costs〉 ≝ res in
       let 〈ppc',pc_costs〉 ≝ ppc_pc_costs in

src/ASM/CostsProof.ma

@@ -290 +290 @@
 include alias "arithmetics/nat.ma".
 
-(*Useless now?
+(*
 lemma minus_m_n_minus_minus_plus_1:
   ∀m, n: nat.
@@ -297 +297 @@
  /3 by lt_plus_to_minus_r, plus_minus/
 qed.
+*)
 
 lemma plus_minus_rearrangement_1:
@@ -313 +314 @@
     (m - n) + (n - o) = m - o.
  /2 by plus_minus_rearrangement_1/
-qed.*)
+qed.
 
 (*
@@ -344 +345 @@
     normalize @compute_max_trace_any_label_cost_is_ok
   |2:
+    cases the_trace
+    [1:
+      #start_status #final_status #is_next #is_not_return #is_costed
+      normalize nodelta;
+      change with (
+        let current_instruction_cost ≝ current_instruction_cost start_status in 
+        let call_trace_cost ≝ compute_max_trace_label_return_cost cost_labels start_fun_call after_fun_call call_trace in 
+        let final_trace_cost ≝ compute_max_trace_any_label_cost cost_labels end_flag after_fun_call final final_trace in 
+        call_trace_cost+current_instruction_cost+final_trace_cost
+      ) in ⊢ (??%?);
+    |2:
+      #start_status #final_status #is_next #is_return
+    |3:
+      #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
+      #status_final #is_next #is_call #is_after_return #fun_call_trace #after_fun_call_trace
+      change with (
+        let current_instruction_cost ≝ current_instruction_cost status_pre_fun_call in 
+        let call_trace_cost ≝ compute_max_trace_label_return_cost cost_labels status_start_fun_call status_after_fun_call fun_call_trace in 
+        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 
+          call_trace_cost+current_instruction_cost+final_trace_cost) in ⊢ (??%?);
+      normalize nodelta;
+      >compute_max_trace_label_return_cost_is_ok
+      >compute_max_trace_any_label_cost_is_ok
+    |4:
+    ]
   |3:
     cases the_trace
@@ -353 +379 @@
       normalize >compute_max_trace_label_label_cost_is_ok
       >compute_max_trace_label_return_cost_is_ok
+      >plus_minus_rearrangement_1
+      [1: %
+      |2:
+      |3:
+      ]
     ]
   ].