Sometimes minimizer does not work

[JasonGross]

rocq-prover/rocq#17888 (comment)
Minimized File /github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto_legacy/src/Primitives/EdDSARepChange.v (from ci-fiat_crypto_legacy) (full log on GitHub Actions)

We are collecting data on the user experience of the Coq Bug Minimizer.
If you haven't already filled the survey for this PR, please fill out our short survey!

Minimized Coq File (consider adding this file to the test-suite)

Require Coq.Init.Ltac.
Module Export AdmitTactic.
Module Import LocalFalse.
Inductive False : Prop := .
End LocalFalse.
Axiom proof_admitted : False.
Import Coq.Init.Ltac.
Tactic Notation "admit" := abstract case proof_admitted.
End AdmitTactic.
Require Import Coq.ZArith.ZArith.
Require Import Crypto.Util.FixCoqMistakes.
Require Import Crypto.Spec.EdDSA bbv.WordScope.
Require Import Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop Coq.Relations.Relation_Definitions.
Require Import Crypto.Algebra.Monoid Crypto.Algebra.Group Crypto.Algebra.ScalarMult.
Require Import Crypto.Util.Decidable Crypto.Util.Option.
Require Import Crypto.Util.Tactics.SetEvars.
Require Import Crypto.Util.Tactics.SubstEvars.
Require Import Crypto.Util.Tactics.BreakMatch.
Require Import Crypto.Util.Tactics.SpecializeBy.
Require Import Coq.micromega.Lia Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop.
Require Import Crypto.Util.Notations.
Require Import Crypto.Util.Option Crypto.Util.Logic Crypto.Util.Relations Crypto.Util.WordUtil Crypto.Util.LetIn Crypto.Util.NatUtil.
Require Import Crypto.Spec.ModularArithmetic Crypto.Arithmetic.PrimeFieldTheorems.
Import Coq.Numbers.Natural.Peano.NPeano.

Import Notations.

