source: src/ASM/AssemblyProof.ma @ 2157

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

Anticipating a proof needed before.

File size: 39.3 KB
Line 
1include "ASM/Assembly.ma".
2include "ASM/Interpret.ma".
3include "ASM/StatusProofs.ma".
4include alias "arithmetics/nat.ma".
5
6let rec encoding_check
7  (code_memory: BitVectorTrie Byte 16) (pc: Word) (final_pc: Word)
8    (encoding: list Byte)
9      on encoding: Prop ≝
10  match encoding with
11  [ nil ⇒ final_pc = pc
12  | cons hd tl ⇒
13    let 〈new_pc, byte〉 ≝ next code_memory pc in
14      hd = byte ∧ encoding_check code_memory new_pc final_pc tl
15  ].
16
17lemma encoding_check_append:
18  ∀code_memory: BitVectorTrie Byte 16.
19  ∀final_pc: Word.
20  ∀l1: list Byte.
21  ∀pc: Word.
22  ∀l2: list Byte.
23    encoding_check code_memory pc final_pc (l1@l2) →
24      let pc_plus_len ≝ add … pc (bitvector_of_nat … (length … l1)) in
25        encoding_check code_memory pc pc_plus_len l1 ∧
26          encoding_check code_memory pc_plus_len final_pc l2.
27  #code_memory #final_pc #l1 elim l1
28  [1:
29    #pc #l2
30    whd in ⊢ (????% → ?); #H
31    <add_zero
32    whd whd in ⊢ (?%?); /2/
33  |2:
34    #hd #tl #IH #pc #l2 * #H1 #H2
35(*    >add_SO in H2; #H2 *)
36    cases (IH … H2) #E1 #E2 %
37    [1:
38      % try @H1
39      <(add_bitvector_of_nat_Sm 16 (|tl|)) in E1;
40      <add_associative #assm assumption
41    |2:
42      <add_associative in E2;
43      <(add_bitvector_of_nat_Sm 16 (|tl|)) #assm
44      assumption
45    ]
46  ]
47qed.
48
49definition ticks_of_instruction ≝
50  λi.
51    let trivial_code_memory ≝ assembly1 i in
52    let trivial_status ≝ load_code_memory trivial_code_memory in
53      \snd (fetch trivial_status (zero ?)).
54
55lemma fetch_assembly:
56  ∀pc: Word.
57  ∀i: instruction.
58  ∀code_memory: BitVectorTrie Byte 16.
59  ∀assembled: list Byte.
60    assembled = assembly1 i →
61      let len ≝ length … assembled in
62      let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
63        encoding_check code_memory pc pc_plus_len assembled →
64          let 〈instr, pc', ticks〉 ≝ fetch code_memory pc in
65           (eq_instruction instr i ∧ eqb ticks (ticks_of_instruction instr) ∧ eq_bv … pc' pc_plus_len) = true.
66  cases daemon
67(* XXX: commented out as takes ages to typecheck
68  #pc #i #code_memory #assembled cases i [8: *]
69 [16,20,29: * * |18,19: * * [1,2,4,5: *] |28: * * [1,2: * [1,2: * [1,2: * [1,2: *]]]]]
70 [47,48,49:
71 |*: #arg @(subaddressing_mode_elim … arg)
72  [2,3,5,7,10,12,16,17,18,21,26,27,28,31,32,33,37,38,39,40,41,42,43,44,45,48,51,58,
73   59,60,63,64,65,66,67: #ARG]]
74 [4,5,6,7,8,9,10,11,12,13,22,23,24,27,28,39,40,41,42,43,44,45,46,47,48,49,50,51,52,
75  56,57,69,70,72: #arg2 @(subaddressing_mode_elim … arg2)
76  [1,2,4,7,9,11,12,14,15,17,18,19,20,22,23,24,25,26,27,28,29,30,31,32,33,36,37,38,
77   39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,
78   68,69,70,71: #ARG2]]
79 [1,2,19,20: #arg3 @(subaddressing_mode_elim … arg3) #ARG3]
80 normalize in ⊢ (???% → ?);
81 [92,94,42,93,95: @vsplit_elim #vl #vm #E >E -E; [2,4: @(bitvector_3_elim_prop … vl)]
82  normalize in ⊢ (???% → ?);]
83 #H >H * #H1 try (whd in ⊢ (% → ?); * #H2)
84 try (whd in ⊢ (% → ?); * #H3) whd in ⊢ (% → ?); #H4
85 whd in match fetch; normalize nodelta <H1 whd in ⊢ (match % with [ _ ⇒ ? ]);
86 [17,18,19,20,21,22,23,24,25,26,32,34,35,36,37,39: <H3]
87 try <H2 whd >eq_instruction_refl >H4 @eq_bv_refl *)
88qed.
89
90let rec fetch_many
91  (code_memory: BitVectorTrie Byte 16) (final_pc: Word) (pc: Word)
92    (expected: list instruction)
93      on expected: Prop ≝
94  match expected with
95  [ nil ⇒ eq_bv … pc final_pc = true
96  | cons i tl ⇒
97    let pc' ≝ add 16 pc (bitvector_of_nat 16 (|assembly1 … i|)) in
98      (〈i, pc', ticks_of_instruction i〉 = fetch code_memory pc ∧
99        fetch_many code_memory final_pc pc' tl)
100  ].
101         
102lemma fetch_assembly_pseudo':
103  ∀lookup_labels.
104  ∀sigma: Word → Word.
105  ∀policy: Word → bool.
106  ∀ppc.
107  ∀lookup_datalabels.
108  ∀pi.
109  ∀code_memory.
110  ∀len.
111  ∀assembled.
112  ∀instructions.
113    let pc ≝ sigma ppc in
114      instructions = expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi →
115        〈len,assembled〉 = assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi →
116          let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
117            encoding_check code_memory pc pc_plus_len assembled →
118              fetch_many code_memory pc_plus_len pc instructions.
119  #lookup_labels #sigma #policy #ppc #lookup_datalabels #pi #code_memory #len #assembled #instructions
120  normalize nodelta #instructions_refl whd in ⊢ (???% → ?); <instructions_refl whd in ⊢ (???% → ?); #assembled_refl
121  cases (pair_destruct ?????? assembled_refl) -assembled_refl #len_refl #assembled_refl
122  >len_refl >assembled_refl -len_refl
123  generalize in match (add 16 (sigma ppc)
124    (bitvector_of_nat 16
125     (|flatten (Vector bool 8)
126       (map instruction (list (Vector bool 8)) assembly1 instructions)|)));
127  #final_pc
128  generalize in match (sigma ppc); elim instructions
129  [1:
130    #pc whd in ⊢ (% → %); #H >H @eq_bv_refl
131  |2:
132    #i #tl #IH #pc #H whd
133    cases (encoding_check_append ????? H) -H #H1 #H2
134    lapply (fetch_assembly pc i code_memory (assembly1 i) (refl …)) whd in ⊢ (% → ?);   
135    cases (fetch ??) * #instr #pc' #ticks
136    #H3 lapply (H3 H1) -H3 normalize nodelta #H3
137    lapply (conjunction_true ?? H3) * #H4 #H5
138    lapply (conjunction_true … H4) * #B1 #B2
139    >(eq_instruction_to_eq … B1) >(eq_bv_eq … H5) %
140    >(eqb_true_to_refl … B2) >(eq_instruction_to_eq … B1) try % @IH @H2
141  ]
142qed.
143
144lemma fetch_assembly_pseudo:
145  ∀program: pseudo_assembly_program.
146  ∀sigma: Word → Word.
147  ∀policy: Word → bool.
148  let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
149  let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in
150  ∀ppc.∀ppc_ok.
151  ∀code_memory.
152  let lookup_datalabels ≝ λx:Identifier. lookup_def … (construct_datalabels (\fst  program)) x (zero 16) in
153  let pi ≝  \fst  (fetch_pseudo_instruction (\snd program) ppc ppc_ok) in
154  let pc ≝ sigma ppc in
155  let instructions ≝ expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi in
156  let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in
157  let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
158    encoding_check code_memory pc pc_plus_len assembled →
159      fetch_many code_memory pc_plus_len pc instructions.
160  #program #sigma #policy
161  @pair_elim #labels #costs #create_label_cost_map_refl
162  letin lookup_labels ≝ (λx.?) #ppc #ppc_ok #code_memory
163  letin lookup_datalabels ≝ (λx.?)
164  letin pi ≝ (fst ???)
165  letin pc ≝ (sigma ?)
166  letin instructions ≝ (expand_pseudo_instruction ??????)
167  @pair_elim #len #assembled #assembled_refl normalize nodelta
168  #H
169  generalize in match
170   (fetch_assembly_pseudo' lookup_labels sigma policy ppc lookup_datalabels pi code_memory len assembled instructions) in ⊢ ?;
171  #X destruct normalize nodelta @X try % <assembled_refl try % assumption
172qed.
173
174definition is_present_in_machine_code_image_p: ∀pseudo_instruction. Prop ≝
175  λpseudo_instruction.
176    match pseudo_instruction with
177    [ Comment c ⇒ False
178    | Cost c ⇒ False
179    | _ ⇒ True
180    ].
181
182lemma monotone_sigma:
183 ∀program. |\snd program| ≤ 2^16 →
184 ∀sigma: Word → Word. ∀policy: Word → bool.
185  sigma_policy_specification program sigma policy →
186   ∀ppc1,ppc2.
187    nat_of_bitvector … ppc2 ≤ |\snd program| →
188    nat_of_bitvector … ppc1 ≤ nat_of_bitvector … ppc2 →
189     (nat_of_bitvector … (sigma ppc1) ≤ nat_of_bitvector … (sigma ppc2) ∨
190      sigma ppc2 = zero … ∧ nat_of_bitvector … ppc2 = |\snd program|).
191 #program #program_bounded #sigma #policy * #SIGMAOK1 #SIGMAOK2 #ppc1 #ppc2
192 #ppc2_ok #LE
193 <(bitvector_of_nat_inverse_nat_of_bitvector … ppc1)
194 <(bitvector_of_nat_inverse_nat_of_bitvector … ppc2) in ⊢ (?%(?%?));
195 lapply (le_n … (nat_of_bitvector … ppc2))
196 elim LE in ⊢ (?%? → %);
197 [ #_ % %
198 | #m #LE_ppc1_m #IH #BOUNDED
199   cases (IH ?)
200   [3: @(transitive_le … BOUNDED) %2 %
201   |2: * #_ #abs @⊥ <abs in ppc2_ok; #abs'
202       @(absurd ?? (not_le_Sn_n m))
203       @(transitive_le … BOUNDED abs') ]
204   -IH #IH
205   cut (m < |\snd program|) [ @(lt_to_le_to_lt … ppc2_ok) assumption ] #LT1
206   cut (m < 2^16) [ @(lt_to_le_to_lt … program_bounded) assumption ] #LT2
207   cases (SIGMAOK2 (bitvector_of_nat … m) ?) -SIGMAOK2
208   [2: >nat_of_bitvector_bitvector_of_nat_inverse assumption ]
209   #H *
210   [ #LTsigma_m %1 @(transitive_le … IH) -IH
211     <add_bitvector_of_nat_Sm >add_commutative >H -H
212     >nat_of_bitvector_add
213     [ //
214     | >nat_of_bitvector_bitvector_of_nat_inverse try assumption lapply LTsigma_m
215       whd in match instruction_size; normalize nodelta
216       inversion (assembly_1_pseudoinstruction ??????) #len #assembled #EQ #X
217       @(transitive_le … X) @le_S_S //
218     ]
219   | * #EQ1 #EQ2 %2 %
220     [ <add_bitvector_of_nat_Sm >add_commutative >H
221       lapply (eq_f … (bitvector_of_nat 16) … EQ2)
222       <add_bitvector_of_nat_plus
223       >bitvector_of_nat_inverse_nat_of_bitvector #X >X @bitvector_of_nat_exp_zero
224     | <(nat_of_bitvector_bitvector_of_nat_inverse 16 m) try assumption
225     ]]]
226qed.
227
228(* This is a non trivial consequence of fetch_assembly_pseudo +
229   load_code_memory_ok because of the finite amount of memory. In
230   particular the case when the compiled program exhausts the
231   code memory is very tricky. It also requires monotonicity of
232   sigma in the out-of-bounds region too. *)     
233lemma assembly_ok:
234  ∀program.
235  ∀length_proof: |\snd program| ≤ 2^16.
236  ∀sigma: Word → Word.
237  ∀policy: Word → bool.
238  ∀sigma_policy_witness: sigma_policy_specification program sigma policy.
239  ∀assembled.
240  ∀costs': BitVectorTrie costlabel 16.
241  let 〈preamble, instr_list〉 ≝ program in
242  let 〈labels, costs〉 ≝ create_label_cost_map instr_list in
243  let datalabels ≝ construct_datalabels preamble in
244  let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero …) in
245    〈assembled,costs'〉 = assembly program sigma policy →
246      (* costs = costs' ∧ CSC: costs != costs', costs' = sigma costs! *)
247        let code_memory ≝ load_code_memory assembled in
248        let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in
249          ∀ppc.∀ppc_ok.
250            let 〈pi, newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc ppc_ok in     
251            let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in
252            let pc ≝ sigma ppc in
253            let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
254              encoding_check code_memory pc pc_plus_len assembled ∧
255                  sigma newppc = add … pc (bitvector_of_nat … len).
256  #program #length_proof #sigma #policy #sigma_policy_witness #assembled #costs'
257  cases (assembly program sigma policy) * #assembled' #costs''
258  @pair_elim #preamble #instr_list #EQprogram whd in ⊢ (% → %);
259  cut (|instr_list| ≤ 2^16) [ >EQprogram in length_proof; // ] #instr_list_ok
260  #H lapply (H sigma_policy_witness instr_list_ok) -H whd in ⊢ (% → ?);
261  @pair_elim #labels #costs #create_label_cost_refl whd in ⊢ (% → %);
262  * * #assembly_ok1 #assembly_ok3 #assembly_ok2 #Pair_eq destruct(Pair_eq) whd
263  #ppc #ppc_ok @pair_elim #pi #newppc #eq_fetch_pseudo_instruction
264  @pair_elim #len #assembled #eq_assembly_1_pseudoinstruction whd
265  lapply (assembly_ok2 ppc ?) try // -assembly_ok2
266  >eq_fetch_pseudo_instruction
267  change with ((let 〈len0,assembledi〉 ≝ assembly_1_pseudoinstruction ????? pi in ? ∧ ∀j.∀H:j<|assembledi|.?) → ?)
268  >eq_assembly_1_pseudoinstruction
269  whd in ⊢ (% → ?); * #assembly_ok4 #assembly_ok
270  %
271  [2: >(pair_destruct_2 ????? (sym_eq … eq_fetch_pseudo_instruction))
272      >snd_fetch_pseudo_instruction
273      cases sigma_policy_witness #_ >EQprogram #H cases (H ? ppc_ok) -H
274      #spw1 #_ >spw1 -spw1 @eq_f @eq_f
275      >eq_fetch_pseudo_instruction whd in match instruction_size;
276      normalize nodelta >create_label_cost_refl
277      >fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels
278      [>eq_assembly_1_pseudoinstruction % | skip]
279  | lapply (load_code_memory_ok assembled' ?) [ assumption ]
280    #load_code_memory_ok
281    lapply (fst_snd_assembly_1_pseudoinstruction … eq_assembly_1_pseudoinstruction) #EQlen
282    (* Nice statement here *)
283    cut (∀j. ∀H: j < |assembled|.
284          nth_safe Byte j assembled H =
285          \snd (next (load_code_memory assembled')
286          (bitvector_of_nat 16
287           (nat_of_bitvector …
288            (add … (sigma ppc) (bitvector_of_nat … j))))))
289    [1: #j #H <load_code_memory_ok
290        [ @assembly_ok
291        | cut (0=|assembled'| → False)
292          [ #abs <abs in assembly_ok4; >EQlen #abs'
293            @(absurd ?? (not_le_Sn_O j)) @(transitive_le … H) assumption ] #NOT_EMPTY
294          cases assembly_ok3 -assembly_ok3
295          [2: * #_ #EQ2 >EQ2 @lt_nat_of_bitvector ]
296          #EQlen_assembled' <EQlen_assembled'
297          cases sigma_policy_witness #sigma_zero >EQprogram #sigma_ok
298          cases (sigma_ok … ppc_ok) -sigma_ok >eq_fetch_pseudo_instruction
299          whd in match instruction_size; normalize nodelta
300          >create_label_cost_refl
301          >fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels
302          [>eq_assembly_1_pseudoinstruction |2: skip] #OK >OK <EQlen *
303          [2: * #EQ1 #EQ2 @⊥ <EQ1 in EQlen_assembled';
304              <add_bitvector_of_nat_Sm >add_commutative
305              >bitvector_of_nat_inverse_nat_of_bitvector >OK >EQ2
306              lapply (eq_f … (bitvector_of_nat 16) … EQ2) -EQ2
307              <add_bitvector_of_nat_plus >bitvector_of_nat_inverse_nat_of_bitvector
308              #X >X #Y @NOT_EMPTY <Y >bitvector_of_nat_exp_zero % ]
309          cases (le_to_or_lt_eq … instr_list_ok)
310          [2: #abs @⊥ >abs in EQlen_assembled'; >bitvector_of_nat_exp_zero >sigma_zero
311              assumption ]
312          #instr_list_ok' #NO_OVERFLOW
313          @(lt_to_le_to_lt … (nat_of_bitvector … (add … (sigma ppc) (bitvector_of_nat … (|assembled|)))))
314          [ @lt_to_lt_nat_of_bitvector_add
315            [ @(eq_ind ?? (λp.λ_. |\snd p| < 2^16) ?? eq_assembly_1_pseudoinstruction)
316              / by /
317            | <EQlen assumption
318            | assumption
319            ]
320          | <EQlen <OK
321            cases (monotone_sigma ???? sigma_policy_witness
322             (add … ppc (bitvector_of_nat … 1))
323             (bitvector_of_nat … (|instr_list|)) ??) try assumption
324            [ #H @H
325            |3: >EQprogram >nat_of_bitvector_bitvector_of_nat_inverse
326                try % assumption
327            |4: >nat_of_bitvector_bitvector_of_nat_inverse try assumption
328                >nat_of_bitvector_add <plus_n_Sm <plus_n_O try assumption
329                @(transitive_le … instr_list_ok') @le_S_S assumption
330            | * #EQ1 @⊥ >EQ1 in EQlen_assembled'; assumption ]]]
331    |2:
332      -assembly_ok -load_code_memory_ok generalize in match (sigma ppc); >EQlen -len
333      elim assembled
334      [1:
335        #pc #_ whd <add_zero %
336      | #hd #tl #IH #pc #H %
337         [ lapply (H 0 ?) [ normalize @le_S_S @le_O_n ] whd in ⊢ (??%? → ?); -H #H
338           >H -H whd in ⊢ (??%?); <add_zero //
339         | >(?: add … pc (bitvector_of_nat … (S (|tl|))) = add … (add … pc (bitvector_of_nat … 1)) (bitvector_of_nat … (|tl|)))
340           [2: <add_bitvector_of_nat_Sm @add_associative ]
341           @IH -IH #j #LTj lapply (H (S j) ?) [ @le_S_S @LTj ]
342           <(nth_safe_prepend … [hd] … LTj) #IH >IH <add_bitvector_of_nat_Sm
343           >add_associative % ]]]]
344qed.
345
346(* XXX: should we add that costs = costs'? *)
347lemma fetch_assembly_pseudo2:
348  ∀program.
349  ∀length_proof: |\snd program| ≤ 2^16.
350  ∀sigma.
351  ∀policy.
352  ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
353  ∀ppc.∀ppc_ok.
354  let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
355  let 〈assembled, costs'〉 ≝ pi1 … (assembly program sigma policy) in
356  let code_memory ≝ load_code_memory assembled in
357  let data_labels ≝ construct_datalabels (\fst program) in
358  let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in
359  let lookup_datalabels ≝ λx. lookup_def ? ? data_labels x (zero ?) in
360  let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc ppc_ok in
361  let instructions ≝ expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi in
362    fetch_many code_memory (sigma newppc) (sigma ppc) instructions.
363  * #preamble #instr_list #length_proof #sigma #policy #sigma_policy_specification_witness #ppc #ppc_ok
364  @pair_elim #labels #costs #create_label_map_refl
365  @pair_elim #assembled #costs' #assembled_refl
366  letin code_memory ≝ (load_code_memory ?)
367  letin data_labels ≝ (construct_datalabels ?)
368  letin lookup_labels ≝ (λx. ?)
369  letin lookup_datalabels ≝ (λx. ?)
370  @pair_elim #pi #newppc #fetch_pseudo_refl
371  lapply (assembly_ok 〈preamble, instr_list〉 ? sigma policy sigma_policy_specification_witness assembled costs')
372  normalize nodelta try assumption
373  >create_label_map_refl in ⊢ (match % with [_ ⇒ ?] → ?); #H
374  lapply (H (sym_eq … assembled_refl)) -H
375  lapply (refl … (assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi))
376  cases (assembly_1_pseudoinstruction ??????) in ⊢ (???% → ?);
377  #len #assembledi #EQ4 #H
378  lapply (H ppc) >fetch_pseudo_refl #H
379  lapply (fetch_assembly_pseudo 〈preamble,instr_list〉 sigma policy)
380  >create_label_map_refl #X lapply (X ppc ppc_ok (load_code_memory assembled)) -X
381  >EQ4 #H1 cases (H ppc_ok)
382  #H2 #H3 >H3 normalize nodelta in H1; normalize nodelta
383  >fetch_pseudo_refl in H1; #assm @assm assumption
384qed.
385
386(* XXX: changed this type.  Bool specifies whether byte is first or second
387        component of an address, and the Word is the pseudoaddress that it
388        corresponds to.  Second component is the same principle for the accumulator
389        A.
390*)
391definition internal_pseudo_address_map ≝ list ((BitVector 8) × (bool × Word)) × (option (bool × Word)).
392
393include alias "ASM/BitVectorTrie.ma".
394 
395include "common/AssocList.ma".
396
397axiom low_internal_ram_of_pseudo_low_internal_ram:
398 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7.
399
400axiom high_internal_ram_of_pseudo_high_internal_ram:
401 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7.
402
403axiom low_internal_ram_of_pseudo_internal_ram_hit:
404 ∀M:internal_pseudo_address_map.∀cm.∀s:PseudoStatus cm.∀sigma:Word → Word × bool.∀high: bool. ∀points_to: Word. ∀addr:BitVector 7.
405  assoc_list_lookup ?? (false:::addr) (eq_bv 8) (\fst M) = Some … (〈high, points_to〉)  →
406   let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in
407   let pbl ≝ lookup ? 7 addr (low_internal_ram … s) (zero 8) in
408   let bl ≝ lookup ? 7 addr ram (zero 8) in
409   let 〈lower, higher〉 ≝ vsplit ? 8 8 points_to in
410   let 〈plower, phigher〉 ≝ vsplit ? 8 8 (\fst (sigma points_to)) in
411     if high then
412       (pbl = higher) ∧ (bl = phigher)
413     else
414       (pbl = lower) ∧ (bl = plower).
415
416(* changed from add to sub *)
417axiom low_internal_ram_of_pseudo_internal_ram_miss:
418 ∀T.∀M:internal_pseudo_address_map.∀cm.∀s:PreStatus T cm.∀addr:BitVector 7.
419  let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in
420    assoc_list_exists ?? (false:::addr) (eq_bv 8) (\fst M) = false →
421      lookup ? 7 addr ram (zero ?) = lookup ? 7 addr (low_internal_ram … s) (zero ?).
422
423definition addressing_mode_ok ≝
424 λT.λM:internal_pseudo_address_map.λcm.λs:PreStatus T cm.
425  λaddr:addressing_mode.
426   match addr with
427    [ DIRECT d ⇒
428       ¬(assoc_list_exists ?? d (eq_bv 8) (\fst M)) ∧
429       ¬(assoc_list_exists ?? (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) (eq_bv 8) (\fst M))
430    | INDIRECT i ⇒
431       let d ≝ get_register … s [[false;false;i]] in
432       ¬(assoc_list_exists ?? d (eq_bv 8) (\fst M)) ∧
433       ¬(assoc_list_exists ?? (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) (eq_bv 8) (\fst M))
434    | EXT_INDIRECT _ ⇒ true
435    | REGISTER _ ⇒ true
436    | ACC_A ⇒ match \snd M with [ None ⇒ true | _ ⇒ false ]
437    | ACC_B ⇒ true
438    | DPTR ⇒ true
439    | DATA _ ⇒ true
440    | DATA16 _ ⇒ true
441    | ACC_DPTR ⇒ true
442    | ACC_PC ⇒ true
443    | EXT_INDIRECT_DPTR ⇒ true
444    | INDIRECT_DPTR ⇒ true
445    | CARRY ⇒ true
446    | BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *)
447    | N_BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *)
448    | RELATIVE _ ⇒ true
449    | ADDR11 _ ⇒ true
450    | ADDR16 _ ⇒ true ].
451   
452definition next_internal_pseudo_address_map0 ≝
453  λT.
454  λcm:T.
455  λaddr_of: Identifier → PreStatus T cm → Word.
456  λfetched.
457  λM: internal_pseudo_address_map.
458  λs: PreStatus T cm.
459   match fetched with
460    [ Comment _ ⇒ Some ? M
461    | Cost _ ⇒ Some … M
462    | Jmp _ ⇒ Some … M
463    | Call a ⇒
464      let a' ≝ addr_of a s in
465      let 〈callM, accM〉 ≝ M in
466         Some … 〈〈(add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)), 〈false, a'〉〉::
467                 〈(add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)), 〈true, a'〉〉::callM, accM〉
468    | Mov _ _ ⇒ Some … M
469    | Instruction instr ⇒
470       match instr with
471        [ ADD addr1 addr2 ⇒
472           if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
473            Some ? M
474           else
475            None ?
476        | ADDC addr1 addr2 ⇒
477           if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
478            Some ? M
479           else
480            None ?
481        | SUBB addr1 addr2 ⇒
482           if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
483            Some ? M
484           else
485            None ?       
486        | _ ⇒ (* TO BE COMPLETED *) Some ? M ]].
487
488definition next_internal_pseudo_address_map ≝
489 λM:internal_pseudo_address_map.
490 λcm.
491 λaddr_of.
492 λs:PseudoStatus cm.
493 λppc_ok.
494    next_internal_pseudo_address_map0 ? cm addr_of
495     (\fst (fetch_pseudo_instruction (\snd cm) (program_counter … s) ppc_ok)) M s.
496
497definition code_memory_of_pseudo_assembly_program:
498    ∀pap:pseudo_assembly_program.
499      (Word → Word) → (Word → bool) → BitVectorTrie Byte 16 ≝
500  λpap.
501  λsigma.
502  λpolicy.
503    let p ≝ pi1 … (assembly pap sigma policy) in
504      load_code_memory (\fst p).
505
506definition sfr_8051_of_pseudo_sfr_8051 ≝
507  λM: internal_pseudo_address_map.
508  λsfrs: Vector Byte 19.
509  λsigma: Word → Word.
510    match \snd M with
511    [ None ⇒ sfrs
512    | Some s ⇒
513      let 〈high, address〉 ≝ s in
514      let index ≝ sfr_8051_index SFR_ACC_A in
515      let 〈upper, lower〉 ≝ vsplit ? 8 8 (sigma address) in
516        if high then
517          set_index Byte 19 sfrs index upper ?
518        else
519          set_index Byte 19 sfrs index lower ?
520    ].
521  //
522qed.
523
524definition status_of_pseudo_status:
525    internal_pseudo_address_map → ∀pap. ∀ps: PseudoStatus pap.
526      ∀sigma: Word → Word. ∀policy: Word → bool.
527        Status (code_memory_of_pseudo_assembly_program pap sigma policy) ≝
528  λM.
529  λpap.
530  λps.
531  λsigma.
532  λpolicy.
533  let cm ≝ code_memory_of_pseudo_assembly_program … sigma policy in
534  let pc ≝ sigma (program_counter … ps) in
535  let lir ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps) in
536  let hir ≝ high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … ps) in
537     mk_PreStatus (BitVectorTrie Byte 16)
538      cm
539      lir
540      hir
541      (external_ram … ps)
542      pc
543      (sfr_8051_of_pseudo_sfr_8051 M (special_function_registers_8051 … ps) sigma)
544      (special_function_registers_8052 … ps)
545      (p1_latch … ps)
546      (p3_latch … ps)
547      (clock … ps).
548
549(*
550definition write_at_stack_pointer':
551 ∀M. ∀ps: PreStatus M. Byte → Σps':PreStatus M.(code_memory … ps = code_memory … ps') ≝
552  λM: Type[0].
553  λs: PreStatus M.
554  λv: Byte.
555    let 〈 nu, nl 〉 ≝ vsplit … 4 4 (get_8051_sfr ? s SFR_SP) in
556    let bit_zero ≝ get_index_v… nu O ? in
557    let bit_1 ≝ get_index_v… nu 1 ? in
558    let bit_2 ≝ get_index_v… nu 2 ? in
559    let bit_3 ≝ get_index_v… nu 3 ? in
560      if bit_zero then
561        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
562                              v (low_internal_ram ? s) in
563          set_low_internal_ram ? s memory
564      else
565        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
566                              v (high_internal_ram ? s) in
567          set_high_internal_ram ? s memory.
568  [ cases l0 %
569  |2,3,4,5: normalize repeat (@ le_S_S) @ le_O_n ]
570qed.
571
572definition execute_1_pseudo_instruction': (Word → nat) → ∀ps:PseudoStatus.
573 Σps':PseudoStatus.(code_memory … ps = code_memory … ps')
574
575  λticks_of.
576  λs.
577  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
578  let ticks ≝ ticks_of (program_counter ? s) in
579  let s ≝ set_clock ? s (clock ? s + ticks) in
580  let s ≝ set_program_counter ? s pc in
581    match instr with
582    [ Instruction instr ⇒
583       execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s
584    | Comment cmt ⇒ s
585    | Cost cst ⇒ s
586    | Jmp jmp ⇒ set_program_counter ? s (address_of_word_labels s jmp)
587    | Call call ⇒
588      let a ≝ address_of_word_labels s call in
589      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
590      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
591      let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 (program_counter ? s) in
592      let s ≝ write_at_stack_pointer' ? s pc_bl in
593      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
594      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
595      let s ≝ write_at_stack_pointer' ? s pc_bu in
596        set_program_counter ? s a
597    | Mov dptr ident ⇒
598       set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr
599    ].
600 [
601 |2,3,4: %
602 | <(sig2 … l7) whd in ⊢ (??? (??%)) <(sig2 … l5) %
603 |
604 | %
605 ]
606 cases not_implemented
607qed.
608*)
609
610(*
611lemma execute_code_memory_unchanged:
612 ∀ticks_of,ps. code_memory ? ps = code_memory ? (execute_1_pseudo_instruction ticks_of ps).
613 #ticks #ps whd in ⊢ (??? (??%))
614 cases (fetch_pseudo_instruction (\snd (code_memory pseudo_assembly_program ps))
615  (program_counter pseudo_assembly_program ps)) #instr #pc
616 whd in ⊢ (??? (??%)) cases instr
617  [ #pre cases pre
618     [ #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
619       cases (vsplit ????) #z1 #z2 %
620     | #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
621       cases (vsplit ????) #z1 #z2 %
622     | #a1 #a2 whd in ⊢ (??? (??%)) cases (sub_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
623       cases (vsplit ????) #z1 #z2 %
624     | #a1 whd in ⊢ (??? (??%)) cases a1 #x #H whd in ⊢ (??? (??%)) cases x
625       [ #x1 whd in ⊢ (??? (??%))
626     | *: cases not_implemented
627     ]
628  | #comment %
629  | #cost %
630  | #label %
631  | #label whd in ⊢ (??? (??%)) cases (half_add ???) #x1 #x2 whd in ⊢ (??? (??%))
632    cases (vsplit ????) #y1 #y2 whd in ⊢ (??? (??%)) cases (half_add ???) #z1 #z2
633    whd in ⊢ (??? (??%)) whd in ⊢ (??? (??%)) cases (vsplit ????) #w1 #w2
634    whd in ⊢ (??? (??%)) cases (get_index_v bool ????) whd in ⊢ (??? (??%))
635    (* CSC: ??? *)
636  | #dptr #label (* CSC: ??? *)
637  ]
638  cases not_implemented
639qed.
640*)
641
642(* XXX: check values returned for conditional jumps below! *)
643definition ticks_of0:
644    ∀p:pseudo_assembly_program.
645      (Word → Word) → (Word → bool) → Word → pseudo_instruction → nat × nat ≝
646  λprogram: pseudo_assembly_program.
647  λsigma.
648  λpolicy.
649  λppc: Word.
650  λfetched.
651    match fetched with
652    [ Instruction instr ⇒
653      match instr with
654      [ JC lbl ⇒
655        if policy ppc then
656          〈4, 4〉
657        else
658          〈2, 2〉
659      | JNC lbl ⇒
660        if policy ppc then
661          〈4, 4〉
662        else
663          〈2, 2〉
664      | JB bit lbl ⇒
665        if policy ppc then
666          〈4, 4〉
667        else
668          〈2, 2〉
669      | JNB bit lbl ⇒
670        if policy ppc then
671          〈4, 4〉
672        else
673          〈2, 2〉
674      | JBC bit lbl ⇒
675        if policy ppc then
676          〈4, 4〉
677        else
678          〈2, 2〉
679      | JZ lbl ⇒
680        if policy ppc then
681          〈4, 4〉
682        else
683          〈2, 2〉
684      | JNZ lbl ⇒
685        if policy ppc then
686          〈4, 4〉
687        else
688          〈2, 2〉
689      | CJNE arg lbl ⇒
690        if policy ppc then
691          〈4, 4〉
692        else
693          〈2, 2〉
694      | DJNZ arg lbl ⇒
695        if policy ppc then
696          〈4, 4〉
697        else
698          〈2, 2〉
699      | ADD arg1 arg2 ⇒
700        let ticks ≝ ticks_of_instruction (ADD ? arg1 arg2) in
701         〈ticks, ticks〉
702      | ADDC arg1 arg2 ⇒
703        let ticks ≝ ticks_of_instruction (ADDC ? arg1 arg2) in
704         〈ticks, ticks〉
705      | SUBB arg1 arg2 ⇒
706        let ticks ≝ ticks_of_instruction (SUBB ? arg1 arg2) in
707         〈ticks, ticks〉
708      | INC arg ⇒
709        let ticks ≝ ticks_of_instruction (INC ? arg) in
710         〈ticks, ticks〉
711      | DEC arg ⇒
712        let ticks ≝ ticks_of_instruction (DEC ? arg) in
713         〈ticks, ticks〉
714      | MUL arg1 arg2 ⇒
715        let ticks ≝ ticks_of_instruction (MUL ? arg1 arg2) in
716         〈ticks, ticks〉
717      | DIV arg1 arg2 ⇒
718        let ticks ≝ ticks_of_instruction (DIV ? arg1 arg2) in
719         〈ticks, ticks〉
720      | DA arg ⇒
721        let ticks ≝ ticks_of_instruction (DA ? arg) in
722         〈ticks, ticks〉
723      | ANL arg ⇒
724        let ticks ≝ ticks_of_instruction (ANL ? arg) in
725         〈ticks, ticks〉
726      | ORL arg ⇒
727        let ticks ≝ ticks_of_instruction (ORL ? arg) in
728         〈ticks, ticks〉
729      | XRL arg ⇒
730        let ticks ≝ ticks_of_instruction (XRL ? arg) in
731         〈ticks, ticks〉
732      | CLR arg ⇒
733        let ticks ≝ ticks_of_instruction (CLR ? arg) in
734         〈ticks, ticks〉
735      | CPL arg ⇒
736        let ticks ≝ ticks_of_instruction (CPL ? arg) in
737         〈ticks, ticks〉
738      | RL arg ⇒
739        let ticks ≝ ticks_of_instruction (RL ? arg) in
740         〈ticks, ticks〉
741      | RLC arg ⇒
742        let ticks ≝ ticks_of_instruction (RLC ? arg) in
743         〈ticks, ticks〉
744      | RR arg ⇒
745        let ticks ≝ ticks_of_instruction (RR ? arg) in
746         〈ticks, ticks〉
747      | RRC arg ⇒
748        let ticks ≝ ticks_of_instruction (RRC ? arg) in
749         〈ticks, ticks〉
750      | SWAP arg ⇒
751        let ticks ≝ ticks_of_instruction (SWAP ? arg) in
752         〈ticks, ticks〉
753      | MOV arg ⇒
754        let ticks ≝ ticks_of_instruction (MOV ? arg) in
755         〈ticks, ticks〉
756      | MOVX arg ⇒
757        let ticks ≝ ticks_of_instruction (MOVX ? arg) in
758         〈ticks, ticks〉
759      | SETB arg ⇒
760        let ticks ≝ ticks_of_instruction (SETB ? arg) in
761         〈ticks, ticks〉
762      | PUSH arg ⇒
763        let ticks ≝ ticks_of_instruction (PUSH ? arg) in
764         〈ticks, ticks〉
765      | POP arg ⇒
766        let ticks ≝ ticks_of_instruction (POP ? arg) in
767         〈ticks, ticks〉
768      | XCH arg1 arg2 ⇒
769        let ticks ≝ ticks_of_instruction (XCH ? arg1 arg2) in
770         〈ticks, ticks〉
771      | XCHD arg1 arg2 ⇒
772        let ticks ≝ ticks_of_instruction (XCHD ? arg1 arg2) in
773         〈ticks, ticks〉
774      | RET ⇒
775        let ticks ≝ ticks_of_instruction (RET ?) in
776         〈ticks, ticks〉
777      | RETI ⇒
778        let ticks ≝ ticks_of_instruction (RETI ?) in
779         〈ticks, ticks〉
780      | NOP ⇒
781        let ticks ≝ ticks_of_instruction (NOP ?) in
782         〈ticks, ticks〉
783      ]
784    | Comment comment ⇒ 〈0, 0〉
785    | Cost cost ⇒ 〈0, 0〉
786    | Jmp jmp ⇒
787      if policy ppc then
788        〈4, 4〉
789      else
790        〈2, 2〉
791    | Call call ⇒
792      if policy ppc then
793        〈4, 4〉
794      else
795        〈2, 2〉
796    | Mov dptr tgt ⇒ 〈2, 2〉
797    ].
798
799definition ticks_of:
800    ∀p:pseudo_assembly_program.
801      (Word → Word) → (Word → bool) → ∀ppc:Word.
802       nat_of_bitvector … ppc < |\snd p| → nat × nat ≝
803  λprogram: pseudo_assembly_program.
804  λsigma.
805  λpolicy.
806  λppc: Word. λppc_ok.
807    let pseudo ≝ \snd program in
808    let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction pseudo ppc ppc_ok in
809     ticks_of0 program sigma policy ppc fetched.
810
811(*
812lemma blah:
813  ∀m: internal_pseudo_address_map.
814  ∀s: PseudoStatus.
815  ∀arg: Byte.
816  ∀b: bool.
817    addressing_mode_ok m s (DIRECT arg) = true →
818      get_arg_8 ? (set_low_internal_ram ? s (low_internal_ram_of_pseudo_low_internal_ram m (low_internal_ram ? s))) b (DIRECT arg) =
819      get_arg_8 ? s b (DIRECT arg).
820  [2, 3: normalize % ]
821  #m #s #arg #b #hyp
822  whd in ⊢ (??%%)
823  @vsplit_elim''
824  #nu' #nl' #arg_nu_nl_eq
825  normalize nodelta
826  generalize in match (refl ? (get_index_v bool 4 nu' ? ?))
827  cases (get_index_v bool 4 nu' ? ?) in ⊢ (??%? → %)
828  #get_index_v_eq
829  normalize nodelta
830  [2:
831    normalize nodelta
832    @vsplit_elim''
833    #bit_one' #three_bits' #bit_one_three_bit_eq
834    generalize in match (low_internal_ram_of_pseudo_internal_ram_miss m s (three_bits'@@nl'))
835    normalize nodelta
836    generalize in match (refl ? (sub_7_with_carry ? ? ?))
837    cases (sub_7_with_carry ? ? ?) in ⊢ (??%? → %)
838    #Saddr #carr' #Saddr_carr_eq
839    normalize nodelta
840    #carr_hyp'
841    @carr_hyp'
842    [1:
843    |2: whd in hyp:(??%?); generalize in match hyp; -hyp;
844        generalize in match (refl ? (¬(member (BitVector 8) ? arg m)))
845        cases (¬(member (BitVector 8) ? arg m)) in ⊢ (??%? → %)
846        #member_eq
847        normalize nodelta
848        [2: #destr destruct(destr)
849        |1: -carr_hyp';
850            >arg_nu_nl_eq
851            <(vsplit_vector_singleton ? ? nu' ? ? ? bit_one_three_bit_eq)
852            [1: >get_index_v_eq in ⊢ (??%? → ?)
853            |2: @le_S @le_S @le_S @le_n
854            ]
855            cases (member (BitVector 8) ? (\fst ?) ?)
856            [1: #destr normalize in destr; destruct(destr)
857            |2:
858            ]
859        ]
860    |3: >get_index_v_eq in ⊢ (??%?)
861        change in ⊢ (??(???%?)?) with ((? ::: three_bits') @@ nl')
862        >(vsplit_vector_singleton … bit_one_three_bit_eq)
863        <arg_nu_nl_eq
864        whd in hyp:(??%?)
865        cases (member (BitVector 8) (eq_bv 8) arg m) in hyp
866        normalize nodelta [*: #ignore @sym_eq ]
867    ]
868  |
869  ].
870*)
871(*
872map_address0 ... (DIRECT arg) = Some .. →
873  get_arg_8 (map_address0 ... (internal_ram ...) (DIRECT arg) =
874  get_arg_8 (internal_ram ...) (DIRECT arg)
875
876((if addressing_mode_ok M ps ACC_A∧addressing_mode_ok M ps (DIRECT ARG2) 
877                     then Some internal_pseudo_address_map M 
878                     else None internal_pseudo_address_map )
879                    =Some internal_pseudo_address_map M')
880
881axiom low_internal_ram_write_at_stack_pointer:
882 ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma: Word → Word.∀policy: Word → bool.
883 ∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
884  get_8051_sfr T2 cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP →
885  low_internal_ram ? cm2 s2 = low_internal_ram T2 cm3 s3 →
886  sp1 = add ? (get_8051_sfr … cm1 s1 SFR_SP) (bitvector_of_nat 8 1) →
887  sp2 = add ? sp1 (bitvector_of_nat 8 1) →
888  bu@@bl = sigma (pbu@@pbl) →
889   low_internal_ram T1 cm1
890     (write_at_stack_pointer …
891       (set_8051_sfr …
892         (write_at_stack_pointer …
893           (set_8051_sfr …
894             (set_low_internal_ram … s1
895               (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s2)))
896             SFR_SP sp1)
897          bl)
898        SFR_SP sp2)
899      bu)
900   = low_internal_ram_of_pseudo_low_internal_ram (sp1::M)
901      (low_internal_ram …
902       (write_at_stack_pointer …
903         (set_8051_sfr …
904           (write_at_stack_pointer … (set_8051_sfr … s3 SFR_SP sp1) pbl)
905          SFR_SP sp2)
906        pbu)).
907
908lemma high_internal_ram_write_at_stack_pointer:
909 ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma:Word → Word.∀policy: Word → bool.
910 ∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
911  get_8051_sfr T2 cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP →
912  high_internal_ram ?? s2 = high_internal_ram T2 cm3 s3 →
913  sp1 = add ? (get_8051_sfr ? cm1 s1 SFR_SP) (bitvector_of_nat 8 1) →
914  sp2 = add ? sp1 (bitvector_of_nat 8 1) →
915  bu@@bl = sigma (pbu@@pbl) →
916   high_internal_ram T1 cm1
917     (write_at_stack_pointer …
918       (set_8051_sfr …
919         (write_at_stack_pointer …
920           (set_8051_sfr …
921             (set_high_internal_ram … s1
922               (high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … s2)))
923             SFR_SP sp1)
924          bl)
925        SFR_SP sp2)
926      bu)
927   = high_internal_ram_of_pseudo_high_internal_ram (sp1::M)
928      (high_internal_ram …
929       (write_at_stack_pointer …
930         (set_8051_sfr …
931           (write_at_stack_pointer … (set_8051_sfr … s3 SFR_SP sp1) pbl)
932          SFR_SP sp2)
933        pbu)).
934  #T1 #T2 #M #cm1 #s1 #cm2 #s2 #cm3 #s3 #sigma #policy #pbu #pbl #bu #bl #sp1 #sp2
935  #get_8051_sfr_refl #high_internal_ram_refl #sp1_refl #sp2_refl #sigma_refl
936  cases daemon (* XXX: !!! *)
937qed.
938*)
939
940lemma snd_assembly_1_pseudoinstruction_ok:
941  ∀program: pseudo_assembly_program.
942  ∀program_length_proof: |\snd program| ≤ 2^16.
943  ∀sigma: Word → Word.
944  ∀policy: Word → bool.
945  ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
946  ∀ppc: Word.
947  ∀ppc_in_bounds: nat_of_bitvector 16 ppc < |\snd program|.
948  ∀pi.
949  ∀lookup_labels.
950  ∀lookup_datalabels.
951    let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
952    lookup_labels = (λx. bitvector_of_nat 16 (lookup_def … labels x 0)) →
953    lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
954    \fst (fetch_pseudo_instruction (\snd program) ppc ppc_in_bounds) = pi →
955    let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels sigma policy (*(sigma ppc)*) ppc lookup_datalabels pi) in
956      sigma (add … ppc (bitvector_of_nat ? 1)) = add … (sigma ppc) (bitvector_of_nat ? len).
957  #program #program_length_proof #sigma #policy #sigma_policy_specification_witness #ppc #ppc_in_bounds #pi
958  #lookup_labels #lookup_datalabels
959  @pair_elim #labels #costs #create_label_cost_map_refl
960  #lookup_labels_refl #lookup_datalabels_refl #fetch_pseudo_refl
961  normalize nodelta
962  generalize in match fetch_pseudo_refl; -fetch_pseudo_refl
963  #fetch_pseudo_refl
964  letin assembled ≝ (\fst (pi1 … (assembly program sigma policy)))
965  letin costs ≝ (\snd (pi1 … (assembly program sigma policy)))
966  lapply (assembly_ok program program_length_proof sigma policy sigma_policy_specification_witness assembled costs)
967  @pair_elim #preamble #instr_list #program_refl
968  lapply create_label_cost_map_refl; -create_label_cost_map_refl
969  >program_refl in ⊢ (% → ?); #create_label_cost_map_refl
970  >create_label_cost_map_refl
971  <eq_pair_fst_snd #H lapply (H (refl …)) -H #H
972  lapply (H ppc ppc_in_bounds) -H
973  @pair_elim #pi' #newppc #fetch_pseudo_refl'
974  @pair_elim #len #assembled #assembly1_refl #H
975  cases H
976  #encoding_check_assm #sigma_newppc_refl
977  >fetch_pseudo_refl' in fetch_pseudo_refl; #pi_refl'
978  >pi_refl' in assembly1_refl; #assembly1_refl
979  >lookup_labels_refl >lookup_datalabels_refl
980  >program_refl normalize nodelta
981  >assembly1_refl
982  <sigma_newppc_refl
983  generalize in match fetch_pseudo_refl';
984  whd in match (fetch_pseudo_instruction ???);
985  @pair_elim #lbl #instr #nth_refl normalize nodelta
986  #G cases (pair_destruct_right ?????? G) %
987qed.
988
989(* To be moved in ProofStatus *)
990lemma program_counter_set_program_counter:
991  ∀T.
992  ∀cm.
993  ∀s.
994  ∀x.
995    program_counter T cm (set_program_counter T cm s x) = x.
996  //
997qed.
Note: See TracBrowser for help on using the repository browser.