Simplify Valid_Context predicate and generating code

* Now for each field, only specify First/Size for this field, don't
  express anything about successor fields
* Use existing Field_First_Internal/Field_Size_Internal functions
* bump timeout for ping
* add unit test for more coverage

For eng/recordflux/recordflux#1382

CHANGELOG.md

@@ -16,6 +16,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 - Syntax for passing repeated `-i` and `-v` options to `rflx validate` (eng/recordflux/RecordFlux#1441)
 - Simplified setter code and removed internal `Successor` function (eng/recordflux/RecordFlux#1448)
+- Simplified `Valid_Context` predicate (eng/recordflux/RecordFlux#1382)
 
 ### Fixed
 

examples/apps/ping/ping.gpr

@@ -33,6 +33,7 @@ project Ping is
    package Prove is
       for Proof_Switches ("Ada") use Defaults.Proof_Switches;
       for Proof_Switches ("rflx-rflx_arithmetic.adb") use ("--prover=Z3,altergo,cvc5,colibri", "--timeout=120");
+      for Proof_Switches ("rflx-icmp-message.adb") use ("--timeout=120");
    end Prove;
 
 end Ping;

rflx/generator/common.py

@@ -322,7 +322,6 @@ def type_conversion(expression: expr.Expr) -> expr.Expr:
 
 def message_structure_invariant(
     message: model.Message,
-    prefix: str,
     embedded: bool = False,
 ) -> Expr:
     """
@@ -338,97 +337,64 @@ def message_structure_invariant(
     def prefixed(name: str) -> expr.Expr:
         return expr.Selected(expr.Variable("Ctx"), name) if not embedded else expr.Variable(name)
 
-    def link_property(link: model.Link, unique: bool) -> Expr:
-        field_type = message.types[link.target]
-        condition = link.condition.substituted(substitution(message, prefix, embedded)).simplified()
-        size = (
-            field_type.size
-            if isinstance(field_type, model.Scalar)
-            else link.size.substituted(
-                substitution(message, prefix, embedded, target_type=const.TYPES_BIT_LENGTH),
-            ).simplified()
-        )
-        first = (
-            prefixed("First")
-            if link.source == model.INITIAL
-            else link.first.substituted(
-                substitution(message, prefix, embedded, target_type=const.TYPES_BIT_INDEX),
-            )
-            .substituted(
-                mapping={
-                    expr.UNDEFINED: expr.Add(
-                        expr.Selected(
-                            expr.Indexed(
-                                prefixed("Cursors"),
-                                expr.Variable(link.source.affixed_name),
+    def field_property(fld: model.Field) -> Expr:
+        return AndThen(
+            Equal(
+                Add(
+                    Sub(
+                        Selected(
+                            Indexed(
+                                prefixed("Cursors").ada_expr(),
+                                Variable(fld.affixed_name),
                             ),
                             "Last",
                         ),
-                        expr.Number(1),
+                        Selected(
+                            Indexed(
+                                prefixed("Cursors").ada_expr(),
+                                Variable(fld.affixed_name),
+                            ),
+                            "First",
+                        ),
                     ),
-                },
-            )
-            .simplified()
-        )
-        precond = (
-            AndThen(
+                    Number(1),
+                ),
                 Call(
-                    "Well_Formed",
-                    [Indexed(Variable("Cursors"), Variable(link.source.affixed_name))],
+                    "Field_Size_Internal",
+                    [
+                        Variable("Cursors"),
+                        Variable("First"),
+                        Variable("Verified_Last"),
+                        Variable("Written_Last"),
+                        Variable("Buffer"),
+                        *[Variable(fld.name) for fld in message.parameter_types],
+                        Variable(fld.affixed_name),
+                    ],
                 ),
-                condition.ada_expr(),
-            )
-            if link.source != model.INITIAL and not unique
-            else TRUE
-        )
-
-        return If(
-            [
-                (
-                    precond,
-                    AndThen(
-                        Equal(
-                            Add(
-                                Sub(
-                                    Selected(
-                                        Indexed(
-                                            prefixed("Cursors").ada_expr(),
-                                            Variable(link.target.affixed_name),
-                                        ),
-                                        "Last",
-                                    ),
-                                    Selected(
-                                        Indexed(
-                                            prefixed("Cursors").ada_expr(),
-                                            Variable(link.target.affixed_name),
-                                        ),
-                                        "First",
-                                    ),
-                                ),
-                                Number(1),
-                            ),
-                            size.ada_expr(),
-                        ),
-                        Equal(
-                            Selected(
-                                Indexed(
-                                    prefixed("Cursors").ada_expr(),
-                                    Variable(link.target.affixed_name),
-                                ),
-                                "First",
-                            ),
-                            first.ada_expr(),
-                        ),
+            ),
+            Equal(
+                Selected(
+                    Indexed(
+                        prefixed("Cursors").ada_expr(),
+                        Variable(fld.affixed_name),
                     ),
+                    "First",
                 ),
-            ],
+                Call(
+                    "Field_First_Internal",
+                    [
+                        Variable("Cursors"),
+                        Variable("First"),
+                        Variable("Verified_Last"),
+                        Variable("Written_Last"),
+                        Variable("Buffer"),
+                        *[Variable(fld.name) for fld in message.parameter_types],
+                        Variable(fld.affixed_name),
+                    ],
+                ),
+            ),
         )
 
-    def field_property(fld: model.Field) -> Expr:
-        incoming = message.incoming(fld)
-        unique = len(incoming) == 1
-        return AndThen(*[link_property(link, unique) for link in incoming])
-
     def map_invariant(fld: model.Field) -> Expr:
         return If(
             [
@@ -447,7 +413,6 @@ def map_invariant(fld: model.Field) -> Expr:
 
 def context_predicate(
     message: model.Message,
-    prefix: str,
 ) -> Expr:
     def invalid_successors_invariant() -> Expr:
         """
@@ -529,7 +494,7 @@ def invalid_successors_invariant() -> Expr:
             ],
         ),
         invalid_successors_invariant(),
-        message_structure_invariant(message, prefix, embedded=True),
+        message_structure_invariant(message, embedded=True),
     )
 
 

