Changeset 1606


Ignore:
Timestamp:
Dec 14, 2011, 1:40:08 PM (8 years ago)
Author:
sacerdot
Message:

Porting to last library of Matita.

Location:
src/ASM
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1597 r1606  
    116116  #new_program_counter_from_fetch #program_counter_within_program
    117117  >new_program_counter_from_fetch
    118   lapply (sig2 ? ? (fetch code_memory program_counter)) #assm
     118  lapply (fetch code_memory program_counter) #assm
    119119  cases daemon
    120120qed.
  • src/ASM/Assembly.ma

    r1593 r1606  
    679679  [ #Hi #l normalize nodelta; cases label normalize nodelta
    680680    [ >occurs_exactly_once_None #Hocc >(nth_append_first ? ? prefix ? ? (le_S_S_to_le ? ? Hi)) #Hl
    681       lapply (sig2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc Hl) #addr #Haddr 
     681      lapply (pi2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc Hl) #addr #Haddr 
    682682      % [ @addr | @Haddr ]
    683683    | #l' #Hocc #Hl lapply (occurs_exactly_once_Some_stronger … Hocc) -Hocc;
     
    686686        >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; #Hl 
    687687        @⊥ @(absurd … Hocc)
    688       | normalize nodelta lapply (sig2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc ?)
     688      | normalize nodelta lapply (pi2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc ?)
    689689        [ #addr #Haddr % [ @addr | <Haddr @lookup_add_miss /2/ ]
    690690        | >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; //
     
    832832   cases (lookup_opt … (bitvector_of_nat 16 i) policy) in ⊢ (???% → ?);
    833833   [ #H @H
    834    | #x cases x #y #z #H @⊥ @(absurd ? ? Hnotjmp) @(proj2 ?? (proj2 ?? (sig2 ?? policy) i Hi))
     834   | #x cases x #y #z #H @⊥ @(absurd ? ? Hnotjmp) @(proj2 ?? (proj2 ?? (pi2 ?? policy) i Hi))
    835835     @(ex_intro … y (ex_intro … z H))
    836836   ]
    837  | #Hnone @nmk #Hj lapply (proj1 ?? (proj2 ?? (sig2 ?? policy) i Hi) Hj)
     837 | #Hnone @nmk #Hj lapply (proj1 ?? (proj2 ?? (pi2 ?? policy) i Hi) Hj)
    838838   #H elim H -H; #x #H elim H -H; #y #H >H in Hnone; #abs destruct (abs)
    839839 ] 
     
    868868     | CJNE _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
    869869     | DJNZ _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
    870      | _ ⇒ (eject … policy)
     870     | _ ⇒ (pi1 … policy)
    871871     ]
    872872   | Call c ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
    873873   | Jmp j  ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
    874    | _      ⇒ (eject … policy)
     874   | _      ⇒ (pi1 … policy)
    875875   ]
    876876  ) (Stub ? ?).
     
    881881  #i >append_length <commutative_plus #Hi normalize in Hi;
    882882  [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:
    883    #Hi2 cases (le_to_or_lt_eq … Hi) -Hi; #Hi @(proj1 ?? (proj1 ?? (sig2 ?? policy)) i)
     883   #Hi2 cases (le_to_or_lt_eq … Hi) -Hi; #Hi @(proj1 ?? (proj1 ?? (pi2 ?? policy)) i)
    884884   [1,5,9,13,17,21,25,29,33,37,41,45,49,53,57,61,65,69,73,77,81,85,89,93,97,101,105,109,113,117,121:
    885885     @le_S_to_le @le_S_to_le @Hi
     
    895895  [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:
    896896    >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi))
    897     @(proj2 ?? (proj1 ?? (sig2 ?? policy)) i (le_S_S_to_le … Hi))
     897    @(proj2 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi))
    898898  ]
    899899  @conj >(injective_S … Hi)
     
    902902   ]
    903903   #H elim H; -H; #t1 #H elim H; -H #t2 #H
    904    >(proj1 ?? (proj1 ?? (sig2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?) in H;
     904   >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?) in H;
    905905   [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:
    906906     #H destruct (H)
    907907   ]
    908    @(transitive_lt … (sig2 ?? program)) >prf >append_length normalize <plus_n_Sm @le_S_S
     908   @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm @le_S_S
    909909   @le_plus_n_r
    910910 ]
     
    912912 -Hi; #Hi
    913913 [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:
    914   #Hj @(proj2 ?? (sig2 ?? policy) i (le_S_S_to_le … Hi))
     914  #Hj @(proj2 ?? (pi2 ?? policy) i (le_S_S_to_le … Hi))
    915915  >(nth_append_first ?? prefix ?? (le_S_S_to_le ?? Hi)) in Hj; //
    916916 ]
     
    922922    #i >append_length <commutative_plus #Hi #Hi2 normalize in Hi; >lookup_opt_insert_miss
    923923   [1,3,5,7,9,11,13,15,17,19,21:
    924      @(proj1 ?? (proj1 ?? (sig2 ?? policy)) i (le_S_to_le … Hi) Hi2)
     924     @(proj1 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_to_le … Hi) Hi2)
    925925   ]
    926926   >eq_bv_sym @bitvector_of_nat_abs
    927927   [1,4,7,10,13,16,19,22,25,28,31:
    928      @(transitive_lt … (sig2 ?? program)) >prf >append_length normalize <plus_n_Sm @le_S_S
     928     @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm @le_S_S
    929929     @le_plus_n_r
    930930   |2,5,8,11,14,17,20,23,26,29,32: @Hi2
     
    937937   >(nth_append_first ?? prefix ?? (le_S_S_to_le … Hi)) >lookup_opt_insert_miss
    938938   [1,3,5,7,9,11,13,15,17,19,21:
    939     @(proj2 ?? (proj1 ?? (sig2 ?? policy)) i (le_S_S_to_le … Hi))
     939    @(proj2 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi))
    940940   ]
    941941   @bitvector_of_nat_abs
     
    943943   |1,4,7,10,13,16,19,22,25,28,31: @(transitive_lt ??? (le_S_S_to_le ?? Hi))
    944944   ]
    945    @(transitive_lt … (sig2 ?? program))
     945   @(transitive_lt … (pi2 ?? program))
    946946   >prf >append_length normalize <plus_n_Sm @le_S_S @le_plus_n_r
    947947  ]
     
    957957  >(nth_append_first ?? prefix ?? (le_S_S_to_le … Hi)) #Hj >lookup_opt_insert_miss
    958958  [1,3,5,7,9,11,13,15,17,19,21:
    959    @(proj2 ?? (sig2 ?? policy) i (le_S_S_to_le … Hi) Hj)
     959   @(proj2 ?? (pi2 ?? policy) i (le_S_S_to_le … Hi) Hj)
    960960  ]
    961961  @bitvector_of_nat_abs
     
    963963  |1,4,7,10,13,16,19,22,25,28,31: @(transitive_lt ??? (le_S_S_to_le ?? Hi))
    964964  ]
    965   @(transitive_lt … (sig2 ?? program))
     965  @(transitive_lt … (pi2 ?? program))
    966966  >prf >append_length normalize <plus_n_Sm @le_S_S @le_plus_n_r
    967967 ]
     
    10281028[ @conj [ @conj #i >append_length <commutative_plus #Hi normalize in Hi;
    10291029[ #Hi2 cases (lookup ??? old_policy ?) #h #n cases add_instr
    1030   [ @(proj1 ?? (proj1 ?? (sig2 ?? policy)) i (le_S_to_le … Hi) Hi2)
     1030  [ @(proj1 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_to_le … Hi) Hi2)
    10311031  | #z normalize nodelta >lookup_opt_insert_miss
    1032     [ @(proj1 ?? (proj1 ?? (sig2 ?? policy)) i (le_S_to_le … Hi) Hi2)
     1032    [ @(proj1 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_to_le … Hi) Hi2)
    10331033    | >eq_bv_sym @bitvector_of_nat_abs
    1034       [ @(transitive_lt … (sig2 ?? program)) >prf >append_length normalize <plus_n_Sm
     1034      [ @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
    10351035        @le_S_S @le_plus_n_r
    10361036      | @Hi2
     
    10411041| cases (le_to_or_lt_eq … Hi) -Hi;
    10421042  [ #Hi; >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) @conj
    1043     [ #Hj lapply (proj2 ?? (proj1 ?? (sig2 ?? policy)) i (le_S_S_to_le … Hi)) #Hacc
     1043    [ #Hj lapply (proj2 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi)) #Hacc
    10441044      cases add_instr cases (lookup ??? old_policy ?) normalize nodelta #x #y
    10451045      [ @(proj1 ?? Hacc Hj)
     
    10491049        |1: @(transitive_lt ??? (le_S_S_to_le ?? Hi))
    10501050        ]
    1051         @(transitive_lt … (sig2 ?? program)) >prf >append_length normalize <plus_n_Sm
     1051        @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
    10521052        @le_S_S @le_plus_n_r
    10531053        ] ]
    10541054      ]
    1055     | lapply (proj2 ?? (proj1 ?? (sig2 ?? policy)) i (le_S_S_to_le … Hi)) #Hacc
     1055    | lapply (proj2 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi)) #Hacc
    10561056      #H elim H -H; #h #H elim H -H; #n cases add_instr cases (lookup ??? old_policy ?)
    10571057      normalize nodelta #x #y [2: #z]
     
    10611061        |1: @(transitive_lt ??? (le_S_S_to_le ?? Hi))
    10621062        ]
    1063         @(transitive_lt … (sig2 ?? program)) >prf >append_length normalize <plus_n_Sm
     1063        @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
    10641064        @le_S_S @le_plus_n_r
    10651065      | @Hl
     
    10711071     [3,5,11: #H @⊥ @H (* instr is not a jump *)
    10721072     |4,6,12: #H elim H -H; #h #H elim H -H #n cases (lookup ??? old_policy ?)
    1073        #x #y normalize nodelta >(proj1 ?? (proj1 ?? (sig2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
     1073       #x #y normalize nodelta >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
    10741074       [1,3,5: #H destruct (H)]
    1075        @(transitive_lt … (sig2 ?? program)) >prf >append_length normalize <plus_n_Sm
     1075       @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
    10761076       @le_S_S @le_plus_n_r
    10771077     |7,9: (* instr is a jump *) #_ cases (lookup ??? old_policy ?) #h #n
     
    10951095       |72,73,74: #H elim H -H; #h #H elim H -H #n cases (lookup ??? old_policy ?)
    10961096        #x #y normalize nodelta
    1097         >(proj1 ?? (proj1 ?? (sig2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
     1097        >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
    10981098        [1,3,5: #H destruct (H)]
    1099         @(transitive_lt … (sig2 ?? program)) >prf >append_length normalize <plus_n_Sm
     1099        @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
    11001100        @le_S_S @le_plus_n_r     
    11011101       |41,42,45,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69: #x
    11021102        #H elim H -H; #h #H elim H -H #n cases (lookup ??? old_policy ?)
    11031103        #x #y normalize nodelta
    1104         >(proj1 ?? (proj1 ?? (sig2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
     1104        >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
    11051105        [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35: #H destruct (H)]
    1106         @(transitive_lt … (sig2 ?? program)) >prf >append_length normalize <plus_n_Sm
     1106        @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
    11071107        @le_S_S @le_plus_n_r
    11081108       |38,39,40,43,44,70,71: #x #y #H elim H -H; #h #H elim H -H #n
    11091109        cases (lookup ??? old_policy ?) #x #y normalize nodelta
    1110         >(proj1 ?? (proj1 ?? (sig2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
     1110        >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
    11111111        [1,3,5,7,9,11,13: #H destruct (H)]
    1112         @(transitive_lt … (sig2 ?? program)) >prf >append_length normalize <plus_n_Sm
     1112        @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
    11131113        @le_S_S @le_plus_n_r             
    11141114       |46,47,51,52: #id #_ //
     
    11221122    cases (le_to_or_lt_eq … Hi) -Hi; #Hi
    11231123    [ cases (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,short_jump〉)
    1124       #x #y @((proj2 ?? (sig2 ?? policy)) i (le_S_S_to_le … Hi))
     1124      #x #y @((proj2 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi))
    11251125    | normalize nodelta >(injective_S … Hi)
    11261126      >lookup_opt_lookup_miss
     
    11291129        | cases (lookup ?? (bitvector_of_nat ? (|prefix|)) old_policy 〈0,short_jump〉)
    11301130          #x #y normalize nodelta
    1131           >(proj1 ?? (proj1 ?? (sig2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
     1131          >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
    11321132          [ //
    1133           | @(transitive_lt … (sig2 ?? program)) >prf >append_length normalize <plus_n_Sm
     1133          | @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
    11341134            @le_S_S @le_plus_n_r
    11351135          ]
     
    11601160    [ cases (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,short_jump〉)
    11611161      #y #z normalize nodelta normalize nodelta >lookup_insert_miss
    1162       [ @((proj2 ?? (sig2 ?? policy)) i (le_S_S_to_le … Hi))
     1162      [ @((proj2 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi))
    11631163      | @bitvector_of_nat_abs
    11641164        [3: @lt_to_not_eq @(le_S_S_to_le … Hi)
    11651165        |1: @(transitive_lt ??? (le_S_S_to_le … Hi))
    11661166        ]
    1167         @(transitive_lt … (sig2 ?? program)) >prf >append_length normalize <plus_n_Sm
     1167        @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
    11681168        @le_S_S @le_plus_n_r
    11691169      ]
    1170     | >(injective_S … Hi) elim (proj1 ?? (proj2 ?? (sig2 ?? old_policy) (|prefix|) ?) ?)
     1170    | >(injective_S … Hi) elim (proj1 ?? (proj2 ?? (pi2 ?? old_policy) (|prefix|) ?) ?)
    11711171      [ #a #H elim H -H; #b #H >H >(lookup_opt_lookup_hit … 〈a,b〉 H)
    11721172        normalize nodelta >lookup_insert_hit @jmpleq_max_length
     
    12071207  | S m ⇒ jump_expansion_step program (jump_expansion_internal program m)
    12081208  ].
    1209 [ @(proj1 ?? (sig2 ?? (jump_expansion_start program)))
    1210 | @(proj1 ?? (sig2 ?? (jump_expansion_step program (jump_expansion_internal program m))))
     1209[ @(proj1 ?? (pi2 ?? (jump_expansion_start program)))
     1210| @(proj1 ?? (pi2 ?? (jump_expansion_step program (jump_expansion_internal program m))))
    12111211]
    12121212qed.
     
    12491249     [ @refl
    12501250     | @(proj1 ?? (jump_not_in_policy program (eject … (jump_expansion_step program p2)) n Hn))
    1251        [ @(proj1 ?? (sig2 … (jump_expansion_step program p2)))
     1251       [ @(proj1 ?? (pi2 … (jump_expansion_step program p2)))
    12521252       | @Hnotjmp
    12531253       ]
    12541254     ]
    12551255   | @(proj1 ?? (jump_not_in_policy program (eject … (jump_expansion_step program p1)) n Hn))
    1256      [ @(proj1 ?? (sig2 ?? (jump_expansion_step program p1)))
     1256     [ @(proj1 ?? (pi2 ?? (jump_expansion_step program p1)))
    12571257     | @Hnotjmp
    12581258     ]
     
    13021302   (\snd (bvt_lookup ?? (bitvector_of_nat ? n) (jump_expansion_step program policy) 〈0,short_jump〉))) ? (|program|))
    13031303 [ #H elim H; -H #i #Hi @(ex_intro ?? i) @Hi
    1304  | #abs @⊥ @(absurd ?? Hp) #n #Hn cases (proj2 ?? (sig2 ?? (jump_expansion_step program policy)) n Hn)
     1304 | #abs @⊥ @(absurd ?? Hp) #n #Hn cases (proj2 ?? (pi2 ?? (jump_expansion_step program policy)) n Hn)
    13051305   [ #Hj @⊥ @(absurd ?? abs) @(ex_intro ?? n) @conj [ @Hn | @Hj ]
    13061306   | #H @H
     
    13551355  [ #Hp #acc normalize @le_n
    13561356  | #h #t #Hind #Hp #acc
    1357     cases (proj2 ?? (sig2 ?? (jump_expansion_step program policy)) (|t|) ?)
     1357    cases (proj2 ?? (pi2 ?? (jump_expansion_step program policy)) (|t|) ?)
    13581358    [ whd in match (measure_int ???); whd in match (measure_int ?(jump_expansion_step ??)?);
    13591359      cases (\snd (bvt_lookup ?? (bitvector_of_nat ? (|t|)) policy 〈0,short_jump〉))
     
    14531453     [ @(transitive_le … Hp) //
    14541454     | whd in match (measure_int ???) in Hm; whd in match (measure_int ?(jump_expansion_step ??)?) in Hm;
    1455        lapply (proj2 ?? (sig2 ?? (jump_expansion_step program policy)) (|t|) ?)
     1455       lapply (proj2 ?? (pi2 ?? (jump_expansion_step program policy)) (|t|) ?)
    14561456       [ @(lt_to_le_to_lt … (|h::t|)) [ // | @Hp ]
    14571457       | cases (\snd (bvt_lookup ?? (bitvector_of_nat ? (|t|)) policy 〈0,short_jump〉)) in Hm;
     
    14761476   | #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm; 
    14771477     whd in match (measure_int ?(jump_expansion_step ??)?) in Hm;
    1478      lapply (proj2 ?? (sig2 ?? (jump_expansion_step program policy)) (|t|) ?)
     1478     lapply (proj2 ?? (pi2 ?? (jump_expansion_step program policy)) (|t|) ?)
    14791479     [ @(lt_to_le_to_lt … (|h::t|)) [ // | @Hp ]
    14801480     | cases (\snd (bvt_lookup ?? (bitvector_of_nat ? (|t|)) policy 〈0,short_jump〉)) in Hm;
     
    15011501 | #h #t #Hind #Hp whd in match (measure_int ???);
    15021502   cases (dec_is_jump (nth (|t|) ? program 〈None ?, Comment []〉)) #Hj
    1503    [ >(lookup_opt_lookup_hit … (proj2 ?? (sig2 ?? (jump_expansion_start program)) (|t|) ? Hj) 〈0,short_jump〉)
     1503   [ >(lookup_opt_lookup_hit … (proj2 ?? (pi2 ?? (jump_expansion_start program)) (|t|) ? Hj) 〈0,short_jump〉)
    15041504     [ normalize nodelta @Hind @le_S_to_le ]
    15051505     @Hp
     
    15341534   [ lapply (measure_full program (jump_expansion_internal program (2*|program|)))
    15351535     #Hfull #i #Hi
    1536      lapply (proj2 ?? (sig2 ?? (jump_expansion_step program (jump_expansion_internal program (2*|program|)))) i Hi)
     1536     lapply (proj2 ?? (pi2 ?? (jump_expansion_step program (jump_expansion_internal program (2*|program|)))) i Hi)
    15371537     >(Hfull ? i Hi)
    15381538     [ cases (\snd (bvt_lookup ?? (bitvector_of_nat 16 i) (jump_expansion_step program (jump_expansion_internal program (2*|program|))) 〈0,short_jump〉))
     
    17001700  match sigma_safe p (eject … policy) return λr:option (Word → Word). r ≠ None … → Word → Word with
    17011701   [ None ⇒ λabs. ⊥
    1702    | Some r ⇒ λ_.r] (sig2 … policy).
     1702   | Some r ⇒ λ_.r] (pi2 … policy).
    17031703 cases abs /2/
    17041704qed.
     
    17351735   sigma00 program pol prefix (Some … 〈0, 〈0, Stub …〉〉) ≠ None ….
    17361736 * #preamble #instr_list #pol #suffix #prefix #prf whd in prf:(???%);
    1737  generalize in match (sig2 ?? pol); whd in prf:(???%); <prf in pol; #pol
     1737 generalize in match (pi2 ?? pol); whd in prf:(???%); <prf in pol; #pol
    17381738 whd in match policy_ok; whd in match sigma_safe; whd in match sigma0;
    17391739 normalize nodelta >sigma00_append
     
    17741774    | Some res ⇒ res ].
    17751775 [ @⊥ whd in p:(??%??);
    1776    generalize in match (sig2 ?? pol); whd in ⊢ (% → ?);
     1776   generalize in match (pi2 ?? pol); whd in ⊢ (% → ?);
    17771777   whd in ⊢ (?(??%?) → ?); change with (sigma00 ????) in ⊢ (?(??(match % with [_ ⇒ ? | _ ⇒ ?])?) → ?);
    17781778   generalize in match (refl … (sigma00 program pol (\snd program) (Some ? 〈O,〈O,Stub (BitVector 16) 16〉〉)));
     
    18481848   = assembly_1_pseudoinstruction_safe program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi.
    18491849 #program #pol #ppc #lookup_labels #lookup_datalabels #pi #prf1 #prf2 #prf3
    1850  cases (sig2 … (assembly_1_pseudoinstruction' program pol ppc lookup_labels lookup_datalabels pi prf1 prf2 prf3))
     1850 cases (pi2 … (assembly_1_pseudoinstruction' program pol ppc lookup_labels lookup_datalabels pi prf1 prf2 prf3))
    18511851 #H1 #_ @H1
    18521852qed.
     
    19231923  whd in match tech_pc_sigma00 in ⊢ %; normalize nodelta;
    19241924  whd in match sigma00 in ⊢ %; normalize nodelta in ⊢ %;
    1925   generalize in match (sig2 … pol) whd in ⊢ (% → ?) whd in ⊢ (?(??%?) → ?)
     1925  generalize in match (pi2 … pol) whd in ⊢ (% → ?) whd in ⊢ (?(??%?) → ?)
    19261926  whd in match sigma0; normalize nodelta;
    19271927  >foldl_step
     
    20042004      let 〈pc, costs〉 ≝ pc_costs in
    20052005        〈labels, costs〉.
    2006  [2: whd generalize in match (sig2 … t); >p >p1 >p2 >p3 * * * #IHn1 #IH0 #IH1 #IH2
     2006 [2: whd generalize in match (pi2 … t); >p >p1 >p2 >p3 * * * #IHn1 #IH0 #IH1 #IH2
    20072007   generalize in match (refl … construct); cases construct in ⊢ (???% → %); #PC #CODE #JMEQ % [% [%]]
    20082008   [ <(construct_costs_sigma … costs i1 IHn1) change with (? = ?(\fst construct)) >JMEQ %
     
    20202020          <(address_of_word_labels_code_mem_Some_miss … EQ … H) @IH2 assumption ]]]
    20212021 |3: whd % [% [%]] [>sigma_0 % | % | % | #id normalize in ⊢ (% → ?); #abs @⊥ // ]
    2022  | generalize in match (sig2 … result) in ⊢ ?;
     2022 | generalize in match (pi2 … result) in ⊢ ?;
    20232023   normalize nodelta in p ⊢ %; -result; >p in ⊢ (match % with [_ ⇒ ?] → ?);
    20242024   normalize nodelta; >p1 normalize nodelta; >p2; normalize nodelta; * #_; #H @H]
  • src/ASM/Interpret.ma

    r1600 r1606  
    608608  clock ? (execute_1_preinstruction ticks a m f i s) = \fst ticks + clock … s ∨
    609609  clock ? (execute_1_preinstruction ticks a m f i s) = \snd ticks + clock … s.
    610  #ticks #a #m #f #i #s whd in match execute_1_preinstruction; normalize nodelta @sig2
     610 #ticks #a #m #f #i #s whd in match execute_1_preinstruction; normalize nodelta @pi2
    611611qed.
    612612
     
    712712      ]. (*10s*)
    713713    [||||||||*:try assumption]
    714     [1,2,3,4,5,7: @sig2 (*35s*)
     714    [1,2,3,4,5,7: @pi2 (*35s*)
    715715    |8: lapply (execute_1_preinstruction_ok 〈ticks, ticks〉 [[ relative ]] ?
    716716        (λx. λs.
     
    736736
    737737lemma execute_1_ok: ∀s. clock … (execute_1 s) = current_instruction_cost s + clock … s.
    738  #s whd in match execute_1; normalize nodelta @sig2
     738 #s whd in match execute_1; normalize nodelta @pi2
    739739qed-. (*x Andrea: indexing takes ages here *)
    740740
  • src/ASM/Interpret2.ma

    r1550 r1606  
    4646 let 〈instr_pc,ticks〉 ≝ fetch (code_memory … s) (program_counter … s) in
    4747 let 〈instr,pc〉 ≝ instr_pc in
    48  let s ≝ eject … (execute_1 s) in
    4948 match lookup_opt … pc costs with
    5049 [ None ⇒ ret … 〈E0, s〉
    51  | Some cst ⇒ ret … 〈Echarge cst, s〉 ].
     50 | Some cst ⇒ ret … 〈Echarge cst, execute_1 s〉 ].
    5251
    5352axiom is_final: BitVectorTrie costlabel 16 → Status → option int.
  • src/ASM/StatusProofs.ma

    r1530 r1606  
    110110    ∀prf:is_in ?
    111111     [[direct;indirect;registr;acc_a;acc_b;ext_indirect;ext_indirect_dptr]] b.
    112   eject … (set_arg_8 ? (set_code_memory T U ps code_mem) b val) =
     112  set_arg_8 ? (set_code_memory T U ps code_mem) b val =
    113113  set_code_memory T U (set_arg_8 ? ps b val) code_mem.
    114114  [2,3: cases b in prf; *; normalize //]
    115115  #n #l #T #U #ps #code_mem #val * *;
    116   #x try (#y #H) try #H whd in H; try cases H
    117   whd in ⊢ (??(???(%))?); whd in ⊢ (???(???(???(%))?)); try %
     116  #x try (#y #H) try #H whd in H; try cases H try %
     117  whd in match set_arg_8; normalize nodelta
     118  whd in match set_arg_8'; normalize nodelta
    118119  cases (split bool 4 4 ?) #nu' #nl' normalize nodelta
    119120  cases (split bool 1 3 nu') #bit1' #ignore' normalize nodelta
     
    132133    ∀prf:is_in ?
    133134     [[direct;indirect;registr;acc_a;acc_b;ext_indirect;ext_indirect_dptr]] b.
    134   eject … (set_arg_8 ? (set_program_counter T ps pc) b val) =
     135  set_arg_8 ? (set_program_counter T ps pc) b val =
    135136  set_program_counter T (set_arg_8 ? ps b val) pc.
    136137  [2,3: cases b in prf; *; normalize //]
    137138  #n #l #T #ps #pc #val * *;
    138   #x try (#y #H) try #H whd in H; try cases H
    139   whd in ⊢ (??(???(%))?); whd in ⊢ (???(??(%)?)); try %
     139  #x try (#y #H) try #H whd in H; try cases H try %
     140  whd in match set_arg_8; normalize nodelta
     141  whd in match set_arg_8'; normalize nodelta
    140142  cases (split bool 4 4 ?) #nu' #nl' normalize nodelta
    141143  cases (split bool 1 3 nu') #bit1' #ignore' normalize nodelta
Note: See TracChangeset for help on using the changeset viewer.