Ignore:
Timestamp:
Jul 20, 2012, 6:15:40 PM (8 years ago)
Author:
sacerdot
Message:

Minor and major improvements everywhere, shortened proofs.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/PolicyFront.ma

    r2222 r2225  
    2222  λx:preinstruction Identifier.
    2323  match x with
    24   [ JC _ ⇒ True
    25   | JNC _ ⇒ True
    26   | JZ _ ⇒ True
    27   | JNZ _ ⇒ True
    28   | JB _ _ ⇒ True
    29   | JNB _ _ ⇒ True
    30   | JBC _ _ ⇒ True
    31   | CJNE _ _ ⇒ True
    32   | DJNZ _ _ ⇒ True
    33   | _ ⇒ False
     24  [ JC _ ⇒ true
     25  | JNC _ ⇒ true
     26  | JZ _ ⇒ true
     27  | JNZ _ ⇒ true
     28  | JB _ _ ⇒ true
     29  | JNB _ _ ⇒ true
     30  | JBC _ _ ⇒ true
     31  | CJNE _ _ ⇒ true
     32  | DJNZ _ _ ⇒ true
     33  | _ ⇒ false
    3434  ].
    3535
     
    3838  match instr with
    3939  [ Instruction i ⇒ is_jump' i
    40   | _             ⇒ False
     40  | _             ⇒ false
    4141  ].
    4242   
     
    4545  match instr with
    4646  [ Instruction i   ⇒ is_jump' i
    47   | Call _ ⇒ True
    48   | Jmp _ ⇒ True
    49   | _ ⇒ False
     47  | Call _ ⇒ true
     48  | Jmp _ ⇒ true
     49  | _ ⇒ false
    5050  ].
    5151
     
    5353  λinstr:pseudo_instruction.
    5454  match instr with
    55   [ Call _ ⇒ True
    56   | _ ⇒ False
     55  [ Call _ ⇒ true
     56  | _ ⇒ false
    5757  ].
    5858 
     
    258258   match j with
    259259   [ short_jump ⇒ \fst (short_jump_cond pc_plus_jmp_length addr) = true ∧
    260       ¬is_call instr
     260       bool_to_Prop (¬is_call instr)
    261261   | absolute_jump ⇒  \fst (absolute_jump_cond pc_plus_jmp_length addr) = true ∧
    262262       \fst (short_jump_cond pc_plus_jmp_length addr) = false ∧
    263        ¬is_relative_jump instr
     263       bool_to_Prop (¬is_relative_jump instr)
    264264   | long_jump   ⇒ \fst (short_jump_cond pc_plus_jmp_length addr) = false ∧
    265265       \fst (absolute_jump_cond pc_plus_jmp_length addr) = false
     
    360360  then short_jump
    361361  else select_call_length labels old_sigma inc_sigma added ppc lbl.
    362  
     362
     363definition destination_of: preinstruction Identifier → option Identifier ≝
     364  λi.
     365  match i with
     366  [ JC j     ⇒ Some ? j
     367  | JNC j    ⇒ Some ? j
     368  | JZ j     ⇒ Some ? j
     369  | JNZ j    ⇒ Some ? j
     370  | JB _ j   ⇒ Some ? j
     371  | JBC _ j  ⇒ Some ? j
     372  | JNB _ j  ⇒ Some ? j
     373  | CJNE _ j ⇒ Some ? j
     374  | DJNZ _ j ⇒ Some ? j
     375  | _        ⇒ None ?
     376  ].
     377
    363378definition jump_expansion_step_instruction: label_map → ppc_pc_map → ppc_pc_map →
    364379  ℕ → ℕ → preinstruction Identifier → option jump_length ≝
    365380  λlabels.λold_sigma.λinc_sigma.λadded.λppc.λi.
    366   match i with
    367   [ JC j     ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)
    368   | JNC j    ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)
    369   | JZ j     ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)
    370   | JNZ j    ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)
    371   | JB _ j   ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)
    372   | JBC _ j  ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)
    373   | JNB _ j  ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)
    374   | CJNE _ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)
    375   | DJNZ _ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)
    376   | _        ⇒ None ?
    377   ].
    378 
    379 lemma dec_is_jump: ∀x.Sum (is_jump x) (¬is_jump x).
    380 #i cases i
    381 [#id cases id
    382  [1,2,3,6,7,33,34:
    383   #x #y %2 whd in match (is_jump ?); /2 by nmk/
    384  |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32:
    385   #x %2 whd in match (is_jump ?); /2 by nmk/
    386  |35,36,37: %2 whd in match (is_jump ?); /2 by nmk/
    387  |9,10,14,15: #x %1 / by I/
    388  |11,12,13,16,17: #x #y %1 / by I/
    389  ]
    390 |2,3: #x %2 /2 by nmk/
    391 |4,5: #x %1 / by I/
    392 |6: #x #y %2 /2 by nmk/
    393 ]
    394 qed.
     381  match destination_of i with
     382  [ Some j     ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)
     383  | None       ⇒ None ?
     384  ].
    395385
    396386(* The first step of the jump expansion: everything to short. *)
     
    599589 #a #b #i cases i
    600590 [1: #pi cases pi
    601    [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:
    602      try (#x #y #H #_) try (#x #H #_) try (#H #_) cases H
    603    |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] #_ try (#_ %)
    604      try (#abs normalize in abs; destruct (abs) @I)
    605      cases a; cases b; try (#_ %) try (#abs normalize in abs; destruct(abs) @I)
    606      try (@(subaddressing_mode_elim … x) #w #abs normalize in abs; destruct (abs) @I)
    607      cases x * #a1 #a2 @(subaddressing_mode_elim … a2) #w
    608      try ( #abs normalize in abs; destruct (abs) @I)
    609      @(subaddressing_mode_elim … a1) #w2 #abs normalize in abs; destruct (abs)
    610    ]
     591   try (#x #y #H #EQ) try (#x #H #EQ) try (#H #EQ) cases H
     592   cases a in EQ; cases b #EQ try %
     593   try (normalize in EQ; destruct(EQ) @False)
     594   try (lapply EQ @(subaddressing_mode_elim … x) #w #EQ normalize in EQ; destruct(EQ) @False)
     595   lapply EQ -EQ cases x * #a1 #a2 @(subaddressing_mode_elim … a2) #w
     596   try (#EQ normalize in EQ; destruct(EQ) @False)
     597   @(subaddressing_mode_elim … a1) #w
     598   #EQ normalize in EQ; destruct(EQ)
    611599  |2,3,6: #x [3: #y] #H cases H
    612   |4,5: #id #_ cases a cases b
    613     [2,3,4,6,11,12,13,15: normalize #H destruct (H)
    614     |1,5,7,8,9,10,14,16,17,18: #H / by refl/
    615     ]
    616   ]
     600  |4,5: #id #_ cases a cases b #H try % normalize in H; destruct(H)
     601 ]
    617602qed.
    618603
     
    623608 |4,5: #id #_ cases a cases b / by le_n/
    624609 |1: #pi cases pi
    625    [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:
    626      try (#x #y #H) try (#x #H) try (#H) cases H
    627    |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y]
    628      #_ cases a cases b
    629      [1,4,5,6,7,8,9: / by le_n/
    630      |10,13,14,15,16,17,18: / by le_n/
    631      |19,22,23,24,25,26,27: / by le_n/
    632      |28,31,32,33,34,35,36: / by le_n/
    633      |37,40,41,42,43,44,45: / by le_n/
    634      |46,47,48,49,50,51,52,53,54: / by le_n/
    635      |55,56,57,58,59,60,61,62,63: / by le_n/
    636      |64,65,66,67,68,69,70,71,72: / by le_n/
    637      |73,74,75,76,77,78,79,80,81: / by le_n/
    638      ]
    639      try (@(subaddressing_mode_elim … x) #w normalize @le_S @le_S @le_S @le_S @le_S @le_n)
    640      cases x * #ad   
    641      try (@(subaddressing_mode_elim … ad) #w #z normalize @le_S @le_S @le_S @le_S @le_S @le_n)
    642      #z @(subaddressing_mode_elim … z) #w normalize / by /
    643    ]
     610    try (#x #y #H) try (#x #H) try (#H) cases H
     611    -H cases a cases b @leb_true_to_le try %
     612    try (@(subaddressing_mode_elim … x) #w % @False)
     613    cases x * #a1 #a2 @(subaddressing_mode_elim … a2) #w try %
     614    @(subaddressing_mode_elim … a1) #w %
    644615 ]
    645616qed.
     
    701672              cases (vsplit bool 9 7 result) #upper #lower normalize nodelta
    702673              cases (get_index' bool 2 0 flags) normalize nodelta
    703               [3,4: #H @⊥ @(absurd ?? (proj2 ?? H)) / by I/
     674              [3,4: #H cases (proj2 ?? H)
    704675              |1,2: cases (eq_bv 9 upper ?)
    705676                [2,4: #H lapply (proj1 ?? H) #H3 destruct (H3)
     
    761732              ]
    762733            ]
    763           |1: #pi cases pi
    764             [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:
    765               [1,2,3,6,7,24,25: #x #y
    766               |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
    767               normalize nodelta #H #Heq @refl
    768             |9,10,11,12,13,14,15,16,17: [1,2,6,7: #x |3,4,5,8,9: #y #x]
    769               normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
    770               #Hj #Heq lapply (Hj x (refl ? x)) -Hj
     734          |1: cut (∀A,B,ab.fst A B ab = (let 〈a,b〉 ≝ ab in a))
     735              [#A #B * / by refl/] #fst_foo
     736              cut (∀x.
     737                    instruction_has_label x (\snd  (nth i labelled_instruction program 〈None (identifier ASMTag),Comment []〉)) →
     738               lookup_def ?? (create_label_map program) x 0 ≤ (|program|))
     739              [#x #Heq cases (create_label_map program) #clm #Hclm
     740               @le_S_to_le @(proj2 ?? (Hclm x ?))
     741               @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (\snd (nth i ? program 〈None ?, Comment []〉)) ??)
     742               [ >nat_of_bitvector_bitvector_of_nat_inverse
     743                 [2: @(transitive_lt … (proj1 ?? Hprogram)) @le_S] @Hi
     744               | whd in match fetch_pseudo_instruction; normalize nodelta
     745                 >nth_safe_nth
     746                 [ >nat_of_bitvector_bitvector_of_nat_inverse
     747                   [ @pair_elim // ]
     748                   @(transitive_lt … (proj1 ?? Hprogram)) @le_S @Hi ]
     749                 | assumption ]] #lookup_in_program
     750              -H #pi cases pi
     751              try (#y #x #H #Heq) try (#x #H #Heq) try (#H #Heq) try %
     752              normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) in H;
     753              #Hj lapply (Hj x (refl ? x)) -Hj
    771754              whd in match expand_relative_jump; normalize nodelta
    772755              whd in match expand_relative_jump_internal; normalize nodelta
     
    776759              <(plus_n_Sm i 0) <plus_n_O <plus_n_O cases x2 normalize nodelta
    777760              [1,4,7,10,13,16,19,22,25:
    778                 cut (∀A,B,ab.fst A B ab = (let 〈a,b〉 ≝ ab in a))
    779                 [1,3,5,7,9,11,13,15,17: #A #B * / by refl/ ]
    780                 #fst_foo >fst_foo @pair_elim #sj_possible #disp #H #H2
     761                >fst_foo @pair_elim #sj_possible #disp #H #H2
    781762                @(pair_replace ?????????? (eq_to_jmeq … H))
    782                 [1,3,5,7,9,11,13,15,17:
    783                   cut (lookup_def ?? (create_label_map program) x 0 ≤ (|program|))
    784                   [1,3,5,7,9,11,13,15,17: cases (create_label_map program) #clm #Hclm
    785                     @le_S_to_le @(proj2 ?? (Hclm x ?))
    786                     @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (\snd (nth i ? program 〈None ?, Comment []〉)) ??)
    787                     [1,4,7,10,13,16,19,22,25: >nat_of_bitvector_bitvector_of_nat_inverse
    788                       [2,4,6,8,10,12,14,16,18: @(transitive_lt … (proj1 ?? Hprogram)) @le_S] @Hi
    789                     |2,5,8,11,14,17,20,23,26: whd in match fetch_pseudo_instruction; normalize nodelta
    790                       >nth_safe_nth
    791                       [1,3,5,7,9,11,13,15,17: >nat_of_bitvector_bitvector_of_nat_inverse
    792                         [1,3,5,7,9,11,13,15,17: >Heq %]
    793                         @(transitive_lt … (proj1 ?? Hprogram)) @le_S @Hi
    794                       ]
    795                     ]
    796                     >Heq / by /
    797                   ]
    798                   #X >(le_to_leb_true … X) @refl
    799                 ]
     763                [1,3,5,7,9,11,13,15,17: >(le_to_leb_true … (lookup_in_program …))
     764                  try % >Heq % ]
    800765                >(proj1 ?? H2) try (@refl) normalize nodelta
    801766                [1,2,3,5: @(subaddressing_mode_elim … y) #w %
     
    803768                  @(subaddressing_mode_elim … sth2) #x [3,4: #x2] %
    804769                ]
    805               |2,5,8,11,14,17,20,23,26: ** #_ #_ #abs cases abs #abs2 @⊥ @abs2 / by I/
     770              |2,5,8,11,14,17,20,23,26: ** #_ #_ #abs cases abs
    806771              ]
    807               cut (∀A,B,ab.fst A B ab = (let 〈a,b〉 ≝ ab in a))
    808               [1,3,5,7,9,11,13,15,17: #A #B * / by refl/ ]
    809               #fst_foo * #H #_ >fst_foo in H; @pair_elim #sj_possible #disp #H
     772              * #H #_ >fst_foo in H; @pair_elim #sj_possible #disp #H
    810773              @(pair_replace ?????????? (eq_to_jmeq … H))
    811                 [1,3,5,7,9,11,13,15,17:
    812                   cut (lookup_def ?? (create_label_map program) x 0 ≤ (|program|))
    813                   [1,3,5,7,9,11,13,15,17: cases (create_label_map program) #clm #Hclm
    814                     @le_S_to_le @(proj2 ?? (Hclm x ?))
    815                     @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (\snd (nth i ? program 〈None ?, Comment []〉)) ??)
    816                     [1,4,7,10,13,16,19,22,25: >nat_of_bitvector_bitvector_of_nat_inverse
    817                       [2,4,6,8,10,12,14,16,18: @(transitive_lt … (proj1 ?? Hprogram)) @le_S] @Hi
    818                     |2,5,8,11,14,17,20,23,26: whd in match fetch_pseudo_instruction; normalize nodelta
    819                       >nth_safe_nth
    820                       [1,3,5,7,9,11,13,15,17: >nat_of_bitvector_bitvector_of_nat_inverse
    821                         [1,3,5,7,9,11,13,15,17: >Heq %]
    822                         @(transitive_lt … (proj1 ?? Hprogram)) @le_S @Hi
    823                       ]
    824                     ]
    825                     >Heq / by /
    826                   ]
    827                   #X >(le_to_leb_true … X) @refl
    828                 ]
     774                [1,3,5,7,9,11,13,15,17: >(le_to_leb_true … (lookup_in_program …))
     775                  try % >Heq % ]
    829776                #H2 >H2 try (@refl) normalize nodelta
    830777                [1,2,3,5: @(subaddressing_mode_elim … y) #w %
     
    832779                  [1,2: %] whd in match (map ????); whd in match (flatten ??);
    833780                  whd in match (map ????) in ⊢ (???%); whd in match (flatten ??) in ⊢ (???%);
    834                   >length_append >length_append @eq_f2 %
    835                 ]
    836               ]
    837             ]
    838           ]
    839         ]
    840       ]
     781                  >length_append >length_append %]]]]]
    841782qed.
    842783
     
    845786 #i cases i
    846787 [2,3,6: #x [3: #y] #Hj #j1 #j2 %
    847  |4,5: #x #Hi cases Hi #abs @⊥ @abs @I
    848  |1: #pi cases pi
    849    [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:
    850      [1,2,3,6,7,24,25: #x #y
    851      |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
    852      #Hj #j1 #j2 %
    853    |9,10,11,12,13,14,15,16,17: [1,2,6,7: #x |3,4,5,8,9: #y #x]
    854      #Hi cases Hi #abs @⊥ @abs @I
    855    ]
    856  ]
    857 qed.
     788 |4,5: #x #Hi cases Hi
     789 |1: #pi cases pi try (#x #y #Hj #j1 #j2) try (#y #Hj #j1 #j2) try (#Hj #j1 #j2)
     790     try % cases Hj ]
     791qed.
Note: See TracChangeset for help on using the changeset viewer.