rflx/generator/generator.py

@@ -496,7 +496,6 @@ def _create_message(self, message: Message) -> dict[ID, Unit]:  # noqa: PLR0912
             self._executor.submit(
                 message_generator.create_valid_context_function,
                 message,
-                self._prefix,
             ),
             self._executor.submit(message_generator.create_context_type, message),
             self._executor.submit(message_generator.create_initialize_procedure, message),

rflx/generator/message.py

@@ -794,7 +794,6 @@ def fld_first_expr(fld: Field) -> expr.Expr:
 
 def create_valid_context_function(
     message: Message,
-    prefix: str,
 ) -> UnitPart:
     specification = FunctionSpecification(
         "Valid_Context",
@@ -832,7 +831,7 @@ def create_valid_context_function(
             ),
             ExpressionFunctionDeclaration(
                 specification,
-                common.context_predicate(message, prefix),
+                common.context_predicate(message),
                 [Postcondition(TRUE)],
             ),
             Pragma(

tests/feature/messages_with_single_opaque_field/generated/rflx-test-message.ads

@@ -644,8 +644,8 @@ private
       and then ((if
                     Well_Formed (Cursors (F_Data))
                  then
-                    (Cursors (F_Data).Last - Cursors (F_Data).First + 1 = RFLX_Types.Bit_Length (Written_Last - First + 1)
-                     and then Cursors (F_Data).First = First))))
+                    Cursors (F_Data).Last - Cursors (F_Data).First + 1 = Field_Size_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Data)
+                    and then Cursors (F_Data).First = Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Data))))
     with
      Post =>
        True;

tests/feature/parameterized_messages/generated/rflx-test-message.ads

@@ -761,13 +761,13 @@ private
       and then ((if
                     Well_Formed (Cursors (F_Data))
                  then
-                    (Cursors (F_Data).Last - Cursors (F_Data).First + 1 = RFLX_Types.Bit_Length (Length) * 8
-                     and then Cursors (F_Data).First = First))
+                    Cursors (F_Data).Last - Cursors (F_Data).First + 1 = Field_Size_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Length, Extended, F_Data)
+                    and then Cursors (F_Data).First = Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Length, Extended, F_Data))
                 and then (if
                              Well_Formed (Cursors (F_Extension))
                           then
-                             (Cursors (F_Extension).Last - Cursors (F_Extension).First + 1 = RFLX_Types.Bit_Length (Length) * 8
-                              and then Cursors (F_Extension).First = Cursors (F_Data).Last + 1))))
+                             Cursors (F_Extension).Last - Cursors (F_Extension).First + 1 = Field_Size_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Length, Extended, F_Extension)
+                             and then Cursors (F_Extension).First = Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, Length, Extended, F_Extension))))
     with
      Post =>
        True;