Section EdDSA.
  Context `{prm:EdDSA}.
  Local Infix "==" := Eeq. Local Infix "+" := Eadd. Local Infix "*" := ZEmul.

  Local Notation valid := (@valid E Eeq Eadd ZEmul b H l B Eenc Senc).
  Lemma sign_valid : forall A_ sk {n} (M:word n), A_ = public sk -> valid M A_ (sign A_ sk M).
  Proof using Type.
    cbv [sign public Spec.EdDSA.valid]; intros; subst;
      repeat match goal with
             | |- exists _, _ => eexists
             | |- _ /\ _ => eapply conj
             | |- _ => reflexivity
             end.
    rewrite F.to_Z_of_Z, scalarmult_mod_order, scalarmult_add_l, cancel_left, scalarmult_mod_order, Z.mul_comm, scalarmult_assoc;
      try solve [ reflexivity
                | setoid_rewrite (*unify 0*) (Z2Nat.inj_iff _ 0); pose proof EdDSA_l_odd; lia
                | pose proof EdDSA_l_odd; lia
                | apply EdDSA_l_order_B
                | rewrite scalarmult_assoc, Z.mul_comm, <-scalarmult_assoc,
                  EdDSA_l_order_B, scalarmult_zero_r; reflexivity].
  Qed.

  Lemma solve_for_R_sig : forall s B R n A, { solution | s * B == R + n * A <-> R == solution }.
  Proof.
    eexists.
    set_evars.
    setoid_rewrite <-(symmetry_iff(R:=Eeq)) at 1.
    setoid_rewrite <-eq_r_opp_r_inv.
    setoid_rewrite <-scalarmult_opp_r.
    subst_evars.
    reflexivity.
  Defined.
  Definition solve_for_R := Eval cbv [proj2_sig solve_for_R_sig] in (fun s B R n A => proj2_sig (solve_for_R_sig s B R n A)).

  Context {Proper_Eenc : Proper (Eeq==>Logic.eq) Eenc}.
  Global Instance Proper_eq_Eenc ref : Proper (Eeq ==> iff) (fun P => Eenc P = ref).
  Proof using Proper_Eenc. intros ? ? Hx; rewrite Hx; reflexivity. Qed.

  Context {Edec:word b-> option E}   {eq_enc_E_iff: forall P_ P, Eenc P = P_ <-> option_eq Eeq (Edec P_) (Some P)}.
  Context {Sdec:word b-> option (F l)} {eq_enc_S_iff: forall n_ n, Senc n = n_ <-> Sdec n_ = Some n}.

  Local Infix "++" := combine.
  Definition verify'_sig : { verify | forall mlen (message:word mlen) (pk:word b) (sig:word (b+b)),
      verify mlen message pk sig = true <-> valid message pk sig }.
  Proof.
    eexists; intros mlen message pk sig; set_evars.
    unfold Spec.EdDSA.valid.
    setoid_rewrite solve_for_R.
    setoid_rewrite combine_eq_iff.
    setoid_rewrite and_comm at 4. setoid_rewrite and_assoc. repeat setoid_rewrite exists_and_indep_l.
    setoid_rewrite (and_rewrite_l Eenc (split1 b b sig)
                            (fun x y => x == _ * B + Z.of_nat (wordToNat (H _ (y ++ Eenc _ ++ message))) mod _ * Eopp _)); setoid_rewrite eq_enc_S_iff.
    setoid_rewrite (@exists_and_equiv_r _ _ _ _ _ _).
    setoid_rewrite <- (fun A => and_rewriteleft_l (fun x => x) (Eenc A) (fun pk EencA => exists a,
        Sdec (split2 b b sig) = Some a /\
        Eenc (_ * B + Z.of_nat (wordToNat (H (b + (b + mlen)) (split1 b b sig ++ EencA ++ message))) mod _ * Eopp A)
        = split1 b b sig)). setoid_rewrite (eq_enc_E_iff pk).
    setoid_rewrite <-weqb_true_iff.
    setoid_rewrite <-option_rect_false_returns_true_iff_eq.
    rewrite <-option_rect_false_returns_true_iff by
     (intros ? ? Hxy; unfold option_rect; break_match; rewrite <-?Hxy; reflexivity).

    subst_evars.
    eapply reflexivity.
  Defined.
  Definition verify' {mlen} (message:word mlen) (pk:word b) (sig:word (b+b)) : bool :=
    Eval cbv [proj1_sig verify'_sig] in proj1_sig verify'_sig mlen message pk sig.
  Lemma verify'_correct : forall {mlen} (message:word mlen) pk sig,
    verify' message pk sig = true <-> valid message pk sig.
  Proof using Type*. exact (proj2_sig verify'_sig). Qed.

  Section ChangeRep.
    Context {Erep ErepEq ErepAdd ErepId ErepOpp} {Agroup:@Algebra.Hierarchy.group Erep ErepEq ErepAdd ErepId ErepOpp}.
    Context {EToRep} {Ahomom:@is_homomorphism E Eeq Eadd Erep ErepEq ErepAdd EToRep}.

    Context {ERepEnc : Erep -> word b}
            {ERepEnc_correct : forall P:E, Eenc P = ERepEnc (EToRep P)}
            {Proper_ERepEnc:Proper (ErepEq==>Logic.eq) ERepEnc}.

    Context {ERepDec : word b -> option Erep}
            {ERepDec_correct : forall w, option_eq ErepEq (ERepDec w) (option_map EToRep (Edec w)) }.

    Context {SRep SRepEq} `{@Equivalence SRep SRepEq} {S2Rep:F l->SRep}.

    Context {SRepDecModL} {SRepDecModL_correct: forall (w:word (b+b)), SRepEq (S2Rep (F.of_Z _ (Z.of_nat (wordToNat w)))) (SRepDecModL w)}.

    Context {SRepERepMul:SRep->Erep->Erep}
            {SRepERepMul_correct:forall n P, ErepEq (EToRep ((n mod l)*P)) (SRepERepMul (S2Rep (F.of_Z _ n)) (EToRep P))}
            {Proper_SRepERepMul: Proper (SRepEq==>ErepEq==>ErepEq) SRepERepMul}.

    Context {SRepDec: word b -> option SRep}
            {SRepDec_correct : forall w, option_eq SRepEq (option_map S2Rep (Sdec w)) (SRepDec w)}.

    Definition verify_using_representation
               {mlen} (message:word mlen) (pk:word b) (sig:word (b+b))
               : { answer | answer = verify' message pk sig }.
    Proof.
      eexists.
      pose proof EdDSA_l_odd.
      cbv [verify'].

      etransitivity. Focus 2. {
        eapply Proper_option_rect_nd_changebody; [intro|reflexivity].
        eapply Proper_option_rect_nd_changebody; [intro|reflexivity].
        rewrite <-F.mod_to_Z by lia.
        repeat (
            rewrite ERepEnc_correct
            || rewrite homomorphism
            || rewrite homomorphism_id
            || rewrite (homomorphism_inv(INV:=Eopp)(inv:=ErepOpp)(eq:=ErepEq)(phi:=EToRep))
            || rewrite SRepERepMul_correct
            || rewrite SdecS_correct
            || rewrite SRepDecModL_correct
            || rewrite (@F.of_Z_to_Z _ _)
            || rewrite (@F.mod_to_Z _ _)
          ).
        reflexivity.
      } Unfocus.

      (* lazymatch goal with |- _ _ (option_rect _ ?some _ _) => idtac some end. *)
      setoid_rewrite (option_rect_option_map EToRep
           (fun s =>
            option_rect (fun _ : option _ => bool)
              (fun s0 =>
               weqb
                 (ERepEnc
                    (ErepAdd (SRepERepMul (_ s0) (EToRep B))
                       (SRepERepMul
                          (SRepDecModL
                             (H _ (split1 b b sig ++ pk ++ message)))
                          (ErepOpp (s))))) (split1 b b sig)) false
              (Sdec (split2 b b sig)))
           false).
      (* rewrite with a complicated proper instance for inline code .. *)
      etransitivity;
        [| eapply Proper_option_rect_nd_changevalue;
           [
           | reflexivity
           | eapply ERepDec_correct
           ];
           [ repeat match goal with
                    | |- _ => intro
                    | |- _ => eapply Proper_option_rect_nd_changebody
                    | |- ?R ?x ?x => reflexivity
                    | H : _ |- _ => rewrite H; reflexivity
                    end
           ]
        ].

      etransitivity. Focus 2. {
        eapply Proper_option_rect_nd_changebody; [intro|reflexivity].
        set_evars.
        setoid_rewrite (option_rect_option_map S2Rep
            (fun s0 =>
             weqb
               (ERepEnc
                  (ErepAdd (SRepERepMul (s0) (EToRep B))
                     (SRepERepMul
                        (SRepDecModL (H _ (split1 b b sig ++ pk ++ message)))
                        (ErepOpp _)))) (split1 b b sig))

                   false).
        subst_evars.

        eapply Proper_option_rect_nd_changevalue;
          [repeat intro; repeat f_equiv; eassumption|reflexivity|..].

        symmetry.
        eapply SRepDec_correct.
      } Unfocus.

      reflexivity.
    Defined.

    Definition verify {mlen} (msg:word mlen) pk sig :=
      Eval cbv beta iota delta [proj1_sig verify_using_representation] in
      proj1_sig (verify_using_representation msg pk sig).
    Lemma verify_correct {mlen} (msg:word mlen) pk sig : verify msg pk sig = true <-> valid msg pk sig.
    Proof using Type*.
      etransitivity; [|eapply (verify'_correct msg pk sig)].
      eapply iff_R_R_same_r, (proj2_sig (verify_using_representation _ _ _)).
    Qed.

    Context {SRepEnc : SRep -> word b}
            {SRepEnc_correct : forall x, Senc x = SRepEnc (S2Rep x)}
            {Proper_SRepEnc:Proper (SRepEq==>Logic.eq) SRepEnc}.
    Context {SRepAdd : SRep -> SRep -> SRep}
            {SRepAdd_correct : forall x y, SRepEq (S2Rep (x+y)%F) (SRepAdd (S2Rep x) (S2Rep y)) }
            {Proper_SRepAdd:Proper (SRepEq==>SRepEq==>SRepEq) SRepAdd}.
    Context {SRepMul : SRep -> SRep -> SRep}
            {SRepMul_correct : forall x y, SRepEq (S2Rep (x*y)%F) (SRepMul (S2Rep x) (S2Rep y)) }
            {Proper_SRepMul:Proper (SRepEq==>SRepEq==>SRepEq) SRepMul}.
    Context {ErepB:Erep} {ErepB_correct:ErepEq ErepB (EToRep B)}.

    Context {SRepDecModLShort} {SRepDecModLShort_correct: forall (w:word (n+1)), SRepEq (S2Rep (F.of_nat _ (wordToNat w))) (SRepDecModLShort w)}.

    (* We would ideally derive the optimized implementations from
    specifications using `setoid_rewrite`, but doing this without
    inlining let-bound subexpressions turned out to be quite messy in
    the current state of Coq: <https://github.com/mit-plv/fiat-crypto/issues/64> *)

    Let n_le_bpb : (n <= b+b)%nat. destruct prm. lia. Qed.

    (* TODO: change impl to basesystem *)
    Context (splitSecretPrngCurve : forall (sk:word b), SRep * word b).
    Context (splitSecretPrngCurve_correct : forall sk,
      let (s, r) := splitSecretPrngCurve sk in
      SRepEq s (S2Rep (F.of_Z l (curveKey sk))) /\ r = prngKey (H:=H) sk).

    Definition sign (pk sk : word b) {mlen} (msg:word mlen) :=
      dlet sp := splitSecretPrngCurve sk in
      dlet s := fst sp in
      dlet p := snd sp in
      dlet r := SRepDecModL (H _ (p ++ msg)) in
      dlet R := SRepERepMul r ErepB in
      dlet S := SRepAdd r (SRepMul (SRepDecModL (H _ (ERepEnc R ++ pk ++ msg))) s) in
      ERepEnc R ++ SRepEnc S.

    Lemma Z_l_nonzero : Z.pos l <> 0%Z. discriminate. Qed.

    Lemma sign_correct (pk sk : word b) {mlen} (msg:word mlen)
               : sign pk sk msg = EdDSA.sign pk sk msg.
    Proof using Agroup Ahomom ERepEnc_correct ErepB_correct H0 Proper_ERepEnc Proper_SRepAdd Proper_SRepERepMul Proper_SRepEnc Proper_SRepMul SRepAdd_correct SRepDecModLShort_correct SRepDecModL_correct SRepERepMul_correct SRepEnc_correct SRepMul_correct splitSecretPrngCurve_correct.
      cbv [sign EdDSA.sign Let_In].

      let H := fresh "H" in
      pose proof (splitSecretPrngCurve_correct sk) as H;
        destruct (splitSecretPrngCurve sk);
        destruct H as [curveKey_correct prngKey_correct].

      repeat (
          reflexivity
          || rewrite ERepEnc_correct
          || rewrite SRepEnc_correct
          || rewrite SRepDecModL_correct
          || rewrite SRepERepMul_correct
          || rewrite (F.of_Z_add (m:=l))
          || rewrite (F.of_Z_mul (m:=l))
          || rewrite SRepAdd_correct
          || rewrite SRepMul_correct
          || rewrite ErepB_correct
          || rewrite <-prngKey_correct
          || rewrite <-curveKey_correct
          || eapply (f_equal2 (fun a b => a ++ b))
          || f_equiv
          || rewrite <-(scalarmult_mod_order l B Z_l_nonzero EdDSA_l_order_B), SRepERepMul_correct
        ).
    Qed.
  End ChangeRep.
End EdDSA.

Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted)

Build Log (contains the Coq error message) (truncated to last 8.0KiB; full 11MiB file on GitHub Actions Artifacts under build.log)

r0 : (0 <= Z.of_nat n)%Z := Nat2Z.is_nonneg n in
                    let cstr1 : (0 <= Z.of_nat b)%Z := Nat2Z.is_nonneg b in
                    let cstr2 : (0 <= Z.of_nat c)%Z := Nat2Z.is_nonneg c in
                    let __arith :
                      forall __x3 __x2 __x1 : Z,
                      __x3 = 2%Z \/ __x3 = 3%Z ->
                      (__x1 >= __x3)%Z ->
                      (__x1 <= __x2)%Z -> (__x1 <= __x2 + __x2)%Z :=
                      fun __x3 __x2 __x1 : Z =>
                      let __wit :=
                        (ZMicromega.RatProof
                           (RingMicromega.PsatzAdd
                              (RingMicromega.PsatzMulC 
                                 (EnvRing.Pc (-1)%Z)
                                 (RingMicromega.PsatzIn Z 3))
                              (RingMicromega.PsatzAdd
                                 (RingMicromega.PsatzIn Z 2)
                                 (RingMicromega.PsatzAdd
                                    (RingMicromega.PsatzMulE
                                       (RingMicromega.PsatzC 2%Z)
                                       (RingMicromega.PsatzIn Z 1))
                                    (RingMicromega.PsatzIn Z 0))))
                           ZMicromega.DoneProof
                         :: ZMicromega.RatProof
                              (RingMicromega.PsatzAdd
                                 (RingMicromega.PsatzMulC 
                                    (EnvRing.Pc (-1)%Z)
                                    (RingMicromega.PsatzIn Z 3))
                                 (RingMicromega.PsatzAdd
                                    (RingMicromega.PsatzIn Z 2)
                                    (RingMicromega.PsatzAdd
                                       (RingMicromega.PsatzMulE
                                          (RingMicromega.PsatzC 2%Z)
                                          (RingMicromega.PsatzIn Z 1))
                                       (RingMicromega.PsatzIn Z 0))))
                              ZMicromega.DoneProof :: nil)%list in
                      let __varmap :=
                        VarMap.Branch
                          (VarMap.Branch (VarMap.Elt __x3) __x2 VarMap.Empty)
                          __x1 VarMap.Empty in
                      let __ff :=
                        Tauto.IMPL
                          (Tauto.OR
                             (Tauto.A Tauto.isProp
                                {|
                                  RingMicromega.Flhs := EnvRing.PEX 4;
                                  RingMicromega.Fop := RingMicromega.OpEq;
                                  RingMicromega.Frhs := EnvRing.PEc 2%Z
                                |} tt)
                             (Tauto.A Tauto.isProp
                                {|
                                  RingMicromega.Flhs := EnvRing.PEX 4;
                                  RingMicromega.Fop := RingMicromega.OpEq;
                                  RingMicromega.Frhs := EnvRing.PEc 3%Z
                                |} tt)) None
                          (Tauto.IMPL
                             (Tauto.A Tauto.isProp
                                {|
                                  RingMicromega.Flhs := EnvRing.PEX 1;
                                  RingMicromega.Fop := RingMicromega.OpGe;
                                  RingMicromega.Frhs := EnvRing.PEX 4
                                |} tt) None
                             (Tauto.IMPL
                                (Tauto.A Tauto.isProp
                                   {|
                                     RingMicromega.Flhs := EnvRing.PEX 1;
                                     RingMicromega.Fop := RingMicromega.OpLe;
                                     RingMicromega.Frhs := EnvRing.PEX 2
                                   |} tt) None
                                (Tauto.A Tauto.isProp
                                   {|
                                     RingMicromega.Flhs := EnvRing.PEX 1;
                                     RingMicromega.Fop := RingMicromega.OpLe;
                                     RingMicromega.Frhs :=
                                       EnvRing.PEadd 
                                         (EnvRing.PEX 2) 
                                         (EnvRing.PEX 2)
                                   |} tt))) in
                      ZMicromega.ZTautoChecker_sound __ff __wit
                        (eq_refl
                         <:
                         ZMicromega.ZTautoChecker __ff __wit = true)
                        (VarMap.find 0%Z __varmap) in
                    __arith (Z.of_nat c) (Z.of_nat b) 
                      (Z.of_nat n) EdDSA_c_valid1 EdDSA_n_ge_c1 EdDSA_n_le_b1))
                  EdDSA_group EdDSA_scalarmult EdDSA_c_valid EdDSA_n_ge_c
                  EdDSA_n_le_b EdDSA_B_not_identity EdDSA_l_prime EdDSA_l_odd
                  EdDSA_l_order_B
            end : (n <= b + b)%nat
splitSecretPrngCurve : word b -> SRep * word b
splitSecretPrngCurve_correct : forall sk : word b,
                               let (s, r) := splitSecretPrngCurve sk in
                               SRepEq s (S2Rep (F.of_Z l (curveKey sk))) /\
                               r = prngKey sk
pk : word b
sk : word b
mlen : nat
msg : word mlen
The term "pk" has type "word b" while it is expected to have type
 "word b -> ?SRep * word b".

Command exited with non-zero status 1
src/Primitives/EdDSARepChange.vo (real: 4.05, user: 3.78, sys: 0.27, mem: 530592 ko)
Makefile.coq:823: recipe for target 'src/Primitives/EdDSARepChange.vo' failed
make[1]: *** [src/Primitives/EdDSARepChange.vo] Error 1
make[1]: Leaving directory '/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto_legacy'
Aggregating timing log...
    Time |  Peak Mem | File Name                                              
------------------------------------------------------------------------------
2m57.08s | 897980 ko | Total Time / Peak Mem                                  
------------------------------------------------------------------------------
1m04.46s | 612104 ko | Arithmetic/Karatsuba.vo                                
0m24.15s | 577732 ko | Arithmetic/Core.vo                                     
0m17.11s | 897980 ko | Curves/Edwards/XYZT/Basic.vo                           
0m15.10s | 544916 ko | Arithmetic/Saturated/AddSub.vo                         
0m11.51s | 560240 ko | Arithmetic/Saturated/Core.vo                           
0m10.65s | 546668 ko | Arithmetic/Saturated/MontgomeryAPI.vo                  
0m07.41s | 528760 ko | Arithmetic/Saturated/MulSplit.vo                       
0m04.97s | 541116 ko | Arithmetic/MontgomeryReduction/WordByWord/Proofs.vo    
0m03.91s | 564184 ko | Compilers/Z/Bounds/Pipeline/Definition.vo              
0m03.78s | 530592 ko | Primitives/EdDSARepChange.vo                           
0m03.16s | 529108 ko | Arithmetic/Saturated/Freeze.vo                         
0m01.69s | 527588 ko | Arithmetic/CoreUnfolder.vo                             
0m01.26s | 527988 ko | Curves/Edwards/XYZT/Precomputed.vo                     
0m01.01s | 530632 ko | Arithmetic/Saturated/CoreUnfolder.vo                   
0m00.91s | 531896 ko | Arithmetic/Saturated/WrappersUnfolder.vo               
0m00.87s | 532428 ko | Arithmetic/Saturated/UniformWeight.vo                  
0m00.76s | 567912 ko | Compilers/Z/Bounds/Pipeline/ReflectiveTactics.vo       
0m00.70s | 529928 ko | Arithmetic/Saturated/MulSplitUnfolder.vo               
0m00.66s | 538288 ko | Compilers/Z/Bounds/Pipeline.vo                         
0m00.64s | 530404 ko | Arithmetic/Saturated/FreezeUnfolder.vo                 
0m00.62s | 511088 ko | Arithmetic/MontgomeryReduction/WordByWord/Definition.vo
0m00.61s | 498212 ko | Arithmetic/Saturated/Wrappers.vo                       
0m00.58s | 478004 ko | Compilers/Z/Bounds/MapCastByDeBruijnWf.vo              
0m00.57s | 492684 ko | Arithmetic/Saturated/UniformWeightInstances.vo         
Makefile.ci:155: recipe for target 'ci-fiat_crypto_legacy' failed
make: *** [ci-fiat_crypto_legacy] Error 2
/github/workspace/builds/coq /github/workspace
::endgroup::

Minimization Log

Coq version: 8.19+alpha compiled with OCaml 4.14.1


First, I will attempt to absolutize relevant [Require]s in /github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto_legacy/src/Primitives/EdDSARepChange.v, and store the result in /github/workspace/cwd/bug_01.v...
getting /github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto_legacy/src/Primitives/EdDSARepChange.v
getting /github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto_legacy/src/Primitives/EdDSARepChange.glob

Now, I will attempt to coq the file, and find the error...

Coqing the file (/github/workspace/cwd/bug_01.v)...

Running command: "/github/workspace/builds/coq/coq-failing/_install_ci/bin/coqc.orig" "-q" "-w" "-deprecated-hint-rewrite-without-locality,+deprecated-hint-without-locality,+deprecated-instance-without-locality,unsupported-attributes" "-w" "-notation-overridden" "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto_legacy/src" "Crypto" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto_legacy/bbv/src/bbv" "bbv" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Ltac2" "Ltac2" "-top" "Crypto.Primitives.EdDSARepChange" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto_legacy/coqprime/src" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto_legacy/coqprime/src/Coqprime" "Coqprime" "-R" "/tmp/tmpsbukrjx2" "" "/tmp/tmpsbukrjx2/Crypto/Primitives/EdDSARepChange.v" "-q"

The timeout for /github/workspace/builds/coq/coq-failing/_install_ci/bin/coqc.orig has been set to: 3

This file produces the following output when Coq'ed:
Error:
More than one file to compile: /github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto_legacy/coqprime/src/Coqprime



The current state of the file does not have a recognizable error.
Traceback (most recent call last):
  File "/github/workspace/coq-tools/find-bug.py", line 1470, in <module>
    env['error_reg_string'] = get_error_reg_string(output_file_name, **env)
  File "/github/workspace/coq-tools/find-bug.py", line 284, in get_error_reg_string
    error_reg_string = get_error_reg_string_of_output(output, **kwargs)
  File "/github/workspace/coq-tools/find-bug.py", line 246, in get_error_reg_string_of_output
    error_reg_string = raw_input('\nPlease enter a regular expression which matches on the output.  Leave blank to re-coq the file.\n')
EOFError: EOF when reading a line

If you have any comments on your experience of the minimizer, please share them in a reply (possibly tagging @JasonGross).
If you believe there's a bug in the bug minimizer, please report it on the bug minimizer issue tracker.

[JasonGross]

Somehow passed things in COQPATH on the command line
bug.verbose.log.zip

@JasonGross, Minimized File /github/workspace/fiat-crypto/src/Experiments/SimplyTypedArithmetic.v (full log on GitHub Actions)

Minimized Coq File (truncated to 32KiB; full 584KiB file on GitHub Actions Artifacts under bug.v)

(* Following http://adam.chlipala.net/theses/andreser.pdf chapter 3 *)
Require Coq.Init.Ltac.
Module Export AdmitTactic.
Module Import LocalFalse.
Inductive False : Prop := .
End LocalFalse.
Axiom proof_admitted : False.
Import Coq.Init.Ltac.
Tactic Notation "admit" := abstract case proof_admitted.
End AdmitTactic.
Require Import Coq.ZArith.ZArith Coq.micromega.Lia Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop Crypto.Algebra.Nsatz.
Require Import Coq.Strings.String.
Require Import Coq.MSets.MSetPositive.
Require Import Coq.FSets.FMapPositive.
Require Import Coq.derive.Derive.
Require Import Crypto.Util.Pointed.
Require Import Crypto.Util.Tactics.UniquePose Crypto.Util.Decidable.
Require Import Crypto.Util.Tuple Crypto.Util.Prod Crypto.Util.LetIn.
Require Import Crypto.Util.ListUtil Coq.Lists.List Crypto.Util.NatUtil.
Require Import QArith.QArith_base QArith.Qround Crypto.Util.QUtil.
Require Import Crypto.Algebra.Ring Crypto.Util.Decidable.Bool2Prop.
Require Import Crypto.Algebra.Ring.
Require Import Crypto.Algebra.SubsetoidRing.
Require Import Crypto.Arithmetic.PrimeFieldTheorems.
Require Import Crypto.Arithmetic.BarrettReduction.Generalized.
Require Import Crypto.Arithmetic.MontgomeryReduction.Definition.
Require Import Crypto.Arithmetic.MontgomeryReduction.Proofs.
Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo.
Require Import Crypto.Util.ZRange.
Require Import Crypto.Util.ZRange.Operations.
Require Import Crypto.Util.Tactics.RunTacticAsConstr.
Require Import Crypto.Util.Tactics.Head.
Require Import Crypto.Util.Option.
Require Import Crypto.Util.OptionList.
Require Import Crypto.Util.Sum.
Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div Crypto.Util.ZUtil.Hints.Core.
Require Import Crypto.Util.ZUtil.Hints.PullPush.
Require Import Crypto.Util.ZUtil.AddGetCarry Crypto.Util.ZUtil.MulSplit.
Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo.
Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem.
Require Import Crypto.Util.ZUtil.Le.
Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall.
Require Import Crypto.Util.ZUtil.Log2.
Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds.
Require Import Crypto.Util.ZUtil.Notations.
Require Import Crypto.Util.ZUtil.Shift.
Require Import Crypto.Util.ZUtil.LandLorShiftBounds.
Require Import Crypto.Util.ZUtil.Testbit.
Require Import Crypto.Util.ZUtil.Notations.
Require Import Crypto.Util.Tactics.SpecializeBy.
Require Import Crypto.Util.Tactics.SplitInContext.
Require Import Crypto.Util.Tactics.SubstEvars.
Require Crypto.Util.Strings.String.
Require Import Crypto.Util.Strings.Decimal.
Require Import Crypto.Util.Strings.HexString.
Require Import Crypto.Util.Notations.
Require Import Crypto.Util.ZUtil.Definitions.
Require Import Crypto.Util.ZUtil.CC Crypto.Util.ZUtil.Rshi.
Require Import Crypto.Util.ZUtil.Zselect Crypto.Util.ZUtil.AddModulo.
Require Import Crypto.Util.ZUtil.AddGetCarry Crypto.Util.ZUtil.MulSplit.
Require Import Crypto.Util.ZUtil.Hints.Core.
Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div.
Require Import Crypto.Util.ZUtil.Hints.PullPush.
Require Import Crypto.Util.ZUtil.EquivModulo.
Require Import Crypto.Util.Tactics.DebugPrint.
Require Import Crypto.Util.CPSNotations.
Require Import Crypto.Util.Equality.
Import ListNotations. Local Open Scope Z_scope.

(** Kludgy hack to get this file to be faster *)
Strategy 0 [LetIn.Let_In LetIn.Let_In_pf].

Module Associational.
  Definition eval (p:list (Z*Z)) : Z :=
    fold_right (fun x y => x + y) 0%Z (map (fun t => fst t * snd t) p).

  Lemma eval_nil : eval nil = 0.
  Proof using Type. trivial.                                             Qed.
  Lemma eval_cons p q : eval (p::q) = fst p * snd p + eval q.
  Proof using Type. trivial.                                             Qed.
  Lemma eval_app p q: eval (p++q) = eval p + eval q.
  Proof using Type. induction p; rewrite <-?List.app_comm_cons;
           rewrite ?eval_nil, ?eval_cons; nsatz.              Qed.

#[global]
  Hint Rewrite eval_nil eval_cons eval_app : push_eval.
  Local Ltac push := autorewrite with
      push_eval push_map push_partition push_flat_map
      push_fold_right push_nth_default cancel_pair.

  Lemma eval_map_mul (a x:Z) (p:list (Z*Z))
  : eval (List.map (fun t => (a*fst t, x*snd t)) p) = a*x*eval p.
  Proof using Type. induction p; push; nsatz.                            Qed.
#[global]
  Hint Rewrite eval_map_mul : push_eval.

  Definition mul (p q:list (Z*Z)) : list (Z*Z) :=
    flat_map (fun t =>
      map (fun t' =>
        (fst t * fst t', snd t * snd t'))
    q) p.
  Lemma eval_mul p q : eval (mul p q) = eval p * eval q.
  Proof using Type. induction p; cbv [mul]; push; nsatz.                 Qed.
#[global]
  Hint Rewrite eval_mul : push_eval.

  Definition negate_snd (p:list (Z*Z)) : list (Z*Z) :=
    map (fun cx => (fst cx, -snd cx)) p.
  Lemma eval_negate_snd p : eval (negate_snd p) = - eval p.
  Proof using Type. induction p; cbv [negate_snd]; push; nsatz.          Qed.
#[global]
  Hint Rewrite eval_negate_snd : push_eval.

  Example base10_2digit_mul (a0:Z) (a1:Z) (b0:Z) (b1:Z) :
    {ab| eval ab = eval [(10,a1);(1,a0)] * eval [(10,b1);(1,b0)]}.
    eexists ?[ab].
    (* Goal: eval ?ab = eval [(10,a1);(1,a0)] * eval [(10,b1);(1,b0)] *)
    rewrite <-eval_mul.
    (* Goal: eval ?ab = eval (mul [(10,a1);(1,a0)] [(10,b1);(1,b0)]) *)
    cbv -[Z.mul eval]; cbn -[eval].
    (* Goal: eval ?ab = eval [(100,(a1*b1));(10,a1*b0);(10,a0*b1);(1,a0*b0)]%RT *)
    trivial.                                              Defined.

  Definition split (s:Z) (p:list (Z*Z)) : list (Z*Z) * list (Z*Z)
    := let hi_lo := partition (fun t => fst t mod s =? 0) p in
       (snd hi_lo, map (fun t => (fst t / s, snd t)) (fst hi_lo)).
  Lemma eval_split s p (s_nz:s<>0) :
    eval (fst (split s p)) + s * eval (snd (split s p)) = eval p.
  Proof using Type. cbv [Let_In split]; induction p;
    repeat match goal with
    | |- context[?a/?b] =>
      unique pose proof (Z_div_exact_full_2 a b ltac:(trivial) ltac:(trivial))
    | _ => progress push
    | _ => progress break_match
    | _ => progress nsatz                                end. Qed.

  Lemma reduction_rule a b s c (modulus_nz:s-c<>0) :
    (a + s * b) mod (s - c) = (a + c * b) mod (s - c).
  Proof using Type. replace (a + s * b) with ((a + c*b) + b*(s-c)) by nsatz.
    rewrite Z.add_mod,Z_mod_mult,Z.add_0_r,Z.mod_mod;trivial. Qed.

  Definition reduce (s:Z) (c:list _) (p:list _) : list (Z*Z) :=
    let lo_hi := split s p in fst lo_hi ++ mul c (snd lo_hi).

  Lemma eval_reduce s c p (s_nz:s<>0) (modulus_nz:s-eval c<>0) :
    eval (reduce s c p) mod (s - eval c) = eval p mod (s - eval c).
  Proof using Type. cbv [reduce]; push.
         rewrite <-reduction_rule, eval_split; trivial.      Qed.
#[global]
  Hint Rewrite eval_reduce : push_eval.

  Definition bind_snd (p : list (Z*Z)) :=
    map (fun t => dlet_nd t2 := snd t in (fst t, t2)) p.

  Lemma bind_snd_correct p : bind_snd p = p.
  Proof using Type.
    cbv [bind_snd]; induction p as [| [? ?] ];
      push; [|rewrite IHp]; reflexivity.
  Qed.

  Lemma eval_rev p : eval (rev p) = eval p.
  Proof using Type. induction p; cbn [rev]; push; lia. Qed.

  Section Carries.
    Definition carryterm (w fw:Z) (t:Z * Z) :=
      if (Z.eqb (fst t) w)
      then dlet_nd t2 := snd t in
           dlet_nd d2 := t2 / fw in
           dlet_nd m2 := t2 mod fw in
           [(w * fw, d2);(w,m2)]
      else [t].

    Lemma eval_carryterm w fw (t:Z * Z) (fw_nonzero:fw<>0):
      eval (carryterm w fw t) = eval [t].
    Proof using Type*.
      cbv [carryterm Let_In]; break_match; push; [|trivial].
      pose proof (Z.div_mod (snd t) fw fw_nonzero).
      rewrite Z.eqb_eq in *.
      nsatz.
    Qed. Hint Rewrite eval_carryterm using auto : push_eval.

    Definition carry (w fw:Z) (p:list (Z * Z)):=
      flat_map (carryterm w fw) p.

    Lemma eval_carry w fw p (fw_nonzero:fw<>0):
      eval (carry w fw p) = eval p.
    Proof using Type*. cbv [carry]; induction p; push; nsatz. Qed.
    Hint Rewrite eval_carry using auto : push_eval.
  End Carries.
  Module Export Hints.
#[global]
    Hint Rewrite eval_nil eval_cons eval_app : push_eval.
#[global]
    Hint Rewrite eval_map_mul : push_eval.
#[global]
    Hint Rewrite eval_mul : push_eval.
#[global]
    Hint Rewrite eval_negate_snd : push_eval.
#[global]
    Hint Rewrite eval_reduce : push_eval.
  End Hints.
End Associational.
Export Associational.Hints.

Module Positional. Section Positional.
  Context (weight : nat -> Z)
          (weight_0 : weight 0%nat = 1)
          (weight_nz : forall i, weight i <> 0).

  Definition to_associational (n:nat) (xs:list Z) : list (Z*Z)
    := combine (map weight (List.seq 0 n)) xs.
  Definition eval n x := Associational.eval (@to_associational n x).
  Lemma eval_to_associational n x :
    Associational.eval (@to_associational n x) = eval n x.
  Proof using Type. trivial.                                             Qed.
  Hint Rewrite @eval_to_associational : push_eval.
  Lemma eval_nil n : eval n [] = 0.
  Proof using Type. cbv [eval to_associational]. rewrite combine_nil_r. reflexivity. Qed.
  Hint Rewrite eval_nil : push_eval.
  Lemma eval0 p : eval 0 p = 0.
  Proof using Type. cbv [eval to_associational]. reflexivity. Qed.
  Hint Rewrite eval0 : push_eval.

  Lemma eval_snoc n m x y : n = length x -> m = S n -> eval m (x ++ [y]) = eval n x + weight n * y.
  Proof using Type.
    cbv [eval to_associational]; intros; subst n m.
    rewrite seq_snoc, map_app.
    rewrite combine_app_samelength by distr_length.
    autorewrite with push_eval. simpl.
    autorewrite with push_eval cancel_pair; ring.
  Qed.

  (* SKIP over this: zeros, add_to_nth *)
  Local Ltac push := autorewrite with push_eval push_map distr_length
    push_flat_map push_fold_right push_nth_default cancel_pair natsimplify.
  Definition zeros n : list Z := repeat 0 n.
  Lemma length_zeros n : length (zeros n) = n. Proof using Type. clear. cbv [zeros]; distr_length. Qed.
  Hint Rewrite length_zeros : distr_length.
  Lemma eval_zeros n : eval n (zeros n) = 0.
  Proof using Type.
    clear.
    cbv [eval Associational.eval to_associational zeros].
    rewrite <- (seq_length n 0) at 2.
    generalize dependent (List.seq 0 n); intro xs.
    induction xs; simpl; nsatz.                               Qed.
  Definition add_to_nth i x (ls : list Z) : list Z
    := ListUtil.update_nth i (fun y => x + y) ls.
  Lemma length_add_to_nth i x ls : length (add_to_nth i x ls) = length ls.
  Proof using Type. clear. cbv [add_to_nth]; distr_length. Qed.
  Hint Rewrite length_add_to_nth : distr_length.
  Lemma eval_add_to_nth (n:nat) (i:nat) (x:Z) (xs:list Z) (H:(i<length xs)%nat)
        (Hn : length xs = n) (* N.B. We really only need [i < Nat.min n (length xs)] *) :
    eval n (add_to_nth i x xs) = weight i * x + eval n xs.
  Proof using Type.
    clear -H Hn.
    subst n.
    cbv [eval to_associational add_to_nth].
    rewrite ListUtil.combine_update_nth_r at 1.
    rewrite <-(update_nth_id i (List.combine _ _)) at 2.
    rewrite <-!(ListUtil.splice_nth_equiv_update_nth_update _ _
      (weight 0, 0)) by (push; lia); cbv [ListUtil.splice_nth id].
    repeat match goal with
           | _ => progress push
           | _ => progress break_match
           | _ => progress (apply Zminus_eq; ring_simplify)
           | _ => rewrite <-ListUtil.map_nth_default_always
           end; lia.                                          Qed.
  Hint Rewrite @eval_add_to_nth eval_zeros : push_eval.

  Definition place (t:Z*Z) (i:nat) : nat * Z :=
    nat_rect
      (fun _ => (nat * Z)%type)
      (O, fst t * snd t)
      (fun i' place_i'
       => let i := S i' in
          if (fst t mod weight i =? 0)
          then (i, let c := fst t / weight i in c * snd t)
          else place_i')
      i.

  Lemma place_in_range (t:Z*Z) (n:nat) : (fst (place t n) < S n)%nat.
  Proof using Type. clear. induction n; cbv [place nat_rect] in *; break_match; autorewrite with cancel_pair; try lia. Qed.
  Lemma weight_place t i : weight (fst (place t i)) * snd (place t i) = fst t * snd t.
  Proof using weight_nz weight_0. clear -weight_nz weight_0. induction i; cbv [place nat_rect] in *; break_match; push;
    repeat match goal with |- context[?a/?b] =>
      unique pose proof (Z_div_exact_full_2 a b ltac:(auto) ltac:(auto))
           end; nsatz.                                        Qed.
  Hint Rewrite weight_place : push_eval.

  Definition from_associational n (p:list (Z*Z)) :=
    List.fold_right (fun t ls =>
      dlet_nd p := place t (pred n) in
      add_to_nth (fst p) (snd p) ls ) (zeros n) p.
  Lemma eval_from_associational n p (n_nz:n<>O \/ p = nil) :
    eval n (from_associational n p) = Associational.eval p.
  Proof using weight_0 weight_nz. destruct n_nz; [ induction p | subst p ];
  cbv [from_associational Let_In] in *; push; try
  pose proof place_in_range a (pred n); try lia; try nsatz;
  apply fold_right_invariant; cbv [zeros add_to_nth];
  intros; rewrite ?map_length, ?List.repeat_length, ?seq_length, ?length_update_nth;
  try lia; destruct n; cbn [Init.Nat.pred] in *; try lia.   Qed.
  Hint Rewrite @eval_from_associational : push_eval.
  Lemma length_from_associational n p : length (from_associational n p) = n.
  Proof using Type. cbv [from_associational Let_In]. apply fold_right_invariant; intros; distr_length. Qed.
  Hint Rewrite length_from_associational : distr_length.

  Section mulmod.
    Context (s:Z) (s_nz:s <> 0)
            (c:list (Z*Z))
            (m_nz:s - Associational.eval c <> 0).
    Definition mulmod (n:nat) (a b:list Z) : list Z
      := let a_a := to_associational n a in
         let b_a := to_associational n b in
         let ab_a := Associational.mul a_a b_a in
         let abm_a := Associational.reduce s c ab_a in
         from_associational n abm_a.
    Lemma eval_mulmod n (f g:list Z)
          (Hf : length f = n) (Hg : length g = n) :
      eval n (mulmod n f g) mod (s - Associational.eval c)
      = (eval n f * eval n g) mod (s - Associational.eval c).
    Proof using m_nz s_nz weight_0 weight_nz. cbv [mulmod]; push; trivial.
    destruct f, g; simpl in *; [ right; subst n | left; try lia.. ].
    clear; cbv -[Associational.reduce].
    induction c as [|?? IHc]; simpl; trivial.                 Qed.
  End mulmod.
  Hint Rewrite @eval_mulmod : push_eval.

  Definition add (n:nat) (a b:list Z) : list Z
    := let a_a := to_associational n a in
       let b_a := to_associational n b in
       from_associational n (a_a ++ b_a).
  Lemma eval_add n (f g:list Z)
        (Hf : length f = n) (Hg : length g = n) :
    eval n (add n f g) = (eval n f + eval n g).
  Proof using weight_0 weight_nz. cbv [add]; push; trivial. destruct n; auto.          Qed.
  Hint Rewrite @eval_add : push_eval.
  Lemma length_add n f g
        (Hf : length f = n) (Hg : length g = n) :
    length (add n f g) = n.
  Proof using Type. clear -Hf Hf; cbv [add]; distr_length.               Qed.
  Hint Rewrite @length_add : distr_length.

  Section Carries.
    Definition carry n m (index:nat) (p:list Z) : list Z :=
      from_associational
        m (@Associational.carry (weight index)
                                (weight (S index) / weight index)
                                (to_associational n p)).

    Lemma length_carry n m index p : length (carry n m index p) = m.
    Proof using Type. cbv [carry]; distr_length. Qed.
    Lemma eval_carry n m i p: (n <> 0%nat) -> (m <> 0%nat) ->
                              weight (S i) / weight i <> 0 ->
      eval m (carry n m i p) = eval n p.
    Proof using weight_0 weight_nz.
      cbv [carry]; intros; push; [|tauto].
      rewrite @Associational.eval_carry by eauto.
      apply eval_to_associational.
    Qed. Hint Rewrite @eval_carry : push_eval.

    Definition carry_reduce n (s:Z) (c:list (Z * Z))
               (index:nat) (p : list Z) :=
      from_associational
        n (Associational.reduce
             s c (to_associational (S n) (@carry n (S n) index p))).

    Lemma eval_carry_reduce n s c index p :
      (s <> 0) -> (s - Associational.eval c <> 0) -> (n <> 0%nat) ->
      (weight (S index) / weight index <> 0) ->
      eval n (carry_reduce n s c index p) mod (s - Associational.eval c)
      = eval n p mod (s - Associational.eval c).
    Proof using weight_0 weight_nz. cbv [carry_reduce]; intros; push; auto.            Qed.
    Hint Rewrite @eval_carry_reduce : push_eval.
    Lemma length_carry_reduce n s c index p
      : length p = n -> length (carry_reduce n s c index p) = n.
    Proof using Type. cbv [carry_reduce]; distr_length.                  Qed.
    Hint Rewrite @length_carry_reduce : distr_length.

    (* N.B. It is important to reverse [idxs] here, because fold_right is
      written such that the first terms in the list are actually used
      last in the computation. For example, running:

      `Eval cbv - [Z.add] in (fun a b c d => fold_right Z.add d [a;b;c]).`

      will produce [fun a b c d => (a + (b + (c + d)))].*)
    Definition chained_carries n s c p (idxs : list nat) :=
      fold_right (fun a b => carry_reduce n s c a b) p (rev idxs).

    Lemma eval_chained_carries n s c p idxs :
      (s <> 0) -> (s - Associational.eval c <> 0) -> (n <> 0%nat) ->
      (forall i, In i idxs -> weight (S i) / weight i <> 0) ->
      eval n (chained_carries n s c p idxs) mod (s - Associational.eval c)
      = eval n p mod (s - Associational.eval c).
    Proof using Type*.
      cbv [chained_carries]; intros; push.
      apply fold_right_invariant; [|intro; rewrite <-in_rev];
        destruct n; intros; push; auto.
    Qed. Hint Rewrite @eval_chained_carries : push_eval.
    Lemma length_chained_carries n s c p idxs
      : length p = n -> length (@chained_carries n s c p idxs) = n.
    Proof using Type.
      intros; cbv [chained_carries]; induction (rev idxs) as [|x xs IHxs];
        cbn [fold_right]; distr_length.
    Qed. Hint Rewrite @length_chained_carries : distr_length.

    (* carries without modular reduction; useful for converting between bases *)
    Definition chained_carries_no_reduce n p (idxs : list nat) :=
      fold_right (fun a b => carry n n a b) p (rev idxs).
    Lemma eval_chained_carries_no_reduce n p idxs:
      (forall i, In i idxs -> weight (S i) / weight i <> 0) ->
      eval n (chained_carries_no_reduce n p idxs) = eval n p.
    Proof using weight_0 weight_nz.
      cbv [chained_carries_no_reduce]; intros.
      destruct n; [push;reflexivity|].
      apply fold_right_invariant; [|intro; rewrite <-in_rev];
        intros; push; auto.
    Qed. Hint Rewrite @eval_chained_carries_no_reduce : push_eval.

    (* Reverse of [eval]; translate from Z to basesystem by putting
    everything in first digit and then carrying. *)
    Definition encode n s c (x : Z) : list Z :=
      chained_carries n s c (from_associational n [(1,x)]) (seq 0 n).
    Lemma eval_encode n s c x :
      (s <> 0) -> (s - Associational.eval c <> 0) -> (n <> 0%nat) ->
      (forall i, In i (seq 0 n) -> weight (S i) / weight i <> 0) ->
      eval n (encode n s c x) mod (s - Associational.eval c)
      = x mod (s - Associational.eval c).
    Proof using Type*. cbv [encode]; intros; push; auto; f_equal; lia. Qed.
    Lemma length_encode n s c x
      : length (encode n s c x) = n.
    Proof using Type. cbv [encode]; repeat distr_length.                 Qed.

  End Carries.
  Hint Rewrite @eval_encode : push_eval.
  Hint Rewrite @length_encode : distr_length.

  Section sub.
    Context (n:nat)
            (s:Z) (s_nz:s <> 0)
            (c:list (Z * Z))
            (m_nz:s - Associational.eval c <> 0)
            (coef:Z).

    Definition negate_snd (a:list Z) : list Z
      := let A := to_associational n a in
         let negA := Associational.negate_snd A in
         from_associational n negA.

    Definition scmul (x:Z) (a:list Z) : list Z
      := let A := to_associational n a in
         let R := Associational.mul A [(1, x)] in
         from_associational n R.

    Definition balance : list Z
      := scmul coef (encode n s c (s - Associational.eval c)).

    Definition sub (a b:list Z) : list Z
      := let ca := add n balance a in
         let _b := negate_snd b in
         add n ca _b.
    Lemma eval_sub a b
      : (forall i, In i (seq 0 n) -> weight (S i) / weight i <> 0) ->
        (List.length a = n) -> (List.length b = n) ->
        eval n (sub a b) mod (s - Associational.eval c)
        = (eval n a - eval n b) mod (s - Associational.eval c).
    Proof using m_nz s_nz weight_0 weight_nz.
      cbv [sub balance scmul negate_snd];
        destruct (zerop n); subst; try reflexivity.
      intros; push; repeat distr_length;
        eauto with lia.
      push_Zmod; push; pull_Zmod; push_Zmod; pull_Zmod; distr_length; eauto.
    Qed.
    Hint Rewrite eval_sub : push_eval.
    Lemma length_sub a b
      : length a = n -> length b = n ->
        length (sub a b) = n.
    Proof using Type. intros; cbv [sub balance scmul negate_snd]; repeat distr_length. Qed.
    Hint Rewrite length_sub : distr_length.
    Definition opp (a:list Z) : list Z
      := sub (zeros n) a.
    Lemma eval_opp
          (a:list Z)
      : (length a = n) ->
        (forall i, In i (seq 0 n) -> weight (S i) / weight i <> 0) ->
        eval n (opp a) mod (s - Associational.eval c)
        = (- eval n a) mod (s - Associational.eval c).
    Proof using m_nz s_nz weight_0 weight_nz. intros; cbv [opp]; push; distr_length; auto.       Qed.
    Lemma length_opp a
      : length a = n -> length (opp a) = n.
    Proof using Type. cbv [opp]; intros; repeat distr_length.            Qed.
  End sub.
  Hint Rewrite @eval_opp @eval_sub : push_eval.
  Hint Rewrite @length_sub @length_opp : distr_length.
End Positional.
(* Hint Rewrite disappears after the end of a section *)
Module Export Hints.
#[global]
  Hint Rewrite length_zeros length_add_to_nth length_from_associational @length_add @length_carry_reduce @length_chained_carries @length_encode @length_sub @length_opp : distr_length.
End Hints.
End Positional.
Export Positional.Hints.

Record weight_properties {weight : nat -> Z} :=
  {
    weight_0 : weight 0%nat = 1;
    weight_positive : forall i, 0 < weight i;
    weight_multiples : forall i, weight (S i) mod weight i = 0;
    weight_divides : forall i : nat, 0 < weight (S i) / weight i;
  }.
Global Hint Resolve weight_0 weight_positive weight_multiples weight_divides.

Section mod_ops.
  Import Positional.
  Local Coercion Z.of_nat : nat >-> Z.
  Local Coercion QArith_base.inject_Z : Z >-> Q.
  (* Design constraints:
     - inputs must be [Z] (b/c reification does not support Q)
     - internal structure must not match on the arguments (b/c reification does not support [positive]) *)
  Context (limbwidth_num limbwidth_den : Z)
          (limbwidth_good : 0 < limbwidth_den <= limbwidth_num)
          (s : Z)
          (c : list (Z*Z))
          (n : nat)
          (len_c : nat)
          (idxs : list nat)
          (len_idxs : nat)
          (m_nz:s - Associational.eval c <> 0) (s_nz:s <> 0)
          (Hn_nz : n <> 0%nat)
          (Hc : length c = len_c)
          (Hidxs : length idxs = len_idxs).
  Definition weight (i : nat)
    := 2^(-(-(limbwidth_num * i) / limbwidth_den)).

  Local Ltac Q_cbv :=
    cbv [Qceiling inject_Z Qle Qfloor Qdiv Qnum Qden Qmult Qinv Qopp].

  Local Lemma weight_ZQ_correct i
        (limbwidth := (limbwidth_num / limbwidth_den)%Q)
    : weight i = 2^Qceiling(limbwidth*i).
  Proof using limbwidth_good.
    clear -limbwidth_good.
    cbv [limbwidth weight]; Q_cbv.
    destruct limbwidth_num, limbwidth_den, i; try reflexivity;
      repeat rewrite ?Pos.mul_1_l, ?Pos.mul_1_r, ?Z.mul_0_l, ?Zdiv_0_l, ?Zdiv_0_r, ?Z.mul_1_l, ?Z.mul_1_r, <- ?Z.opp_eq_mul_m1, ?Pos2Z.opp_pos;
      try reflexivity; try lia.
  Qed.

  Local Ltac t_weight_with lem :=
    clear -limbwidth_good;
    intros; rewrite !weight_ZQ_correct;
    apply lem;
    try lia; Q_cbv; destruct limbwidth_den; cbn; try lia.

  Definition wprops : @weight_properties weight.
  Proof.
    constructor.
    { cbv [weight Z.of_nat]; autorewrite with zsimplify_fast; reflexivity. }
    { intros; apply Z.gt_lt. t_weight_with (@pow_ceil_mul_nat_pos 2). }
    { t_weight_with (@pow_ceil_mul_nat_multiples 2). }
    { intros; apply Z.gt_lt. t_weight_with (@pow_ceil_mul_nat_divide 2). }
  Defined.
  Local Hint Immediate (weight_0 wprops).
  Local Hint Immediate (weight_positive wprops).
  Local Hint Immediate (weight_multiples wprops).
  Local Hint Immediate (weight_divides wprops).
  Local Hint Resolve Z.positive_is_nonzero Z.lt_gt.

  Local Lemma weight_1_gt_1 : weight 1 > 1.
  Proof using limbwidth_good.
    clear -limbwidth_good.
    cut (1 < weight 1); [ lia | ].
    cbv [weight Z.of_nat]; autorewrite with zsimplify_fast.
    apply Z.pow_gt_1; [ lia | ].
    Z.div_mod_to_quot_rem_in_goal; nia.
  Qed.

  Derive carry_mulmod
         SuchThat (forall (f g : list Z)
                          (Hf : length f = n)
                          (Hg : length g = n),
                      (eval weight n (carry_mulmod f g)) mod (s - Associational.eval c)
                      = (eval weight n f * eval weight n g) mod (s - Associational.eval c))
         As eval_carry_mulmod.
  Proof.
    intros.
    rewrite <-eval_mulmod with (s:=s) (c:=c) by auto.
    etransitivity;
      [ | rewrite <- @eval_chained_carries with (s:=s) (c:=c) (idxs:=idxs)
          by auto; reflexivity ].
    eapply f_equal2; [|trivial]. eapply f_equal.
    expand_lists ().
    subst carry_mulmod; reflexivity.
  Qed.

  Derive carrymod
         SuchThat (forall (f : list Z)
                          (Hf : length f = n),
                      (eval weight n (carrymod f)) mod (s - Associational.eval c)
                      = (eval weight n f) mod (s - Associational.eval c))
         As eval_carrymod.
  Proof.
    intros.
    etransitivity;
      [ | rewrite <- @eval_chained_carries with (s:=s) (c:=c) (idxs:=idxs)
          by auto; reflexivity ].
    eapply f_equal2; [|trivial]. eapply f_equal.
    expand_lists ().
    subst carrymod; reflexivity.
  Qed.

  Derive addmod
         SuchThat (forall (f g : list Z)
                          (Hf : length f = n)
                          (Hg : length g = n),
                      (eval weight n (addmod f g)) mod (s - Associational.eval c)
                      = (eval weight n f + eval weight n g) mod (s - Associational.eval c))
         As eval_addmod.
  Proof.
    intros.
    rewrite <-eval_add by auto.
    eapply f_equal2; [|trivial]. eapply f_equal.
    expand_lists ().
    subst addmod; reflexivity.
  Qed.

  Derive submod
         SuchThat (forall (coef:Z)
                          (f g : list Z)
                          (Hf : length f = n)
                          (Hg : length g = n),
                      (eval weight n (submod coef f g)) mod (s - Associational.eval c)
                      = (eval weight n f - eval weight n g) mod (s - Associational.eval c))
         As eval_submod.
  Proof.
    intros.
    rewrite <-eval_sub with (coef:=coef) by auto.
    eapply f_equal2; [|trivial]. eapply f_equal.
    expand_lists ().
    subst submod; reflexivity.
  Qed.

  Derive oppmod
         SuchThat (forall (coef:Z)
                          (f: list Z)
                          (Hf : length f = n),
                      (eval weight n (oppmod coef f)) mod (s - Associational.eval c)
                      = (- eval weight n f) mod (s - Associational.eval c))
         As eval_oppmod.
  Proof.
    intros.
    rewrite <-eval_opp with (coef:=coef) by auto.
    eapply f_equal2; [|trivial]. eapply f_equal.
    expand_lists ().
    subst oppmod; reflexivity.
  Qed.

  Derive encodemod
         SuchThat (forall (f:Z),
                      (eval weight n (encodemod f)) mod (s - Associational.eval c)
                      = f mod (s - Associational.eval c))
         As eval_encodemod.
  Proof.
    intros.
    etransitivity.
    2:rewrite <-@eval_encode with (weight:=weight) (n:=n) by auto; reflexivity.
    eapply f_equal2; [|trivial]. eapply f_equal.
    expand_lists ().
    subst encodemod; reflexivity.
  Qed.
End mod_ops.

Module Saturated.
  Global Hint Resolve weight_positive weight_0 weight_multiples weight_divides.
  Global Hint Resolve Z.positive_is_nonzero Z.lt_gt Nat2Z.is_nonneg.

  Section Weight.
    Context weight {wprops : @weight_properties weight}.

    Lemma weight_multiples_full' j : forall i, weight (i+j) mod weight i = 0.
    Proof using wprops.
      induction j; intros;
        repeat match goal with
               | _ => rewrite Nat.add_succ_r
               | _ => rewrite IHj
               | |- context [weight (S ?x) mod weight _] =>
                 rewrite (Z.div_mod (weight (S x)) (weight x)), weight_multiples by auto
               | _ => progress autorewrite with push_Zmod natsimplify zsimplify_fast
               | _ => reflexivity
               end.
    Qed.

    Lemma weight_multiples_full j i : (i <= j)%nat -> weight j mod weight i = 0.
    Proof using wprops.
      intros; replace j with (i + (j - i))%nat by lia.
      apply weight_multiples_full'.
    Qed.

    Lemma weight_divides_full j i : (i <= j)%nat -> 0 < weight j / weight i.
    Proof using wprops. auto using Z.gt_lt, Z.div_positive_gt_0, weight_multiples_full. Qed.

    Lemma weight_div_mod j i : (i <= j)%nat -> weight j = weight i * (weight j / weight i).
    Proof using wprops. intros. apply Z.div_exact; auto using weight_multiples_full. Qed.
  End Weight.

  Module Associational.
    Section Associational.

      Definition sat_multerm s (t t' : (Z * Z)) : list (Z * Z) :=
        dlet_nd xy := Z.mul_split s (snd t) (snd t') in
              [(fst t * fst t', fst xy); (fst t * fst t' * s, snd xy)].

      Definition sat_mul s (p q : list (Z * Z)) : list (Z * Z) :=
        flat_map (fun t => flat_map (fun t' => sat_multerm s t t') q) p.

      Lemma eval_map_sat_multerm s a q (s_nonzero:s<>0):
        Associational.eval (flat_map (sat_multerm s a) q) = fst a * snd a * Associational.eval q.
      Proof using Type.
        cbv [sat_multerm Let_In]; induction q;
          repeat match goal with
                 | _ => progress autorewrite with cancel_pair push_eval to_div_mod in *
                 | _ => progress simpl flat_map
                 | _ => rewrite IHq
                 | _ => rewrite Z.mod_eq by assumption
                 | _ => ring_simplify; lia
                 end.
      Qed.
      Hint Rewrite eval_map_sat_multerm using (lia || assumption) : push_eval.

      Lemma eval_sat_mul s p q (s_nonzero:s<>0):
        Associational.eval (sat_mul s p q) = Associational.eval p * Associational.eval q.
      Proof using Type.
        cbv [sat_mul]; induction p; [reflexivity|].
        repeat match goal with
               | _ => progress (autorewrite with push_flat_map push_eval in * )
               | _ => rewrite IHp
               | _ => ring_simplify; lia
               end.
      Qed.
      Hint Rewrite eval_sat_mul : push_eval.

      Definition sat_multerm_const s (t t' : (Z * Z)) : list (Z * Z) :=
        if snd t =? 1
        then [(fst t * fst t', snd t')]
        else if snd t =? -1
             then [(fst t * fst t', - snd t')]
             else if snd t =? 0
                  then nil
                  else dlet_nd xy := Z.mul_split s (snd t) (snd t') in
              [(fst t * fst t', fst xy); (fst t * fst t' * s, snd xy)].

      Definition sat_mul_const s (p q : list (Z * Z)) : list (Z * Z) :=
        flat_map (fun t => flat_map (fun t' => sat_multerm_const s t t') q) p.

      Lemma eval_map_sat_multerm_const s a q (s_nonzero:s<>0):
        Associational.eval (flat_map (sat_multerm_const s a) q) = fst a * snd a * Associational.eval q.
      Proof using Type.
        cbv [sat_multerm_const Let_In]; induction q;
          repeat match goal with
                 | _ => progress autorewrite with cancel_pair push_eval to_div_mod in *
                 | _ => progress simpl flat_map
                 | H : _ = 1 |- _ => rewrite H
                 | H : _ = -1 |- _ => rewrite H
                 | H : _ = 0 |- _ => rewrite H
                 | _ => progress break_match; Z.ltb_to_lt
                 | _ => rewrite IHq
                 | _ => rewrite Z.mod_eq by assumption
                 | _ => ring_simplify; lia
                 end.
      Qed.
      Hint Rewrite eval_map_sat_multerm_const using (lia || assumption) : push_eval.

      Lemma eval_sat_mul_const s p q (s_nonzero:s<>0):
        Associational.eval (sat_mul_const s p q) = Associational.eval p * Associational.eval q.
      Proof using Type.
        cbv [sat_mul_const]; induction p; [reflexivity|].
        repeat match goal with
               | _ 

Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted)

Build Log (contains the Coq error message) (truncated to last 8.0KiB; full 304KiB file on GitHub Actions Artifacts under build.log)

edArithmetic.v", line 56, characters 0-45:
Warning: Trying to mask the absolute name "Coq.omega.PreOmega"!
[masking-absolute-name,deprecated-since-8.8,deprecated,default]
File "./src/Experiments/SimplyTypedArithmetic.v", line 56, characters 0-45:
Warning: Trying to mask the absolute name "Coq.omega.PreOmega"!
[masking-absolute-name,deprecated-since-8.8,deprecated,default]
File "./src/Experiments/SimplyTypedArithmetic.v", line 502, characters 0-77:
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated-since-8.10,deprecated,default]
File "./src/Experiments/SimplyTypedArithmetic.v", line 554, characters 2-41:
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated-since-8.10,deprecated,default]
File "./src/Experiments/SimplyTypedArithmetic.v", line 554, characters 2-41:
Warning: Declaring arbitrary terms as hints is fragile; it is recommended to
declare a toplevel constant instead [fragile-hint-constr,automation,default]
File "./src/Experiments/SimplyTypedArithmetic.v", line 555, characters 2-48:
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated-since-8.10,deprecated,default]
File "./src/Experiments/SimplyTypedArithmetic.v", line 555, characters 2-48:
Warning: Declaring arbitrary terms as hints is fragile; it is recommended to
declare a toplevel constant instead [fragile-hint-constr,automation,default]
File "./src/Experiments/SimplyTypedArithmetic.v", line 556, characters 2-49:
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated-since-8.10,deprecated,default]
File "./src/Experiments/SimplyTypedArithmetic.v", line 556, characters 2-49:
Warning: Declaring arbitrary terms as hints is fragile; it is recommended to
declare a toplevel constant instead [fragile-hint-constr,automation,default]
File "./src/Experiments/SimplyTypedArithmetic.v", line 557, characters 2-47:
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated-since-8.10,deprecated,default]
File "./src/Experiments/SimplyTypedArithmetic.v", line 557, characters 2-47:
Warning: Declaring arbitrary terms as hints is fragile; it is recommended to
declare a toplevel constant instead [fragile-hint-constr,automation,default]
File "./src/Experiments/SimplyTypedArithmetic.v", line 558, characters 2-51:
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated-since-8.10,deprecated,default]
File "./src/Experiments/SimplyTypedArithmetic.v", line 665, characters 2-79:
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated-since-8.10,deprecated,default]
File "./src/Experiments/SimplyTypedArithmetic.v", line 666, characters 2-68:
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated-since-8.10,deprecated,default]
File "./src/Experiments/SimplyTypedArithmetic.v", line 946, characters 6-33:
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated-since-8.10,deprecated,default]
File "./src/Experiments/SimplyTypedArithmetic.v", line 1094, characters 4-37:
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated-since-8.10,deprecated,default]
File "./src/Experiments/SimplyTypedArithmetic.v", line 1482, characters 6-41:
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated-since-8.10,deprecated,default]
File "./src/Experiments/SimplyTypedArithmetic.v", line 1778, characters 4-31:
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated-since-8.10,deprecated,default]
File "./src/Experiments/SimplyTypedArithmetic.v", line 1954, characters 4-69:
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated-since-8.10,deprecated,default]
File "./src/Experiments/SimplyTypedArithmetic.v", line 1999, characters 6-13:
Warning: The Focus command is deprecated; use '2: {' instead.
[deprecated-focus,deprecated-since-8.8,deprecated,default]
File "./src/Experiments/SimplyTypedArithmetic.v", line 2006, characters 23-30:
Warning: The Unfocus command is deprecated
[deprecated-unfocus,deprecated-since-8.8,deprecated,default]
File "./src/Experiments/SimplyTypedArithmetic.v", line 2346, characters 6-43:
Warning: Declaring a scope implicitly is deprecated; use in advance an
explicit "Declare Scope ctype_scope.".
[undeclared-scope,deprecated-since-8.10,deprecated,default]
File "./src/Experiments/SimplyTypedArithmetic.v", line 2372, characters 8-40:
Warning: Declaring a scope implicitly is deprecated; use in advance an
explicit "Declare Scope expr_scope.".
[undeclared-scope,deprecated-since-8.10,deprecated,default]
File "./src/Experiments/SimplyTypedArithmetic.v", line 2374, characters 8-40:
Warning: Declaring a scope implicitly is deprecated; use in advance an
explicit "Declare Scope Expr_scope.".
[undeclared-scope,deprecated-since-8.10,deprecated,default]
File "./src/Experiments/SimplyTypedArithmetic.v", line 3964, characters 10-51:
Warning: Declaring a scope implicitly is deprecated; use in advance an
explicit "Declare Scope cpstype_scope.".
[undeclared-scope,deprecated-since-8.10,deprecated,default]
File "./src/Experiments/SimplyTypedArithmetic.v", line 4042, characters 10-51:
Warning: Declaring a scope implicitly is deprecated; use in advance an
explicit "Declare Scope cpsexpr_scope.".
[undeclared-scope,deprecated-since-8.10,deprecated,default]
File "./src/Experiments/SimplyTypedArithmetic.v", line 6759, characters 4-455:
Warning: Collision between bound variables of name x0
[variable-collision,ltac,default]
File "./src/Experiments/SimplyTypedArithmetic.v", line 6759, characters 4-455:
Warning: Collision between bound variables of name x0
[variable-collision,ltac,default]
Tactic call ran for 0.039 secs (0.039u,0.s) (success)
Tactic call ran for 0.202 secs (0.198u,0.003s) (success)
Finished transaction in 1.165 secs (1.152u,0.011s) (successful)
Finished transaction in 1.783 secs (1.775u,0.007s) (successful)
Tactic call ran for 0.036 secs (0.036u,0.s) (success)
Tactic call ran for 0.159 secs (0.159u,0.s) (success)
Tactic call ran for 0.032 secs (0.032u,0.s) (success)
Tactic call ran for 0.155 secs (0.151u,0.003s) (success)
Tactic call ran for 0.002 secs (0.002u,0.s) (success)
Tactic call ran for 0.015 secs (0.015u,0.s) (success)
Tactic call ran for 0.038 secs (0.038u,0.s) (success)
Tactic call ran for 0.248 secs (0.248u,0.s) (success)
Tactic call ran for 0.021 secs (0.021u,0.s) (success)
Tactic call ran for 0.23 secs (0.226u,0.004s) (success)
Tactic call ran for 0.013 secs (0.013u,0.s) (success)
Tactic call ran for 0.143 secs (0.139u,0.004s) (success)
Tactic call ran for 0.04 secs (0.04u,0.s) (success)
Tactic call ran for 0.172 secs (0.172u,0.s) (success)
Tactic call ran for 0. secs (0.u,0.s) (success)
Tactic call ran for 0.001 secs (0.001u,0.s) (success)
File "./src/Experiments/SimplyTypedArithmetic.v", line 7059, characters 4-350:
Error: Anomaly "Not an unfoldable reference."
Please report at http://coq.inria.fr/bugs/.

