Existential Specs and the monoid instance (<>) sometimes fails

[TimSheard]

Consider the following specification built from evenSpec an existential, and the simple assertion that x is greater than 10. Surely there are even numbers greater than 10. This should succeed. but it does not

ghci> debugSpec $ constrained $ \ x -> [satisfies x evenSpec, Assert $ x >. 10] 
Stepping the plan:

    SolverPlan

      Linearization:
      v_2 <-
        ErrorSpec
          The two Integer Specifications are inconsistent.
            MemberSpec [ 10 ]
            TypeSpec [11..] []
  Env
  somey_0 -> 5


StepPlan for variable: v_2 fails to produce Specification, probably overconstrained.PS = 
Original spec ErrorSpec
  The two Integer Specifications are inconsistent.
    MemberSpec [ 10 ]
    TypeSpec [11..] []
Predicates
The two Integer Specifications are inconsistent.
  MemberSpec [ 10 ]
  TypeSpec [11..] []

Here is the definition of evenSpec which is defined in cardano-ledger/libs/constrained/Examples/Fold.hs

evenSpec ::
  forall n.
  (TypeSpec n ~ NumSpec n, Integral n, HasSpec n, MaybeBounded n) =>
  Specification n
evenSpec = ExplainSpec ["even via (x+x)"] $
  constrained $ \ [var|evenx|] ->
    exists
      (\eval -> pure (div (eval evenx) 2))
      (\ [var|somey|] -> [assert $ evenx ==. somey + somey])

The same problem also occurs in oddSpec which is also an Existential, but fixed to Int, rather than Integral

oddSpec :: Specification Int
oddSpec = ExplainSpec ["odd via (y+y+1)"] $
  constrained $ \ [var|oddx|] ->
    exists
      (\eval -> pure (div (eval oddx - 1) 2))
      (\ [var|y|] -> [assert $ oddx ==. y + y + 1])

It would be good ti find a way to fix this.

[MaximilianAlgehed]

The problem boils down to this:

$> printPlan $ constrained @Int $ \ [var|x|] -> [satisfies x evenSpec, Assert $ x >. 10]
Simplified spec:
  constrained $ \ x_2 ->
    {exists somey_0 in
     Explain ["even via (x+x)"] $ assert $ x_2 ==. addFn somey_0 somey_0
     assert $ 11 <=. x_2}

  SolverPlan

    Linearization:
    somey_0 <- 
    x_2 <-
      TypeSpec [11..] []
      ---
      Explain ["even via (x+x)"] $ assert $ x_2 ==. addFn somey_0 somey_0
      assert $ x_2 ==. addFn somey_0 somey_0

The plan here says to solve somey before we do anything about x even though we know that x == somey + somey. The problem is that back-propagation can't kick in properly here because there is no way to back-propagate TypeSpec [11..] [] over somey + somey. Two possible solutions:

1. Work out some nifty way of propagating over arbitrary expressions in a single variable (hard, but might be necessary)
2. Rewrite somey + somey to 2 * somey, thus allowing us to back-propagate because the assert $ x == somey + somey constraint is now assert $ x == 2 * somey.

[MaximilianAlgehed]

I tried testing this fix by trying to quickly introduce a multiplication operation. However, doing so became (perhaps unnecessarily) difficult because of the generality of the way we deal with numbers and number specifications. I don't yet know what the right approach to fixing this is but I'm afraid we might need to re-work numbers a little bit to make working with that code not suck badly.

[TimSheard]

So remember the experimental PR for Pressburger arithmetic? That was one attempt. The problem is that NumberSpec will need some sort of coefficiant, saying all the numbers in the range are multiplied by some constant.