Skip to content

Commit fce230f

Browse files
capt-hbcapt-hb
committed
Add update_vector_subrange BinOp
1 parent a34d530 commit fce230f

File tree

5 files changed

+86
-20
lines changed

5 files changed

+86
-20
lines changed

‎theories/BitvectorBase.v

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -820,6 +820,25 @@ Module bv.
820820
Goal vector_subrange 8 8 (@of_nat 16 256) = one. reflexivity. Abort.
821821
End Extract.
822822

823+
Section Update.
824+
Definition update_vector_subrange {n} (start len : nat)
825+
(p : IsTrue (start + len <=? n)) : bv n -> bv len -> bv n :=
826+
match leview (start + len) n in LeView _ sl return bv sl -> bv len -> bv sl with
827+
| is_le k =>
828+
fun bits upd =>
829+
let (xs, rest1) := appView (start + len) k bits in
830+
let (rest2, _) := appView start len xs in
831+
app (app rest2 upd) rest1
832+
end.
833+
#[global] Arguments update_vector_subrange {n} _ _ {_} _ _.
834+
835+
Goal update_vector_subrange 0 1 (@of_nat 2 0) (of_nat 1) = of_nat 1. reflexivity. Abort.
836+
Goal update_vector_subrange 0 4 (@of_nat 4 0) (of_nat 15) = of_nat 15. reflexivity. Abort.
837+
Goal update_vector_subrange 0 4 (@of_nat 8 15) (of_nat 0) = of_nat 0. reflexivity. Abort.
838+
Goal update_vector_subrange 0 4 (@of_nat 8 255) (of_nat 0) = of_nat 240. reflexivity. Abort.
839+
Goal update_vector_subrange 4 4 (@of_nat 8 255) (of_nat 0) = of_nat 15. reflexivity. Abort.
840+
End Update.
841+
823842
Section Shift.
824843
Definition shiftr {m n} (x : bv m) (y : bv n) : bv m :=
825844
of_Z (Z.shiftr (unsigned x) (unsigned y)).

‎theories/Prelude.v

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -82,6 +82,22 @@ Section Equality.
8282
right (fun e => p (f_equal (@pr1 _ (fun _ => _)) (inj e)))
8383
end.
8484

85+
Definition f_equal3_dec {A1 A2 A3 B : Type} (f : A1 -> A2 -> A3 -> B) {x1 y1 : A1} {x2 y2 : A2} {x3 y3 : A3}
86+
(inj : f x1 x2 x3 = f y1 y2 y3 -> @sigmaI _ _ (@sigmaI _ _ x1 x2) x3 = @sigmaI _ _ (@sigmaI _ _ y1 y2) y3)
87+
(hyp1 : dec_eq x1 y1) (hyp2 : dec_eq x2 y2) (hyp3 : dec_eq x3 y3) :
88+
dec_eq (f x1 x2 x3) (f y1 y2 y3) :=
89+
match hyp1 , hyp2 , hyp3 with
90+
| left p , left q , left r => left (eq_trans
91+
(f_equal2 (f x1) q r)
92+
(f_equal (fun x => f x y2 y3) p))
93+
| _ , right q , _ =>
94+
right (fun e => q (f_equal (fun s => @pr2 _ (fun _ => _) (@pr1 _ (fun _ => _) s)) (inj e)))
95+
| right p , _ , _ =>
96+
right (fun e => p (f_equal (fun s => @pr1 _ (fun _ => _) (@pr1 _ (fun _ => _) s)) (inj e)))
97+
| _ , _ , right r =>
98+
right (fun e => r (f_equal (@pr2 _ (fun _ => _)) (inj e)))
99+
end.
100+
85101
Local Set Transparent Obligations.
86102

87103
#[export] Instance Z_eqdec : EqDec Z := Z.eq_dec.

‎theories/Symbolic/PartialEvaluation.v

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -227,6 +227,7 @@ Module Type PartialEvaluationOn
227227
(fun n m e1 e2 => Term_bv_Quote_def (term_binop bop.shiftl e1 e2))
228228
(fun n1 n2 e1 e2 => Term_bv_Quote_def (term_binop bop.bvapp e1 e2))
229229
(fun n e1 e2 => Term_bv_Quote_def (term_binop bop.bvcons e1 e2))
230+
(fun n s l pf e1 e2 => Term_bv_Quote_def (term_binop (bop.update_vector_subrange s l) e1 e2))
230231
(fun n e => Term_bv_Quote_def (term_unop uop.bvnot e))
231232
(fun n e => Term_bv_Quote_def (term_unop uop.negate e))
232233
(fun n m pf e => Term_bv_Quote_def (term_unop uop.sext e))

‎theories/Syntax/BinOps.v

