Changeset 2213


Ignore:
Timestamp:
Jul 18, 2012, 5:57:26 PM (5 years ago)
Author:
boender
Message:
  • removed one cases daemon
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/PolicyFront.ma

    r2211 r2213  
    644644qed.
    645645
    646 lemma label_in_program: ∀program:(Σl.S (|l|) < 2^16 ∧ is_well_labelled_p l).∀labels:(Σlm.
    647    ∀l.occurs_exactly_once ?? l program →
    648     bitvector_of_nat ? (lookup_def ?? lm l 0) =
    649      address_of_word_labels_code_mem program l).∀x.
    650  occurs_exactly_once ?? x program →   
    651  lookup_def ASMTag ℕ labels x O≤|program|.
    652 #program cases program -program #program #Hprogram #labels #x cases labels
    653 -labels #labels #H lapply (H x) -H
    654 generalize in match (lookup_def … labels x 0);
    655 whd in match address_of_word_labels_code_mem;
    656 whd in match index_of; normalize nodelta elim program in Hprogram;
    657 [ #Hprogram #n cases not_implemented
    658 | #h #t #Hind #Hprogram #n #Hlm #Hocc lapply (Hlm Hocc) -Hlm #Hbv
    659   whd in match (occurs_exactly_once ????) in Hocc;
    660   whd in match (index_of_internal ????) in Hbv;
    661   lapply (refl ? (instruction_matches_identifier … x h))
    662   lapply Hocc; lapply Hbv; -Hocc -Hbv
    663   cases (instruction_matches_identifier … x h) in ⊢ (% → % → ???% → %);
    664   normalize nodelta #Hbv #Hocc #EQ
    665   [ >(bitvector_of_nat_ok 16 n 0)
    666     [ @le_O_n
    667     | >(eq_eq_bv … Hbv) @I
    668     | / by /
    669     | cases daemon
    670     ]
    671   | cases n in Hbv;
    672     [ #_ @le_O_n
    673     | -n #n #Hbv @le_S_S @(Hind … Hocc)
    674       [ @conj
    675         [ @(transitive_lt … (proj1 ?? Hprogram)) @le_n
    676         | cases daemon (* axiomatize this *)
    677         ]
    678       | #_ lapply (bitvector_of_nat_ok 16 (S n) (index_of_internal ? (instruction_matches_identifier ?? x) t 1) ???)
    679         [ >Hbv >eq_bv_refl @I
    680         | @(transitive_lt … (proj1 ?? Hprogram)) cases daemon
    681         | cases daemon
    682         | #H >(index_of_label_from_internal … Hocc)
    683           <plus_O_n >(index_of_label_from_internal … Hocc) in H;
    684           #H >(injective_S … H) <plus_O_n @refl
    685         ]
    686       ]
    687     ]
    688   ]
    689 ]
    690 qed.
    691 
    692646lemma equal_compact_unsafe_compact: ∀program:(Σl.(S (|l|)) < 2^16 ∧ is_well_labelled_p l).
    693   ∀labels.∀old_sigma.∀sigma.
     647  ∀old_sigma.∀sigma.
    694648  sigma_pc_equal program old_sigma sigma →
    695   sigma_safe program labels 0 old_sigma sigma →
    696   sigma_compact_unsafe program labels sigma →
    697   sigma_compact program labels sigma.
    698   #program #labels #old_sigma #sigma #Hequal #Hsafe #Hcp_unsafe #i #Hi
     649  sigma_safe program (create_label_map program) 0 old_sigma sigma →
     650  sigma_compact_unsafe program (create_label_map program) sigma →
     651  sigma_compact program (create_label_map program) sigma.
     652  #program #old_sigma #sigma #Hequal #Hsafe #Hcp_unsafe #i #Hi
    699653  lapply (Hcp_unsafe i Hi) lapply (Hsafe i Hi)
    700654  lapply (refl ? (lookup_opt … (bitvector_of_nat ? i) (\snd sigma)))
     
    723677            cases x2 normalize nodelta
    724678            [1,4: whd in match short_jump_cond; normalize nodelta
    725               lapply (refl ? (leb (lookup_def ?? labels x 0) (|[]@program|)))
    726               cases (leb (lookup_def ?? labels x 0) (|[]@program|)) in ⊢ (???% → %); #Hlab
    727               normalize nodelta
    728               >(Hequal (lookup_def ?? labels x 0) ?)
    729               [2,4,6,8: @(label_in_program program labels x)
    730                 cases daemon (* XXX this has to come from somewhere else *)
    731               ]
    732               <plus_n_O
     679              cut (lookup_def ?? (create_label_map program) x 0 ≤ (|program|))
     680              [1,3: cases daemon (* XXX should this be a property of create_label_map? *)
     681              |2,4: #H >(le_to_leb_true … H) normalize nodelta <plus_n_O
    733682              cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false)
    734683              #result #flags normalize nodelta
    735684              cases (vsplit bool 9 7 result) #upper #lower normalize nodelta
    736685              cases (get_index' bool 2 0 flags) normalize nodelta
    737               [5,6,7,8: #H @⊥ @(absurd ?? (proj2 ?? H)) / by I/
    738               |1,2,3,4: cases (eq_bv 9 upper ?)
    739                 [2,4,6,8: #H lapply (proj1 ?? H) #H3 destruct (H3)
    740                 |1,3,5,7: #_ normalize nodelta @refl
     686              [3,4: #H @⊥ @(absurd ?? (proj2 ?? H)) / by I/
     687              |1,2: cases (eq_bv 9 upper ?)
     688                [2,4: #H lapply (proj1 ?? H) #H3 destruct (H3)
     689                |1,3: #_ normalize nodelta @refl
    741690                ]
    742691              ]
     692              ]
    743693            |2,5: whd in match short_jump_cond; whd in match absolute_jump_cond;
    744               lapply (refl ? (leb (lookup_def ?? labels x 0) (|[]@program|)))
    745               cases (leb (lookup_def ?? labels x 0) (|[]@program|)) in ⊢ (???% → %); #Hlab
    746               normalize nodelta
    747               (* USE: added = 0 → policy_pc_equal (from fold) *)
    748               >(Hequal (lookup_def ?? labels x 0) ?)
    749               [2,4,6,8: @(label_in_program program labels x)
    750                 cases daemon (* XXX this has to come from somewhere else *)]
    751               <plus_n_O
     694              cut (lookup_def ?? (create_label_map program) x 0 ≤ (|program|))
     695              [1,3: cases daemon (* XXX should this be a property of create_label_map? *)
     696              |2,4: #H >(le_to_leb_true … H) normalize nodelta <plus_n_O
    752697              normalize nodelta cases (vsplit bool 5 11 ?) #addr1 #addr2
    753698              cases (vsplit bool 5 11 ?) #pc1 #pc2 normalize nodelta
     
    757702              cases (get_index' bool 2 0 flags) normalize nodelta
    758703              #H >(proj2 ?? (proj1 ?? H)) >(proj1 ?? (proj1 ?? H)) normalize nodelta @refl
     704              ]
    759705            |3,6: whd in match short_jump_cond; whd in match absolute_jump_cond;
    760               lapply (refl ? (leb (lookup_def ?? labels x 0) (|[]@program|)))
    761               cases (leb (lookup_def ?? labels x 0) (|[]@program|)) in ⊢ (???% → %); #Hlab
    762               normalize nodelta
    763               (* USE: added = 0 → policy_pc_equal (from fold) *)
    764               >(Hequal (lookup_def ?? labels x 0) ?)
    765               [2,4,6,8: @(label_in_program program labels x)
    766                 cases daemon (* XXX this has to come from somewhere else *)]
    767               <plus_n_O normalize nodelta
     706              cut (lookup_def ?? (create_label_map program) x 0 ≤ (|program|))
     707              [1,3: cases daemon (* XXX should this be a property of create_label_map? *)
     708              |2,4: #H >(le_to_leb_true … H) normalize nodelta <plus_n_O
    768709              cases (vsplit bool 5 11 ?) #addr1 #addr2
    769710              cases (vsplit bool 5 11 ?) #pc1 #pc2 normalize nodelta
     
    773714              cases (get_index' bool 2 0 flags) normalize nodelta
    774715              #H >(proj1 ?? H) >(proj2 ?? H) normalize nodelta @refl
     716              ]
    775717            ]
    776718          |1: #pi cases pi
     
    787729              whd in match expand_relative_jump_internal_unsafe;
    788730              normalize nodelta >(add_bitvector_of_nat_plus ? i 1)
    789               <(plus_n_Sm i 0) <plus_n_O
    790               cases daemon (* XXX this needs subadressing mode magic, see above *)
     731              <(plus_n_Sm i 0) <plus_n_O <plus_n_O cases x2 normalize nodelta
     732              [1,4,7,10,13,16,19,22,25:
     733                cut (∀A,B,ab.fst A B ab = (let 〈a,b〉 ≝ ab in a))
     734                [1,3,5,7,9,11,13,15,17: #A #B * / by refl/ ]
     735                #fst_foo >fst_foo @pair_elim #sj_possible #disp #H #H2
     736                @(pair_replace ?????????? (eq_to_jmeq … H))
     737                [1,3,5,7,9,11,13,15,17:
     738                  cut (lookup_def ?? (create_label_map program) x 0 ≤ (|program|))
     739                  [1,3,5,7,9,11,13,15,17: cases daemon] (* XXX should this be a property of create_label_map? *)
     740                  #X >(le_to_leb_true … X) @refl
     741                ]
     742                >(proj1 ?? H2) try (@refl) normalize nodelta
     743                [1,2,3,5: @(subaddressing_mode_elim … y) #w %
     744                | cases y * #sth #sth2 @(subaddressing_mode_elim … sth)
     745                  @(subaddressing_mode_elim … sth2) #x [3,4: #x2] %
     746                ]
     747              |2,5,8,11,14,17,20,23,26: ** #_ #_ #abs cases abs #abs2 @⊥ @abs2 / by I/
     748              ]
     749              cut (∀A,B,ab.fst A B ab = (let 〈a,b〉 ≝ ab in a))
     750              [1,3,5,7,9,11,13,15,17: #A #B * / by refl/ ]
     751              #fst_foo * #H #_ >fst_foo in H; @pair_elim #sj_possible #disp #H
     752              @(pair_replace ?????????? (eq_to_jmeq … H))
     753                [1,3,5,7,9,11,13,15,17:
     754                  cut (lookup_def ?? (create_label_map program) x 0 ≤ (|program|))
     755                  [1,3,5,7,9,11,13,15,17: cases daemon] (* XXX should this be a property of create_label_map? *)
     756                  #X >(le_to_leb_true … X) @refl
     757                ]
     758                #H2 >H2 try (@refl) normalize nodelta
     759                [1,2,3,5: @(subaddressing_mode_elim … y) #w %
     760                | cases y * #sth #sth2 @(subaddressing_mode_elim … sth2) #w
     761                  [1,2: %] whd in match (map ????); whd in match (flatten ??);
     762                  whd in match (map ????) in ⊢ (???%); whd in match (flatten ??) in ⊢ (???%);
     763                  >length_append >length_append @eq_f2 %
     764                ]
     765              ]
    791766            ]
    792767          ]
    793768        ]
    794769      ]
    795     ]
    796770qed.
    797771
Note: See TracChangeset for help on using the changeset viewer.