Command exited with non-zero status 129
src/Experiments/SimplyTypedArithmetic.vo (real: 70.32, user: 69.84, sys: 0.45, mem: 890216 ko)
make: *** [Makefile.coq:847: src/Experiments/SimplyTypedArithmetic.vo] Error 129
make: *** [src/Experiments/SimplyTypedArithmetic.vo] Deleting file 'src/Experiments/SimplyTypedArithmetic.glob'

Minimization Log

Coq version: 8.19+alpha compiled with OCaml 4.13.1


First, I will attempt to absolutize relevant [Require]s in /github/workspace/fiat-crypto/src/Experiments/SimplyTypedArithmetic.v, and store the result in /github/workspace/cwd/bug_01.v...
getting /github/workspace/fiat-crypto/src/Experiments/SimplyTypedArithmetic.v
/home/coq/.opam/4.13.1+flambda/bin/coqc.orig -q -R /github/workspace/fiat-crypto/src Crypto -R /github/workspace/fiat-crypto/bbv/src/bbv bbv -Q /github/workspace/cwd Top -Q /home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Bignums Bignums -Q /home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Ltac2 Ltac2 -q -w -deprecated-hint-rewrite-without-locality,+deprecated-hint-without-locality,+deprecated-instance-without-locality,unsupported-attributes -w -notation-overridden -w -deprecated-native-compiler-option -native-compiler no -R /github/workspace/fiat-crypto/src Crypto -R /github/workspace/fiat-crypto/bbv/src/bbv bbv -Q /github/workspace/cwd Top -Q /home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Bignums Bignums -Q /home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Ltac2 Ltac2 -top Crypto.Experiments.SimplyTypedArithmetic /github/workspace/fiat-crypto/coqprime/src /github/workspace/fiat-crypto/coqprime/src/Coqprime Coqprime -o /tmp/SimplyTypedArithmetic.vo -dump-glob ../fiat-crypto/src/Experiments/SimplyTypedArithmetic.glob ../fiat-crypto/src/Experiments/SimplyTypedArithmetic.v

