Changeset 1555 for src/ASM


Ignore:
Timestamp:
Nov 24, 2011, 5:19:30 PM (8 years ago)
Author:
boender
Message:
  • changes to assembly
  • added lookup to PositiveMap?
  • lightly changed Fetch to make it compile
Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/Assembly.ma

    r1528 r1555  
    11include "ASM/ASM.ma".
    2 include "ASM/BitVectorTrie.ma".
    32include "ASM/Arithmetic.ma".
    43include "ASM/Fetch.ma".
    … …  
    592591qed. 
    593592
    594 (* lemma coerc_sigma:
    595  ∀A,P.∀p:A.P p → Σx:A.P x.
    596 #A #P #a #p % [ @a | /2/]
    597 qed.
    598 coercion coerc_sigma:∀A,P.∀p:A.P p → Σx:A.P x
    599 ≝ coerc_sigma on p: ? to (Sig ??). *)
    600 
    601593lemma coerc_pair_sigma:
    602594 ∀A,B,P. ∀p:A × B. P (\snd p) → A × (Σx:B.P x).
    … …  
    606598≝ coerc_pair_sigma on p: (? × ?) to (? × (Sig ??)).
    607599
    608 let rec create_label_map (program: list labelled_instruction)
    609   (policy: jump_expansion_policy):
     600definition create_label_map: ∀program:list labelled_instruction.
     601  ∀policy:jump_expansion_policy.
    610602  (Σlabels:label_map.
    611     ∀i:ℕ.lt i (|program|) (* XXX using < causes (false?) ambiguity *) →
     603    ∀i:ℕ.lt i (|program|) →
    612604    ∀l.occurs_exactly_once l program →
    613605    is_label (nth i ? program 〈None ?, Comment [ ]〉) l →
    614606    ∃a.lookup … labels l = Some ? 〈i,a〉
    615607  ) ≝
     608  λprogram.λpolicy.
    616609  let 〈final_pc, final_labels〉 ≝
    617610    foldl_strong (option Identifier × pseudo_instruction)
    618611    (λprefix.ℕ × (Σlabels.
    619       ∀i:ℕ.i < |prefix| →
     612      ∀i:ℕ.lt i (|prefix|) →
    620613      ∀l.occurs_exactly_once l prefix →
    621614      is_label (nth i ? prefix 〈None ?, Comment [ ]〉) l →
    … …  
    724717  ].
    725718
    726 definition jmpleq: jump_length → jump_length → Prop ≝
     719definition jmple: jump_length → jump_length → Prop ≝
    727720  λj1.λj2.
    728721  match j1 with
    729   [ short_jump  ⇒ True
    730   | medium_jump ⇒
     722  [ short_jump  ⇒
    731723    match j2 with
    732724    [ short_jump ⇒ False
    733725    | _          ⇒ True
    734726    ]
    735   | long_jump  ⇒
     727  | medium_jump ⇒
    736728    match j2 with
    737729    [ long_jump ⇒ True
    738730    | _         ⇒ False
    739731    ]
     732  | long_jump   ⇒ False
    740733  ].
    741734
    742 lemma jmpleq_max_length: ∀x,y.jmpleq y (max_length y x).
    743  #x #y
    744  cases y
    745  [ //
    746  | cases x //
    747  | //
    748  ]
    749 qed.
    750 
     735definition jmpleq: jump_length → jump_length → Prop ≝
     736  λj1.λj2.jmple j1 j2 ∨ j1 = j2.
     737  
     738lemma jmpleq_max_length: ∀ol,nl.
     739  jmpleq ol (max_length ol nl).
     740 #ol #nl cases ol cases nl
     741 /2 by or_introl, or_intror, I/
     742qed.
     743 
    751744definition is_jump' ≝
    752745  λx:preinstruction Identifier.
    … …  
    776769definition jump_in_policy ≝
    777770  λprefix:list labelled_instruction.λpolicy:jump_expansion_policy.
    778   ∀i:ℕ.i < |prefix| → is_jump (nth i ? prefix 〈None ?, Comment []〉) →
    779   ∃p,j.lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈p,j〉.
     771  ∀i:ℕ.i < |prefix| →
     772  (is_jump (nth i ? prefix 〈None ?, Comment []〉) ↔
     773   ∃p,j.lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈p,j〉).
    780774 
    781775axiom bitvector_of_nat_abs:
    782776  ∀x,y:ℕ.x ≠ y → ¬eq_bv 16 (bitvector_of_nat 16 x) (bitvector_of_nat 16 y).
    783  
    784 let rec jump_expansion_start (program: list labelled_instruction):
    785   (Σpolicy.jump_in_policy program policy) ≝
     777
     778lemma le_S_to_le: ∀n,m:ℕ.S n ≤ m → n ≤ m.
     779 /2/ qed.
     780
     781lemma jump_not_in_policy: ∀prefix:list labelled_instruction.
     782 ∀policy:(Σp:jump_expansion_policy.
     783 (∀i.i ≥ |prefix| → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧
     784 jump_in_policy prefix p).
     785  ∀i:ℕ.i < |prefix| →
     786  ¬is_jump (nth i ? prefix 〈None ?, Comment []〉) ↔
     787  lookup_opt … (bitvector_of_nat 16 i) policy = None ?.
     788 #prefix #policy #i #Hi @conj
     789 [ #Hnotjmp lapply (refl ? (lookup_opt … (bitvector_of_nat 16 i) policy))
     790   cases (lookup_opt … (bitvector_of_nat 16 i) policy) in ⊢ (???% → ?);
     791   [ #H @H
     792   | #x cases x #y #z #H @⊥ @(absurd ? ? Hnotjmp) @(proj2 ?? (proj2 ?? (sig2 ?? policy) i Hi))
     793     @(ex_intro … y (ex_intro … z H))
     794   ]
     795 | #Hnone @nmk #Hj lapply (proj1 ?? (proj2 ?? (sig2 ?? policy) i Hi) Hj)
     796   #H elim H -H; #x #H elim H -H; #y #H >H in Hnone; #abs destruct (abs)
     797 ] 
     798qed.
     799 
     800definition jump_expansion_start: ∀program:list labelled_instruction.
     801  Σpolicy:jump_expansion_policy.(∀i.i ≥ |program| → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧ jump_in_policy program policy ≝
     802  λprogram.
    786803  foldl_strong (option Identifier × pseudo_instruction)
    787   (λprefix.Σpolicy.jump_in_policy prefix policy)
     804  (λprefix.Σpolicy:jump_expansion_policy.(∀i.i ≥ |prefix| → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧ jump_in_policy prefix policy)
    788805  program
    789806  (λprefix.λx.λtl.λprf.λpolicy.
    … …  
    791808   match instr with
    792809   [ Instruction i ⇒ match i with
    793      [ JC _ ⇒ insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
    794      | JNC _ ⇒ insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
    795      | JZ _ ⇒ insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
    796      | JNZ _ ⇒ insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
    797      | JB _ _ ⇒ insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
    798      | JNB _ _ ⇒ insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
    799      | JBC _ _ ⇒ insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
    800      | CJNE _ _ ⇒ insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
    801      | DJNZ _ _ ⇒ insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
     810     [ JC _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
     811     | JNC _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
     812     | JZ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
     813     | JNZ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
     814     | JB _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
     815     | JNB _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
     816     | JBC _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
     817     | CJNE _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
     818     | DJNZ _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
    802819     | _ ⇒ (eject … policy)
    803820     ]
    804    | Call c ⇒ insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
    805    | Jmp j  ⇒ insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
     821   | Call c ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
     822   | Jmp j  ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
    806823   | _      ⇒ (eject … policy)
    807824   ]
    808825  ) (Stub ? ?).
    809 [43: normalize #i #Hi @⊥ @(absurd (i < 0)) [ @Hi | @not_le_Sn_O ] ]
    810 whd #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi;
    811 #Hi
    812 [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:
    813  >nth_append_second >(injective_S … Hi)
    814  [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]
    815  <minus_n_n #Hj normalize in Hj; @⊥ @Hj
    816 |4,6,52,54,56,58,60,62,64,66,68: >nth_append_second >(injective_S … Hi)
    817  [2,4,6,8,10,12,14,16,18,20,22: @le_n]
    818  <minus_n_n #Hj % [1,3,5,7,9,11,13,15,17,19,21: @O ] %
    819  [1,3,5,7,9,11,13,15,17,19,21: @short_jump ] @lookup_opt_insert_hit
     826@conj
     827(* non-jumps, lookup_opt = None *)
     828[1,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,69,71,73,75,77,79,81,83:
     829  #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi)
     830  -Hi; #Hi @((proj1 ?? (sig2 ?? policy)) i)
     831  [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:
     832    @le_S_to_le @le_S_to_le @Hi
     833  |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,64,66:
     834    <Hi @le_n_Sn
     835  ]
     836(* non-jumps, lookup_opt = Some *)
     837|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:
     838  #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi)
     839  -Hi; #Hi
     840  [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:
     841    >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi))
     842    @((proj2 ?? (sig2 ?? policy)) i (le_S_S_to_le … Hi))
     843  |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,64,66:
     844    @conj >(injective_S … Hi)
     845    [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:
     846      >(nth_append_second ? ? prefix ? ? (le_n (|prefix|)))
     847      <minus_n_n #H @⊥ @H
     848    |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,64,66:
     849      #H elim H; -H; #t1 #H elim H; -H #t2 #H
     850      lapply (proj1 ?? (sig2 ?? policy) (|prefix|) (le_n (|prefix|)))
     851      #H2 >H2 in H; #H destruct (H)
     852    ]
     853  ]
     854(* jumps, lookup_opt = None *)
     855|3,5,51,53,55,57,59,61,63,65,67: #i >append_length <commutative_plus #Hi normalize in Hi;
     856  >lookup_opt_insert_miss
     857  [1,3,5,7,9,11,13,15,17,19,21,23: @((proj1 ?? (sig2 ?? policy)) i) @(le_S_to_le … Hi)
     858  |2,4,6,8,10,12,14,16,18,20,22,24: >eq_bv_sym @bitvector_of_nat_abs @lt_to_not_eq @Hi
     859  ]
     860(* non-jumps, lookup_opt = Some *)
     861|4,6,52,54,56,58,60,62,64,66,68: #i >append_length <commutative_plus #Hi normalize in Hi;
     862  cases (le_to_or_lt_eq … Hi) -Hi; #Hi
     863  [1,3,5,7,9,11,13,15,17,19,21,23: >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi))
     864    >lookup_opt_insert_miss
     865    [1,3,5,7,9,11,13,15,17,19,21,23: @((proj2 ?? (sig2 ?? policy)) i) @(le_S_S_to_le … Hi)
     866    |2,4,6,8,10,12,14,16,18,20,22,24: @bitvector_of_nat_abs @(lt_to_not_eq … (le_S_S_to_le … Hi))
     867    ]
     868  |2,4,6,8,10,12,14,16,18,20,22,24: @conj >(injective_S … Hi) #H
     869    [2,4,6,8,10,12,14,16,18,20,22,24: >(nth_append_second ? ? prefix ? ? (le_n (|prefix|)))
     870       <minus_n_n // ]
     871    @(ex_intro ? ? 0 (ex_intro ? ? short_jump (lookup_opt_insert_hit ? ? 16 ? policy)))
     872  ]
     873(* cases for the empty program *)
     874|85: #i #Hi //
     875|86: whd #i #Hi @⊥ @(absurd (i < 0)) [ @Hi | @not_le_Sn_O ]
    820876]
    821  >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) #Hj
    822  lapply (sig2 … policy) #Hpolicy elim (Hpolicy i (le_S_S_to_le … Hi) Hj)
    823  #p #H elim H #j #Hpj %
    824  [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] %
    825  [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]
    826  [2,3,26,27,28,29,30,31,32,33,34: >lookup_opt_insert_miss]
    827  [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
    828 qed.
    829 
    830 (* not really recursive *)
    831 let rec jump_expansion_step (program: list labelled_instruction)
    832   (old_policy: Σpolicy.jump_in_policy program policy):
     877qed.
     878
     879definition policy_increase: list labelled_instruction → jump_expansion_policy →
     880  jump_expansion_policy → Prop ≝
     881 λprogram.λop.λp.
     882  (* (∀i:ℕ.i < |program| →
     883    lookup_opt … (bitvector_of_nat ? i) op = lookup_opt … (bitvector_of_nat ? i) p) ∨ *)
     884  (∀i:ℕ.i < |program| →
     885    jmpleq
     886      (\snd (bvt_lookup … (bitvector_of_nat ? i) op 〈0,short_jump〉))
     887      (\snd (bvt_lookup … (bitvector_of_nat ? i) p 〈0,short_jump〉))).
     888   
     889definition jump_expansion_step: ∀program:list labelled_instruction.
     890  ∀old_policy:(Σpolicy.
     891    (∀i.i ≥ |program| → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧
     892    jump_in_policy program policy).
    833893  (Σpolicy.
    834     And (jump_in_policy program policy) (* XXX ∧ causes ambiguity *)
    835     (jump_in_policy program policy →
    836      (∀i.lt i (|program|) (* XXX < causes ambiguity *) → is_jump (nth i ? program 〈None ?, Comment []〉) →
    837      jmpleq
    838        (\snd (lookup … (bitvector_of_nat 16 i) old_policy 〈0,short_jump〉))
    839        (\snd (lookup … (bitvector_of_nat 16 i) policy 〈0,short_jump〉)))
    840     )
    841    ) ≝
     894    (∀i.i ≥ |program| → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧
     895    jump_in_policy program policy ∧
     896    policy_increase program old_policy policy)
     897    ≝
     898  λprogram.λold_policy.
    842899  let labels ≝ create_label_map program old_policy in
    843900  let 〈final_pc, final_policy〉 ≝
    844901    foldl_strong (option Identifier × pseudo_instruction)
    845902    (λprefix.ℕ × Σpolicy.
     903      (∀i.i ≥ |prefix| → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧
    846904      jump_in_policy prefix policy ∧
    847       (jump_in_policy prefix policy →
    848        (∀i.i < |prefix| → is_jump (nth i ? prefix 〈None ?, Comment []〉) →
    849        jmpleq
    850          (\snd (lookup … (bitvector_of_nat 16 i) old_policy 〈0,short_jump〉))
    851          (\snd (lookup … (bitvector_of_nat 16 i) policy 〈0,short_jump〉)))
    852       )
     905      policy_increase prefix old_policy policy
    853906    )
    854907    program
    … …  
    876929    ) 〈0, Stub ? ?〉 in
    877930    final_policy.
    878 [ @conj
    879   [ #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi;
    880     [ #Hi; >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) #Hj
    881       lapply (sig2 … policy) #Hacc elim ((proj1 … Hacc) i (le_S_S_to_le … Hi) Hj) #h #n elim n
    882       -n #n #Hn
    883       % [ @h | % [ @n | normalize nodelta cases instr normalize nodelta
    884       [2,3: #x cases (lookup ??? old_policy ?) #y #z @Hn
    885       |6: #x #y cases (lookup ??? old_policy ?) #w #z @Hn
    886       |1: #pi cases (lookup ??? old_policy ?) #x #y cases (jump_expansion_step_instruction ???)
    887         [ @Hn
    888         | #z normalize nodelta <Hn @lookup_opt_insert_miss
    889           @bitvector_of_nat_abs @(lt_to_not_eq i (|prefix|)) @(le_S_S_to_le … Hi)
     931[ @conj [ @conj #i >append_length <commutative_plus #Hi normalize in Hi;
     932[ cases (lookup ??? old_policy ?) #h #n cases add_instr
     933  [ @(proj1 ?? (proj1 ?? (sig2 ?? policy)) i (le_S_to_le … Hi))
     934  | #z normalize nodelta >lookup_opt_insert_miss
     935    [ @(proj1 ?? (proj1 ?? (sig2 ?? policy)) i (le_S_to_le … Hi))
     936    | >eq_bv_sym @bitvector_of_nat_abs @lt_to_not_eq @Hi
     937    ]
     938  ]
     939| cases (le_to_or_lt_eq … Hi) -Hi;
     940  [ #Hi; >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) @conj
     941    [ #Hj lapply (proj2 ?? (proj1 ?? (sig2 ?? policy)) i (le_S_S_to_le … Hi)) #Hacc
     942      cases add_instr cases (lookup ??? old_policy ?) normalize nodelta #x #y
     943      [ @(proj1 ?? Hacc Hj)
     944      | #z elim (proj1 ?? Hacc Hj) #h #n elim n -n #n #Hn
     945        % [ @h | % [ @n | <Hn @lookup_opt_insert_miss @bitvector_of_nat_abs
     946            @(lt_to_not_eq i (|prefix|)) @(le_S_S_to_le … Hi) ] ]
     947      ]
     948    | lapply (proj2 ?? (proj1 ?? (sig2 ?? policy)) i (le_S_S_to_le … Hi)) #Hacc
     949      #H elim H -H; #h #H elim H -H; #n cases add_instr cases (lookup ??? old_policy ?)
     950      normalize nodelta #x #y [2: #z]
     951      #Hl @(proj2 ?? Hacc) @(ex_intro ?? h (ex_intro ?? n ?))
     952      [ <Hl @sym_eq @lookup_opt_insert_miss @bitvector_of_nat_abs @lt_to_not_eq @(le_S_S_to_le … Hi)
     953      | @Hl
     954      ]
     955    ]
     956  | #Hi >(injective_S … Hi) >(nth_append_second ? ? prefix ? ? (le_n (|prefix|)))
     957     <minus_n_n whd in match (nth ????); whd in match (add_instr); cases instr
     958     [1: #pi | 2,3: #x | 4,5: #id | 6: #x #y] @conj normalize nodelta
     959     [3,5,11: #H @⊥ @H (* instr is not a jump *)
     960     |4,6,12: #H elim H -H; #h #H elim H -H #n cases (lookup ??? old_policy ?)
     961       #x #y normalize nodelta >(proj1 ?? (proj1 ?? (sig2 ?? policy)) (|prefix|) (le_n (|prefix|)))
     962       #H destruct (H)
     963     |7,9: (* instr is a jump *) #_ cases (lookup ??? old_policy ?) #h #n
     964       whd in match (snd ???); @(ex_intro ?? pc)
     965       [ @(ex_intro ?? (max_length n (select_jump_length (create_label_map program old_policy) pc id)))
     966       | @(ex_intro ?? (max_length n (select_call_length (create_label_map program old_policy) pc id)))
     967       ] @lookup_opt_insert_hit
     968     |8,10: #_ //
     969     |1,2: cases pi
     970       [35,36,37: #H @⊥ @H
     971       |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #H @⊥ @H
     972       |1,2,3,6,7,33,34: #x #y #H @⊥ @H
     973       |9,10,14,15: #id #_ cases (lookup ??? old_policy ?) #h #n
     974         whd in match (snd ???);
     975         @(ex_intro ?? pc (ex_intro ?? (max_length n (select_reljump_length (create_label_map program old_policy) pc id)) ?))
     976         @lookup_opt_insert_hit
     977       |11,12,13,16,17: #x #id #_ cases (lookup ??? old_policy ?) #h #n
     978         whd in match (snd ???);
     979         @(ex_intro ?? pc (ex_intro ?? (max_length n (select_reljump_length (create_label_map program old_policy) pc id)) ?))
     980         @lookup_opt_insert_hit
     981       |72,73,74: #H elim H -H; #h #H elim H -H #n cases (lookup ??? old_policy ?)
     982        #x #y normalize nodelta
     983        >(proj1 ?? (proj1 ?? (sig2 ?? policy)) (|prefix|) (le_n (|prefix|))) #H destruct (H)
     984       |41,42,45,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69: #x
     985        #H elim H -H; #h #H elim H -H #n cases (lookup ??? old_policy ?)
     986        #x #y normalize nodelta
     987        >(proj1 ?? (proj1 ?? (sig2 ?? policy)) (|prefix|) (le_n (|prefix|))) #H destruct (H)
     988       |38,39,40,43,44,70,71: #x #y #H elim H -H; #h #H elim H -H #n
     989        cases (lookup ??? old_policy ?) #x #y normalize nodelta
     990        >(proj1 ?? (proj1 ?? (sig2 ?? policy)) (|prefix|) (le_n (|prefix|))) #H destruct (H)
     991       |46,47,51,52: #id #_ //
     992       |48,49,50,53,54: #x #id #_ //
     993       ]
     994     ]
     995   ]
     996  ]
     997| lapply (refl ? add_instr) cases add_instr in ⊢ (???% → %);
     998  [ #Ha #i >append_length >commutative_plus #Hi normalize in Hi;
     999    cases (le_to_or_lt_eq … Hi) -Hi; #Hi
     1000    [ cases (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,short_jump〉)
     1001      #x #y @((proj2 ?? (sig2 ?? policy)) i (le_S_S_to_le … Hi))
     1002    | normalize nodelta >(injective_S … Hi)
     1003      >lookup_opt_lookup_miss
     1004      [ >lookup_opt_lookup_miss
     1005        [ //
     1006        | cases (lookup ?? (bitvector_of_nat ? (|prefix|)) old_policy 〈0,short_jump〉)
     1007          #x #y normalize nodelta
     1008          >(proj1 ?? (proj1 ?? (sig2 ?? policy)) (|prefix|) (le_n (|prefix|))) //
    8901009        ]
    891       |4,5: #id cases (lookup ??? old_policy ?) #x #y normalize nodelta <Hn
    892         @lookup_opt_insert_miss @bitvector_of_nat_abs
    893         @(lt_to_not_eq i (|prefix|)) @(le_S_S_to_le … Hi)
    894       ] ] ]
    895     | #Hi >nth_append_second >(injective_S … Hi)
    896       [ <minus_n_n #Hj normalize in Hj; normalize nodelta cases instr in Hj;
    897         [2,3: #x #Hj @⊥ @Hj
    898         |6: #x #y #Hj @⊥ @Hj
    899         |1: #pi cases pi
    900           [35,36,37: #Hj @⊥ @Hj
    901           |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #Hj @⊥ @Hj
    902           |1,2,3,6,7,33,34: #x #y #Hj @⊥ @Hj
    903           |9,10,14,15: #j normalize nodelta #_
    904             % [1,3,5,7: @pc
    905               |2,4,6,8: lapply (refl ? (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,short_jump〉))
    906                 cases (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,short_jump〉) in ⊢ (???% → %);
    907                 #x #y #Hl normalize nodelta
    908             % [1,3,5,7: @(max_length y (select_reljump_length (create_label_map program old_policy) pc j))
    909               |2,4,6,8: @lookup_opt_insert_hit
    910               ] ]
    911           |11,12,13,16,17: #x #j normalize nodelta #_
    912             % [1,3,5,7,9: @pc
    913               |2,4,6,8,10: lapply (refl ? (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,short_jump〉))
    914                 cases (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,short_jump〉) in ⊢ (???% → %);
    915                 #x #y #Hl normalize nodelta
    916             % [1,3,5,7,9: @(max_length y (select_reljump_length (create_label_map program old_policy) pc j))
    917               |2,4,6,8,10: @lookup_opt_insert_hit
    918               ] ]
    919           ]
    920         |4,5: #j normalize nodelta #_
    921           % [1,3: @pc
    922             |2,4: cases (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,short_jump〉)
    923                 #x #y normalize nodelta
    924             % [1: @(max_length y (select_jump_length (create_label_map program old_policy) pc j))
    925               |3: @(max_length y (select_call_length (create_label_map program old_policy) pc j))
    926               |2,4: @lookup_opt_insert_hit
    927               ]
    928             ]
    929         ]
    930       | @le_n
     1010      | >(proj1 ?? (jump_not_in_policy program old_policy (|prefix|) ?))
     1011        [ //
     1012        | >prf >p1 >nth_append_second [ <minus_n_n
     1013        generalize in match Ha; normalize nodelta cases instr normalize nodelta
     1014        [1: #pi cases pi
     1015         [1,2,3,6,7,33,34: #x #y #H normalize /2 by nmk/
     1016         |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #H normalize /2 by nmk/
     1017         |35,36,37: #H normalize /2 by nmk/
     1018         |9,10,14,15: #id whd in match (jump_expansion_step_instruction ???);
     1019           #H destruct (H)
     1020         |11,12,13,16,17: #x #id whd in match (jump_expansion_step_instruction ???);
     1021           #H destruct (H)
     1022         ]
     1023        |2,3: #x #H normalize /2 by nmk/
     1024        |6: #x #y #H normalize /2 by nmk/
     1025        |4,5: #id #H destruct (H)
     1026        ] | @le_n ]
     1027        | >prf >append_length normalize <plus_n_Sm @le_plus_n_r
     1028        ]
    9311029      ]
    9321030    ]
    933   | #Hjip #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi;
    934     [ #Hi >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) #Hj
    935       lapply (sig2 … policy) #Hpolicy normalize nodelta cases instr normalize nodelta
    936       [2,3: #x cases (lookup ? 16 (bitvector_of_nat 16 (|prefix|)) old_policy ?) #y #z
    937         normalize nodelta @(proj2 ? ? Hpolicy (proj1 ? ? Hpolicy) ? (le_S_S_to_le … Hi) Hj)
    938       |6: #x #y cases (lookup ? 16 (bitvector_of_nat 16 (|prefix|)) old_policy ?) #w #z
    939         normalize nodelta @(proj2 ? ? Hpolicy (proj1 ? ? Hpolicy) ? (le_S_S_to_le … Hi) Hj)
    940       |1: #pi cases (lookup ? 16 (bitvector_of_nat 16 (|prefix|)) old_policy ?) #x #y
    941         cases (jump_expansion_step_instruction ???)
    942         [ @(proj2 ? ? Hpolicy (proj1 ? ? Hpolicy) ? (le_S_S_to_le … Hi) Hj)
    943         | #z normalize nodelta
    944           whd in match (snd ℕ jump_expansion_policy ?); >lookup_insert_miss
    945           [ @(proj2 … Hpolicy (proj1 ? ? Hpolicy) ? (le_S_S_to_le … Hi) Hj)
    946           | @bitvector_of_nat_abs @(lt_to_not_eq i (|prefix|)) @(le_S_S_to_le … Hi)
     1031  | #x #Ha #i >append_length >commutative_plus #Hi normalize in Hi;
     1032    cases (le_to_or_lt_eq … Hi) -Hi; #Hi
     1033    [ cases (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,short_jump〉)
     1034      #y #z normalize nodelta normalize nodelta >lookup_insert_miss
     1035      [ @((proj2 ?? (sig2 ?? policy)) i (le_S_S_to_le … Hi))
     1036      | @bitvector_of_nat_abs @lt_to_not_eq @(le_S_S_to_le … Hi)
     1037      ]
     1038    | >(injective_S … Hi) elim (proj1 ?? (proj2 ?? (sig2 ?? old_policy) (|prefix|) ?) ?)
     1039      [ #a #H elim H -H; #b #H >H >(lookup_opt_lookup_hit … 〈a,b〉 H)
     1040        normalize nodelta >lookup_insert_hit @jmpleq_max_length
     1041      | >prf >p1 >nth_append_second
     1042        [ <minus_n_n generalize in match Ha; normalize nodelta cases instr normalize nodelta
     1043          [1: #pi cases pi
     1044           [1,2,3,6,7,33,34: #x #y #H normalize in H; destruct (H)
     1045           |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #H normalize in H; destruct (H)
     1046           |35,36,37: #H normalize in H; destruct (H)
     1047           |9,10,14,15: #id #H //
     1048           |11,12,13,16,17: #x #id #H //
     1049           ]
     1050          |2,3: #x #H normalize in H; destruct (H)
     1051          |6: #x #y #H normalize in H; destruct (H)
     1052          |4,5: #id #H //
    9471053          ]
    948         ]
    949       |4,5: #id cases (lookup ? 16 (bitvector_of_nat 16 (|prefix|)) old_policy ?) #x #y
    950         normalize nodelta >lookup_insert_miss
    951         [1,3: @(proj2 … Hpolicy (proj1 ? ? Hpolicy) ? (le_S_S_to_le … Hi) Hj)
    952         |2,4: @bitvector_of_nat_abs @(lt_to_not_eq i (|prefix|)) @(le_S_S_to_le … Hi)
    953         ]
     1054        | @le_n ]
     1055      | >prf >append_length normalize <plus_n_Sm @le_plus_n_r
    9541056      ]
    955     | #Hi >nth_append_second >(injective_S … Hi)
    956       [ <minus_n_n #Hj normalize in Hj; normalize nodelta cases instr in Hj;
    957         [2,3: #x #Hj @⊥ @Hj
    958         |6: #x #y #Hj @⊥ @Hj
    959         |1: #pi cases pi
    960           [35,36,37: #Hj @⊥ @Hj
    961           |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #Hj @⊥ @Hj
    962           |1,2,3,6,7,33,34: #x #y #Hj @⊥ @Hj
    963           |9,10,14,15: #j normalize nodelta #_
    964             cases (lookup ???? 〈0,short_jump〉) #x #y
    965             whd in match (snd ℕ jump_expansion_policy ?);
    966             >lookup_insert_hit normalize @jmpleq_max_length
    967           |11,12,13,16,17: #z #j normalize nodelta #_
    968             cases (lookup ???? 〈0,short_jump〉) #x #y           
    969             whd in match (snd ℕ jump_expansion_policy ?);
    970             >lookup_insert_hit normalize @jmpleq_max_length
    971           ]
    972         |4,5: #id #_ cases (lookup ???? 〈0,short_jump〉) #x #y
    973               whd in match (snd ℕ jump_expansion_policy ?);
    974               >lookup_insert_hit normalize @jmpleq_max_length
    975         ]
    976       | @le_n
    977       ]
    978     ]
    979   ]
    980 | @conj
    981   [ #i #Hi @⊥ @(absurd (i<0)) [ @Hi | @(not_le_Sn_O) ]
    982   | #H #i #Hi @⊥ @(absurd (i<0)) [ @Hi | @(not_le_Sn_O) ]
    983   ]
     1057    ]
     1058  ] ]
     1059| @conj [ @conj
     1060  [ #i #Hi //
     1061  | #i #Hi @conj [ >nth_nil #H @⊥ @H | #H elim H #x #H1 elim H1 #y #H2
     1062                   normalize in H2; destruct (H2) ]
     1063  ]                 
     1064  | #i #Hi @⊥ @(absurd (i<0)) [ @Hi | @(not_le_Sn_O) ]
    9841065]
    9851066qed.
    9861067 
    9871068let rec jump_expansion_internal (program: list labelled_instruction)
    988   (n: ℕ) on n: (Σpolicy:jump_expansion_policy.jump_in_policy program policy) ≝
     1069  (n: ℕ) on n: (Σpolicy:jump_expansion_policy.
     1070    And
     1071    (∀i:ℕ.i ≥ |program| → lookup_opt ? 16 (bitvector_of_nat ? i) policy = None ?)
     1072    (jump_in_policy program policy)) ≝
    9891073  match n with
    9901074  [ O   ⇒ jump_expansion_start program
    … …  
    9951079]
    9961080qed.
     1081
     1082definition policy_equal ≝
     1083  λprogram:list labelled_instruction.λp1,p2:jump_expansion_policy.
     1084  ∀n:ℕ.n < |program| →
     1085    (\snd (bvt_lookup … (bitvector_of_nat 16 n) p1 〈0,short_jump〉)) =
     1086    (\snd (bvt_lookup … (bitvector_of_nat 16 n) p2 〈0,short_jump〉)).
     1087
     1088lemma pe_refl:
     1089  ∀program.reflexive ? (policy_equal program).
     1090 #program whd #x whd #n #Hn @refl
     1091qed.
     1092
     1093lemma pe_sym:
     1094  ∀program.symmetric ? (policy_equal program).
     1095 #program whd #x #y #Hxy whd #n #Hn
     1096 >(Hxy n Hn) @refl
     1097qed.
     1098
     1099lemma pe_trans:
     1100  ∀program.transitive ? (policy_equal program).
     1101 #program whd #x #y #z #Hxy #Hyz whd #n #Hn
     1102 >(Hxy n Hn) @(Hyz n Hn)
     1103qed.
     1104
     1105lemma le_plus:
     1106  ∀n,m:ℕ.n ≤ m → ∃k:ℕ.m = n + k.
     1107 #n #m elim m -m;
     1108 [ #Hn % [ @O | <(le_n_O_to_eq n Hn) // ]
     1109 | #m #Hind #Hn cases (le_to_or_lt_eq … Hn) -Hn; #Hn
     1110   [ elim (Hind (le_S_S_to_le … Hn)) #k #Hk % [ @(S k) | >Hk // ]
     1111   | % [ @O | <Hn // ]
     1112   ]
     1113 ]
     1114qed.
     1115
     1116theorem plus_Sn_m1: ∀n,m:nat. S m + n = m + S n.
     1117#n (elim n) normalize /2 by S_pred/ qed.
     1118
     1119lemma pe_step: ∀program:list labelled_instruction.
     1120 ∀p1,p2:Σpolicy.
     1121 (∀i:ℕ.i ≥ |program| → lookup_opt … (bitvector_of_nat ? i) policy = None ?)
     1122 ∧jump_in_policy program policy.
     1123  policy_equal program p1 p2 →
     1124  policy_equal program (jump_expansion_step program p1) (jump_expansion_step program p2).
     1125 #program #p1 #p2 #Heq whd #n #Hn lapply (Heq n Hn) #H
     1126 lapply (refl ? (lookup_opt … (bitvector_of_nat ? n) p1))
     1127 cases (lookup_opt … (bitvector_of_nat ? n) p1) in ⊢ (???% → ?);
     1128 [ #Hl lapply ((proj2 ?? (jump_not_in_policy program p1 n Hn)) Hl)
     1129   #Hnotjmp >lookup_opt_lookup_miss
     1130   [ >lookup_opt_lookup_miss
     1131     [ @refl
     1132     | @(proj1 ?? (jump_not_in_policy program (eject … (jump_expansion_step program p2)) n Hn))
     1133       [ @(proj1 ?? (sig2 … (jump_expansion_step program p2)))
     1134       | @Hnotjmp
     1135       ]
     1136     ]
     1137   | @(proj1 ?? (jump_not_in_policy program (eject … (jump_expansion_step program p1)) n Hn))
     1138     [ @(proj1 ?? (sig2 ?? (jump_expansion_step program p1)))
     1139     | @Hnotjmp
     1140     ]
     1141   ]
     1142 | #x #Hl cases daemon
     1143 ]
     1144qed.
     1145   
     1146lemma equal_remains_equal: ∀program:list labelled_instruction.∀n:ℕ.
     1147  policy_equal program (jump_expansion_internal program n) (jump_expansion_internal program (S n)) →
     1148  ∀k.k ≥ n → policy_equal program (jump_expansion_internal program n) (jump_expansion_internal program k).
     1149 #program #n #Heq #k #Hk elim (le_plus … Hk); #z #H >H -H -Hk -k;
     1150 lapply Heq -Heq; lapply n -n; elim z -z;
     1151 [ #n #Heq <plus_n_O @pe_refl 
     1152 | #z #Hind #n #Heq <plus_Sn_m1 whd in match (plus (S n) z); @(pe_trans … (jump_expansion_internal program (S n)))
     1153   [ @Heq
     1154   | @pe_step @Hind @Heq
     1155   ]
     1156 ]
     1157qed.
     1158
     1159lemma dec_bounded_forall:
     1160  ∀P:ℕ → Prop.(∀n.(P n) + (¬P n)) → ∀k.(∀n.n < k → P n) + ¬(∀n.n < k → P n).
     1161 #P #HP_dec #k elim k -k
     1162 [ %1 #n #Hn @⊥ @(absurd (n < 0) Hn) @not_le_Sn_O
     1163 | #k #Hind cases Hind
     1164   [ #Hk cases (HP_dec k)
     1165     [ #HPk %1 #n #Hn cases (le_to_or_lt_eq … Hn)
     1166       [ #H @(Hk … (le_S_S_to_le … H))
     1167       | #H >(injective_S … H) @HPk
     1168       ]
     1169     | #HPk %2 @nmk #Habs @(absurd (P k)) [ @(Habs … (le_n (S k))) | @HPk ]
     1170     ]
     1171   | #Hk %2 @nmk #Habs @(absurd (∀n.n<k→P n)) [ #n' #Hn' @(Habs … (le_S … Hn')) | @Hk ]
     1172   ]
     1173 ]
     1174qed.
     1175
     1176lemma dec_bounded_exists:
     1177  ∀P:ℕ→Prop.(∀n.(P n) + (¬P n)) → ∀k.(∃n.n < k ∧ P n) + ¬(∃n.n < k ∧ P n).
     1178 #P #HP_dec #k elim k -k
     1179 [ %2 @nmk #Habs elim Habs #n #Hn @(absurd (n < 0) (proj1 … Hn)) @not_le_Sn_O
     1180 | #k #Hind cases Hind
     1181   [ #Hk %1 elim Hk #n #Hn @(ex_intro … n) @conj [ @le_S @(proj1 … Hn) | @(proj2 … Hn) ]
     1182   | #Hk cases (HP_dec k)
     1183     [ #HPk %1 @(ex_intro … k) @conj [ @le_n | @HPk ]
     1184     | #HPk %2 @nmk #Habs elim Habs #n #Hn cases (le_to_or_lt_eq … (proj1 … Hn))
     1185       [ #H @(absurd (∃n.n < k ∧ P n)) [ @(ex_intro … n) @conj
     1186         [ @(le_S_S_to_le … H) | @(proj2 … Hn) ] | @Hk ]
     1187       | #H @(absurd (P k)) [ <(injective_S … H) @(proj2 … Hn) | @HPk ]
     1188       ] 
     1189     ]
     1190   ]
     1191 ]
     1192qed.
     1193
     1194lemma not_exists_forall:
     1195  ∀A:Type[0].∀P:A → Prop.¬(∃x.P x) → ∀x.¬P x.
     1196 #A #P #Hex #x @nmk #Habs @(absurd ? ? Hex) @(ex_intro … x) @Habs
     1197qed.
     1198
     1199lemma de_morgan1:
     1200 ∀A,B:Prop.¬(A ∧ ¬B) → A → ¬¬B.
     1201 #A #B #Hnot #HA @nmk #H @(absurd (A∧¬B)) [ % [ @HA | @H ] | @Hnot ]
     1202qed.
     1203
     1204lemma thingie:
     1205  ∀A:Prop.(A + ¬A) → (¬¬A) → A.
     1206 #A #Adec #nnA cases Adec
     1207 [ //
     1208 | #H @⊥ @(absurd (¬A) H nnA)
     1209 ]
     1210qed.
     1211 
     1212lemma dec_eq_jump_length: ∀a,b:jump_length.(a = b) + (a ≠ b).
     1213  #a #b cases a cases b /2/
     1214  %2 @nmk #H destruct (H)
     1215qed.
     1216
     1217lemma incr_or_equal: ∀program:list labelled_instruction.
     1218  ∀policy:(Σp:jump_expansion_policy.
     1219    (∀i.i ≥ |program| → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧
     1220    jump_in_policy program p).
     1221  policy_equal program policy (jump_expansion_step program policy) ∨
     1222  ∃n:ℕ.jmple
     1223    (\snd (bvt_lookup … (bitvector_of_nat ? n) policy 〈0,short_jump〉))
     1224    (\snd (bvt_lookup … (bitvector_of_nat ? n) (jump_expansion_step program policy) 〈0,short_jump〉)).
     1225 #program #policy cases (dec_bounded_exists
     1226   (λk.
     1227     \snd (bvt_lookup ?? (bitvector_of_nat ? k) policy 〈0,short_jump〉) ≠
     1228     \snd (bvt_lookup ?? (bitvector_of_nat ? k) (jump_expansion_step program policy) 〈0,short_jump〉))
     1229   ? (|program|))
     1230   [ #H %2 elim H -H; #i #Hi
     1231     cases (proj2 ?? (sig2 ?? (jump_expansion_step program policy)) i (proj1 ?? Hi))
     1232     [ #H @(ex_intro … i H)
     1233     | #H @⊥ @(absurd ? H (proj2 ?? Hi))
     1234     ]
     1235   | #H %1 whd #i #Hi @(thingie ? (dec_eq_jump_length ??)) elim H -H #H; @nmk #H2 @H
     1236     @(ex_intro … i) @conj [ @Hi | @H2 ]
     1237   | #n cases (dec_eq_jump_length (\snd (lookup ?? (bitvector_of_nat ? n) policy 〈0,short_jump〉))
     1238     (\snd (lookup ?? (bitvector_of_nat ? n) (jump_expansion_step program policy) 〈0,short_jump〉)))
     1239     [ #H %2 @nmk #H1 elim H1 #H2 @H2 @H
     1240     | #H %1 @H
     1241     ]
     1242   ]
     1243qed. 
    9971244
    9981245(**************************************** START OF POLICY ABSTRACTION ********************)

  • src/ASM/Fetch.ma

    r895 r1555  
    66 λpmem: BitVectorTrie Byte 16.
    77 λpc: Word.
    8   〈\snd (half_add … pc (bitvector_of_nat 16 (S O))), lookup … pc pmem (zero 8)〉.
     8  〈\snd (half_add … pc (bitvector_of_nat 16 (S O))), lookup ? ? pc pmem (zero 8)〉.
    99
    1010(* timings taken from SIEMENS *)
Note: See TracChangeset for help on using the changeset viewer.