source: src/ASM/AssemblyProof.ma @ 839

Last change on this file since 839 was 839, checked in by sacerdot, 8 years ago

More experiments.

File size: 8.0 KB
Line 
1include "ASM/Assembly.ma".
2include "ASM/Interpret.ma".
3
4let rec encoding_check (code_memory: BitVectorTrie Byte 16) (pc: Word) (final_pc: Word)
5                       (encoding: list Byte) on encoding: Prop ≝
6  match encoding with
7  [ nil ⇒ final_pc = pc
8  | cons hd tl ⇒
9    let 〈new_pc, byte〉 ≝ next code_memory pc in
10      hd = byte ∧ encoding_check code_memory new_pc final_pc tl
11  ].
12
13axiom sigma: pseudo_assembly_program → Word → Word.
14
15definition assembly_specification:
16  ∀assembly_program: pseudo_assembly_program.
17  ∀code_mem: BitVectorTrie Byte 16. Prop ≝
18  λpseudo_assembly_program.
19  λcode_mem.
20    ∀pc: Word.
21      let 〈preamble, instr_list〉 ≝ pseudo_assembly_program in
22      let 〈pre_instr, pre_new_pc〉 ≝ fetch_pseudo_instruction instr_list pc in
23      let labels ≝ λx. sigma pseudo_assembly_program (address_of_word_labels_code_mem instr_list x) in
24      let datalabels ≝ λx. sigma pseudo_assembly_program (lookup ? ? x (construct_datalabels preamble) (zero ?)) in
25      let pre_assembled ≝ assembly_1_pseudoinstruction pseudo_assembly_program
26       (sigma pseudo_assembly_program pc) labels datalabels pre_instr in
27      match pre_assembled with
28       [ None ⇒ True
29       | Some pc_code ⇒
30          let 〈new_pc,code〉 ≝ pc_code in
31           encoding_check code_mem pc (sigma pseudo_assembly_program pre_new_pc) code ].
32
33axiom assembly_meets_specification:
34  ∀pseudo_assembly_program.
35    match assembly pseudo_assembly_program with
36    [ None ⇒ True
37    | Some code_mem_cost ⇒
38      let 〈code_mem, cost〉 ≝ code_mem_cost in
39        assembly_specification pseudo_assembly_program (load_code_memory code_mem)
40    ].
41(*
42  # PROGRAM
43  [ cases PROGRAM
44    # PREAMBLE
45    # INSTR_LIST
46    elim INSTR_LIST
47    [ whd
48      whd in ⊢ (∀_. %)
49      # PC
50      whd
51    | # INSTR
52      # INSTR_LIST_TL
53      # H
54      whd
55      whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?])
56    ]
57  | cases not_implemented
58  ] *)
59
60definition status_of_pseudo_status: PseudoStatus → option Status ≝
61 λps.
62  let pap ≝ code_memory … ps in
63   match assembly pap with
64    [ None ⇒ None …
65    | Some p ⇒
66       let cm ≝ load_code_memory (\fst p) in
67       let pc ≝ sigma pap (program_counter ? ps) in
68        Some …
69         (mk_PreStatus (BitVectorTrie Byte 16)
70           cm
71           (low_internal_ram … ps)
72           (high_internal_ram … ps)
73           (external_ram … ps)
74           pc
75           (special_function_registers_8051 … ps)
76           (special_function_registers_8052 … ps)
77           (p1_latch … ps)
78           (p3_latch … ps)
79           (clock … ps)) ].
80           
81(* RUSSEL **)
82
83include "basics/jmeq.ma".
84
85definition inject : ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ λA,P,a,p. dp … a p.
86definition eject : ∀A.∀P: A → Prop.(Σx:A.P x) → A ≝ λA,P,c.match c with [ dp w p ⇒ w].
87
88coercion inject : ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ inject on a:? to Σx:?.?.
89coercion eject : ∀A.∀P:A → Prop.∀c:Σx:A.P x.A ≝ eject on _c:Σx:?.? to ?.
90
91lemma sig2: ∀A.∀P:A → Prop. ∀p:Σx:A.P x. P (eject … p).
92 #A #P #p cases p #w #q @q
93qed.
94
95(* END RUSSELL **)
96
97definition write_at_stack_pointer':
98 ∀M. ∀ps: PreStatus M. Byte → Σps':PreStatus M.(code_memory … ps = code_memory … ps') ≝
99  λM: Type[0].
100  λs: PreStatus M.
101  λv: Byte.
102    let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr ? s SFR_SP) in
103    let bit_zero ≝ get_index_v… nu O ? in
104    let bit_1 ≝ get_index_v… nu 1 ? in
105    let bit_2 ≝ get_index_v… nu 2 ? in
106    let bit_3 ≝ get_index_v… nu 3 ? in
107      if bit_zero then
108        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
109                              v (low_internal_ram ? s) in
110          set_low_internal_ram ? s memory
111      else
112        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
113                              v (high_internal_ram ? s) in
114          set_high_internal_ram ? s memory.
115  [ cases l0 %
116  |2,3,4,5: cases not_implemented (* CSC: ???? normalize repeat (@ le_S_S) @ le_O_n *)
117  ]
118qed.
119
120definition execute_1_pseudo_instruction': (Word → nat) → ∀ps:PseudoStatus.
121 Σps':PseudoStatus.(code_memory … ps = code_memory … ps')
122
123  λticks_of.
124  λs.
125  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
126  let ticks ≝ ticks_of (program_counter ? s) in
127  let s ≝ set_clock ? s (clock ? s + ticks) in
128  let s ≝ set_program_counter ? s pc in
129    match instr with
130    [ Instruction instr ⇒
131       execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s
132    | Comment cmt ⇒ s
133    | Cost cst ⇒ s
134    | Jmp jmp ⇒ set_program_counter ? s (address_of_word_labels s jmp)
135    | Call call ⇒
136      let a ≝ address_of_word_labels s call in
137      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
138      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
139      let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
140      let s ≝ write_at_stack_pointer' ? s pc_bl in
141      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
142      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
143      let s ≝ write_at_stack_pointer' ? s pc_bu in
144        set_program_counter ? s a
145    | Mov dptr ident ⇒
146       set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr
147    ].
148 [
149 |2,3,4: %
150 | <(sig2 … l7) whd in ⊢ (??? (??%)) <(sig2 … l5) %
151 |
152 | (*CSC: ??? *)
153 | (*CSC: ??? *)
154 | %
155 ]
156 cases not_implemented
157qed.
158
159(*
160lemma execute_code_memory_unchanged:
161 ∀ticks_of,ps. code_memory ? ps = code_memory ? (execute_1_pseudo_instruction ticks_of ps).
162 #ticks #ps whd in ⊢ (??? (??%))
163 cases (fetch_pseudo_instruction (\snd (code_memory pseudo_assembly_program ps))
164  (program_counter pseudo_assembly_program ps)) #instr #pc
165 whd in ⊢ (??? (??%)) cases instr
166  [ #pre cases pre
167     [ #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
168       cases (split ????) #z1 #z2 %
169     | #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
170       cases (split ????) #z1 #z2 %
171     | #a1 #a2 whd in ⊢ (??? (??%)) cases (sub_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
172       cases (split ????) #z1 #z2 %
173     | #a1 whd in ⊢ (??? (??%)) cases a1 #x #H whd in ⊢ (??? (??%)) cases x
174       [ #x1 whd in ⊢ (??? (??%))
175     | *: cases not_implemented
176     ]
177  | #comment %
178  | #cost %
179  | #label %
180  | #label whd in ⊢ (??? (??%)) cases (half_add ???) #x1 #x2 whd in ⊢ (??? (??%))
181    cases (split ????) #y1 #y2 whd in ⊢ (??? (??%)) cases (half_add ???) #z1 #z2
182    whd in ⊢ (??? (??%)) whd in ⊢ (??? (??%)) cases (split ????) #w1 #w2
183    whd in ⊢ (??? (??%)) cases (get_index_v bool ????) whd in ⊢ (??? (??%))
184    (* CSC: ??? *)
185  | #dptr #label (* CSC: ??? *)
186  ]
187  cases not_implemented
188qed.
189*)
190
191lemma status_of_pseudo_status_failure_depends_only_on_code_memory:
192 ∀ps,ps': PseudoStatus.
193  code_memory … ps = code_memory … ps' →
194   match status_of_pseudo_status ps with
195    [ None ⇒ status_of_pseudo_status ps' = None …
196    | Some _ ⇒ ∃w. status_of_pseudo_status ps' = Some … w
197    ].
198 #ps #ps' #H whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
199 generalize in match (refl … (assembly (code_memory … ps)))
200 cases (assembly ?) in ⊢ (???% → %)
201  [ #K whd whd in ⊢ (??%?) <H >K %
202  | #x #K whd whd in ⊢ (?? (λ_.??%?)) <H >K % [2: % ] ]
203qed.
204 
205lemma main_thm:
206 ∀ticks_of.
207 ∀ps: PseudoStatus.
208  match status_of_pseudo_status ps with [ None ⇒ True | Some s ⇒
209  let ps' ≝ execute_1_pseudo_instruction ticks_of ps in
210  match status_of_pseudo_status ps' with [ None ⇒ True | Some s'' ⇒
211  let s' ≝ execute_1 s in
212   s = s'']].
213 #ticks_of #ps
214 whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
215 cases (assembly (code_memory pseudo_assembly_program ps)) [%] * #cm #costs whd
216 whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
217 generalize in match (sig2 … (execute_1_pseudo_instruction' ticks_of ps))
218 
219 cases (status_of_pseudo_status (execute_1_pseudo_instruction ticks_of ps)) [%] #s'' whd
Note: See TracBrowser for help on using the repository browser.