Ignore:
Timestamp:
Jul 4, 2012, 1:23:00 PM (8 years ago)
Author:
boender
Message:
  • this should compile
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/PolicyFront.ma

    r2141 r2152  
    400400    match policy with
    401401    [ None ⇒ True
    402     | Some p ⇒ And (And (And (And (And (And
    403        (out_of_program_none (pi1 ?? program) p)
    404        (not_jump_default (pi1 ?? program) p))
     402    | Some p ⇒ And (And (And (And (And
     403       (not_jump_default (pi1 ?? program) p)
    405404       (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0))
    406405       (\fst p = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd p) 〈0,short_jump〉)))
     
    412411  λprogram.λlabels.
    413412  let final_policy ≝ foldl_strong (option Identifier × pseudo_instruction)
    414   (λprefix.Σpolicy:ppc_pc_map.And (And (And (And (And
    415     (out_of_program_none prefix policy)
    416     (not_jump_default prefix policy))
     413  (λprefix.Σpolicy:ppc_pc_map.And (And (And (And
     414    (not_jump_default prefix policy)
    417415    (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0))
    418416    (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd policy) 〈0,short_jump〉)))
     
    434432| lapply p -p generalize in match (foldl_strong ?????); * #p #Hp #hg
    435433  @conj [ @Hp | @not_le_to_lt @leb_false_to_not_le <geb_to_leb @hg ]
    436 | @conj [ @conj [ @conj [ @conj [ @conj
     434| @conj [ @conj [ @conj [ @conj (*[@conj
    437435  [ (* out_of_program_none *)
    438436    #i #Hi2 >append_length <commutative_plus @conj
     
    482480      ]
    483481    ]
    484   | (* not_jump_default *) cases p -p #p cases p -p #pc #sigma #Hp
     482  | *)
     483  [ (* not_jump_default *) cases p -p #p cases p -p #pc #sigma #Hp
    485484    cases x in prf; #lbl #ins #prf #i >append_length <commutative_plus #Hi
    486485    normalize in Hi; normalize nodelta cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    487486    [ >lookup_insert_miss
    488487      [ (* USE[pass]: not_jump_default *)
    489         lapply ((proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))))) i Hi)
     488        lapply (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))) i Hi)
    490489        >nth_append_first
    491490        [ #H #H2 @H @H2
     
    511510      ]
    512511    ]
    513   ]
    514512  | (* 0 ↦ 0 *)
    515513    cases p -p #p cases p -p #pc #sigma #Hp cases x #lbl #instr normalize nodelta
    516514    >lookup_insert_miss
    517515    [ (* USE[pass]: 0 ↦ 0 *)
    518       @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) 
     516      @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))))
    519517    | @bitvector_of_nat_abs
    520518      [ / by /
     
    596594    ]
    597595  ]
    598 | @conj [ @conj [ @conj [ @conj [ @conj
     596| @conj [ @conj [ @conj [ @conj (*[ @conj
    599597  [ #i cases i
    600598    [ #Hi2 @conj
     
    613611      | #_ @le_S_S @le_O_n
    614612      ]
    615     ]
    616   | #i cases i
     613    ] *)
     614  [ #i cases i
    617615    [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
    618616    | -i #i #Hi #Hj @⊥ @(absurd … Hi) @not_le_Sn_O
    619617    ]
    620   ] ] ]
     618  ] ]
    621619  >lookup_insert_hit @refl
    622620  | #i cases i
     
    862860    ]
    863861qed.
     862
     863lemma instruction_size_irrelevant: ∀i.
     864  ¬is_jump i → ∀j1,j2.instruction_size_jmplen j1 i = instruction_size_jmplen j2 i.
     865 #i cases i
     866 [2,3,6: #x [3: #y] #Hj #j1 #j2 %
     867 |4,5: #x #Hi cases Hi #abs @⊥ @abs @I
     868 |1: #pi cases pi
     869   [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:
     870     [1,2,3,6,7,24,25: #x #y
     871     |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
     872     #Hj #j1 #j2 %
     873   |9,10,11,12,13,14,15,16,17: [1,2,6,7: #x |3,4,5,8,9: #y #x]
     874     #Hi cases Hi #abs @⊥ @abs @I
     875   ]
     876 ]
     877qed.
Note: See TracChangeset for help on using the changeset viewer.