source: src/ASM/CodeMemory.ma @ 2771

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

WARNING: BIG commit, which pushes code_size_opt check into LIN/LINToASM.ma
following CSC's comment on my previous partial commit
plus rolls all the miscellaneous code motion into the rest of the repo.

suggest REBUILD compiler.ma/correctness.ma from scratch.

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