Changeset 845
 Timestamp:
 May 25, 2011, 6:09:38 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r841 r845 1 1 include "ASM/Assembly.ma". 2 2 include "ASM/Interpret.ma". 3 4 (* RUSSEL **) 5 6 include "basics/jmeq.ma". 7 8 definition inject : ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ λA,P,a,p. dp … a p. 9 definition eject : ∀A.∀P: A → Prop.(Σx:A.P x) → A ≝ λA,P,c.match c with [ dp w p ⇒ w]. 10 11 coercion inject : ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ inject on a:? to Σx:?.?. 12 coercion eject : ∀A.∀P:A → Prop.∀c:Σx:A.P x.A ≝ eject on _c:Σx:?.? to ?. 13 14 axiom VOID: Type[0]. 15 axiom assert_false: VOID. 16 definition bigbang: ∀A:Type[0].∀P:A → Prop. False → VOID → Σx:A.P x. 17 #A #P #abs cases abs 18 qed. 19 20 (*coercion bigbang : ∀A.∀P:A → Prop.False → ∀v:VOID.Σx:A.P x ≝ bigbang on _v:VOID to Σx:?.?.*) 21 22 lemma sig2: ∀A.∀P:A → Prop. ∀p:Σx:A.P x. P (eject … p). 23 #A #P #p cases p #w #q @q 24 qed. 25 26 (* END RUSSELL **) 3 27 4 28 (* This establishes the correspondence between pseudo program counters and 5 29 program counters. It is at the heart of the proof. *) 6 30 (*CSC: code taken from build_maps *) 7 definition sigma : pseudo_assembly_program → option (Word → Word) ≝31 definition sigma0: pseudo_assembly_program → option (nat × (nat × (BitVectorTrie Word 16))) ≝ 8 32 λinstr_list. 9 let result ≝foldl ??33 foldl ?? 10 34 (λt. λi. 11 35 match t with … … 20 44 let 〈pc,ignore〉 ≝ pc_ignore in 21 45 Some … 〈S ppc,〈pc, insert ? ? (bitvector_of_nat ? ppc) (bitvector_of_nat ? pc) sigma_map〉〉 ] 22 ]) (Some ? 〈0, 〈0, (Stub ? ?)〉〉) (\snd instr_list) in 23 match result with 46 ]) (Some ? 〈0, 〈0, (Stub ? ?)〉〉) (\snd instr_list). 47 48 definition tech_pc_sigma0: pseudo_assembly_program → option nat ≝ 49 λinstr_list. 50 match sigma0 instr_list with 51 [ None ⇒ None … 52  Some result ⇒ 53 let 〈ppc,pc_sigma_map〉 ≝ result in 54 let 〈pc, sigma_map〉 ≝ pc_sigma_map in 55 Some … pc ]. 56 57 definition sigma: pseudo_assembly_program → option (Word → Word) ≝ 58 λinstr_list. 59 match sigma0 instr_list with 24 60 [ None ⇒ None ? 25 61  Some result ⇒ … … 30 66 else 31 67 Some ? (λx.lookup ?? x sigma_map (zero …)) ]. 68 69 axiom policy_ok: ∀p. sigma p ≠ None …. 70 71 axiom is_prefix: ∀A:Type[0]. list A → list A → Prop. 72 73 definition build_maps' ≝ 74 λpseudo_program. 75 let 〈preamble,instr_list〉 ≝ pseudo_program in 76 let result ≝ 77 foldl 78 (Σt:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))). 79 ∃instr_list_prefix. is_prefix ? instr_list_prefix instr_list ∧ 80 tech_pc_sigma0 〈preamble,instr_list_prefix〉 = Some ? (\fst (\snd t))) 81 (Σi:option Identifier × pseudo_instruction. ∀instr_list_prefix. 82 let instr_list_prefix' ≝ instr_list_prefix @ [i] in 83 is_prefix ? instr_list_prefix' instr_list ∧ 84 tech_pc_sigma0 〈preamble,instr_list_prefix'〉 ≠ None ?) 85 (λt: Σt:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))). 86 ∃instr_list_prefix. is_prefix ? instr_list_prefix instr_list ∧ 87 tech_pc_sigma0 〈preamble,instr_list_prefix〉 = Some ? (\fst (\snd t)). 88 λi: Σi:option Identifier × pseudo_instruction. ∀instr_list_prefix. 89 let instr_list_prefix' ≝ instr_list_prefix @ [i] in 90 is_prefix ? instr_list_prefix' instr_list ∧ 91 tech_pc_sigma0 〈preamble,instr_list_prefix'〉 ≠ None ? . 92 let 〈labels, pc_costs〉 ≝ t in 93 let 〈program_counter, costs〉 ≝ pc_costs in 94 let 〈label, i'〉 ≝ i in 95 let labels ≝ 96 match label with 97 [ None ⇒ labels 98  Some label ⇒ 99 let program_counter_bv ≝ bitvector_of_nat ? program_counter in 100 insert ? ? label program_counter_bv labels 101 ] 102 in 103 match construct_costs pseudo_program program_counter (λx. zero ?) (λx. zero ?) costs i' with 104 [ None ⇒ 〈labels,pc_costs〉 (*assert_false*) 105  Some construct ⇒ 〈labels, construct〉 106 ] 107 ) 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉 (\snd ?(*instr_list*)) 108 in 109 let 〈labels, pc_costs〉 ≝ result in 110 let 〈pc, costs〉 ≝ pc_costs in 111 〈labels, costs〉. 112 [ cases t in c2 ⊢ % #t' * #LIST_PREFIX * #H1t' #H2t' #HJMt' 113 % [@ (LIST_PREFIX @ [i])] % 114 [ cases (sig2 … i LIST_PREFIX) #K1 #K2 @K1 115  (* DOABLE IN PRINCIPLE *) 116 ] 117  (* assert false case *) 118 3: % [@ ([ ])] % [2: %  (* DOABLE *)] 119  120 121 32 122 33 123 … … 109 199 (clock … ps)) ]. 110 200 111 (* RUSSEL **)112 113 include "basics/jmeq.ma".114 115 definition inject : ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ λA,P,a,p. dp … a p.116 definition eject : ∀A.∀P: A → Prop.(Σx:A.P x) → A ≝ λA,P,c.match c with [ dp w p ⇒ w].117 118 coercion inject : ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ inject on a:? to Σx:?.?.119 coercion eject : ∀A.∀P:A → Prop.∀c:Σx:A.P x.A ≝ eject on _c:Σx:?.? to ?.120 121 lemma sig2: ∀A.∀P:A → Prop. ∀p:Σx:A.P x. P (eject … p).122 #A #P #p cases p #w #q @q123 qed.124 125 (* END RUSSELL **)126 127 201 definition write_at_stack_pointer': 128 202 ∀M. ∀ps: PreStatus M. Byte → Σps':PreStatus M.(code_memory … ps = code_memory … ps') ≝
Note: See TracChangeset
for help on using the changeset viewer.