Support expected/unexpected results in parallel proofs

Ref. #625

rflx/model/message.py

@@ -641,13 +641,13 @@ def __compute_field_condition(self, final: Field) -> expr.Expr:
         )
 
 
-class Proofs:
+class ParallelProofs:
     def __init__(self) -> None:
         self.proofs: List[
-            List[Tuple[expr.Expr, List[expr.Expr], expr.ProofResult, RecordFluxError, bool]]
+            List[Tuple[expr.Expr, List[expr.Expr], expr.ProofResult, RecordFluxError, bool, bool]]
         ] = []
         self.current: List[
-            Tuple[expr.Expr, List[expr.Expr], expr.ProofResult, RecordFluxError, bool]
+            Tuple[expr.Expr, List[expr.Expr], expr.ProofResult, RecordFluxError, bool, bool]
         ] = []
 
     def add(
@@ -656,9 +656,10 @@ def add(
         facts: List[expr.Expr],
         expected: expr.ProofResult,
         message: RecordFluxError,
+        unexpected: bool = False,
         add_unsat: bool = False,
     ) -> None:
-        self.current.append((goal, facts, expected, message, add_unsat))
+        self.current.append((goal, facts, expected, message, unexpected, add_unsat))
 
     def pop(self) -> None:
         if self.current:
@@ -671,9 +672,9 @@ def check_proof(
         argument: List[Tuple[expr.Expr, List[expr.Expr], expr.ProofResult, RecordFluxError, bool]],
     ) -> RecordFluxError:
         result = RecordFluxError()
-        for goal, facts, expected, message, add_unsat in argument:
+        for goal, facts, expected, message, unexpected, add_unsat in argument:
             proof = goal.check(facts)
-            if proof.result == expected:
+            if unexpected == (proof.result != expected):
                 continue
             result.extend(message)
             if add_unsat:
@@ -688,7 +689,7 @@ def check_proof(
     def check(self, error: RecordFluxError) -> None:
         self.pop()
         with ProcessPoolExecutor() as executor:
-            for e in executor.map(Proofs.check_proof, self.proofs):
+            for e in executor.map(ParallelProofs.check_proof, self.proofs):
                 error.extend(e)
         error.propagate()
 
@@ -1416,7 +1417,7 @@ def __prove_overlays(self) -> None:
 
     def __prove_field_positions(self) -> None:
         # pylint: disable=too-many-locals
-        proofs = Proofs()
+        proofs = ParallelProofs()
         for f in (*self.fields, FINAL):
             for path in self.paths(f):
                 last = path[-1]