anomaly non functional construction in zify

[SkySkimmer]

From Coq Require Import Program.Basics.
From Coq Require Import Vectors.Vector.

Import VectorNotations.

Require Import Lia.
Require Import ZArith.
Import ZifyClasses.

Definition Vec (n : nat) (a : Type) : Type := VectorDef.t a n.
Notation bitvector n := (Vec n bool).

(* Workaround for https://github.com/coq/coq/issues/16803 *)
Constraint Vec.u1 <= mkapp2.u0.
Constraint Vec.u1 <= mkapp2.u1.
Constraint Vec.u1 <= mkapp2.u2.
Constraint Vec.u1 <= mkrel.u0.

Definition bvToInt : forall w, bitvector w -> Z. Admitted.
Definition bvAdd : forall w, bitvector w -> bitvector w -> bitvector w. Admitted.

Axiom w : nat.

Definition bitvector_w := bitvector w.

(* now we have to use of_nat since w : nat *)
Notation modulus := (Z.pow 2 (Z.of_nat w)).

Global Program Instance Inj_bv_Z : InjTyp bitvector_w Z :=
  { inj := bvToInt w
  ; pred := fun x => Z.le 0 x /\ Z.lt x modulus
  }.
Next Obligation.
Admitted.

Global Program Instance Rel_eq_bv : BinRel (@eq bitvector_w) :=
  { TR := @eq Z
  }.
Next Obligation.
Admitted.

Global Program Instance Op_bvAdd : BinOp (bvAdd w : bitvector_w -> bitvector_w -> bitvector_w) :=
  { TBOp := fun x y => Z.modulo (Z.add x y) modulus
  }.
Next Obligation.
Admitted.

Add Zify InjTyp Inj_bv_Z.
Add Zify BinRel Rel_eq_bv.
Add Zify BinOp Op_bvAdd.

Module Good.

Axiom intToBv : Z -> bitvector w.
Axiom intToBv_ok : forall x, (bvToInt w (intToBv x) = x mod (Z.pow 2 (Z.of_nat w)))%Z.

#[export] Program Instance i2bv : UnOpSpec (intToBv : Z -> bitvector_w) :=
  { UPred := fun x b => bvToInt w b = (x mod modulus)%Z }.
Next Obligation. (* bvToInt w (intToBv x) = (x mod modulus)%Z *)
  apply intToBv_ok.
Qed.
Add Zify UnOpSpec i2bv.

End Good.

Module Bad.

Axiom intToBv : forall {w}, Z -> bitvector w.
Axiom intToBv_ok : forall w x, (bvToInt w (intToBv x) = x mod (Z.pow 2 (Z.of_nat w)))%Z.

#[export] Program Instance i2bv : UnOpSpec (@intToBv w : Z -> bitvector_w) :=
  { UPred := fun x b => bvToInt w b = (x mod modulus)%Z }.
Next Obligation. (* bvToInt w (intToBv x) = (x mod modulus)%Z *)
  apply intToBv_ok.
Qed.
Add Zify UnOpSpec i2bv.

End Bad.

Ltac hook :=
  repeat match goal with
      H : bvToInt _ _ = _ |- _ => rewrite H;clear H
    end.

Ltac Zify.zify_post_hook ::= hook.

(* if Bad imported instead, zify will anomaly non functional construction
   it tries to do
   "Pose (H2, (i2bv_obligation_1 w 0%Z))"
   where the "w" argument was gotten from (intToBv w 0) in spec_of_term but should not be there
 *)
Import Good.

Lemma test_bvAdd_max_1 : bvAdd w (intToBv (modulus - 1)) (intToBv 1) = intToBv 0.
Proof.
  zify;simpl in *. (* anomaly here if Bad was imported *)
  rewrite Zmod_0_l.
  rewrite <-Zplus_mod.
  rewrite <-(Z_mod_same_full modulus).
  f_equal;lia.
Qed.

Not sure if this is supposed to be supported, but at least it shouldn't anomaly.