Prototype for Probably Correct: Oscar issue 3110

[JohnAAbbott]

Prototype implementation incorporating some feedback.
This code is needed to make the PRs in Oscar and Nemo work.

[codecov]

Codecov Report

❌ Patch coverage is 0% with 19 lines in your changes missing coverage. Please review.
✅ Project coverage is 88.12%. Comparing base (487ce33) to head (69d63bb).
⚠️ Report is 63 commits behind head on master.

Files with missing lines	Patch %	Lines
src/ProbablyCorrect.jl	0.00%	19 Missing ⚠️

Additional details and impacted files

@@            Coverage Diff             @@
##           master    #2395      +/-   ##
==========================================
- Coverage   88.14%   88.12%   -0.03%     
==========================================
  Files         128      129       +1     
  Lines       32886    32909      +23     
==========================================
+ Hits        28987    29000      +13     
- Misses       3899     3909      +10     

☔ View full report in Codecov by Harness.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.

[JohnAAbbott]

FWIW here is the test suite that I have been using (not intended to be exhaustive).

# Not really sure how to test DodgyMode

AbstractAlgebra.set_dodgy_mode(false)
AbstractAlgebra.dodgy_steps_clear()
AbstractAlgebra.dodgy_steps_get()  # should be an empty list

p1 = 97;
is_prime(p1);
isempty(AbstractAlgebra.dodgy_steps_get())  || println("OOPS!");

P1 = ZZ(p1)
is_prime(P1);
isempty(AbstractAlgebra.dodgy_steps_get())  || println("OOPS!");

N = P1^20;
is_prime(N);  # false, of course!
isempty(AbstractAlgebra.dodgy_steps_get())  || println("OOPS!");

P2 = next_prime(N);
isempty(AbstractAlgebra.dodgy_steps_get())  || println("OOPS!");

is_prime(P2);
isempty(AbstractAlgebra.dodgy_steps_get())  || println("OOPS!");

P3 = 73742412689492826067; # too big to be Int64, so is Int128
is_prime(P3);
isempty(AbstractAlgebra.dodgy_steps_get())  || println("OOPS!");

next_prime(P3);
isempty(AbstractAlgebra.dodgy_steps_get())  || println("OOPS!");

AbstractAlgebra.set_dodgy_mode(true)

is_prime(p1);
isempty(AbstractAlgebra.dodgy_steps_get())  || println("OOPS!");

is_prime(P1); # the value of P1 is "small", so result is surely correct (and so does not need to be registered in the log of dodgy steps)
isempty(AbstractAlgebra.dodgy_steps_get())  || println("OOPS!");

is_prime(N);  # false, of course!
isempty(AbstractAlgebra.dodgy_steps_get())  || println("OOPS!");

P2 = next_prime(N);
(length(AbstractAlgebra.dodgy_steps_get()) == 1)  || println("OOPS!");

is_prime(P2);
(length(AbstractAlgebra.dodgy_steps_get()) == 2)  || println("OOPS!");

is_prime(P3);
(length(AbstractAlgebra.dodgy_steps_get()) == 3)  || println("OOPS!");

next_prime(P3);
(length(AbstractAlgebra.dodgy_steps_get()) == 4)  || println("OOPS!");

next_prime(P3, true);  # verify value is prime
(length(AbstractAlgebra.dodgy_steps_get()) == 4)  || println("OOPS!");

next_prime(P3, false); # do not verify that value is prime
(length(AbstractAlgebra.dodgy_steps_get()) == 4)  || println("OOPS!");

AbstractAlgebra.dodgy_steps_get()

##################################################################

AbstractAlgebra.set_dodgy_mode(false)
AbstractAlgebra.dodgy_steps_clear()
isempty(AbstractAlgebra.dodgy_steps_get())  || println("OOPS!");


QQxy,(x,y) = QQ["x","y"]
L = [x^2+y+1, y^2+x+1];

I = ideal(L)
GB = groebner_basis(I);
isempty(AbstractAlgebra.dodgy_steps_get())  || println("OOPS!");

I = ideal(L)
SB = standard_basis(I);
isempty(AbstractAlgebra.dodgy_steps_get())  || println("OOPS!");


AbstractAlgebra.set_dodgy_mode(true)

I = ideal(L)
GB = groebner_basis(I);
(length(AbstractAlgebra.dodgy_steps_get()) == 1)  || println("OOPS!");

I = ideal(L)
SB = standard_basis(I);
(length(AbstractAlgebra.dodgy_steps_get()) == 2)  || println("OOPS!");

# Now we see where there were "potentially" dodgy computations:
AbstractAlgebra.dodgy_steps_get()


# ----- Over a finite field: cannot use :modular when DodgyMode is active -----

AbstractAlgebra.set_dodgy_mode(false)
AbstractAlgebra.dodgy_steps_clear()
isempty(AbstractAlgebra.dodgy_steps_get())  || println("OOPS!");

k = Native.GF(101);
kxy,(x,y) = k["x","y"]
L = [x^2+y+1, y^2+x+1];

I = ideal(L)
GB = groebner_basis(I);
isempty(AbstractAlgebra.dodgy_steps_get())  || println("OOPS!");

I = ideal(L)
SB = standard_basis(I);
isempty(AbstractAlgebra.dodgy_steps_get())  || println("OOPS!");


AbstractAlgebra.set_dodgy_mode(true)

I = ideal(L)
GB = groebner_basis(I);
isempty(AbstractAlgebra.dodgy_steps_get())  || println("OOPS!");

I = ideal(L)
SB = standard_basis(I);
isempty(AbstractAlgebra.dodgy_steps_get())  || println("OOPS!");

# --> THERE WERE NO "potentially" dodgy computations

[YueRen]

Some thoughts that I also voiced during today's rebel triage.

First off, the main reason behind what I am about to suggest are twofold:

1. Ensure that the system can be easily extended once the need for local probabilistic scopes eventually arises. For example: If I have a huge tropical computation where the bottleneck are all matroidal, I would like to be able to set all matroidal algorithms to probabilistic whilst keeping all Groebner bases exact.
2. Ensure that the user experience is as consistent with existing functions as possible.

Now here is what I suggest (I haven't given it nearly as much thought as @JohnAAbbott and some others, so take it with a grain of salt):

1. The logging system is great and some form of logging system should definitely stay!
2. Add new functions add_probabilistic_scope and set_probabilistic_level (names are up to debate) mirroring existing functions on verbosity and assertions.
3. Add a global dodgy scope for now as in this PR. We can make the system finer if the need arises.

The result is hopefully something that is feature-wise similar to the current PR, usability-wiser similar to existing features in AbstractAlgebra, and easily extendable in the future.