Changeset 2102
 Timestamp:
 Jun 20, 2012, 4:51:35 PM (6 years ago)
 Location:
 src/ASM
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/PolicyFront.ma
r2101 r2102 767 767 ] 768 768 qed. 769 770 lemma occurs_does_not: ∀tag,A,id,list_instr. 771 does_not_occur tag A id list_instr = true → 772 occurs_exactly_once tag A id list_instr = true → 773 False. 774 #tag #A #id #list_instr elim list_instr 775 [ #_ whd in match (occurs_exactly_once ????); #ABS destruct (ABS) 776  #h #t #Hind whd in match (does_not_occur ????); 777 whd in match (occurs_exactly_once ????); 778 cases (instruction_matches_identifier ?? id h) normalize nodelta 779 [ #ABS destruct (ABS) 780  @Hind 781 ] 782 ] 783 qed. 784 785 lemma label_in_program: ∀program:(Σl.S (l) < 2^16).∀labels:(Σlm. 786 ∀l.occurs_exactly_once ?? l program → 787 bitvector_of_nat ? (lookup_def ?? lm l 0) = 788 address_of_word_labels_code_mem program l).∀x. 789 occurs_exactly_once ?? x program → 790 lookup_def ASMTag ℕ labels x O≤program. 791 #program cases program program #program #Hprogram #labels #x cases labels 792 labels #labels #H lapply (H x) H 793 generalize in match (lookup_def … labels x 0); 794 whd in match address_of_word_labels_code_mem; 795 whd in match index_of; normalize nodelta elim program in Hprogram; 796 [ #Hprogram #n cases not_implemented 797  #h #t #Hind #Hprogram #n #Hlm #Hocc lapply (Hlm Hocc) Hlm #Hbv 798 whd in match (occurs_exactly_once ????) in Hocc; 799 whd in match (index_of_internal ????) in Hbv; 800 lapply (refl ? (instruction_matches_identifier … x h)) 801 lapply Hocc; lapply Hbv; Hocc Hbv 802 cases (instruction_matches_identifier … x h) in ⊢ (% → % → ???% → %); 803 normalize nodelta #Hbv #Hocc #EQ 804 [ >(bitvector_of_nat_ok 16 n 0) 805 [ @le_O_n 806  >(eq_eq_bv … Hbv) @I 807  / by / 808  cases daemon 809 ] 810  cases n in Hbv; 811 [ #_ @le_O_n 812  n #n #Hbv @le_S_S @(Hind … Hocc) 813 [ @(transitive_lt … Hprogram) @le_n 814  #_ lapply (bitvector_of_nat_ok 16 (S n) (index_of_internal ? (instruction_matches_identifier ?? x) t 1) ???) 815 [ >Hbv >eq_bv_refl @I 816  @(transitive_lt … Hprogram) cases daemon 817  cases daemon 818  #H >(index_of_label_from_internal … Hocc) 819 <plus_O_n >(index_of_label_from_internal … Hocc) in H; 820 #H >(injective_S … H) <plus_O_n @refl 821 ] 822 ] 823 ] 824 ] 825 ] 826 qed. 
src/ASM/PolicyStep.ma
r2101 r2102 116 116 ] 117 117  #Hnj 118 (* USE: jump_not_in_policy(from fold and old_sigma) *)118 (* USE: not_jump_default (from fold and old_sigma) *) 119 119 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind))))))) i Hi Hnj) 120 120 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) i Hi Hnj) … … 127 127 >H2 in H; normalize nodelta H2 x #H @conj 128 128 [ @conj [ @conj [ @conj [ @conj [ @conj 129 [ (* USE[pass]: out_of_program_none, jump_not_in_policy, policy_increase (from fold) *)129 [ (* USE[pass]: out_of_program_none, not_jump_default, policy_increase (from fold) *) 130 130 @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))) 131 131  (* policy_compact_unsafe → policy_compact (in the end) *) … … 165 165 (* USE: added = 0 → policy_pc_equal *) 166 166 >(proj2 ?? (proj1 ?? H) (eqb_true_to_eq … Hch) (lookup_def ?? labels x 0) ?) 167 [2,4,6,8: lapply ((pi2 ?? labels) x)168 whd in match address_of_word_labels_code_mem;169 normalize nodelta cases daemon (* XXX *)]167 [2,4,6,8: @(label_in_program program labels x) 168 cases daemon (* XXX this has to come from somewhere else *) 169 ] 170 170 [1,5: >(eqb_true_to_eq … Hch) <plus_n_O] 171 171 cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false) … … 185 185 (* USE: added = 0 → policy_pc_equal *) 186 186 >(proj2 ?? (proj1 ?? H) (eqb_true_to_eq … Hch) (lookup_def ?? labels x 0) ?) 187 [2,4,6,8: cases daemon (* XXX *)] 187 [2,4,6,8: @(label_in_program program labels x) 188 cases daemon (* XXX this has to come from somewhere else *)] 188 189 [1,3: >(eqb_true_to_eq … Hch) <plus_n_O] 189 190 normalize nodelta cases (vsplit bool 5 11 ?) #addr1 #addr2 … … 199 200 normalize nodelta 200 201 >(proj2 ?? (proj1 ?? H) (eqb_true_to_eq … Hch) (lookup_def ?? labels x 0) ?) 201 [2,4,6,8: cases daemon (* XXX *)] 202 [2,4,6,8: @(label_in_program program labels x) 203 cases daemon (* XXX this has to come from somewhere else *)] 202 204 [1,3: >(eqb_true_to_eq … Hch) <plus_n_O] 203 205 normalize nodelta … … 224 226 normalize nodelta >(add_bitvector_of_nat_plus ? i 1) 225 227 <(plus_n_Sm i 0) <plus_n_O 226 cases daemon (* XXX *)228 cases daemon (* XXX this needs subadressing mode magic, see above *) 227 229 ] 228 230 ] … … 286 288 ] 287 289 ] 288  (* jump_not_in_policy*) #i >append_length <commutative_plus #Hi normalize in Hi;290  (* not_jump_default *) #i >append_length <commutative_plus #Hi normalize in Hi; 289 291 cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 290 292 [ <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss 291 293 [ >lookup_insert_miss 292 294 [ >(nth_append_first ? i prefix ?? Hi) 293 (* USE: jump_not_in_policy*)295 (* USE: not_jump_default *) 294 296 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) i Hi) 295 297  @bitvector_of_nat_abs … … 381 383 whd in match jump_expansion_step_instruction; normalize nodelta #Heqi #Heq1 382 384 #Hj <(proj1 ?? (pair_destruct ?????? Heq1)) 383 (* USE: jump_not_in_policy(from old_sigma) *)385 (* USE: not_jump_default (from old_sigma) *) 384 386 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) (prefix) ??) 385 387 [1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,64,67,70,73,76,79,82: … … 401 403 ] 402 404 2,3,6: #x [3: #y] #Heqi #Heq1 #Hj <(proj1 ?? (pair_destruct ?????? Heq1)) 403 (* USE: jump_not_in_policy(from old_sigma) *)405 (* USE: not_jump_default (from old_sigma) *) 404 406 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) (prefix) ??) 405 407 [1,4,7: >prf >nth_append_second
Note: See TracChangeset
for help on using the changeset viewer.