Changeset 2220 for src/ASM


Ignore:
Timestamp:
Jul 20, 2012, 2:05:56 AM (7 years ago)
Author:
sacerdot
Message:

Some minor speed up and daemon-uncommenting.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/PolicyStep.ma

    r2215 r2220  
    266266    >append_length >(commutative_plus (|prefix|)) >lookup_insert_hit @refl
    267267  ]
    268   | (* jump_increase *) cases daemon
    269     (* #i >append_length >commutative_plus #Hi normalize in Hi;
     268  | (* jump_increase *) (* cases daemon *)
     269    #i >append_length >commutative_plus #Hi normalize in Hi;
    270270    cases (le_to_or_lt_eq … Hi) -Hi; #Hi
    271271    [ cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
     
    275275        @pair_elim #opc #oj #EQ1 >lookup_insert_miss
    276276        [ >lookup_insert_miss
    277           [ @pair_elim #pc #j #EQ2 / by /
     277          [ @pair_elim #pc #j #EQ2 #X @X
    278278          | @bitvector_of_nat_abs
    279279            [ @(transitive_lt ??? Hi) ]
     
    290290          ]
    291291        ]
    292       | >Hi <(proj2 ?? (pair_destruct ?????? Heq2)) @pair_elim #opc #oj #EQ1
     292      | >Hi <(proj2 ?? (pair_destruct ?????? Heq2)) >Holdeq normalize nodelta
    293293        >lookup_insert_miss
    294294        [ >lookup_insert_hit cases (dec_is_jump instr)
     
    300300              |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y]
    301301                whd in match jump_expansion_step_instruction; normalize nodelta #Heq1
    302                 #_ <(proj1 ?? (pair_destruct ?????? Heq1)) >Holdeq in EQ1; normalize nodelta
    303                 #H42 >(proj2 ?? (pair_destruct ?????? H42)) @jmpleq_max_length
     302                #_ <(proj1 ?? (pair_destruct ?????? Heq1))
     303                @jmpleq_max_length
    304304              ]
    305305            |2,3,6: #x [3: #y] #_ #Hj cases Hj
    306             |4,5: #x #Heq1 #_ <(proj1 ?? (pair_destruct ?????? Heq1)) >Holdeq in EQ1;
    307               normalize nodelta #H42 >(proj2 ?? (pair_destruct ?????? H42)) @jmpleq_max_length
     306            |4,5: #x #Heq1 #_ <(proj1 ?? (pair_destruct ?????? Heq1)) @jmpleq_max_length
    308307            ]
    309308          | lapply Heq1 -Heq1; lapply (refl ? instr); cases instr in ⊢ (???% → %); normalize nodelta
     
    326325                  >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
    327326                |3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,60,63,66,69,72,75,78,81,84:
    328                   cases (lookup ?? (bitvector_of_nat ? (|prefix|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in EQ1;
    329                   #a #b #EQ1 >(proj2 ?? (pair_destruct ?????? EQ1)) #EQ2 >EQ2
    330                   %2 @refl
     327                  >Holdeq #EQ2 >EQ2 %2 @refl
    331328                ]
    332329              |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y]
    333                 #_ #_ #abs cases abs #ABS @⊥ @ABS / by I/
     330                #_ #_ #abs @⊥ @(absurd ? I abs)
    334331              ]
    335332            |2,3,6: #x [3: #y] #Heqi #Heq1 #Hj <(proj1 ?? (pair_destruct ?????? Heq1))
     
    341338                ]
    342339              |2,5,8: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
    343               |3,6,9:
    344                 cases (lookup ?? (bitvector_of_nat ? (|prefix|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in EQ1;
    345                 #a #b #EQ1 >(proj2 ?? (pair_destruct ?????? EQ1)) #EQ2 >EQ2 %2 @refl
    346               ]
    347             |4,5: #x #_ #_ #abs cases abs #ABS @⊥ @ABS / by I/
     340              |3,6,9: >Holdeq #EQ2 >EQ2 %2 @refl
     341              ]
     342            |4,5: #x #_ #_ #abs @⊥ @(absurd ? I abs)
    348343            ]
    349344          ]
     
    357352      ]
    358353    | <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_hit
    359       normalize nodelta 
     354      normalize nodelta
    360355      cases (bvt_lookup … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma) 〈0,short_jump〉)
    361356      #a #b normalize nodelta %2 @refl
    362     ] *)
    363   ]
    364   | (* sigma_compact_unsafe *) cases daemon
    365     (* #i >append_length <commutative_plus #Hi normalize in Hi;
     357    ]
     358  ]
     359  | (* sigma_compact_unsafe *)
     360    #i >append_length <commutative_plus #Hi normalize in Hi;
    366361    <(proj2 ?? (pair_destruct ?????? Heq2))
    367362    cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
     
    375370                [ @le_S_to_le @Hi ]
    376371                cases (bvt_lookup_opt … (bitvector_of_nat ? i) inc_sigma)
    377                 [ normalize nodelta / by /
     372                [ normalize nodelta #X @X
    378373                | #x cases x -x #x1 #x2
    379374                  cases (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma)
    380375                  normalize nodelta
    381                   [ / by /
     376                  [ #X @X
    382377                  | #y cases y -y #y1 #y2 normalize nodelta >nth_append_first
    383                     [ / by /
     378                    [ #X @X
    384379                    | @le_S_to_le @Hi
    385380                    ]
     
    394389              [ <Hi @le_n
    395390              | cases (bvt_lookup_opt … (bitvector_of_nat ? i) inc_sigma)
    396                 [ normalize nodelta / by /
     391                [ normalize nodelta #X @X
    397392                | #x cases x -x #x1 #x2
    398393                  (* USE: inc_pc = fst inc_sigma *)
     
    403398                  | #y cases y -y #y1 #y2 #Heq >nth_append_first
    404399                    [ normalize nodelta >(lookup_opt_lookup_hit … Heq 〈0,short_jump〉)
    405                       #Heq2 <Heq2 / by /
     400                      #Heq2 <Heq2 #X @X
    406401                    | <Hi @le_n
    407402                    ]
     
    465460        ]
    466461      ]
    467     ] *)
    468   ]
    469   | (* policy_jump_equal → added = 0 *) cases daemon
    470     (* <(proj2 ?? (pair_destruct ?????? Heq2))
     462    ]
     463  ]
     464  | (* policy_jump_equal → added = 0 *)
     465    <(proj2 ?? (pair_destruct ?????? Heq2))
    471466    #Heq <(proj1 ?? (pair_destruct ?????? Heq2))
    472467    (* USE[pass]: policy_jump_equal → added = 0 *)
     
    483478        [1,3: >lookup_insert_hit <(proj1 ?? (pair_destruct ?????? Heq1))
    484479          #Heq <Heq cases (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉)
    485           #y #z #Hyz >(proj2 ?? (pair_destruct ?????? Hyz)) <minus_n_n / by /
     480          #y #z #Hyz >(proj2 ?? (pair_destruct ?????? Hyz)) <minus_n_n %
    486481        |2,4: @bitvector_of_nat_abs
    487482          [1,4: @le_S_to_le]
     
    502497          [1,3,5,7,9,11,13,15,17: >append_length <plus_n_Sm @le_S_S @le_plus_n_r]
    503498          -Heq >lookup_insert_miss
    504           [1,3,5,7,9,11,13,15,17: >lookup_insert_hit <(proj1 ?? (pair_destruct ?????? Heq1))
     499          [1,3,5,7,9,11,13,15,17: >lookup_insert_hit in ⊢ (???(???%) → ?); <(proj1 ?? (pair_destruct ?????? Heq1))
    505500            #Heq <Heq cases (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉)
    506501            #y #z #Hyz >(proj2 ?? (pair_destruct ?????? Hyz)) <minus_n_n / by /
     
    534529        ]
    535530      ]
    536     ] *)
     531    ]
    537532  ]
    538533  | (* added = 0 → policy_pc_equal *) cases daemon
Note: See TracChangeset for help on using the changeset viewer.