repr_inj handles int64 compares better; updated submodules

floyd/forward.v

@@ -2099,11 +2099,14 @@ Lemma typed_true_ptr' :
   typed_true (tptr t) v -> isptr v.
 Proof. intros ? ?. apply typed_true_ptr. Qed.
 
+
 Ltac do_repr_inj H :=
    simpl typeof in H;  (* this 'simpl' should be fine, since its argument is just clightgen-produced ASTs *)
+   cbv delta [Int64.zero Int.zero] in H;
    lazymatch type of H with
       | typed_true _ ?A => 
            change (typed_true tuint) with (typed_true tint) in H;
+           change (typed_true tulong) with (typed_true tlong) in H;
           let B := eval hnf in A in change A with B in H;
           try first
                [ simple apply typed_true_of_bool' in H
@@ -2115,20 +2118,23 @@ Ltac do_repr_inj H :=
                | simple apply typed_true_Ceq_eq' in H
                | apply typed_true_nullptr4 in H
                | simple apply typed_true_Cne_neq' in H
+               | simple apply typed_true_tlong_Vlong in H
               ]
       | typed_false _ ?A => 
            change (typed_false tuint) with (typed_false tint) in H;
+           change (typed_false tulong) with (typed_false tlong) in H;
            let B := eval hnf in A in change A with B in H;
            try first
                [ simple apply typed_false_of_bool' in H
                | simple apply typed_false_ptr_e in H
-               | simple apply typed_false_negb_bool_val_p in H; [| solve [auto]]
+               | simple apply typed_false_negb_bool_val_p in H; [| solve [auto ] ]
                | apply typed_false_negb_bool_val_p' in H
                | simple apply typed_false_tint_Vint in H
                | apply typed_false_nullptr3 in H
                | simple apply typed_false_Ceq_neq' in H
                | apply typed_false_nullptr4 in H
                | simple apply typed_false_Cne_eq' in H
+               | simple apply typed_false_tlong_Vlong in H
                ]
      | _ => idtac
     end;
@@ -2152,6 +2158,8 @@ Ltac do_repr_inj H :=
   end;
   first [ simple apply repr_inj_signed in H; [ | rep_lia | rep_lia ]
          | simple apply repr_inj_unsigned in H; [ | rep_lia | rep_lia ]
+         | simple apply repr_inj_signed64 in H; [ | rep_lia | rep_lia ]
+         | simple apply repr_inj_unsigned64 in H; [ | rep_lia | rep_lia ]
          | simple apply repr_inj_signed' in H; [ | rep_lia | rep_lia ]
          | simple apply repr_inj_unsigned' in H; [ | rep_lia | rep_lia ]
          | simple apply ltu_repr in H; [ | rep_lia | rep_lia]

floyd/functional_base.v

@@ -724,6 +724,18 @@ rewrite <- (Int.signed_repr j) by rep_lia.
 congruence.
 Qed.
 
+Lemma repr_inj_signed64:
+  forall i j,
+    Int64.min_signed <= i <= Int.max_signed ->
+    Int64.min_signed <= j <= Int.max_signed ->
+    Int64.repr i = Int64.repr j -> i=j.
+Proof.
+intros.
+rewrite <- (Int64.signed_repr i) by rep_lia.
+rewrite <- (Int64.signed_repr j) by rep_lia.
+congruence.
+Qed.
+
 Lemma repr_inj_unsigned:
   forall i j,
     0 <= i <= Int.max_unsigned ->

floyd/val_lemmas.v

@@ -447,6 +447,15 @@ pose proof (Int64.eq_spec v Int64.zero).
 destruct (Int64.eq v Int64.zero); auto. inv H.
 Qed.
 
+Lemma typed_false_tlong_Vlong:
+  forall v, typed_false tlong (Vlong v) -> v = Int64.zero.
+Proof.
+intros.
+unfold typed_false, strict_bool_val in H. simpl in H.
+pose proof (Int64.eq_spec v Int64.zero).
+destruct (Int64.eq v Int64.zero); auto. discriminate.
+Qed.
+
 Ltac intro_redundant P :=
  match goal with H: P |- _ => idtac end.