tests/feature/session_case_expression_numeric/generated/rflx-test-message.ads

@@ -581,8 +581,8 @@ private
       and then ((if
                     Well_Formed (Cursors (F_Value))
                  then
-                    (Cursors (F_Value).Last - Cursors (F_Value).First + 1 = 8
-                     and then Cursors (F_Value).First = First))))
+                    Cursors (F_Value).Last - Cursors (F_Value).First + 1 = Field_Size_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Value)
+                    and then Cursors (F_Value).First = Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Value))))
     with
      Post =>
        True;

tests/feature/session_endianness/generated/rflx-messages-msg.ads

@@ -621,13 +621,13 @@ private
       and then ((if
                     Well_Formed (Cursors (F_A))
                  then
-                    (Cursors (F_A).Last - Cursors (F_A).First + 1 = 32
-                     and then Cursors (F_A).First = First))
+                    Cursors (F_A).Last - Cursors (F_A).First + 1 = Field_Size_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_A)
+                    and then Cursors (F_A).First = Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_A))
                 and then (if
                              Well_Formed (Cursors (F_B))
                           then
-                             (Cursors (F_B).Last - Cursors (F_B).First + 1 = 32
-                              and then Cursors (F_B).First = Cursors (F_A).Last + 1))))
+                             Cursors (F_B).Last - Cursors (F_B).First + 1 = Field_Size_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_B)
+                             and then Cursors (F_B).First = Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_B))))
     with
      Post =>
        True;

tests/feature/session_endianness/generated/rflx-messages-msg_le.ads

@@ -621,13 +621,13 @@ private
       and then ((if
                     Well_Formed (Cursors (F_C))
                  then
-                    (Cursors (F_C).Last - Cursors (F_C).First + 1 = 32
-                     and then Cursors (F_C).First = First))
+                    Cursors (F_C).Last - Cursors (F_C).First + 1 = Field_Size_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_C)
+                    and then Cursors (F_C).First = Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_C))
                 and then (if
                              Well_Formed (Cursors (F_D))
                           then
-                             (Cursors (F_D).Last - Cursors (F_D).First + 1 = 32
-                              and then Cursors (F_D).First = Cursors (F_C).Last + 1))))
+                             Cursors (F_D).Last - Cursors (F_D).First + 1 = Field_Size_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_D)
+                             and then Cursors (F_D).First = Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_D))))
     with
      Post =>
        True;

tests/feature/session_endianness/generated/rflx-messages-msg_le_nested.ads

@@ -664,18 +664,18 @@ private
       and then ((if
                     Well_Formed (Cursors (F_X_A))
                  then
-                    (Cursors (F_X_A).Last - Cursors (F_X_A).First + 1 = 32
-                     and then Cursors (F_X_A).First = First))
+                    Cursors (F_X_A).Last - Cursors (F_X_A).First + 1 = Field_Size_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_X_A)
+                    and then Cursors (F_X_A).First = Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_X_A))
                 and then (if
                              Well_Formed (Cursors (F_X_B))
                           then
-                             (Cursors (F_X_B).Last - Cursors (F_X_B).First + 1 = 32
-                              and then Cursors (F_X_B).First = Cursors (F_X_A).Last + 1))
+                             Cursors (F_X_B).Last - Cursors (F_X_B).First + 1 = Field_Size_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_X_B)
+                             and then Cursors (F_X_B).First = Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_X_B))
                 and then (if
                              Well_Formed (Cursors (F_Y))
                           then
-                             (Cursors (F_Y).Last - Cursors (F_Y).First + 1 = 32
-                              and then Cursors (F_Y).First = Cursors (F_X_B).Last + 1))))
+                             Cursors (F_Y).Last - Cursors (F_Y).First + 1 = Field_Size_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Y)
+                             and then Cursors (F_Y).First = Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Y))))
     with
      Post =>
        True;

