Bump F* to nightly 2026-09-25 by gebner · Pull Request #327 · FStarLang/pal

gebner · 2026-09-25T15:11:28Z

Bumps the pinned F* nightly from 2026-09-15 to 2026-09-25.

The nightlies after FStarLang/FStar#4515 (_revise_primitive_effects) needed two fixes in PAL:

Pulse.Lib.C.Array.array_spec_upd_mask no longer verifies automatically. It now uses explicit Seq.lemma_index_upd1/upd2.
= against SizeT.v now infers the refined x:nat{SizeT.fits x} as the equality type, which broke arrayptrs and compare_elements (Regression: f () = (y <: _) infers the refinement from f's Pure postcondition, rejecting y FStar#4586). As a workaround, the emitter now produces reveal #nat (length_of x), and the docs are updated to match.

A third regression, in ghost_fnptr (FStarLang/FStar#4587), is fixed upstream as of the 2026-09-25 nightly.

make test -j8 passes locally with nightly-2026-09-25.

- Prove array_spec_upd_mask with explicit Seq.upd lemmas. - Emit `reveal #nat (length_of x)` so the equality type is not inferred as the refined `x:nat{SizeT.fits x}` (FStarLang/FStar#4586). Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

ghost_fnptr/call_across_shapes fails with this nightly due to FStarLang/FStar#4587. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Includes the fix for FStarLang/FStar#4587; all tests pass. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

github-actions · 2026-09-25T15:15:23Z

Generated F* output diff

Effect of this pull request on the F* code pal generates for the test suite (62dff7f → 638900f).

Summary

 {base => head}/array_deref/Func_deref_read.fst                         |  4 ++--
 {base => head}/array_deref/Func_deref_read.fsti                        |  4 ++--
 {base => head}/array_deref/Func_deref_write.fst                        |  4 ++--
 {base => head}/array_deref/Func_deref_write.fsti                       |  4 ++--
 {base => head}/array_ptr_arith/Func_post_decr.fst                      |  4 ++--
 {base => head}/array_ptr_arith/Func_post_decr.fsti                     |  4 ++--
 {base => head}/array_ptr_arith/Func_post_incr.fst                      |  4 ++--
 {base => head}/array_ptr_arith/Func_post_incr.fsti                     |  4 ++--
 {base => head}/array_ptr_arith/Func_pre_decr.fst                       |  4 ++--
 {base => head}/array_ptr_arith/Func_pre_decr.fsti                      |  4 ++--
 {base => head}/array_ptr_arith/Func_pre_incr.fst                       |  4 ++--
 {base => head}/array_ptr_arith/Func_pre_incr.fsti                      |  4 ++--
 {base => head}/array_test/Func_foo.fst                                 |  4 ++--
 {base => head}/array_test/Func_foo.fsti                                |  4 ++--
 {base => head}/array_test/Func_ptr_attr.fst                            |  4 ++--
 {base => head}/array_test/Func_ptr_attr.fsti                           |  4 ++--
 {base => head}/array_test/Func_struct_arr.fst                          |  9 ++++++---
 {base => head}/array_test/Func_struct_arr.fsti                         |  7 ++++---
 {base => head}/array_test/Func_tydef_array.fst                         |  4 ++--
 {base => head}/array_test/Func_tydef_array.fsti                        |  4 ++--
 {base => head}/array_test/Typedef_b32_struct.fst                       |  2 +-
 {base => head}/array_to_ref/Func_caller.fst                            |  2 +-
 {base => head}/array_to_ref/Func_caller.fsti                           |  2 +-
 {base => head}/array_to_ref/Func_caller_out.fst                        |  2 +-
 {base => head}/array_to_ref/Func_caller_out.fsti                       |  2 +-
 {base => head}/array_to_ref/Func_fill_first.fst                        |  2 +-
 {base => head}/array_to_ref/Func_fill_first.fsti                       |  2 +-
 {base => head}/array_typedef_pointer/Func_get_entry.fst                |  2 +-
 {base => head}/array_typedef_pointer/Func_get_entry.fsti               |  2 +-
 {base => head}/array_typedef_pointer/Func_read_first.fst               |  2 +-
 {base => head}/array_typedef_pointer/Func_read_first.fsti              |  2 +-
 {base => head}/array_update/Func_set_both.fst                          |  4 ++--
 {base => head}/array_update/Func_set_both.fsti                         |  4 ++--
 {base => head}/array_update/Func_set_elem_fields.fst                   |  5 +++--
 {base => head}/array_update/Func_set_elem_fields.fsti                  |  5 +++--
 {base => head}/array_update/Func_set_x.fst                             |  4 ++--
 {base => head}/array_update/Func_set_x.fsti                            |  4 ++--
 {base => head}/array_update/Func_set_x_alt.fst                         |  2 +-
 {base => head}/array_update/Func_set_x_alt.fsti                        |  2 +-
 {base => head}/array_update/Func_set_y.fst                             |  4 ++--
 {base => head}/array_update/Func_set_y.fsti                            |  4 ++--
 {base => head}/arrayptr_compare/Func_less.fst                          |  2 +-
 {base => head}/arrayptr_compare/Func_less.fsti                         |  2 +-
 {base => head}/arrayptr_diff/Func_same_object_diff.fst                 |  2 +-
 {base => head}/arrayptr_diff/Func_same_object_diff.fsti                |  2 +-
 {base => head}/arrayptr_ref/Func_assign_cell_address_to_ref.fst        |  2 +-
 {base => head}/arrayptr_ref/Func_assign_cell_address_to_ref.fsti       |  2 +-
 {base => head}/arrayptr_ref/Func_consume_returned_arrayptr_as_ref.fst  |  2 +-
 {base => head}/arrayptr_ref/Func_consume_returned_arrayptr_as_ref.fsti |  2 +-
 {base => head}/arrayptr_ref/Func_pass_arrayptr_as_ref.fst              |  2 +-
 {base => head}/arrayptr_ref/Func_pass_arrayptr_as_ref.fsti             |  2 +-
 {base => head}/arrayptrs/Func_use_binary_search.fst                    |  3 ++-
 {base => head}/arrayptrs/Func_use_binary_search.fsti                   |  2 +-
 {base => head}/arrayptrs/Func_write_via_ptr.fst                        |  4 ++--
 {base => head}/arrayptrs/Func_write_via_ptr.fsti                       |  4 ++--
 {base => head}/calloc_alloc_size/Func_test_calloc_count_mul_size.fst   |  2 +-
 {base => head}/calloc_alloc_size/Func_test_calloc_count_size_mul.fst   |  2 +-
 {base => head}/compare_elements/Func_compare_elems.fst                 |  8 ++++----
 {base => head}/compare_elements/Func_compare_elems.fsti                |  8 ++++----
 {base => head}/conditional_write/Func_caller.fst                       |  2 +-
 {base => head}/conditional_write/Func_caller.fsti                      |  2 +-
 {base => head}/default_test/Func_test_calloc_array.fst                 |  2 +-
 {base => head}/dpe/Func_compare.fst                                    |  4 ++--
 {base => head}/dpe/Func_compare.fsti                                   |  4 ++--
 {base => head}/dpe/Func_derive_child_from_context.fst                  |  2 +-
 {base => head}/dpe/Func_ed25519_verify.fst                             |  2 +-
 {base => head}/dpe/Func_hacl_hash.fst                                  |  2 +-
 {base => head}/dpe/Func_hacl_hmac.fst                                  |  4 ++--
 {base => head}/dpe/Func_memcpy_.fst                                    |  8 ++++----
 {base => head}/dpe/Func_memcpy_.fsti                                   |  8 ++++----
 {base => head}/dpe/Func_mk_l0_context.fst                              |  2 +-
 {base => head}/dpe/Typedef_dice_digest.fst                             |  2 +-
 {base => head}/dpe/Typedef_ed25519_key.fst                             |  2 +-
 {base => head}/dpe/Typedef_ed25519_sig.fst                             |  2 +-
 {base => head}/dpe/Typedef_engine_record_t.fst                         |  5 +++--
 {base => head}/dpe/Typedef_l1_context_t.fst                            |  4 ++--
 {base => head}/dpe/Typedef_uds_array.fst                               |  2 +-
 {base => head}/fnptr_spec/Func_use.fst                                 |  8 ++++----
 {base => head}/fnptr_spec/Func_use.fsti                                |  8 ++++----
 {base => head}/fnptr_spec/Func_use_byval.fst                           |  8 ++++----
 {base => head}/fnptr_spec/Func_use_byval.fsti                          |  8 ++++----
 {base => head}/fnptr_spec/Funcptr_use.fst                              |  9 +++++----
 {base => head}/fnptr_spec/Funcptr_use.fsti                             |  9 +++++----
 {base => head}/fnptr_spec/Funcptr_use_byval.fst                        |  8 ++++----
 {base => head}/fnptr_spec/Funcptr_use_byval.fsti                       |  8 ++++----
 {base => head}/global_mutable_array/Func_read_ext.fst                  |  5 +++--
 {base => head}/global_mutable_array/Func_read_ext.fsti                 |  5 +++--
 {base => head}/inline_array_aliasing/Func_read_first.fst               |  4 ++--
 {base => head}/inline_array_aliasing/Func_read_first.fsti              |  4 ++--
 {base => head}/letimpure/Typedef_hash.fst                              |  2 +-
 {base => head}/local_fn_decl/Func_local_decl.fst                       |  4 ++--
 {base => head}/local_fn_decl/Func_local_decl.fsti                      |  4 ++--
 {base => head}/malloc/Func_test_array_malloc_free.fst                  |  2 +-
 {base => head}/malloc_sizeof_expr/Func_array_alloc.fst                 |  2 +-
 {base => head}/malloc_sizeof_expr/Func_array_alloc_count_first.fst     |  2 +-
 {base => head}/malloc_sizeof_expr/Func_calloc_array.fst                |  2 +-
 {base => head}/memset/Func_zero_bytes.fst                              |  2 +-
 {base => head}/memset/Func_zero_bytes.fsti                           
... (summary truncated)

Full diff: full diff artifact

Diff

diff --git base/array_deref/Func_deref_read.fst head/array_deref/Func_deref_read.fst
index 69c752a..830f0c7 100644
--- base/array_deref/Func_deref_read.fst
+++ head/array_deref/Func_deref_read.fst
@@ -5,10 +5,10 @@ open Pulse.Lib.C
 
 divergent fn func_deref_read (var_p: (array Int32.t))
   requires exists* (val_p_0: (full_array_spec Int32.t)). ((array_pts_to_full var_p 1.0R val_p_0))
-  requires (with_pure (1 <= (reveal (length_of var_p))))
+  requires (with_pure (1 <= (reveal #nat (length_of var_p))))
   returns return_1 : Int32.t
   ensures exists* (val_p_0: (full_array_spec Int32.t)). ((array_pts_to_full var_p 1.0R val_p_0))
-  ensures (with_pure ((reveal (length_of var_p)) = (old (reveal (length_of var_p)))))
+  ensures (with_pure ((reveal #nat (length_of var_p)) = (old (reveal #nat (length_of var_p)))))
   ensures (with_pure (return_1 = ((array_read var_p 0sz))))
 {
   let mut var_p = var_p;
diff --git base/array_deref/Func_deref_read.fsti head/array_deref/Func_deref_read.fsti
index 6c10659..0402acc 100644
--- base/array_deref/Func_deref_read.fsti
+++ head/array_deref/Func_deref_read.fsti
@@ -5,8 +5,8 @@ open Pulse.Lib.C
 
 divergent fn func_deref_read (var_p: (array Int32.t))
 requires exists* (val_p_0: (full_array_spec Int32.t)). ((array_pts_to_full var_p 1.0R val_p_0))
-requires (with_pure (1 <= (reveal (length_of var_p))))
+requires (with_pure (1 <= (reveal #nat (length_of var_p))))
 returns return_1 : Int32.t
 ensures exists* (val_p_0: (full_array_spec Int32.t)). ((array_pts_to_full var_p 1.0R val_p_0))
-ensures (with_pure ((reveal (length_of var_p)) = (old (reveal (length_of var_p)))))
+ensures (with_pure ((reveal #nat (length_of var_p)) = (old (reveal #nat (length_of var_p)))))
 ensures (with_pure (return_1 = ((array_read var_p 0sz))))
\ No newline at end of file
diff --git base/array_deref/Func_deref_write.fst head/array_deref/Func_deref_write.fst
index e0d2494..7adb86d 100644
--- base/array_deref/Func_deref_write.fst
+++ head/array_deref/Func_deref_write.fst
@@ -5,10 +5,10 @@ open Pulse.Lib.C
 
 divergent fn func_deref_write (var_p: (array Int32.t)) (var_v: Int32.t)
   requires exists* (val_p_0: (full_array_spec Int32.t)). ((array_pts_to_full var_p 1.0R val_p_0))
-  requires (with_pure (1 <= (reveal (length_of var_p))))
+  requires (with_pure (1 <= (reveal #nat (length_of var_p))))
   returns return_1 : unit
   ensures exists* (val_p_0: (full_array_spec Int32.t)). ((array_pts_to_full var_p 1.0R val_p_0))
-  ensures (with_pure ((reveal (length_of var_p)) = (old (reveal (length_of var_p)))))
+  ensures (with_pure ((reveal #nat (length_of var_p)) = (old (reveal #nat (length_of var_p)))))
   ensures (with_pure (((array_read var_p 0sz)) = var_v))
 {
   let mut var_p = var_p;
diff --git base/array_deref/Func_deref_write.fsti head/array_deref/Func_deref_write.fsti
index d977130..4168491 100644
--- base/array_deref/Func_deref_write.fsti
+++ head/array_deref/Func_deref_write.fsti
@@ -5,8 +5,8 @@ open Pulse.Lib.C
 
 divergent fn func_deref_write (var_p: (array Int32.t)) (var_v: Int32.t)
 requires exists* (val_p_0: (full_array_spec Int32.t)). ((array_pts_to_full var_p 1.0R val_p_0))
-requires (with_pure (1 <= (reveal (length_of var_p))))
+requires (with_pure (1 <= (reveal #nat (length_of var_p))))
 returns return_1 : unit
 ensures exists* (val_p_0: (full_array_spec Int32.t)). ((array_pts_to_full var_p 1.0R val_p_0))
-ensures (with_pure ((reveal (length_of var_p)) = (old (reveal (length_of var_p)))))
+ensures (with_pure ((reveal #nat (length_of var_p)) = (old (reveal #nat (length_of var_p)))))
 ensures (with_pure (((array_read var_p 0sz)) = var_v))
\ No newline at end of file
diff --git base/array_ptr_arith/Func_post_decr.fst head/array_ptr_arith/Func_post_decr.fst
index fbb3433..9b02b8f 100644
--- base/array_ptr_arith/Func_post_decr.fst
+++ head/array_ptr_arith/Func_post_decr.fst
@@ -7,13 +7,13 @@ divergent fn func_post_decr (var_a: (array Typedef_int32_t.ty_int32_t))
   requires
     exists* (val_a_0: (full_array_spec Typedef_int32_t.ty_int32_t)).
     ((array_pts_to_full var_a 1.0R val_a_0))
-  requires (with_pure ((reveal (length_of var_a)) = 4))
+  requires (with_pure ((reveal #nat (length_of var_a)) = 4))
   returns return_1 : Typedef_int32_t.ty_int32_t
   ensures
     exists* (val_a_0: (full_array_spec Typedef_int32_t.ty_int32_t)).
     ((array_pts_to_full var_a 1.0R val_a_0))
   ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
-  ensures (with_pure ((reveal (length_of var_a)) = (old (reveal (length_of var_a)))))
+  ensures (with_pure ((reveal #nat (length_of var_a)) = (old (reveal #nat (length_of var_a)))))
   ensures (with_pure ((id #int (Int32.v return_1)) = 1))
 {
   let mut var_a = var_a;
diff --git base/array_ptr_arith/Func_post_decr.fsti head/array_ptr_arith/Func_post_decr.fsti
index dc3a763..1a0a138 100644
--- base/array_ptr_arith/Func_post_decr.fsti
+++ head/array_ptr_arith/Func_post_decr.fsti
@@ -7,11 +7,11 @@ divergent fn func_post_decr (var_a: (array Typedef_int32_t.ty_int32_t))
 requires
   exists* (val_a_0: (full_array_spec Typedef_int32_t.ty_int32_t)).
   ((array_pts_to_full var_a 1.0R val_a_0))
-requires (with_pure ((reveal (length_of var_a)) = 4))
+requires (with_pure ((reveal #nat (length_of var_a)) = 4))
 returns return_1 : Typedef_int32_t.ty_int32_t
 ensures
   exists* (val_a_0: (full_array_spec Typedef_int32_t.ty_int32_t)).
   ((array_pts_to_full var_a 1.0R val_a_0))
 ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
-ensures (with_pure ((reveal (length_of var_a)) = (old (reveal (length_of var_a)))))
+ensures (with_pure ((reveal #nat (length_of var_a)) = (old (reveal #nat (length_of var_a)))))
 ensures (with_pure ((id #int (Int32.v return_1)) = 1))
\ No newline at end of file
diff --git base/array_ptr_arith/Func_post_incr.fst head/array_ptr_arith/Func_post_incr.fst
index 9618a8f..ce2ecb5 100644
--- base/array_ptr_arith/Func_post_incr.fst
+++ head/array_ptr_arith/Func_post_incr.fst
@@ -7,13 +7,13 @@ divergent fn func_post_incr (var_a: (array Typedef_int32_t.ty_int32_t))
   requires
     exists* (val_a_0: (full_array_spec Typedef_int32_t.ty_int32_t)).
     ((array_pts_to_full var_a 1.0R val_a_0))
-  requires (with_pure ((reveal (length_of var_a)) = 4))
+  requires (with_pure ((reveal #nat (length_of var_a)) = 4))
   returns return_1 : Typedef_int32_t.ty_int32_t
   ensures
     exists* (val_a_0: (full_array_spec Typedef_int32_t.ty_int32_t)).
     ((array_pts_to_full var_a 1.0R val_a_0))
   ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
-  ensures (with_pure ((reveal (length_of var_a)) = (old (reveal (length_of var_a)))))
+  ensures (with_pure ((reveal #nat (length_of var_a)) = (old (reveal #nat (length_of var_a)))))
   ensures (with_pure ((id #int (Int32.v return_1)) = 1))
 {
   let mut var_a = var_a;
diff --git base/array_ptr_arith/Func_post_incr.fsti head/array_ptr_arith/Func_post_incr.fsti
index 6b8ae87..f1d4b98 100644
--- base/array_ptr_arith/Func_post_incr.fsti
+++ head/array_ptr_arith/Func_post_incr.fsti
@@ -7,11 +7,11 @@ divergent fn func_post_incr (var_a: (array Typedef_int32_t.ty_int32_t))
 requires
   exists* (val_a_0: (full_array_spec Typedef_int32_t.ty_int32_t)).
   ((array_pts_to_full var_a 1.0R val_a_0))
-requires (with_pure ((reveal (length_of var_a)) = 4))
+requires (with_pure ((reveal #nat (length_of var_a)) = 4))
 returns return_1 : Typedef_int32_t.ty_int32_t
 ensures
   exists* (val_a_0: (full_array_spec Typedef_int32_t.ty_int32_t)).
   ((array_pts_to_full var_a 1.0R val_a_0))
 ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
-ensures (with_pure ((reveal (length_of var_a)) = (old (reveal (length_of var_a)))))
+ensures (with_pure ((reveal #nat (length_of var_a)) = (old (reveal #nat (length_of var_a)))))
 ensures (with_pure ((id #int (Int32.v return_1)) = 1))
\ No newline at end of file
diff --git base/array_ptr_arith/Func_pre_decr.fst head/array_ptr_arith/Func_pre_decr.fst
index 9375913..18ed67d 100644
--- base/array_ptr_arith/Func_pre_decr.fst
+++ head/array_ptr_arith/Func_pre_decr.fst
@@ -7,13 +7,13 @@ divergent fn func_pre_decr (var_a: (array Typedef_int32_t.ty_int32_t))
   requires
     exists* (val_a_0: (full_array_spec Typedef_int32_t.ty_int32_t)).
     ((array_pts_to_full var_a 1.0R val_a_0))
-  requires (with_pure ((reveal (length_of var_a)) = 4))
+  requires (with_pure ((reveal #nat (length_of var_a)) = 4))
   returns return_1 : Typedef_int32_t.ty_int32_t
   ensures
     exists* (val_a_0: (full_array_spec Typedef_int32_t.ty_int32_t)).
     ((array_pts_to_full var_a 1.0R val_a_0))
   ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
-  ensures (with_pure ((reveal (length_of var_a)) = (old (reveal (length_of var_a)))))
+  ensures (with_pure ((reveal #nat (length_of var_a)) = (old (reveal #nat (length_of var_a)))))
   ensures (with_pure ((id #int (Int32.v return_1)) = 1))
 {
   let mut var_a = var_a;
diff --git base/array_ptr_arith/Func_pre_decr.fsti head/array_ptr_arith/Func_pre_decr.fsti
index 482755c..9824423 100644
--- base/array_ptr_arith/Func_pre_decr.fsti
+++ head/array_ptr_arith/Func_pre_decr.fsti
@@ -7,11 +7,11 @@ divergent fn func_pre_decr (var_a: (array Typedef_int32_t.ty_int32_t))
 requires
   exists* (val_a_0: (full_array_spec Typedef_int32_t.ty_int32_t)).
   ((array_pts_to_full var_a 1.0R val_a_0))
-requires (with_pure ((reveal (length_of var_a)) = 4))
+requires (with_pure ((reveal #nat (length_of var_a)) = 4))
 returns return_1 : Typedef_int32_t.ty_int32_t
 ensures
   exists* (val_a_0: (full_array_spec Typedef_int32_t.ty_int32_t)).
   ((array_pts_to_full var_a 1.0R val_a_0))
 ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
-ensures (with_pure ((reveal (length_of var_a)) = (old (reveal (length_of var_a)))))
+ensures (with_pure ((reveal #nat (length_of var_a)) = (old (reveal #nat (length_of var_a)))))
 ensures (with_pure ((id #int (Int32.v return_1)) = 1))
\ No newline at end of file
diff --git base/array_ptr_arith/Func_pre_incr.fst head/array_ptr_arith/Func_pre_incr.fst
index 4f901db..fe9c46e 100644
--- base/array_ptr_arith/Func_pre_incr.fst
+++ head/array_ptr_arith/Func_pre_incr.fst
@@ -7,13 +7,13 @@ divergent fn func_pre_incr (var_a: (array Typedef_int32_t.ty_int32_t))
   requires
     exists* (val_a_0: (full_array_spec Typedef_int32_t.ty_int32_t)).
     ((array_pts_to_full var_a 1.0R val_a_0))
-  requires (with_pure ((reveal (length_of var_a)) = 4))
+  requires (with_pure ((reveal #nat (length_of var_a)) = 4))
   returns return_1 : Typedef_int32_t.ty_int32_t
   ensures
     exists* (val_a_0: (full_array_spec Typedef_int32_t.ty_int32_t)).
     ((array_pts_to_full var_a 1.0R val_a_0))
   ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
-  ensures (with_pure ((reveal (length_of var_a)) = (old (reveal (length_of var_a)))))
+  ensures (with_pure ((reveal #nat (length_of var_a)) = (old (reveal #nat (length_of var_a)))))
   ensures (with_pure ((id #int (Int32.v return_1)) = 1))
 {
   let mut var_a = var_a;
diff --git base/array_ptr_arith/Func_pre_incr.fsti head/array_ptr_arith/Func_pre_incr.fsti
index eb92509..3c89ff4 100644
--- base/array_ptr_arith/Func_pre_incr.fsti
+++ head/array_ptr_arith/Func_pre_incr.fsti
@@ -7,11 +7,11 @@ divergent fn func_pre_incr (var_a: (array Typedef_int32_t.ty_int32_t))
 requires
   exists* (val_a_0: (full_array_spec Typedef_int32_t.ty_int32_t)).
   ((array_pts_to_full var_a 1.0R val_a_0))
-requires (with_pure ((reveal (length_of var_a)) = 4))
+requires (with_pure ((reveal #nat (length_of var_a)) = 4))
 returns return_1 : Typedef_int32_t.ty_int32_t
 ensures
   exists* (val_a_0: (full_array_spec Typedef_int32_t.ty_int32_t)).
   ((array_pts_to_full var_a 1.0R val_a_0))
 ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
-ensures (with_pure ((reveal (length_of var_a)) = (old (reveal (length_of var_a)))))
+ensures (with_pure ((reveal #nat (length_of var_a)) = (old (reveal #nat (length_of var_a)))))
 ensures (with_pure ((id #int (Int32.v return_1)) = 1))
\ No newline at end of file
diff --git base/array_test/Func_foo.fst head/array_test/Func_foo.fst
index bb95d93..feb0c16 100644
--- base/array_test/Func_foo.fst
+++ head/array_test/Func_foo.fst
@@ -5,10 +5,10 @@ open Pulse.Lib.C
 
 divergent fn func_foo (var_a: (array UInt32.t))
   requires exists* (val_a_0: (full_array_spec UInt32.t)). ((array_pts_to_full var_a 1.0R val_a_0))
-  requires (with_pure ((reveal (length_of var_a)) = 2))
+  requires (with_pure ((reveal #nat (length_of var_a)) = 2))
   returns return_1 : unit
   ensures exists* (val_a_0: (full_array_spec UInt32.t)). ((array_pts_to_full var_a 1.0R val_a_0))
-  ensures (with_pure ((reveal (length_of var_a)) = (old (reveal (length_of var_a)))))
+  ensures (with_pure ((reveal #nat (length_of var_a)) = (old (reveal #nat (length_of var_a)))))
   ensures (with_pure ((id #int (UInt32.v ((array_read var_a 0sz)))) = 42))
 {
   let mut var_a = var_a;
diff --git base/array_test/Func_foo.fsti head/array_test/Func_foo.fsti
index 6e653d1..5fb182e 100644
--- base/array_test/Func_foo.fsti
+++ head/array_test/Func_foo.fsti
@@ -5,8 +5,8 @@ open Pulse.Lib.C
 
 divergent fn func_foo (var_a: (array UInt32.t))
 requires exists* (val_a_0: (full_array_spec UInt32.t)). ((array_pts_to_full var_a 1.0R val_a_0))
-requires (with_pure ((reveal (length_of var_a)) = 2))
+requires (with_pure ((reveal #nat (length_of var_a)) = 2))
 returns return_1 : unit
 ensures exists* (val_a_0: (full_array_spec UInt32.t)). ((array_pts_to_full var_a 1.0R val_a_0))
-ensures (with_pure ((reveal (length_of var_a)) = (old (reveal (length_of var_a)))))
+ensures (with_pure ((reveal #nat (length_of var_a)) = (old (reveal #nat (length_of var_a)))))
 ensures (with_pure ((id #int (UInt32.v ((array_read var_a 0sz)))) = 42))
\ No newline at end of file
diff --git base/array_test/Func_ptr_attr.fst head/array_test/Func_ptr_attr.fst
index a5c81a8..55a3aad 100644
--- base/array_test/Func_ptr_attr.fst
+++ head/array_test/Func_ptr_attr.fst
@@ -5,10 +5,10 @@ open Pulse.Lib.C
 
 divergent fn func_ptr_attr (var_a: (array UInt32.t))
   requires exists* (val_a_0: (full_array_spec UInt32.t)). ((array_pts_to_full var_a 1.0R val_a_0))
-  requires (with_pure ((reveal (length_of var_a)) = 2))
+  requires (with_pure ((reveal #nat (length_of var_a)) = 2))
   returns return_1 : unit
   ensures exists* (val_a_0: (full_array_spec UInt32.t)). ((array_pts_to_full var_a 1.0R val_a_0))
-  ensures (with_pure ((reveal (length_of var_a)) = (old (reveal (length_of var_a)))))
+  ensures (with_pure ((reveal #nat (length_of var_a)) = (old (reveal #nat (length_of var_a)))))
   ensures (with_pure ((id #int (UInt32.v ((array_read var_a 0sz)))) = 42))
 {
   let mut var_a = var_a;
diff --git base/array_test/Func_ptr_attr.fsti head/array_test/Func_ptr_attr.fsti
index 956dd82..3023d34 100644
--- base/array_test/Func_ptr_attr.fsti
+++ head/array_test/Func_ptr_attr.fsti
@@ -5,8 +5,8 @@ open Pulse.Lib.C
 
 divergent fn func_ptr_attr (var_a: (array UInt32.t))
 requires exists* (val_a_0: (full_array_spec UInt32.t)). ((array_pts_to_full var_a 1.0R val_a_0))
-requires (with_pure ((reveal (length_of var_a)) = 2))
+requires (with_pure ((reveal #nat (length_of var_a)) = 2))
 returns return_1 : unit
 ensures exists* (val_a_0: (full_array_spec UInt32.t)). ((array_pts_to_full var_a 1.0R val_a_0))
-ensures (with_pure ((reveal (length_of var_a)) = (old (reveal (length_of var_a)))))
+ensures (with_pure ((reveal #nat (length_of var_a)) = (old (reveal #nat (length_of var_a)))))
 ensures (with_pure ((id #int (UInt32.v ((array_read var_a 0sz)))) = 42))
\ No newline at end of file
diff --git base/array_test/Func_struct_arr.fst head/array_test/Func_struct_arr.fst
index 69546f8..6120e66 100644
--- base/array_test/Func_struct_arr.fst
+++ head/array_test/Func_struct_arr.fst
@@ -9,15 +9,18 @@ divergent fn func_struct_arr (var_a: Typedef_uptr_struct.ty_uptr_struct)
     ((Typedef_uptr_struct.ty_uptr_struct__pred var_a 1.0R val_a_0))
   requires
     (with_pure
-      ((reveal (length_of (var_a).Struct_uptr_struct_anon_1.struct_uptr_struct_anon_1__x)) = 2))
+      ((reveal #nat (length_of (var_a).Struct_uptr_struct_anon_1.struct_uptr_struct_anon_1__x)) =
+        2))
   returns return_1 : unit
   ensures
     exists* (val_a_0: Struct_uptr_struct_anon_1.struct_uptr_struct_anon_1__spec).
     ((Typedef_uptr_struct.ty_uptr_struct__pred var_a 1.0R val_a_0))
   ensures
     (with_pure
-      ((reveal (length_of (var_a).Struct_uptr_struct_anon_1.struct_uptr_struct_anon_1__x)) =
-        (old (reveal (length_of (var_a).Struct_uptr_struct_anon_1.struct_uptr_struct_anon_1__x)))))
+      ((reveal #nat (length_of (var_a).Struct_uptr_struct_anon_1.struct_uptr_struct_anon_1__x)) =
+        (old
+          (reveal #nat
+            (length_of (var_a).Struct_uptr_struct_anon_1.struct_uptr_struct_anon_1__x)))))
   ensures
     (with_pure
       ((id
diff --git base/array_test/Func_struct_arr.fsti head/array_test/Func_struct_arr.fsti
index e7322eb..a6db380 100644
--- base/array_test/Func_struct_arr.fsti
+++ head/array_test/Func_struct_arr.fsti
@@ -9,15 +9,16 @@ requires
   ((Typedef_uptr_struct.ty_uptr_struct__pred var_a 1.0R val_a_0))
 requires
   (with_pure
-    ((reveal (length_of (var_a).Struct_uptr_struct_anon_1.struct_uptr_struct_anon_1__x)) = 2))
+    ((reveal #nat (length_of (var_a).Struct_uptr_struct_anon_1.struct_uptr_struct_anon_1__x)) = 2))
 returns return_1 : unit
 ensures
   exists* (val_a_0: Struct_uptr_struct_anon_1.struct_uptr_struct_anon_1__spec).
   ((Typedef_uptr_struct.ty_uptr_struct__pred var_a 1.0R val_a_0))
 ensures
   (with_pure
-    ((reveal (length_of (var_a).Struct_uptr_struct_anon_1.struct_uptr_struct_anon_1__x)) =
-      (old (reveal (length_of (var_a).Struct_uptr_struct_anon_1.struct_uptr_struct_anon_1__x)))))
+    ((reveal #nat (length_of (var_a).Struct_uptr_struct_anon_1.struct_uptr_struct_anon_1__x)) =
+      (old
+        (reveal #nat (length_of (var_a).Struct_uptr_struct_anon_1.struct_uptr_struct_anon_1__x)))))
 ensures
   (with_pure
     ((id
diff --git base/array_test/Func_tydef_array.fst head/array_test/Func_tydef_array.fst
index c7665e4..15cbeca 100644
--- base/array_test/Func_tydef_array.fst
+++ head/array_test/Func_tydef_array.fst
@@ -7,12 +7,12 @@ divergent fn func_tydef_array (var_a: Typedef_uptr.ty_uptr)
   requires
     exists* (val_a_0: (full_array_spec UInt32.t)).
     ((Typedef_uptr.ty_uptr__pred var_a 1.0R val_a_0))
-  requires (with_pure ((reveal (length_of var_a)) = 2))
+  requires (with_pure ((reveal #nat (length_of var_a)) = 2))
   returns return_1 : unit
   ensures
     exists* (val_a_0: (full_array_spec UInt32.t)).
     ((Typedef_uptr.ty_uptr__pred var_a 1.0R val_a_0))
-  ensures (with_pure ((reveal (length_of var_a)) = (old (reveal (length_of var_a)))))
+  ensures (with_pure ((reveal #nat (length_of var_a)) = (old (reveal #nat (length_of var_a)))))
   ensures (with_pure ((id #int (UInt32.v ((array_read var_a 0sz)))) = 42))
 {
   let mut var_a = var_a;
diff --git base/array_test/Func_tydef_array.fsti head/array_test/Func_tydef_array.fsti
index b3c7832..3bb89f4 100644
--- base/array_test/Func_tydef_array.fsti
+++ head/array_test/Func_tydef_array.fsti
@@ -7,10 +7,10 @@ divergent fn func_tydef_array (var_a: Typedef_uptr.ty_uptr)
 requires
   exists* (val_a_0: (full_array_spec UInt32.t)).
   ((Typedef_uptr.ty_uptr__pred var_a 1.0R val_a_0))
-requires (with_pure ((reveal (length_of var_a)) = 2))
+requires (with_pure ((reveal #nat (length_of var_a)) = 2))
 returns return_1 : unit
 ensures
   exists* (val_a_0: (full_array_spec UInt32.t)).
   ((Typedef_uptr.ty_uptr__pred var_a 1.0R val_a_0))
-ensures (with_pure ((reveal (length_of var_a)) = (old (reveal (length_of var_a)))))
+ensures (with_pure ((reveal #nat (length_of var_a)) = (old (reveal #nat (length_of var_a)))))
 ensures (with_pure ((id #int (UInt32.v ((array_read var_a 0sz)))) = 42))
\ No newline at end of file
diff --git base/array_test/Typedef_b32_struct.fst head/array_test/Typedef_b32_struct.fst
index a90d140..11b3898 100644
--- base/array_test/Typedef_b32_struct.fst
+++ head/array_test/Typedef_b32_struct.fst
@@ -11,7 +11,7 @@ let ty_b32_struct : Type = Struct_b32_struct_anon_1.struct_b32_struct_anon_1
       (val_this_0: Struct_b32_struct_anon_1.struct_b32_struct_anon_1__spec) =
   ((Struct_b32_struct_anon_1.struct_b32_struct_anon_1__pred this p val_this_0) **
     (with_pure
-      ((reveal (length_of (this).Struct_b32_struct_anon_1.struct_b32_struct_anon_1__x)) = 32)))
+      ((reveal #nat (length_of (this).Struct_b32_struct_anon_1.struct_b32_struct_anon_1__x)) = 32)))
 [@@pulse_eager_unfold] let predicate ty_b32_struct__uninit_pred
       ([@@@mkey] this: ty_b32_struct)
       (val_this_0: (array_spec UInt8.t)) =
diff --git base/array_to_ref/Func_caller.fst head/array_to_ref/Func_caller.fst
index 25df099..766c3ad 100644
--- base/array_to_ref/Func_caller.fst
+++ head/array_to_ref/Func_caller.fst
@@ -5,7 +5,7 @@ open Pulse.Lib.C
 
 divergent fn func_caller (var_a: (array Int32.t)) (var_i: SizeT.t)
   requires exists* (val_a_0: (full_array_spec Int32.t)). ((array_pts_to_full var_a 1.0R val_a_0))
-  requires (with_pure ((SizeT.v var_i) < (reveal (length_of var_a))))
+  requires (with_pure ((SizeT.v var_i) < (reveal #nat (length_of var_a))))
   returns return_1 : unit
   ensures exists* (val_a_0: (full_array_spec Int32.t)). ((array_pts_to_full var_a 1.0R val_a_0))
 {
diff --git base/array_to_ref/Func_caller.fsti head/array_to_ref/Func_caller.fsti
index 995fe6f..1289adf 100644
--- base/array_to_ref/Func_caller.fsti
+++ head/array_to_ref/Func_caller.fsti
@@ -5,6 +5,6 @@ open Pulse.Lib.C
 
 divergent fn func_caller (var_a: (array Int32.t)) (var_i: SizeT.t)
 requires exists* (val_a_0: (full_array_spec Int32.t)). ((array_pts_to_full var_a 1.0R val_a_0))
-requires (with_pure ((SizeT.v var_i) < (reveal (length_of var_a))))
+requires (with_pure ((SizeT.v var_i) < (reveal #nat (length_of var_a))))
 returns return_1 : unit
 ensures exists* (val_a_0: (full_array_spec Int32.t)). ((array_pts_to_full var_a 1.0R val_a_0))
\ No newline at end of file
diff --git base/array_to_ref/Func_caller_out.fst head/array_to_ref/Func_caller_out.fst
index b5b50f3..7d5b23f 100644
--- base/array_to_ref/Func_caller_out.fst
+++ head/array_to_ref/Func_caller_out.fst
@@ -5,7 +5,7 @@ open Pulse.Lib.C
 
 divergent fn func_caller_out (var_a: (array Int32.t)) (var_i: SizeT.t)
   requires exists* (val_a_0: (full_array_spec Int32.t)). ((array_pts_to_full var_a 1.0R val_a_0))
-  requires (with_pure ((SizeT.v var_i) < (reveal (length_of var_a))))
+  requires (with_pure ((SizeT.v var_i) < (reveal #nat (length_of var_a))))
   returns return_1 : unit
   ensures exists* (val_a_0: (full_array_spec Int32.t)). ((array_pts_to_full var_a 1.0R val_a_0))
 {
diff --git base/array_to_ref/Func_caller_out.fsti head/array_to_ref/Func_caller_out.fsti
index a9df0f0..064df63 100644
--- base/array_to_ref/Func_caller_out.fsti
+++ head/array_to_ref/Func_caller_out.fsti
@@ -5,6 +5,6 @@ open Pulse.Lib.C
 
 divergent fn func_caller_out (var_a: (array Int32.t)) (var_i: SizeT.t)
 requires exists* (val_a_0: (full_array_spec Int32.t)). ((array_pts_to_full var_a 1.0R val_a_0))
-requires (with_pure ((SizeT.v var_i) < (reveal (length_of var_a))))
+requires (with_pure ((SizeT.v var_i) < (reveal #nat (length_of var_a))))
 returns return_1 : unit
 ensures exists* (val_a_0: (full_array_spec Int32.t)). ((array_pts_to_full var_a 1.0R val_a_0))
\ No newline at end of file
diff --git base/array_to_ref/Func_fill_first.fst head/array_to_ref/Func_fill_first.fst
index c1735bf..7afd4f1 100644
--- base/array_to_ref/Func_fill_first.fst
+++ head/array_to_ref/Func_fill_first.fst
@@ -5,7 +5,7 @@ open Pulse.Lib.C
 
 divergent fn func_fill_first (var_a: (array Int32.t))
   requires exists* ('val_a_0: (array_spec Int32.t)). ((array_pts_to_uninit var_a 'val_a_0))
-  requires (with_pure ((reveal (length_of var_a)) = 1))
+  requires (with_pure ((reveal #nat (length_of var_a)) = 1))
   returns return_1 : unit
   ensures exists* (val_a_0: (full_array_spec Int32.t)). ((array_pts_to_full var_a 1.0R val_a_0))
 {
diff --git base/array_to_ref/Func_fill_first.fsti head/array_to_ref/Func_fill_first.fsti
index 943cfc0..eab8b67 100644
--- base/array_to_ref/Func_fill_first.fsti
+++ head/array_to_ref/Func_fill_first.fsti
@@ -5,6 +5,6 @@ open Pulse.Lib.C
 
 divergent fn func_fill_first (var_a: (array Int32.t))
 requires exists* ('val_a_0: (array_spec Int32.t)). ((array_pts_to_uninit var_a 'val_a_0))
-requires (with_pure ((reveal (length_of var_a)) = 1))
+requires (with_pure ((reveal #nat (length_of var_a)) = 1))
 returns return_1 : unit
 ensures exists* (val_a_0: (full_array_spec Int32.t)). ((array_pts_to_full var_a 1.0R val_a_0))
\ No newline at end of file
diff --git base/array_typedef_pointer/Func_get_entry.fst head/array_typedef_pointer/Func_get_entry.fst
index d6fbf3b..134132c 100644
--- base/array_typedef_pointer/Func_get_entry.fst
+++ head/array_typedef_pointer/Func_get_entry.fst
@@ -14,7 +14,7 @@ divergent fn func_get_entry
   requires ((Typedef_uint32_t.ty_uint32_t__pred var_idx 1.0R))
   requires
     (with_pure
-      (((reveal (length_of var_table)) = (id #int (UInt32.v var_count))) &&
+      (((reveal #nat (length_of var_table)) = (id #int (UInt32.v var_count))) &&
         (var_idx `UInt32.lt` var_count)))
   returns return_1 : (array Typedef_E.ty_e)
   ensures
diff --git base/array_typedef_pointer/Func_get_entry.fsti head/array_typedef_pointer/Func_get_entry.fsti
index 1f35286..58b2afd 100644
--- base/array_typedef_pointer/Func_get_entry.fsti
+++ head/array_typedef_pointer/Func_get_entry.fsti
@@ -14,7 +14,7 @@ requires ((Typedef_uint32_t.ty_uint32_t__pred var_count 1.0R))
 requires ((Typedef_uint32_t.ty_uint32_t__pred var_idx 1.0R))
 requires
   (with_pure
-    (((reveal (length_of var_table)) = (id #int (UInt32.v var_count))) &&
+    (((reveal #nat (length_of var_table)) = (id #int (UInt32.v var_count))) &&
       (var_idx `UInt32.lt` var_count)))
 returns return_1 : (array Typedef_E.ty_e)
 ensures
diff --git base/array_typedef_pointer/Func_read_first.fst head/array_typedef_pointer/Func_read_first.fst
index 7d569aa..910582b 100644
--- base/array_typedef_pointer/Func_read_first.fst
+++ head/array_typedef_pointer/Func_read_first.fst
@@ -7,7 +7,7 @@ divergent fn func_read_first (var_table: (array Typedef_E.ty_e))
   requires
     exists* (val_table_0: (full_array_spec Typedef_E.ty_e)).
     ((array_pts_to_full var_table 1.0R val_table_0))
-  requires (with_pure (0 < (reveal (length_of var_table))))
+  requires (with_pure (0 < (reveal #nat (length_of var_table))))
   returns return_1 : Typedef_uint16_t.ty_uint16_t
   ensures
     exists* (val_table_0: (full_array_spec Typedef_E.ty_e)).
diff --git base/array_typedef_pointer/Func_read_first.fsti head/array_typedef_pointer/Func_read_first.fsti
index 785dabc..26c2dea 100644
--- base/array_typedef_pointer/Func_read_first.fsti
+++ head/array_typedef_pointer/Func_read_first.fsti
@@ -7,7 +7,7 @@ divergent fn func_read_first (var_table: (array Typedef_E.ty_e))
 requires
   exists* (val_table_0: (full_array_spec Typedef_E.ty_e)).
   ((array_pts_to_full var_table 1.0R val_table_0))
-requires (with_pure (0 < (reveal (length_of var_table))))
+requires (with_pure (0 < (reveal #nat (length_of var_table))))
 returns return_1 : Typedef_uint16_t.ty_uint16_t
 ensures
   exists* (val_table_0: (full_array_spec Typedef_E.ty_e)).
diff --git base/array_update/Func_set_both.fst head/array_update/Func_set_both.fst
index 87a04db..0f6e2fc 100644
--- base/array_update/Func_set_both.fst
+++ head/array_update/Func_set_both.fst
@@ -11,12 +11,12 @@ divergent fn func_set_both
   requires
     exists* (val_pts_0: (full_array_spec Struct_point.struct_point)).
     ((array_pts_to_full var_pts 1.0R val_pts_0))
-  requires (with_pure ((SizeT.v var_i) < (reveal (length_of var_pts))))
+  requires (with_pure ((SizeT.v var_i) < (reveal #nat (length_of var_pts))))
   returns return_1 : unit
   ensures
     exists* (val_pts_0: (full_array_spec Struct_point.struct_point)).
     ((array_pts_to_full var_pts 1.0R val_pts_0))
-  ensures (with_pure ((reveal (length_of var_pts)) = (old (reveal (length_of var_pts)))))
+  ensures (with_pure ((reveal #nat (length_of var_pts)) = (old (reveal #nat (length_of var_pts)))))
   ensures (with_pure ((((array_read var_pts var_i))).Struct_point.struct_point__x = var_vx))
   ensures (with_pure ((((array_read var_pts var_i))).Struct_point.struct_point__y = var_vy))
 {
diff --git base/array_update/Func_set_both.fsti head/array_update/Func_set_both.fsti
index 058d763..cbb2fc1 100644
--- base/array_update/Func_set_both.fsti
+++ head/array_update/Func_set_both.fsti
@@ -11,11 +11,11 @@ divergent fn func_set_both
 requires
   exists* (val_pts_0: (full_array_spec Struct_point.struct_point)).
   ((array_pts_to_full var_pts 1.0R val_pts_0))
-requires (with_pure ((SizeT.v var_i) < (reveal (length_of var_pts))))
+requires (with_pure ((SizeT.v var_i) < (reveal #nat (length_of var_pts))))
 returns return_1 : unit
 ensures
   exists* (val_pts_0: (full_array_spec Struct_point.struct_point)).
   ((array_pts_to_full var_pts 1.0R val_pts_0))
-ensures (with_pure ((reveal (length_of var_pts)) = (old (reveal (length_of var_pts)))))
+ensures (with_pure ((reveal #nat (length_of var_pts)) = (old (reveal #nat (length_of var_pts)))))
 ensures (with_pure ((((array_read var_pts var_i))).Struct_point.struct_point__x = var_vx))
 ensures (with_pure ((((array_read var_pts var_i))).Struct_point.struct_point__y = var_vy))
\ No newline at end of file
diff --git base/array_update/Func_set_elem_fields.fst head/array_update/Func_set_elem_fields.fst
index 5bd29c4..eb8a9ca 100644
--- base/array_update/Func_set_elem_fields.fst
+++ head/array_update/Func_set_elem_fields.fst
@@ -14,7 +14,8 @@ divergent fn func_set_elem_fields
   requires ((Typedef_uint32_t.ty_uint32_t__pred var_i 1.0R))
   requires ((Typedef_uint64_t.ty_uint64_t__pred var_v 1.0R))
   requires ((Typedef_uint64_t.ty_uint64_t__pred var_t 1.0R))
-  requires (with_pure ((SizeT.v (SizeT.uint_to_t (UInt32.v var_i))) < (reveal (length_of var_a))))
+  requires
+    (with_pure ((SizeT.v (SizeT.uint_to_t (UInt32.v var_i))) < (reveal #nat (length_of var_a))))
   returns return_1 : unit
   ensures
     exists* (val_a_0: (full_array_spec Struct_entry.struct_entry)).
@@ -22,7 +23,7 @@ divergent fn func_set_elem_fields
   ensures ((Typedef_uint32_t.ty_uint32_t__pred var_i 1.0R))
   ensures ((Typedef_uint64_t.ty_uint64_t__pred var_v 1.0R))
   ensures ((Typedef_uint64_t.ty_uint64_t__pred var_t 1.0R))
-  ensures (with_pure ((reveal (length_of var_a)) = (old (reveal (length_of var_a)))))
+  ensures (with_pure ((reveal #nat (length_of var_a)) = (old (reveal #nat (length_of var_a)))))
   ensures
     (with_pure
       (((((array_read var_a (SizeT.uint_to_t (UInt32.v var_i))))).Struct_entry.struct_entry__value =
diff --git base/array_update/Func_set_elem_fields.fsti head/array_update/Func_set_elem_fields.fsti
index f2f0269..c04ea31 100644
--- base/array_update/Func_set_elem_fields.fsti
+++ head/array_update/Func_set_elem_fields.fsti
@@ -14,7 +14,8 @@ requires
 requires ((Typedef_uint32_t.ty_uint32_t__pred var_i 1.0R))
 requires ((Typedef_uint64_t.ty_uint64_t__pred var_v 1.0R))
 requires ((Typedef_uint64_t.ty_uint64_t__pred var_t 1.0R))
-requires (with_pure ((SizeT.v (SizeT.uint_to_t (UInt32.v var_i))) < (reveal (length_of var_a))))
+requires
+  (with_pure ((SizeT.v (SizeT.uint_to_t (UInt32.v var_i))) < (reveal #nat (length_of var_a))))
 returns return_1 : unit
 ensures
   exists* (val_a_0: (full_array_spec Struct_entry.struct_entry)).
@@ -22,7 +23,7 @@ ensures
 ensures ((Typedef_uint32_t.ty_uint32_t__pred var_i 1.0R))
 ensures ((Typedef_uint64_t.ty_uint64_t__pred var_v 1.0R))
 ensures ((Typedef_uint64_t.ty_uint64_t__pred var_t 1.0R))
-ensures (with_pure ((reveal (length_of var_a)) = (old (reveal (length_of var_a)))))
+ensures (with_pure ((reveal #nat (length_of var_a)) = (old (reveal #nat (length_of var_a)))))
 ensures
   (with_pure
     (((((array_read var_a (SizeT.uint_to_t (UInt32.v var_i))))).Struct_entry.struct_entry__value =
diff --git base/array_update/Func_set_x.fst head/array_update/Func_set_x.fst
index f070a53..f0a4d5c 100644
--- base/array_update/Func_set_x.fst
+++ head/array_update/Func_set_x.fst
@@ -10,12 +10,12 @@ divergent fn func_set_x
   requires
     exists* (val_pts_0: (full_array_spec Struct_point.struct_point)).
     ((array_pts_to_full var_pts 1.0R val_pts_0))
-  requires (with_pure ((SizeT.v var_i) < (reveal (length_of var_pts))))
+  requires (with_pure ((SizeT.v var_i) < (reveal #nat (length_of var_pts))))
   returns return_1 : unit
   ensures
     exists* (val_pts_0: (full_array_spec Struct_point.struct_point)).
     ((array_pts_to_full var_pts 1.0R val_pts_0))
-  ensures (with_pure ((reveal (length_of var_pts)) = (old (reveal (length_of var_pts)))))
+  ensures (with_pure ((reveal #nat (length_of var_pts)) = (old (reveal #nat (length_of var_pts)))))
   ensures (with_pure ((((array_read var_pts var_i))).Struct_point.struct_point__x = var_val))
 {
   let mut var_pts = var_pts;
diff --git base/array_update/Func_set_x.fsti head/array_update/Func_set_x.fsti
index c6ea73b..723542d 100644
--- base/array_update/Func_set_x.fsti
+++ head/array_update/Func_set_x.fsti
@@ -10,10 +10,10 @@ divergent fn func_set_x
 requires
   exists* (val_pts_0: (full_array_spec Struct_point.struct_point)).
   ((array_pts_to_full var_pts 1.0R val_pts_0))
-requires (with_pure ((SizeT.v var_i) < (reveal (length_of var_pts))))
+requires (with_pure ((SizeT.v var_i) < (reveal #nat (length_of var_pts))))
 returns return_1 : unit
 ensures
   exists* (val_pts_0: (full_array_spec Struct_point.struct_point)).
   ((array_pts_to_full var_pts 1.0R val_pts_0))
-ensures (with_pure ((reveal (length_of var_pts)) = (old (reveal (length_of var_pts)))))
+ensures (with_pure ((reveal #nat (length_of var_pts)) = (old (reveal #nat (length_of var_pts)))))
 ensures (with_pure ((((array_read var_pts var_i))).Struct_point.struct_point__x = var_val))
\ No newline at end of file
diff --git base/array_update/Func_set_x_alt.fst head/array_update/Func_set_x_alt.fst
index f801e2d..f945100 100644
--- base/array_update/Func_set_x_alt.fst
+++ head/array_update/Func_set_x_alt.fst
@@ -7,7 +7,7 @@ divergent fn func_set_x_alt (var_arr: (array Struct_point.struct_point))
   requires
     exists* (val_arr_0: (full_array_spec Struct_point.struct_point)).
     ((array_pts_to_full var_arr 1.0R val_arr_0))
-  requires (with_pure ((reveal (length_of var_arr)) = 2))
+  requires (with_pure ((reveal #nat (length_of var_arr)) = 2))
   returns return_1 : unit
   ensures
     exists* (val_arr_0: (full_array_spec Struct_point.struct_point)).
diff --git base/array_update/Func_set_x_alt.fsti head/array_update/Func_set_x_alt.fsti
index 667bb14..2825209 100644
--- base/array_update/Func_set_x_alt.fsti
+++ head/array_update/Func_set_x_alt.fsti
@@ -7,7 +7,7 @@ divergent fn func_set_x_alt (var_arr: (array Struct_point.struct_point))
 requires
   exists* (val_arr_0: (full_array_spec Struct_point.struct_point)).
   ((array_pts_to_full var_arr 1.0R val_arr_0))
-requires (with_pure ((reveal (length_of var_arr)) = 2))
+requires (with_pure ((reveal #nat (length_of var_arr)) = 2))
 returns return_1 : unit
 ensures
   exists* (val_arr_0: (full_array_spec Struct_point.struct_point)).
diff --git base/array_update/Func_set_y.fst head/array_update/Func_set_y.fst
index e9fb3b2..5dbdfde 100644
--- base/array_update/Func_set_y.fst
+++ head/array_update/Func_set_y.fst
@@ -10,12 +10,12 @@ divergent fn func_set_y
   requires
     exists* (val_pts_0: (full_array_spec Struct_point.struct_point)).
     ((array_pts_to_full var_pts 1.0R val_pts_0))
-  requires (with_pure ((SizeT.v var_i) < (reveal (length_of var_pts))))
+  requires (with_pure ((SizeT.v var_i) < (reveal #nat (length_of var_pts))))
   returns return_1 : unit
   ensures
     exists* (val_pts_0: (full_array_spec Struct_point.struct_point)).
     ((array_pts_to_full var_pts 1.0R val_pts_0))
-  ensures (with_pure ((reveal (length_of var_pts)) = (old (reveal (length_of var_pts)))))
+  ensures (with_pure ((reveal #nat (length_of var_pts)) = (old (reveal #nat (length_of var_pts)))))
   ensures (with_pure ((((array_read var_pts var_i))).Struct_point.struct_point__y = var_val))
 {
   let mut var_pts = var_pts;
diff --git base/array_update/Func_set_y.fsti head/array_update/Func_set_y.fsti
index e952d1e..c953b6b 100644
--- base/array_update/Func_set_y.fsti
+++ head/array_update/Func_set_y.fsti
@@ -10,10 +10,10 @@ divergent fn func_set_y
 requires
   exists* (val_pts_0: (full_array_spec Struct_point.struct_point)).
   ((array_pts_to_full var_pts 1.0R val_pts_0))
-requires (with_pure ((SizeT.v var_i) < (reveal (length_of var_pts))))
+requires (with_pure ((SizeT.v var_i) < (reveal #nat (length_of var_pts))))
 returns return_1 : unit
 ensures
   exists* (val_pts_0: (full_array_spec Struct_point.struct_point)).
   ((array_pts_to_full var_pts 1.0R val_pts_0))
-ensures (with_pure ((reveal (length_of var_pts)) = (old (reveal (length_of var_pts)))))
+ensures (with_pure ((reveal #nat (length_of var_pts)) = (old (reveal #nat (length_of var_pts)))))
 ensures (with_pure ((((array_read var_pts var_i))).Struct_point.struct_point__y = var_val))
\ No newline at end of file
diff --git base/arrayptr_compare/Func_less.fst head/arrayptr_compare/Func_less.fst
index eb1522e..ca2e2a7 100644
--- base/arrayptr_compare/Func_less.fst
+++ head/arrayptr_compare/Func_less.fst
@@ -5,7 +5,7 @@ open Pulse.Lib.C
 
 divergent fn func_less (var_a: (array Int32.t))
   requires exists* (val_a_0: (full_array_spec Int32.t)). ((array_pts_to_full var_a 1.0R val_a_0))
-  requires (with_pure ((reveal (length_of var_a)) = 10))
+  requires (with_pure ((reveal #nat (length_of var_a)) = 10))
   returns return_1 : Int32.t
   ensures exists* (val_a_0: (full_array_spec Int32.t)). ((array_pts_to_full var_a 1.0R val_a_0))
   ensures (with_pure ((id #int (Int32.v return_1)) = 1))
diff --git base/arrayptr_compare/Func_less.fsti head/arrayptr_compare/Func_less.fsti
index ccefb77..692e893 100644
--- base/arrayptr_compare/Func_less.fsti
+++ head/arrayptr_compare/Func_less.fsti
@@ -5,7 +5,7 @@ open Pulse.Lib.C
 
 divergent fn func_less (var_a: (array Int32.t))
 requires exists* (val_a_0: (full_array_spec Int32.t)). ((array_pts_to_full var_a 1.0R val_a_0))
-requires (with_pure ((reveal (length_of var_a)) = 10))
+requires (with_pure ((reveal #nat (length_of var_a)) = 10))
 returns return_1 : Int32.t
 ensures exists* (val_a_0: (full_array_spec Int32.t)). ((array_pts_to_full var_a 1.0R val_a_0))
 ensures (with_pure ((id #int (Int32.v return_1)) = 1))
\ No newline at end of file
diff --git base/arrayptr_diff/Func_same_object_diff.fst head/arrayptr_diff/Func_same_object_diff.fst
index c0504d1..0dd22c9 100644
--- base/arrayptr_diff/Func_same_object_diff.fst
+++ head/arrayptr_diff/Func_same_object_diff.fst
@@ -5,7 +5,7 @@ open Pulse.Lib.C
 
 divergent fn func_same_object_diff (var_a: (array Int32.t))
   requires exists* (val_a_0: (full_array_spec Int32.t)). ((array_pts_to_full var_a 1.0R val_a_0))
-  requires (with_pure ((reveal (length_of var_a)) = 10))
+  requires (with_pure ((reveal #nat (length_of var_a)) = 10))
   returns return_1 : Typedef_ptrdiff_t.ty_ptrdiff_t
   ensures exists* (val_a_0: (full_array_spec Int32.t)). ((array_pts_to_full var_a 1.0R val_a_0))
   ensures ((Typedef_ptrdiff_t.ty_ptrdiff_t__pred return_1 1.0R))
diff --git base/arrayptr_diff/Func_same_object_diff.fsti head/arrayptr_diff/Func_same_object_diff.fsti
index 9fcca70..646263f 100644
--- base/arrayptr_diff/Func_same_object_diff.fsti
+++ head/arrayptr_diff/Func_same_object_diff.fsti
@@ -5,7 +5,7 @@ open Pulse.Lib.C
 
 divergent fn func_same_object_diff (var_a: (array Int32.t))
 requires exists* (val_a_0: (full_array_spec Int32.t)). ((array_pts_to_full var_a 1.0R val_a_0))
-requires (with_pure ((reveal (length_of var_a)) = 10))
+requires (with_pure ((reveal #nat (length_of var_a)) = 10))
 returns return_1 : Typedef_ptrdiff_t.ty_ptrdiff_t
 ensures exists* (val_a_0: (full_array_spec Int32.t)). ((array_pts_to_full var_a 1.0R val_a_0))
 ensures ((Typedef_ptrdiff_t.ty_ptrdiff_t__pred return_1 1.0R))
\ 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..b7a0692 100644
--- base/arrayptr_ref/Func_assign_cell_address_to_ref.fst
+++ head/arrayptr_ref/Func_assign_cell_address_to_ref.fst
@@ -7,7 +7,7 @@ divergent fn func_assign_cell_address_to_ref (var_a: (array Typedef_SUBRANGE.ty_
   requires
     exists* ('val_a_0: (array_spec Typedef_SUBRANGE.ty_subrange)).
     ((array_pts_to_uninit var_a 'val_a_0))
-  requires (with_pure ((reveal (length_of var_a)) = 1))
+  requires (with_pure ((reveal #nat (length_of var_a)) = 1))
   returns return_1 : unit
   ensures
     exists* (val_a_0: (full_array_spec Typedef_SUBRANGE.ty_subrange)).
diff --git base/arrayptr_ref/Func_assign_cell_address_to_ref.fsti head/arrayptr_ref/Func_assign_cell_address_to_ref.fsti
index d2e8728..5db8310 100644
--- base/arrayptr_ref/Func_assign_cell_address_to_ref.fsti
+++ head/arrayptr_ref/Func_assign_cell_address_to_ref.fsti
@@ -7,7 +7,7 @@ divergent fn func_assign_cell_address_to_ref (var_a: (array Typedef_SUBRANGE.ty_
 requires
   exists* ('val_a_0: (array_spec Typedef_SUBRANGE.ty_subrange)).
   ((array_pts_to_uninit var_a 'val_a_0))
-requires (with_pure ((reveal (length_of var_a)) = 1))
+requires (with_pure ((reveal #nat (length_of var_a)) = 1))
 returns return_1 : unit
 ensures
   exists* (val_a_0: (full_array_spec Typedef_SUBRANGE.ty_subrange)).
diff --git base/arrayptr_ref/Func_consume_returned_arrayptr_as_ref.fst head/arrayptr_ref/Func_consume_returned_arrayptr_as_ref.fst
index 9717eb2..ab053b6 100644
--- base/arrayptr_ref/Func_consume_returned_arrayptr_as_ref.fst
+++ head/arrayptr_ref/Func_consume_returned_arrayptr_as_ref.fst
@@ -7,7 +7,7 @@ divergent fn func_consume_returned_arrayptr_as_ref (var_a: (array Typedef_SUBRAN
   requires
     exists* ('val_a_0: (array_spec Typedef_SUBRANGE.ty_subrange)).
     ((array_pts_to_uninit var_a 'val_a_0))
-  requires (with_pure ((reveal (length_of var_a)) = 1))
+  requires (with_pure ((reveal #nat (length_of var_a)) = 1))
   returns return_1 : unit
   ensures
     exists* (val_a_0: (full_array_spec Typedef_SUBRANGE.ty_subrange)).
diff --git base/arrayptr_ref/Func_consume_returned_arrayptr_as_ref.fsti head/arrayptr_ref/Func_consume_returned_arrayptr_as_ref.fsti
index 85ba07b..58b1192 100644
--- base/arrayptr_ref/Func_consume_returned_arrayptr_as_ref.fsti
+++ head/arrayptr_ref/Func_consume_returned_arrayptr_as_ref.fsti
@@ -7,7 +7,7 @@ divergent fn func_consume_returned_arrayptr_as_ref (var_a: (array Typedef_SUBRAN
 requires
   exists* ('val_a_0: (array_spec Typedef_SUBRANGE.ty_subrange)).
   ((array_pts_to_uninit var_a 'val_a_0))
-requires (with_pure ((reveal (length_of var_a)) = 1))
+requires (with_pure ((reveal #nat (length_of var_a)) = 1))
 returns return_1 : unit
 ensures
   exists* (val_a_0: (full_array_spec Typedef_SUBRANGE.ty_subrange)).
diff --git base/arrayptr_ref/Func_pass_arrayptr_as_ref.fst head/arrayptr_ref/Func_pass_arrayptr_as_ref.fst
index 0311e53..9b535d2 100644
--- base/arrayptr_ref/Func_pass_arrayptr_as_ref.fst
+++ head/arrayptr_ref/Func_pass_arrayptr_as_ref.fst
@@ -5,7 +5,7 @@ open Pulse.Lib.C
 
 divergent fn func_pass_arrayptr_as_ref (var_a: (array Int32.t))
   requires exists* (val_a_0: (full_array_spec Int32.t)). ((array_pts_to_full var_a 1.0R val_a_0))
-  requires (with_pure ((reveal (length_of var_a)) = 3))
+  requires (with_pure ((reveal #nat (length_of var_a)) = 3))
   returns return_1 : unit
   ensures exists* (val_a_0: (full_array_spec Int32.t)). ((array_pts_to_full var_a 1.0R val_a_0))
 {
diff --git base/arrayptr_ref/Func_pass_arrayptr_as_ref.fsti head/arrayptr_ref/Func_pass_arrayptr_as_ref.fsti
index 3962130..83b3db4 100644
--- base/arrayptr_ref/Func_pass_arrayptr_as_ref.fsti
+++ head/arrayptr_ref/Func_pass_arrayptr_as_ref.fsti
@@ -5,6 +5,6 @@ open Pulse.Lib.C
 
 divergent fn func_pass_arrayptr_as_ref (var_a: (array Int32.t))
 requires exists* (val_a_0: (full_array_spec Int32.t)). ((array_pts_to_full var_a 1.0R val_a_0))
-requires (with_pure ((reveal (length_of var_a)) = 3))
+requires (with_pure ((reveal #nat (length_of var_a)) = 3))
 returns return_1 : unit
 ensures exists* (val_a_0: (full_array_spec Int32.t)). ((array_pts_to_full var_a 1.0R val_a_0))
\ No newline at end of file
diff --git base/arrayptrs/Func_use_binary_search.fst head/arrayptrs/Func_use_binary_search.fst
index 92f6f1c..81130ac 100644
--- base/arrayptrs/Func_use_binary_search.fst
+++ head/arrayptrs/Func_use_binary_search.fst
@@ -9,7 +9,8 @@ divergent fn func_use_binary_search
     (var_length: SizeT.t)
   requires
     (with_pure
-      (((SizeT.v var_length) = (reveal (length_of var_arr))) && ((SizeT.v var_length) <= 10000)))
+      (((SizeT.v var_length) = (reveal #nat (length_of var_arr))) &&
+        ((SizeT.v var_length) <= 10000)))
   preserves (array_pts_to_full var_arr 'p_arr_0 'val_arr_0)
   returns return_1 : unit
 {
diff --git base/arrayptrs/Func_use_binary_search.fsti head/arrayptrs/Func_use_binary_search.fsti
index 79f39b9..738df48 100644
--- base/arrayptrs/Func_use_binary_search.fsti
+++ head/arrayptrs/Func_use_binary_search.fsti
@@ -9,6 +9,6 @@ divergent fn func_use_binary_search
   (var_length: SizeT.t)
 requires
   (with_pure
-    (((SizeT.v var_length) = (reveal (length_of var_arr))) && ((SizeT.v var_length) <= 10000)))
+    (((SizeT.v var_length) = (reveal #nat (length_of var_arr))) && ((SizeT.v var_length) <= 10000)))
 preserves (array_pts_to_full var_arr 'p_arr_0 'val_arr_0)
 returns return_1 : unit
\ No newline at end of file
diff --git base/arrayptrs/Func_write_via_ptr.fst head/arrayptrs/Func_write_via_ptr.fst
index 150785e..6ee64db 100644
--- base/arrayptrs/Func_write_via_ptr.fst
+++ head/arrayptrs/Func_write_via_ptr.fst
@@ -5,10 +5,10 @@ open Pulse.Lib.C
 
 divergent fn func_write_via_ptr (var_a: (array Int32.t))
   requires exists* (val_a_0: (full_array_spec Int32.t)). ((array_pts_to_full var_a 1.0R val_a_0))
-  requires (with_pure ((reveal (length_of var_a)) = 10))
+  requires (with_pure ((reveal #nat (length_of var_a)) = 10))
   returns return_1 : unit
   ensures exists* (val_a_0: (full_array_spec Int32.t)). ((array_pts_to_full var_a 1.0R val_a_0))
-  ensures (with_pure ((reveal (length_of var_a)) = (old (reveal (length_of var_a)))))
+  ensures (with_pure ((reveal #nat (length_of var_a)) = (old (reveal #nat (length_of var_a)))))
 {
   let mut var_a = var_a;
   let mut var_p : (array Int32.t);
diff --git base/arrayptrs/Func_write_via_ptr.fsti head/arrayptrs/Func_write_via_ptr.fsti
index 5602460..ce421d6 100644
--- base/arrayptrs/Func_write_via_ptr.fsti
+++ head/arrayptrs/Func_write_via_ptr.fsti
@@ -5,7 +5,7 @@ open Pulse.Lib.C
 
 divergent fn func_write_via_ptr (var_a: (array Int32.t))
 requires exists* (val_a_0: (full_array_spec Int32.t)). ((array_pts_to_full var_a 1.0R val_a_0))
-requires (with_pure ((reveal (length_of var_a)) = 10))
+requires (with_pure ((reveal #nat (length_of var_a)) = 10))
 returns return_1 : unit
 ensures exists* (val_a_0: (full_array_spec Int32.t)). ((array_pts_to_full var_a 1.0R val_a_0))
-ensures (with_pure ((reveal (length_of var_a)) = (old (reveal (length_of var_a)))))
\ No newline at end of file
+ensures (with_pure ((reveal #nat (length_of var_a)) = (old (reveal #nat (length_of var_a)))))
\ No newline at end of file
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..46db6e5 100644
--- base/calloc_alloc_size/Func_test_calloc_count_mul_size.fst
+++ head/calloc_alloc_size/Func_test_calloc_count_mul_size.fst
@@ -11,7 +11,7 @@ divergent fn func_test_calloc_count_mul_size ()
     (Pulse.Lib.C.Array.calloc_array
       #Int32.t
       (SizeT.uint_to_t (UInt64.v (id #UInt64.t (Int.Cast.int32_to_uint64 3l)))));
-  assert (with_pure ((reveal (length_of (!var_array))) = 3));
+  assert (with_pure ((reveal #nat (length_of (!var_array))) = 3));
   assert (with_pure ((id #int (Int32.v ((array_read (!var_array) 0sz)))) = 0));
   (array_write (!var_array) 0sz 67l);
   (Pulse.Lib.C.Array.free_array (!var_array));
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..bed3f0d 100644
--- base/calloc_alloc_size/Func_test_calloc_count_size_mul.fst
+++ head/calloc_alloc_size/Func_test_calloc_count_size_mul.fst
@@ -11,7 +11,7 @@ divergent fn func_test_calloc_count_size_mul ()
     (Pulse.Lib.C.Array.calloc_array
       #Int32.t
       (SizeT.uint_to_t (UInt64.v (id #UInt64.t (Int.Cast.int32_to_uint64 4l)))));
-  assert (with_pure ((reveal (length_of (!var_array))) = 4));
+  assert (with_pure ((reveal #nat (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));
 }
\ No newline at end of file
diff --git base/compare_elements/Func_compare_elems.fst head/compare_elements/Func_compare_elems.fst
index 20560d4..c659772 100644
--- base/compare_elements/Func_compare_elems.fst
+++ head/compare_elements/Func_compare_elems.fst
@@ -8,13 +8,13 @@ divergent fn func_compare_elems (var_a: (array Int32.t)) (var_b: (array Int32.t)
   requires exists* (val_b_0: (full_array_spec Int32.t)). ((array_pts_to_full var_b 1.0R val_b_0))
   requires
     (with_pure
-      (((reveal (length_of var_a)) = (SizeT.v var_len)) &&
-        ((reveal (length_of var_b)) = (SizeT.v var_len))))
+      (((reveal #nat (length_of var_a)) = (SizeT.v var_len)) &&
+        ((reveal #nat (length_of var_b)) = (SizeT.v var_len))))
   returns return_1 : bool
   ensures exists* (val_a_0: (full_array_spec Int32.t)). ((array_pts_to_full var_a 1.0R val_a_0))
   ensures exists* (val_b_0: (full_array_spec Int32.t)). ((array_pts_to_full var_b 1.0R val_b_0))
-  ensures (with_pure ((reveal (length_of var_a)) = (old (reveal (length_of var_a)))))
-  ensures (with_pure ((reveal (length_of var_b)) = (old (reveal (length_of var_b)))))
+  ensures (with_pure ((reveal #nat (length_of var_a)) = (old (reveal #nat (length_of var_a)))))
+  ensures (with_pure ((reveal #nat (length_of var_b)) = (old (reveal #nat (length_of var_b)))))
   ensures
     (with_pure
       (return_1 =
diff --git base/compare_elements/Func_compare_elems.fsti head/compare_elements/Func_compare_elems.fsti
index 1e6ae76..06a3e3a 100644
--- base/compare_elements/Func_compare_elems.fsti
+++ head/compare_elements/Func_compare_elems.fsti
@@ -8,13 +8,13 @@ requires exists* (val_a_0: (full_array_spec Int32.t)). ((array_pts_to_full var_a
 requires exists* (val_b_0: (full_array_spec Int32.t)). ((array_pts_to_full var_b 1.0R val_b_0))
 requires
   (with_pure
-    (((reveal (length_of var_a)) = (SizeT.v var_len)) &&
-      ((reveal (length_of var_b)) = (SizeT.v var_len))))
+    (((reveal #nat (length_of var_a)) = (SizeT.v var_len)) &&
+      ((reveal #nat (length_of var_b)) = (SizeT.v var_len))))
 returns return_1 : bool
 ensures exists* (val_a_0: (full_array_spec Int32.t)). ((array_pts_to_full var_a 1.0R val_a_0))
 ensures exists* (val_b_0: (full_array_spec Int32.t)). ((array_pts_to_full var_b 1.0R val_b_0))
-ensures (with_pure ((reveal (length_of var_a)) = (old (reveal (length_of var_a)))))
-ensures (with_pure ((reveal (length_of var_b)) = (old (reveal (length_of var_b)))))

Diff truncated; see the links above for the full version.

gebner and others added 3 commits September 24, 2026 00:59

Bump F* to 2026-09-23

f78caf8

ghost_fnptr/call_across_shapes fails with this nightly due to FStarLang/FStar#4587. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Bump F* to 2026-09-25

638900f

Includes the fix for FStarLang/FStar#4587; all tests pass. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

gebner enabled auto-merge September 25, 2026 15:12

gebner added this pull request to the merge queue Sep 25, 2026

Merged via the queue into main with commit 196a913 Sep 25, 2026
4 checks passed

Navigation Menu

Bump F* to nightly 2026-09-25 - #327

Bump F* to nightly 2026-09-25#327
gebner merged 3 commits into
mainfrom
gebner/bump-fstar-2026-09-25

gebner commented Sep 25, 2026

Uh oh!

github-actions Bot commented Sep 25, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

gebner commented Sep 25, 2026

Uh oh!

github-actions Bot commented Sep 25, 2026

Generated F* output diff

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant