Transparent integers #1238

karthikbhargavan · 2025-01-17T16:32:31Z

This PR modifies the F* model of machine integers so that they are transparent to the normalizer and hence more amenable to tactic based proofs.

The current model of machine integers in proof-libs/fstar/rust_primitives/Rust_primitives.Integers.fsti is based on HACL* integers (Lib.IntTypes.int_t), which in turn is based on F* integers (FStar.UInt*.t). This has several advantages:

the possibility of proving secret independence, using secret integers
compatibility with HACL* specifications for crypto primitives
the ability to use classic F* integer constants.

Conversely, for verification this model has some deficiencies:

integers are constructed using an opaque function int_to_t
extracting the underlying integer requires the application of a ghost function v
Consequently, any proofs that rely on mathematical properties of integers cannot use "normalization" and instead must rely on the careful application of lemmas that reveal that int_to_t and v are inverses of each other. It also makes it particularly hard to define tactics that can verify mathematical algorithms like ML-KEM and ML-DSA.

In the current PR, we cut the link the HACL* integers, and to F* integers, and instead locally define all machine integers as wrappers around mathematical integers. This allows us to be transparent about the implementation of integers, significantly simplifying their semantics. We expect that this will significanly help with writing new tactics and automation for proofs, and will speed up existing proofs.

This PR is the first round of changes and aims to be non-disruptive.
A future PR will link the definition of these integers also to their bitvector representations.

(We need to test this PR for libcrux and other projects. This comment will be removed or amended when these tests are done.)

karthikbhargavan · 2025-01-17T16:34:55Z

Libcrux passes lax checking with some edits.

cryspen/libcrux#756

W95Psp

The code looks good, I only have a few nits.

I still need to look at:

libcrux tcing
the serialize tactic

W95Psp · 2025-01-20T07:45:29Z

proof-libs/fstar/rust_primitives/Rust_primitives.Integers.fsti

+type u32 = int_t U32
+type i32 = int_t I32
+type u64 = int_t U64
+type i64=  int_t I64


Suggested change

type i64= int_t I64

type i64 = int_t I64

W95Psp · 2025-01-20T07:47:19Z

proof-libs/fstar/rust_primitives/Rust_primitives.Integers.fsti

+let from_uint8 (x:FStar.UInt8.t) : u8  = mk_int (FStar.UInt8.v x)
+let from_int8 (x:FStar.Int8.t) : i8  = mk_int (FStar.Int8.v x)
+let from_uint16 (x:FStar.UInt16.t) : u16  = mk_int (FStar.UInt16.v x)
+let from_int16 (x:FStar.Int16.t) : i16  = mk_int (FStar.Int16.v x)
+let from_uint32 (x:FStar.UInt32.t) : u32  = mk_int (FStar.UInt32.v x)
+let from_int32 (x:FStar.Int32.t) : i32  = mk_int (FStar.Int32.v x)
+let from_uint64 (x:FStar.UInt64.t) : u64  = mk_int (FStar.UInt64.v x)
+let from_int64 (x:FStar.Int64.t) : i64  = mk_int (FStar.Int64.v x)
+let from_uint128 (x:FStar.UInt128.t) : u128  = mk_int (FStar.UInt128.v x)
+let from_int128 (x:FStar.Int128.t) : i128  = mk_int (FStar.Int128.v x)
+let from_usize (x:FStar.UInt32.t) : usize  = mk_int (FStar.UInt32.v x)
+let from_isize (x:FStar.Int32.t) : isize  = mk_int (FStar.Int32.v x)
+
+let to_uint8 (x:u8) : FStar.UInt8.t = FStar.UInt8.uint_to_t (v x)
+let to_int8 (x:i8) : FStar.Int8.t  = FStar.Int8.int_to_t (v x)
+let to_uint16 (x:u16) : FStar.UInt16.t  = FStar.UInt16.uint_to_t (v x)
+let to_int16 (x:i16) : FStar.Int16.t  = FStar.Int16.int_to_t (v x)
+let to_uint32 (x:u32) : FStar.UInt32.t  = FStar.UInt32.uint_to_t (v x)
+let to_int32 (x:i32) : FStar.Int32.t  = FStar.Int32.int_to_t (v x)
+let to_uint64 (x:u64) : FStar.UInt64.t  = FStar.UInt64.uint_to_t (v x)
+let to_int64 (x:i64) : FStar.Int64.t  = FStar.Int64.int_to_t (v x)
+let to_uint128 (x:u128) : FStar.UInt128.t  = FStar.UInt128.uint_to_t (v x)
+let to_int128 (x:i128) : FStar.Int128.t  = FStar.Int128.int_to_t (v x)


I wonder if those function are used at all: since this PR aims at being non-disruptive, keeping them seems legitimate, but maybe we should add a TODO to get rid of those?

W95Psp · 2025-01-20T08:25:32Z

engine/backends/fstar/fstar_backend.ml

+  (* Print a literal as an F* constant *)
+  let rec pliteral_as_const span (e : literal) =
    match e with
    | String s -> F.Const.Const_string (s, F.dummyRange)
    | Char c -> F.Const.Const_char (Char.to_int c)
    | Int { value; kind = { size; signedness }; negative } ->