Now, I will attempt to coq the file, and find the error...

Coqing the file (/github/workspace/cwd/bug_01.v)...

Running command: "/home/coq/.opam/4.13.1+flambda/bin/coqc.orig" "-q" "-w" "-deprecated-hint-rewrite-without-locality,+deprecated-hint-without-locality,+deprecated-instance-without-locality,unsupported-attributes" "-w" "-notation-overridden" "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" "-R" "/github/workspace/fiat-crypto/src" "Crypto" "-R" "/github/workspace/fiat-crypto/bbv/src/bbv" "bbv" "-Q" "/github/workspace/cwd" "Top" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Bignums" "Bignums" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Ltac2" "Ltac2" "-top" "Crypto.Experiments.SimplyTypedArithmetic" "/github/workspace/fiat-crypto/coqprime/src" "/github/workspace/fiat-crypto/coqprime/src/Coqprime" "Coqprime" "-R" "/tmp/tmpsngot9bc" "" "/tmp/tmpsngot9bc/Crypto/Experiments/SimplyTypedArithmetic.v" "-q"

The timeout for /home/coq/.opam/4.13.1+flambda/bin/coqc.orig has been set to: 3

This file produces the following output when Coq'ed:
Error:
More than one file to compile: /github/workspace/fiat-crypto/coqprime/src/Coqprime



