Skip to content

Commit

Permalink
Revert unnecessary ulib changes.
Browse files Browse the repository at this point in the history
  • Loading branch information
@gebner
gebner committed Jan 9, 2025
1 parent ec3ebed commit 21f1655
Show file tree
Hide file tree
Showing 2 changed files with 18 additions and 17 deletions.
19 changes: 10 additions & 9 deletions ulib/FStar.HyperStack.ST.fsti
View file
Original file line number Diff line number Diff line change
Expand Up @@ -324,6 +324,7 @@ val pop_frame (_:unit)
#push-options "--z3rlimit 40"
let salloc_post (#a:Type) (#rel:preorder a) (init:a) (m0:mem)
(s:mreference a rel{is_stack_region (frameOf s)}) (m1:mem)
: GTot prop
= is_stack_region (get_tip m0) /\
Map.domain (get_hmap m0) == Map.domain (get_hmap m1) /\
get_tip m0 == get_tip m1 /\
Expand All @@ -337,14 +338,14 @@ let salloc_post (#a:Type) (#rel:preorder a) (init:a) (m0:mem)
*)
val salloc (#a:Type) (#rel:preorder a) (init:a)
:StackInline (mstackref a rel) (requires (fun m -> is_stack_region (get_tip m)))
(ensures fun m0 r m1 -> salloc_post init m0 r m1)
(ensures salloc_post init)

// JP, AR: these are not supported in C, and `salloc` already benefits from
// automatic memory management.
[@@ (deprecated "Use salloc instead") ]
val salloc_mm (#a:Type) (#rel:preorder a) (init:a)
:StackInline (mmmstackref a rel) (requires (fun m -> is_stack_region (get_tip m)))
(ensures fun m0 r m1 -> salloc_post init m0 r m1)
(ensures salloc_post init)

[@@ (deprecated "Use salloc instead") ]
val sfree (#a:Type) (#rel:preorder a) (r:mmmstackref a rel)
Expand Down Expand Up @@ -378,7 +379,7 @@ val new_colored_region (r0:rid) (c:int)
(r1, m1) == HS.new_eternal_region m0 r0 (Some c)))

let ralloc_post (#a:Type) (#rel:preorder a) (i:rid) (init:a) (m0:mem)
(x:mreference a rel) (m1:mem) =
(x:mreference a rel) (m1:mem) : GTot prop =
let region_i = get_hmap m0 `Map.sel` i in
as_ref x `Heap.unused_in` region_i /\
i `is_in` get_hmap m0 /\
Expand All @@ -387,11 +388,11 @@ let ralloc_post (#a:Type) (#rel:preorder a) (i:rid) (init:a) (m0:mem)

val ralloc (#a:Type) (#rel:preorder a) (i:rid) (init:a)
:ST (mref a rel) (requires (fun m -> is_eternal_region i))
(ensures fun m0 r m1 -> ralloc_post i init m0 r m1)
(ensures (ralloc_post i init))

val ralloc_mm (#a:Type) (#rel:preorder a) (i:rid) (init:a)
:ST (mmmref a rel) (requires (fun m -> is_eternal_region i))
(ensures fun m0 r m1 -> ralloc_post i init m0 r m1)
(ensures (ralloc_post i init))

(*
* AR: 12/26: For a ref to be readable/writable/free-able,
Expand All @@ -408,7 +409,7 @@ val rfree (#a:Type) (#rel:preorder a) (r:mreference a rel{HS.is_mm r /\ HS.is_he
:ST unit (requires (fun m0 -> r `is_live_for_rw_in` m0))
(ensures (fun m0 _ m1 -> m0 `contains` r /\ m1 == HS.free r m0))

unfold let assign_post (#a:Type) (#rel:preorder a) (r:mreference a rel) (v:a) (m0:mem) (_:unit) (m1:mem) =
unfold let assign_post (#a:Type) (#rel:preorder a) (r:mreference a rel) (v:a) (m0:mem) (_:unit) (m1:mem) : GTot prop =
m0 `contains` r /\ m1 == HyperStack.upd m0 r v

(**
Expand All @@ -417,9 +418,9 @@ unfold let assign_post (#a:Type) (#rel:preorder a) (r:mreference a rel) (v:a) (m
*)
val op_Colon_Equals (#a:Type) (#rel:preorder a) (r:mreference a rel) (v:a)
:STL unit (requires (fun m -> r `is_live_for_rw_in` m /\ rel (HS.sel m r) v))
(ensures fun m0 _ m1 -> assign_post r v m0 () m1)
(ensures (assign_post r v))

unfold let deref_post (#a:Type) (#rel:preorder a) (r:mreference a rel) (m0:mem) (x:a) (m1:mem) =
unfold let deref_post (#a:Type) (#rel:preorder a) (r:mreference a rel) (m0:mem) (x:a) (m1:mem) : GTot prop =
m1 == m0 /\ m0 `contains` r /\ x == HyperStack.sel m0 r

(**
Expand All @@ -428,7 +429,7 @@ unfold let deref_post (#a:Type) (#rel:preorder a) (r:mreference a rel) (m0:mem)
*)
val op_Bang (#a:Type) (#rel:preorder a) (r:mreference a rel)
:Stack a (requires (fun m -> r `is_live_for_rw_in` m))
(ensures fun m0 x m1 -> deref_post r m0 x m1)
(ensures (deref_post r))

let modifies_none (h0:mem) (h1:mem) = modifies Set.empty h0 h1

Expand Down
16 changes: 8 additions & 8 deletions ulib/LowStar.Endianness.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -113,7 +113,7 @@ assume val store16_le_i
(z:u16)
: Stack unit
(requires (store_pre b (U32.v i) 2 (fun s -> le_to_n s == U16.v z)))
(ensures fun h0 r h1 -> (store_post b (U32.v i) 2 (fun s -> le_to_n s == U16.v z)) h0 r h1)
(ensures (store_post b (U32.v i) 2 (fun s -> le_to_n s == U16.v z)))

assume val load16_le_i
(#rrel #rel:MB.srel u8) (b:MB.mbuffer u8 rrel rel)
Expand All @@ -131,7 +131,7 @@ assume val store16_be_i
(z:u16)
: Stack unit
(requires (store_pre b (U32.v i) 2 (fun s -> be_to_n s == U16.v z)))
(ensures fun h0 r h1 -> (store_post b (U32.v i) 2 (fun s -> be_to_n s == U16.v z)) h0 r h1)
(ensures (store_post b (U32.v i) 2 (fun s -> be_to_n s == U16.v z)))

assume val load16_be_i
(#rrel #rel:MB.srel u8) (b:MB.mbuffer u8 rrel rel)
Expand All @@ -149,7 +149,7 @@ assume val store32_le_i
(z:u32)
: Stack unit
(requires (store_pre b (U32.v i) 4 (fun s -> le_to_n s == U32.v z)))
(ensures fun h0 r h1 -> (store_post b (U32.v i) 4 (fun s -> le_to_n s == U32.v z)) h0 r h1 )
(ensures (store_post b (U32.v i) 4 (fun s -> le_to_n s == U32.v z)))

assume val load32_le_i
(#rrel #rel:MB.srel u8) (b:MB.mbuffer u8 rrel rel)
Expand All @@ -167,7 +167,7 @@ assume val store32_be_i
(z:u32)
: Stack unit
(requires (store_pre b (U32.v i) 4 (fun s -> be_to_n s == U32.v z)))
(ensures fun h0 r h1 -> (store_post b (U32.v i) 4 (fun s -> be_to_n s == U32.v z)) h0 r h1 )
(ensures (store_post b (U32.v i) 4 (fun s -> be_to_n s == U32.v z)))

assume val load32_be_i
(#rrel #rel:MB.srel u8) (b:MB.mbuffer u8 rrel rel)
Expand All @@ -185,7 +185,7 @@ assume val store64_le_i
(z:u64)
: Stack unit
(requires (store_pre b (U32.v i) 8 (fun s -> le_to_n s == U64.v z)))
(ensures fun h0 r h1 -> (store_post b (U32.v i) 8 (fun s -> le_to_n s == U64.v z)) h0 r h1 )
(ensures (store_post b (U32.v i) 8 (fun s -> le_to_n s == U64.v z)))

assume val load64_le_i
(#rrel #rel:MB.srel u8) (b:MB.mbuffer u8 rrel rel)
Expand All @@ -203,7 +203,7 @@ assume val store64_be_i
(z:u64)
: Stack unit
(requires (store_pre b (U32.v i) 8 (fun s -> be_to_n s == U64.v z)))
(ensures fun h0 r h1 -> (store_post b (U32.v i) 8 (fun s -> be_to_n s == U64.v z)) h0 r h1 )
(ensures (store_post b (U32.v i) 8 (fun s -> be_to_n s == U64.v z)))

assume val load64_be_i
(#rrel #rel:MB.srel u8) (b:MB.mbuffer u8 rrel rel)
Expand All @@ -221,7 +221,7 @@ assume val store128_le_i
(z:u128)
: Stack unit
(requires (store_pre b (U32.v i) 16 (fun s -> le_to_n s == U128.v z)))
(ensures fun h0 r h1 -> (store_post b (U32.v i) 16 (fun s -> le_to_n s == U128.v z)) h0 r h1 )
(ensures (store_post b (U32.v i) 16 (fun s -> le_to_n s == U128.v z)))

assume val load128_le_i
(#rrel #rel:MB.srel u8) (b:MB.mbuffer u8 rrel rel)
Expand All @@ -239,7 +239,7 @@ assume val store128_be_i
(z:u128)
: Stack unit
(requires (store_pre b (U32.v i) 16 (fun s -> be_to_n s == U128.v z)))
(ensures fun h0 r h1 -> (store_post b (U32.v i) 16 (fun s -> be_to_n s == U128.v z)) h0 r h1 )
(ensures (store_post b (U32.v i) 16 (fun s -> be_to_n s == U128.v z)))


assume val load128_be_i
Expand Down

0 comments on commit 21f1655

Please sign in to comment.