Changeset 2102


Ignore:
Timestamp:
Jun 20, 2012, 4:51:35 PM (5 years ago)
Author:
boender
Message:
  • some small changes
Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/PolicyFront.ma

    r2101 r2102  
    767767 ]
    768768qed.
     769
     770lemma 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 ]
     783qed.
     784 
     785lemma 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 ]
     826qed.
  • src/ASM/PolicyStep.ma

    r2101 r2102  
    116116      ]
    117117    | #Hnj
    118       (* USE: jump_not_in_policy (from fold and old_sigma) *)
     118      (* USE: not_jump_default (from fold and old_sigma) *)
    119119      >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind))))))) i Hi Hnj)
    120120      >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) i Hi Hnj)
     
    127127  >H2 in H; normalize nodelta -H2 -x #H @conj
    128128  [ @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) *)
    130130    @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))))
    131131  | (* policy_compact_unsafe → policy_compact (in the end) *)
     
    165165                (* USE: added = 0 → policy_pc_equal *)
    166166                >(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                ]
    170170                [1,5: >(eqb_true_to_eq … Hch) <plus_n_O]
    171171                cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false)
     
    185185                (* USE: added = 0 → policy_pc_equal *)
    186186                >(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 *)]
    188189                [1,3: >(eqb_true_to_eq … Hch) <plus_n_O]
    189190                normalize nodelta cases (vsplit bool 5 11 ?) #addr1 #addr2
     
    199200                normalize nodelta
    200201                >(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 *)]
    202204                [1,3: >(eqb_true_to_eq … Hch) <plus_n_O]
    203205                normalize nodelta
     
    224226               normalize nodelta >(add_bitvector_of_nat_plus ? i 1)
    225227               <(plus_n_Sm i 0) <plus_n_O
    226                cases daemon (* XXX *)
     228               cases daemon (* XXX this needs subadressing mode magic, see above *)
    227229             ]
    228230           ]
     
    286288      ]
    287289    ]
    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;
    289291    cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    290292    [ <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
    291293      [ >lookup_insert_miss
    292294        [ >(nth_append_first ? i prefix ?? Hi)
    293           (* USE: jump_not_in_policy *)
     295          (* USE: not_jump_default *)
    294296          @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) i Hi)
    295297        | @bitvector_of_nat_abs
     
    381383                whd in match jump_expansion_step_instruction; normalize nodelta #Heqi #Heq1
    382384                #Hj <(proj1 ?? (pair_destruct ?????? Heq1))
    383                 (* USE: jump_not_in_policy (from old_sigma) *)
     385                (* USE: not_jump_default (from old_sigma) *)
    384386                lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) (|prefix|) ??)
    385387                [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:
     
    401403              ]
    402404            |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) *)
    404406              lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) (|prefix|) ??)
    405407              [1,4,7: >prf >nth_append_second
Note: See TracChangeset for help on using the changeset viewer.