source: src/ASM/AssemblyProof.ma @ 838

Last change on this file since 838 was 838, checked in by sacerdot, 10 years ago

Restored.

File size: 7.4 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 ]
156qed.
157
158
159
160
161lemma execute_code_memory_unchanged:
162 ∀ticks_of,ps. code_memory ? ps = code_memory ? (execute_1_pseudo_instruction ticks_of ps).
163 #ticks #ps whd in ⊢ (??? (??%))
164 cases (fetch_pseudo_instruction (\snd (code_memory pseudo_assembly_program ps))
165  (program_counter pseudo_assembly_program ps)) #instr #pc
166 whd in ⊢ (??? (??%)) cases instr
167  [ #pre cases pre
168     [ #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
169       cases (split ????) #z1 #z2 %
170     | #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
171       cases (split ????) #z1 #z2 %
172     | #a1 #a2 whd in ⊢ (??? (??%)) cases (sub_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
173       cases (split ????) #z1 #z2 %
174     | #a1 whd in ⊢ (??? (??%)) cases a1 #x #H whd in ⊢ (??? (??%)) cases x
175       [ #x1 whd in ⊢ (??? (??%))
176     | *: cases not_implemented
177     ]
178  | #comment %
179  | #cost %
180  | #label %
181  | #label whd in ⊢ (??? (??%)) cases (half_add ???) #x1 #x2 whd in ⊢ (??? (??%))
182    cases (split ????) #y1 #y2 whd in ⊢ (??? (??%)) cases (half_add ???) #z1 #z2
183    whd in ⊢ (??? (??%)) whd in ⊢ (??? (??%)) cases (split ????) #w1 #w2
184    whd in ⊢ (??? (??%)) cases (get_index_v bool ????) whd in ⊢ (??? (??%))
185    (* CSC: ??? *)
186  | #dptr #label (* CSC: ??? *)
187  ]
188  cases not_implemented
189qed.
190
191lemma foo:
192 ∀ticks_of.
193 ∀ps: PseudoStatus.
194  match status_of_pseudo_status ps with [ None ⇒ True | Some s ⇒
195  let ps' ≝ execute_1_pseudo_instruction ticks_of ps in
196  match status_of_pseudo_status ps' with [ None ⇒ True | Some s'' ⇒
197  let s' ≝ execute_1 s in
198   s = s'']].
199 #ticks_of #ps
200 whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
201 cases (assembly (code_memory pseudo_assembly_program ps)) [%] * #cm #costs whd
202 whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
203 cases (status_of_pseudo_status (execute_1_pseudo_instruction ticks_of ps)) [%] #s'' whd
Note: See TracBrowser for help on using the repository browser.