Changeset 2714 for src/ASM


Ignore:
Timestamp:
Feb 22, 2013, 11:20:03 PM (7 years ago)
Author:
sacerdot
Message:

PolicyStep?.ma repaired

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/PolicyStep.ma

    r2652 r2714  
    7171 | <Heq2 >Hi >lookup_insert_miss
    7272   [ >lookup_insert_hit cases instr in Heq1;
    73      [2,3,6: #x [3: #y] normalize nodelta #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) #_ @refl
    74      |4,5: #x normalize nodelta #Heq1 >nth_append_second try %
     73     [2,3,8: #x [3: #y] normalize nodelta #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) #_ @refl
     74     |5,6: #x #y #z normalize nodelta #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) #_ %
     75     |4,7: #x normalize nodelta #Heq1 >nth_append_second try %
    7576           <minus_n_n #abs cases abs
    7677     |1: #pi normalize nodelta >nth_append_second [2: @le_n] <minus_n_n whd in match (nth ????);
     
    146147   |Comment (_:String)⇒None jump_length
    147148   |Cost (_:costlabel)⇒None jump_length
     149   |Jnz _ _ _ ⇒ None ?
     150   |MovSuccessor _ _ _ ⇒ None ?
    148151   |Jmp (j:Identifier)⇒
    149152    Some jump_length
     
    203206        [ >lookup_insert_hit normalize nodelta
    204207          inversion instr in Heq1; normalize nodelta
    205           [4,5: #x #_ #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) @jmpleq_max_length
     208          [4,7: #x #_ #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) @jmpleq_max_length
    206209          | #pi #Heqi whd in match jump_expansion_step_instruction; normalize nodelta
    207210            lapply (destination_of_None_to_is_jump_false pi)
     
    211214            | #tgt #_ #_ #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) @jmpleq_max_length
    212215            ]
    213           |2,3,6: #x [3: #y] #Heqi ]
     216          |5,6: #x #y #z #Heqi
     217          |2,3,8: #x [3: #y] #Heqi ]
    214218          #Hj <(proj1 ?? (pair_destruct ?????? Hj))
    215219          lapply (pi2 ?? old_sigma (|prefix|) ??) try assumption
    216           [1,3,5,7: >prf >nth_append_second try @le_n
     220          [1,3,5,7,9,11: >prf >nth_append_second try @le_n
    217221            <minus_n_n whd in match (nth ????); >p1 >Heqi
    218222            whd in match is_jump; normalize nodelta try % >Hx %
     
    261265   |Comment (_:String)⇒None jump_length
    262266   |Cost (_:costlabel)⇒None jump_length
     267   |Jnz _ _ _ ⇒ None ?
     268   |MovSuccessor _ _ _ ⇒ None ?
    263269   |Jmp (j:Identifier)⇒
    264270    Some jump_length
     
    426432    >Hpolicy1
    427433    [ cases instr in Heq1 Heq;
    428       [2,3,6: #x [3: #y] normalize nodelta #_ #_ %
     434      [2,3,8: #x [3: #y] normalize nodelta #_ #_ %
     435      |5,6: #x #y #z #_ #_ %
    429436      |1: #pi normalize nodelta whd in match jump_expansion_step_instruction;
    430437          normalize nodelta cases (destination_of ?) normalize nodelta [#_ #_ %]]
     
    575582            cases (destination_of ?) normalize nodelta
    576583            [ #_ #dest_None | #tgt #dest_Some #_ ]]
     584            try (#x #y #z #Heq1 #Hadded #X)
    577585            try (#x #y #Heq1 #Hadded #X) try (#x #Heq1 #Hadded #X) try (#Heq1 #Hadded #X)
    578586            <(proj2 ?? (pair_destruct ?????? Heq1)) >X @plus_left_monotone
    579             [1,3,4,7: @instruction_size_irrelevant try %
     587            [1,3,4,6,7,9: @instruction_size_irrelevant try %
    580588              whd in match is_jump; normalize nodelta >dest_None %
    581589            |*: >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) in Holdeq; #EQ'
     
    718726    (* USE: sigma_compact_unsafe (from old_sigma) *)
    719727    lapply (proj1 ?? (pi2 ?? old_sigma) (|prefix|) ?)
    720     [1,3,5,7,9,11,13,15: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r]
     728    [1,3,5,7,9,11,13,15,17: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r]
    721729    lapply Holdeq -Holdeq
    722730    inversion (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma))
    723     [1,3,5,7,9,11,13,15: normalize nodelta #_ #_ #abs cases abs]
     731    [1,3,5,7,9,11,13,15,17: normalize nodelta #_ #_ #abs cases abs]
    724732    inversion (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma))
    725     [1,3,5,7,9,11,13,15: normalize nodelta #_ * #Spc #Sj normalize nodelta #_ #_ #abs cases abs]
     733    normalize nodelta
     734    [1,3,5,7,9,11,13,15,17: #_ * #Spc #Sj normalize nodelta #_ #_ #abs cases abs]
    726735    * #Spc #Sj #EQS * #pc #j #Holdeq #EQ normalize nodelta
    727736    #H (* USE: fst p = lookup |prefix| *) (*CSC: This part of the proof is repeated somewhere else*)
     
    729738    (* USE[pass]: lookup p = lookup old_sigma + added *)
    730739    >Hpolicy2
    731     [1,3,4,7:
     740    [1,3,4,6,7,9:
    732741      >(lookup_opt_lookup_hit … Holdeq 〈0,short_jump〉) in EQ;
    733742      -Holdeq #EQ <(proj1 ?? (pair_destruct ?????? EQ))
     
    737746      @plus_right_monotone @instruction_size_irrelevant try %
    738747      whd in match is_jump; normalize nodelta >y %
    739     |2,5,6:
     748    |2,5,6,8:
    740749      >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) >H
    741750      >(lookup_opt_lookup_hit … Holdeq 〈0,short_jump〉) in EQ; #EQ
     
    859868   |Comment (_:String)⇒None jump_length
    860869   |Cost (_:costlabel)⇒None jump_length
     870   |Jnz _ _ _ ⇒ None ?
     871   |MovSuccessor _ _ _ ⇒ None ?
    861872   |Jmp (j:Identifier)⇒
    862873    Some jump_length
     
    9911002      ]
    9921003      normalize nodelta cases instr in Hjump Heq1;
    993       [1,7: #pi normalize nodelta cases pi
     1004      [1,9: #pi normalize nodelta cases pi
    9941005        try (#y #id #Hjump #Heq1) try (#id #Hjump #Heq1) try (#Hjump #Heq1)
    9951006        try (cases Hjump) lapply Heq1 -Heq1 lapply Hjump -Hjump lapply id -id
    996       |2,3,6,8,9,12: #y [3,6: #id] normalize nodelta #abs cases abs
     1007      |2,3,8,10,11,16: #y [3,6: #id] normalize nodelta #abs cases abs
     1008      |5,6,13,14: #x #y #z #abs cases abs
    9971009      ]
    9981010      #id #Hjump normalize nodelta #Heq1
     
    10401052          #Holdeq >prf >nth_append_second [2: @le_n] <minus_n_n whd in match (nth ????);
    10411053          >p1 cases instr in Hjump Heq1;
    1042           [1,7: #pi normalize nodelta cases pi
     1054          [1,9: #pi normalize nodelta cases pi
    10431055            try (#y #id #Hjump #Heq1) try (#id #Hjump #Heq1) try (#Hjump #Heq1)
    10441056            try (cases Hjump) lapply Heq1 -Heq1 lapply Hjump -Hjump lapply id -id
    1045           |2,3,6,8,9,12: #y [3,6: #id] normalize nodelta #abs cases abs
     1057          |2,3,8,10,11,16: #y [3,6: #id] normalize nodelta #abs cases abs
     1058          |5,6,13,14: #x #y #z #abs cases abs
    10461059          ]
    10471060          #id #Hjump normalize nodelta <Hjump #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1))
Note: See TracChangeset for help on using the changeset viewer.