JasonGross
commented
1 year ago 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)
```coq
(* 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:(iIntermediate Coq File (useful for debugging if minimization did not go as far as you wanted)
```coq ```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 https://github.com/coq/coq/issues/18239#issuecomment-1788443775
coqbot
https://github.com/coq/coq/pull/17888#issuecomment-1653573500 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)
```coq 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:Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted)
```coq ```Build Log (contains the Coq error message) (truncated to last 8.0KiB; full 11MiB file on GitHub Actions Artifacts under
``` 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:: ```build.log)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, inIf 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.