update to master

theories/bitvector.v

@@ -4,65 +4,6 @@ From stdpp Require Import options.
 
 Local Open Scope Z_scope.
 
-(* Checks that a term is closed using a trick by Jason Gross. *)
-Ltac check_closed t :=
-  assert_succeeds (
-    let x := fresh "x" in
-    exfalso; pose t as x; revert x;
-    repeat match goal with H : _ |- _ => clear H end;
-    lazymatch goal with H : _ |- _ => fail | _ => idtac end
-  ).
-
-Lemma list_fmap_inj1 {A B} (f1 f2 : A → B) (l : list A) x:
-  f1 <$> l = f2 <$> l → x ∈ l → f1 x = f2 x.
-Proof.
-  induction l; csimpl.
-  - intros ? ?%elem_of_nil. done.
-  - intros [=] [?|?]%elem_of_cons; naive_solver.
-Qed.
-
-Lemma Z_to_little_endian_lookup_Some m n z (i : nat) x:
-  0 ≤ m →
-  0 ≤ n →
-  Z_to_little_endian m n z !! i = Some x ↔
-    Z.of_nat i < m ∧ x = Z.land (z ≫ (Z.of_nat i * n)) (Z.ones n).
-Proof.
-  revert z m. induction i as [|i IH]; intros z m Hm Hn; rewrite <-(Z.succ_pred m) at 1.
-  all: destruct (decide (m = 0)); subst; simpl; [ naive_solver lia|].
-  all: rewrite Z_to_little_endian_succ; simpl; [|lia].
-  { rewrite Z.shiftr_0_r. naive_solver lia. }
-  rewrite IH, ?Z.shiftr_shiftr; [|nia..].
-  assert ((n + Z.of_nat i * n) = (Z.of_nat (S i) * n)) as -> by lia.
-  naive_solver lia.
-Qed.
-
-Lemma little_endian_to_Z_spec n bs i b:
-  0 ≤ i → 0 < n →
-  Forall (λ b, 0 ≤ b < 2 ^ n) bs →
-  bs !! Z.to_nat (i `div` n) = Some b →
-  Z.testbit (little_endian_to_Z n bs) i = Z.testbit b (i `mod` n).
-Proof.
-  intros Hi Hn. rewrite Z2Nat_inj_div; [|lia..].
-  assert (Z.to_nat n ≠ 0%nat). { intros ?%(Z2Nat.inj _ 0); lia. }
-  revert i Hi.
-  induction bs as [|b' bs IH]; intros i ?; [done|]; simpl.
-  intros [[? Hb]?]%Forall_cons. intros [[Hx ?]|[? Hbs]]%lookup_cons_Some; subst.
-  - apply Nat.div_small_iff in Hx; [|lia]. apply Z2Nat.inj_lt in Hx; [|lia..].
-    rewrite Z.lor_spec, Z.shiftl_spec, Z.mod_small, (Z.testbit_neg_r _ (i - n)); [|lia..].
-    by rewrite orb_false_r.
-  - rewrite Z.lor_spec, Z.shiftl_spec by lia.
-    assert (Z.to_nat n <= Z.to_nat i)%nat as Hle. { apply Nat.div_str_pos_iff; lia. }
-    assert (n ≤ i). { apply Z2Nat.inj_le; lia. }
-    revert Hbs.
-    assert (Z.to_nat i `div` Z.to_nat n - 1 = Z.to_nat (i - n) `div` Z.to_nat n)%nat as ->. {
-      apply Nat2Z.inj. rewrite !Z2Nat.inj_sub, !Nat2Z_inj_div, !Nat2Z.inj_sub, !Nat2Z_inj_div; [|lia..].
-      rewrite <-(Z.add_opp_r (Z.of_nat _)), Z.opp_eq_mul_m1, Z.mul_comm, Z.div_add; [|lia]. lia.
-    }
-    intros ->%IH; [|lia|done]. rewrite <-Zminus_mod_idemp_r, Z_mod_same_full, Z.sub_0_r.
-    assert (Z.testbit b' i = false) as ->; [|done].
-    eapply Z_bounded_iff_bits_nonneg; [| |done|]; lia.
-Qed.
-
 (** * Preliminary definitions *)
 Definition bv_modulus (n : N) : Z := 2 ^ (Z.of_N n).
 Definition bv_half_modulus (n : N) : Z := bv_modulus n `div` 2.
@@ -291,7 +232,7 @@ Typeclasses Opaque BvWf.
 Ltac solve_BvWf :=
   lazymatch goal with
     |- BvWf ?n ?v =>
-      check_closed v;
+      is_closed_term v;
       try (vm_compute; exact I);
       fail "Bitvector constant" v "does not fit into" n "bits"
   end.
@@ -1233,7 +1174,7 @@ Section bv_bits.
     unfold bv_to_bits. intros x y Hf.
     apply bv_eq_wrap. apply Z.bits_inj_iff'. intros i Hi.
     rewrite !bv_wrap_spec; [|lia..]. case_bool_decide; simpl; [|done].
-    eapply list_fmap_inj1 in Hf; [done|]. apply elem_of_seqZ. lia.
+    eapply list_fmap_inj_1 in Hf; [done|exact (const true)|]. apply elem_of_seqZ. lia.
   Qed.
 End bv_bits.