Lines changed: 46 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -29,6 +29,7 @@
2929
From Coq Require Import
3030
Bool.Bool
3131
Strings.String
32+
Arith.PeanoNat
3233
ZArith.BinInt.
3334
From Equations Require Import
3435
Equations.
@@ -80,6 +81,7 @@ Module bop.
8081
| bvxor {n} : BinOp (bvec n) (bvec n) (bvec n)
8182
| bvapp {m n} : BinOp (bvec m) (bvec n) (bvec (m + n))
8283
| bvcons {m} : BinOp (bool) (bvec m) (bvec (S m))
84+
| update_vector_subrange {n} (s l : nat) {p : IsTrue (s + l <=? n)} : BinOp (bvec n) (bvec l) (bvec n)
8385
| relop {σ} (r : RelOp σ) : BinOp σ σ bool
8486
.
8587
Set Transparent Obligations.
@@ -153,6 +155,22 @@ Module bop.
153155
n (noConfusion_inv e))
154156
end.
155157

158+
Obligation Tactic := cbn; intros;
159+
try solve
160+
[let e := fresh in intro e; depelim e; try easy;
161+
try progress cbn in * |-; congruence
162+
|subst; repeat f_equal; apply IsTrue.proof_irrelevance
163+
].
164+
165+
#[derive(equations=no)] Equations update_vector_subrange_eq_dec (n1 n2 s1 s2 l1 l2 : nat) (p1 : IsTrue (s1 + l1 <=? n1)) (p2 : IsTrue (s2 + l2 <=? n2)) :
166+
dec_eq (A := BinOpTel) ((bvec n1, bvec l1, bvec n1),update_vector_subrange s1 l1) ((bvec n2, bvec l2, bvec n2),update_vector_subrange s2 l2) :=
167+
| n1 | n2 | s1 | s2 | l1 | l2 | p1 | p2 with eq_dec n1 n2, eq_dec s1 s2, eq_dec l1 l2 => {
168+
| left _ | left _ | left _ => left _
169+
| right _ | _ | _ => right _
170+
| _ | right _ | _ => right _
171+
| _ | _ | right _ => right _
172+
}.
173+
156174
Definition binoptel_eq_dec {σ1 σ2 σ3 τ1 τ2 τ3 : Ty}
157175
(op1 : BinOp σ1 σ2 σ3) (op2 : BinOp τ1 τ2 τ3) :
158176
dec_eq (A := BinOpTel) ((σ1,σ2,σ3),op1) ((τ1,τ2,τ3),op2) :=
@@ -206,6 +224,13 @@ Module bop.
206224
f_equal_dec
207225
(fun n => ((bool, bvec n, bvec (S n)), bvcons))
208226
(ninv _ _) (eq_dec m n)
227+
| @update_vector_subrange n1 s1 l1 p1, @update_vector_subrange n2 s2 l2 p2 =>
228+
update_vector_subrange_eq_dec n1 n2 s1 s2 l1 l2 p1 p2
229+
(* f_equal3_dec
230+
(fun n s l =>
231+
((bvec n, bvec l, bvec n), @update_vector_subrange n s l _))
232+
(ninv ((bvec n1, bvec l1, bvec n1), @update_vector_subrange n1 s1 l1 p1) ((bvec n2, bvec l2, bvec n2), @update_vector_subrange n2 s2 l2 p2))
233+
(eq_dec n1 n2) (eq_dec s1 s2) (eq_dec l1 l2) *)
209234
| @relop σ op1 , @relop τ op2 =>
210235
binoptel_eq_dec_relop op1 op2
211236
| _ , _ => right (ninv _ _)
@@ -280,26 +305,27 @@ Module bop.
280305

281306
Definition eval {σ1 σ2 σ3 : Ty} (op : BinOp σ1 σ2 σ3) : Val σ1 -> Val σ2 -> Val σ3 :=
282307
match op in BinOp σ1 σ2 σ3 return Val σ1 -> Val σ2 -> Val σ3 with
283-
| plus => Z.add
284-
| times => Z.mul
285-
| minus => Z.sub
286-
| land => Z.land
287-
| and => andb
288-
| or => fun v1 v2 => orb v1 v2
289-
| pair => Datatypes.pair
290-
| cons => List.cons
291-
| shiftr => fun v1 v2 => bv.shiftr v1 v2
292-
| shiftl => fun v1 v2 => bv.shiftl v1 v2
293-
| append => app
294-
| bvadd => fun v1 v2 => bv.add v1 v2
295-
| bvsub => fun v1 v2 => bv.sub v1 v2
296-
| bvmul => fun v1 v2 => bv.mul v1 v2
297-
| bvand => fun v1 v2 => bv.land v1 v2
298-
| bvor => fun v1 v2 => bv.lor v1 v2
299-
| bvxor => fun v1 v2 => bv.lxor v1 v2
300-
| bvapp => fun v1 v2 => bv.app v1 v2
301-
| bvcons => fun b bs => bv.cons b bs
302-
| relop op => eval_relop_val op
308+
| plus => Z.add
309+
| times => Z.mul
310+
| minus => Z.sub
311+
| land => Z.land
312+
| and => andb
313+
| or => fun v1 v2 => orb v1 v2
314+
| pair => Datatypes.pair
315+
| cons => List.cons
316+
| shiftr => fun v1 v2 => bv.shiftr v1 v2
317+
| shiftl => fun v1 v2 => bv.shiftl v1 v2
318+
| append => app
319+
| bvadd => fun v1 v2 => bv.add v1 v2
320+
| bvsub => fun v1 v2 => bv.sub v1 v2
321+
| bvmul => fun v1 v2 => bv.mul v1 v2
322+
| bvand => fun v1 v2 => bv.land v1 v2
323+
| bvor => fun v1 v2 => bv.lor v1 v2
324+
| bvxor => fun v1 v2 => bv.lxor v1 v2
325+
| bvapp => fun v1 v2 => bv.app v1 v2
326+
| bvcons => fun b bs => bv.cons b bs
327+
| update_vector_subrange s l => fun v1 v2 => bv.update_vector_subrange s l v1 v2
328+
| relop op => eval_relop_val op
303329
end.
304330