The current state of the file does not have a recognizable error.
Traceback (most recent call last):
  File "/github/workspace/coq-tools/coq_tools/find_bug.py", line 1471, in main
    env['error_reg_string'] = get_error_reg_string(output_file_name, **env)
  File "/github/workspace/coq-tools/coq_tools/find_bug.py", line 280, in get_error_reg_string
    error_reg_string = get_error_reg_string_of_output(output, output_file_name, **kwargs)
  File "/github/workspace/coq-tools/coq_tools/find_bug.py", line 242, in get_error_reg_string_of_output
    error_reg_string = raw_input('\nPlease enter a regular expression which matches on the output.  Leave blank to re-coq the file.\n')
EOFError: EOF when reading a line

If you have any comments on your experience of the minimizer, please share them in a reply (possibly tagging @JasonGross).
If you believe there's a bug in the bug minimizer, please report it on the bug minimizer issue tracker.

Originally posted by @coqbot-app[bot] in rocq-prover/rocq#18239 (comment)

[JasonGross]

Most recent one should be fixed by a3d4de4 (issue with printf "-Q\n"). Let's try again
@coqbot minimize coq.dev

git clone --recurse-submodules https://github.com/mit-plv/fiat-crypto.git --branch=sp2019latest
cd fiat-crypto
make TIMED=1 some-early util

[coqbot]

Hey @JasonGross, the coq bug minimizer is running your script, I'll come back to you with the results once it's done.

[coqbot]

@JasonGross, Minimized File /github/workspace/fiat-crypto/src/Experiments/SimplyTypedArithmetic.v (interrupted by timeout) (full log on GitHub Actions)

Partially Minimized Coq File (timeout) (truncated to 32KiB; full 184KiB file on GitHub Actions Artifacts under bug.v)

(* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-w" "-deprecated-hint-rewrite-without-locality,+deprecated-hint-without-locality,+deprecated-instance-without-locality,unsupported-attributes" "-w" "-notation-overridden" "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" "-R" "/github/workspace/fiat-crypto/src" "Crypto" "-R" "/github/workspace/fiat-crypto/bbv/src/bbv" "bbv" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/fiat-crypto/coqprime/src/Coqprime" "Coqprime" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Bignums" "Bignums" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Ltac2" "Ltac2" "-I" "/github/workspace/fiat-crypto/coqprime/src" "-top" "Crypto.Experiments.SimplyTypedArithmetic") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 12849 lines to 4129 lines *)
(* coqc version 8.19+alpha compiled with OCaml 4.13.1
   coqtop version buildkitsandbox:/home/coq/.opam/4.13.1+flambda/.opam-switch/build/coq-core.dev/_build/default,master (2a7bea412a5817a55d2f5834302c019a7dcb0c91)
   Expected coqc runtime on this file: 2.828 sec *)
Require Coq.Init.Ltac.
Require Coq.ZArith.ZArith.
Require Coq.micromega.Lia.
Require Coq.Classes.Morphisms.
Require Coq.Classes.Morphisms_Prop.
Require Coq.nsatz.Nsatz.
Require Coq.Lists.List.
Require Crypto.Util.GlobalSettings.
Require Crypto.Util.FixCoqMistakes.
Require Coq.setoid_ring.Ring_polynom.
Require Crypto.Algebra.Nsatz.
Require Coq.Strings.String.
Require Coq.MSets.MSetPositive.
Require Coq.FSets.FMapPositive.
Require Coq.derive.Derive.
Require Coq.Numbers.BinNums.
Require Crypto.Util.Pointed.
Require Crypto.Util.Tactics.UniquePose.
Require Coq.Logic.Eqdep_dec.
Require Crypto.Util.Isomorphism.
Require Crypto.Util.HProp.
Require Crypto.Util.Equality.
Require Crypto.Util.Sigma.
Require Coq.ZArith.BinInt.
Require Coq.ZArith.ZArith_dec.
Require Coq.NArith.BinNat.
Require Crypto.Util.Decidable.
Require Coq.Relations.Relation_Definitions.
Require Crypto.Util.Tactics.Head.
Require Crypto.Util.Tactics.BreakMatch.
Require Crypto.Util.Tactics.DestructHyps.
Require Crypto.Util.Tactics.DestructHead.
Require Crypto.Util.Notations.
Require Crypto.Util.Option.
Require Coq.Classes.RelationClasses.
Require Crypto.Util.IffT.
Require Crypto.Util.Prod.
Require Crypto.Util.Tactics.SpecializeBy.
Require Coq.Arith.Arith.
Require Coq.Arith.Peano_dec.
Require Coq.Numbers.Natural.Peano.NPeano.
Require Coq.NArith.NArith.
Require Crypto.Util.NatUtil.
Require Crypto.Util.Tactics.Test.
Require Crypto.Util.Tactics.Not.
Require Crypto.Util.Tactics.DoWithHyp.
Require Crypto.Util.Tactics.RewriteHyp.
Require Coq.Lists.SetoidList.
Require Crypto.Util.ListUtil.
Require Crypto.Util.Tuple.
Require Crypto.Util.Tactics.GetGoal.
Require Crypto.Util.LetIn.
Require Coq.QArith.QArith_base.
Require Coq.QArith.Qround.
Require Coq.QArith.QArith.
Require Coq.micromega.Psatz.
Require Crypto.Util.ZUtil.Hints.Core.
Require Crypto.Util.ZUtil.Div.Bootstrap.
Require Crypto.Util.ZUtil.Modulo.Bootstrap.
Require Crypto.Util.ZUtil.Tactics.DivModToQuotRem.
Require Coq.Classes.RelationPairs.
Require Crypto.Util.ZUtil.Notations.
Require Crypto.Util.ZUtil.Definitions.
Require Coq.ZArith.Znumtheory.
Require Crypto.Util.ZUtil.Tactics.CompareToSgn.
Require Coq.Bool.Bool.
Require Crypto.Util.Bool.
Require Crypto.Util.ZUtil.Tactics.LtbToLt.
Require Crypto.Util.ZUtil.Le.
Require Crypto.Util.ZUtil.Hints.ZArith.
Require Crypto.Util.ZUtil.Hints.PullPush.
Require Crypto.Util.ZUtil.Hints.Ztestbit.
Require Crypto.Util.ZUtil.ZSimplify.Core.
Require Crypto.Util.ZUtil.Hints.
Require Crypto.Util.ZUtil.Div.
Require Crypto.Util.ZUtil.Pow.
Require Crypto.Util.ZUtil.Pow2.
Require Crypto.Util.ZUtil.ZSimplify.Simple.
Require Crypto.Util.ZUtil.Log2.
Require Crypto.Util.ZUtil.Tactics.PeelLe.
Require Crypto.Util.ZUtil.Tactics.ReplaceNegWithPos.
Require Crypto.Util.ZUtil.Tactics.RewriteModSmall.
Require Crypto.Util.Tactics.Contains.
Require Crypto.Util.ZUtil.Tactics.LinearSubstitute.
Require Crypto.Util.ZUtil.Tactics.SplitMinMax.
Require Coq.ZArith.Zpow_facts.
Require Crypto.Util.ZUtil.Modulo.PullPush.
Require Crypto.Util.ZUtil.Lnot.
Require Crypto.Util.ZUtil.Tactics.PrimeBound.
Require Crypto.Util.ZUtil.Tactics.ZeroBounds.
Require Crypto.Util.ZUtil.Testbit.
Require Crypto.Util.NUtil.WithoutReferenceToZ.
Require Crypto.Util.ZUtil.LandLorShiftBounds.
Require Crypto.Util.ZUtil.Tactics.PullPush.Modulo.
Require Crypto.Util.ZUtil.Modulo.
Require Crypto.Util.ZUtil.Ones.
Require Crypto.Util.ZUtil.Land.
Require Crypto.Util.ZUtil.LandLorBounds.
Require Crypto.Util.ZUtil.Morphisms.
Require Crypto.Util.QUtil.
Require Coq.setoid_ring.Ncring.
Require Coq.setoid_ring.Cring.
Require Crypto.Util.Tactics.OnSubterms.
Require Crypto.Util.Tactics.Revert.
Require Coq.Classes.Equivalence.
Require Coq.PArith.BinPos.
Require Crypto.Algebra.Hierarchy.
Require Crypto.Util.Logic.
Require Coq.Setoids.Setoid.
Require Crypto.Util.Relations.
Require Crypto.Algebra.Monoid.
Require Crypto.Algebra.Group.
Require Coq.PArith.PArith.
Require Coq.setoid_ring.Ring_tac.
Require Crypto.Algebra.Ring.
Require Crypto.Util.Decidable.Bool2Prop.
Require Crypto.Algebra.SubsetoidRing.
Require Coq.ZArith.BinIntDef.
Require Coq.NArith.BinNatDef.
Require Coq.PArith.BinPosDef.
Require Coq.ZArith.Zdiv.
Require Coq.Logic.EqdepFacts.
Require Coq.ZArith.Zpower.
Require Crypto.Util.ZUtil.Tactics.DivideExistsMul.
Require Crypto.Util.ZUtil.Divide.
Require Crypto.Util.ZUtil.Odd.
Require Coqprime.Tactic.Tactic.
Require Coq.setoid_ring.ArithRing.
Require Coq.Wellfounded.Inverse_Image.
Require Coq.Arith.Wf_nat.
Require Coqprime.List.ListAux.
Require Coqprime.List.Permutation.
Require Coqprime.List.Iterator.
Require Coq.Lists.ListSet.
Require Coqprime.List.UList.
Require Coqprime.List.ZProgression.
Require Coqprime.Z.ZSum.
Require Coqprime.PrimalityTest.Euler.
Require Coqprime.PrimalityTest.FGroup.
Require Coqprime.Z.ZCAux.
Require Coqprime.N.NatAux.
Require Coqprime.PrimalityTest.Lagrange.
Require Coqprime.PrimalityTest.EGroup.
Require Coqprime.PrimalityTest.IGroup.
Require Coqprime.PrimalityTest.Root.
Require Coqprime.PrimalityTest.Cyclic.
Require Coqprime.PrimalityTest.Zp.
Require Crypto.Util.NumTheoryUtil.
Require Crypto.Arithmetic.ModularArithmeticPre.
Require Crypto.Spec.ModularArithmetic.
Require Coq.setoid_ring.Ring_theory.
Require Crypto.Util.ZUtil.Peano.
Require Crypto.Algebra.ScalarMult.
Require Crypto.Util.Tactics.DebugPrint.
Require Coq.setoid_ring.Integral_domain.
Require Coq.Bool.Sumbool.
Require Coq.Init.Wf.
Require Crypto.Util.Factorize.
Require Crypto.Algebra.IntegralDomain.
Require Coq.setoid_ring.Field_theory.
Require Crypto.Algebra.Field.
Require Crypto.Arithmetic.ModularArithmeticTheorems.
Require Coq.setoid_ring.Field_tac.
Require Crypto.Arithmetic.PrimeFieldTheorems.
Require Crypto.Util.ZUtil.Tactics.SimplifyFractionsLe.
Require Crypto.Util.ZUtil.ZSimplify.Autogenerated.
Require Crypto.Util.ZUtil.ZSimplify.
Require Crypto.Arithmetic.BarrettReduction.Generalized.
Require Coq.Structures.Equalities.
Require Crypto.Util.ZUtil.EquivModulo.
Require Crypto.Arithmetic.MontgomeryReduction.Definition.
Require Crypto.Util.Tactics.SimplifyRepeatedIfs.
Require Crypto.Arithmetic.MontgomeryReduction.Proofs.
Require Crypto.Util.ZRange.
Require Crypto.Util.ZRange.Operations.
Require Crypto.Util.Tactics.RunTacticAsConstr.
Require Crypto.Util.OptionList.
Require Crypto.Util.Sum.
Require Crypto.Util.ZUtil.AddGetCarry.
Require Crypto.Util.ZUtil.MulSplit.
Require Crypto.Util.ZUtil.Pow2Mod.
Require Crypto.Util.ZUtil.Shift.
Require Crypto.Util.Tactics.SplitInContext.
Require Crypto.Util.Tactics.SubstEvars.
Require Coq.Strings.Ascii.
Require Crypto.Util.Bool.Equality.
Require Crypto.Util.Strings.Equality.
Require Crypto.Util.Strings.Ascii.
Require Crypto.Util.Strings.String.
Require Crypto.Util.Strings.Decimal.
Require Crypto.Util.Strings.HexString.
Require Crypto.Util.ZUtil.CC.
Require Crypto.Util.ZUtil.Rshi.
Require Crypto.Util.ZUtil.Zselect.
Require Crypto.Util.ZUtil.AddModulo.
Require Crypto.Util.CPSNotations.

