Use S63 type instead of U64 type to store field values

defaults.gpr

@@ -58,7 +58,7 @@ abstract project Defaults is
 
    Proof_Switches :=
    (
-      "--prover=z3,cvc4,altergo",
+      "--prover=z3,cvc4,colibri",
       "--steps=0",
       "--timeout=180",
       "--memlimit=1000",

examples/apps/ping/src/generic_checksum.adb

@@ -20,8 +20,8 @@ is
    is
       use type ICMP.Checksum;
       use type Types.Index;
-      Checksum : ICMP.Checksum := Shift_Left (ICMP.Checksum (ICMP.To_U64 (Tag)))
-                                  + ICMP.Checksum (ICMP.To_U64 (Code));
+      Checksum : ICMP.Checksum := Shift_Left (ICMP.Checksum (ICMP.To_S63 (Tag)))
+                                  + ICMP.Checksum (ICMP.To_S63 (Code));
       Index    : Types.Index;
    begin
       Checksum := Add (Checksum, Add (ICMP.Checksum (Identifier), ICMP.Checksum (Sequence_Number)));

rflx/generator/common.py

@@ -59,7 +59,7 @@ def substitution(
     prefix: str,
     embedded: bool = False,
     public: bool = False,
-    target_type: Optional[ID] = const.TYPES_U64,
+    target_type: Optional[ID] = const.TYPES_S63,
 ) -> Callable[[expr.Expr], expr.Expr]:
     facts = substitution_facts(message, prefix, embedded, public, target_type)
 
@@ -145,7 +145,7 @@ def byte_aggregate(aggregate: expr.Aggregate) -> expr.Aggregate:
                 other = expression.left
             if boolean_literal and other:
                 return expression.__class__(
-                    other, type_conversion(expr.Call("To_U64", [boolean_literal]))
+                    other, type_conversion(expr.Call("To_S63", [boolean_literal]))
                 )
 
         def field_value(field: model.Field) -> expr.Expr:
@@ -187,7 +187,7 @@ def substitution_facts(
     prefix: str,
     embedded: bool = False,
     public: bool = False,
-    target_type: Optional[ID] = const.TYPES_U64,
+    target_type: Optional[ID] = const.TYPES_S63,
 ) -> Mapping[expr.Name, expr.Expr]:
     def prefixed(name: str) -> expr.Expr:
         return expr.Variable(rid.ID("Ctx") * name) if not embedded else expr.Variable(name)
@@ -226,8 +226,8 @@ def field_size(field: model.Field) -> expr.Expr:
     def parameter_value(parameter: model.Field, parameter_type: model.Type) -> expr.Expr:
         if isinstance(parameter_type, model.Enumeration):
             if embedded:
-                return expr.Call("To_U64", [expr.Variable(parameter.name)])
-            return expr.Call("To_U64", [expr.Variable("Ctx" * parameter.identifier)])
+                return expr.Call("To_S63", [expr.Variable(parameter.name)])
+            return expr.Call("To_S63", [expr.Variable("Ctx" * parameter.identifier)])
         if isinstance(parameter_type, model.Scalar):
             if embedded:
                 return expr.Variable(parameter.name)
@@ -238,7 +238,7 @@ def parameter_value(parameter: model.Field, parameter_type: model.Type) -> expr.
     def field_value(field: model.Field, field_type: model.Type) -> expr.Expr:
         if isinstance(field_type, model.Enumeration):
             if public:
-                return expr.Call("To_U64", [expr.Call(f"Get_{field.name}", [expr.Variable("Ctx")])])
+                return expr.Call("To_S63", [expr.Call(f"Get_{field.name}", [expr.Variable("Ctx")])])
             return expr.Selected(
                 expr.Indexed(cursors, expr.Variable(field.affixed_name)),
                 "Value",
@@ -274,14 +274,14 @@ def type_conversion(expression: expr.Expr) -> expr.Expr:
             for f, t in message.field_types.items()
         },
         **{
-            expr.Variable(l): type_conversion(expr.Call("To_U64", [expr.Variable(l)]))
+            expr.Variable(l): type_conversion(expr.Call("To_S63", [expr.Variable(l)]))
             for t in message.types.values()
             if isinstance(t, model.Enumeration) and t != model.BOOLEAN
             for l in t.literals.keys()
         },
         **{
             expr.Variable(t.package * l): type_conversion(
-                expr.Call("To_U64", [expr.Variable(prefix * t.package * l)])
+                expr.Call("To_S63", [expr.Variable(prefix * t.package * l)])
             )
             for t in message.types.values()
             if isinstance(t, model.Enumeration) and t != model.BOOLEAN
@@ -930,7 +930,7 @@ def create_sequence_instantiation(
                 str(element_type.size),
                 prefix * element_type_package * f"Valid_{element_type.name}",
                 prefix * element_type_package * "To_Actual",
-                prefix * element_type_package * "To_U64",
+                prefix * element_type_package * "To_S63",
             ],
         )
     else:

rflx/generator/const.py

@@ -49,6 +49,7 @@
 TYPES_TO_LAST_BIT_INDEX = TYPES * "To_Last_Bit_Index"
 TYPES_OFFSET = TYPES * "Offset"
 TYPES_U64 = TYPES * "U64"
+TYPES_S63 = TYPES * "S63"
 TYPES_BYTE_ORDER = TYPES * "Byte_Order"
 TYPES_HIGH_ORDER_FIRST = TYPES * "High_Order_First"
 TYPES_LOW_ORDER_FIRST = TYPES * "Low_Order_First"

rflx/generator/generator.py

@@ -663,11 +663,10 @@ def __integer_functions(self, integer: Integer) -> UnitPart:
                 ]
             )
         else:
