Changeset 1404
 Timestamp:
 Oct 18, 2011, 3:39:56 PM (10 years ago)
 Location:
 src/ASM
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Arithmetic.ma
r1207 r1404 141 141 λn,v. nat_of_bitvector_aux n O v. 142 142 143 axiom bitvector_of_nat_ok: 144 ∀n,x,y.bitvector_of_nat (S n) x = bitvector_of_nat (S n) y → x = y. 145 (* if anyone wants to prove this... *) 146 143 147 definition two_complement_negation ≝ 144 148 λn: nat. 
src/ASM/Assembly.ma
r1393 r1404 797 797  _ ⇒ False 798 798 ]. 799 800 axiom bitvector_of_nat_ok: 801 ∀x,y,n.bitvector_of_nat (S n) x = bitvector_of_nat (S n) y → x = y. 802 799 800 definition jump_in_policy ≝ 801 λprefix:list labelled_instruction.λpolicy:jump_expansion_policy. 802 ∀i:ℕ.i < prefix → is_jump (nth i ? prefix 〈None ?, Comment []〉) → 803 ∃p,j.lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈p,j〉. 804 803 805 let rec jump_expansion_step (program: list labelled_instruction) 804 (old_policy: jump_expansion_policy): 805 (Σpolicy.∀i:ℕ.i < program → 806 is_jump (nth i ? program 〈None ?, Comment [ ]〉) → 807 ∃p,j.lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈p,j〉 808 ) ≝ 806 (old_policy: Σpolicy.jump_in_policy program policy): 807 (Σpolicy. 808 jump_in_policy program policy ∧ 809 (jump_in_policy program policy → True)) ≝ 809 810 let labels ≝ create_label_trie program old_policy in 810 811 let 〈final_pc, final_policy〉 ≝ 811 812 foldl_strong (option Identifier × pseudo_instruction) 812 (λprefix.ℕ × Σpolicy. ∀i:ℕ.i < prefix →813 is_jump (nth i ? prefix 〈None ?, Comment [ ]〉) →814 ∃p,j.lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈p,j〉813 (λprefix.ℕ × Σpolicy. 814 jump_in_policy prefix policy ∧ 815 (jump_in_policy prefix policy → True) 815 816 ) 816 817 program … … 838 839 ) 〈0, Stub ? ?〉 in 839 840 final_policy. 840 [ #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) Hi; 841 [ #Hi; >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) #Hj 842 lapply (sig2 … policy) #Hacc elim (Hacc i (le_S_S_to_le … Hi) Hj) #henk #ingrid elim ingrid 843 ingrid #ingrid #Hingrid 844 % [ @henk  % [ @ingrid  normalize nodelta cases instr normalize nodelta 845 [2,3: #x cases (lookup ??? policy ?) #y #z @Hingrid 846 6: #x #y cases (lookup ??? policy ?) #w #z @Hingrid 847 1: #pi cases (lookup ??? policy ?) #x #y cases (jump_expansion_step_instruction ???) 848 [ @Hingrid 849  #z normalize nodelta <Hingrid @lookup_opt_insert_miss 850 @notb_elim >eq_bv_false [ //  @nmk #H @(absurd (i = (prefix))) 851 [ @(bitvector_of_nat_ok … H) 852  @(lt_to_not_eq i (prefix)) @(le_S_S_to_le … Hi) 853 ] ] 841 [ @conj 842 [ #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) Hi; 843 [ #Hi; >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) #Hj 844 lapply (sig2 … policy) #Hacc elim ((proj1 … Hacc) i (le_S_S_to_le … Hi) Hj) #h #n elim n 845 n #n #Hn 846 % [ @h  % [ @n  normalize nodelta cases instr normalize nodelta 847 [2,3: #x cases (lookup ??? policy ?) #y #z @Hn 848 6: #x #y cases (lookup ??? policy ?) #w #z @Hn 849 1: #pi cases (lookup ??? policy ?) #x #y cases (jump_expansion_step_instruction ???) 850 [ @Hn 851  #z normalize nodelta <Hn @lookup_opt_insert_miss 852 @notb_elim >eq_bv_false [ //  @nmk #H @(absurd (i = (prefix))) 853 [ @(bitvector_of_nat_ok … H) 854  @(lt_to_not_eq i (prefix)) @(le_S_S_to_le … Hi) 855 ] ] 856 ] 857 4,5: #id cases (lookup ??? policy ?) #x #y normalize nodelta <Hn 858 @lookup_opt_insert_miss @notb_elim >eq_bv_false 859 [1,3: // 860 2,4: @nmk #H @(absurd (i = (prefix))) 861 [1,3: @(bitvector_of_nat_ok … H) 862 2,4: @(lt_to_not_eq i (prefix)) @(le_S_S_to_le … Hi) 863 ] ] 864 ] ] ] 865  #Hi >nth_append_second >(injective_S … Hi) 866 [ <minus_n_n #Hj normalize in Hj; normalize nodelta cases instr in Hj; 867 [2,3: #x #Hj @⊥ @Hj 868 6: #x #y #Hj @⊥ @Hj 869 1: #pi cases pi 870 [35,36,37: #Hj @⊥ @Hj 871 4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #Hj @⊥ @Hj 872 1,2,3,6,7,33,34: #x #y #Hj @⊥ @Hj 873 9,10,14,15: #j normalize nodelta #_ 874 % [1,3,5,7: @pc 875 2,4,6,8: lapply (refl ? (lookup … (bitvector_of_nat ? (prefix)) policy 〈pc,short_jump〉)) 876 cases (lookup … (bitvector_of_nat ? (prefix)) policy 〈pc,short_jump〉) in ⊢ (???% → %) 877 #x #y #Hl normalize nodelta 878 % [1,3,5,7: @(max_length y (select_reljump_length (create_label_trie program old_policy) pc j)) 879 2,4,6,8: @lookup_opt_insert_hit 880 ] ] 881 11,12,13,16,17: #x #j normalize nodelta #_ 882 % [1,3,5,7,9: @pc 883 2,4,6,8,10: lapply (refl ? (lookup … (bitvector_of_nat ? (prefix)) policy 〈pc,short_jump〉)) 884 cases (lookup … (bitvector_of_nat ? (prefix)) policy 〈pc,short_jump〉) in ⊢ (???% → %) 885 #x #y #Hl normalize nodelta 886 % [1,3,5,7,9: @(max_length y (select_reljump_length (create_label_trie program old_policy) pc j)) 887 2,4,6,8,10: @lookup_opt_insert_hit 888 ] ] 889 ] 890 4,5: #j normalize nodelta #_ 891 % [1,3: @pc 892 2,4: cases (lookup … (bitvector_of_nat ? (prefix)) policy 〈pc,short_jump〉) 893 #x #y normalize nodelta 894 % [1: @(max_length y (select_jump_length (create_label_trie program old_policy) pc j)) 895 3: @(max_length y (select_call_length (create_label_trie program old_policy) pc j)) 896 2,4: @lookup_opt_insert_hit 897 ] 898 ] 899 ] 900  @le_n 854 901 ] 855 4,5: #id cases (lookup ??? policy ?) #x #y normalize nodelta <Hingrid856 @lookup_opt_insert_miss @notb_elim >eq_bv_false857 [1,3: //858 2,4: @nmk #H @(absurd (i = (prefix)))859 [1,3: @(bitvector_of_nat_ok … H)860 2,4: @(lt_to_not_eq i (prefix)) @(le_S_S_to_le … Hi)861 ] ]862 ] ] ]863  #Hi >nth_append_second >(injective_S … Hi)864 [ <minus_n_n #Hj normalize in Hj; normalize nodelta cases instr in Hj;865 [2,3: #x #Hj @⊥ @Hj866 6: #x #y #Hj @⊥ @Hj867 1: #pi cases pi868 [35,36,37: #Hj @⊥ @Hj869 4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #Hj @⊥ @Hj870 1,2,3,6,7,33,34: #x #y #Hj @⊥ @Hj871 9,10,14,15: #j normalize nodelta #_872 % [1,3,5,7: @pc873 2,4,6,8: lapply (refl ? (lookup … (bitvector_of_nat ? (prefix)) policy 〈pc,short_jump〉))874 cases (lookup … (bitvector_of_nat ? (prefix)) policy 〈pc,short_jump〉) in ⊢ (???% → %)875 #x #y #Hl normalize nodelta876 % [1,3,5,7: @(max_length y (select_reljump_length (create_label_trie program old_policy) pc j))877 2,4,6,8: @lookup_opt_insert_hit878 ] ]879 11,12,13,16,17: #x #j normalize nodelta #_880 % [1,3,5,7,9: @pc881 2,4,6,8,10: lapply (refl ? (lookup … (bitvector_of_nat ? (prefix)) policy 〈pc,short_jump〉))882 cases (lookup … (bitvector_of_nat ? (prefix)) policy 〈pc,short_jump〉) in ⊢ (???% → %)883 #x #y #Hl normalize nodelta884 % [1,3,5,7,9: @(max_length y (select_reljump_length (create_label_trie program old_policy) pc j))885 2,4,6,8,10: @lookup_opt_insert_hit886 ] ]887 ]888 4,5: #j normalize nodelta #_889 % [1,3: @pc890 2,4: cases (lookup … (bitvector_of_nat ? (prefix)) policy 〈pc,short_jump〉)891 #x #y normalize nodelta892 % [1: @(max_length y (select_jump_length (create_label_trie program old_policy) pc j))893 3: @(max_length y (select_call_length (create_label_trie program old_policy) pc j))894 2,4: @lookup_opt_insert_hit895 ]896 ]897 ]898  @le_n899 902 ] 903  // 900 904 ] 901  #i #Hi @⊥ @(absurd (i<0)) [ @Hi  @(not_le_Sn_O) ] 905  @conj 906 [ #i #Hi @⊥ @(absurd (i<0)) [ @Hi  @(not_le_Sn_O) ] 907  // 908 ] 902 909 ] 903 910 qed.
Note: See TracChangeset
for help on using the changeset viewer.