Use (new) bool2val instead of Val.of_bool (#661)

* Use (new) bool2val instead of Val.of_bool

This P.R. implements the suggestion in issue #625.
It's an experiment, as in some cases it breaks existing VST proofs
at `forward_if` and related tactics.  The changes required in those
proofs are generally positive (simplifies proof scripts).
See further discussion at #625.  closes #625

Incidentally and unrelated:  closes #660

* Adjustment for 32/64-bit portability
* Fix memory blowup; bring verif_strlib up to date in 64-bit mode
* Fix up a proof in tweetnacl
* Bring mailbox up to date with bool2val
* simplify_new_temp in fwd_result, in connection with new bool2val stuff
* Flesh out simplify_new_temp hint DB; bring 32-bit examples up to date
* Update CHANGES file

CHANGES

@@ -1,3 +1,8 @@
+CHANGES IN THE WORKS FOR 2.12
+
+- New entailer!! tactic
+- Use bool2val instead of Val.of_bool, improves forward_if 
+
 CHANGES IN RELEASE 2.11.1 (December 2022)
 - Compatible with Coq 8.16.1, 8.15, and (perhaps) 8.14.
 

Makefile

@@ -576,8 +576,8 @@ TWEETNACL_FILES = \
   verif_fcore_jbody.v verif_fcore_loop3.v \
   verif_fcore_epilogue_hfalse.v verif_fcore_epilogue_htrue.v \
   verif_fcore.v verif_crypto_core.v \
-  verif_crypto_stream_salsa20_xor.v verif_crypto_stream.v \
-  verif_verify.v
+  verif_crypto_stream_salsa20_xor1.v verif_crypto_stream_salsa20_xor.v \
+  verif_crypto_stream.v verif_verify.v
 
 HMACDRBG_FILES = \
   entropy.v entropy_lemmas.v DRBG_functions.v HMAC_DRBG_algorithms.v \

floyd/client_lemmas.v

@@ -1842,7 +1842,7 @@ Qed.
 Lemma typed_false_of_bool':
  forall x (P: Prop),
     ((x=false) -> P) ->
-    (typed_false tint (Val.of_bool x) -> P).
+    (typed_false tint (bool2val x) -> P).
 Proof.
 intuition.
 apply H, typed_false_of_bool; auto.
@@ -1851,7 +1851,7 @@ Qed.
 Lemma typed_true_of_bool':
  forall x (P: Prop),
     ((x=true) -> P) ->
-    (typed_true tint (Val.of_bool x) -> P).
+    (typed_true tint (bool2val x) -> P).
 Proof.
 intuition.
 apply H, typed_true_of_bool; auto.
@@ -1881,9 +1881,9 @@ Ltac intro_if_new :=
           let H := fresh "P" x in intro H
   | |- is_pointer_or_null ?x =>
           let H := fresh "PN" x in intro H
-  | |- typed_false _ (Val.of_bool _) -> _ =>
+  | |- typed_false _ (bool2val _) -> _ =>
           simple apply typed_false_of_bool'
-  | |- typed_true _ (Val.of_bool _) -> _ =>
+  | |- typed_true _ (bool2val _) -> _ =>
           simple apply typed_true_of_bool'
   | |- ptr_eq _ _ -> _ =>
           apply ptr_eq_e'

floyd/compare_lemmas.v

@@ -53,14 +53,16 @@ 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.
- unfold sem_cmp_pp, strict_bool_val, nullval in *.
- destruct Archi.ptr64  eqn:Hp; simpl in H1;
- try solve [inv H1];
- try solve [pose proof (Int64.eq_spec i Int64.zero);
-                destruct (Int64.eq i Int64.zero); inv H1; auto];
- try solve [pose proof (Int.eq_spec i Int.zero);
-                destruct (Int.eq i Int.zero); inv H1; auto].
+ simpl in H.
+ red in H.
+ forget (v rho) as x. clear - H.
+ unfold sem_cmp_pp, strict_bool_val, nullval in *; simpl in *.
+ destruct Archi.ptr64; simpl in H;
+ destruct x; inv H.
+ - pose proof (Int64.eq_spec i Int64.zero);
+                destruct (Int64.eq i Int64.zero); inv H1; auto.
+ - pose proof (Int.eq_spec i Int.zero);
+                destruct (Int.eq i Int.zero); inv H1; auto.
 Qed.
 
 Definition  binary_operation_to_comparison (op: Cop.binary_operation) :=