Investigating alternate definition of Val.of_bool

roconnor-blockstream · Feb 1, 2023 · 5a23519 · 5a23519
1 parent 24a1072
commit 5a23519
Show file tree

Hide file tree

Showing 7 changed files with 23 additions and 23 deletions.
diff --git a/atomics/verif_lock.v b/atomics/verif_lock.v
@@ -121,7 +121,7 @@ Section PROOFS.
       unfold inv_for_lock.
       do 2 (apply allp_right; intros).
       eapply derives_trans, now_later.
-      Exists true; simpl; cancel. apply derives_refl. }
+      Exists true; simpl; cancel. }
     simpl.
     forward.
     simpl; Exists (p, i, g); unfold atomic_lock_inv; entailer!.

diff --git a/compcert/common/Values.v b/compcert/common/Values.v
@@ -270,7 +270,7 @@ Definition notint (v: val) : val :=
   | _ => Vundef
   end.
 
-Definition of_bool (b: bool): val := if b then Vtrue else Vfalse.
+Definition of_bool (b: bool): val := Vint (Int.repr (Z.b2z  b)).
 
 Definition boolval (v: val) : val :=
   match v with

diff --git a/compcert_new/common/Values.v b/compcert_new/common/Values.v
@@ -252,7 +252,7 @@ Definition notint (v: val) : val :=
   | _ => Vundef
   end.
 
-Definition of_bool (b: bool): val := if b then Vtrue else Vfalse.
+Definition of_bool (b: bool): val := Vint (Int.repr (Z.b2z  b)).
 
 Definition boolval (v: val) : val :=
   match v with

diff --git a/floyd/compare_lemmas.v b/floyd/compare_lemmas.v
@@ -53,9 +53,9 @@ intros.
  apply prop_derives; intro.
  unfold tptr in H; simpl in H. unfold sem_binary_operation' in H.
  simpl in H. rewrite !andb_false_r in H.
- destruct (v rho); inv H.
+ destruct (v rho); try discriminate.
  unfold sem_cmp_pp, strict_bool_val, nullval in *.
- destruct Archi.ptr64  eqn:Hp; simpl in H1;
+ destruct Archi.ptr64  eqn:Hp; simpl in H; inv H;
  try solve [inv H1];
  try solve [pose proof (Int64.eq_spec i Int64.zero);
                 destruct (Int64.eq i Int64.zero); inv H1; auto];

diff --git a/floyd/forward.v b/floyd/forward.v
@@ -1676,7 +1676,7 @@ Lemma typed_true_Cne_neq:
   forall x y, 
     typed_true tint (force_val (sem_cmp_pp Cne x y)) -> x <> y.
 Proof.
-  intros. hnf in H. destruct x, y; try inversion H.
+  intros. hnf in H. destruct x, y; try discriminate H.
   - unfold sem_cmp_pp, strict_bool_val, Val.cmplu_bool, Val.cmpu_bool in H.
     destruct Archi.ptr64 eqn:Hp; simpl in H; 
     try destruct (Int64.eq i i0) eqn:?;
@@ -1697,7 +1697,7 @@ Proof.
         subst b i. inversion H.  
       * intro. inversion H0.
         subst i.
-        pose proof (Ptrofs.eq_spec i0 i0). rewrite Heqb1 in H2.
+        pose proof (Ptrofs.eq_spec i0 i0). rewrite Heqb1 in H1.
         contradiction.  
     + intro. inversion H0. subst b. contradiction.
 Qed.
@@ -1706,7 +1706,7 @@ Lemma typed_true_Ceq_eq:
   forall x y, 
     typed_true tint (force_val (sem_cmp_pp Ceq x y)) -> x = y.
 Proof.
-  intros. hnf in H. destruct x, y; try inversion H.
+  intros. hnf in H. destruct x, y; try discriminate H.
   - unfold sem_cmp_pp, strict_bool_val, Val.cmplu_bool, Val.cmpu_bool in H;
     destruct Archi.ptr64 eqn:Hp; simpl in H; 
     try destruct (Int64.eq i i0) eqn:?; 
@@ -1740,7 +1740,7 @@ Lemma typed_false_Cne_eq:
   forall x y, 
     typed_false tint (force_val (sem_cmp_pp Cne x y)) -> x = y.
 Proof.
-  intros. hnf in H. destruct x, y; try inversion H.
+  intros. hnf in H. destruct x, y; try discriminate H.
   - unfold sem_cmp_pp, strict_bool_val, Val.cmplu_bool, Val.cmpu_bool in H;
     destruct Archi.ptr64 eqn:Hp; simpl in H; 
     try destruct (Int64.eq i i0) eqn:?; 
@@ -1773,7 +1773,7 @@ Lemma typed_false_Ceq_neq:
   forall x y, 
     typed_false tint (force_val (sem_cmp_pp Ceq x y)) -> x <> y.
 Proof.
