Changeset 2248


Ignore:
Timestamp:
Jul 24, 2012, 7:15:24 PM (7 years ago)
Author:
sacerdot
Message:

Final changes. All daemons removed, but the real one (open goal).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/PolicyStep.ma

    r2246 r2248  
    453453
    454454lemma jump_expansion_step6:
    455  ∀program : list labelled_instruction.(*
    456   (Σl:list labelled_instruction.S (|l|)< 2 \sup 16 ∧is_well_labelled_p l)*)
    457  ∀labels : label_map.(*
    458   (Σlm:label_map
    459    .(∀l:identifier ASMTag
    460      .occurs_exactly_once ASMTag pseudo_instruction l program
    461       →bitvector_of_nat 16 (lookup_def ASMTag ℕ lm l O)
    462        =address_of_word_labels_code_mem program l))*)
    463  ∀old_sigma :
    464    Σpolicy:ppc_pc_map
    465    .(*not_jump_default program policy
    466     ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd  policy)
    467                  〈O,short_jump〉)
    468      =O
    469     ∧\fst  policy
    470      =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|program|))
    471                   (\snd  policy) 〈O,short_jump〉)
    472     ∧*)sigma_compact_unsafe program labels policy
    473     (*∧\fst  policy≤ 2 \sup 16*).
     455 ∀program : list labelled_instruction.
     456 ∀labels : label_map.
     457 ∀old_sigma : Σpolicy:ppc_pc_map.sigma_compact_unsafe program labels policy.
    474458 ∀prefix : list (option Identifier×pseudo_instruction).
    475459 ∀x : option Identifier×pseudo_instruction.
    476460 ∀tl : list (option Identifier×pseudo_instruction).
    477  ∀prf : program=prefix@[x]@tl.(*
    478  acc :
    479   (Σx0:ℕ×ppc_pc_map
    480    .(let 〈added,policy〉 ≝x0 in 
    481      not_jump_default prefix policy
    482      ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd  policy)
    483                   〈O,short_jump〉)
    484       =O
    485      ∧\fst  policy
    486       =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
    487                    (\snd  policy) 〈O,short_jump〉)
    488      ∧jump_increase prefix old_sigma policy
    489      ∧sigma_compact_unsafe prefix labels policy
    490      ∧(sigma_jump_equal prefix old_sigma policy→added=O)
    491      ∧(added=O→sigma_pc_equal prefix old_sigma policy)
    492      ∧out_of_program_none prefix policy
    493      ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
    494                   (\snd  policy) 〈O,short_jump〉)
    495       =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
    496                    (\snd  old_sigma) 〈O,short_jump〉)
    497        +added
    498      ∧sigma_safe prefix labels added old_sigma policy))*)
     461 ∀prf : program=prefix@[x]@tl.
    499462 ∀inc_added : ℕ.
    500  ∀inc_pc_sigma : ppc_pc_map.(*
    501  p : (acc≃〈inc_added,inc_pc_sigma〉)*)
     463 ∀inc_pc_sigma : ppc_pc_map.
    502464 ∀label : option Identifier.
    503465 ∀instr : pseudo_instruction.
    504  ∀p1 : x≃〈label,instr〉.(*
    505  add_instr ≝
    506   match instr
    507    in pseudo_instruction
    508    return λ_:pseudo_instruction.(option jump_length)
    509    with 
    510   [Instruction (i:(preinstruction Identifier))⇒
    511    jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
    512    (|prefix|) i
    513   |Comment (_:String)⇒None jump_length
    514   |Cost (_:costlabel)⇒None jump_length
    515   |Jmp (j:Identifier)⇒
    516    Some jump_length
    517    (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
    518   |Call (c:Identifier)⇒
    519    Some jump_length
    520    (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
    521   |Mov (_:[[dptr]])   (_0:Identifier)⇒None jump_length]*)
     466 ∀p1 : x≃〈label,instr〉.
    522467 ∀inc_pc : ℕ.
    523  ∀inc_sigma : BitVectorTrie (ℕ×jump_length) 16.(*
    524  Hips : (inc_pc_sigma=〈inc_pc,inc_sigma〉)*)
     468 ∀inc_sigma : BitVectorTrie (ℕ×jump_length) 16.
    525469 ∀old_pc : ℕ.
    526470 ∀old_length : jump_length.
     
    529473   〈O,short_jump〉
    530474   =〈old_pc,old_length〉.
    531  ∀Hpolicy1 :(*
    532   (not_jump_default prefix 〈inc_pc,inc_sigma〉
    533    ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) inc_sigma
    534                 〈O,short_jump〉)
    535     =O
    536    ∧inc_pc
    537     =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) inc_sigma
    538                  〈O,short_jump〉)
    539    ∧jump_increase prefix old_sigma 〈inc_pc,inc_sigma〉
    540    ∧sigma_compact_unsafe prefix labels 〈inc_pc,inc_sigma〉
    541    ∧(sigma_jump_equal prefix old_sigma 〈inc_pc,inc_sigma〉→inc_added=O)
    542    ∧( *)inc_added=O→sigma_pc_equal prefix old_sigma 〈inc_pc,inc_sigma〉.(*)
    543    ∧out_of_program_none prefix 〈inc_pc,inc_sigma〉
    544    ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) inc_sigma
    545                 〈O,short_jump〉)
    546     =old_pc+inc_added
    547    ∧sigma_safe prefix labels inc_added old_sigma 〈inc_pc,inc_sigma〉)*)
    548  ∀Hpolic2: inc_pc
    549     =\fst  (lookup … (bitvector_of_nat … (|prefix|)) inc_sigma 〈O,short_jump〉).
     475 ∀Hpolicy1 : inc_added=O→sigma_pc_equal prefix old_sigma 〈inc_pc,inc_sigma〉.
     476 ∀Hpolic2: inc_pc =\fst  (lookup … (bitvector_of_nat … (|prefix|)) inc_sigma 〈O,short_jump〉).
    550477 ∀added : ℕ.
    551478 ∀policy : ppc_pc_map.
     
    588515    (* USE[pass]: added = 0 → policy_pc_equal *)
    589516    lapply Hpolicy1 <Heq2b <Heq2a lapply Heq1 -Heq1
    590     inversion instr normalize nodelta
    591     [ #pi #Hins whd in match jump_expansion_step_instruction; normalize nodelta
    592       lapply (destination_of_None_to_is_jump_false pi)
    593       lapply (destination_of_Some_to_is_jump_true pi)
    594       cases (destination_of ?) normalize nodelta
    595       [ #_ #dest_None | #tgt #dest_Some #_ ]]
    596     try (#x #y #Hins #Heq1 #Hold #Hadded #i #Hi)
    597     try (#x #Hins #Heq1 #Hold #Hadded #i #Hi)
    598     try (#Heq1 #Hold #Hadded #i #Hi)
     517    #Hins #Hold #Hadded #i #Hi
    599518    >append_length in Hi; >commutative_plus #Hi normalize in Hi;
    600519    cases (le_to_or_lt_eq … Hi) -Hi #Hi
    601     [1,3,5,7,9,11,13: cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    602       [1,3,5,7,9,11,13: <Heq2b >lookup_insert_miss
    603         [1,3,5,7,9,11,13: >lookup_insert_miss
    604           [1,3,5,7,9,11,13:
     520    [ cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
     521      [ <Heq2b >lookup_insert_miss
     522        [ >lookup_insert_miss
     523          [ cases instr in Hadded; normalize nodelta
     524            [ whd in match jump_expansion_step_instruction; normalize nodelta
     525              #pi cases (destination_of ?) normalize nodelta ]
     526            try (#x #y #Hadded) try (#x #Hadded) try #Hadded
    605527            try @(Hold Hadded i (le_S_to_le … Hi))
    606528            @(Hold ? i (le_S_to_le … Hi)) >commutative_plus in Hadded; @plus_zero_zero
    607           |*: @bitvector_of_nat_abs try assumption
    608             [2,4,6,8,10,12,14: @lt_to_not_eq @Hi
    609             |*: @(transitive_lt ??? Hi) assumption ]]
    610         |*: @bitvector_of_nat_abs try assumption
    611           [2,4,6,8,10,12,14: @lt_to_not_eq @le_S @Hi
    612           |*: @(transitive_lt … Hi) assumption ]]
    613       |*: >Hi >lookup_insert_miss
    614         [1,3,5,7,9,11,13: >lookup_insert_hit
     529          | @bitvector_of_nat_abs try assumption
     530            [2: @lt_to_not_eq @Hi
     531            | @(transitive_lt ??? Hi) assumption ]]
     532        | @bitvector_of_nat_abs try assumption
     533          [2: @lt_to_not_eq @le_S @Hi
     534          | @(transitive_lt … Hi) assumption ]]
     535      | >Hi >lookup_insert_miss
     536        [ cases instr in Hadded; normalize nodelta
     537          [ whd in match jump_expansion_step_instruction; normalize nodelta
     538            #pi cases (destination_of ?) normalize nodelta ]
     539          try (#x #y #Hadded) try (#x #Hadded) try #Hadded
     540          >lookup_insert_hit
    615541          try (>(Hold Hadded (|prefix|) (le_n (|prefix|)))
    616542               @sym_eq (* USE: fst p = lookup |prefix| *)
     
    625551      (* USE fst p = lookup |prefix| *)
    626552      >Hpolicy2
    627       <(Hold ? (|prefix|) (le_n (|prefix|))) try @Hadded
    628       [3,7,9: @plus_zero_zero [2,4,6: >commutative_plus @Hadded |*: skip]]
     553      <(Hold ? (|prefix|) (le_n (|prefix|)))
     554      [2: cases instr in Hadded; normalize nodelta
     555          [ whd in match jump_expansion_step_instruction; normalize nodelta
     556            #pi cases (destination_of ?) normalize nodelta ]
     557          try (#x #y #Hadded) try (#x #Hadded) try #Hadded
     558          try @Hadded
     559          @plus_zero_zero [2,4,6: >commutative_plus @Hadded |*: skip]]
    629560      (* USE: sigma_compact (from old_sigma) *)
    630561      lapply (pi2 ?? old_sigma (|prefix|) ?)
    631       [1,3,5,7,9,11,13: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
    632       |*:
    633         inversion (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma))
    634         [1,3,5,7,9,11,13: normalize nodelta #_ #ABS cases ABS
    635         |*: inversion (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma))
    636           [1,3,5,7,9,11,13: normalize nodelta #Hl * #pc #j normalize nodelta #Hl2 #ABS cases ABS
    637           |*: normalize nodelta * #Spc #Sj #EQS * #pc #j #EQ
     562      [ >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
     563      | inversion (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma))
     564        [ normalize nodelta #_ #ABS cases ABS
     565        | inversion (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma))
     566          [ normalize nodelta #Hl * #pc #j normalize nodelta #Hl2 #ABS cases ABS
     567          | normalize nodelta * #Spc #Sj #EQS * #pc #j #EQ
    638568            normalize nodelta >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉)
    639569            >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
    640570            >prf >p1 >Hins >nth_append_second try %
    641             <minus_n_n whd in match (nth ????); <(proj2 ?? (pair_destruct ?????? Heq1))
    642             #H >H @plus_left_monotone
     571            <minus_n_n whd in match (nth ????);
     572            cases instr in Hins Hadded; normalize nodelta
     573            [ whd in match jump_expansion_step_instruction; normalize nodelta
     574            #pi lapply (destination_of_None_to_is_jump_false pi)
     575            lapply (destination_of_Some_to_is_jump_true pi)
     576            cases (destination_of ?) normalize nodelta
     577            [ #_ #dest_None | #tgt #dest_Some #_ ]]
     578            try (#x #y #Heq1 #Hadded #X) try (#x #Heq1 #Hadded #X) try (#Heq1 #Hadded #X)
     579            <(proj2 ?? (pair_destruct ?????? Heq1)) >X @plus_left_monotone
    643580            [1,3,4,7: @instruction_size_irrelevant try %
    644581              whd in match is_jump; normalize nodelta >dest_None %
     
    12761213 cases (pair_destruct ?????? Heq2) -Heq2 #Heq2a #Heq2b
    12771214  % [ % [ % [ % [ % [ % [ % [ % [ % ]]]]]]]]
    1278   (* NOTE: to save memory and speed up work, there's cases daemon here. They can be
    1279    * commented out for full proofs, but this needs a lot of memory and time *)
    12801215  [ (* not_jump_default *)
    12811216    @(jump_expansion_step1 … Heq1 Heq2b) try assumption
     
    13011236    try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))
    13021237    @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
    1303   | (* added = 0 → policy_pc_equal *) cases daemon (*
    1304     @(jump_expansion_step6 … Heq1 … Heq2b) try assumption
     1238  | (* added = 0 → policy_pc_equal *)
     1239    @(jump_expansion_step6 (pi1 ?? program) (pi1 ?? labels) (pi1 ?? old_sigma) … Holdeq … Heq1 … Heq2a Heq2b) try assumption
    13051240    try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))
    1306     @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
    1307     *)
     1241    try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
     1242    cases (pi2 … old_sigma) * #_ #X #_ @X
    13081243  | (* out_of_program_none *)
    13091244    @(jump_expansion_step7 … Heq2b)
     
    13141249    | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
    13151250    | @(proj2 ?? (proj1 ?? Hpolicy)) ]
    1316   | (* sigma_safe *) cases daemon (*
    1317     @jump_expansion_step9 try assumption
     1251  | (* sigma_safe *)
     1252    @jump_expansion_step9 (*try assumption
    13181253    @(proj2 ?? Hpolicy) *)
    13191254  ]     
Note: See TracChangeset for help on using the changeset viewer.