source: src/joint/semanticsUtils_paolo.ma @ 2200

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