Changeset 2245 for src


Ignore:
Timestamp:
Jul 24, 2012, 4:50:20 PM (9 years ago)
Author:
sacerdot
Message:

Temporary commit to have a backtracking point. Yes, I know this breaks
PolicyStep? temporarily.

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/PolicyStep.ma

    r2244 r2245  
    453453
    454454lemma jump_expansion_step6:
    455 (*
    456  program :
    457   (Σl:list labelled_instruction.S (|l|)< 2 \sup 16 ∧is_well_labelled_p l)
    458  labels :
     455 ∀program : list labelled_instruction.(*
     456  (Σl:list labelled_instruction.S (|l|)< 2 \sup 16 ∧is_well_labelled_p l)*)
     457 ∀labels : label_map.(*
    459458  (Σlm:label_map
    460459   .(∀l:identifier ASMTag
    … …  
    462461      →bitvector_of_nat 16 (lookup_def ASMTag ℕ lm l O)
    463462       =address_of_word_labels_code_mem program l))*)
    464  ∀old_sigma : ppc_pc_map.(*
    465   (Σpolicy:ppc_pc_map
    466    .not_jump_default program policy
     463 ∀old_sigma :
     464   Σpolicy:ppc_pc_map
     465   .(*not_jump_default program policy
    467466    ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd  policy)
    468467                 〈O,short_jump〉)
    … …  
    471470     =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|program|))
    472471                  (\snd  policy) 〈O,short_jump〉)
    473     ∧sigma_compact_unsafe program labels policy
    474     ∧\fst  policy≤ 2 \sup 16 )*)
    475  ∀prefix : list (option Identifier×pseudo_instruction).(*
    476  x : (option Identifier×pseudo_instruction)
    477  tl : (list (option Identifier×pseudo_instruction))
    478  prf : (program=prefix@[x]@tl)
     472    ∧*)sigma_compact_unsafe program labels policy
     473    (*∧\fst  policy≤ 2 \sup 16*).
     474 ∀prefix : list (option Identifier×pseudo_instruction).
     475 ∀x : option Identifier×pseudo_instruction.
     476 ∀tl : list (option Identifier×pseudo_instruction).
     477 ∀prf : program=prefix@[x]@tl.(*
    479478 acc :
    480479  (Σx0:ℕ×ppc_pc_map
    … …  
    497496                   (\snd  old_sigma) 〈O,short_jump〉)
    498497       +added
    499      ∧sigma_safe prefix labels added old_sigma policy))
    500  inc_added : ℕ
    501  inc_pc_sigma : ppc_pc_map
     498     ∧sigma_safe prefix labels added old_sigma policy))*)
     499 ∀inc_added : ℕ.
     500 ∀inc_pc_sigma : ppc_pc_map.(*
    502501 p : (acc≃〈inc_added,inc_pc_sigma〉)*)
    503502 ∀label : option Identifier.
    504  ∀instr : pseudo_instruction.(*
    505  p1 : (x≃〈label,instr〉)
     503 ∀instr : pseudo_instruction.
     504 ∀p1 : x≃〈label,instr〉.(*
    506505 add_instr ≝
    507506  match instr
    … …  
    520519   Some jump_length
    521520   (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
    522   |Mov (_:[[dptr]])   (_0:Identifier)⇒None jump_length]
    523  inc_pc : ℕ
    524  inc_sigma : (BitVectorTrie (ℕ×jump_length) 16)
    525  Hips : (inc_pc_sigma=〈inc_pc,inc_sigma〉)
    526  old_pc : ℕ
    527  old_length : jump_length
    528  Holdeq :
    529   (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) (\snd  old_sigma)
     521  |Mov (_:[[dptr]])   (_0:Identifier)⇒None jump_length]*)
     522 ∀inc_pc : ℕ.
     523 ∀inc_sigma : BitVectorTrie (ℕ×jump_length) 16.(*
     524 Hips : (inc_pc_sigma=〈inc_pc,inc_sigma〉)*)
     525 ∀old_pc : ℕ.
     526 ∀old_length : jump_length.
     527 ∀Holdeq :
     528  lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) (\snd  old_sigma)
    530529   〈O,short_jump〉
    531    =〈old_pc,old_length〉)
    532  Hpolicy :
     530   =〈old_pc,old_length〉.
     531 ∀Hpolicy1 :(*
    533532  (not_jump_default prefix 〈inc_pc,inc_sigma〉
    534533   ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) inc_sigma
    … …  
    541540   ∧sigma_compact_unsafe prefix labels 〈inc_pc,inc_sigma〉
    542541   ∧(sigma_jump_equal prefix old_sigma 〈inc_pc,inc_sigma〉→inc_added=O)
    543    ∧(inc_added=O→sigma_pc_equal prefix old_sigma 〈inc_pc,inc_sigma〉)
     542   ∧( *)inc_added=O→sigma_pc_equal prefix old_sigma 〈inc_pc,inc_sigma〉.(*)
    544543   ∧out_of_program_none prefix 〈inc_pc,inc_sigma〉
    545544   ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) inc_sigma
    … …  
    547546    =old_pc+inc_added
    548547   ∧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〉).
    549550 ∀added : ℕ.
    550  ∀policy : ppc_pc_map.(*
    551  new_length : jump_length
    552  isize : ℕ
    553  Heq1 :
    554   (match 
    555    match instr
    556     in pseudo_instruction
    557     return λ_:pseudo_instruction.(option jump_length)
    558     with 
    559    [Instruction (i:(preinstruction Identifier))⇒
    560     jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
    561     (|prefix|) i
    562    |Comment (_:String)⇒None jump_length
    563    |Cost (_:costlabel)⇒None jump_length
    564    |Jmp (j:Identifier)⇒
    565     Some jump_length
    566     (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
    567    |Call (c:Identifier)⇒
    568     Some jump_length
    569     (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
    570    |Mov (_:[[dptr]])   (_0:Identifier)⇒None jump_length]
    571     in option
    572     return λ_0:(option jump_length).(jump_length×ℕ)
    573     with 
     551 ∀policy : ppc_pc_map.
     552 ∀new_length : jump_length.
     553 ∀isize : ℕ.
     554 let add_instr ≝ match instr with
     555  [ Jmp  j        ⇒ Some ? (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
     556  | Call c        ⇒ Some ? (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
     557  | Instruction i ⇒ jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added (|prefix|) i
     558  | _             ⇒ None ?
     559  ] in
     560 ∀Heq1 :
     561  match add_instr with 
    574562   [None⇒〈short_jump,instruction_size_jmplen short_jump instr〉
    575563   |Some (pl:jump_length)⇒
    576564    〈max_length old_length pl,
    577565    instruction_size_jmplen (max_length old_length pl) instr〉]
    578    =〈new_length,isize〉)
    579  prefix_ok1 : (S (|prefix|)< 2 \sup 16 )
    580  prefix_ok : (|prefix|< 2 \sup 16 )
    581  Heq2a :
    582   (match 
    583    match instr
    584     in pseudo_instruction
    585     return λ_0:pseudo_instruction.(option jump_length)
    586     with 
    587    [Instruction (i:(preinstruction Identifier))⇒
    588     jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
    589     (|prefix|) i
    590    |Comment (_0:String)⇒None jump_length
    591    |Cost (_0:costlabel)⇒None jump_length
    592    |Jmp (j:Identifier)⇒
    593     Some jump_length
    594     (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
    595    |Call (c:Identifier)⇒
    596     Some jump_length
    597     (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
    598    |Mov (_0:[[dptr]])   (_00:Identifier)⇒None jump_length]
    599     in option
    600     return λ_0:(option jump_length).ℕ
    601     with 
     566   =〈new_length,isize〉.
     567 ∀prefix_ok1 : S (|prefix|)< 2 \sup 16.
     568 ∀prefix_ok : |prefix|< 2 \sup 16.
     569 ∀Heq2a :
     570  match add_instr with
    602571   [None⇒inc_added
    603572   |Some (x0:jump_length)⇒
    604573    inc_added+(isize-instruction_size_jmplen old_length instr)]
    605    =added)
    606  Heq2b :
    607   (〈inc_pc+isize,
     574   =added.
     575 ∀Heq2b :
     576  〈inc_pc+isize,
    608577   insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
    609578   〈inc_pc+isize,
    … …  
    612581   (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
    613582    〈inc_pc,new_length〉 inc_sigma)〉
    614    =policy)
    615 *)
     583   =policy.
    616584 added=O→sigma_pc_equal (prefix@[〈label,instr〉]) old_sigma policy.
    617 cases daemon(*
     585 #program #labels #old_sigma #prefix #x #tl #prf #inc_added #inc_pc_sigma #label
     586 #instr #p1 #inc_pc #inc_sigma #old_pc #old_length #Holdeq #Hpolicy1 #Hpolicy2
     587 #added #policy #new_length #isize #Heq1 #prefix_ok #prefix_ok1 #Heq2a #Heq2b
    618588    (* USE[pass]: added = 0 → policy_pc_equal *)
    619      lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))
    620     <(proj2 ?? (pair_destruct ?????? Heq2))
    621     <(proj1 ?? (pair_destruct ?????? Heq2))
    622     lapply Heq1 -Heq1 lapply (refl ? instr)
    623     cases instr in ⊢ (???% → % → %); normalize nodelta
     589    lapply Hpolicy1 <Heq2b <Heq2a lapply Heq1 -Heq1
     590    inversion instr normalize nodelta
    624591    [2,3,6: #x [3: #y] #Hins #Heq1 #Hold #Hadded #i >append_length >commutative_plus
    625592      #Hi normalize in Hi;
    626593      cases (le_to_or_lt_eq … Hi) -Hi #Hi
    627594      [1,3,5: cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    628         [1,3,5: <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
     595        [1,3,5: <Heq2b >lookup_insert_miss
    629596          [1,3,5: >lookup_insert_miss
    630597            [1,3,5: @(Hold Hadded i (le_S_to_le … Hi))
    631             |2,4,6: @bitvector_of_nat_abs
    632               [3,6,9: @lt_to_not_eq @Hi
    633               |1,4,7: @(transitive_lt ??? Hi)
    634               ]
    635               @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length
    636               @le_S_S <plus_n_Sm @le_S @le_plus_n_r
    637             ]
    638           |2,4,6: @bitvector_of_nat_abs
    639             [3,6,9: @lt_to_not_eq @le_S @Hi
    640             |1,4,7: @(transitive_lt … Hi) @le_S_to_le
    641             ]
    642             @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length
    643               @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
    644           ]
    645         |2,4,6: >Hi >lookup_insert_miss
     598            |*: @bitvector_of_nat_abs try assumption
     599              [2,4,6: @lt_to_not_eq @Hi
     600              |*: @(transitive_lt ??? Hi) assumption ]]
     601          |*: @bitvector_of_nat_abs try assumption
     602            [2,4,6: @lt_to_not_eq @le_S @Hi
     603            |*: @(transitive_lt … Hi) assumption ]]
     604        |*: >Hi >lookup_insert_miss
    646605          [1,3,5: >lookup_insert_hit >(Hold Hadded (|prefix|) (le_n (|prefix|)))
    647606            @sym_eq (* USE: fst p = lookup |prefix| *)
    648             @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
    649           |2,4,6: @bitvector_of_nat_abs
    650             [3,6,9: @lt_to_not_eq @le_n
    651             |1,4,7: @le_S_to_le
    652             ]
    653             @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length
    654               @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
    655           ]
    656         ]
     607            @Hpolicy2
     608          |*: @bitvector_of_nat_abs try assumption
     609              @lt_to_not_eq %]]
    657610      |2,4,6: >Hi >lookup_insert_hit
    658611        (* USE fst p = lookup |prefix| *)
    659         >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
     612        >Hpolicy2
    660613        <(Hold Hadded (|prefix|) (le_n (|prefix|)))
    661614        (* USE: sigma_compact (from old_sigma) *)
    662         lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?)
     615        lapply (pi2 ?? old_sigma (|prefix|) ?)
    663616        [1,3,5: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
    664         |2,4,6:
    665           lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)))
    666           cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% -> %);
     617        |*:
     618          inversion (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma))
    667619          [1,3,5: normalize nodelta #_ #ABS cases ABS
    668           |2,4,6: lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)))
    669             cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %);
    670             [1,3,5: normalize nodelta #Hl #x cases x -x #pc #j normalize nodelta #Hl2 #ABS cases ABS
    671             |2,4,6: normalize nodelta #x cases x -x #Spc #Sj #EQS #x cases x -x #pc #j #EQ
     620          |*: inversion (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma))
     621            [1,3,5: normalize nodelta #Hl * #pc #j normalize nodelta #Hl2 #ABS cases ABS
     622            |*: normalize nodelta * #Spc #Sj #EQS * #pc #j #EQ
    672623              normalize nodelta >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉)
    673624              >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
    674               >prf >p1 >Hins >nth_append_second
    675               [2,4,6: @(le_n (|prefix|))
    676               |1,3,5: <minus_n_n whd in match (nth ????); <(proj2 ?? (pair_destruct ?????? Heq1))
    677                  #H >H @plus_left_monotone @instruction_size_irrelevant @nmk / by /
    678               ]
    679             ]
    680           ]
    681         ]
    682       ]
     625              >prf >p1 >Hins >nth_append_second try %
     626              <minus_n_n whd in match (nth ????); <(proj2 ?? (pair_destruct ?????? Heq1))
     627                 #H >H @plus_left_monotone @instruction_size_irrelevant % ]]]]
    683628    |4,5: #x #Hins #Heq1 #Hold #Hadded #i >append_length >commutative_plus
    684629       #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi #Hi
    … …  
    692637               |1,4: @(transitive_lt ??? Hi)
    693638               ]
    694                @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf
    695                >append_length @le_plus_n_r
     639               assumption
    696640             ]
    697641           |2,4: @bitvector_of_nat_abs
    698642             [3,6: @lt_to_not_eq @le_S @Hi
    699              |1,4: @(transitive_lt ??? Hi) @le_S_to_le
    700              ]
    701              @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf
    702              >append_length <plus_n_Sm @le_S_S @le_plus_n_r
    703            ]
     643             |1,4: @(transitive_lt ??? Hi) assumption]
     644             assumption ]
    704645         |2,4: >Hi >lookup_insert_miss
    705646           [1,3: >lookup_insert_hit >(Hold ? (|prefix|) (le_n (|prefix|)))
    706647             [2,4: >commutative_plus in Hadded; @plus_zero_zero] @sym_eq
    707648             (* USE: fst p = lookup |prefix| *)
    708              @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
    709            |2,4: @bitvector_of_nat_abs
    710              [3,6: @lt_to_not_eq @le_n
    711              |1,4: @(transitive_lt ??? (le_S_S … (le_n (|prefix|))))
    712              ]
    713              @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf
    714              >append_length <plus_n_Sm @le_S_S @le_plus_n_r
    715            ]
    716          ]
     649             @Hpolicy2
     650           |2,4: @bitvector_of_nat_abs try assumption
     651             @lt_to_not_eq @le_n]]
    717652       |2,4: >Hi >lookup_insert_hit <(proj2 ?? (pair_destruct ?????? Heq1))
    718653         elim (le_to_or_lt_eq … (minus_zero_to_le … (plus_zero_zero … Hadded)))
    719654         [1,3: #H @⊥ @(absurd ? H) @le_to_not_lt <(proj2 ?? (pair_destruct ?????? Heq1))
    720            @jump_length_le_max / by I/
    721          |2,4: #H (* USE: fst p = lookup |prefix| *)
    722            >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
     655           @jump_length_le_max %
     656         |*: #H (* USE: fst p = lookup |prefix| *)
     657           >Hpolicy2
    723658           <(Hold ? (|prefix|) (le_n (|prefix|)))
    724659           [1,3: <(proj2 ?? (pair_destruct ?????? Heq1)) in H; #H
    725              >(jump_length_equal_max … H)
    726              [1,3: (* USE: sigma_compact_unsafe (from old_sigma) *)
    727                lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?)
    728                [1,3: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
    729                |2,4: lapply Holdeq lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)))
    730                  cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% → %);
    731                  [1,3: normalize nodelta #_ #_ #ABS cases ABS
    732                  |2,4: normalize nodelta
    733                    lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)))
    734                    cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %);
    735                    [1,3: #_ #x cases x -x #pc #j normalize nodelta #_ #_ #ABS cases ABS
    736                    |2,4: #x cases x -x #Spc #Sj #EQS #x cases x -x #pc #j #EQ
    737                      normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
    738                      >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) #EQpair
    739                      >(proj2 ?? (pair_destruct ?????? EQpair)) >prf >nth_append_second
    740                      [1,3: <minus_n_n >p1 whd in match (nth ????); >Hins #H @H
    741                      |2,4: @le_n
    742                      ]
    743                    ]
    744                  ]
    745                ]
    746              |2,4: / by I/
    747              ]
    748            |2,4: @plus_zero_zero [2,4: >commutative_plus @Hadded]
    749            ]
    750          ]
    751        ]
     660             >(jump_length_equal_max … H) try %
     661             (* USE: sigma_compact_unsafe (from old_sigma) *)
     662             lapply (pi2 ?? old_sigma (|prefix|) ?)
     663             [1,3: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
     664             |2,4: inversion (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma))
     665               [1,3: normalize nodelta #_ #ABS cases ABS
     666               |2,4: normalize nodelta
     667                 inversion (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma))
     668                 [1,3: #_ * #pc #j normalize nodelta #_ #ABS cases ABS
     669                 |2,4: * #Spc #Sj #EQS #x cases x -x #pc #j #EQ
     670                   normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
     671                   >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) #EQpair
     672                   >EQpair @eq_f >prf >nth_append_second try %
     673                   <minus_n_n >p1 whd in match (nth ????); >Hins
     674                   >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) in Holdeq; #EQ'
     675                   >(proj2 … (pair_destruct … EQ')) % ]]]
     676           |2,4: @plus_zero_zero [2,4: >commutative_plus @Hadded |*: skip]]]]
    752677     |1: #pi cases pi normalize nodelta
    753678      [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
    … …  
    914839        ]
    915840      ]
    916     ]*)
     841    ]
    917842qed.
    918843
    … …  
    15281453  | @not_lt_to_le @ltb_false_to_not_lt @p1
    15291454  ]
    1530 |4: lapply (pi2 ?? acc) >p lapply (refl ? (inc_pc_sigma)) cases inc_pc_sigma in ⊢ (???% → %);
    1531   #inc_pc #inc_sigma #Hips
     1455|4: lapply (pi2 ?? acc) >p -acc inversion inc_pc_sigma
     1456  #inc_pc #inc_sigma #Hips normalize nodelta
    15321457  inversion (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉)
    15331458  #old_pc #old_length #Holdeq #Hpolicy normalize nodelta in Hpolicy; @pair_elim
Note: See TracChangeset for help on using the changeset viewer.