tests/feature/session_functions/generated/rflx-test-definite_message.ads

@@ -773,18 +773,18 @@ private
       and then ((if
                     Well_Formed (Cursors (F_Message_Type))
                  then
-                    (Cursors (F_Message_Type).Last - Cursors (F_Message_Type).First + 1 = 8
-                     and then Cursors (F_Message_Type).First = First))
+                    Cursors (F_Message_Type).Last - Cursors (F_Message_Type).First + 1 = Field_Size_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Message_Type)
+                    and then Cursors (F_Message_Type).First = Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Message_Type))
                 and then (if
                              Well_Formed (Cursors (F_Length))
                           then
-                             (Cursors (F_Length).Last - Cursors (F_Length).First + 1 = 8
-                              and then Cursors (F_Length).First = Cursors (F_Message_Type).Last + 1))
+                             Cursors (F_Length).Last - Cursors (F_Length).First + 1 = Field_Size_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Length)
+                             and then Cursors (F_Length).First = Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Length))
                 and then (if
                              Well_Formed (Cursors (F_Data))
                           then
-                             (Cursors (F_Data).Last - Cursors (F_Data).First + 1 = RFLX_Types.Bit_Length (Cursors (F_Length).Value) * 8
-                              and then Cursors (F_Data).First = Cursors (F_Length).Last + 1))))
+                             Cursors (F_Data).Last - Cursors (F_Data).First + 1 = Field_Size_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Data)
+                             and then Cursors (F_Data).First = Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Data))))
     with
      Post =>
        True;

tests/feature/session_message_optimization/generated/rflx-test-option_data.ads

@@ -712,13 +712,13 @@ private
       and then ((if
                     Well_Formed (Cursors (F_Length))
                  then
-                    (Cursors (F_Length).Last - Cursors (F_Length).First + 1 = 16
-                     and then Cursors (F_Length).First = First))
+                    Cursors (F_Length).Last - Cursors (F_Length).First + 1 = Field_Size_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Length)
+                    and then Cursors (F_Length).First = Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Length))
                 and then (if
                              Well_Formed (Cursors (F_Data))
                           then
-                             (Cursors (F_Data).Last - Cursors (F_Data).First + 1 = RFLX_Types.Bit_Length (Cursors (F_Length).Value) * 8
-                              and then Cursors (F_Data).First = Cursors (F_Length).Last + 1))))
+                             Cursors (F_Data).Last - Cursors (F_Data).First + 1 = Field_Size_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Data)
+                             and then Cursors (F_Data).First = Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Data))))
     with
      Post =>
        True;

tests/feature/session_sequence_append_head/generated/rflx-tlv-message.ads

@@ -740,18 +740,18 @@ private
       and then ((if
                     Well_Formed (Cursors (F_Tag))
                  then
-                    (Cursors (F_Tag).Last - Cursors (F_Tag).First + 1 = 8
-                     and then Cursors (F_Tag).First = First))
+                    Cursors (F_Tag).Last - Cursors (F_Tag).First + 1 = Field_Size_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Tag)
+                    and then Cursors (F_Tag).First = Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Tag))
                 and then (if
                              Well_Formed (Cursors (F_Length))
                           then
-                             (Cursors (F_Length).Last - Cursors (F_Length).First + 1 = 16
-                              and then Cursors (F_Length).First = Cursors (F_Tag).Last + 1))
+                             Cursors (F_Length).Last - Cursors (F_Length).First + 1 = Field_Size_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Length)
+                             and then Cursors (F_Length).First = Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Length))
                 and then (if
                              Well_Formed (Cursors (F_Value))
                           then
-                             (Cursors (F_Value).Last - Cursors (F_Value).First + 1 = RFLX_Types.Bit_Length (Cursors (F_Length).Value) * 8
-                              and then Cursors (F_Value).First = Cursors (F_Length).Last + 1))))
+                             Cursors (F_Value).Last - Cursors (F_Value).First + 1 = Field_Size_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Value)
+                             and then Cursors (F_Value).First = Field_First_Internal (Cursors, First, Verified_Last, Written_Last, Buffer, F_Value))))
     with
      Post =>
        True;