wip

cryspen · Mar 24, 2024 · 97c8405 · 97c8405
1 parent f5a5766
commit 97c8405
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 0 deletions.
diff --git a/proof-libs/fstar/core/Core.Num.fsti b/proof-libs/fstar/core/Core.Num.fsti
@@ -4,6 +4,7 @@ open Rust_primitives
 let impl__u8__wrapping_add: u8 -> u8 -> u8 = add_mod
 let impl__u8__wrapping_sub: u8 -> u8 -> u8 = sub_mod
 let impl__u16__wrapping_add: u16 -> u16 ->  u16 = add_mod
+val impl__u16__to_be_bytes: u16 -> t_Array u8 (sz 2)
 let impl__i32__wrapping_add: i32 -> i32 -> i32 = add_mod
 let impl__i32__abs (a:i32{minint i32_inttype < v a}) : i32 = abs_int a
 

diff --git a/proof-libs/fstar/core/Core.Slice.fsti b/proof-libs/fstar/core/Core.Slice.fsti
@@ -33,3 +33,6 @@ val impl__split_at #t (s: t_Slice t) (mid: usize): Pure (t_Slice t * t_Slice t)
     (ensures (fun (x,y) -> Seq.length x == v mid /\ Seq.length y == Seq.length s - v mid /\
                         x == Seq.slice s 0 (v mid) /\ y == Seq.slice s (v mid) (Seq.length s) /\
                         s == Seq.append x y))
+
+let impl__is_empty (s: t_Slice 'a): bool = Seq.length s = 0
+