-            specification.append(UseTypeClause(self.__prefix * const.TYPES_U64))
+            specification.append(UseTypeClause(self.__prefix * const.TYPES_S63))
+
+        specification += self.__type_validation_functions(integer.name, "Val", constraints.ada_expr())
 
-        specification.append(
-            self.__type_validation_function(integer.name, "Val", constraints.ada_expr())
-        )
 
         if constraints == expr.TRUE:
             specification.extend(
@@ -702,15 +701,13 @@ def __enumeration_functions(self, enum: Enumeration) -> UnitPart:
         )
 
         if validation_expression != TRUE:
-            specification.append(UseTypeClause(self.__prefix * const.TYPES_U64))
+            specification.append(UseTypeClause(self.__prefix * const.TYPES_S63))
 
-        specification.append(
-            self.__type_validation_function(
+        specification += self.__type_validation_functions(
                 enum.name,
                 "Val" if validation_expression != TRUE else "Unused_Val",
                 validation_expression,
             )
-        )
 
         if enum.always_valid:
             specification.append(
@@ -736,8 +733,8 @@ def __enumeration_functions(self, enum: Enumeration) -> UnitPart:
         specification.append(
             ExpressionFunctionDeclaration(
                 FunctionSpecification(
-                    "To_U64",
-                    self.__prefix * const.TYPES_U64,
+                    "To_S63",
+                    self.__prefix * const.TYPES_S63,
                     [
                         Parameter(
                             ["Enum"],
@@ -760,7 +757,7 @@ def __enumeration_functions(self, enum: Enumeration) -> UnitPart:
         conversion_function = FunctionSpecification(
             "To_Actual",
             self.__prefix * ID(enum.identifier),
-            [Parameter(["Val"], self.__prefix * const.TYPES_U64)],
+            [Parameter(["Val"], self.__prefix * const.TYPES_S63)],
         )
         precondition = Precondition(Call(f"Valid_{enum.name}", [Variable("Val")]))
         conversion_cases: ty.List[ty.Tuple[Expr, Expr]] = []
@@ -794,17 +791,16 @@ def __enumeration_functions(self, enum: Enumeration) -> UnitPart:
             specification.append(
                 ExpressionFunctionDeclaration(
                     FunctionSpecification(
-                        "To_U64",
-                        self.__prefix * const.TYPES_U64,
+                        "To_S63",
+                        self.__prefix * const.TYPES_S63,
                         [Parameter(["Val"], self.__prefix * ID(enum.identifier))],
                     ),
                     If(
-                        [(Variable("Val.Known"), Call("To_U64", [Variable("Val.Enum")]))],
+                        [(Variable("Val.Known"), Call("To_S63", [Variable("Val.Enum")]))],
                         Variable("Val.Raw"),
                     ),
                 )
             )
-
         else:
             conversion_cases.extend(
                 [
@@ -1233,33 +1229,35 @@ def __license_header(self) -> str:
             )
         )
 
-    def __type_validation_function(
+    def __type_validation_functions(
         self, type_name: str, enum_value: str, validation_expression: Expr
-    ) -> Subprogram:
-        return ExpressionFunctionDeclaration(
-            FunctionSpecification(
-                f"Valid_{type_name}",
-                "Boolean",
-                [Parameter([enum_value], self.__prefix * const.TYPES_U64)],
+    ) -> Sequence[Subprogram]:
+        return [
+            ExpressionFunctionDeclaration(
+                FunctionSpecification(
+                    f"Valid_{type_name}",
+                    "Boolean",
+                    [Parameter([enum_value], self.__prefix * const.TYPES_S63)],
+                ),
+                validation_expression,
             ),
-            validation_expression,
-        )
+        ]
 
     def __integer_conversion_functions(self, integer: Integer) -> ty.Sequence[Subprogram]:
         return [
             ExpressionFunctionDeclaration(
                 FunctionSpecification(
-                    "To_U64",
-                    self.__prefix * const.TYPES_U64,
+                    "To_S63",
+                    self.__prefix * const.TYPES_S63,
                     [Parameter(["Val"], self.__prefix * ID(integer.identifier))],
                 ),
-                Call(self.__prefix * const.TYPES_U64, [Variable("Val")]),
+                Call(self.__prefix * const.TYPES_S63, [Variable("Val")]),
             ),
             ExpressionFunctionDeclaration(
                 FunctionSpecification(
                     "To_Actual",
                     self.__prefix * ID(integer.identifier),
-                    [Parameter(["Val"], self.__prefix * const.TYPES_U64)],
+                    [Parameter(["Val"], self.__prefix * const.TYPES_S63)],
                 ),
                 Call(self.__prefix * ID(integer.identifier), [Variable("Val")]),
                 [Precondition(Call(f"Valid_{integer.name}", [Variable("Val")]))],
@@ -1371,7 +1369,7 @@ def enumeration_types(enum: Enumeration) -> ty.List[Declaration]:
                     "Known",
                     [
                         Variant([TRUE], [Component("Enum", common.enum_name(enum))]),
-                        Variant([FALSE], [Component("Raw", const.TYPES_U64)]),
+                        Variant([FALSE], [Component("Raw", const.TYPES_S63)]),
                     ],
                 ),
             )

rflx/generator/message.py

@@ -111,13 +111,13 @@ def create_use_type_clause(composite_fields: ty.Sequence[Field], offset: bool) -
         [
             Pragma(
                 "Warnings",
-                [Variable("Off"), String('use clause for type "U64" * has no effect')],
+                [Variable("Off"), String('use clause for type "S63" * has no effect')],
             ),
             Pragma(
                 "Warnings",
                 [
                     Variable("Off"),
-                    String('"U64" is already use-visible through previous use_type_clause'),
+                    String('"S63" is already use-visible through previous use_type_clause'),
                 ],
             ),
             Pragma(
@@ -135,7 +135,7 @@ def create_use_type_clause(composite_fields: ty.Sequence[Field], offset: bool) -
                     const.TYPES_LENGTH,
                     const.TYPES_INDEX,
                     const.TYPES_BIT_INDEX,
-                    const.TYPES_U64,
+                    const.TYPES_S63,
                     *([const.TYPES_OFFSET] if offset else []),
                 ]
             ],
@@ -150,12 +150,12 @@ def create_use_type_clause(composite_fields: ty.Sequence[Field], offset: bool) -
                 "Warnings",
                 [
                     Variable("On"),
-                    String('"U64" is already use-visible through previous use_type_clause'),
+                    String('"S63" is already use-visible through previous use_type_clause'),
                 ],
             ),
             Pragma(
                 "Warnings",
-                [Variable("On"), String('use clause for type "U64" * has no effect')],
+                [Variable("On"), String('use clause for type "S63" * has no effect')],
             ),
         ]
     )
@@ -234,7 +234,7 @@ def create_cursor_type() -> UnitPart:
                                 ),
                                 Component(
                                     "Value",
-                                    const.TYPES_U64,
+                                    const.TYPES_S63,
                                     Number(0),
                                 ),
                             ],
@@ -1296,7 +1296,7 @@ def create_valid_value_function(
         "Boolean",
         [
             Parameter(["Fld" if scalar_fields else "Unused_Fld"], "Field"),
-            Parameter(["Val" if scalar_fields else "Unused_Val"], const.TYPES_U64),
+            Parameter(["Val" if scalar_fields else "Unused_Val"], const.TYPES_S63),
         ],
     )
 
@@ -1516,7 +1516,7 @@ def create_field_first_function(message: Message, prefix: str) -> UnitPart:
 
     def first(link: Link, message: Message) -> tuple[Expr, Expr]:
         def substituted(
-            expression: expr.Expr, target_type: ty.Optional[ID] = const.TYPES_U64
+            expression: expr.Expr, target_type: ty.Optional[ID] = const.TYPES_S63
         ) -> Expr:
             return (
                 expression.substituted(
@@ -1678,9 +1678,9 @@ def condition(field: Field, message: Message) -> Expr:
         c: expr.Expr = expr.Or(*[l.condition for l in message.outgoing(field)])
         c = c.substituted(
             mapping={
-                expr.Size(field.name): expr.Call(const.TYPES_U64, [expr.Variable("Size")]),
+                expr.Size(field.name): expr.Call(const.TYPES_S63, [expr.Variable("Size")]),
                 expr.Last(field.name): expr.Call(
-                    const.TYPES_U64,
+                    const.TYPES_S63,
                     [
                         expr.Call(
                             "Field_Last",
@@ -1711,7 +1711,7 @@ def condition(field: Field, message: Message) -> Expr:
         Parameter(["Ctx"], "Context"),
         Parameter(["Fld"], "Field"),
         *(
-            [Parameter(["Val"], const.TYPES_U64)]
+            [Parameter(["Val"], const.TYPES_S63)]
             if common.has_value_dependent_condition(message)
             else []
         ),
@@ -3043,7 +3043,7 @@ def _create_valid_structure_function(message: Message, prefix: str) -> UnitPart:
             )
             .substituted(
                 lambda x: expr.Call(
-                    "To_U64",
+                    "To_S63",
                     [expr.Variable("Struct" * x.identifier)],
                 )
                 if isinstance(x, expr.Variable)

rflx/generator/parser.py

@@ -96,7 +96,7 @@ def create_get_function(
                 SubprogramBody(
                     FunctionSpecification(
                         "Get",
-                        const.TYPES_U64,
+                        const.TYPES_S63,
                         [Parameter(["Ctx"], "Context"), Parameter(["Fld"], "Field")],
                     ),
                     [
@@ -371,7 +371,7 @@ def create_verify_procedure(
             [
                 SubprogramBody(
                     specification,
-                    [ObjectDeclaration(["Value"], const.TYPES_U64)],
+                    [ObjectDeclaration(["Value"], const.TYPES_S63)],
                     [
                         IfStatement(
                             [