summaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/arith.sail2
-rw-r--r--lib/coq/Sail2_operators_mwords.v9
-rw-r--r--lib/coq/Sail2_prompt.v31
-rw-r--r--lib/coq/Sail2_prompt_monad.v2
-rw-r--r--lib/coq/Sail2_real.v24
-rw-r--r--lib/coq/Sail2_values.v251
-rw-r--r--lib/vector_dec.sail3
7 files changed, 299 insertions, 23 deletions
diff --git a/lib/arith.sail b/lib/arith.sail
index 1950080a..d04c7988 100644
--- a/lib/arith.sail
+++ b/lib/arith.sail
@@ -70,7 +70,7 @@ val _shl_int = "shl_int" : (int, int) -> int
overload shl_int = {_shl8, _shl32, _shl_int}
-val _shr32 = {c: "shr_mach_int", _: "shr_int"} : forall 'n, 0 <= 'n <= 31. (int('n), int(1)) -> {'m, 0 <= 'm <= 15. int('m)}
+val _shr32 = {c: "shr_mach_int", coq: "shr_int_32", _: "shr_int"} : forall 'n, 0 <= 'n <= 31. (int('n), int(1)) -> {'m, 0 <= 'm <= 15. int('m)}
val _shr_int = "shr_int" : (int, int) -> int
diff --git a/lib/coq/Sail2_operators_mwords.v b/lib/coq/Sail2_operators_mwords.v
index 5a5f130c..9b5888c7 100644
--- a/lib/coq/Sail2_operators_mwords.v
+++ b/lib/coq/Sail2_operators_mwords.v
@@ -291,6 +291,9 @@ rewrite <- Z.lt_le_pred.
auto.
Defined.
+Definition sint0 {a} `{ArithFact (a >= 0)} (x : mword a) : Z :=
+ if sumbool_of_bool (Z.eqb a 0) then 0 else projT1 (sint x).
+
Lemma length_list_pos : forall {A} {l:list A}, length_list l >= 0.
unfold length_list.
auto with zarith.
@@ -393,9 +396,9 @@ val arith_shiftr : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
val rotl : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
val rotr : forall 'a. Size 'a => mword 'a -> integer -> mword 'a*)
(* TODO: check/redefine behaviour on out-of-range n *)
-Definition shiftl {a} (v : mword a) n : mword a := with_word (P := id) (fun w => Word.wlshift w (Z.to_nat n)) v.
-Definition shiftr {a} (v : mword a) n : mword a := with_word (P := id) (fun w => Word.wrshift w (Z.to_nat n)) v.
-Definition arith_shiftr {a} (v : mword a) n : mword a := with_word (P := id) (fun w => Word.wrshifta w (Z.to_nat n)) v.
+Definition shiftl {a} (v : mword a) n : mword a := with_word (P := id) (fun w => Word.wlshift' w (Z.to_nat n)) v.
+Definition shiftr {a} (v : mword a) n : mword a := with_word (P := id) (fun w => Word.wrshift' w (Z.to_nat n)) v.
+Definition arith_shiftr {a} (v : mword a) n : mword a := with_word (P := id) (fun w => Word.wrshifta' w (Z.to_nat n)) v.
(*
Definition rotl := rotl_bv
Definition rotr := rotr_bv
diff --git a/lib/coq/Sail2_prompt.v b/lib/coq/Sail2_prompt.v
index 5ab93cbc..68d097fb 100644
--- a/lib/coq/Sail2_prompt.v
+++ b/lib/coq/Sail2_prompt.v
@@ -181,6 +181,37 @@ Definition untilMT {RV Vars E} limit (vars : Vars) (cond : Vars -> monad RV bool
else slice vec (start_vec - size_r1) (start_vec - size_vec) in
write_reg r1 r1_v >> write_reg r2 r2_v*)
+Fixpoint pick_bit_list {rv e} (n:nat) : monad rv (list bool) e :=
+ match n with
+ | O => returnm []
+ | S m => choose_bool "pick_bit_list" >>= fun b =>
+ pick_bit_list m >>= fun t =>
+ returnm (b::t)
+ end%list.
+
+Definition internal_pick {rv a e} (xs : list a) : monad rv a e :=
+ let n := length xs in
+ match xs with
+ | h::_ =>
+ pick_bit_list (2 + n) >>= fun bs =>
+ let i := (Word.wordToNat (wordFromBitlist bs) mod n)%nat in
+ returnm (List.nth i xs h)
+ | [] => Fail "internal_pick called on empty list"
+ end.
+
+Fixpoint undefined_word_nat {rv e} n : monad rv (Word.word n) e :=
+ match n with
+ | O => returnm Word.WO
+ | S m =>
+ choose_bool "undefined_word_nat" >>= fun b =>
+ undefined_word_nat m >>= fun t =>
+ returnm (Word.WS b t)
+ end.
+
+Definition undefined_bitvector {rv e} n `{ArithFact (n >= 0)} : monad rv (mword n) e :=
+ undefined_word_nat (Z.to_nat n) >>= fun w =>
+ returnm (word_to_mword w).
+
(* If we need to build an existential after a monadic operation, assume that
we can do it entirely from the type. *)
diff --git a/lib/coq/Sail2_prompt_monad.v b/lib/coq/Sail2_prompt_monad.v
index f95e4b6c..b26a2ff3 100644
--- a/lib/coq/Sail2_prompt_monad.v
+++ b/lib/coq/Sail2_prompt_monad.v
@@ -113,6 +113,8 @@ Definition choose_bool {rv E} descr : monad rv bool E := Choose descr returnm.
(*val undefined_bool : forall 'rv 'e. unit -> monad 'rv bool 'e*)
Definition undefined_bool {rv e} (_:unit) : monad rv bool e := choose_bool "undefined_bool".
+Definition undefined_unit {rv e} (_:unit) : monad rv unit e := returnm tt.
+
(*val assert_exp : forall rv e. bool -> string -> monad rv unit e*)
Definition assert_exp {rv E} (exp :bool) msg : monad rv unit E :=
if exp then Done tt else Fail msg.
diff --git a/lib/coq/Sail2_real.v b/lib/coq/Sail2_real.v
index e4e4316e..494e36d4 100644
--- a/lib/coq/Sail2_real.v
+++ b/lib/coq/Sail2_real.v
@@ -9,16 +9,28 @@ Instance Decidable_eq_real : forall (x y : R), Decidable (x = y) :=
Definition realFromFrac (num denom : Z) : R := Rdiv (IZR num) (IZR denom).
+Definition neg_real := Ropp.
+Definition mult_real := Rmult.
+Definition sub_real := Rminus.
+Definition add_real := Rplus.
+Definition div_real := Rdiv.
+Definition sqrt_real := sqrt.
+Definition abs_real := Rabs.
+
+(* Use flocq definitions, but without making the whole library a dependency. *)
+Definition round_down (x : R) := (up x - 1)%Z.
+Definition round_up (x : R) := (- round_down (- x))%Z.
+
+Definition to_real := IZR.
+
+Definition eq_real := Reqb.
Definition gteq_real (x y : R) : bool := if Rge_dec x y then true else false.
Definition lteq_real (x y : R) : bool := if Rle_dec x y then true else false.
Definition gt_real (x y : R) : bool := if Rgt_dec x y then true else false.
Definition lt_real (x y : R) : bool := if Rlt_dec x y then true else false.
(* Export select definitions from outside of Rbase *)
-Definition powerRZ := powerRZ.
-Definition Rabs := Rabs.
-Definition sqrt := sqrt.
+Definition pow_real := powerRZ.
-(* Use flocq definitions, but without making the whole library a dependency. *)
-Definition Zfloor (x : R) := (up x - 1)%Z.
-Definition Zceil (x : R) := (- Zfloor (- x))%Z.
+Definition print_real (_ : string) (_ : R) : unit := tt.
+Definition prerr_real (_ : string) (_ : R) : unit := tt.
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index 1ddc3f22..17d79830 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -156,6 +156,16 @@ apply Zmult_ge_compat; auto with zarith.
* apply Z_div_ge0; auto. apply Z.lt_gt. apply Z.abs_pos. auto with zarith.
Qed.
+Lemma ZEuclid_pos_div : forall x y, y > 0 -> ZEuclid.div x y >= 0 -> x >= 0.
+intros x y GT.
+ specialize (ZEuclid.div_mod x y);
+ specialize (ZEuclid.mod_always_pos x y);
+ generalize (ZEuclid.modulo x y);
+ generalize (ZEuclid.div x y);
+ intros.
+nia.
+Qed.
+
Lemma ZEuclid_div_ge : forall x y, y > 0 -> x >= 0 -> x - ZEuclid.div x y >= 0.
intros.
unfold ZEuclid.div.
@@ -185,7 +195,7 @@ apply ZEuclid.div_mod.
assumption.
Qed.
-Hint Resolve ZEuclid_div_pos ZEuclid_div_ge ZEuclid_div_mod0 : sail.
+Hint Resolve ZEuclid_div_pos ZEuclid_pos_div ZEuclid_div_ge ZEuclid_div_mod0 : sail.
(*
@@ -873,6 +883,9 @@ Program Definition to_word {n} : n >= 0 -> word (Z.to_nat n) -> mword n :=
| Zpos _ => fun _ w => w
end.
+Definition word_to_mword {n} (w : word (Z.to_nat n)) `{H:ArithFact (n >= 0)} : mword n :=
+ to_word (match H with Build_ArithFact _ H' => H' end) w.
+
(*val length_mword : forall a. mword a -> Z*)
Definition length_mword {n} (w : mword n) := n.
@@ -904,7 +917,7 @@ Parameter undefined_bit : bool.
Definition getBit {n} :=
match n with
| O => fun (w : word O) i => undefined_bit
-| S n => fun (w : word (S n)) i => wlsb (wrshift w i)
+| S n => fun (w : word (S n)) i => wlsb (wrshift' w i)
end.
Definition access_mword_dec {m} (w : mword m) n := bitU_of_bool (getBit (get_word w) (Z.to_nat n)).
@@ -922,7 +935,7 @@ Definition setBit {n} :=
match n with
| O => fun (w : word O) i b => w
| S n => fun (w : word (S n)) i (b : bool) =>
- let bit : word (S n) := wlshift (natToWord _ 1) i in
+ let bit : word (S n) := wlshift' (natToWord _ 1) i in
let mask : word (S n) := wnot bit in
let masked := wand mask w in
if b then masked else wor masked bit
@@ -1051,9 +1064,9 @@ end.
(* Definitions in the context that involve proof for other constraints can
break some of the constraint solving tactics, so prune definition bodies
down to integer types. *)
-Ltac not_Z ty := match ty with Z => fail 1 | _ => idtac end.
-Ltac clear_non_Z_defns :=
- repeat match goal with H := _ : ?X |- _ => not_Z X; clearbody H end.
+Ltac not_Z_bool ty := match ty with Z => fail 1 | bool => fail 1 | _ => idtac end.
+Ltac clear_non_Z_bool_defns :=
+ repeat match goal with H := _ : ?X |- _ => not_Z_bool X; clearbody H end.
Ltac clear_irrelevant_defns :=
repeat match goal with X := _ |- _ =>
match goal with |- context[X] => idtac end ||
@@ -1119,11 +1132,11 @@ Ltac unbool_comparisons_goal :=
(* Split up dependent pairs to get at proofs of properties *)
Ltac extract_properties :=
(* Properties of local definitions *)
- repeat match goal with H := (projT1 ?X) |- _ =>
+ repeat match goal with H := context[projT1 ?X] |- _ =>
let x := fresh "x" in
let Hx := fresh "Hx" in
destruct X as [x Hx] in *;
- change (projT1 (existT _ x Hx)) with x in *; unfold H in * end;
+ change (projT1 (existT _ x Hx)) with x in * end;
(* Properties in the goal *)
repeat match goal with |- context [projT1 ?X] =>
let x := fresh "x" in
@@ -1240,7 +1253,9 @@ Ltac filter_disjunctions :=
| H1:context [?t = true \/ ?P], H2: ?t = false |- _ => is_var t; rewrite H2 in H1
| H1:context [?t = false \/ ?P], H2: ?t = true |- _ => is_var t; rewrite H2 in H1
end;
- repeat rewrite truefalse, falsetrue, or_False_l, or_False_r in *.
+ rewrite ?truefalse, ?falsetrue, ?or_False_l, ?or_False_r in *;
+ (* We may have uncovered more conjunctions *)
+ repeat match goal with H:and _ _ |- _ => destruct H end.
(* Turn x := if _ then ... into x = ... \/ x = ... *)
@@ -1296,10 +1311,51 @@ Ltac clear_irrelevant_bindings :=
end
end.
+(* Currently, the ASL to Sail translation produces some constraints of the form
+ P \/ x = true, P \/ x = false, which are simplified by the tactic below. In
+ future the translation is likely to be cleverer, and this won't be
+ necessary. *)
+(* TODO: remove duplication with filter_disjunctions *)
+Lemma remove_unnecessary_casesplit {P:Prop} {x} :
+ P \/ x = true -> P \/ x = false -> P.
+ intuition congruence.
+Qed.
+Lemma remove_eq_false_true {P:Prop} {x} :
+ x = true -> P \/ x = false -> P.
+intros H1 [H|H]; congruence.
+Qed.
+Lemma remove_eq_true_false {P:Prop} {x} :
+ x = false -> P \/ x = true -> P.
+intros H1 [H|H]; congruence.
+Qed.
+Ltac remove_unnecessary_casesplit :=
+repeat match goal with
+| H1 : ?P \/ ?v = true, H2 : ?v = true |- _ => clear H1
+| H1 : ?P \/ ?v = true, H2 : ?v = false |- _ => apply (remove_eq_true_false H2) in H1
+| H1 : ?P \/ ?v = false, H2 : ?v = false |- _ => clear H1
+| H1 : ?P \/ ?v = false, H2 : ?v = true |- _ => apply (remove_eq_false_true H2) in H1
+| H1 : ?P \/ ?v1 = true, H2 : ?P \/ ?v2 = false |- _ =>
+ constr_eq v1 v2;
+ is_var v1;
+ apply (remove_unnecessary_casesplit H1) in H2;
+ clear H1
+ (* There are worse cases where the hypotheses are different, so we actually
+ do the casesplit *)
+| H1 : _ \/ ?v = true, H2 : _ \/ ?v = false |- _ =>
+ is_var v;
+ destruct v;
+ [ clear H1; destruct H2; [ | congruence ]
+ | clear H2; destruct H1; [ | congruence ]
+ ]
+end;
+(* We may have uncovered more conjunctions *)
+repeat match goal with H:and _ _ |- _ => destruct H end.
+
+
Ltac prepare_for_solver :=
(*dump_context;*)
clear_irrelevant_defns;
- clear_non_Z_defns;
+ clear_non_Z_bool_defns;
autounfold with sail in * |- *; (* You can add Hint Unfold ... : sail to let omega see through fns *)
split_cases;
extract_properties;
@@ -1309,6 +1365,7 @@ Ltac prepare_for_solver :=
unbool_comparisons;
unbool_comparisons_goal;
repeat match goal with H:and _ _ |- _ => destruct H end;
+ remove_unnecessary_casesplit;
unfold_In; (* after unbool_comparisons to deal with && and || *)
reduce_list_lengths;
reduce_pow;
@@ -1357,7 +1414,14 @@ tauto.
Qed.
Ltac solve_euclid :=
-repeat match goal with |- context [ZEuclid.modulo ?x ?y] =>
+repeat match goal with
+| |- context [ZEuclid.modulo ?x ?y] =>
+ specialize (ZEuclid.div_mod x y);
+ specialize (ZEuclid.mod_always_pos x y);
+ generalize (ZEuclid.modulo x y);
+ generalize (ZEuclid.div x y);
+ intros
+| |- context [ZEuclid.div ?x ?y] =>
specialize (ZEuclid.div_mod x y);
specialize (ZEuclid.mod_always_pos x y);
generalize (ZEuclid.modulo x y);
@@ -1420,14 +1484,136 @@ Ltac simple_ex_iff :=
solve [apply iff_refl | eassumption]
end.
+(* Another attempt at similar goals, this time allowing for conjuncts to move
+ around, and filling in integer existentials and redundant boolean ones.
+ TODO: generalise / combine with simple_ex_iff. *)
+
+Ltac ex_iff_construct_bool_witness :=
+let rec search x y :=
+ lazymatch y with
+ | x => constr:(true)
+ | ?y1 /\ ?y2 =>
+ let b1 := search x y1 in
+ let b2 := search x y2 in
+ constr:(orb b1 b2)
+ | _ => constr:(false)
+ end
+in
+let rec make_clause x :=
+ lazymatch x with
+ | ?l = true => l
+ | ?l = false => constr:(negb l)
+ | @eq Z ?l ?n => constr:(Z.eqb l n)
+ | ?p \/ ?q =>
+ let p' := make_clause p in
+ let q' := make_clause q in
+ constr:(orb p' q')
+ | _ => fail
+ end in
+let add_clause x xs :=
+ let l := make_clause x in
+ match xs with
+ | true => l
+ | _ => constr:(andb l xs)
+ end
+in
+let rec construct_ex l r x :=
+ lazymatch l with
+ | ?l1 /\ ?l2 =>
+ let y := construct_ex l1 r x in
+ construct_ex l2 r y
+ | _ =>
+ let present := search l r in
+ lazymatch eval compute in present with true => x | _ => add_clause l x end
+ end
+in
+let witness := match goal with
+| |- ?l <-> ?r => construct_ex l r constr:(true)
+end in
+instantiate (1 := witness).
+
+Ltac ex_iff_fill_in_ints :=
+ let rec search l r y :=
+ match y with
+ | l = r => idtac
+ | ?v = r => is_evar v; unify v l
+ | ?y1 /\ ?y2 => first [search l r y1 | search l r y2]
+ | _ => fail
+ end
+ in
+ match goal with
+ | |- ?l <-> ?r =>
+ let rec traverse l :=
+ lazymatch l with
+ | ?l1 /\ ?l2 =>
+ traverse l1; traverse l2
+ | @eq Z ?x ?y => search x y r
+ | _ => idtac
+ end
+ in traverse l
+ end.
+
+Ltac ex_iff_fill_in_bools :=
+ let rec traverse t :=
+ lazymatch t with
+ | ?v = ?t => try (is_evar v; unify v t)
+ | ?p /\ ?q => traverse p; traverse q
+ | _ => idtac
+ end
+ in match goal with
+ | |- _ <-> ?r => traverse r
+ end.
+
+Ltac conjuncts_iff_solve :=
+ ex_iff_fill_in_ints;
+ ex_iff_construct_bool_witness;
+ ex_iff_fill_in_bools;
+ unbool_comparisons_goal;
+ clear;
+ intuition.
+
+Ltac ex_iff_solve :=
+ match goal with
+ | |- @ex _ _ => eexists; ex_iff_solve
+ (* Range constraints are attached to the right *)
+ | |- _ /\ _ => split; [ex_iff_solve | omega]
+ | |- _ <-> _ => conjuncts_iff_solve
+ end.
+
+
Lemma iff_false_left {P Q R : Prop} : (false = true) <-> Q -> (false = true) /\ P <-> Q /\ R.
intuition.
Qed.
+(* Very simple proofs for trivial arithmetic. Preferable to running omega/lia because
+ they can get bogged down if they see large definitions; should also guarantee small
+ proof terms. *)
+Lemma Z_compare_lt_eq : Lt = Eq -> False. congruence. Qed.
+Lemma Z_compare_lt_gt : Lt = Gt -> False. congruence. Qed.
+Lemma Z_compare_eq_lt : Eq = Lt -> False. congruence. Qed.
+Lemma Z_compare_eq_gt : Eq = Gt -> False. congruence. Qed.
+Lemma Z_compare_gt_lt : Gt = Lt -> False. congruence. Qed.
+Lemma Z_compare_gt_eq : Gt = Eq -> False. congruence. Qed.
+Ltac z_comparisons :=
+ solve [
+ exact eq_refl
+ | exact Z_compare_lt_eq
+ | exact Z_compare_lt_gt
+ | exact Z_compare_eq_lt
+ | exact Z_compare_eq_gt
+ | exact Z_compare_gt_lt
+ | exact Z_compare_gt_eq
+ ].
+
+
+(* Redefine this to add extra solver tactics *)
+Ltac sail_extra_tactic := fail.
+
Ltac main_solver :=
solve
[ match goal with |- (?x ?y) => is_evar x; idtac "Warning: unknown constraint"; exact (I : (fun _ => True) y) end
| apply ArithFact_mword; assumption
+ | z_comparisons
| omega with Z
(* Try sail hints before dropping the existential *)
| subst; eauto 3 with zarith sail
@@ -1439,8 +1625,22 @@ Ltac main_solver :=
| |- context [ZEuclid.modulo] => solve_euclid
end
| match goal with |- context [Z.mul] => nia end
+ (* If we have a disjunction from a set constraint on a variable we can often
+ solve a goal by trying them (admittedly this is quite heavy handed...) *)
+ | subst;
+ let aux x :=
+ is_var x;
+ intuition (subst;auto)
+ in
+ match goal with
+ | _:(@eq Z _ ?x) \/ (@eq Z _ ?x) \/ _ |- context[?x] => aux x
+ | _:(@eq Z ?x _) \/ (@eq Z ?x _) \/ _ |- context[?x] => aux x
+ | _:(@eq Z _ ?x) \/ (@eq Z _ ?x) \/ _, _:@eq Z ?y (ZEuclid.div ?x _) |- context[?y] => is_var x; aux y
+ | _:(@eq Z ?x _) \/ (@eq Z ?x _) \/ _, _:@eq Z ?y (ZEuclid.div ?x _) |- context[?y] => is_var x; aux y
+ end
(* Booleans - and_boolMP *)
| simple_ex_iff
+ | ex_iff_solve
| drop_bool_exists; solve [eauto using iff_refl, or_iff_cong, and_iff_cong | intuition]
| match goal with |- (forall l r:bool, _ -> _ -> exists _ : bool, _) =>
let r := fresh "r" in
@@ -1479,9 +1679,18 @@ Ltac main_solver :=
(* Don't use auto for the fallback to keep runtime down *)
firstorder fail
end*)
+ | sail_extra_tactic
| idtac "Unable to solve constraint"; dump_context; fail
].
+(* Omega can get upset by local definitions that are projections from value/proof pairs.
+ Complex goals can use prepare_for_solver to extract facts; this tactic can be used
+ for simpler proofs without using prepare_for_solver. *)
+Ltac simple_omega :=
+ repeat match goal with
+ H := projT1 _ |- _ => clearbody H
+ end; omega.
+
Ltac solve_arithfact :=
(* Attempt a simple proof first to avoid lengthy preparation steps (especially
as the large proof terms can upset subsequent proofs). *)
@@ -1492,7 +1701,8 @@ try match goal with |- context [projT1 ?X] => apply (ArithFact_self_proof X) end
(* Trying reflexivity will fill in more complex metavariable examples than
fill_in_evar_eq above, e.g., 8 * n = 8 * ?Goal3 *)
try (constructor; reflexivity);
-try (constructor; omega);
+try (constructor; repeat match goal with |- and _ _ => split end; z_comparisons);
+try (constructor; simple_omega);
prepare_for_solver;
(*dump_context;*)
constructor;
@@ -2145,6 +2355,23 @@ subst; compute;
auto using Build_ArithFact.
Defined.
+Definition shr_int_32 (x y : Z) `{HE:ArithFact (0 <= x <= 31)} `{HR:ArithFact (y = 1)}: {z : Z & ArithFact (0 <= z <= 15)}.
+refine (existT _ (shr_int x y) _).
+destruct HE as [HE].
+destruct HR as [HR];
+subst.
+unfold shr_int.
+rewrite <- Z.div2_spec.
+constructor.
+rewrite Z.div2_div.
+specialize (Z.div_mod x 2).
+specialize (Z.mod_pos_bound x 2).
+generalize (Z.div x 2).
+generalize (x mod 2).
+intros.
+nia.
+Defined.
+
Lemma shl_8_ge_0 {n} : shl_int 8 n >= 0.
unfold shl_int.
apply Z.le_ge.
diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail
index 4e4a099f..965b236e 100644
--- a/lib/vector_dec.sail
+++ b/lib/vector_dec.sail
@@ -61,6 +61,7 @@ THIS`(v, n)` truncates `v`, keeping only the _most_ significant `n` bits.
*/
val truncateLSB = {
ocaml: "vector_truncateLSB",
+ interpreter: "vector_truncateLSB",
lem: "vector_truncateLSB",
coq: "vector_truncateLSB",
c: "sail_truncateLSB"
@@ -205,7 +206,7 @@ val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), int('m)) -> bit
val slice_mask : forall 'n, 'n >= 0. (implicit('n), int, int) -> bits('n) effect pure
function slice_mask(n,i,l) =
if l >= n then {
- sail_ones(n)
+ sail_shiftleft(sail_ones(n), i)
} else {
let one : bits('n) = sail_mask(n, 0b1 : bits(1)) in
sail_shiftleft(sub_bits(sail_shiftleft(one, l), one), i)
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-13 09:44:32 +0000