Module Export AdmitTactic.
Module Import LocalFalse.
Inductive False : Prop := .
End LocalFalse.
Axiom proof_admitted : False.
Import Coq.Init.Ltac.
Tactic Notation "admit" := abstract case proof_admitted.
End AdmitTactic.
Import Coq.ZArith.ZArith.
Import Coq.micromega.Lia.
Import Coq.Classes.Morphisms.
Import Coq.Classes.Morphisms_Prop.
Import Crypto.Algebra.Nsatz.
Import Coq.Strings.String.
Import Coq.MSets.MSetPositive.
Import Coq.FSets.FMapPositive.
Import Coq.derive.Derive.
Import Crypto.Util.Pointed.
Import Crypto.Util.Tactics.UniquePose.
Import Crypto.Util.Decidable.
Import Crypto.Util.Tuple.
Import Crypto.Util.Prod.
Import Crypto.Util.LetIn.
Import Crypto.Util.ListUtil.
Import Coq.Lists.List.
Import Crypto.Util.NatUtil.
Import Coq.QArith.QArith_base.
Import Coq.QArith.Qround.
Import Crypto.Util.QUtil.
Import Crypto.Algebra.Ring.
Import Crypto.Util.Decidable.Bool2Prop.
Import Crypto.Algebra.Ring.
Import Crypto.Algebra.SubsetoidRing.
Import Crypto.Arithmetic.PrimeFieldTheorems.
Import Crypto.Arithmetic.BarrettReduction.Generalized.
Import Crypto.Arithmetic.MontgomeryReduction.Definition.
Import Crypto.Arithmetic.MontgomeryReduction.Proofs.
Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo.
Import Crypto.Util.ZRange.
Import Crypto.Util.ZRange.Operations.
Import Crypto.Util.Tactics.RunTacticAsConstr.
Import Crypto.Util.Tactics.Head.
Import Crypto.Util.Option.
Import Crypto.Util.OptionList.
Import Crypto.Util.Sum.
Import Crypto.Util.ZUtil.Modulo.
Import Crypto.Util.ZUtil.Div.
Import Crypto.Util.ZUtil.Hints.Core.
Import Crypto.Util.ZUtil.Hints.PullPush.
Import Crypto.Util.ZUtil.AddGetCarry.
Import Crypto.Util.ZUtil.MulSplit.
Import Crypto.Util.ZUtil.Tactics.LtbToLt.
Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo.
Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem.
Import Crypto.Util.ZUtil.Le.
Import Crypto.Util.ZUtil.Tactics.RewriteModSmall.
Import Crypto.Util.ZUtil.Log2.
Import Crypto.Util.ZUtil.Tactics.ZeroBounds.
Import Crypto.Util.ZUtil.Notations.
Import Crypto.Util.ZUtil.Shift.
Import Crypto.Util.ZUtil.LandLorShiftBounds.
Import Crypto.Util.ZUtil.Testbit.
Import Crypto.Util.ZUtil.Notations.
Import Crypto.Util.Tactics.SpecializeBy.
Import Crypto.Util.Tactics.SplitInContext.
Import Crypto.Util.Tactics.SubstEvars.
Import Crypto.Util.Strings.Decimal.
Import Crypto.Util.Strings.HexString.
Import Crypto.Util.Notations.
Import Crypto.Util.ZUtil.Definitions.
Import Crypto.Util.ZUtil.CC.
Import Crypto.Util.ZUtil.Rshi.
Import Crypto.Util.ZUtil.Zselect.
Import Crypto.Util.ZUtil.AddModulo.
Import Crypto.Util.ZUtil.AddGetCarry.
Import Crypto.Util.ZUtil.MulSplit.
Import Crypto.Util.ZUtil.Hints.Core.
Import Crypto.Util.ZUtil.Modulo.
Import Crypto.Util.ZUtil.Div.
Import Crypto.Util.ZUtil.Hints.PullPush.
Import Crypto.Util.ZUtil.EquivModulo.
Import Crypto.Util.Tactics.DebugPrint.
Import Crypto.Util.CPSNotations.
Import Crypto.Util.Equality.
Import ListNotations.
Local Open Scope Z_scope.

 
Strategy 0 [LetIn.Let_In LetIn.Let_In_pf].

Module Export Associational.
Definition eval (p:list (Z*Z)) : Z. exact (fold_right (fun x y => x + y) 0%Z (map (fun t => fst t * snd t) p)). Defined.

  Lemma eval_nil : eval nil = 0.
Admitted.
  Lemma eval_cons p q : eval (p::q) = fst p * snd p + eval q.
Admitted.
  Lemma eval_app p q: eval (p++q) = eval p + eval q.
Admitted.

#[global]
  Hint Rewrite eval_nil eval_cons eval_app : push_eval.

  Lemma eval_map_mul (a x:Z) (p:list (Z*Z))
  : eval (List.map (fun t => (a*fst t, x*snd t)) p) = a*x*eval p.
Admitted.
#[global]
  Hint Rewrite eval_map_mul : push_eval.
Definition mul (p q:list (Z*Z)) : list (Z*Z). exact (flat_map (fun t =>
      map (fun t' =>
        (fst t * fst t', snd t * snd t'))
    q) p). Defined.
  Lemma eval_mul p q : eval (mul p q) = eval p * eval q.
Admitted.
#[global]
  Hint Rewrite eval_mul : push_eval.
Definition negate_snd (p:list (Z*Z)) : list (Z*Z). exact (map (fun cx => (fst cx, -snd cx)) p). Defined.
  Lemma eval_negate_snd p : eval (negate_snd p) = - eval p.
Admitted.
#[global]
  Hint Rewrite eval_negate_snd : push_eval.

  Example base10_2digit_mul (a0:Z) (a1:Z) (b0:Z) (b1:Z) :
    {ab| eval ab = eval [(10,a1);(1,a0)] * eval [(10,b1);(1,b0)]}.
Admitted.
Definition split (s:Z) (p:list (Z*Z)) : list (Z*Z) * list (Z*Z). exact (let hi_lo := partition (fun t => fst t mod s =? 0) p in
       (snd hi_lo, map (fun t => (fst t / s, snd t)) (fst hi_lo))). Defined.
  Lemma eval_split s p (s_nz:s<>0) :
    eval (fst (split s p)) + s * eval (snd (split s p)) = eval p.
Admitted.

  Lemma reduction_rule a b s c (modulus_nz:s-c<>0) :
    (a + s * b) mod (s - c) = (a + c * b) mod (s - c).
Admitted.

  Definition reduce (s:Z) (c:list _) (p:list _) : list (Z*Z) :=
    let lo_hi := split s p in fst lo_hi ++ mul c (snd lo_hi).

  Lemma eval_reduce s c p (s_nz:s<>0) (modulus_nz:s-eval c<>0) :
    eval (reduce s c p) mod (s - eval c) = eval p mod (s - eval c).
Admitted.
#[global]
  Hint Rewrite eval_reduce : push_eval.

  Definition bind_snd (p : list (Z*Z)) :=
    map (fun t => dlet_nd t2 := snd t in (fst t, t2)) p.

  Lemma bind_snd_correct p : bind_snd p = p.
Admitted.

  Lemma eval_rev p : eval (rev p) = eval p.
Admitted.

  Section Carries.
    Definition carryterm (w fw:Z) (t:Z * Z) :=
      if (Z.eqb (fst t) w)
      then dlet_nd t2 := snd t in
           dlet_nd d2 := t2 / fw in
           dlet_nd m2 := t2 mod fw in
           [(w * fw, d2);(w,m2)]
      else [t].

    Lemma eval_carryterm w fw (t:Z * Z) (fw_nonzero:fw<>0):
      eval (carryterm w fw t) = eval [t].
Admitted.
Hint Rewrite eval_carryterm using auto : push_eval.

    Definition carry (w fw:Z) (p:list (Z * Z)):=
      flat_map (carryterm w fw) p.

    Lemma eval_carry w fw p (fw_nonzero:fw<>0):
      eval (carry w fw p) = eval p.
Admitted.
    Hint Rewrite eval_carry using auto : push_eval.
  End Carries.
  Module Export Hints.
#[global]
    Hint Rewrite eval_nil eval_cons eval_app : push_eval.
#[global]
    Hint Rewrite eval_map_mul : push_eval.
#[global]
    Hint Rewrite eval_mul : push_eval.
#[global]
    Hint Rewrite eval_negate_snd : push_eval.
#[global]
    Hint Rewrite eval_reduce : push_eval.
  End Hints.
End Associational.
Export Associational.Hints.

Module Export Positional.
Section Positional.
  Context (weight : nat -> Z)
          (weight_0 : weight 0%nat = 1)
          (weight_nz : forall i, weight i <> 0).
Definition to_associational (n:nat) (xs:list Z) : list (Z*Z). exact (combine (map weight (List.seq 0 n)) xs). Defined.
  Definition eval n x := Associational.eval (@to_associational n x).
  Lemma eval_to_associational n x :
    Associational.eval (@to_associational n x) = eval n x.
Admitted.
  Hint Rewrite @eval_to_associational : push_eval.
  Lemma eval_nil n : eval n [] = 0.
Admitted.
  Hint Rewrite eval_nil : push_eval.
  Lemma eval0 p : eval 0 p = 0.
Admitted.
  Hint Rewrite eval0 : push_eval.

  Lemma eval_snoc n m x y : n = length x -> m = S n -> eval m (x ++ [y]) = eval n x + weight n * y.
Admitted.
  Definition zeros n : list Z := repeat 0 n.
  Lemma length_zeros n : length (zeros n) = n.
Admitted.
  Hint Rewrite length_zeros : distr_length.
  Lemma eval_zeros n : eval n (zeros n) = 0.
Admitted.
  Definition add_to_nth i x (ls : list Z) : list Z
    := ListUtil.update_nth i (fun y => x + y) ls.
  Lemma length_add_to_nth i x ls : length (add_to_nth i x ls) = length ls.
Admitted.
  Hint Rewrite length_add_to_nth : distr_length.
  Lemma eval_add_to_nth (n:nat) (i:nat) (x:Z) (xs:list Z) (H:(i<length xs)%nat)
        (Hn : length xs = n)   :
    eval n (add_to_nth i x xs) = weight i * x + eval n xs.
Admitted.
  Hint Rewrite @eval_add_to_nth eval_zeros : push_eval.
