source: src/joint/SemanticUtils.ma @ 2286

Last change on this file since 2286 was 2286, checked in by tranquil, 8 years ago

Big update!

  • merge of all _paolo variants
  • reorganised some depends (in particular, Register and thus back-end laguages no longer have fake ASM dependency)
  • split I8051.ma spawning new BackEndOps?.ma

compiler.ma broken at the moment, but not by these changes as far as I can tell

File size: 5.9 KB
Line 
1include "joint/semantics.ma".
2include alias "common/Identifiers.ma".
3include "utilities/hide.ma".
4include "ASM/BitVectorTrie.ma".
5
6record hw_register_env : Type[0] ≝
7  { reg_env : BitVectorTrie beval 6
8  ; carry_bit : bebit
9  ; other_bit : bebit
10  }.
11
12definition empty_hw_register_env: hw_register_env ≝
13  mk_hw_register_env (Stub …) BBundef BBundef.
14
15include alias "ASM/BitVectorTrie.ma".
16
17definition hwreg_retrieve: hw_register_env → Register → beval ≝
18 λenv,r. lookup … (bitvector_of_register r) (reg_env env) BVundef.
19
20definition hwreg_store: Register → beval → hw_register_env → hw_register_env ≝
21 λr,v,env.mk_hw_register_env (insert … (bitvector_of_register r) v (reg_env env))
22  (carry_bit env) (other_bit env).
23
24definition hwreg_set_carry : bebit → hw_register_env → hw_register_env ≝
25λv,env.mk_hw_register_env (reg_env env) v (other_bit env).
26
27definition hwreg_set_other : bebit → hw_register_env → hw_register_env ≝
28λv,env.mk_hw_register_env (reg_env env) (carry_bit env) v.
29
30
31(*** Store/retrieve on pseudo-registers ***)
32include alias "common/Identifiers.ma".
33
34axiom BadRegister : String.
35
36definition reg_store ≝ λreg,v,locals. update RegisterTag beval locals reg v.
37
38definition reg_retrieve : register_env beval → register → res beval ≝
39 λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup … locals reg).
40
41(*** Store/retrieve on hardware registers ***)
42
43definition init_hw_register_env: xpointer → hw_register_env ≝
44 λsp.
45  let 〈dpl,dph〉 ≝
46    match beval_pair_of_pointer sp return λx.beval_pair_of_pointer sp = x → ? with
47    [ OK p ⇒ λ_.p
48    | _ ⇒ λprf.⊥
49    ] (refl …) in
50  let env ≝ hwreg_store RegisterDPH dph empty_hw_register_env in
51   hwreg_store RegisterDPL dpl env.
52@hide_prf
53normalize in prf; destruct(prf)
54qed.
55
56(******************************** GRAPHS **************************************)
57
58definition bitvector_from_pos :
59  ∀n.Pos → BitVector n ≝
60  λn,p.bitvector_of_Z n (Zpred (pos p)).
61
62definition pos_from_bitvector :
63  ∀n.BitVector n → Pos ≝
64  λn,v.
65  match Zsucc (Z_of_unsigned_bitvector n v)
66  return λx.Zsucc (Z_of_unsigned_bitvector n v) = x → ?
67  with
68  [ OZ ⇒ λprf.⊥
69  | pos x ⇒ λ_. x
70  | neg x ⇒ λprf.⊥
71  ] (refl …).
72@hide_prf
73elim v in prf;
74[2,4: #n * #v #IH [2,4: assumption ]] normalize #ABS destruct(ABS) qed.
75
76lemma pos_pos_from_bitvector :
77  ∀n,bv.pos (pos_from_bitvector n bv) = Zsucc (Z_of_unsigned_bitvector n bv).
78#n #bv elim bv -n
79[ %
80| #n * #bv #IH [ % | @IH ]
81]
82qed.
83
84lemma bitvector_from_pos_from_bitvector :
85  ∀n,bv.bitvector_from_pos n (pos_from_bitvector n bv) = bv.
86#n #bv whd in ⊢ (??%?); >pos_pos_from_bitvector
87>Zpred_Zsucc //
88qed.
89
90lemma divide_elim : ∀P : (natp × natp) → Prop.∀m,n : Pos.
91  (∀q,r.
92    ppos m = natp_plus (natp_times q (ppos n)) r →
93    natp_lt r n →
94    P (〈q,r〉)) →
95  P (divide m n).
96#P #m #n #H
97lapply (refl … (divide m n))
98cases (divide ??) in ⊢ (???%→%);
99#q #r #EQ elim (divide_ok … EQ) -EQ @H
100qed.
101
102lemma lt_divisor_to_eq_mod : ∀p,q : Pos.
103  p < q → \snd (divide p q) = ppos p.
104#p #q #H @divide_elim * [2: #quot ]
105* [2,4: #rest] normalize #EQ destruct(EQ) #_ [2: %]
106@⊥ elim (lt_to_not_le ?? H) #H @H -H -H
107[ @(transitive_le … (quot*q)) ] /2 by /
108qed.
109
110lemma pos_from_bitvector_from_pos :
111  ∀n,p.
112  p ≤ two_power_nat n →
113  pos_from_bitvector n (bitvector_from_pos n p) = p.
114#n #p #H
115cut (pos (pos_from_bitvector n (bitvector_from_pos n p)) = pos p)
116[2: #EQ destruct(EQ) <e0 in ⊢ (???%); % ]
117>pos_pos_from_bitvector
118whd in match (bitvector_from_pos ??);
119>Z_of_unsigned_bitvector_of_Z
120cases p in H ⊢ %;
121[ #_ %
122|*: #p' #H
123  whd in match (Zpred ?);
124  whd in match (Z_two_power_nat ?);
125  whd in ⊢ (??(?%)?);
126  >lt_divisor_to_eq_mod [1,3: normalize nodelta whd in match (Zsucc ?); ]
127  whd
128  <succ_pred_n try assumption % #ABS destruct(ABS)
129]
130qed.
131
132lemma pos_from_bitvector_max : ∀n,bv.
133  pos_from_bitvector n bv ≤ two_power_nat n.
134#n #bv
135change with (pos (pos_from_bitvector n bv) ≤ Z_two_power_nat n)
136>pos_pos_from_bitvector
137@Zlt_to_Zle
138@bv_Z_unsigned_max
139qed.
140
141definition graph_offset_of_label : label → option offset ≝
142  λl.let p ≝ word_of_identifier … l in
143  if leb p (two_power_nat offset_size) then
144    return mk_offset (bitvector_from_pos … p)
145  else
146    None ?.
147
148definition graph_label_of_offset: offset → label ≝
149 λo.an_identifier ? (pos_from_bitvector ? (offv o)).
150
151definition make_sem_graph_params :
152  ∀pars : graph_params.
153  ∀g_pars : more_sem_unserialized_params pars (joint_internal_function pars).
154  sem_params ≝
155  λpars,g_pars.
156  mk_sem_params
157    pars
158    (mk_more_sem_params
159      pars
160      g_pars
161      graph_offset_of_label
162      graph_label_of_offset
163      ??
164    ).
165whd in match graph_label_of_offset;
166whd in match graph_offset_of_label;
167whd in match word_of_identifier;
168normalize nodelta * #x
169@(leb_elim ? (two_power_nat ?)) normalize nodelta
170[ #_ >bitvector_from_pos_from_bitvector %
171| #ABS @⊥ @(absurd ?? ABS) @pos_from_bitvector_max
172| #H whd >(pos_from_bitvector_from_pos … H) %
173| #_ %
174]
175qed.
176
177(******************************** LINEAR **************************************)
178
179definition lin_offset_of_nat : ℕ → option offset ≝
180  λn.
181  if leb (S n) (2^offset_size) then
182    return mk_offset (bitvector_of_nat ? n)
183  else
184    None ?.
185
186definition lin_nat_of_offset : offset → ℕ ≝
187  λo.nat_of_bitvector ? (offv o).
188
189
190definition make_sem_lin_params :
191  ∀pars : lin_params.
192  ∀g_pars : more_sem_unserialized_params pars (joint_internal_function pars).
193  sem_params ≝
194  λpars,g_pars.
195  mk_sem_params
196    pars
197    (mk_more_sem_params
198      pars
199      g_pars
200      lin_offset_of_nat
201      lin_nat_of_offset
202      ??
203    ).
204[ * ] #x
205whd in match lin_offset_of_nat;
206whd in match lin_nat_of_offset;
207normalize nodelta
208@leb_elim normalize nodelta #H
209[ >bitvector_of_nat_inverse_nat_of_bitvector %
210| @⊥ cases H #H @H -H -H //
211| whd >(nat_of_bitvector_bitvector_of_nat_inverse … H) %
212| %
213]
214qed.
Note: See TracBrowser for help on using the repository browser.