Remove proof of message coverage

This property is true by construction and a verification is useless.

Also remove corresponding unit tests.

For eng/recordflux/recordflux#1495

CHANGELOG.md

@@ -5,6 +5,12 @@ All notable changes to this project will be documented in this file.
 The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
 and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
 
+## [Unreleased]
+
+### Removed
+
+- Verification of message bit coverage (eng/recordflux/RecordFlux#1495)
+
 ## [0.16.0] - 2023-12-05
 
 ### Added
@@ -434,6 +440,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## [0.1.0] - 2019-05-14
 
+[Unreleased]: https://github.com/AdaCore/RecordFlux/compare/v0.16.0...HEAD
 [0.16.0]: https://github.com/AdaCore/RecordFlux/compare/v0.15.0...v0.16.0
 [0.15.0]: https://github.com/AdaCore/RecordFlux/compare/v0.14.0...v0.15.0
 [0.14.0]: https://github.com/AdaCore/RecordFlux/compare/v0.13.0...v0.14.0

rflx/model/message.py

@@ -1248,7 +1248,6 @@ def _verify(self) -> None:
 
             self._prove_static_conditions(proofs)
             self._prove_conflicting_conditions(proofs)
-            self._prove_coverage(proofs)
             self._prove_overlays(proofs)
             self._prove_field_positions(proofs, valid_paths)
             self._prove_message_size(proofs)
@@ -1822,71 +1821,6 @@ def is_proper_prefix(path: tuple[Link, ...], paths: set[tuple[Link, ...]]) -> bo
                         )
                     self.error.extend(error)
 
-    def _prove_coverage(self, proofs: expr.ParallelProofs) -> None:
-        """
-        Prove that the fields of a message cover all message bits.
-
-        This ensures that there are no holes in the message definition.
-
-        Idea: Let f be the bits covered by the message. By definition
-            (1) f >= Message'First and f <= Message'Last
-        holds. For every field add a conjunction of the form
-            (2) Not(f >= Field'First and f <= Field'Last),
-        effectively pruning the range that this field covers from the bit range of the message. For
-        the overall expression, prove that it is false for all f, i.e. no bits are left.
-        """
-        for path in [p[:-1] for p in self.paths(FINAL) if p]:
-            facts: Sequence[expr.Expr]
-
-            # Calculate (1)
-            facts = [
-                expr.GreaterEqual(expr.Variable("f"), expr.First("Message")),
-                expr.LessEqual(expr.Variable("f"), expr.Last("Message")),
-            ]
-            # Calculate (2) for all fields
-            facts.extend(
-                [
-                    expr.Not(
-                        expr.And(
-                            expr.GreaterEqual(expr.Variable("f"), self._target_first(l)),
-                            expr.LessEqual(expr.Variable("f"), self._target_last(l)),
-                            location=l.location,
-                        ),
-                    )
-                    for l in path
-                ],
-            )
-
-            # Define that the end of the last field of a path is the end of the message
-            facts.append(
-                expr.Equal(self._target_last(path[-1]), expr.Last("Message"), self.location),
-            )
-
-            # Constraints for links on path
-            facts.extend(self._path_constraints(path))
-
-            # Coverage expression must be False, i.e. no bits left
-            error = RecordFluxError(
-                [
-                    (
-                        "path does not cover whole message",
-                        Subsystem.MODEL,
-                        Severity.ERROR,
-                        self.identifier.location,
-                    ),
-                    *[
-                        (
-                            f'on path: "{l.target.identifier}"',
-                            Subsystem.MODEL,
-                            Severity.INFO,
-                            l.target.identifier.location,
-                        )
-                        for l in path
-                    ],
-                ],
-            )
-            proofs.add(expr.TRUE, facts, sat_error=error, unknown_error=error)
-
     def _prove_overlays(self, proofs: expr.ParallelProofs) -> None:
         for f in (INITIAL, *self.fields):
             for p, l in [(p, p[-1]) for p in self.paths(f) if p]:

tests/unit/model/message_test.py

@@ -1933,61 +1933,6 @@ def test_incongruent_overlay() -> None:
     )
 
 
-def test_field_coverage_1(monkeypatch: pytest.MonkeyPatch) -> None:
-    structure = [
-        Link(INITIAL, Field("F1")),
-        Link(Field("F1"), Field("F2"), first=Add(First("Message"), Number(64))),
-        Link(Field("F2"), FINAL),
-    ]
-
-    types = {Field("F1"): models.integer(), Field("F2"): models.integer()}
-    monkeypatch.setattr(Message, "_verify_links", lambda _: None)
-    assert_message_model_error(
-        structure,
-        types,
-        r"^"
-        r"model: error: path does not cover whole message\n"
-        r'model: info: on path: "F1"\n'
-        r'model: info: on path: "F2"'
-        r"$",
-    )
-
-
-def test_field_coverage_2(monkeypatch: pytest.MonkeyPatch) -> None:
-    structure = [
-        Link(INITIAL, Field("F1")),
-        Link(Field("F1"), Field("F2")),
-        Link(Field("F2"), Field("F4"), Greater(Variable("F1"), Number(100))),
-        Link(
-            Field("F2"),
-            Field("F3"),
-            LessEqual(Variable("F1"), Number(100)),
-            first=Add(Last("F2"), Number(64)),
-        ),
-        Link(Field("F3"), Field("F4")),
-        Link(Field("F4"), FINAL),
-    ]
-
-    types = {
-        Field("F1"): models.integer(),
-        Field("F2"): models.integer(),
-        Field("F3"): models.integer(),
-        Field("F4"): models.integer(),
-    }
-    monkeypatch.setattr(Message, "_verify_links", lambda _: None)
-    assert_message_model_error(
-        structure,
-        types,
-        r"^"
-        r"model: error: path does not cover whole message\n"
-        r'model: info: on path: "F1"\n'
-        r'model: info: on path: "F2"\n'
-        r'model: info: on path: "F3"\n'
-        r'model: info: on path: "F4"'
-        r"$",
-    )
-
-
 def test_field_after_message_start(monkeypatch: pytest.MonkeyPatch) -> None:
     structure = [
         Link(INITIAL, Field("F1")),