Remove invalid successors invariant from context predicate

Ref. eng/recordflux/RecordFlux#1802
AdaCore · Oct 29, 2024 · 4981cd5 · 4981cd5
1 parent 5c66746
commit 4981cd5
Show file tree

Hide file tree

Showing 32 changed files with 2 additions and 142 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -27,6 +27,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ### Changed
 
 - Remove unused `Buffer` arguments in generated code (eng/recordflux/RecordFlux#1802)
+- Remove unnecessary part of `Valid_Context` predicate (eng/recordflux/RecordFlux#1802)
 
 ## [0.24.0] - 2024-09-12
 

diff --git a/examples/apps/spdm_responder/build_lib.gpr b/examples/apps/spdm_responder/build_lib.gpr
@@ -107,7 +107,7 @@ project Build_Lib is
    package Prove is
       for Proof_Switches ("Ada") use Defaults.Proof_Switches;
       for Proof_Switches ("responder.adb") use ("--prover=z3,cvc5", "--steps=64000", "--memlimit=6000", "--timeout=600");
-      for Proof_Switches ("rflx-spdm_responder-session-fsm.adb") use ("--timeout=240");
+      for Proof_Switches ("rflx-spdm_responder-session-fsm.adb") use ("--timeout=240", "--memlimit=3000");
    end Prove;
 
 end Build_Lib;
diff --git a/rflx/generator/common.py b/rflx/generator/common.py
@@ -486,39 +486,6 @@ def context_predicate(
     message: model.Message,
     prefix: str,
 ) -> Expr:
-    def invalid_successors_invariant() -> Expr:
-        """
-        Create the invariant that defines the state of successors of invalid fields.
-
-        This invariant ensures for all invalid message fields that all its successor fields are also
-        invalid.
-        """
-        return AndThen(
-            *[
-                IfThenElse(
-                    AndThen(
-                        *[
-                            Call(
-                                "Invalid",
-                                [Indexed(Variable("Cursors"), Variable(p.affixed_name))],
-                            )
-                            for p in message.direct_predecessors(f)
-                        ],
-                    ),
-                    Call(
-                        "Invalid",
-                        [
-                            Indexed(
-                                Variable("Cursors"),
-                                Variable(f.affixed_name),
-                            ),
-                        ],
-                    ),
-                )
-                for f in message.fields
-                if f not in message.direct_successors(model.INITIAL)
-            ],
-        )
 
     return AndThen(
         IfThenElse(
@@ -553,7 +520,6 @@ def invalid_successors_invariant() -> Expr:
                 *[Variable(p.identifier) for p in message.parameter_types],
             ],
         ),
-        invalid_successors_invariant(),
         message_structure_invariant(message, prefix, embedded=True),
     )
 

diff --git a/tests/feature/fsm_case_expression_numeric/generated/rflx-test-message.ads b/tests/feature/fsm_case_expression_numeric/generated/rflx-test-message.ads
@@ -601,7 +601,6 @@ private
       and then Written_Last rem RFLX_Types.Byte'Size = 0
       and then Cursors_Invariant (Cursors, First, Verified_Last)
       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last)