Definition place (t:Z*Z) (i:nat) : nat * Z. exact (nat_rect
      (fun _ => (nat * Z)%type)
      (O, fst t * snd t)
      (fun i' place_i'
       => let i := S i' in
          if (fst t mod weight i =? 0)
          then (i, let c := fst t / weight i in c * snd t)
          else place_i')
      i). Defined.

  Lemma place_in_range (t:Z*Z) (n:nat) : (fst (place t n) < S n)%nat.
Admitted.
  Lemma weight_place t i : weight (fst (place t i)) * snd (place t i) = fst t * snd t.
Admitted.
  Hint Rewrite weight_place : push_eval.

  Definition from_associational n (p:list (Z*Z)) :=
    List.fold_right (fun t ls =>
      dlet_nd p := place t (pred n) in
      add_to_nth (fst p) (snd p) ls ) (zeros n) p.
  Lemma eval_from_associational n p (n_nz:n<>O \/ p = nil) :
    eval n (from_associational n p) = Associational.eval p.
Admitted.
  Hint Rewrite @eval_from_associational : push_eval.
  Lemma length_from_associational n p : length (from_associational n p) = n.
Admitted.
  Hint Rewrite length_from_associational : distr_length.

  Section mulmod.
    Context (s:Z) (s_nz:s <> 0)
            (c:list (Z*Z))
            (m_nz:s - Associational.eval c <> 0).
Definition mulmod (n:nat) (a b:list Z) : list Z. exact (let a_a := to_associational n a in
         let b_a := to_associational n b in
         let ab_a := Associational.mul a_a b_a in
         let abm_a := Associational.reduce s c ab_a in
         from_associational n abm_a). Defined.
    Lemma eval_mulmod n (f g:list Z)
          (Hf : length f = n) (Hg : length g = n) :
      eval n (mulmod n f g) mod (s - Associational.eval c)
      = (eval n f * eval n g) mod (s - Associational.eval c).
Admitted.
  End mulmod.
  Hint Rewrite @eval_mulmod : push_eval.
Definition add (n:nat) (a b:list Z) : list Z. exact (let a_a := to_associational n a in
       let b_a := to_associational n b in
       from_associational n (a_a ++ b_a)). Defined.
  Lemma eval_add n (f g:list Z)
        (Hf : length f = n) (Hg : length g = n) :
    eval n (add n f g) = (eval n f + eval n g).
Admitted.
  Hint Rewrite @eval_add : push_eval.
  Lemma length_add n f g
        (Hf : length f = n) (Hg : length g = n) :
    length (add n f g) = n.
Admitted.
  Hint Rewrite @length_add : distr_length.

  Section Carries.
    Definition carry n m (index:nat) (p:list Z) : list Z :=
      from_associational
        m (@Associational.carry (weight index)
                                (weight (S index) / weight index)
                                (to_associational n p)).

    Lemma length_carry n m index p : length (carry n m index p) = m.
Admitted.
    Lemma eval_carry n m i p: (n <> 0%nat) -> (m <> 0%nat) ->
                              weight (S i) / weight i <> 0 ->
      eval m (carry n m i p) = eval n p.
Admitted.
Hint Rewrite @eval_carry : push_eval.

    Definition carry_reduce n (s:Z) (c:list (Z * Z))
               (index:nat) (p : list Z) :=
      from_associational
        n (Associational.reduce
             s c (to_associational (S n) (@carry n (S n) index p))).

    Lemma eval_carry_reduce n s c index p :
      (s <> 0) -> (s - Associational.eval c <> 0) -> (n <> 0%nat) ->
      (weight (S index) / weight index <> 0) ->
      eval n (carry_reduce n s c index p) mod (s - Associational.eval c)
      = eval n p mod (s - Associational.eval c).
Admitted.
    Hint Rewrite @eval_carry_reduce : push_eval.
    Lemma length_carry_reduce n s c index p
      : length p = n -> length (carry_reduce n s c index p) = n.
Admitted.
    Hint Rewrite @length_carry_reduce : distr_length.

     
    Definition chained_carries n s c p (idxs : list nat) :=
      fold_right (fun a b => carry_reduce n s c a b) p (rev idxs).

    Lemma eval_chained_carries n s c p idxs :
      (s <> 0) -> (s - Associational.eval c <> 0) -> (n <> 0%nat) ->
      (forall i, In i idxs -> weight (S i) / weight i <> 0) ->
      eval n (chained_carries n s c p idxs) mod (s - Associational.eval c)
      = eval n p mod (s - Associational.eval c).
Admitted.
Hint Rewrite @eval_chained_carries : push_eval.
    Lemma length_chained_carries n s c p idxs
      : length p = n -> length (@chained_carries n s c p idxs) = n.
Admitted.
Hint Rewrite @length_chained_carries : distr_length.

     
    Definition chained_carries_no_reduce n p (idxs : list nat) :=
      fold_right (fun a b => carry n n a b) p (rev idxs).
    Lemma eval_chained_carries_no_reduce n p idxs:
      (forall i, In i idxs -> weight (S i) / weight i <> 0) ->
      eval n (chained_carries_no_reduce n p idxs) = eval n p.
Admitted.
Hint Rewrite @eval_chained_carries_no_reduce : push_eval.

     
    Definition encode n s c (x : Z) : list Z :=
      chained_carries n s c (from_associational n [(1,x)]) (seq 0 n).
    Lemma eval_encode n s c x :
      (s <> 0) -> (s - Associational.eval c <> 0) -> (n <> 0%nat) ->
      (forall i, In i (seq 0 n) -> weight (S i) / weight i <> 0) ->
      eval n (encode n s c x) mod (s - Associational.eval c)
      = x mod (s - Associational.eval c).
Admitted.
    Lemma length_encode n s c x
      : length (encode n s c x) = n.
Admitted.

  End Carries.
  Hint Rewrite @eval_encode : push_eval.
  Hint Rewrite @length_encode : distr_length.

  Section sub.
    Context (n:nat)
            (s:Z) (s_nz:s <> 0)
            (c:list (Z * Z))
            (m_nz:s - Associational.eval c <> 0)
            (coef:Z).
Definition negate_snd (a:list Z) : list Z. exact (let A := to_associational n a in
         let negA := Associational.negate_snd A in
         from_associational n negA). Defined.
Definition scmul (x:Z) (a:list Z) : list Z. exact (let A := to_associational n a in
         let R := Associational.mul A [(1, x)] in
         from_associational n R). Defined.
Definition balance : list Z. exact (scmul coef (encode n s c (s - Associational.eval c))). Defined.
Definition sub (a b:list Z) : list Z. exact (let ca := add n balance a in
         let _b := negate_snd b in
         add n ca _b). Defined.
    Lemma eval_sub a b
      : (forall i, In i (seq 0 n) -> weight (S i) / weight i <> 0) ->
        (List.length a = n) -> (List.length b = n) ->
        eval n (sub a b) mod (s - Associational.eval c)
        = (eval n a - eval n b) mod (s - Associational.eval c).
Admitted.
    Hint Rewrite eval_sub : push_eval.
    Lemma length_sub a b
      : length a = n -> length b = n ->
        length (sub a b) = n.
Admitted.
    Hint Rewrite length_sub : distr_length.
Definition opp (a:list Z) : list Z. exact (sub (zeros n) a). Defined.
    Lemma eval_opp
          (a:list Z)
      : (length a = n) ->
        (forall i, In i (seq 0 n) -> weight (S i) / weight i <> 0) ->
        eval n (opp a) mod (s - Associational.eval c)
        = (- eval n a) mod (s - Associational.eval c).
Admitted.
    Lemma length_opp a
      : length a = n -> length (opp a) = n.
Admitted.
  End sub.
  Hint Rewrite @eval_opp @eval_sub : push_eval.
  Hint Rewrite @length_sub @length_opp : distr_length.
End Positional.
 
Module Export Hints.
#[global]
  Hint Rewrite length_zeros length_add_to_nth length_from_associational @length_add @length_carry_reduce @length_chained_carries @length_encode @length_sub @length_opp : distr_length.
End Hints.
End Positional.
Export Positional.Hints.

Record weight_properties {weight : nat -> Z} :=
  {
    weight_0 : weight 0%nat = 1;
    weight_positive : forall i, 0 < weight i;
    weight_multiples : forall i, weight (S i) mod weight i = 0;
    weight_divides : forall i : nat, 0 < weight (S i) / weight i;
  }.
Global Hint Resolve weight_0 weight_positive weight_multiples weight_divides.

Section mod_ops.
  Import Positional.
  Local Coercion Z.of_nat : nat >-> Z.
  Local Coercion QArith_base.inject_Z : Z >-> Q.
   
  Context (limbwidth_num limbwidth_den : Z)
          (limbwidth_good : 0 < limbwidth_den <= limbwidth_num)
          (s : Z)
          (c : list (Z*Z))
          (n : nat)
          (len_c : nat)
          (idxs : list nat)
          (len_idxs : nat)
          (m_nz:s - Associational.eval c <> 0) (s_nz:s <> 0)
          (Hn_nz : n <> 0%nat)
          (Hc : length c = len_c)
          (Hidxs : length idxs = len_idxs).
  Definition weight (i : nat)
    := 2^(-(-(limbwidth_num * i) / limbwidth_den)).

  Local Ltac Q_cbv :=
    cbv [Qceiling inject_Z Qle Qfloor Qdiv Qnum Qden Qmult Qinv Qopp].

  Local Lemma weight_ZQ_correct i
        (limbwidth := (limbwidth_num / limbwidth_den)%Q)
    : weight i = 2^Qceiling(limbwidth*i).
admit.
Defined.

  Local Ltac t_weight_with lem :=
    clear -limbwidth_good;
    intros; rewrite !weight_ZQ_correct;
    apply lem;
    try lia; Q_cbv; destruct limbwidth_den; cbn; try lia.

  Definition wprops : @weight_properties weight.
  Proof.
    constructor.
    {
 cbv [weight Z.of_nat]; autorewrite with zsimplify_fast; reflexivity.
}
    {
 intros; apply Z.gt_lt.
t_weight_with (@pow_ceil_mul_nat_pos 2).
}
    {
 t_weight_with (@pow_ceil_mul_nat_multiples 2).
}
    {
 intros; apply Z.gt_lt.
t_weight_with (@pow_ceil_mul_nat_divide 2).
}
  Defined.
  Local Hint Immediate (weight_0 wprops).
  Local Hint Immediate (weight_positive wprops).
  Local Hint Immediate (weight_multiples wprops).
  Local Hint Immediate (weight_divides wprops).
  Local Hint Resolve Z.positive_is_nonzero Z.lt_gt.

  Local Lemma weight_1_gt_1 : weight 1 > 1.
Admitted.

  Derive carry_mulmod
         SuchThat (forall (f g : list Z)
                          (Hf : length f = n)
                          (Hg : length g = n),
                      (eval weight n (carry_mulmod f g)) mod (s - Associational.eval c)
                      = (eval weight n f * eval weight n g) mod (s - Associational.eval c))
         As eval_carry_mulmod.
  Proof.
    intros.
    rewrite <-eval_mulmod with (s:=s) (c:=c) by auto.
    etransitivity;
      [ | rewrite <- @eval_chained_carries with (s:=s) (c:=c) (idxs:=idxs)
          by auto; reflexivity ].
    eapply f_equal2; [|trivial].
eapply f_equal.
    expand_lists ().
    subst carry_mulmod; reflexivity.
  Qed.

  Derive carrymod
         SuchThat (forall (f : list Z)
                          (Hf : length f = n),
                      (eval weight n (carrymod f)) mod (s - Associational.eval c)
                      = (eval weight n f) mod (s - Associational.eval c))
         As eval_carrymod.
  Proof.
    intros.
    etransitivity;
      [ | rewrite <- @eval_chained_carries with (s:=s) (c:=c) (idxs:=idxs)
          by auto; reflexivity ].
    eapply f_equal2; [|trivial].
eapply f_equal.
    expand_lists ().
    subst carrymod; reflexivity.
  Qed.

  Derive addmod
         SuchThat (forall (f g : list Z)
                          (Hf : length f = n)
                          (Hg : length g = n),
                      (eval weight n (addmod f g)) mod (s - Associational.eval c)
                      = (eval weight n f + eval weight n g) mod (s - Associational.eval c))
         As eval_addmod.
  Proof.
    intros.
    rewrite <-eval_add by auto.
    eapply f_equal2; [|trivial].
eapply f_equal.
    expand_lists ().
    subst addmod; reflexivity.
  Qed.

  Derive submod
         SuchThat (forall (coef:Z)
                          (f g : list Z)
                          (Hf : length f = n)
                          (Hg : length g = n),
                      (eval weight n (submod coef f g)) mod (s - Associational.eval c)
                      = (eval weight n f - eval weight n g) mod (s - Associational.eval c))
         As eval_submod.
  Proof.
    intros.
    rewrite <-eval_sub with (coef:=coef) by auto.
    eapply f_equal2; [|trivial].
eapply f_equal.
    expand_lists ().
    subst submod; reflexivity.
  Qed.

  Derive oppmod
         SuchThat (forall (coef:Z)
                          (f: list Z)
                          (Hf : length f = n),
                      (eval weight n (oppmod coef f)) mod (s - Associational.eval c)
                      = (- eval weight n f) mod (s - Associational.eval c))
         As eval_oppmod.
  Proof.
    intros.
    rewrite <-eval_opp with (coef:=coef) by auto.
    eapply f_equal2; [|trivial].
eapply f_equal.
    expand_lists ().
    subst oppmod; reflexivity.
  Qed.

  Derive encodemod
         SuchThat (forall (f:Z),
                      (eval weight n (encodemod f)) mod (s - Associational.eval c)
                      = f mod (s - Associational.eval c))
         As eval_encodemod.
  Proof.
    intros.
    etransitivity.
    2:rewrite <-@eval_encode with (weight:=weight) (n:=n) by auto; reflexivity.
    eapply f_equal2; [|trivial].
eapply f_equal.
    expand_lists ().
    subst encodemod; reflexivity.
  Qed.
End mod_ops.

Module Export Saturated.
  Global Hint Resolve weight_positive weight_0 weight_multiples weight_divides.
  Global Hint Resolve Z.positive_is_nonzero Z.lt_gt Nat2Z.is_nonneg.

  Section Weight.
    Context weight {wprops : @weight_properties weight}.

    Lemma weight_multiples_full' j : forall i, weight (i+j) mod weight i = 0.
Admitted.

    Lemma weight_multiples_full j i : (i <= j)%nat -> weight j mod weight i = 0.
Admitted.

    Lemma weight_divides_full j i : (i <= j)%nat -> 0 < weight j / weight i.
Admitted.

    Lemma weight_div_mod j i : (i <= j)%nat -> weight j = weight i * (weight j / weight i).
Admitted.
  End Weight.

  Module Export Associational.
    Section Associational.

      Definition sat_multerm s (t t' : (Z * Z)) : list (Z * Z) :=
        dlet_nd xy := Z.mul_split s (snd t) (snd t') in
              [(fst t * fst t', fst xy); (fst t * fst t' * s, snd xy)].

      Definition sat_mul s (p q : list (Z * Z)) : list (Z * Z) :=
        flat_map (fun t => flat_map (fun t' => sat_multerm s t t') q) p.

      Lemma eval_map_sat_multerm s a q (s_nonzero:s<>0):
        Associational.eval (flat_map (sat_multerm s a) q) = fst a * snd a * Associational.eval q.
Admitted.
      Hint Rewrite eval_map_sat_multerm using (lia || assumption) : push_eval.

      Lemma eval_sat_mul s p q (s_nonzero:s<>0):
        Associational.eval (sat_mul s p q) = Associational.eval p * Associational.eval q.
Admitted.
      Hint Rewrite eval_sat_mul : push_eval.

      Definition sat_multerm_const s (t t' : (Z * Z)) : list (Z * Z) :=
        if snd t =? 1
        then [(fst t * fst t', snd t')]
        else if snd t =? -1
             then [(fst t * fst t', - snd t')]
             else if snd t =? 0
                  then nil
                  else dlet_nd xy := Z.mul_split s (snd t) (snd t') in
              [(fst t * fst t', fst xy); (fst t * fst t' * s, snd xy)].

      Definition sat_mul_const s (p q : list (Z * Z)) : list (Z * Z) :=
        flat_map (fun t => flat_map (fun t' => sat_multerm_const s t t') q) p.

      Lemma eval_map_sat_multerm_const s a q (s_nonzero:s<>0):
        Associational.eval (flat_map (sat_multerm_const s a) q) = fst a * snd a * Associational.eval q.
Admitted.
      Hint Rewrite eval_map_sat_multerm_const using (lia || assumption) : push_eval.

      Lemma eval_sat_mul_const s p q (s_nonzero:s<>0):
        Associational.eval (sat_mul_const s p q) = Associational.eval p * Associational.eval q.
Admitted.
      Hint Rewrite eval_sat_mul_const : push_eval.
    End Associational.
  End Associational.

  Section DivMod.
    Lemma mod_step a b c d: 0 < a -> 0 < b ->
                            c mod a + a * ((c / a + d) mod b) = (a * d + c) mod (a * b).
Admitted.

    Lemma div_step a b c d : 0 < a -> 0 < b ->
                             (c / a + d) / b = (a * d + c) / (a * b).
Admitted.

    Lemma add_mod_div_multiple a b n m:
      n > 0 ->
      0 <= m / n ->
      m mod n = 0 ->
      (a / n + b) mod (m / n) = (a + n * b) mod m / n.
Admitted.

    Lemma add_mod_l_multiple a b n m:
      0 < n / m -> m <> 0 -> n mod m = 0 ->
      (a mod n + b) mod m = (a + b) mod m.
Admitted.

    Definition is_div_mod {T} (evalf : T -> Z) dm y n :=
      evalf (fst dm) = y mod n /\ snd dm = y / n.

    Lemma is_div_mod_step {T} evalf1 evalf2 dm1 dm2 y1 y2 n1 n2 x :
      n1 > 0 ->
      0 < n2 / n1 ->
      n2 mod n1 = 0 ->
      evalf2 (fst dm2) = evalf1 (fst dm1) + n1 * ((snd dm1 + x) mod (n2 / n1)) ->
      snd dm2 = (snd dm1 + x) / (n2 / n1) ->
      y2 = y1 + n1 * x ->
      @is_div_mod T evalf1 dm1 y1 n1 ->
      @is_div_mod T evalf2 dm2 y2 n2.
Admitted.

    Lemma is_div_mod_result_equal {T} evalf dm y1 y2 n :
      y1 = y2 ->
      @is_div_mod T evalf dm y1 n ->
      @is_div_mod T evalf dm y2 n.
Admitted.
  End DivMod.
End Saturated.

Module Export Columns.
  Import Saturated.
  Section Columns.
    Context weight {wprops : @weight_properties weight}.

    Definition eval n (x : list (list Z)) : Z := Positional.eval weight n (map sum x).

    Lemma eval_nil n : eval n [] = 0.
Admitted.
    Hint Rewrite eval_nil : push_eval.
    Lemma eval_snoc n x y : n = length x -> eval (S n) (x ++ [y]) = eval n x + weight n * sum y.
Admitted.
Hint Rewrite eval_snoc using (solve [distr_length]) : push_eval.

    Hint Rewrite <- Z.div_add' using lia : pull_Zdiv.

    Section Flatten.
      Section flatten_column.
        Context (fw : Z).
Definition flatten_column (digit: list Z) : (Z * Z). exact (list_rect (fun _ => (Z * Z)%type) (0,0)
                    (fun xx tl flatten_column_tl =

Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted)

Build Log (contains the Coq error message) (truncated to last 8.0KiB; full 304KiB file on GitHub Actions Artifacts under build.log)

SimplyTypedArithmetic.v", line 56, characters 0-45:
Warning: Trying to mask the absolute name "Coq.omega.PreOmega"!
[masking-absolute-name,deprecated-since-8.8,deprecated,default]
File "./src/Experiments/SimplyTypedArithmetic.v", line 56, characters 0-45:
Warning: Trying to mask the absolute name "Coq.omega.PreOmega"!
[masking-absolute-name,deprecated-since-8.8,deprecated,default]
File "./src/Experiments/SimplyTypedArithmetic.v", line 502, characters 0-77:
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated-since-8.10,deprecated,default]
File "./src/Experiments/SimplyTypedArithmetic.v", line 554, characters 2-41:
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated-since-8.10,deprecated,default]
File "./src/Experiments/SimplyTypedArithmetic.v", line 554, characters 2-41:
Warning: Declaring arbitrary terms as hints is fragile; it is recommended to
declare a toplevel constant instead [fragile-hint-constr,automation,default]
File "./src/Experiments/SimplyTypedArithmetic.v", line 555, characters 2-48:
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated-since-8.10,deprecated,default]
File "./src/Experiments/SimplyTypedArithmetic.v", line 555, characters 2-48:
Warning: Declaring arbitrary terms as hints is fragile; it is recommended to
declare a toplevel constant instead [fragile-hint-constr,automation,default]
File "./src/Experiments/SimplyTypedArithmetic.v", line 556, characters 2-49:
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated-since-8.10,deprecated,default]
File "./src/Experiments/SimplyTypedArithmetic.v", line 556, characters 2-49:
Warning: Declaring arbitrary terms as hints is fragile; it is recommended to
declare a toplevel constant instead [fragile-hint-constr,automation,default]
File "./src/Experiments/SimplyTypedArithmetic.v", line 557, characters 2-47:
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated-since-8.10,deprecated,default]
File "./src/Experiments/SimplyTypedArithmetic.v", line 557, characters 2-47:
Warning: Declaring arbitrary terms as hints is fragile; it is recommended to
declare a toplevel constant instead [fragile-hint-constr,automation,default]
File "./src/Experiments/SimplyTypedArithmetic.v", line 558, characters 2-51:
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated-since-8.10,deprecated,default]
File "./src/Experiments/SimplyTypedArithmetic.v", line 665, characters 2-79:
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated-since-8.10,deprecated,default]
File "./src/Experiments/SimplyTypedArithmetic.v", line 666, characters 2-68:
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated-since-8.10,deprecated,default]
File "./src/Experiments/SimplyTypedArithmetic.v", line 946, characters 6-33:
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated-since-8.10,deprecated,default]
File "./src/Experiments/SimplyTypedArithmetic.v", line 1094, characters 4-37:
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated-since-8.10,deprecated,default]
File "./src/Experiments/SimplyTypedArithmetic.v", line 1482, characters 6-41:
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated-since-8.10,deprecated,default]
File "./src/Experiments/SimplyTypedArithmetic.v", line 1778, characters 4-31:
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated-since-8.10,deprecated,default]
File "./src/Experiments/SimplyTypedArithmetic.v", line 1954, characters 4-69:
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated-since-8.10,deprecated,default]
File "./src/Experiments/SimplyTypedArithmetic.v", line 1999, characters 6-13:
Warning: The Focus command is deprecated; use '2: {' instead.
[deprecated-focus,deprecated-since-8.8,deprecated,default]
File "./src/Experiments/SimplyTypedArithmetic.v", line 2006, characters 23-30:
Warning: The Unfocus command is deprecated
[deprecated-unfocus,deprecated-since-8.8,deprecated,default]
File "./src/Experiments/SimplyTypedArithmetic.v", line 2346, characters 6-43:
Warning: Declaring a scope implicitly is deprecated; use in advance an
explicit "Declare Scope ctype_scope.".
[undeclared-scope,deprecated-since-8.10,deprecated,default]
File "./src/Experiments/SimplyTypedArithmetic.v", line 2372, characters 8-40:
Warning: Declaring a scope implicitly is deprecated; use in advance an
explicit "Declare Scope expr_scope.".
[undeclared-scope,deprecated-since-8.10,deprecated,default]
File "./src/Experiments/SimplyTypedArithmetic.v", line 2374, characters 8-40:
Warning: Declaring a scope implicitly is deprecated; use in advance an
explicit "Declare Scope Expr_scope.".
[undeclared-scope,deprecated-since-8.10,deprecated,default]
File "./src/Experiments/SimplyTypedArithmetic.v", line 3964, characters 10-51:
Warning: Declaring a scope implicitly is deprecated; use in advance an
explicit "Declare Scope cpstype_scope.".
[undeclared-scope,deprecated-since-8.10,deprecated,default]
File "./src/Experiments/SimplyTypedArithmetic.v", line 4042, characters 10-51:
Warning: Declaring a scope implicitly is deprecated; use in advance an
explicit "Declare Scope cpsexpr_scope.".
[undeclared-scope,deprecated-since-8.10,deprecated,default]
File "./src/Experiments/SimplyTypedArithmetic.v", line 6759, characters 4-455:
Warning: Collision between bound variables of name x0
[variable-collision,ltac,default]
File "./src/Experiments/SimplyTypedArithmetic.v", line 6759, characters 4-455:
Warning: Collision between bound variables of name x0
[variable-collision,ltac,default]
Tactic call ran for 0.053 secs (0.053u,0.s) (success)
Tactic call ran for 0.23 secs (0.23u,0.s) (success)
Finished transaction in 1.087 secs (1.083u,0.003s) (successful)
Finished transaction in 1.734 secs (1.724u,0.007s) (successful)
Tactic call ran for 0.048 secs (0.048u,0.s) (success)
Tactic call ran for 0.172 secs (0.172u,0.s) (success)
Tactic call ran for 0.043 secs (0.043u,0.s) (success)
Tactic call ran for 0.178 secs (0.174u,0.003s) (success)
Tactic call ran for 0.004 secs (0.004u,0.s) (success)
Tactic call ran for 0.018 secs (0.018u,0.s) (success)
Tactic call ran for 0.044 secs (0.044u,0.s) (success)
Tactic call ran for 0.232 secs (0.232u,0.s) (success)
Tactic call ran for 0.031 secs (0.031u,0.s) (success)
Tactic call ran for 0.244 secs (0.236u,0.007s) (success)
Tactic call ran for 0.021 secs (0.021u,0.s) (success)
Tactic call ran for 0.15 secs (0.146u,0.003s) (success)
Tactic call ran for 0.054 secs (0.054u,0.s) (success)
Tactic call ran for 0.205 secs (0.205u,0.s) (success)
Tactic call ran for 0. secs (0.u,0.s) (success)
Tactic call ran for 0. secs (0.u,0.s) (success)
File "./src/Experiments/SimplyTypedArithmetic.v", line 7059, characters 4-350:
Error: Anomaly "Not an unfoldable reference."
Please report at http://coq.inria.fr/bugs/.

