source: src/ASM/CodeMemory.ma @ 2750

Last change on this file since 2750 was 2750, checked in by mckinna, 7 years ago

Miscellany on 216 bounds, memory, lemmas+definitions.

Completes compiler.ma; offers opportunity to refactor ASM/*.ma.

File size: 8.2 KB
Line 
1
2include "ASM/BitVectorTrie.ma".
3include "ASM/Arithmetic.ma".
4(*include "ASM/UtilBranch.ma". *)
5
6include alias "arithmetics/nat.ma".
7
8(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
9(* Program Counters & Object Code: BitVectors, Nats  and Lists of Bytes       *)
10(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
11
12(* from Fetch.ma *)
13definition bitvector_max_nat ≝ λlength: nat. 2^length.
14
15definition size_ok ≝
16  λn.λsize. size ≤ bitvector_max_nat n.
17
18lemma size_ok_mono :
19  ∀n. ∀s,s'. s' ≤ s → size_ok n s -> size_ok n s'.
20  #n #s #s' #mono #ok @(transitive_le … ok) //
21qed.
22
23lemma size_okS :
24  ∀n. ∀s. size_ok n (S s) → size_ok n s.
25  #n #s #ok @size_ok_mono //
26qed.
27
28lemma size_okS' :
29  ∀n. ∀s. size_ok n (s+1) → size_ok n s.
30  #n #s #ok @size_ok_mono //
31qed.
32
33definition address_ok ≝
34  λn.λaddr. size_ok n (S addr).
35
36lemma size_okS_to_address_ok :
37  ∀n. ∀s. size_ok n (S s) → address_ok n s.
38  #n #s #ok assumption.
39qed.
40
41lemma address_ok_to_size_okS :
42  ∀n. ∀pc. address_ok n pc → size_ok n (S pc).
43  #n #pc #ok assumption.
44qed.
45
46lemma size_ok_neq_to_address_ok :
47  ∀n. ∀s. size_ok n s → s ≠ bitvector_max_nat n → address_ok n s.
48  #n #s #s_ok #s_neq
49  @not_eq_to_le_to_lt assumption
50qed.
51
52lemma address_ok_mono :
53  ∀n. ∀pc,pc'. pc' ≤ pc → address_ok n pc -> address_ok n pc'.
54  #n #pc #pc' #mono #ok
55  @size_okS_to_address_ok
56  @(size_ok_mono … (le_S_S …))
57  assumption
58qed.
59
60lemma address_okS :
61  ∀n. ∀pc. address_ok n (S pc) → address_ok n pc.
62  #n #pc #ok @address_ok_mono //
63qed.
64
65lemma address_okS' :
66  ∀n. ∀pc. address_ok n (pc+1) → address_ok n pc.
67  #n #pc #ok @address_ok_mono //
68qed.
69
70definition addrS : ∀n. BitVector n → BitVector n ≝ (* can overflow back to 0 *)
71  λn.λpc. add n pc (bitvector_of_nat n 1).
72 
73lemma addrS_is_Saddr : ∀n. ∀pc.
74  let npcS ≝ S (nat_of_bitvector n pc) in
75    address_ok n npcS →
76      nat_of_bitvector ? (addrS ? pc) = npcS.
77  #n #pc #pcS_ok cases daemon
78  (* XXX: needs UtilBranch.ma; needs re-proving!
79  >succ_nat_of_bitvector_half_add_1
80  [2:
81    @le_plus_to_minus_r
82    change with (S ? ≤ ?) <plus_n_Sm <plus_n_O assumption
83  |1: cases daemon
84  ] *)
85qed.
86
87lemma addrS_useful : ∀n. ∀pc.
88  let npcS ≝ S (nat_of_bitvector n pc) in
89    ∀m. plus npcS (S m) = bitvector_max_nat n → 
90      nat_of_bitvector ? (addrS ? pc) = npcS.
91#n #pc #offset #npcS_ok
92@addrS_is_Saddr //
93qed.
94
95lemma addr_useful : ∀n. ∀pc.
96  let npc ≝ nat_of_bitvector n pc in
97    ∀k,m. plus npc m = bitvector_max_nat n →
98      k < m → address_ok n (npc + k).
99#n #pc #k #m #max #lt change with (? < ?)
100<max @monotonic_lt_plus_r assumption
101qed.   
102
103lemma addr_max : ∀n. ∀pc.
104  let npc ≝ nat_of_bitvector n pc in
105    address_ok n npc ->  address_ok n (S npc) ∨ S npc = bitvector_max_nat n.
106#n #pc #ok @(le_to_or_lt_eq … (lt_nat_of_bitvector … pc))
107qed.   
108
109lemma addr_overflow_offset : ∀n.∀pc.
110  let npc ≝ nat_of_bitvector n pc in
111    ∀m. npc + m = bitvector_max_nat n → add n pc (bitvector_of_nat n m) = (zero n).
112  #n #pc #m #eq <(add_overflow … eq) >bitvector_of_nat_inverse_nat_of_bitvector //
113qed.
114
115lemma addrS_overflow : ∀n. ∀pc.
116  let npc ≝ nat_of_bitvector n pc in
117    S npc = bitvector_max_nat n → addrS n pc = (zero n).
118#n #pc #max change with (add ? ? ? = ?)
119@addr_overflow_offset >commutative_plus assumption
120qed.
121
122(* now we fix the magic number 16 *)
123
124definition ADDRESS_WIDTH ≝ 16.
125
126definition PC  ≝ BitVector ADDRESS_WIDTH.
127
128definition pc0 : PC ≝ zero ?.
129
130definition nat_of_PC : PC → nat ≝ nat_of_bitvector ?.
131
132definition PC_of_nat : nat → PC ≝ bitvector_of_nat ?.
133
134definition pcS : PC → PC ≝ addrS ?.
135
136definition max_program_size ≝ bitvector_max_nat ADDRESS_WIDTH.
137
138definition program_size_ok ≝ size_ok ADDRESS_WIDTH.
139
140definition program_size_ok_mono ≝ size_ok_mono ADDRESS_WIDTH.
141
142definition program_size_okS_to_program_counter_ok ≝ size_okS_to_address_ok ADDRESS_WIDTH. 
143
144definition program_size_okS ≝ size_okS ADDRESS_WIDTH.
145
146definition program_size_okS' ≝ size_okS' ADDRESS_WIDTH.
147
148definition program_counter_ok ≝ address_ok ADDRESS_WIDTH.
149
150definition program_counter_ok_mono ≝ address_ok_mono ADDRESS_WIDTH.
151
152definition program_counter_okS ≝ address_okS ADDRESS_WIDTH.
153
154definition program_counter_okS' ≝ address_okS' ADDRESS_WIDTH.
155
156definition program_size_ok_neq_to_program_counter_ok:
157  ∀s. program_size_ok s → s ≠ max_program_size → program_counter_ok s ≝
158  size_ok_neq_to_address_ok ?.
159
160lemma nat_of_PC_inverse_PC_of_nat :
161  ∀n. program_counter_ok n → 
162    nat_of_PC (PC_of_nat n) = n.
163  #n #n_ok @nat_of_bitvector_bitvector_of_nat_inverse assumption
164qed.
165
166lemma PC_of_nat_inverse_nat_of_PC :
167  ∀pc. PC_of_nat (nat_of_PC pc) = pc.
168  #pc @bitvector_of_nat_inverse_nat_of_bitvector
169qed.
170
171lemma nat_of_PC_offset :  ∀n.∀pc: PC.
172  program_counter_ok (n + nat_of_PC pc) → 
173    nat_of_PC (add … (PC_of_nat n) pc) = n + nat_of_PC pc.
174  #n #pc #n_pc_ok
175  cut (program_counter_ok n)
176    [@program_counter_ok_mono //]
177  #n_ok change with (nat_of_bitvector … (add ? ? ?) = ?)
178  >nat_of_bitvector_add
179    [1: change with (((nat_of_PC ?) + (nat_of_PC ?)) = ?)
180    |2: change with (program_counter_ok ((nat_of_PC ?) + (nat_of_PC ?)))
181    ]
182  >nat_of_PC_inverse_PC_of_nat //
183qed.
184
185lemma nat_of_PC_offset' :  ∀n.∀pc: PC.
186  program_counter_ok (nat_of_PC pc + n) → 
187    nat_of_PC (add … pc (PC_of_nat n)) = nat_of_PC pc + n.
188  #n #pc >commutative_plus >add_commutative @nat_of_PC_offset
189qed.
190
191definition pcS_useful : ∀pc.
192  let npcS ≝ S (nat_of_PC pc) in
193    ∀m. plus npcS (S m) = max_program_size → 
194      nat_of_PC (pcS pc) = npcS ≝
195      addrS_useful ?.
196
197lemma pc_useful : ∀pc.
198  let npc ≝ nat_of_PC pc in
199    ∀k,m. plus npc k = max_program_size →
200      m < k → address_ok ? (npc + m) ≝
201  λpc.λk,m.λEQ.λLT.(addr_useful … EQ LT).   
202
203definition pcS_is_Spc : ∀pc: PC.
204  let npcS ≝ S (nat_of_PC pc) in
205    address_ok ? npcS →
206      nat_of_PC (pcS pc) = npcS ≝
207      addrS_is_Saddr ?.
208     
209definition pc_max : ∀pc.
210  let npc ≝ nat_of_PC pc in
211    program_counter_ok npc ->
212      program_counter_ok (S npc) ∨ S npc = max_program_size ≝
213  addr_max ?.
214 
215definition pcS_overflow : ∀pc.
216  let npc ≝ nat_of_PC pc in
217    S npc = max_program_size -> pcS pc = pc0 ≝ addrS_overflow ?. 
218
219definition pc_overflow_offset : ∀m.∀pc.
220  let npc ≝ nat_of_PC pc in
221    npc + m = max_program_size -> add ? pc (PC_of_nat m) = pc0.
222  #m #pc #max @addr_overflow_offset assumption
223qed.
224
225(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
226(* Memory: one of two distinguished instances of BitVectorTrie.               *)
227(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
228
229definition byte0 : Byte ≝ zero ?.
230
231definition RAM ≝ BitVectorTrie Byte. 
232
233definition ram0 : ∀n. RAM n ≝   
234  λn. Stub ….
235
236definition memory_lookup : ∀n. BitVector n → RAM n → Byte ≝   
237  λn,addr,mem. lookup ? n addr mem byte0.
238
239(* instances *)
240
241definition code_memory ≝ RAM ADDRESS_WIDTH.
242
243definition code_memory0 : code_memory ≝ ram0 ?.
244
245definition code_memory_lookup : PC → code_memory → Byte ≝ memory_lookup ?.
246
247(* ***** Object-code ***** JHM: push elsewherein ASM/*.ma? *)
248
249definition object_code ≝ list Byte.
250
251inductive nat_bounded : nat → nat → Type[0] ≝
252| nat_ok : ∀n,m:nat. nat_bounded n (n+m)
253| nat_overflow : ∀n,m:nat. nat_bounded (n+S m) n.
254
255let rec nat_bound (n:nat) (m:nat) : nat_bounded n m ≝
256match n return λx. nat_bounded x m with
257[ O ⇒ nat_ok ??
258| S n' ⇒
259    match m return λy. nat_bounded (S n') y with
260    [ O ⇒ nat_overflow O ?
261    | S m' ⇒ match nat_bound n' m' return λx,y.λ_. nat_bounded (S x) (S y) with
262             [ nat_ok x y ⇒ nat_ok ??
263             | nat_overflow x y ⇒ nat_overflow (S x) y
264             ]
265    ]
266].
267
268lemma nat_bound_opt : ∀N,n:nat. option (n ≤ N).
269  #N #n elim (nat_bound n N) -n #n #offset
270  [ @Some //
271  | @None
272  ]
273qed. 
274
275definition program_ok_opt : ∀A. ∀instrs : list A. option (program_size_ok (S(S(|instrs|))))
276  ≝ λA.λinstrs. nat_bound_opt max_program_size (S(S(|instrs|))). (* for Policy.ma etc. *)
277
278
279
280
281
282 
Note: See TracBrowser for help on using the repository browser.