source: src/joint/semanticsUtils_paolo.ma @ 2214

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