uwu

src/f4/f4.jl

@@ -40,8 +40,7 @@
         permutation = collect(1:(basis.nfilled))
     end
 
-    # Divide each polynomial by the leading coefficient. We do not need
-    # normalization in some cases, e.g., when computing the normal forms
+    # We do not need normalization when computing normal forms
     if make_monic
         basis_make_monic!(basis, params.arithmetic, params.changematrix)
     end
@@ -400,8 +399,6 @@ end
 
 # Adds the first `npairs` pairs from the pairset to the matrix.
 # Write the corresponding monomials to symbolic hashtable.
-#
-# Assumes that the pairset is sorted w.r.t. the lcms of pairs.
 function f4_add_critical_pairs_to_matrix!(
     ctx::Context,
     pairset::Pairset,
@@ -411,6 +408,11 @@ function f4_add_critical_pairs_to_matrix!(
     ht::MonomialHashtable,
     symbol_ht::MonomialHashtable
 )
+    @invariant issorted(
+        pairset.pairs[1:npairs],
+        by=pair -> monom_totaldeg(ht.monoms[pair.lcm])
+    )
+
     matrix_reinitialize!(matrix, npairs)
     pairs = pairset.pairs
     uprows = matrix.upper_rows
@@ -488,7 +490,6 @@ function f4_add_critical_pairs_to_matrix!(
             # hash of the quotient
             htmp = ht.hashdata[lcm].hash - ht.hashdata[vidx].hash
 
-            # The polynomial will be reduced.
             row_idx = matrix.nrows_filled_lower += 1
             lowrows[row_idx] = matrix_polynomial_multiple_to_row!(
                 ctx,
@@ -566,7 +567,7 @@ end
     end
 
     if params.sweep
-        @log :debug "Sweeping redundant elements in the basis"
+        @log :debug "Sweeping redundant elements in the basis.."
         basis_sweep_redundant!(basis, hashtable)
     end
 
@@ -591,8 +592,6 @@ end
     nothing
 end
 
-# Checks that all S-polynomials formed by the elements of the given basis reduce
-# to zero.
 @timeit function f4_isgroebner!(
     ctx::Context,
     ring::PolyRing,
@@ -624,7 +623,6 @@ end
     linalg_isgroebner!(ctx, matrix, basis, arithmetic)
 end
 
-# Reduces each polynomial in the `tobereduced` by the polynomials from the `basis`.
 @timeit function f4_normalform!(
     ctx::Context,
     ring::PolyRing,

src/f4/linalg/backend.jl

@@ -1066,8 +1066,7 @@ function linalg_extract_sparse_row!(
     from::J,
     to::J
 ) where {I, J, T <: Coeff, A <: Coeff}
-    # NOTE: also assumes that the provided sparse row has the necessary capacity
-    # allocated
+    # NOTE: assumes that the sparse row has the necessary capacity allocated
     @invariant length(indices) == length(coeffs)
     @invariant 1 <= from <= to <= length(row)
 
@@ -1082,6 +1081,7 @@ function linalg_extract_sparse_row!(
         end
     end
 
+    @invariant j - 1 <= length(coeffs)
     j - 1
 end
 
@@ -1096,8 +1096,7 @@ function linalg_extract_sparse_row!(
     from::J,
     to::J
 ) where {I, J, T <: Coeff}
-    # NOTE: also assumes that the provided sparse row has the necessary capacity
-    # allocated
+    # NOTE: assumes that the sparse row has the necessary capacity allocated
     @invariant length(indices) == length(coeffs)
     @invariant 1 <= from <= to <= length(row)
 
@@ -1111,5 +1110,6 @@ function linalg_extract_sparse_row!(
         end
     end
 
+    @invariant j - 1 <= length(coeffs)
     j - 1
 end

src/groebner/correctness.jl

@@ -46,11 +46,6 @@
             params
         )
             @log :misc "Randomized check failed."
-
-            # Freeze the hashtable.
-            # TODO: this is a strange place to do it, but OK
-            # hashtable.frozen = true
-
             return false
         end
         @log :misc "Randomized check passed!"

src/groebner/groebner.jl

@@ -498,7 +498,7 @@ function _groebner_learn_and_apply_threaded(
     end
     threadbuf_bigint_buffer = map(_ -> CoefficientBuffer(), 1:nthreads())
     threadbuf_params = map(_ -> deepcopy(params), 1:nthreads())
-    threadbuf_ctx = map(_ -> ctx_initialize(tlocal=true), 1:nthreads())
+    threadbuf_ctx = map(_ -> ctx_initialize(), 1:nthreads())
 
     iters = 0
     while !correct_basis