305331
End WithTypes.

‎theories/Syntax/Terms.v

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -201,6 +201,7 @@ Module Type TermsOn (Import TY : Types).
201201
Variable (pshiftl : forall n m (e1 : Term Σ (ty.bvec n)) (e2 : Term Σ (ty.bvec m)), P (term_binop bop.shiftl e1 e2)).
202202
Variable (pbvapp : forall n1 n2 (e1 : Term Σ (ty.bvec n1)) (e2 : Term Σ (ty.bvec n2)), P (term_binop bop.bvapp e1 e2)).
203203
Variable (pbvcons : forall n (e1 : Term Σ ty.bool) (e2 : Term Σ (ty.bvec n)), P (term_binop bop.bvcons e1 e2)).
204+
Variable (pupdate_subrange : forall {n s l : nat} (pf : IsTrue (s + l <=? n)) (e1 : Term Σ (ty.bvec n)) (e2 : Term Σ (ty.bvec l)), P (term_binop (@bop.update_vector_subrange _ _ s l pf) e1 e2)).
204205
Variable (pbvnot : forall n (e : Term Σ (ty.bvec n)), P (term_unop uop.bvnot e)).
205206
Variable (pnegate : forall n (e : Term Σ (ty.bvec n)), P (term_unop uop.negate e)).
206207
Variable (psext : forall n m (pf : IsTrue (m <=? n)) (e : Term Σ (ty.bvec m)), P (term_unop (uop.sext (p := pf)) e)).
@@ -222,6 +223,7 @@ Module Type TermsOn (Import TY : Types).
222223
| term_binop bop.shiftl s t => pshiftl s t
223224
| term_binop bop.bvapp s t => pbvapp s t
224225
| term_binop bop.bvcons s t => pbvcons s t
226+
| term_binop (bop.update_vector_subrange _ _) e t => pupdate_subrange _ e t
225227
| term_unop uop.bvnot t => pbvnot t
226228
| term_unop uop.negate t => pnegate t
227229
| term_unop uop.sext t => psext _ _ t
@@ -249,6 +251,7 @@ Module Type TermsOn (Import TY : Types).
249251
Variable (pshiftl : forall n m (e1 : Term Σ (ty.bvec n)) (e2 : Term Σ (ty.bvec m)), P e1 -> P e2 -> P (term_binop bop.shiftl e1 e2)).
250252
Variable (pbvapp : forall n1 n2 (e1 : Term Σ (ty.bvec n1)) (e2 : Term Σ (ty.bvec n2)), P e1 -> P e2 -> P (term_binop bop.bvapp e1 e2)).
251253
Variable (pbvcons : forall n (e1 : Term Σ ty.bool) (e2 : Term Σ (ty.bvec n)), P e2 -> P (term_binop bop.bvcons e1 e2)).
254+
Variable (pupdate_subrange : forall {n s l : nat} (pf : IsTrue (s + l <=? n)) (e1 : Term Σ (ty.bvec n)) (e2 : Term Σ (ty.bvec l)), P e1 -> P e2 -> P (term_binop (@bop.update_vector_subrange _ _ s l pf) e1 e2)).
252255
Variable (pbvnot : forall n (e : Term Σ (ty.bvec n)), P e -> P (term_unop uop.bvnot e)).
253256
Variable (pnegate : forall n (e : Term Σ (ty.bvec n)), P e -> P (term_unop uop.negate e)).
254257
Variable (psext : forall n m (pf : IsTrue (m <=? n)) (e : Term Σ (ty.bvec m)), P e -> P (term_unop (uop.sext (p := pf)) e)).
@@ -271,6 +274,7 @@ Module Type TermsOn (Import TY : Types).
271274
ltac:(intros; apply pshiftl; auto)
272275
ltac:(intros; apply pbvapp; auto)
273276
ltac:(intros; apply pbvcons; auto)
277+
ltac:(intros; apply pupdate_subrange; auto)
274278
ltac:(intros; apply pbvnot; auto)
275279
ltac:(intros; apply pnegate; auto)
276280
ltac:(intros; apply psext; auto)

0 commit comments

Comments
 (0)