-      and then (True)
       and then ((if
                     Well_Formed (Cursors (F_Value))
                  then

diff --git a/tests/feature/fsm_endianness/generated/rflx-messages-msg.ads b/tests/feature/fsm_endianness/generated/rflx-messages-msg.ads
@@ -649,7 +649,6 @@ private
       and then Written_Last rem RFLX_Types.Byte'Size = 0
       and then Cursors_Invariant (Cursors, First, Verified_Last)
       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last)
-      and then ((if Invalid (Cursors (F_A)) then Invalid (Cursors (F_B))))
       and then ((if
                     Well_Formed (Cursors (F_A))
                  then

diff --git a/tests/feature/fsm_endianness/generated/rflx-messages-msg_le.ads b/tests/feature/fsm_endianness/generated/rflx-messages-msg_le.ads
@@ -649,7 +649,6 @@ private
       and then Written_Last rem RFLX_Types.Byte'Size = 0
       and then Cursors_Invariant (Cursors, First, Verified_Last)
       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last)
-      and then ((if Invalid (Cursors (F_C)) then Invalid (Cursors (F_D))))
       and then ((if
                     Well_Formed (Cursors (F_C))
                  then

diff --git a/tests/feature/fsm_endianness/generated/rflx-messages-msg_le_nested.ads b/tests/feature/fsm_endianness/generated/rflx-messages-msg_le_nested.ads
@@ -699,8 +699,6 @@ private
       and then Written_Last rem RFLX_Types.Byte'Size = 0
       and then Cursors_Invariant (Cursors, First, Verified_Last)
       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last)
-      and then ((if Invalid (Cursors (F_X_A)) then Invalid (Cursors (F_X_B)))
-                and then (if Invalid (Cursors (F_X_B)) then Invalid (Cursors (F_Y))))
       and then ((if
                     Well_Formed (Cursors (F_X_A))
                  then

diff --git a/tests/feature/fsm_functions/generated/rflx-test-definite_message.ads b/tests/feature/fsm_functions/generated/rflx-test-definite_message.ads
@@ -808,8 +808,6 @@ private
       and then Written_Last rem RFLX_Types.Byte'Size = 0
       and then Cursors_Invariant (Cursors, First, Verified_Last)
       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last)
-      and then ((if Invalid (Cursors (F_Message_Type)) then Invalid (Cursors (F_Length)))
-                and then (if Invalid (Cursors (F_Length)) then Invalid (Cursors (F_Data))))
       and then ((if
                     Well_Formed (Cursors (F_Message_Type))
                  then

diff --git a/tests/feature/fsm_message_optimization/generated/rflx-test-option_data.ads b/tests/feature/fsm_message_optimization/generated/rflx-test-option_data.ads
@@ -740,7 +740,6 @@ private
       and then Written_Last rem RFLX_Types.Byte'Size = 0
       and then Cursors_Invariant (Cursors, First, Verified_Last)
       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last)
-      and then ((if Invalid (Cursors (F_Length)) then Invalid (Cursors (F_Data))))
       and then ((if
                     Well_Formed (Cursors (F_Length))
                  then

diff --git a/tests/feature/fsm_sequence_append_head/generated/rflx-tlv-message.ads b/tests/feature/fsm_sequence_append_head/generated/rflx-tlv-message.ads
@@ -775,8 +775,6 @@ private
       and then Written_Last rem RFLX_Types.Byte'Size = 0
       and then Cursors_Invariant (Cursors, First, Verified_Last)
       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last)
-      and then ((if Invalid (Cursors (F_Tag)) then Invalid (Cursors (F_Length)))
-                and then (if Invalid (Cursors (F_Length)) then Invalid (Cursors (F_Value))))
       and then ((if
                     Well_Formed (Cursors (F_Tag))
                  then

diff --git a/tests/feature/fsm_setting_of_message_fields/generated/rflx-test-message.ads b/tests/feature/fsm_setting_of_message_fields/generated/rflx-test-message.ads
@@ -798,8 +798,6 @@ private
       and then Written_Last rem RFLX_Types.Byte'Size = 0
       and then Cursors_Invariant (Cursors, First, Verified_Last)
       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
-      and then ((if Invalid (Cursors (F_Has_Data)) then Invalid (Cursors (F_Length)))
-                and then (if Invalid (Cursors (F_Length)) then Invalid (Cursors (F_Data))))
       and then ((if
                     Well_Formed (Cursors (F_Has_Data))
                  then

diff --git a/tests/feature/message_with_variable_as_condition_on_same_field/generated/rflx-test-m.ads b/tests/feature/message_with_variable_as_condition_on_same_field/generated/rflx-test-m.ads
@@ -654,7 +654,6 @@ private
       and then Written_Last rem RFLX_Types.Byte'Size = 0
       and then Cursors_Invariant (Cursors, First, Verified_Last)
       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last)
-      and then ((if Invalid (Cursors (F_A)) then Invalid (Cursors (F_B))))
       and then ((if
                     Well_Formed (Cursors (F_A))
                  then

diff --git a/.../feature/message_with_variable_as_condition_on_subsequent_field/generated/rflx-test-m.ads b/.../feature/message_with_variable_as_condition_on_subsequent_field/generated/rflx-test-m.ads
@@ -653,7 +653,6 @@ private
       and then Written_Last rem RFLX_Types.Byte'Size = 0
       and then Cursors_Invariant (Cursors, First, Verified_Last)
       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last)
-      and then ((if Invalid (Cursors (F_A)) then Invalid (Cursors (F_B))))
       and then ((if
                     Well_Formed (Cursors (F_A))
                  then

diff --git a/tests/feature/messages_with_multiple_initial_links/generated/rflx-test-m.ads b/tests/feature/messages_with_multiple_initial_links/generated/rflx-test-m.ads
@@ -633,7 +633,6 @@ private
       and then Written_Last rem RFLX_Types.Byte'Size = 0
       and then Cursors_Invariant (Cursors, First, Verified_Last)
       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, P)
-      and then (True)
       and then ((if
                     Well_Formed (Cursors (F_F1))
                  then

diff --git a/tests/feature/messages_with_single_opaque_field/generated/rflx-test-message.ads b/tests/feature/messages_with_single_opaque_field/generated/rflx-test-message.ads
@@ -664,7 +664,6 @@ private
       and then Written_Last rem RFLX_Types.Byte'Size = 0
       and then Cursors_Invariant (Cursors, First, Verified_Last)
       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last)
-      and then (True)
       and then ((if
                     Well_Formed (Cursors (F_Data))
                  then

diff --git a/tests/feature/parameterized_messages/generated/rflx-test-message.ads b/tests/feature/parameterized_messages/generated/rflx-test-message.ads
@@ -773,7 +773,6 @@ private
       and then Written_Last rem RFLX_Types.Byte'Size = 0
       and then Cursors_Invariant (Cursors, First, Verified_Last)
       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Length, Extended)
-      and then ((if Invalid (Cursors (F_Data)) then Invalid (Cursors (F_Extension))))
       and then ((if
                     Well_Formed (Cursors (F_Data))
                  then

diff --git a/tests/feature/shared/generated/rflx-universal-message.ads b/tests/feature/shared/generated/rflx-universal-message.ads
@@ -1440,20 +1440,6 @@ private
       and then Written_Last rem RFLX_Types.Byte'Size = 0
       and then Cursors_Invariant (Cursors, First, Verified_Last)
       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last)
-      and then ((if Invalid (Cursors (F_Message_Type)) then Invalid (Cursors (F_Length)))
-                and then (if
-                             Invalid (Cursors (F_Length))
-                             and then Invalid (Cursors (F_Message_Type))
-                          then
-                             Invalid (Cursors (F_Data)))
-                and then (if Invalid (Cursors (F_Length)) then Invalid (Cursors (F_Option_Types)))
-                and then (if
-                             Invalid (Cursors (F_Length))
-                             and then Invalid (Cursors (F_Message_Type))
-                          then
-                             Invalid (Cursors (F_Options)))
-                and then (if Invalid (Cursors (F_Length)) then Invalid (Cursors (F_Value)))
-                and then (if Invalid (Cursors (F_Length)) then Invalid (Cursors (F_Values))))
       and then ((if
                     Well_Formed (Cursors (F_Message_Type))
                  then

diff --git a/tests/feature/shared/generated/rflx-universal-option.ads b/tests/feature/shared/generated/rflx-universal-option.ads
@@ -775,8 +775,6 @@ private
       and then Written_Last rem RFLX_Types.Byte'Size = 0
       and then Cursors_Invariant (Cursors, First, Verified_Last)
       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last)
-      and then ((if Invalid (Cursors (F_Option_Type)) then Invalid (Cursors (F_Length)))
-                and then (if Invalid (Cursors (F_Length)) then Invalid (Cursors (F_Data))))
       and then ((if
                     Well_Formed (Cursors (F_Option_Type))
                  then

diff --git a/tests/spark/generated/rflx-derivation-message.ads b/tests/spark/generated/rflx-derivation-message.ads
@@ -777,8 +777,6 @@ private
       and then Written_Last rem RFLX_Types.Byte'Size = 0
       and then Cursors_Invariant (Cursors, First, Verified_Last)
       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last)
-      and then ((if Invalid (Cursors (F_Tag)) then Invalid (Cursors (F_Length)))
-                and then (if Invalid (Cursors (F_Length)) then Invalid (Cursors (F_Value))))
       and then ((if
                     Well_Formed (Cursors (F_Tag))
                  then

diff --git a/tests/spark/generated/rflx-enumeration-message.ads b/tests/spark/generated/rflx-enumeration-message.ads
@@ -601,7 +601,6 @@ private
       and then Written_Last rem RFLX_Types.Byte'Size = 0
       and then Cursors_Invariant (Cursors, First, Verified_Last)
       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last)
-      and then (True)
       and then ((if
                     Well_Formed (Cursors (F_Priority))
                  then

diff --git a/tests/spark/generated/rflx-ethernet-frame.ads b/tests/spark/generated/rflx-ethernet-frame.ads
@@ -989,16 +989,6 @@ private
       and then Written_Last rem RFLX_Types.Byte'Size = 0
       and then Cursors_Invariant (Cursors, First, Verified_Last)
       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last)
-      and then ((if Invalid (Cursors (F_Destination)) then Invalid (Cursors (F_Source)))
-                and then (if Invalid (Cursors (F_Source)) then Invalid (Cursors (F_Type_Length_TPID)))
-                and then (if Invalid (Cursors (F_Type_Length_TPID)) then Invalid (Cursors (F_TPID)))
-                and then (if Invalid (Cursors (F_TPID)) then Invalid (Cursors (F_TCI)))
-                and then (if
-                             Invalid (Cursors (F_TCI))
-                             and then Invalid (Cursors (F_Type_Length_TPID))
-                          then
-                             Invalid (Cursors (F_Type_Length)))
-                and then (if Invalid (Cursors (F_Type_Length)) then Invalid (Cursors (F_Payload))))
       and then ((if
                     Well_Formed (Cursors (F_Destination))
                  then

diff --git a/tests/spark/generated/rflx-expression-message.ads b/tests/spark/generated/rflx-expression-message.ads
@@ -673,7 +673,6 @@ private
       and then Written_Last rem RFLX_Types.Byte'Size = 0
       and then Cursors_Invariant (Cursors, First, Verified_Last)
       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last, Buffer)
-      and then (True)
       and then ((if
                     Well_Formed (Cursors (F_Payload))
                  then

diff --git a/tests/spark/generated/rflx-fixed_size-simple_message.ads b/tests/spark/generated/rflx-fixed_size-simple_message.ads
@@ -743,7 +743,6 @@ private
       and then Written_Last rem RFLX_Types.Byte'Size = 0
       and then Cursors_Invariant (Cursors, First, Verified_Last)
       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last)
-      and then ((if Invalid (Cursors (F_Message_Type)) then Invalid (Cursors (F_Data))))
       and then ((if
                     Well_Formed (Cursors (F_Message_Type))
                  then

diff --git a/tests/spark/generated/rflx-icmp-message.ads b/tests/spark/generated/rflx-icmp-message.ads
@@ -1637,33 +1637,6 @@ private
       and then Written_Last rem RFLX_Types.Byte'Size = 0
       and then Cursors_Invariant (Cursors, First, Verified_Last)
       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last)
-      and then ((if Invalid (Cursors (F_Tag)) then Invalid (Cursors (F_Code_Destination_Unreachable)))
-                and then (if Invalid (Cursors (F_Tag)) then Invalid (Cursors (F_Code_Redirect)))
-                and then (if Invalid (Cursors (F_Tag)) then Invalid (Cursors (F_Code_Time_Exceeded)))
-                and then (if Invalid (Cursors (F_Tag)) then Invalid (Cursors (F_Code_Zero)))
-                and then (if
-                             Invalid (Cursors (F_Code_Destination_Unreachable))
-                             and then Invalid (Cursors (F_Code_Redirect))
-                             and then Invalid (Cursors (F_Code_Time_Exceeded))
-                             and then Invalid (Cursors (F_Code_Zero))
-                          then
-                             Invalid (Cursors (F_Checksum)))
-                and then (if Invalid (Cursors (F_Checksum)) then Invalid (Cursors (F_Gateway_Internet_Address)))
-                and then (if Invalid (Cursors (F_Checksum)) then Invalid (Cursors (F_Identifier)))
-                and then (if Invalid (Cursors (F_Checksum)) then Invalid (Cursors (F_Pointer)))
-                and then (if Invalid (Cursors (F_Checksum)) then Invalid (Cursors (F_Unused_32)))
-                and then (if Invalid (Cursors (F_Identifier)) then Invalid (Cursors (F_Sequence_Number)))
-                and then (if Invalid (Cursors (F_Pointer)) then Invalid (Cursors (F_Unused_24)))
-                and then (if Invalid (Cursors (F_Sequence_Number)) then Invalid (Cursors (F_Originate_Timestamp)))
-                and then (if
-                             Invalid (Cursors (F_Gateway_Internet_Address))
-                             and then Invalid (Cursors (F_Sequence_Number))
-                             and then Invalid (Cursors (F_Unused_24))
-                             and then Invalid (Cursors (F_Unused_32))
-                          then
-                             Invalid (Cursors (F_Data)))
-                and then (if Invalid (Cursors (F_Originate_Timestamp)) then Invalid (Cursors (F_Receive_Timestamp)))
-                and then (if Invalid (Cursors (F_Receive_Timestamp)) then Invalid (Cursors (F_Transmit_Timestamp))))
       and then ((if
                     Well_Formed (Cursors (F_Tag))
                  then

diff --git a/tests/spark/generated/rflx-ipv4-option.ads b/tests/spark/generated/rflx-ipv4-option.ads
@@ -920,10 +920,6 @@ private
       and then Written_Last rem RFLX_Types.Byte'Size = 0
       and then Cursors_Invariant (Cursors, First, Verified_Last)
       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last)
-      and then ((if Invalid (Cursors (F_Copied)) then Invalid (Cursors (F_Option_Class)))
-                and then (if Invalid (Cursors (F_Option_Class)) then Invalid (Cursors (F_Option_Number)))
-                and then (if Invalid (Cursors (F_Option_Number)) then Invalid (Cursors (F_Option_Length)))
-                and then (if Invalid (Cursors (F_Option_Length)) then Invalid (Cursors (F_Option_Data))))
       and then ((if
                     Well_Formed (Cursors (F_Copied))
                  then

diff --git a/tests/spark/generated/rflx-ipv4-packet.ads b/tests/spark/generated/rflx-ipv4-packet.ads
@@ -1803,22 +1803,6 @@ private
       and then Written_Last rem RFLX_Types.Byte'Size = 0
       and then Cursors_Invariant (Cursors, First, Verified_Last)
       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last)
-      and then ((if Invalid (Cursors (F_Version)) then Invalid (Cursors (F_IHL)))
-                and then (if Invalid (Cursors (F_IHL)) then Invalid (Cursors (F_DSCP)))
-                and then (if Invalid (Cursors (F_DSCP)) then Invalid (Cursors (F_ECN)))
-                and then (if Invalid (Cursors (F_ECN)) then Invalid (Cursors (F_Total_Length)))
-                and then (if Invalid (Cursors (F_Total_Length)) then Invalid (Cursors (F_Identification)))
-                and then (if Invalid (Cursors (F_Identification)) then Invalid (Cursors (F_Flag_R)))
-                and then (if Invalid (Cursors (F_Flag_R)) then Invalid (Cursors (F_Flag_DF)))
-                and then (if Invalid (Cursors (F_Flag_DF)) then Invalid (Cursors (F_Flag_MF)))
-                and then (if Invalid (Cursors (F_Flag_MF)) then Invalid (Cursors (F_Fragment_Offset)))
-                and then (if Invalid (Cursors (F_Fragment_Offset)) then Invalid (Cursors (F_TTL)))
-                and then (if Invalid (Cursors (F_TTL)) then Invalid (Cursors (F_Protocol)))
-                and then (if Invalid (Cursors (F_Protocol)) then Invalid (Cursors (F_Header_Checksum)))
-                and then (if Invalid (Cursors (F_Header_Checksum)) then Invalid (Cursors (F_Source)))
-                and then (if Invalid (Cursors (F_Source)) then Invalid (Cursors (F_Destination)))
-                and then (if Invalid (Cursors (F_Destination)) then Invalid (Cursors (F_Options)))
-                and then (if Invalid (Cursors (F_Options)) then Invalid (Cursors (F_Payload))))
       and then ((if
                     Well_Formed (Cursors (F_Version))
                  then

diff --git a/tests/spark/generated/rflx-sequence-inner_message.ads b/tests/spark/generated/rflx-sequence-inner_message.ads
@@ -753,7 +753,6 @@ private
       and then Written_Last rem RFLX_Types.Byte'Size = 0
       and then Cursors_Invariant (Cursors, First, Verified_Last)
       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last)
-      and then ((if Invalid (Cursors (F_Length)) then Invalid (Cursors (F_Payload))))
       and then ((if
                     Well_Formed (Cursors (F_Length))
                  then

diff --git a/tests/spark/generated/rflx-sequence-message.ads b/tests/spark/generated/rflx-sequence-message.ads
@@ -1014,9 +1014,6 @@ private
       and then Written_Last rem RFLX_Types.Byte'Size = 0
       and then Cursors_Invariant (Cursors, First, Verified_Last)
       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last)
-      and then ((if Invalid (Cursors (F_Length)) then Invalid (Cursors (F_Integer_Vector)))
-                and then (if Invalid (Cursors (F_Integer_Vector)) then Invalid (Cursors (F_Enumeration_Vector)))
-                and then (if Invalid (Cursors (F_Enumeration_Vector)) then Invalid (Cursors (F_AV_Enumeration_Vector))))
       and then ((if
                     Well_Formed (Cursors (F_Length))
                  then

diff --git a/tests/spark/generated/rflx-sequence-messages_message.ads b/tests/spark/generated/rflx-sequence-messages_message.ads
@@ -738,7 +738,6 @@ private
       and then Written_Last rem RFLX_Types.Byte'Size = 0
       and then Cursors_Invariant (Cursors, First, Verified_Last)
       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last)
-      and then ((if Invalid (Cursors (F_Length)) then Invalid (Cursors (F_Messages))))
       and then ((if
                     Well_Formed (Cursors (F_Length))
                  then

diff --git a/tests/spark/generated/rflx-sequence-sequence_size_defined_by_message_size.ads b/tests/spark/generated/rflx-sequence-sequence_size_defined_by_message_size.ads
@@ -740,7 +740,6 @@ private
       and then Written_Last rem RFLX_Types.Byte'Size = 0
       and then Cursors_Invariant (Cursors, First, Verified_Last)
       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last)
-      and then ((if Invalid (Cursors (F_Header)) then Invalid (Cursors (F_Vector))))
       and then ((if
                     Well_Formed (Cursors (F_Header))
                  then

diff --git a/tests/spark/generated/rflx-tlv-message.ads b/tests/spark/generated/rflx-tlv-message.ads
@@ -775,8 +775,6 @@ private
       and then Written_Last rem RFLX_Types.Byte'Size = 0
       and then Cursors_Invariant (Cursors, First, Verified_Last)
       and then Valid_Predecessors_Invariant (Cursors, First, Verified_Last, Written_Last)
-      and then ((if Invalid (Cursors (F_Tag)) then Invalid (Cursors (F_Length)))
-                and then (if Invalid (Cursors (F_Length)) then Invalid (Cursors (F_Value))))
       and then ((if
                     Well_Formed (Cursors (F_Tag))
                  then