add alloc_from_start to paper example 1

examples/paper_example_2_1.c

@@ -16,21 +16,35 @@
 //@Coercion byte_layout : nat >-> layout.
 //@rc::end
 
-struct [[rc::refined_by("a : nat")]] mem_t {
+struct [[rc::refined_by("a: nat")]] mem_t {
   [[rc::field("a @ int<size_t>")]] size_t len;
-  [[rc::field("&own<uninit<a>>")]] unsigned char *buffer;
+  [[rc::field("&own<uninit<a>>")]] unsigned char* buffer;
 };
 
-[[rc::parameters("a : nat", "n : nat", "p : loc")]]
+[[rc::parameters("a: nat", "n: nat", "p: loc")]]
 [[rc::args   ("p @ &own<a @ mem_t>", "n @ int<size_t>")]]
 [[rc::returns("{n ≤ a} @ optional<&own<uninit<n>>, null>")]]
 [[rc::ensures("own p : {n ≤ a ? a - n : a} @ mem_t")]]
-void *alloc(struct mem_t *d, size_t size) {
-  if(size > d->len) return NULL;
-  d->len -= size;
+void* alloc(struct mem_t* d, size_t sz) {
+  if(sz > d->len) return NULL;
+  d->len -= sz;
   return d->buffer + d->len;
 }
 
+// variant of alloc that allocates from the start of buffer instead of the end
+
+[[rc::parameters("a: nat", "n: nat", "p: loc")]]
+[[rc::args   ("p @ &own<a @ mem_t>", "n @ int<size_t>")]]
+[[rc::returns("{n ≤ a} @ optional<&own<uninit<n>>, null>")]]
+[[rc::ensures("own p : {n ≤ a ? a - n : a} @ mem_t")]]
+void* alloc_from_start(struct mem_t* d, size_t sz) {
+  if(sz > d->len) return NULL;
+  d->len -= sz;
+  unsigned char *res = d->buffer;
+  d->buffer += sz;
+  return res;
+}
+
 // Thread-safe version (given in appendix).
 
 [[rc::parameters("lid : lock_id")]]

examples/proofs/paper_example_2_1/generated_proof_alloc.v

@@ -14,7 +14,7 @@ Section proof_alloc.
     ⊢ typed_function impl_alloc type_of_alloc.
   Proof.
     Open Scope printing_sugar.
-    start_function "alloc" ([[a n] p]) => arg_d arg_size.
+    start_function "alloc" ([[a n] p]) => arg_d arg_sz.
     split_blocks ((
       ∅
     )%I : gmap label (iProp Σ)) ((

examples/proofs/paper_example_2_1/generated_proof_alloc_from_start.v

+From refinedc.typing Require Import typing.
+From refinedc.examples.paper_example_2_1 Require Import generated_code.
+From refinedc.examples.paper_example_2_1 Require Import generated_spec.
+From refinedc.examples.spinlock Require Import spinlock_def.
+Set Default Proof Using "Type".
+
+(* Generated from [examples/paper_example_2_1.c]. *)
+Section proof_alloc_from_start.
+  Context `{!typeG Σ} `{!globalG Σ}.
+  Context `{!lockG Σ}.
+
+  (* Typing proof for [alloc_from_start]. *)
+  Lemma type_alloc_from_start :
+    ⊢ typed_function impl_alloc_from_start type_of_alloc_from_start.
+  Proof.
+    Open Scope printing_sugar.
+    start_function "alloc_from_start" ([[a n] p]) => arg_d arg_sz local_res.
+    split_blocks ((
+      ∅
+    )%I : gmap label (iProp Σ)) ((
+      ∅
+    )%I : gmap label (iProp Σ)).
+    - repeat liRStep; liShow.
+      all: print_typesystem_goal "alloc_from_start" "#0".
+    Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
+    all: print_sidecondition_goal "alloc_from_start".
+  Qed.
+End proof_alloc_from_start.

examples/proofs/paper_example_2_1/generated_spec.v

@@ -92,6 +92,11 @@ Section spec.
     fn(∀ (a, n, p) : nat * nat * loc; (p @ (&own (a @ (mem_t)))), (n @ (int (size_t))); True)
       → ∃ () : (), ((n ≤ a) @ (optional (&own (uninit (n))) (null))); (p ◁ₗ ((n ≤ a ? a - n : a) @ (mem_t))).
 
+  (* Specifications for function [alloc_from_start]. *)
+  Definition type_of_alloc_from_start :=
+    fn(∀ (a, n, p) : nat * nat * loc; (p @ (&own (a @ (mem_t)))), (n @ (int (size_t))); True)
+      → ∃ () : (), ((n ≤ a) @ (optional (&own (uninit (n))) (null))); (p ◁ₗ ((n ≤ a ? a - n : a) @ (mem_t))).
+
   (* Specifications for function [thread_safe_alloc]. *)
   Definition type_of_thread_safe_alloc :=
     fn(∀ (lid, n) : lock_id * nat; (n @ (int (size_t))); (initialized "lock" lid) ∗ (initialized "data" lid))

examples/proofs/paper_example_2_1/proof_files

 generated_proof_alloc.v
+generated_proof_alloc_from_start.v
 generated_proof_atomic_signal_fence.v
 generated_proof_atomic_thread_fence.v
 generated_proof_fork.v