Emit integer literals the way C means them - #221
Draft
nikswamy wants to merge 4 commits into
Draft
Conversation
Generated C interfaces commonly define fixed-width bit-pattern constants as explicit casts from long integer literals and expand them into switch tables. On LP64 hosts, a high-bit long literal is a signed 64-bit value, while casting it to int32_t denotes a negative target bit pattern under the PAL two-complement model. Emitting the source literal followed by Int.Cast.int64_to_int32 leaves F* with an out-of-range conversion and prevents otherwise routine generated switches from verifying. Add a dedicated post-elaboration cast-normalization pass. It recovers an integer literal mathematical value from its signedness and width, preserves representable casts as explicit Int.Cast operations, and rewrites only out-of-range casts to target-typed literals. Unsigned conversions use C modulo semantics; non-representable signed conversions follow the PAL two-complement policy. Keep emission responsible only for rendering normalized IR. Use one machine-literal emitter for expressions and patterns, with native F* suffixes at widths 8, 16, 32, and 64 and constructor fallbacks for non-standard widths. Cover direct and X-macro-generated high-bit switch constants, narrowing and wraparound at every width, UINT64_MAX converted to signed int64, and a representable int64-to-uint64 cast that remains explicit. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 981f7d3c-6a91-47ad-84d7-7aadf747123d (cherry picked from commit 9f5c474)
F* lexes a leading `-` as the infix subtraction operator, so the emitted `Int16.int_to_t -1` parses as `Int16.int_to_t - 1`: a partial application of `int_to_t` minus one, which fails to typecheck with Expected expression of type Prims.int got expression FStar.Int16.int_to_t Parenthesize the argument when the value is negative. The 32-bit signed case already avoided this by emitting the `-1l` literal form; only widths that go through `intN_to_t` were affected. This fixes test/integer_literal_casts, which covers exactly the casts that produce negative values (`(int64_t)UINT64_MAX` and friends). Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 981f7d3c-6a91-47ad-84d7-7aadf747123d (cherry picked from commit d1e32c4)
A negative machine-integer literal was rendered bare, as `-1l`. F* lexes `=-` and `:=-` as single operators, so such a literal in a record field initializer or an assignment did not parse at all. Parenthesize the whole literal, suffix included, for the signed 32-bit, size_t, and specification-integer forms. The remaining forms are either normalized non-negative or already parenthesized as function arguments. Extend the negative-literal test to cover a record field and an assignment. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 981f7d3c-6a91-47ad-84d7-7aadf747123d (cherry picked from commit a207b96)
`emit_rvalue_inner` suffixed a literal only at 32-bit signed, 32-bit unsigned and `size_t`; every other width fell through to a constructor application such as `Int64.int_to_t 62586880`. `emit_pattern` already had the full table, so the same constant was spelled two ways depending on where it appeared. The constructor form is not interchangeable with a suffixed literal. `IntN.int_to_t` takes an `FStar.Int.int_t N`, whose refinement only the SMT solver discharges, and Pulse typechecks candidate witnesses without SMT. A value built from those constructors therefore cannot be guessed, and the failure surfaces as "Cannot find witness / Ill-typed term" pointing at `FStar.Int.fsti` rather than at the literal. Factor the table into a shared `machine_int_literal` helper covering 8/16/32/64 signed and unsigned plus `sz`, and use it from both emitters. The constructor form remains only as a fallback for widths that have no F* suffix. `normalize_casts` had the same problem from the other side: it folded a cast of a literal only when the value did *not* fit the target type, so a representable cast kept an `id #T (Int.Cast...)` wrapper that reduces to the refined constructor. Fold both cases. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 981f7d3c-6a91-47ad-84d7-7aadf747123d (cherry picked from commit 6668b8a)
Contributor
|
!diff |
Generated F* output diffEffect of this pull request on the F* code SummaryFull diff: full diff artifact Diffdiff --git base/addr_global/Global_g_const.fst head/addr_global/Global_g_const.fst
index 5cb845a..1c228e3 100644
--- base/addr_global/Global_g_const.fst
+++ head/addr_global/Global_g_const.fst
@@ -3,7 +3,7 @@ open Pulse
open Pulse.Lib.C
#lang-pulse
-let var_g_const : Typedef_uint32_t.ty_uint32_t = (id #UInt32.t (Int.Cast.int32_to_uint32 42l))
+let var_g_const : Typedef_uint32_t.ty_uint32_t = 42ul
assume val addr_var_g_const : (ref Typedef_uint32_t.ty_uint32_t)
assume val addr_var_g_const_not_null : squash (~(Pulse.Lib.Reference.is_null addr_var_g_const))
assume val acquire_var_g_const :
diff --git base/addr_global/Global_g_implicit.fst head/addr_global/Global_g_implicit.fst
index e84e21b..aa7dde4 100644
--- base/addr_global/Global_g_implicit.fst
+++ head/addr_global/Global_g_implicit.fst
@@ -3,7 +3,7 @@ open Pulse
open Pulse.Lib.C
#lang-pulse
-let var_g_implicit : Typedef_uint32_t.ty_uint32_t = (id #UInt32.t (Int.Cast.int32_to_uint32 7l))
+let var_g_implicit : Typedef_uint32_t.ty_uint32_t = 7ul
assume val addr_var_g_implicit : (ref Typedef_uint32_t.ty_uint32_t)
assume val addr_var_g_implicit_not_null : squash (~(Pulse.Lib.Reference.is_null addr_var_g_implicit))
assume val acquire_var_g_implicit :
diff --git base/antiquot/Func_test_union.fst head/antiquot/Func_test_union.fst
index f8d7293..55c1c78 100644
--- base/antiquot/Func_test_union.fst
+++ head/antiquot/Func_test_union.fst
@@ -7,8 +7,7 @@ divergent fn func_test_union ()
returns return_1 : unit
{
let mut var_x : Typedef_my_union.ty_my_union;
- var_x :=
- (Union_my_union_anon_1.Field_my_union_anon_1__b (id #Int64.t (Int.Cast.int32_to_int64 1l)));
+ var_x := (Union_my_union_anon_1.Field_my_union_anon_1__b 1L);
assert (with_pure (not (Union_my_union_anon_1.Field_my_union_anon_1__a? (!var_x))));
assert pure (~(Antiquot_include2.other_fun (!var_x)));
}
\ No newline at end of file
diff --git base/array_test/Func_b32_arr.fst head/array_test/Func_b32_arr.fst
index 4e1f7a7..7a511a3 100644
--- base/array_test/Func_b32_arr.fst
+++ head/array_test/Func_b32_arr.fst
@@ -20,8 +20,5 @@ divergent fn func_b32_arr (var_a: Typedef_b32_struct.ty_b32_struct)
67))
{
let mut var_a = var_a;
- (array_write
- (!(Struct_b32_struct_anon_1.struct_b32_struct_anon_1__get_x var_a))
- 10sz
- (id #UInt8.t (Int.Cast.int32_to_uint8 67l)));
+ (array_write (!(Struct_b32_struct_anon_1.struct_b32_struct_anon_1__get_x var_a)) 10sz 67uy);
}
\ No newline at end of file
diff --git base/array_test/Func_foo.fst head/array_test/Func_foo.fst
index bb95d93..603356b 100644
--- base/array_test/Func_foo.fst
+++ head/array_test/Func_foo.fst
@@ -12,10 +12,6 @@ divergent fn func_foo (var_a: (array UInt32.t))
ensures (with_pure ((id #int (UInt32.v ((array_read var_a 0sz)))) = 42))
{
let mut var_a = var_a;
- (array_write (!var_a) 0sz (id #UInt32.t (Int.Cast.int32_to_uint32 42l)));
- (array_write
- (!var_a)
- 1sz
- (((array_read (!var_a) 0sz)) `Pulse.Lib.C.UInt32.add_wrap`
- (id #UInt32.t (Int.Cast.int32_to_uint32 67l))));
+ (array_write (!var_a) 0sz 42ul);
+ (array_write (!var_a) 1sz (((array_read (!var_a) 0sz)) `Pulse.Lib.C.UInt32.add_wrap` 67ul));
}
\ No newline at end of file
diff --git base/array_test/Func_ptr_attr.fst head/array_test/Func_ptr_attr.fst
index a5c81a8..7827546 100644
--- base/array_test/Func_ptr_attr.fst
+++ head/array_test/Func_ptr_attr.fst
@@ -12,10 +12,6 @@ divergent fn func_ptr_attr (var_a: (array UInt32.t))
ensures (with_pure ((id #int (UInt32.v ((array_read var_a 0sz)))) = 42))
{
let mut var_a = var_a;
- (array_write (!var_a) 0sz (id #UInt32.t (Int.Cast.int32_to_uint32 42l)));
- (array_write
- (!var_a)
- 1sz
- (((array_read (!var_a) 0sz)) `Pulse.Lib.C.UInt32.add_wrap`
- (id #UInt32.t (Int.Cast.int32_to_uint32 67l))));
+ (array_write (!var_a) 0sz 42ul);
+ (array_write (!var_a) 1sz (((array_read (!var_a) 0sz)) `Pulse.Lib.C.UInt32.add_wrap` 67ul));
}
\ No newline at end of file
diff --git base/array_test/Func_struct_arr.fst head/array_test/Func_struct_arr.fst
index 844596e..edddb6d 100644
--- base/array_test/Func_struct_arr.fst
+++ head/array_test/Func_struct_arr.fst
@@ -28,14 +28,11 @@ divergent fn func_struct_arr (var_a: Typedef_uptr_struct.ty_uptr_struct)
42))
{
let mut var_a = var_a;
- (array_write
- (!(Struct_uptr_struct_anon_1.struct_uptr_struct_anon_1__get_x var_a))
- 0sz
- (id #UInt32.t (Int.Cast.int32_to_uint32 42l)));
+ (array_write (!(Struct_uptr_struct_anon_1.struct_uptr_struct_anon_1__get_x var_a)) 0sz 42ul);
(array_write
(!(Struct_uptr_struct_anon_1.struct_uptr_struct_anon_1__get_x var_a))
1sz
(((array_read (!(Struct_uptr_struct_anon_1.struct_uptr_struct_anon_1__get_x var_a)) 0sz))
`Pulse.Lib.C.UInt32.add_wrap`
- (id #UInt32.t (Int.Cast.int32_to_uint32 67l))));
+ 67ul));
}
\ No newline at end of file
diff --git base/array_test/Func_test_two_arrays.fst head/array_test/Func_test_two_arrays.fst
index 7a18d9e..1eb31bf 100644
--- base/array_test/Func_test_two_arrays.fst
+++ head/array_test/Func_test_two_arrays.fst
@@ -14,7 +14,7 @@ divergent fn func_test_two_arrays ()
3sz);
Struct_two_arrays_anon_1.struct_two_arrays_anon_1__y=(Pulse.Lib.C.Array.alloc_array
#Int32.t
- (SizeT.uint_to_t (UInt64.v (id #UInt64.t (Int.Cast.int32_to_uint64 4l)))));
+ 4sz);
};
(array_write (!(Struct_two_arrays_anon_1.struct_two_arrays_anon_1__get_x var_p)) 2sz 3l);
(Pulse.Lib.C.Array.free_array
diff --git base/array_test/Func_tydef_array.fst head/array_test/Func_tydef_array.fst
index c7665e4..aef88e0 100644
--- base/array_test/Func_tydef_array.fst
+++ head/array_test/Func_tydef_array.fst
@@ -16,10 +16,6 @@ divergent fn func_tydef_array (var_a: Typedef_uptr.ty_uptr)
ensures (with_pure ((id #int (UInt32.v ((array_read var_a 0sz)))) = 42))
{
let mut var_a = var_a;
- (array_write (!var_a) 0sz (id #UInt32.t (Int.Cast.int32_to_uint32 42l)));
- (array_write
- (!var_a)
- 1sz
- (((array_read (!var_a) 0sz)) `Pulse.Lib.C.UInt32.add_wrap`
- (id #UInt32.t (Int.Cast.int32_to_uint32 67l))));
+ (array_write (!var_a) 0sz 42ul);
+ (array_write (!var_a) 1sz (((array_read (!var_a) 0sz)) `Pulse.Lib.C.UInt32.add_wrap` 67ul));
}
\ No newline at end of file
diff --git base/arrayptr_ref/Func_assign_cell_address_to_ref.fst head/arrayptr_ref/Func_assign_cell_address_to_ref.fst
index 1dea4a2..e2ac111 100644
--- base/arrayptr_ref/Func_assign_cell_address_to_ref.fst
+++ head/arrayptr_ref/Func_assign_cell_address_to_ref.fst
@@ -18,10 +18,8 @@ divergent fn func_assign_cell_address_to_ref (var_a: (array Typedef_SUBRANGE.ty_
var_sub := (array_borrow_cell (!var_a) 0sz);
Pulse.Lib.C.MaybeUninit.forget_maybe (!var_sub);
Struct_SUBRANGE_anon_1.struct_subrange_anon_1__aux_raw_unfold_uninit (!var_sub);
- (Struct_SUBRANGE_anon_1.struct_subrange_anon_1__get_low (!var_sub)) :=
- (id #UInt64.t (Int.Cast.int32_to_uint64 10l));
- (Struct_SUBRANGE_anon_1.struct_subrange_anon_1__get_count (!var_sub)) :=
- (id #UInt64.t (Int.Cast.int32_to_uint64 5l));
+ (Struct_SUBRANGE_anon_1.struct_subrange_anon_1__get_low (!var_sub)) := 10uL;
+ (Struct_SUBRANGE_anon_1.struct_subrange_anon_1__get_count (!var_sub)) := 5uL;
Struct_SUBRANGE_anon_1.struct_subrange_anon_1__aux_raw_fold (!var_sub) _ _;
Pulse.Lib.C.MaybeUninit.intro_maybe_some (!var_sub);
array_return_cell (!var_a);
diff --git base/arrayptr_ref/Func_consume_returned_arrayptr_as_ref.fst head/arrayptr_ref/Func_consume_returned_arrayptr_as_ref.fst
index 9717eb2..3f374ac 100644
--- base/arrayptr_ref/Func_consume_returned_arrayptr_as_ref.fst
+++ head/arrayptr_ref/Func_consume_returned_arrayptr_as_ref.fst
@@ -18,10 +18,8 @@ divergent fn func_consume_returned_arrayptr_as_ref (var_a: (array Typedef_SUBRAN
var_sub := (arrayptr_borrow_cell (Func_get_uninit.func_get_uninit (!var_a)));
Pulse.Lib.C.MaybeUninit.forget_maybe (!var_sub);
Struct_SUBRANGE_anon_1.struct_subrange_anon_1__aux_raw_unfold_uninit (!var_sub);
- (Struct_SUBRANGE_anon_1.struct_subrange_anon_1__get_low (!var_sub)) :=
- (id #UInt64.t (Int.Cast.int32_to_uint64 10l));
- (Struct_SUBRANGE_anon_1.struct_subrange_anon_1__get_count (!var_sub)) :=
- (id #UInt64.t (Int.Cast.int32_to_uint64 5l));
+ (Struct_SUBRANGE_anon_1.struct_subrange_anon_1__get_low (!var_sub)) := 10uL;
+ (Struct_SUBRANGE_anon_1.struct_subrange_anon_1__get_count (!var_sub)) := 5uL;
Struct_SUBRANGE_anon_1.struct_subrange_anon_1__aux_raw_fold (!var_sub) _ _;
Pulse.Lib.C.MaybeUninit.intro_maybe_some (!var_sub);
array_return_cell (!var_a);
diff --git base/arrayptrs/Func_binary_search.fst head/arrayptrs/Func_binary_search.fst
index 05c0b94..5560295 100644
--- base/arrayptrs/Func_binary_search.fst
+++ head/arrayptrs/Func_binary_search.fst
@@ -34,8 +34,7 @@ pure (offset_of var_lo <= offset_of return_1 /\ offset_of return_1 < offset_of v
(!var_lo)
(SizeT.uint_to_t (Pulse.Lib.C.PtrdiffT.v
(((arrayptr_diff (!var_hi) (!var_lo))) `Pulse.Lib.C.PtrdiffT.div`
- (Pulse.Lib.C.PtrdiffT.of_int (Int64.v
- (id #Int64.t (Int.Cast.int32_to_int64 2l)))))))));
+ (Pulse.Lib.C.PtrdiffT.of_int (Int64.v 2L)))))));
if ((((arrayptr_read (!var_mid) 0sz)) = (!var_target))) {
return (!var_mid);
} else {
diff --git base/bitfields/Func_set_a.fst head/bitfields/Func_set_a.fst
index d913f13..0b10b65 100644
--- base/bitfields/Func_set_a.fst
+++ head/bitfields/Func_set_a.fst
@@ -16,6 +16,5 @@ divergent fn func_set_a (var_s: (ref Struct_flags.struct_flags))
ensures (with_pure ((id #int (UInt32.v (!(Struct_flags.struct_flags__get_a var_s)))) = 5))
{
let mut var_s = var_s;
- (Struct_flags.struct_flags__get_a (!var_s)) :=
- (Pulse.Lib.C.BitField.mask_u32 3 (id #UInt32.t (Int.Cast.int32_to_uint32 5l)));
+ (Struct_flags.struct_flags__get_a (!var_s)) := (Pulse.Lib.C.BitField.mask_u32 3 5ul);
}
\ No newline at end of file
diff --git base/break_continue/Func_count_to_limit.fst head/break_continue/Func_count_to_limit.fst
index 2cee6e5..4e3da4d 100644
--- base/break_continue/Func_count_to_limit.fst
+++ head/break_continue/Func_count_to_limit.fst
@@ -16,7 +16,7 @@ divergent fn func_count_to_limit
let mut var_n = var_n;
let mut var_limit = var_limit;
let mut var_i : Typedef_uint32_t.ty_uint32_t;
- var_i := (id #UInt32.t (Int.Cast.int32_to_uint32 0l));
+ var_i := 0ul;
while (((!var_i) `UInt32.lt` (!var_n)))
invariant (live var_i)
invariant (with_pure ((!var_i) `UInt32.lte` (!var_n)))
@@ -25,7 +25,7 @@ divergent fn func_count_to_limit
if (((!var_i) = (!var_limit))) {
break;
} else {};
- var_i := ((!var_i) `Pulse.Lib.C.UInt32.add_wrap` (id #UInt32.t (Int.Cast.int32_to_uint32 1l)));
+ var_i := ((!var_i) `Pulse.Lib.C.UInt32.add_wrap` 1ul);
};
return (!var_i);
}
\ No newline at end of file
diff --git base/break_continue/Func_sum_evens.fst head/break_continue/Func_sum_evens.fst
index 3c496e0..8a65e2f 100644
--- base/break_continue/Func_sum_evens.fst
+++ head/break_continue/Func_sum_evens.fst
@@ -12,16 +12,16 @@ divergent fn func_sum_evens (var_n: Typedef_uint32_t.ty_uint32_t)
{
let mut var_n = var_n;
let mut var_i : Typedef_uint32_t.ty_uint32_t;
- var_i := (id #UInt32.t (Int.Cast.int32_to_uint32 0l));
+ var_i := 0ul;
let mut var_s : Typedef_uint32_t.ty_uint32_t;
- var_s := (id #UInt32.t (Int.Cast.int32_to_uint32 0l));
+ var_s := 0ul;
while (((!var_i) `UInt32.lt` (!var_n)))
invariant ((live var_i) ** (live var_s))
invariant (with_pure ((!var_i) `UInt32.lte` (!var_n)))
invariant (with_pure ((id #int (UInt32.v (!var_s))) <= (10000 * (id #int (UInt32.v (!var_i))))))
{
- var_i := ((!var_i) `Pulse.Lib.C.UInt32.add_wrap` (id #UInt32.t (Int.Cast.int32_to_uint32 1l)));
- if (((!var_i) = (id #UInt32.t (Int.Cast.int32_to_uint32 1l)))) {
+ var_i := ((!var_i) `Pulse.Lib.C.UInt32.add_wrap` 1ul);
+ if (((!var_i) = 1ul)) {
continue;
} else {};
var_s := ((!var_s) `Pulse.Lib.C.UInt32.add_wrap` (!var_i));
diff --git base/calloc_alloc_size/Func_test_calloc_count_mul_size.fst head/calloc_alloc_size/Func_test_calloc_count_mul_size.fst
index 96c3908..cf2f06e 100644
--- base/calloc_alloc_size/Func_test_calloc_count_mul_size.fst
+++ head/calloc_alloc_size/Func_test_calloc_count_mul_size.fst
@@ -7,10 +7,7 @@ divergent fn func_test_calloc_count_mul_size ()
returns return_1 : unit
{
let mut var_array : (array Int32.t);
- var_array :=
- (Pulse.Lib.C.Array.calloc_array
- #Int32.t
- (SizeT.uint_to_t (UInt64.v (id #UInt64.t (Int.Cast.int32_to_uint64 3l)))));
+ var_array := (Pulse.Lib.C.Array.calloc_array #Int32.t 3sz);
assert (with_pure ((reveal (length_of (!var_array))) = 3));
assert (with_pure ((id #int (Int32.v ((array_read (!var_array) 0sz)))) = 0));
(array_write (!var_array) 0sz 67l);
diff --git base/calloc_alloc_size/Func_test_calloc_count_size_mul.fst head/calloc_alloc_size/Func_test_calloc_count_size_mul.fst
index 367339b..df2ac86 100644
--- base/calloc_alloc_size/Func_test_calloc_count_size_mul.fst
+++ head/calloc_alloc_size/Func_test_calloc_count_size_mul.fst
@@ -7,10 +7,7 @@ divergent fn func_test_calloc_count_size_mul ()
returns return_1 : unit
{
let mut var_array : (array Int32.t);
- var_array :=
- (Pulse.Lib.C.Array.calloc_array
- #Int32.t
- (SizeT.uint_to_t (UInt64.v (id #UInt64.t (Int.Cast.int32_to_uint64 4l)))));
+ var_array := (Pulse.Lib.C.Array.calloc_array #Int32.t 4sz);
assert (with_pure ((reveal (length_of (!var_array))) = 4));
assert (with_pure ((id #int (Int32.v ((array_read (!var_array) 0sz)))) = 0));
(Pulse.Lib.C.Array.free_array (!var_array));
diff --git base/char_array_padding/Global_entry_bytes.fst head/char_array_padding/Global_entry_bytes.fst
index c5e9296..90cb5d8 100644
--- base/char_array_padding/Global_entry_bytes.fst
+++ head/char_array_padding/Global_entry_bytes.fst
@@ -7,22 +7,22 @@ let var_entry_bytes : Typedef_entry.ty_entry =
{
Struct_entry_anon_1.struct_entry_anon_1__desc=(array_spec_of_list_with_len
#Int8.t
- (Cons #Int8.t (Int8.int_to_t 98)
- (Cons #Int8.t (Int8.int_to_t 121)
- (Cons #Int8.t (Int8.int_to_t 116)
- (Cons #Int8.t (Int8.int_to_t 101)
- (Cons #Int8.t (Int8.int_to_t 115)
- (Cons #Int8.t (Int8.int_to_t 0)
- (Cons #Int8.t (Int8.int_to_t 0)
- (Cons #Int8.t (Int8.int_to_t 0)
- (Cons #Int8.t (Int8.int_to_t 0)
- (Cons #Int8.t (Int8.int_to_t 0)
- (Cons #Int8.t (Int8.int_to_t 0)
- (Cons #Int8.t (Int8.int_to_t 0)
- (Cons #Int8.t (Int8.int_to_t 0)
- (Cons #Int8.t (Int8.int_to_t 0)
- (Cons #Int8.t (Int8.int_to_t 0)
- (Cons #Int8.t (Int8.int_to_t 0)
+ (Cons #Int8.t 98y
+ (Cons #Int8.t 121y
+ (Cons #Int8.t 116y
+ (Cons #Int8.t 101y
+ (Cons #Int8.t 115y
+ (Cons #Int8.t 0y
+ (Cons #Int8.t 0y
+ (Cons #Int8.t 0y
+ (Cons #Int8.t 0y
+ (Cons #Int8.t 0y
+ (Cons #Int8.t 0y
+ (Cons #Int8.t 0y
+ (Cons #Int8.t 0y
+ (Cons #Int8.t 0y
+ (Cons #Int8.t 0y
+ (Cons #Int8.t 0y
(Nil #Int8.t)))))))))))))))))
16);
}
diff --git base/char_array_padding/Global_entry_packets.fst head/char_array_padding/Global_entry_packets.fst
index e54a0eb..f53d895 100644
--- base/char_array_padding/Global_entry_packets.fst
+++ head/char_array_padding/Global_entry_packets.fst
@@ -7,22 +7,22 @@ let var_entry_packets : Typedef_entry.ty_entry =
{
Struct_entry_anon_1.struct_entry_anon_1__desc=(array_spec_of_list_with_len
#Int8.t
- (Cons #Int8.t (Int8.int_to_t 112)
- (Cons #Int8.t (Int8.int_to_t 97)
- (Cons #Int8.t (Int8.int_to_t 99)
- (Cons #Int8.t (Int8.int_to_t 107)
- (Cons #Int8.t (Int8.int_to_t 101)
- (Cons #Int8.t (Int8.int_to_t 116)
- (Cons #Int8.t (Int8.int_to_t 115)
- (Cons #Int8.t (Int8.int_to_t 0)
- (Cons #Int8.t (Int8.int_to_t 0)
- (Cons #Int8.t (Int8.int_to_t 0)
- (Cons #Int8.t (Int8.int_to_t 0)
- (Cons #Int8.t (Int8.int_to_t 0)
- (Cons #Int8.t (Int8.int_to_t 0)
- (Cons #Int8.t (Int8.int_to_t 0)
- (Cons #Int8.t (Int8.int_to_t 0)
- (Cons #Int8.t (Int8.int_to_t 0)
+ (Cons #Int8.t 112y
+ (Cons #Int8.t 97y
+ (Cons #Int8.t 99y
+ (Cons #Int8.t 107y
+ (Cons #Int8.t 101y
+ (Cons #Int8.t 116y
+ (Cons #Int8.t 115y
+ (Cons #Int8.t 0y
+ (Cons #Int8.t 0y
+ (Cons #Int8.t 0y
+ (Cons #Int8.t 0y
+ (Cons #Int8.t 0y
+ (Cons #Int8.t 0y
+ (Cons #Int8.t 0y
+ (Cons #Int8.t 0y
+ (Cons #Int8.t 0y
(Nil #Int8.t)))))))))))))))))
16);
}
diff --git base/char_array_padding/Global_exact.fst head/char_array_padding/Global_exact.fst
index 9eeb432..2df8515 100644
--- base/char_array_padding/Global_exact.fst
+++ head/char_array_padding/Global_exact.fst
@@ -6,13 +6,13 @@ open Pulse.Lib.C
let var_exact : (full_array_lspec Int8.t 8) =
(array_spec_of_list_with_len
#Int8.t
- (Cons #Int8.t (Int8.int_to_t 112)
- (Cons #Int8.t (Int8.int_to_t 97)
- (Cons #Int8.t (Int8.int_to_t 99)
- (Cons #Int8.t (Int8.int_to_t 107)
- (Cons #Int8.t (Int8.int_to_t 101)
- (Cons #Int8.t (Int8.int_to_t 116)
- (Cons #Int8.t (Int8.int_to_t 115)
- (Cons #Int8.t (Int8.int_to_t 0)
+ (Cons #Int8.t 112y
+ (Cons #Int8.t 97y
+ (Cons #Int8.t 99y
+ (Cons #Int8.t 107y
+ (Cons #Int8.t 101y
+ (Cons #Int8.t 116y
+ (Cons #Int8.t 115y
+ (Cons #Int8.t 0y
(Nil #Int8.t)))))))))
8)
\ No newline at end of file
diff --git base/char_array_padding/Global_padded.fst head/char_array_padding/Global_padded.fst
index d9ce31c..e7563d1 100644
--- base/char_array_padding/Global_padded.fst
+++ head/char_array_padding/Global_padded.fst
@@ -6,21 +6,21 @@ open Pulse.Lib.C
let var_padded : (full_array_lspec Int8.t 16) =
(array_spec_of_list_with_len
#Int8.t
- (Cons #Int8.t (Int8.int_to_t 112)
- (Cons #Int8.t (Int8.int_to_t 97)
- (Cons #Int8.t (Int8.int_to_t 99)
- (Cons #Int8.t (Int8.int_to_t 107)
- (Cons #Int8.t (Int8.int_to_t 101)
- (Cons #Int8.t (Int8.int_to_t 116)
- (Cons #Int8.t (Int8.int_to_t 115)
- (Cons #Int8.t (Int8.int_to_t 0)
- (Cons #Int8.t (Int8.int_to_t 0)
- (Cons #Int8.t (Int8.int_to_t 0)
- (Cons #Int8.t (Int8.int_to_t 0)
- (Cons #Int8.t (Int8.int_to_t 0)
- (Cons #Int8.t (Int8.int_to_t 0)
- (Cons #Int8.t (Int8.int_to_t 0)
- (Cons #Int8.t (Int8.int_to_t 0)
- (Cons #Int8.t (Int8.int_to_t 0)
+ (Cons #Int8.t 112y
+ (Cons #Int8.t 97y
+ (Cons #Int8.t 99y
+ (Cons #Int8.t 107y
+ (Cons #Int8.t 101y
+ (Cons #Int8.t 116y
+ (Cons #Int8.t 115y
+ (Cons #Int8.t 0y
+ (Cons #Int8.t 0y
+ (Cons #Int8.t 0y
+ (Cons #Int8.t 0y
+ (Cons #Int8.t 0y
+ (Cons #Int8.t 0y
+ (Cons #Int8.t 0y
+ (Cons #Int8.t 0y
+ (Cons #Int8.t 0y
(Nil #Int8.t)))))))))))))))))
16)
\ No newline at end of file
diff --git base/compound_ops/Func_test_u16_post_incr_wrap.fst head/compound_ops/Func_test_u16_post_incr_wrap.fst
index 57eefac..e046fb3 100644
--- base/compound_ops/Func_test_u16_post_incr_wrap.fst
+++ head/compound_ops/Func_test_u16_post_incr_wrap.fst
@@ -9,7 +9,7 @@ divergent fn func_test_u16_post_incr_wrap ()
ensures (with_pure ((id #int (UInt16.v return_1)) = 0))
{
let mut var_a : Typedef_uint16_t.ty_uint16_t;
- var_a := (id #UInt16.t (Int.Cast.int32_to_uint16 65535l));
+ var_a := 65535us;
let _ = (Pulse.Lib.C.UnaryOps.pluspluspost_uint16 var_a);
return (!var_a);
}
\ No newline at end of file
diff --git base/compound_ops/Func_test_u32_pre_decr_wrap.fst head/compound_ops/Func_test_u32_pre_decr_wrap.fst
index 374f65d..1a5f576 100644
--- base/compound_ops/Func_test_u32_pre_decr_wrap.fst
+++ head/compound_ops/Func_test_u32_pre_decr_wrap.fst
@@ -9,7 +9,7 @@ divergent fn func_test_u32_pre_decr_wrap ()
ensures (with_pure (return_1 = 4294967295ul))
{
let mut var_a : Typedef_uint32_t.ty_uint32_t;
- var_a := (id #UInt32.t (Int.Cast.int32_to_uint32 0l));
+ var_a := 0ul;
let _ = (Pulse.Lib.C.UnaryOps.minusminuspre_uint32 var_a);
return (!var_a);
}
\ No newline at end of file
diff --git base/compound_ops/Func_test_u64_post_decr_wrap.fst head/compound_ops/Func_test_u64_post_decr_wrap.fst
index 195e076..cd3a766 100644
--- base/compound_ops/Func_test_u64_post_decr_wrap.fst
+++ head/compound_ops/Func_test_u64_post_decr_wrap.fst
@@ -6,10 +6,10 @@ open Pulse.Lib.C
divergent fn func_test_u64_post_decr_wrap ()
returns return_1 : Typedef_uint64_t.ty_uint64_t
ensures ((Typedef_uint64_t.ty_uint64_t__pred return_1 1.0R))
- ensures (with_pure (return_1 = (UInt64.uint_to_t 18446744073709551615)))
+ ensures (with_pure (return_1 = 18446744073709551615uL))
{
let mut var_a : Typedef_uint64_t.ty_uint64_t;
- var_a := (id #UInt64.t (Int.Cast.int32_to_uint64 0l));
+ var_a := 0uL;
let _ = (Pulse.Lib.C.UnaryOps.minusminuspost_uint64 var_a);
return (!var_a);
}
\ No newline at end of file
diff --git base/compound_ops/Func_test_u64_post_decr_wrap.fsti head/compound_ops/Func_test_u64_post_decr_wrap.fsti
index d6bc3bc..67b3170 100644
--- base/compound_ops/Func_test_u64_post_decr_wrap.fsti
+++ head/compound_ops/Func_test_u64_post_decr_wrap.fsti
@@ -6,4 +6,4 @@ open Pulse.Lib.C
divergent fn func_test_u64_post_decr_wrap ()
returns return_1 : Typedef_uint64_t.ty_uint64_t
ensures ((Typedef_uint64_t.ty_uint64_t__pred return_1 1.0R))
-ensures (with_pure (return_1 = (UInt64.uint_to_t 18446744073709551615)))
\ No newline at end of file
+ensures (with_pure (return_1 = 18446744073709551615uL))
\ No newline at end of file
diff --git base/compound_ops/Func_test_u8_pre_incr_wrap.fst head/compound_ops/Func_test_u8_pre_incr_wrap.fst
index 24ff0d0..f73d5c5 100644
--- base/compound_ops/Func_test_u8_pre_incr_wrap.fst
+++ head/compound_ops/Func_test_u8_pre_incr_wrap.fst
@@ -9,7 +9,7 @@ divergent fn func_test_u8_pre_incr_wrap ()
ensures (with_pure ((id #int (UInt8.v return_1)) = 0))
{
let mut var_a : Typedef_uint8_t.ty_uint8_t;
- var_a := (id #UInt8.t (Int.Cast.int32_to_uint8 255l));
+ var_a := 255uy;
let _ = (Pulse.Lib.C.UnaryOps.pluspluspre_uint8 var_a);
return (!var_a);
}
\ No newline at end of file
diff --git base/decl_ref/Func_enum_to_int.fst head/decl_ref/Func_enum_to_int.fst
index 550a24e..6f1b389 100644
--- base/decl_ref/Func_enum_to_int.fst
+++ head/decl_ref/Func_enum_to_int.fst
@@ -13,10 +13,10 @@ divergent fn func_enum_to_int (var_c: Typedef_uint32_t.ty_uint32_t)
ensures (with_pure (((id #int (UInt32.v var_c)) = 2) ==> ((id #int (Int32.v return_1)) = 2)))
{
let mut var_c = var_c;
- if (((!var_c) = (id #UInt32.t (Int.Cast.int32_to_uint32 0l)))) {
+ if (((!var_c) = 0ul)) {
return 0l;
} else {};
- if (((!var_c) = (id #UInt32.t (Int.Cast.int32_to_uint32 1l)))) {
+ if (((!var_c) = 1ul)) {
return 1l;
} else {};
return 2l;
diff --git base/decl_ref/Func_opposite.fst head/decl_ref/Func_opposite.fst
index c59d948..d7a4368 100644
--- base/decl_ref/Func_opposite.fst
+++ head/decl_ref/Func_opposite.fst
@@ -14,13 +14,13 @@ divergent fn func_opposite (var_d: Typedef_uint32_t.ty_uint32_t)
ensures (with_pure (((id #int (UInt32.v var_d)) = 3) ==> ((id #int (Int32.v return_1)) = 2)))
{
let mut var_d = var_d;
- if (((!var_d) = (id #UInt32.t (Int.Cast.int32_to_uint32 0l)))) {
+ if (((!var_d) = 0ul)) {
return 1l;
} else {};
- if (((!var_d) = (id #UInt32.t (Int.Cast.int32_to_uint32 1l)))) {
+ if (((!var_d) = 1ul)) {
return 0l;
} else {};
- if (((!var_d) = (id #UInt32.t (Int.Cast.int32_to_uint32 2l)))) {
+ if (((!var_d) = 2ul)) {
return 3l;
} else {};
return 2l;
diff --git base/do_while/Func_count_odd.fst head/do_while/Func_count_odd.fst
index d888b93..a87fe68 100644
--- base/do_while/Func_count_odd.fst
+++ head/do_while/Func_count_odd.fst
@@ -12,9 +12,9 @@ divergent fn func_count_odd (var_n: Typedef_uint32_t.ty_uint32_t)
{
let mut var_n = var_n;
let mut var_i : Typedef_uint32_t.ty_uint32_t;
- var_i := (id #UInt32.t (Int.Cast.int32_to_uint32 0l));
+ var_i := 0ul;
let mut var_count : Typedef_uint32_t.ty_uint32_t;
- var_count := (id #UInt32.t (Int.Cast.int32_to_uint32 0l));
+ var_count := 0ul;
let mut var_first : bool;
var_first := true;
while (((!var_first) || ((!var_i) `UInt32.lt` (!var_n))))
@@ -25,13 +25,11 @@ divergent fn func_count_odd (var_n: Typedef_uint32_t.ty_uint32_t)
invariant (with_pure ((id #int (UInt32.v (!var_count))) <= (id #int (UInt32.v (!var_i)))))
{
var_first := false;
- var_i := ((!var_i) `Pulse.Lib.C.UInt32.add_wrap` (id #UInt32.t (Int.Cast.int32_to_uint32 1l)));
- if ((((!var_i) `UInt32.rem` (id #UInt32.t (Int.Cast.int32_to_uint32 2l))) =
- (id #UInt32.t (Int.Cast.int32_to_uint32 0l)))) {
+ var_i := ((!var_i) `Pulse.Lib.C.UInt32.add_wrap` 1ul);
+ if ((((!var_i) `UInt32.rem` 2ul) = 0ul)) {
continue;
} else {};
- var_count :=
- ((!var_count) `Pulse.Lib.C.UInt32.add_wrap` (id #UInt32.t (Int.Cast.int32_to_uint32 1l)));
+ var_count := ((!var_count) `Pulse.Lib.C.UInt32.add_wrap` 1ul);
};
return (!var_count);
}
\ No newline at end of file
diff --git base/do_while/Func_find_limit.fst head/do_while/Func_find_limit.fst
index cba1cf5..f16dd12 100644
--- base/do_while/Func_find_limit.fst
+++ head/do_while/Func_find_limit.fst
@@ -20,7 +20,7 @@ divergent fn func_find_limit
let mut var_n = var_n;
let mut var_limit = var_limit;
let mut var_i : Typedef_uint32_t.ty_uint32_t;
- var_i := (id #UInt32.t (Int.Cast.int32_to_uint32 0l));
+ var_i := 0ul;
let mut var___do_cont_2 : bool;
var___do_cont_2 := true;
let mut var_first : bool;
@@ -37,7 +37,7 @@ divergent fn func_find_limit
if (((!var_i) = (!var_limit))) {
break;
} else {};
- var_i := ((!var_i) `Pulse.Lib.C.UInt32.add_wrap` (id #UInt32.t (Int.Cast.int32_to_uint32 1l)));
+ var_i := ((!var_i) `Pulse.Lib.C.UInt32.add_wrap` 1ul);
var_first := false;
var___do_cont_2 := ((!var_i) `UInt32.lt` (!var_n));
};
diff --git base/do_while/Func_nested_continue.fst head/do_while/Func_nested_continue.fst
index 04a0385..d779592 100644
--- base/do_while/Func_nested_continue.fst
+++ head/do_while/Func_nested_continue.fst
@@ -12,7 +12,7 @@ divergent fn func_nested_continue (var_n: Typedef_uint32_t.ty_uint32_t)
{
let mut var_n = var_n;
let mut var_i : Typedef_uint32_t.ty_uint32_t;
- var_i := (id #UInt32.t (Int.Cast.int32_to_uint32 0l));
+ var_i := 0ul;
let mut var___do_cont_4 : bool;
var___do_cont_4 := true;
let mut var_first : bool;
@@ -26,18 +26,17 @@ divergent fn func_nested_continue (var_n: Typedef_uint32_t.ty_uint32_t)
invariant (with_pure ((!var___do_cont_4) = ((!var_first) || ((!var_i) `UInt32.lt` (!var_n)))))
{
let mut var_j : Typedef_uint32_t.ty_uint32_t;
- var_j := (id #UInt32.t (Int.Cast.int32_to_uint32 0l));
- while (((!var_j) `UInt32.lt` (id #UInt32.t (Int.Cast.int32_to_uint32 3l))))
+ var_j := 0ul;
+ while (((!var_j) `UInt32.lt` 3ul))
invariant (live var_j)
invariant (with_pure ((id #int (UInt32.v (!var_j))) <= 3))
{
- var_j :=
- ((!var_j) `Pulse.Lib.C.UInt32.add_wrap` (id #UInt32.t (Int.Cast.int32_to_uint32 1l)));
- if (((!var_j) = (id #UInt32.t (Int.Cast.int32_to_uint32 2l)))) {
+ var_j := ((!var_j) `Pulse.Lib.C.UInt32.add_wrap` 1ul);
+ if (((!var_j) = 2ul)) {
continue;
} else {};
};
- var_i := ((!var_i) `Pulse.Lib.C.UInt32.add_wrap` (id #UInt32.t (Int.Cast.int32_to_uint32 1l)));
+ var_i := ((!var_i) `Pulse.Lib.C.UInt32.add_wrap` 1ul);
var_first := false;
var___do_cont_4 := ((!var_i) `UInt32.lt` (!var_n));
};
diff --git base/do_while/Func_run_once.fst head/do_while/Func_run_once.fst
index 3cb327b..4127008 100644
--- base/do_while/Func_run_once.fst
+++ head/do_while/Func_run_once.fst
@@ -12,7 +12,7 @@ divergent fn func_run_once (var_x: Typedef_uint32_t.ty_uint32_t)
{
let mut var_x = var_x;
let mut var_r : Typedef_uint32_t.ty_uint32_t;
- var_r := (id #UInt32.t (Int.Cast.int32_to_uint32 0l));
+ var_r := 0ul;
let mut var___do_cont_1 : bool;
var___do_cont_1 := true;
let mut var___do_first_0 : bool;
diff --git base/do_while/Func_simple_do.fst head/do_while/Func_simple_do.fst
index 1b37d0b..f788051 100644
--- base/do_while/Func_simple_do.fst
+++ head/do_while/Func_simple_do.fst
@@ -12,7 +12,7 @@ divergent fn func_simple_do (var_n: Typedef_uint32_t.ty_uint32_t)
{
let mut var_n = var_n;
let mut var_i : Typedef_uint32_t.ty_uint32_t;
- var_i := (id #UInt32.t (Int.Cast.int32_to_uint32 0l));
+ var_i := 0ul;
let mut var___do_cont_0 : bool;
var___do_cont_0 := true;
let mut var_first : bool;
@@ -25,7 +25,7 @@ divergent fn func_simple_do (var_n: Typedef_uint32_t.ty_uint32_t)
invariant (live var___do_cont_0)
invariant (with_pure ((!var___do_cont_0) = ((!var_first) || ((!var_i) `UInt32.lt` (!var_n)))))
{
- var_i := ((!var_i) `Pulse.Lib.C.UInt32.add_wrap` (id #UInt32.t (Int.Cast.int32_to_uint32 1l)));
+ var_i := ((!var_i) `Pulse.Lib.C.UInt32.add_wrap` 1ul);
var_first := false;
var___do_cont_0 := ((!var_i) `UInt32.lt` (!var_n));
};
diff --git base/dpe/Func_authenticate_l0_image.fst head/dpe/Func_authenticate_l0_image.fst
index dc62cbe..c85424d 100644
--- base/dpe/Func_authenticate_l0_image.fst
+++ head/dpe/Func_authenticate_l0_image.fst
@@ -23,7 +23,7 @@ divergent fn func_authenticate_l0_image
defer (array_pts_to_uninit' var_scratch) { stack_free_array _ };
let mut var_scratch = var_scratch;
(Func_hacl_hash.func_hacl_hash
- (id #UInt8.t (Int.Cast.int32_to_uint8 0l))
+ 0uy
(!(Struct__engine_record_t.struct__engine_record_t__get_l0_binary_size (!var_record)))
(!(Struct__engine_record_t.struct__engine_record_t__get_l0_binary (!var_record)))
(!var_scratch));
diff --git base/dpe/Func_compute_cdi.fst head/dpe/Func_compute_cdi.fst
index a1b0b4e..9d5d89c 100644
--- base/dpe/Func_compute_cdi.fst
+++ head/dpe/Func_compute_cdi.fst
@@ -28,21 +28,11 @@ divergent fn func_compute_cdi
let var_l0_digest = (stack_alloc_array #Typedef_uint8_t.ty_uint8_t 64sz);
defer (array_pts_to_uninit' var_l0_digest) { stack_free_array _ };
let mut var_l0_digest = var_l0_digest;
+ (Func_hacl_hash.func_hacl_hash 0uy 32sz (!var_uds) (!var_uds_digest));
(Func_hacl_hash.func_hacl_hash
- (id #UInt8.t (Int.Cast.int32_to_uint8 0l))
- 32sz
- (!var_uds)
- (!var_uds_digest));
- (Func_hacl_hash.func_hacl_hash
- (id #UInt8.t (Int.Cast.int32_to_uint8 0l))
+ 0uy
(!(Struct__engine_record_t.struct__engine_record_t__get_l0_binary_size (!var_record)))
(!(Struct__engine_record_t.struct__engine_record_t__get_l0_binary (!var_record)))
(!var_l0_digest));
- (Func_hacl_hmac.func_hacl_hmac
- (id #UInt8.t (Int.Cast.int32_to_uint8 0l))
- (!var_cdi)
- (!var_uds_digest)
- 64sz
- (!var_l0_digest)
- 64sz);
+ (Func_hacl_hmac.func_hacl_hmac 0uy (!var_cdi) (!var_uds_digest) 64sz (!var_l0_digest) 64sz);
}
\ No newline at end of file
diff --git base/dpe/Func_init_engine_context.fst head/dpe/Func_init_engine_context.fst
index e6ab3a6..6ae065e 100644
--- base/dpe/Func_init_engine_context.fst
+++ head/dpe/Func_init_engine_context.fst
@@ -18,18 +18,13 @@ divergent fn func_init_engine_context (var_uds: Typedef_uds_array.ty_uds_array)
{
let mut var_uds = var_uds;
let mut var_uds_buf : (array Typedef_uint8_t.ty_uint8_t);
- var_uds_buf :=
- (Pulse.Lib.C.Array.alloc_array
- #Typedef_uint8_t.ty_uint8_t
- (SizeT.uint_to_t (UInt64.v (id #UInt64.t (Int.Cast.int32_to_uint64 32l)))));
+ var_uds_buf := (Pulse.Lib.C.Array.alloc_array #Typedef_uint8_t.ty_uint8_t 32sz);
(Func_memcpy_.func_memcpy_ 32sz (!var_uds) (!var_uds_buf));
let mut var_ctx : (ref Typedef_context_t.ty_context_t);
var_ctx := (Pulse.Lib.C.Ref.alloc_ref #Typedef_context_t.ty_context_t ());
(!var_ctx) :=
{
- Struct_context_t_anon_1.struct_context_t_anon_1__tag=(id
- #UInt8.t
- (Int.Cast.int32_to_uint8 0l));
+ Struct_context_t_anon_1.struct_context_t_anon_1__tag=0uy;
Struct_context_t_anon_1.struct_context_t_anon_1__payload=(Union__u_context_t.Field__u_context_t__uds
(!var_uds_buf));
};
diff --git base/dpe/Func_init_l0_context.fst head/dpe/Func_init_l0_context.fst
index 0821b35..f8c984e 100644
--- base/dpe/Func_init_l0_context.fst
+++ head/dpe/Func_init_l0_context.fst
@@ -27,10 +27,7 @@ divergent fn func_init_l0_context
let mut var_ctx = var_ctx;
let mut var_cdi = var_cdi;
let mut var_cdi_buf : (array Typedef_uint8_t.ty_uint8_t);
- var_cdi_buf :=
- (Pulse.Lib.C.Array.alloc_array
- #Typedef_uint8_t.ty_uint8_t
- (SizeT.uint_to_t (UInt64.v (id #UInt64.t (Int.Cast.int32_to_uint64 64l)))));
+ var_cdi_buf := (Pulse.Lib.C.Array.alloc_array #Typedef_uint8_t.ty_uint8_t 64sz);
(Func_memcpy_.func_memcpy_ 64sz (!var_cdi) (!var_cdi_buf));
DPE_predicates.elim_context_full_pred_uds (!(!var_ctx));
let mut var_uds_buf : (array Typedef_uint8_t.ty_uint8_t);
@@ -38,8 +35,7 @@ divergent fn func_init_l0_context
(!(Union__u_context_t.union__u_context_t__get_uds
(Struct_context_t_anon_1.struct_context_t_anon_1__get_payload (!var_ctx))));
(Pulse.Lib.C.Array.free_array (!var_uds_buf));
- (Struct_context_t_anon_1.struct_context_t_anon_1__get_tag (!var_ctx)) :=
- (id #UInt8.t (Int.Cast.int32_to_uint8 1l));
+ (Struct_context_t_anon_1.struct_context_t_anon_1__get_tag (!var_ctx)) := 1uy;
(Struct_context_t_anon_1.struct_context_t_anon_1__get_payload (!var_ctx)) :=
(Union__u_context_t.Field__u_context_t__cdi (!var_cdi_buf));
DPE_predicates.intro_context_full_pred_cdi (!(!var_ctx));
diff --git base/dpe/Func_mk_l0_context.fst head/dpe/Func_mk_l0_context.fst
index d6da3dd..29e0943 100644
--- base/dpe/Func_mk_l0_context.fst
+++ head/dpe/Func_mk_l0_context.fst
@@ -37,8 +37,7 @@ divergent fn func_mk_l0_context
(!(Union__u_context_t.union__u_context_t__get_uds
(Struct_context_t_anon_1.struct_context_t_anon_1__get_payload (!var_ctx))));
(Pulse.Lib.C.Array.free_array (!var_uds_buf));
- (Struct_context_t_anon_1.struct_context_t_anon_1__get_tag (!var_ctx)) :=
- (id #UInt8.t (Int.Cast.int32_to_uint8 1l));
+ (Struct_context_t_anon_1.struct_context_t_anon_1__get_tag (!var_ctx)) := 1uy;
(Struct_context_t_anon_1.struct_context_t_anon_1__get_payload (!var_ctx)) :=
(Union__u_context_t.Field__u_context_t__cdi (!var_cdi));
DPE_predicates.intro_context_full_pred_cdi (!(!var_ctx));
diff --git base/enum_constant_in_contract/Func_classify.fst head/enum_constant_in_contract/Func_classify.fst
index f42812f..02fdda9 100644
--- base/enum_constant_in_contract/Func_classify.fst
+++ head/enum_constant_in_contract/Func_classify.fst
@@ -22,7 +22,7 @@ divergent fn func_classify
let mut var_raw = var_raw;
let mut var_out = var_out;
if ((3l `Int32.lte` (id #Int32.t (Int.Cast.uint8_to_int32 (!var_raw))))) {
- (!var_out) := (id #UInt32.t (Int.Cast.int32_to_uint32 0l));
+ (!var_out) := 0ul;
} else {
(!var_out) := (id #UInt32.t (Int.Cast.uint8_to_uint32 (!var_raw)));
};
diff --git base/enum_constant_in_contract/Func_next_color.fst head/enum_constant_in_contract/Func_next_color.fst
index 5c3af5f..a01fa7b 100644
--- base/enum_constant_in_contract/Func_next_color.fst
+++ head/enum_constant_in_contract/Func_next_color.fst
@@ -18,11 +18,10 @@ divergent fn func_next_color (var_c: Typedef_COLOR.ty_color)
{
let mut var_c = var_c;
let mut var_result : Typedef_COLOR.ty_color;
- if (((!var_c) = (id #UInt32.t (Int.Cast.int32_to_uint32 2l)))) {
- var_result := (id #UInt32.t (Int.Cast.int32_to_uint32 0l));
+ if (((!var_c) = 2ul)) {
+ var_result := 0ul;
} else {
- var_result :=
- ((!var_c) `Pulse.Lib.C.UInt32.add_wrap` (id #UInt32.t (Int.Cast.int32_to_uint32 1l)));
+ var_result := ((!var_c) `Pulse.Lib.C.UInt32.add_wrap` 1ul);
};
return (!var_result);
}
\ No newline at end of file
diff --git base/extern_globals/Func_read_p_to_d_early_addressed.fst head/extern_globals/Func_read_p_to_d_early_addressed.fst
index 5296cbb..1290cb0 100644
--- base/extern_globals/Func_read_p_to_d_early_addressed.fst
+++ head/extern_globals/Func_read_p_to_d_early_addressed.fst
@@ -15,8 +15,8 @@ divergent fn func_read_p_to_d_early_addressed ()
var_v := (!(!var_pp));
drop_ (exists* q. pts_to Global_p_to_d_early_addressed.addr_var_p_to_d_early_addressed #q _);
if ((Pulse.Lib.Reference.is_null (!var_v))) {
- return (id #UInt32.t (Int.Cast.int32_to_uint32 1l));
+ return 1ul;
} else {
- return (id #UInt32.t (Int.Cast.int32_to_uint32 0l));
+ return 0ul;
};
}
\ No newline at end of file
diff --git base/extern_globals/Func_read_p_to_e_addressed.fst head/extern_globals/Func_read_p_to_e_addressed.fst
index 446d8f1..aab391d 100644
--- base/extern_globals/Func_read_p_to_e_addressed.fst
+++ head/extern_globals/Func_read_p_to_e_addressed.fst
@@ -15,8 +15,8 @@ divergent fn func_read_p_to_e_addressed ()
var_v := (!(!var_pp));
drop_ (exists* q. pts_to Global_p_to_e_addressed.addr_var_p_to_e_addressed #q _);
if ((Pulse.Lib.Reference.is_null (!var_v))) {
- return (id #UInt32.t (Int.Cast.int32_to_uint32 1l));
+ return 1ul;
} else {
- return (id #UInt32.t (Int.Cast.int32_to_uint32 0l));
+ return 0ul;
};
}
\ No newline at end of file
diff --git base/extern_globals/Global_d_early_addressed.fst head/extern_globals/Global_d_early_addressed.fst
index b1cc21d..ab9d72f 100644
--- base/extern_globals/Global_d_early_addressed.fst
+++ head/extern_globals/Global_d_early_addressed.fst
@@ -3,8 +3,7 @@ open Pulse
open Pulse.Lib.C
#lang-pulse
-let var_d_early_addressed : Typedef_uint32_t.ty_uint32_t =
- (id #UInt32.t (Int.Cast.int32_to_uint32 8l))
+let var_d_early_addressed : Typedef_uint32_t.ty_uint32_t = 8ul
assume val addr_var_d_early_addressed : (ref Typedef_uint32_t.ty_uint32_t)
assume val addr_var_d_early_addressed_not_null : squash (~(Pulse.Lib.Reference.is_null addr_var_d_early_addressed))
assume val acquire_var_d_early_addressed :
diff --git base/extern_globals/Global_d_early_const.fst head/extern_globals/Global_d_early_const.fst
index 5ca268e..aae19fc 100644
--- base/extern_globals/Global_d_early_const.fst
+++ head/extern_globals/Global_d_early_const.fst
@@ -3,7 +3,7 @@ open Pulse
open Pulse.Lib.C
#lang-pulse
-let var_d_early_const : Typedef_uint32_t.ty_uint32_t = (id #UInt32.t (Int.Cast.int32_to_uint32 5l))
+let var_d_early_const : Typedef_uint32_t.ty_uint32_t = 5ul
assume val addr_var_d_early_const : (ref Typedef_uint32_t.ty_uint32_t)
assume val addr_var_d_early_const_not_null : squash (~(Pulse.Lib.Reference.is_null addr_var_d_early_const))
assume val acquire_var_d_early_const :
diff --git base/extern_globals/Global_d_early_pure.fst head/extern_globals/Global_d_early_pure.fst
index 095aadd..08b9d44 100644
--- base/extern_globals/Global_d_early_pure.fst
+++ head/extern_globals/Global_d_early_pure.fst
@@ -3,7 +3,7 @@ open Pulse
open Pulse.Lib.C
#lang-pulse
-let var_d_early_pure : Typedef_uint32_t.ty_uint32_t = (id #UInt32.t (Int.Cast.int32_to_uint32 7l))
+let var_d_early_pure : Typedef_uint32_t.ty_uint32_t = 7ul
assume val addr_var_d_early_pure : (ref Typedef_uint32_t.ty_uint32_t)
assume val addr_var_d_early_pure_not_null : squash (~(Pulse.Lib.Reference.is_null addr_var_d_early_pure))
assume val acquire_var_d_early_pure :
diff --git base/extern_globals/Global_d_late_const.fst head/extern_globals/Global_d_late_const.fst
index 240bb23..edda809 100644
--- base/extern_globals/Global_d_late_const.fst
+++ head/extern_globals/Global_d_late_const.fst
@@ -3,7 +3,7 @@ open Pulse
open Pulse.Lib.C
#lang-pulse
-let var_d_late_const : Typedef_uint32_t.ty_uint32_t = (id #UInt32.t (Int.Cast.int32_to_uint32 6l))
+let var_d_late_const : Typedef_uint32_t.ty_uint32_t = 6ul
assume val addr_var_d_late_const : (ref Typedef_uint32_t.ty_uint32_t)
assume val addr_var_d_late_const_not_null : squash (~(Pulse.Lib.Reference.is_null addr_var_d_late_const))
assume val acquire_var_d_late_const :
diff --git base/for_loop/Func_count_skip.fst head/for_loop/Func_count_skip.fst
index c128f46..b85dac6 100644
--- base/for_loop/Func_count_skip.fst
+++ head/for_loop/Func_count_skip.fst
@@ -16,22 +16,20 @@ divergent fn func_count_skip
let mut var_n = var_n;
let mut var_skip = var_skip;
let mut var_count : Typedef_uint32_t.ty_uint32_t;
- var_count := (id #UInt32.t (Int.Cast.int32_to_uint32 0l));
+ var_count := 0ul;
let mut var_i : Typedef_uint32_t.ty_uint32_t;
- var_i := (id #UInt32.t (Int.Cast.int32_to_uint32 0l));
+ var_i := 0ul;
while (((!var_i) `UInt32.lt` (!var_n)))
invariant ((live var_i) ** (live var_count))
invariant (with_pure ((!var_i) `UInt32.lte` (!var_n)))
invariant (with_pure ((!var_count) `UInt32.lte` (!var_i)))
{
if (((!var_i) = (!var_skip))) {
- var_i :=
- ((!var_i) `Pulse.Lib.C.UInt32.add_wrap` (id #UInt32.t (Int.Cast.int32_to_uint32 1l)));
+ var_i := ((!var_i) `Pulse.Lib.C.UInt32.add_wrap` 1ul);
continue;
} else {};
- var_count :=
- ((!var_count) `Pulse.Lib.C.UInt32.add_wrap` (id #UInt32.t (Int.Cast.int32_to_uint32 1l)));
- var_i := ((!var_i) `Pulse.Lib.C.UInt32.add_wrap` (id #UInt32.t (Int.Cast.int32_to_uint32 1l)));
+ var_count := ((!var_count) `Pulse.Lib.C.UInt32.add_wrap` 1ul);
+ var_i := ((!var_i) `Pulse.Lib.C.UInt32.add_wrap` 1ul);
};
return (!var_count);
}
\ No newline at end of file
diff --git base/for_loop/Func_multiply_for.fst head/for_loop/Func_multiply_for.fst
index 218eeb8..c814c6e 100644
--- base/for_loop/Func_multiply_for.fst
+++ head/for_loop/Func_multiply_for.fst
@@ -21,9 +21,9 @@ divergent fn func_multiply_for
let mut var_x = var_x;
let mut var_y = var_y;
let mut var_acc : Typedef_uint32_t.ty_uint32_t;
- var_acc := (id #UInt32.t (Int.Cast.int32_to_uint32 0l));
+ var_acc := 0ul;
let mut var_ctr : Typedef_uint32_t.ty_uint32_t;
- var_ctr := (id #UInt32.t (Int.Cast.int32_to_uint32 0l));
+ var_ctr := 0ul;
while (((!var_ctr) `UInt32.lt` (!var_x)))
invariant ((live var_ctr) ** (live var_acc))
invariant (with_pure
@@ -31,8 +31,7 @@ divergent fn func_multiply_for
((!var_acc) = ((!var_ctr) `Pulse.Lib.C.UInt32.mul_wrap` (!var_y)))))
{
var_acc := ((!var_acc) `Pulse.Lib.C.UInt32.add_wrap` (!var_y));
- var_ctr :=
- ((!var_ctr) `Pulse.Lib.C.UInt32.add_wrap` (id #UInt32.t (Int.Cast.int32_to_uint32 1l)));
+ var_ctr := ((!var_ctr) `Pulse.Lib.C.UInt32.add_wrap` 1ul);
};
return (!var_acc);
}
\ No newline at end of file
diff --git base/func_pointer/Func_mk_itemx.fst head/func_pointer/Func_mk_itemx.fst
index 87610a9..107216f 100644
--- base/func_pointer/Func_mk_itemx.fst
+++ head/func_pointer/Func_mk_itemx.fst
@@ -17,7 +17,7 @@ divergent fn func_mk_itemx ()
(Pulse.Lib.C.FuncPtr.pre_of Funcptr_destroy_impl.func_destroy_impl__fp)
(Pulse.Lib.C.FuncPtr.post_of Funcptr_destroy_impl.func_destroy_impl__fp)
Funcptr_destroy_impl.func_destroy_impl__fp));
- (Struct_itemx.struct_itemx__get_n (!var_it)) := (id #UInt32.t (Int.Cast.int32_to_uint32 0l));
+ (Struct_itemx.struct_itemx__get_n (!var_it)) := 0ul;
Pulse.Lib.C.FuncPtr.of_fn_div_valid _ _ Funcptr_destroy_impl.func_destroy_impl__fp;
return (!var_it);
}
\ No newline at end of file
diff --git base/func_pointer/Func_use_arity3.fst head/func_pointer/Func_use_arity3.fst
index 225b4d0..4c86b09 100644
--- base/func_pointer/Func_use_arity3.fst
+++ head/func_pointer/Func_use_arity3.fst
@@ -18,14 +18,7 @@ divergent fn func_use_arity3 ()
(Pulse.Lib.C.FuncPtr.post_of Funcptr_combine.func_combine__fp)
Funcptr_combine.func_combine__fp));
Pulse.Lib.C.FuncPtr.of_fn_div_valid _ _ Funcptr_combine.func_combine__fp;
- let return_1 = ((Pulse.Lib.C.FuncPtr.call_div
- _
- _
- (!var_fp3)
- ((id #UInt8.t (Int.Cast.int32_to_uint8 5l)), (id
- #UInt32.t
- (Int.Cast.int32_to_uint32 10l)), 3l)
- (hide ())));
+ let return_1 = ((Pulse.Lib.C.FuncPtr.call_div _ _ (!var_fp3) (5uy, 10ul, 3l) (hide ())));
Pulse.Lib.C.FuncPtr.drop_is_valid _ _ _;
return return_1;
}
\ No newline at end of file
diff --git base/func_pointer/Func_use_arity3_amp.fst head/func_pointer/Func_use_arity3_amp.fst
index 3b3f061..545ab59 100644
--- base/func_pointer/Func_use_arity3_amp.fst
+++ head/func_pointer/Func_use_arity3_amp.fst
@@ -18,14 +18,7 @@ divergent fn func_use_arity3_amp ()
(Pulse.Lib.C.FuncPtr.post_of Funcptr_combine.func_combine__fp)
Funcptr_combine.func_combine__fp));
Pulse.Lib.C.FuncPtr.of_fn_div_valid _ _ Funcptr_combine.func_combine__fp;
- let return_1 = ((Pulse.Lib.C.FuncPtr.call_div
- _
- _
- (!var_fp3)
- ((id #UInt8.t (Int.Cast.int32_to_uint8 5l)), (id
- #UInt32.t
- (Int.Cast.int32_to_uint32 10l)), 3l)
- (hide ())));
+ let return_1 = ((Pulse.Lib.C.FuncPtr.call_div _ _ (!var_fp3) (5uy, 10ul, 3l) (hide ())));
Pulse.Lib.C.FuncPtr.drop_is_valid _ _ _;
return return_1;
}
\ No newline at end of file
diff --git base/generic_selection/Func_store_selected_wide.fst head/generic_selection/Func_store_selected_wide.fst
index 69098d0..f6f9eb0 100644
--- base/generic_selection/Func_store_selected_wide.fst
+++ head/generic_selection/Func_store_selected_wide.fst
@@ -17,11 +17,9 @@ divergent fn func_store_selected_wide
((Pulse.Lib.Reference.pts_to var_slots #1.0R val_slots_0) **
(Struct_generic_slots.struct_generic_slots__pred (!var_slots) 1.0R))
ensures ((Typedef_uint64_t.ty_uint64_t__pred var_selector 1.0R))
- ensures
- (with_pure
- ((!(Struct_generic_slots.struct_generic_slots__get_wide var_slots)) = (UInt64.uint_to_t 84)))
+ ensures (with_pure ((!(Struct_generic_slots.struct_generic_slots__get_wide var_slots)) = 84uL))
{
let mut var_slots = var_slots;
let mut var_selector = var_selector;
- (Struct_generic_slots.struct_generic_slots__get_wide (!var_slots)) := (UInt64.uint_to_t 84);
+ (Struct_generic_slots.struct_generic_slots__get_wide (!var_slots)) := 84uL;
}
\ No newline at end of file
diff --git base/generic_selection/Func_store_selected_wide.fsti head/generic_selection/Func_store_selected_wide.fsti
index 6c1147f..45b874e 100644
--- base/generic_selection/Func_store_selected_wide.fsti
+++ head/generic_selection/Func_store_selected_wide.fsti
@@ -17,6 +17,4 @@ ensures
((Pulse.Lib.Reference.pts_to var_slots #1.0R val_slots_0) **
(Struct_generic_slots.struct_generic_slots__pred (!var_slots) 1.0R))
ensures ((Typedef_uint64_t.ty_uint64_t__pred var_selector 1.0R))
-ensures
- (with_pure
- ((!(Struct_generic_slots.struct_generic_slots__get_wide var_slots)) = (UInt64.uint_to_t 84)))
\ No newline at end of file
+ensures (with_pure ((!(Struct_generic_slots.struct_generic_slots__get_wide var_slots)) = 84uL))
\ No newline at end of file
diff --git base/ghost_stmt_for_clause/Func_assert_in_for_clause.fst head/ghost_stmt_for_clause/Func_assert_in_for_clause.fst
index eca2c62..1fd88bd 100644
--- base/ghost_stmt_for_clause/Func_assert_in_for_clause.fst
+++ head/ghost_stmt_for_clause/Func_assert_in_for_clause.fst
@@ -21,10 +21,10 @@ divergent fn func_assert_in_for_clause
let mut var_x = var_x;
let mut var_y = var_y;
let mut var_acc : Typedef_uint32_t.ty_uint32_t;
- var_acc := (id #UInt32.t (Int.Cast.int32_to_uint32 0l));
+ var_acc := 0ul;
let mut var_ctr : Typedef_uint32_t.ty_uint32_t;
assert (with_pure ((id #int (UInt32.v (!var_acc))) = 0));
- var_ctr := (id #UInt32.t (Int.Cast.int32_to_uint32 0l));
+ var_ctr := 0ul;
while (((!var_ctr) `UInt32.lt` (!var_x)))
invariant ((live var_ctr) ** (live var_acc))
invariant (with_pure
@@ -33,8 +33,7 @@ divergent fn func_assert_in_for_clause
{
var_acc := ((!var_acc) `Pulse.Lib.C.UInt32.add_wrap` (!var_y));
assert (with_pure ((!var_ctr) `UInt32.lt` (!var_x)));
- var_ctr :=
- ((!var_ctr) `Pulse.Lib.C.UInt32.add_wrap` (id #UInt32.t (Int.Cast.int32_to_uint32 1l)));
+ var_ctr := ((!var_ctr) `Pulse.Lib.C.UInt32.add_wrap` 1ul);
};
return (!var_acc);
}
\ No newline at end of file
diff --git base/ghost_stmt_for_clause/Func_ghost_in_for_clause.fst head/ghost_stmt_for_clause/Func_ghost_in_for_clause.fst
index e83a6e5..db91c6a 100644
--- base/ghost_stmt_for_clause/Func_ghost_in_for_clause.fst
+++ head/ghost_stmt_for_clause/Func_ghost_in_for_clause.fst
@@ -21,11 +21,11 @@ divergent fn func_ghost_in_for_clause
let mut var_x = var_x;
let mut var_y = var_y;
let mut var_acc : Typedef_uint32_t.ty_uint32_t;
- var_acc := (id #UInt32.t (Int.Cast.int32_to_uint32 0l));
+ var_acc := 0ul;
let mut var_ctr : Typedef_uint32_t.ty_uint32_t;
assert pure (0 == 0);
assert pure (0 == 0);
- var_ctr := (id #UInt32.t (Int.Cast.int32_to_uint32 0l));
+ var_ctr := 0ul;
while (((!var_ctr) `UInt32.lt` (!var_x)))
invariant ((live var_ctr) ** (live var_acc))
invariant (with_pure
@@ -34,8 +34,7 @@ divergent fn func_ghost_in_for_clause
{
var_acc := ((!var_acc) `Pulse.Lib.C.UInt32.add_wrap` (!var_y));
assert pure (0 == 0);
- var_ctr :=
- ((!var_ctr) `Pulse.Lib.C.UInt32.add_wrap` (id #UInt32.t (Int.Cast.int32_to_uint32 1l)));
+ var_ctr := ((!var_ctr) `Pulse.Lib.C.UInt32.add_wrap` 1ul);
};
assert (with_pure ((!var_acc) = ((!var_x) `Pulse.Lib.C.UInt32.mul_wrap` (!var_y))));
return (!var_acc);
diff --git base/global_header_addr/Global_h_plain_const.fst head/global_header_addr/Global_h_plain_const.fst
index 7209ae5..fefd28a 100644
--- base/global_header_addr/Global_h_plain_const.fst
+++ head/global_header_addr/Global_h_plain_const.fst
@@ -3,7 +3,7 @@ open Pulse
open Pulse.Lib.C
#lang-pulse
-let var_h_plain_const : Typedef_uint32_t.ty_uint32_t = (id #UInt32.t (Int.Cast.int32_to_uint32 7l))
+let var_h_plain_const : Typedef_uint32_t.ty_uint32_t = 7ul
assume val addr_var_h_plain_const : (ref Typedef_uint32_t.ty_uint32_t)
assume val addr_var_h_plain_const_not_null : squash (~(Pulse.Lib.Reference.is_null addr_var_h_plain_const))
assume val acquire_var_h_plain_const :
diff --git base/global_header_addr/Global_h_static_const.fst head/global_header_addr/Global_h_static_const.fst
index 0de0e26..8601961 100644
--- base/global_header_addr/Global_h_static_const.fst
+++ head/global_header_addr/Global_h_static_const.fst
@@ -3,7 +3,7 @@ open Pulse
open Pulse.Lib.C
#lang-pulse
-let var_h_static_const : Typedef_uint32_t.ty_uint32_t = (id #UInt32.t (Int.Cast.int32_to_uint32 5l))
+let var_h_static_const : Typedef_uint32_t.ty_uint32_t = 5ul
assume val addr_var_h_static_const : (ref Typedef_uint32_t.ty_uint32_t)
assume val addr_var_h_static_const_not_null : squash (~(Pulse.Lib.Reference.is_null addr_var_h_static_const))
assume val acquire_var_h_static_const :
diff --git base/global_header_addr/Global_m_plain_const.fst head/global_header_addr/Global_m_plain_const.fst
index ec62158..72b560a 100644
--- base/global_header_addr/Global_m_plain_const.fst
+++ head/global_header_addr/Global_m_plain_const.fst
@@ -3,7 +3,7 @@ open Pulse
open Pulse.Lib.C
#lang-pulse
-let var_m_plain_const : Typedef_uint32_t.ty_uint32_t = (id #UInt32.t (Int.Cast.int32_to_uint32 7l))
Diff truncated; see the links above for the full version. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Part of the upstreaming of
nswamy/pal-c-project-integration(PR07 of 35 PRs) — seePR_PLAN.mdon that branch for the whole plan and the dependency graph.Base:
main. Depends on nothing; reviewable on its own.Generated interfaces define fixed-width bit-pattern constants as casts from long
literals. On LP64 a high-bit long is a signed 64-bit value, and emitting the source
literal followed by
Int.Cast.int64_to_int32left F* with an out-of-range conversion.Adds a post-elaboration
normalize_castspass that recovers the mathematical value,preserves representable casts as explicit
Int.Castoperations, and rewrites onlyout-of-range ones to target-typed literals. The three follow-ups make emission agree
with it: one shared
machine_int_literaltable for expressions and patterns (theconstructor form is not interchangeable — its refinement needs SMT, and Pulse typechecks
candidate witnesses without it), and parentheses around negative literals, which F*
otherwise lexes as infix subtraction (
=-and:=-are single operators).Commits
Testing
Verified:
make rust lib,test/check-template.sh,cargo fmt --check,clang-format --dry-run --Werror, and F* verification oftest/integer_literal_casts,test/negative_literals.