-        let open F.Const in
-        let size =
-          match size with
-          | S8 -> Int8
-          | S16 -> Int16
-          | S32 -> Int32
-          | S64 -> Int64
-          | S128 ->
-              Error.unimplemented ~issue_id:464
-                ~details:
-                  "Matching on u128 or i128 literals is not yet supported." span
-          | SSize ->
-              Error.unimplemented ~issue_id:464
-                ~details:
-                  "Matching on usize or isize literals is not yet supported. \
-                   As a work-around, instead of `match expr { 0 => ... }`, \
-                   please cast for instance to `u64` before: `match expr as \
-                   u64 { 0 => ... }`."
-                span
+        Error.unimplemented
+          ~details:
+            "Integers cannot be printed as constants, they can only be printed \
+             as expressions."
+          span
+    | Float _ ->
+        Error.unimplemented
+          ~details:
+            "Floats cannot be printed as constants, they can only be printed \
+             as expressions."
+          span
+    | Bool b -> F.Const.Const_bool b
+
+  (* Print a literal appearing in a pattern as an F* pattern *)
+  let rec pliteral_as_pat span (e : literal) =
+    match e with
+    | Int { value; kind = { size; signedness }; negative } ->
+        let pat_name =
+          F.pat
+          @@ F.AST.PatName (F.lid [ "Rust_primitives"; "Integers"; "MkInt" ])
+        in
+        let mk_const c = F.AST.PatConst c |> F.pat in
+        let mk_int value negative =
+          mk_const (F.Const.Const_int (pnegative negative ^ value, None))
        in
-        F.Const.Const_int
-          ( pnegative negative ^ value,
-            Some
-              ( (match signedness with Signed -> Signed | Unsigned -> Unsigned),
-                size ) )
+        F.pat_app pat_name @@ [ mk_int value negative ]
    | Float _ ->
        Error.unimplemented ~issue_id:464
-          ~details:"Matching on f32 or f64 literals is not yet supported." span
-    | Bool b -> F.Const.Const_bool b
+          ~details:"Pattern matching on floats is not yet supported." span
+    | _ -> F.pat @@ F.AST.PatConst (pliteral_as_const span e)

  let pliteral_as_expr span (e : literal) =
    let mk_const c = F.AST.Const c |> F.term in
-    let mk_nat value negative =
+    let mk_int value negative =
      mk_const (F.Const.Const_int (pnegative negative ^ value, None))
    in
-    let wrap_app fn x n = F.mk_e_app (F.term_of_lid [ fn ]) [ mk_nat x n ] in
    match e with
-    | Int { value; kind = { size = SSize; signedness = sn }; negative = n } ->
-        wrap_app (match sn with Signed -> "isz" | Unsigned -> "sz") value n
-    | Int { value; kind = { size = S128; signedness = sn }; negative } ->
-        let prefix = match sn with Signed -> "i" | Unsigned -> "u" in
-        wrap_app ("pub_" ^ prefix ^ "128") value negative
+    | Int { value; kind = { size; signedness }; negative = n } ->
+        let f =
+          match (size, signedness) with
+          | S8, Signed -> F.lid [ "mk_i8" ]
+          | S16, Signed -> F.lid [ "mk_i16" ]
+          | S32, Signed -> F.lid [ "mk_i32" ]
+          | S64, Signed -> F.lid [ "mk_i64" ]
+          | S128, Signed -> F.lid [ "mk_i128" ]
+          | SSize, Signed -> F.lid [ "mk_isize" ]
+          | S8, Unsigned -> F.lid [ "mk_u8" ]
+          | S16, Unsigned -> F.lid [ "mk_u16" ]
+          | S32, Unsigned -> F.lid [ "mk_u32" ]
+          | S64, Unsigned -> F.lid [ "mk_u64" ]
+          | S128, Unsigned -> F.lid [ "mk_u128" ]
+          | SSize, Unsigned -> F.lid [ "mk_usize" ]
+        in
+        F.mk_e_app (F.term @@ F.AST.Name f) [ mk_int value n ]


I think the pliteral_as_expr / pliteral_as_pat no longer makes sense, we should just have a pliteral with a flag mode:[`Expr | `Pat].
(now we have runtime errors that we should kill statically)

If you want I can implement it, or we can also decide to ignore that, since we want to drop that backend (but I don't see that happening too soon)

karthikbhargavan added 3 commits January 16, 2025 18:53

transparent integers

62ef72d

transparent integers

3818ddd

fixed examples

0a3cac4

fmt

edc07c8

W95Psp mentioned this pull request Jan 20, 2025

F*: bit vector library: restore implementations #1242

Open

W95Psp reviewed Jan 20, 2025

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Transparent integers #1238

Transparent integers #1238

karthikbhargavan commented Jan 17, 2025 •

edited

Loading

karthikbhargavan commented Jan 17, 2025 •

edited

Loading

W95Psp left a comment

W95Psp Jan 20, 2025

W95Psp Jan 20, 2025

W95Psp Jan 20, 2025

Transparent integers #1238

Are you sure you want to change the base?

Transparent integers #1238

Conversation

karthikbhargavan commented Jan 17, 2025 • edited Loading

karthikbhargavan commented Jan 17, 2025 • edited Loading

W95Psp left a comment

Choose a reason for hiding this comment

W95Psp Jan 20, 2025

Choose a reason for hiding this comment

W95Psp Jan 20, 2025

Choose a reason for hiding this comment

W95Psp Jan 20, 2025

Choose a reason for hiding this comment

karthikbhargavan commented Jan 17, 2025 •

edited

Loading

karthikbhargavan commented Jan 17, 2025 •

edited

Loading