Changeset 1070
 Timestamp:
 Jul 15, 2011, 12:56:48 PM (9 years ago)
 Location:
 src
 Files:

 4 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/BitVectorTrie.ma
r1052 r1070 358 358 qed. 359 359 360 lemma lookup_opt_prepare_trie_for_insertion_miss: 361 ∀A:Type[0].∀v:A.∀n.∀c,b:BitVector n. 362 (notb (eq_bv ? b c)) → lookup_opt … b (prepare_trie_for_insertion … c v) = None ?. 363 #A #v #n #c elim c 364 [ #b >(BitVector_O … b) normalize #abs @⊥ // 365  #m #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ 366 cases hd cases hd' normalize 367 [2,3: #_ cases tl' // 368 *: change with (bool_to_Prop (notb (eq_bv ???)) → ?) @IH ]] 369 qed. 370 360 371 lemma lookup_opt_insert_hit: 361 372 ∀A:Type[0].∀v:A.∀n.∀b:BitVector n.∀t:BitVectorTrie A n. … … 374 385 ] 375 386 qed. 376 387 388 lemma lookup_opt_insert_miss: 389 ∀A:Type[0].∀v:A.∀n.∀c,b:BitVector n.∀t:BitVectorTrie A n. 390 (notb (eq_bv ? b c)) → lookup_opt … b (insert … c v t) = lookup_opt … b t. 391 #A #v #n #c elim c c n 392 [ #b #t #DIFF @⊥ whd in DIFF; >(BitVector_O … b) in DIFF // 393  #n #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ 394 #t cases(BitVectorTrie_Sn … t) 395 [ * #l * #r #JMEQ >JMEQ cases hd cases hd' #H normalize in H; 396 [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize // @IH // 397  #JMEQ >JMEQ cases hd cases hd' #H normalize in H; 398 [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize 399 [3,4: cases tl' //  *: @lookup_opt_prepare_trie_for_insertion_miss //]]] 400 qed. 401 377 402 lemma forall_insert_inv1: 378 403 ∀A.∀n.∀b.∀a.∀t.∀P. 
src/Cminor/toRTLabs.ma
r1056 r1070 26 26 mk_internal_function (f_labgen f) (f_reggen f) 27 27 (f_result f) (f_params f) (f_locals f) 28 (f_stacksize f) (add ?? (f_graph f) l s) (f_entry f) (f_exit f). 28 (f_stacksize f) (add ?? (f_graph f) l s) 29 (dp ?? (f_entry f) ?) (dp ?? (f_exit f) ?). 30 @lookup_add_oblivious [ cases (f_entry f)  cases (f_exit f) ] // 31 qed. 29 32 30 33 (* Add a statement to the graph, making it the entry label. *) … … 33 36 mk_internal_function (f_labgen f) (f_reggen f) 34 37 (f_result f) (f_params f) (f_locals f) 35 (f_stacksize f) (add ?? (f_graph f) l s) l (f_exit f). 38 (f_stacksize f) (add ?? (f_graph f) l s) 39 (dp ?? l ?) (dp ?? (f_exit f) ?). 40 [ %{s} @lookup_add_hit 41  @lookup_add_oblivious cases (f_exit f) // 42 ] qed. 36 43 37 44 (* Add a statement with a fresh label to the start of the function. The … … 43 50 (mk_internal_function g (f_reggen f) 44 51 (f_result f) (f_params f) (f_locals f) 45 (f_stacksize f) (add ?? (f_graph f) l s') l (f_exit f)). 46 52 (f_stacksize f) (add ?? (f_graph f) l s') 53 (dp ?? l ?) (dp ?? (f_exit f) ?)). 54 [ %{s'} @lookup_add_hit 55  @lookup_add_oblivious cases (f_exit f) // 56 ] qed. 57 (* 47 58 (* Generate a fresh label and use it as a dangling entry point, to be filled in 48 59 later with the loop head. *) … … 53 64 (f_result f) (f_params f) (f_locals f) 54 65 (f_stacksize f) (f_graph f) l (f_exit f)). 55 66 *) 56 67 definition fresh_reg : internal_function → typ → register × internal_function ≝ 57 68 λf,ty. … … 189 200 add_expr env ? e r f 190 201  St_loop s ⇒ 191 let f ≝ add_ loop_label_to_graph f in202 let f ≝ add_fresh_to_graph ? f in (* dummy statement, fill in afterwards *) 192 203 let l_loop ≝ f_entry f in 193 204 do f ← add_stmt env label_env s exits f; … … 235 246 [ @(λ_. St_skip l_next) 236 247  @(St_skip (f_entry f)) 248  @St_skip 237 249  @(λ_. St_skip l) 238 250  @(λ_. St_skip l_default) … … 284 296 OK ? f 285 297 . 298 % [2,4: @lookup_add_hit  *: skip ] 299 qed. 286 300 287 301 definition cminor_to_rtlabs : Cminor_program → res RTLabs_program ≝ 
src/RTLabs/syntax.ma
r1056 r1070 35 35 ; f_stacksize : nat 36 36 ; f_graph : graph statement 37 ; f_entry : label38 ; f_exit : label37 ; f_entry : Σl:label. ∃s. lookup ?? f_graph l = Some ? s 38 ; f_exit : Σl:label. ∃s. lookup ?? f_graph l = Some ? s 39 39 }. 40 40 
src/common/Identifiers.ma
r1068 r1070 43 43 else OK ? it. 44 44 45 definition eq_identifier ≝ 46 λt. 47 λl, r: identifier t. 45 definition eq_identifier : ∀t. identifier t → identifier t → bool ≝ 46 λt,l,r. 48 47 match l with 49 48 [ an_identifier l' ⇒ … … 53 52 ] 54 53 ]. 54 55 lemma eq_identifier_elim : ∀P:bool → Type[0]. ∀t,x,y. 56 (x = y → P true) → (x ≠ y → P false) → 57 P (eq_identifier t x y). 58 #P #t * #x * #y #T #F 59 change with (P (eq_bv ???)) 60 @eq_bv_elim [ /2/  * #H @F % #E destruct /2/ ] 61 qed. 55 62 56 63 definition word_of_identifier ≝ … … 90 97 λtag,A,m,l,a. an_id_map tag A (insert A 16 (match l with [ an_identifier l' ⇒ l' ]) a 91 98 (match m with [ an_id_map m' ⇒ m' ])). 99 100 lemma lookup_add_hit : ∀tag,A,m,i,a. 101 lookup tag A (add tag A m i a) i = Some ? a. 102 #tag #A * #m * #i #a 103 @lookup_opt_insert_hit 104 qed. 105 106 lemma lookup_add_miss : ∀tag,A,m,i,j,a. 107 (notb (eq_identifier tag i j)) → 108 lookup tag A (add tag A m j a) i = lookup tag A m i. 109 #tag #A * #m * #i * #j #a 110 change with (notb (eq_bv ???) → ?) 111 @lookup_opt_insert_miss 112 qed. 113 114 lemma lookup_add_oblivious : ∀tag,A,m,i,j,a. 115 (∃v. lookup tag A m i = Some ? v) → 116 ∃v. lookup tag A (add tag A m j a) i = Some ? v. 117 #tag #A #m #i #j #a * #v #H 118 lapply (lookup_add_miss … m i j a) 119 @eq_identifier_elim 120 [ #E #_ %{a} >E @lookup_add_hit 121  #_ #H' %{v} <H @H' % 122 ] qed. 92 123 93 124 (* Extract every identifier, value pair from the map. *)
Note: See TracChangeset
for help on using the changeset viewer.