fact: Fixpoint fuzzLoopAux {A} (fuel : nat) (st : State) (favored : list (nat * A)) (discards : list (nat * A)) (favored_queue : list (nat * A)) (discard_queue : list (nat * A)) (randoms : nat) (saved : list (nat * A)) (gen : G A) (fuzz : A -> G A) (print : A -> string) (prop : A -> option bool) : Result := match fuel with | O => giveUp st | S fuel' => if (gte (numSuccessTests st) (maxSuccessTests st)) then let x : nat := printnvb tt in doneTestingFuzz (trace (show x) x) st else if (gte (numDiscardedTests st) (maxDiscardedTests st)) then giveUp st else let size := (computeSize st) (numSuccessTests st) (numDiscardedTests st) in let (rnd1, rnd2) := randomSplit (randomSeed st) in let '(g,favored',discards',favored_queue', discard_queue', randoms', saved') := pick_next gen fuzz favored discards favored_queue discard_queue randoms saved in let a := run g size rnd1 in let '(res, (is_interesting, energy)) := withInstrumentation (fun _ : unit => prop a) in let zero_0 := 0 in match res with | Some true => match clear_queues fuel with | true => fuzzLoopAux fuel' (updSuccTests st S) nil nil nil nil randoms' nil gen fuzz print prop | _ => if is_interesting then fuzzLoopAux fuel' (updSuccTests st S) favored' discards' ((energy, a)::favored_queue') discard_queue' randoms' ((energy,a) :: saved') gen fuzz print prop else fuzzLoopAux fuel' (updSuccTests st S) favored' discards' favored_queue' discard_queue' randoms' saved' gen fuzz print prop end | Some false => let '(MkState mst mdt ms cs nst ndt ls e r nss nts ana) := st in let zero := trace (print a ++ nl) zero_0 in let pre : string := "*** Failed " in let numShrinks := 0 in let suf := ("after " ++ (show (S nst)) ++ " tests and " ++ (show numShrinks) ++ " shrinks. (" ++ (show ndt) ++ " discards)")%string in Failure (nst + 1 + zero) numShrinks ndt r size (pre ++ suf) (summary st) "Falsified!" | None => match clear_queues fuel with | true => fuzzLoopAux fuel' (updDiscTests st S) nil nil nil nil randoms' nil gen fuzz print prop | _ => if is_interesting then fuzzLoopAux fuel' (updDiscTests st S) favored' discards' favored_queue' ((energy, a)::discard_queue') randoms' saved' gen fuzz print prop else fuzzLoopAux fuel' (updDiscTests st S) favored' discards' favored_queue' discard_queue' randoms' saved' gen fuzz print prop end end end.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrnat ssrbool eqtype div) ExtLib(Structures.Monad) SimpleIO(SimpleIO) QuickChick(RoseTrees RandomQC Generators Producer SemChecker) QuickChick(Show Checker State Classes) Coq.Strings.Ascii Coq.Strings.String List Recdef Arith.EqNat ZArith