Parallize __proof_field_positions

This gives a significant speedup on the SPDM spec:
   - Original: 15m26
   - Parallel: 9m59

Ref. #625

rflx/model/message.py

@@ -3,6 +3,7 @@
 import itertools
 from abc import abstractmethod
 from collections import defaultdict
+from concurrent.futures import ProcessPoolExecutor
 from copy import copy
 from dataclasses import dataclass, field as dataclass_field
 from typing import Dict, List, Mapping, Optional, Sequence, Set, Tuple, Union
@@ -640,6 +641,26 @@ def __compute_field_condition(self, final: Field) -> expr.Expr:
         )
 
 
+def check_proofs(
+    proofs: List[Tuple[expr.Expr, List[expr.Expr], expr.ProofResult, RecordFluxError, bool]]
+) -> RecordFluxError:
+    result = RecordFluxError()
+    for goal, facts, expected, error, unsat in proofs:
+        proof = goal.check(facts)
+        if proof.result == expected:
+            continue
+        result.extend(error)
+        if unsat:
+            result.extend(
+                [
+                    (f'unsatisfied "{m}"', Subsystem.MODEL, Severity.INFO, locn)
+                    for m, locn in proof.error
+                ]
+            )
+        break
+    return result
+
+
 class Message(AbstractMessage):
     # pylint: disable=too-many-arguments
     def __init__(
@@ -1490,28 +1511,10 @@ def proofs() -> List[
                     results.append(result)
             return results
 
-        def check(
-            proofs: List[Tuple[expr.Expr, List[expr.Expr], expr.ProofResult, RecordFluxError, bool]]
-        ) -> RecordFluxError:
-            result = RecordFluxError()
-            for goal, facts, expected, error, unsat in proofs:
-                proof = goal.check(facts)
-                if proof.result == expected:
-                    continue
-                result.extend(error)
-                if unsat:
-                    result.extend(
-                        [
-                            (f'unsatisfied "{m}"', Subsystem.MODEL, Severity.INFO, locn)
-                            for m, locn in proof.error
-                        ]
-                    )
-                break
-            return result
-
-        errors = map(check, proofs())
-        for e in errors:
-            self.error.extend(e)
+        with ProcessPoolExecutor() as executor:
+            errors = executor.map(check_proofs, proofs())
+            for e in errors:
+                self.error.extend(e)
         self.error.propagate()
 
     def __prove_message_size(self) -> None: