Changeset 1459


Ignore:
Timestamp:
Oct 24, 2011, 2:34:02 PM (8 years ago)
Author:
boender
Message:
  • moved stronger occurs_exactly_once lemma to its proper place in Status
  • renamed 'bla' to something more descriptive
  • finished stuff with sigma types
Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r1417 r1459  
    44include "ASM/Fetch.ma".
    55include "ASM/Status.ma".
     6include alias "basics/logic.ma".
    67
    78definition assembly_preinstruction ≝
     
    565566  ].
    566567 
    567 lemma oeo_Some_Stronger:
    568   ∀id,id',i,prefix.
    569     occurs_exactly_once id (prefix@[〈Some ? id',i〉]) →
    570     (eq_bv ? id' id ∧ does_not_occur id prefix) ∨
    571     (¬eq_bv ? id' id ∧ occurs_exactly_once id prefix).
    572  #id #id' #i #prefix elim prefix
    573  [ whd in ⊢ (?% → ?) whd in ⊢ (?(match % with [_ ⇒ ?| _ ⇒ ?]) → ?)
    574   change with (? → eq_v ?? eq_b id' id∧?∨?) cases (eq_v ?????)
    575   [ normalize //
    576   | normalize #H @⊥ @H 
    577   ]
    578  | *; #he #i' #tl #IH whd in ⊢ (?% → ?) whd in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?)
    579    cases he; normalize nodelta
    580    [ #H @ (IH H)
    581    | #x whd in ⊢ (? → ?(??%)) whd in match (instruction_matches_identifier ??)
    582      generalize in match (refl ? (eq_bv 16 x id)) change in match (eq_v ???x id) with (eq_bv ? x id)
    583      cases (eq_bv ???) in ⊢ (???% → %) #Heq
    584      [ generalize in match (refl ? (eq_bv 16 id' id)) cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta
    585        [ #H >(eq_bv_eq … (sym_eq … H)) >does_not_occur_absurd #Hf @⊥ @Hf
    586        | #H >(does_not_occur_Some)
    587          [ #H2 whd in match (does_not_occur ??) whd in match (instruction_matches_identifier ??)
    588            change in match (eq_v ???x id) with (eq_bv ? x id) >Heq normalize nodelta
    589            @orb_elim normalize nodelta whd in match (occurs_exactly_once ??) whd in match (instruction_matches_identifier ??)
    590            change in match (eq_v ???x id) with (eq_bv ? x id) >Heq normalize nodelta @H2 
    591          | @(sym_eq … H)
    592          ]
    593        ]
    594      | normalize nodelta #H lapply (IH H) -IH -H; #Hor @orb_elim
    595        generalize in match (refl ? (eq_bv 16 id' id)) cases (eq_bv ???) in ⊢ (??%? → %)
    596        #Heq2
    597        [ normalize nodelta <Heq2 in Hor; #Hor normalize in Hor;
    598          whd in match (does_not_occur ??) whd in match (instruction_matches_identifier ??)
    599          change in match (eq_v ???x id) with (eq_bv ? x id) >Heq normalize nodelta
    600          cases (does_not_occur id tl) in Hor; normalize nodelta //
    601        | normalize nodelta whd in match (occurs_exactly_once ??)
    602          whd in match (instruction_matches_identifier ??) change in match (eq_v ???x id) with (eq_bv ? x id)
    603          >Heq normalize nodelta <Heq2 in Hor; normalize //
    604        ]
    605      ] 
    606    ]
    607  ]
    608 qed.   
    609 
    610 lemma bla:
     568lemma label_does_not_occur:
    611569  ∀i,p,l.
    612570  is_label (nth i ? p 〈None ?, Comment [ ]〉) l → does_not_occur l p = false.
     
    631589 ]
    632590qed. 
     591
     592(* lemma coerc_sigma:
     593 ∀A,P.∀p:A.P p → Σx:A.P x.
     594#A #P #a #p % [ @a | /2/]
     595qed.
     596coercion coerc_sigma:∀A,P.∀p:A.P p → Σx:A.P x
     597≝ coerc_sigma on p: ? to (Sig ??). *)
    633598
    634599lemma coerc_pair_sigma:
     
    673638      lapply (sig2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc Hl) #addr #Haddr 
    674639      % [ @addr | @Haddr ]
    675     | #l' #Hocc #Hl lapply (oeo_Some_Stronger … Hocc) -Hocc; #Hocc
     640    | #l' #Hocc #Hl lapply (occurs_exactly_once_Some_stronger … Hocc) -Hocc; #Hocc
    676641      lapply (refl ? (eq_bv 16 l' l)) cases (eq_bv ? l' l) in ⊢ (???% → %) #Heq
    677642      [ >Heq in Hocc; #Hocc normalize in Hocc;
     
    683648        ]
    684649      ]
    685       >(bla i … Hl) normalize nodelta @nmk //
     650      >(label_does_not_occur i … Hl) normalize nodelta @nmk //
    686651    ]
    687652  | #Hi #l #Hocc >(injective_S … Hi) >nth_append_second
     
    811776  ∀i:ℕ.i < |prefix| → is_jump (nth i ? prefix 〈None ?, Comment []〉) →
    812777  ∃p,j.lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈p,j〉.
    813    
     778 
     779axiom bitvector_of_nat_abs:
     780  ∀x,y:ℕ.x ≠ y → ¬eq_bv 16 (bitvector_of_nat 16 x) (bitvector_of_nat 16 y).
     781 
     782let rec jump_expansion_start (program: list labelled_instruction):
     783  (Σpolicy.jump_in_policy program policy) ≝
     784  foldl_strong (option Identifier × pseudo_instruction)
     785  (λprefix.Σpolicy.jump_in_policy prefix policy)
     786  program
     787  (λprefix.λx.λtl.λprf.λpolicy.
     788   let 〈label,instr〉 ≝ x in
     789   match instr with
     790   [ Instruction i ⇒ match i with
     791     [ JC _ ⇒ insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
     792     | JNC _ ⇒ insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
     793     | JZ _ ⇒ insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
     794     | JNZ _ ⇒ insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
     795     | JB _ _ ⇒ insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
     796     | JNB _ _ ⇒ insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
     797     | JBC _ _ ⇒ insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
     798     | CJNE _ _ ⇒ insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
     799     | DJNZ _ _ ⇒ insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
     800     | _ ⇒ (eject … policy)
     801     ]
     802   | Call c ⇒ insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
     803   | Jmp j  ⇒ insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
     804   | _      ⇒ (eject … policy)
     805   ]
     806  ) (Stub ? ?).
     807[43: normalize #i #Hi @⊥ @(absurd (i < 0)) [ @Hi | @not_le_Sn_O ] ]
     808whd #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi;
     809#Hi
     810[2,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,70,72,74,76,78,80,82,84:
     811 >nth_append_second >(injective_S … Hi)
     812 [2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56,58,60,62: @le_n]
     813 <minus_n_n #Hj normalize in Hj; @⊥ @Hj
     814|4,6,52,54,56,58,60,62,64,66,68: >nth_append_second >(injective_S … Hi)
     815 [2,4,6,8,10,12,14,16,18,20,22: @le_n]
     816 <minus_n_n #Hj % [1,3,5,7,9,11,13,15,17,19,21: @O ] %
     817 [1,3,5,7,9,11,13,15,17,19,21: @short_jump ] @lookup_opt_insert_hit
     818]
     819 >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) #Hj
     820 lapply (sig2 … policy) #Hpolicy elim (Hpolicy i (le_S_S_to_le … Hi) Hj)
     821 #p #H elim H #j #Hpj %
     822 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55,57,59,61,63,65,67,69,71,73,75,77,79,81,83: @p] %
     823 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55,57,59,61,63,65,67,69,71,73,75,77,79,81,83: @j]
     824 [2,3,26,27,28,29,30,31,32,33,34: >lookup_opt_insert_miss]
     825 [2,4,6,8,10,12,14,16,18,20,22: @bitvector_of_nat_abs @lt_to_not_eq @(le_S_S_to_le … Hi) ] @Hpj
     826qed.
     827
     828(* not really recursive *)
    814829let rec jump_expansion_step (program: list labelled_instruction)
    815830  (old_policy: Σpolicy.jump_in_policy program policy):
     
    870885        [ @Hn
    871886        | #z normalize nodelta <Hn @lookup_opt_insert_miss
    872           @notb_elim >eq_bv_false [ // | @nmk #H @(absurd (i = (|prefix|)))
    873           [ @(bitvector_of_nat_ok … H)
    874           | @(lt_to_not_eq i (|prefix|)) @(le_S_S_to_le … Hi)
    875           ] ]
     887          @bitvector_of_nat_abs @(lt_to_not_eq i (|prefix|)) @(le_S_S_to_le … Hi)
    876888        ]
    877889      |4,5: #id cases (lookup ??? old_policy ?) #x #y normalize nodelta <Hn
    878         @lookup_opt_insert_miss @notb_elim >eq_bv_false
    879         [1,3: //
    880         |2,4: @nmk #H @(absurd (i = (|prefix|)))
    881           [1,3: @(bitvector_of_nat_ok … H)
    882           |2,4: @(lt_to_not_eq i (|prefix|)) @(le_S_S_to_le … Hi)
    883           ] ]
     890        @lookup_opt_insert_miss @bitvector_of_nat_abs
     891        @(lt_to_not_eq i (|prefix|)) @(le_S_S_to_le … Hi)
    884892      ] ] ]
    885893    | #Hi >nth_append_second >(injective_S … Hi)
     
    934942          whd in match (snd ℕ jump_expansion_policy ?) >lookup_insert_miss
    935943          [ @(proj2 … Hpolicy (proj1 ? ? Hpolicy) ? (le_S_S_to_le … Hi) Hj)
    936           | @notb_elim >eq_bv_false [ // | @nmk #H @(absurd (i = (|prefix|)))
    937             [ @(bitvector_of_nat_ok … H)
    938             | @(lt_to_not_eq i (|prefix|)) @(le_S_S_to_le … Hi)
    939             ] ]
     944          | @bitvector_of_nat_abs @(lt_to_not_eq i (|prefix|)) @(le_S_S_to_le … Hi)
    940945          ]
    941946        ]
     
    943948        normalize nodelta >lookup_insert_miss
    944949        [1,3: @(proj2 … Hpolicy (proj1 ? ? Hpolicy) ? (le_S_S_to_le … Hi) Hj)
    945         |2,4: @notb_elim >eq_bv_false [1,3: // | 2,4: @nmk #H @(absurd (i = (|prefix|)))
    946           [1,3: @(bitvector_of_nat_ok … H)
    947           |2,4: @(lt_to_not_eq i (|prefix|)) @(le_S_S_to_le … Hi)
    948           ] ]
     950        |2,4: @bitvector_of_nat_abs @(lt_to_not_eq i (|prefix|)) @(le_S_S_to_le … Hi)
    949951        ]
    950952      ]
     
    981983qed.
    982984 
    983 definition jump_expansion_internal: list labelled_instruction → jump_expansion_policy ≝
    984   λprogram.
    985     Stub ? ?.
    986    
     985let rec jump_expansion_internal (program: list labelled_instruction)
     986  (n: ℕ) on n: (Σpolicy:jump_expansion_policy.jump_in_policy program policy) ≝
     987  match n with
     988  [ O   ⇒ jump_expansion_start program
     989  | S m ⇒ jump_expansion_step program (jump_expansion_internal program m)
     990  ].
     991[ @(sig2 … (jump_expansion_start program))
     992| @(proj1 … (sig2 … (jump_expansion_step program (jump_expansion_internal program m))))
     993]
     994qed.
     995
    987996(**************************************** START OF POLICY ABSTRACTION ********************)
    988997
  • src/ASM/Status.ma

    r1393 r1459  
    11651165qed.
    11661166
     1167lemma occurs_exactly_once_Some_stronger:
     1168  ∀id,id',i,prefix.
     1169    occurs_exactly_once id (prefix@[〈Some ? id',i〉]) →
     1170    (eq_bv ? id' id ∧ does_not_occur id prefix) ∨
     1171    (¬eq_bv ? id' id ∧ occurs_exactly_once id prefix).
     1172 #id #id' #i #prefix elim prefix
     1173 [ whd in ⊢ (?% → ?) whd in ⊢ (?(match % with [_ ⇒ ?| _ ⇒ ?]) → ?)
     1174  change with (? → eq_v ?? eq_b id' id∧?∨?) cases (eq_v ?????)
     1175  [ normalize //
     1176  | normalize #H @⊥ @H 
     1177  ]
     1178 | *; #he #i' #tl #IH whd in ⊢ (?% → ?) whd in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?)
     1179   cases he; normalize nodelta
     1180   [ #H @ (IH H)
     1181   | #x whd in ⊢ (? → ?(??%)) whd in match (instruction_matches_identifier ??)
     1182     generalize in match (refl ? (eq_bv 16 x id)) change in match (eq_v ???x id) with (eq_bv ? x id)
     1183     cases (eq_bv ???) in ⊢ (???% → %) #Heq
     1184     [ generalize in match (refl ? (eq_bv 16 id' id)) cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta
     1185       [ #H >(eq_bv_eq … (sym_eq … H)) >does_not_occur_absurd #Hf @⊥ @Hf
     1186       | #H >(does_not_occur_Some)
     1187         [ #H2 whd in match (does_not_occur ??) whd in match (instruction_matches_identifier ??)
     1188           change in match (eq_v ???x id) with (eq_bv ? x id) >Heq normalize nodelta
     1189           @orb_elim normalize nodelta whd in match (occurs_exactly_once ??) whd in match (instruction_matches_identifier ??)
     1190           change in match (eq_v ???x id) with (eq_bv ? x id) >Heq normalize nodelta @H2 
     1191         | @(sym_eq … H)
     1192         ]
     1193       ]
     1194     | normalize nodelta #H lapply (IH H) -IH -H; #Hor @orb_elim
     1195       generalize in match (refl ? (eq_bv 16 id' id)) cases (eq_bv ???) in ⊢ (??%? → %)
     1196       #Heq2
     1197       [ normalize nodelta <Heq2 in Hor; #Hor normalize in Hor;
     1198         whd in match (does_not_occur ??) whd in match (instruction_matches_identifier ??)
     1199         change in match (eq_v ???x id) with (eq_bv ? x id) >Heq normalize nodelta
     1200         cases (does_not_occur id tl) in Hor; normalize nodelta //
     1201       | normalize nodelta whd in match (occurs_exactly_once ??)
     1202         whd in match (instruction_matches_identifier ??) change in match (eq_v ???x id) with (eq_bv ? x id)
     1203         >Heq normalize nodelta <Heq2 in Hor; normalize //
     1204       ]
     1205     ] 
     1206   ]
     1207 ]
     1208qed.   
     1209
    11671210let rec index_of_internal (A: Type[0]) (pred: A → bool) (l: list A) (acc: nat) on l: nat ≝
    11681211  match l with
Note: See TracChangeset for help on using the changeset viewer.