Command exited with non-zero status 129
src/Experiments/SimplyTypedArithmetic.vo (real: 58.91, user: 58.41, sys: 0.48, mem: 891536 ko)
make: *** [Makefile.coq:847: src/Experiments/SimplyTypedArithmetic.vo] Error 129
make: *** [src/Experiments/SimplyTypedArithmetic.vo] Deleting file 'src/Experiments/SimplyTypedArithmetic.glob'

Minimization Log (truncated to last 8.0KiB; full 235KiB file on GitHub Actions Artifacts under bug.log)

bsolute-name,deprecated-since-8.8,deprecated,default]
File "/tmp/tmpgjvsyity/Crypto/Experiments/SimplyTypedArithmetic.v", line 242, characters 0-31:
Warning: Trying to mask the absolute name "Coq.omega.PreOmega"!
[masking-absolute-name,deprecated-since-8.8,deprecated,default]
File "/tmp/tmpgjvsyity/Crypto/Experiments/SimplyTypedArithmetic.v", line 242, characters 0-31:
Warning: Trying to mask the absolute name "Coq.omega.PreOmega"!
[masking-absolute-name,deprecated-since-8.8,deprecated,default]
File "/tmp/tmpgjvsyity/Crypto/Experiments/SimplyTypedArithmetic.v", line 243, characters 0-44:
Warning: Trying to mask the absolute name "Coq.omega.PreOmega"!
[masking-absolute-name,deprecated-since-8.8,deprecated,default]
File "/tmp/tmpgjvsyity/Crypto/Experiments/SimplyTypedArithmetic.v", line 243, characters 0-44:
Warning: Trying to mask the absolute name "Coq.omega.PreOmega"!
[masking-absolute-name,deprecated-since-8.8,deprecated,default]
File "/tmp/tmpgjvsyity/Crypto/Experiments/SimplyTypedArithmetic.v", line 244, characters 0-33:
Warning: Trying to mask the absolute name "Coq.omega.PreOmega"!
[masking-absolute-name,deprecated-since-8.8,deprecated,default]
File "/tmp/tmpgjvsyity/Crypto/Experiments/SimplyTypedArithmetic.v", line 244, characters 0-33:
Warning: Trying to mask the absolute name "Coq.omega.PreOmega"!
[masking-absolute-name,deprecated-since-8.8,deprecated,default]
File "/tmp/tmpgjvsyity/Crypto/Experiments/SimplyTypedArithmetic.v", line 253, characters 0-51:
Warning: Trying to mask the absolute name "Coq.omega.PreOmega"!
[masking-absolute-name,deprecated-since-8.8,deprecated,default]
File "/tmp/tmpgjvsyity/Crypto/Experiments/SimplyTypedArithmetic.v", line 253, characters 0-51:
Warning: Trying to mask the absolute name "Coq.omega.PreOmega"!
[masking-absolute-name,deprecated-since-8.8,deprecated,default]
File "/tmp/tmpgjvsyity/Crypto/Experiments/SimplyTypedArithmetic.v", line 253, characters 0-51:
Warning: Trying to mask the absolute name "Coq.omega.PreOmega"!
[masking-absolute-name,deprecated-since-8.8,deprecated,default]
File "/tmp/tmpgjvsyity/Crypto/Experiments/SimplyTypedArithmetic.v", line 253, characters 0-51:
Warning: Trying to mask the absolute name "Coq.omega.PreOmega"!
[masking-absolute-name,deprecated-since-8.8,deprecated,default]
File "/tmp/tmpgjvsyity/Crypto/Experiments/SimplyTypedArithmetic.v", line 255, characters 0-64:
Warning: Trying to mask the absolute name "Coq.omega.PreOmega"!
[masking-absolute-name,deprecated-since-8.8,deprecated,default]
File "/tmp/tmpgjvsyity/Crypto/Experiments/SimplyTypedArithmetic.v", line 255, characters 0-64:
Warning: Trying to mask the absolute name "Coq.omega.PreOmega"!
[masking-absolute-name,deprecated-since-8.8,deprecated,default]
File "/tmp/tmpgjvsyity/Crypto/Experiments/SimplyTypedArithmetic.v", line 256, characters 0-36:
Warning: Trying to mask the absolute name "Coq.omega.PreOmega"!
[masking-absolute-name,deprecated-since-8.8,deprecated,default]
File "/tmp/tmpgjvsyity/Crypto/Experiments/SimplyTypedArithmetic.v", line 256, characters 0-36:
Warning: Trying to mask the absolute name "Coq.omega.PreOmega"!
[masking-absolute-name,deprecated-since-8.8,deprecated,default]
File "/tmp/tmpgjvsyity/Crypto/Experiments/SimplyTypedArithmetic.v", line 257, characters 0-54:
Warning: Trying to mask the absolute name "Coq.omega.PreOmega"!
[masking-absolute-name,deprecated-since-8.8,deprecated,default]
File "/tmp/tmpgjvsyity/Crypto/Experiments/SimplyTypedArithmetic.v", line 257, characters 0-54:
Warning: Trying to mask the absolute name "Coq.omega.PreOmega"!
[masking-absolute-name,deprecated-since-8.8,deprecated,default]
File "/tmp/tmpgjvsyity/Crypto/Experiments/SimplyTypedArithmetic.v", line 257, characters 0-54:
Warning: Trying to mask the absolute name "Coq.omega.PreOmega"!
[masking-absolute-name,deprecated-since-8.8,deprecated,default]
File "/tmp/tmpgjvsyity/Crypto/Experiments/SimplyTypedArithmetic.v", line 257, characters 0-54:
Warning: Trying to mask the absolute name "Coq.omega.PreOmega"!
[masking-absolute-name,deprecated-since-8.8,deprecated,default]
File "/tmp/tmpgjvsyity/Crypto/Experiments/SimplyTypedArithmetic.v", line 258, characters 0-40:
Warning: Trying to mask the absolute name "Coq.omega.PreOmega"!
[masking-absolute-name,deprecated-since-8.8,deprecated,default]
File "/tmp/tmpgjvsyity/Crypto/Experiments/SimplyTypedArithmetic.v", line 258, characters 0-40:
Warning: Trying to mask the absolute name "Coq.omega.PreOmega"!
[masking-absolute-name,deprecated-since-8.8,deprecated,default]
File "/tmp/tmpgjvsyity/Crypto/Experiments/SimplyTypedArithmetic.v", line 259, characters 0-37:
Warning: Trying to mask the absolute name "Coq.omega.PreOmega"!
[masking-absolute-name,deprecated-since-8.8,deprecated,default]
File "/tmp/tmpgjvsyity/Crypto/Experiments/SimplyTypedArithmetic.v", line 259, characters 0-37:
Warning: Trying to mask the absolute name "Coq.omega.PreOmega"!
[masking-absolute-name,deprecated-since-8.8,deprecated,default]
File "/tmp/tmpgjvsyity/Crypto/Experiments/SimplyTypedArithmetic.v", line 619, characters 0-77:
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated-since-8.10,deprecated,default]
File "/tmp/tmpgjvsyity/Crypto/Experiments/SimplyTypedArithmetic.v", line 659, characters 2-41:
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated-since-8.10,deprecated,default]
File "/tmp/tmpgjvsyity/Crypto/Experiments/SimplyTypedArithmetic.v", line 659, characters 2-41:
Warning: Declaring arbitrary terms as hints is fragile; it is recommended to
declare a toplevel constant instead [fragile-hint-constr,automation,default]
File "/tmp/tmpgjvsyity/Crypto/Experiments/SimplyTypedArithmetic.v", line 660, characters 2-48:
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated-since-8.10,deprecated,default]
File "/tmp/tmpgjvsyity/Crypto/Experiments/SimplyTypedArithmetic.v", line 660, characters 2-48:
Warning: Declaring arbitrary terms as hints is fragile; it is recommended to
declare a toplevel constant instead [fragile-hint-constr,automation,default]
File "/tmp/tmpgjvsyity/Crypto/Experiments/SimplyTypedArithmetic.v", line 661, characters 2-49:
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated-since-8.10,deprecated,default]
File "/tmp/tmpgjvsyity/Crypto/Experiments/SimplyTypedArithmetic.v", line 661, characters 2-49:
Warning: Declaring arbitrary terms as hints is fragile; it is recommended to
declare a toplevel constant instead [fragile-hint-constr,automation,default]
File "/tmp/tmpgjvsyity/Crypto/Experiments/SimplyTypedArithmetic.v", line 662, characters 2-47:
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated-since-8.10,deprecated,default]
File "/tmp/tmpgjvsyity/Crypto/Experiments/SimplyTypedArithmetic.v", line 662, characters 2-47:
Warning: Declaring arbitrary terms as hints is fragile; it is recommended to
declare a toplevel constant instead [fragile-hint-constr,automation,default]
File "/tmp/tmpgjvsyity/Crypto/Experiments/SimplyTypedArithmetic.v", line 663, characters 2-51:
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated-since-8.10,deprecated,default]
File "/tmp/tmpgjvsyity/Crypto/Experiments/SimplyTypedArithmetic.v", line 675, characters 0-5:
Error: Some unresolved existential variables remain


�[93mIntermediate code not saved.�[0m
Failed to do everything at once; trying one at a time.
Admitting definitions unsuccessful.
No successful changes.

I will now attempt to export modules
Module exportation successful

I will now attempt to split imports and exports
Import/Export splitting successful

I will now attempt to split := definitions
One-line definition splitting successful

I will now attempt to remove all lines, one at a time

If you have any comments on your experience of the minimizer, please share them in a reply (possibly tagging @JasonGross).
If you believe there's a bug in the bug minimizer, please report it on the bug minimizer issue tracker.