-  intros. hnf in H. destruct x, y; try inversion H. 
+  intros. hnf in H. destruct x, y; try discriminate H. 
   - unfold sem_cmp_pp, strict_bool_val, Val.cmplu_bool, Val.cmpu_bool in H.
     destruct Archi.ptr64 eqn:Hp; simpl in H; 
     try destruct (Int64.eq i i0) eqn:?;
@@ -1793,7 +1793,7 @@ Proof.
       * simpl in H. pose proof (Ptrofs.eq_spec i i0). rewrite Heqb1 in H0.
         subst b i. inversion H.
       * intro. inversion H0. subst b i. pose proof (Ptrofs.eq_spec i0 i0). 
-        rewrite Heqb1 in H2. contradiction.
+        rewrite Heqb1 in H1. contradiction.
     + intro. inversion H0. contradiction. 
 Qed.
 
@@ -1935,9 +1935,9 @@ Lemma typed_true_negb_bool_val_p:
             (bool_val_p p))) ->
      p = nullval.
 Proof.
-intros. destruct p; inv H.
+intros. destruct p; try discriminate H; simpl in H.
 destruct Archi.ptr64 eqn:Hp;
-(simpl in H1;
+(simpl in H; inv H;
 try (pose proof (Int64.eq_spec i Int64.zero);
       destruct (Int64.eq i Int64.zero); inv H1; auto);
 try (pose proof (Int.eq_spec i Int.zero);
@@ -1953,7 +1953,7 @@ Lemma typed_false_negb_bool_val_p:
             (bool_val_p p))) ->
      isptr p.
 Proof.
-intros. destruct p; try solve [inv H0]; auto; rename H0 into H1.
+intros. destruct p; try solve [discriminate H0]; auto; rename H0 into H1.
 simpl in H.
 simpl.
 destruct Archi.ptr64 eqn:Hp;

diff --git a/progs64/verif_strlib.v b/progs64/verif_strlib.v
@@ -291,7 +291,6 @@ forward_loop (EX i : Z,
   forward. fold_Vbyte.
   forward_if (temp _t'1 (Val.of_bool (Z.eqb i (Zlength ls1) && Z.eqb i (Zlength ls2)))).
   { forward.
-    simpl force_val.
     rewrite Hs1 in *.
     destruct (Byte.eq_dec (Znth i (ls2 ++ [Byte.zero])) Byte.zero).
     + rewrite e; simpl force_val.
@@ -300,8 +299,8 @@ forward_loop (EX i : Z,
      rewrite (proj2 (Z.eqb_eq i (Zlength ls1)) H6).
      rewrite (proj2 (Z.eqb_eq i (Zlength ls2)) H7).
      entailer!.
-  +
-    rewrite Int.eq_false.
+  + simpl (Z.b2z _).
+    rewrite (Int.eq_false (Int.repr (Byte.signed (Znth i (ls2 ++ [Byte.zero]))))).
      rewrite (proj2 (Z.eqb_eq i (Zlength ls1)) H6).
      rewrite Hs2 in n.
      rewrite (proj2 (Z.eqb_neq i (Zlength ls2))) by auto.
@@ -529,6 +528,7 @@ forward_loop (EX i : Z,
   (* these two parts are not much simplified *)
   { forward. cstring1. entailer!.
     rewrite (proj2 (Z.eqb_eq _ _)) by auto.
+    simpl.
     destruct (Int.eq (Int.repr (Byte.signed (Znth (Zlength ls1) (ls2 ++ [Byte.zero])))) (Int.repr 0)) eqn:Heqb;
     do_repr_inj Heqb. (* utilize this internal tactic *)
     - rewrite (proj2 (Z.eqb_eq _ _)) by cstring.

diff --git a/veric/binop_lemmas3.v b/veric/binop_lemmas3.v
@@ -240,13 +240,13 @@ Lemma int_type_tc_val_of_bool:
   forall t b, is_int_type t = true -> tc_val t (Val.of_bool b).
 Proof.
 intros.
-    destruct t as [| [| | |] [|] | | | | | | |]; 
+    destruct t as [| [| | |] [|] | | | | | | |];
  try discriminate; hnf; auto; clear H;
- destruct b; simpl; auto;
-change (Int.signed Int.one) with 1;
-change (Int.signed Int.zero) with 0;
-change (Int.unsigned Int.one) with 1;
-change (Int.unsigned Int.zero) with 0;
+ destruct b; cbn; auto; try discriminate;
+change (Int.signed (Int.repr 1)) with 1;
+change (Int.signed (Int.repr 0)) with 0;
+change (Int.unsigned (Int.repr 1)) with 1;
+change (Int.unsigned (Int.repr 0)) with 0;
 change Byte.min_signed with (-128);
 change Byte.max_signed with 127;
 change Byte.max_unsigned with 255;