let ((lemma_modifies_2_comm (#a:Type) (#a':Type) (b:buffer a) (b':buffer a') h0 h1):(Lemma ((requires True)) ((ensures (<==>(modifies_2 b b' h0 h1, modifies_2 b' b h0 h1)))) (Prims.Cons (SMTPat (modifies_2 b b' h0 h1)) (Prims.Nil )))):()

let ((lemma_modifies_0_trans h0 h1 h2):(Lemma ((requires (/\(modifies_0 h0 h1, modifies_0 h1 h2)))) ((ensures (modifies_0 h0 h2))) (Prims.Cons (SMTPat (modifies_0 h0 h1)) (Prims.Cons (SMTPat (modifies_0 h1 h2)) (Prims.Nil ))))):()

val create:Unidentified product: [#a:Type] Unidentified product: [init:a] Unidentified product: [len:UInt32.t] (StackInline (buffer a) ((requires ((fun h -> True)))) ((ensures ((fun (h0:mem) b h1 -> /\(/\(/\(/\(/\(/\(/\(unused_in b h0, live h1 b), ==(idx b, 0)), ==(length b, v len)), ==(frameOf b, HS.get_tip h0)), ==(Map.domain (HS.get_hmap h1), Map.domain (HS.get_hmap h0))), modifies_0 h0 h1), ==(as_seq h1 b, Seq.create (v len) init)))))))

val createL:Unidentified product: [#a:Type0] Unidentified product: [init:list a] (StackInline (buffer a) ((requires ((fun h -> p #a init)))) ((ensures ((fun (h0:mem) b h1 -> let  len = FStar.List.Tot.length init in /\(/\(/\(/\(/\(/\(/\(/\(/\(>(len, 0), unused_in b h0), live h1 b), ==(idx b, 0)), ==(length b, len)), ==(frameOf b, (HS.get_tip h0))), ==(Map.domain (HS.get_hmap h1), Map.domain (HS.get_hmap h0))), modifies_0 h0 h1), ==(as_seq h1 b, Seq.seq_of_list init)), q #a len b))))))

val rcreate:Unidentified product: [#a:Type] Unidentified product: [r:rid] Unidentified product: [init:a] Unidentified product: [len:UInt32.t] (ST (buffer a) ((requires ((fun h -> is_eternal_region r)))) ((ensures ((fun (h0:mem) b h1 -> /\(rcreate_post_common r init len b h0 h1, ~((is_mm b.content))))))))

This function allocates a buffer in an "eternal" region, i.e. a region where memory is // * automatically-managed. One does not need to call rfree on such a buffer. It // * translates to C as a call to malloc and assumes a conservative garbage // * collector is runnning.

let ((freeable (#a:Type) (b:buffer a)):(GTot Type0)):/\(/\(is_mm b.content, is_eternal_region (frameOf b)), ==(idx b, 0))

This predicate tells whether a buffer can be rfreed. The only way to produce it should be rcreate_mm, and the only way to consume it should be rfree. Rationale: a buffer can be rfreed only if it is the result of rcreate_mm. Subbuffers should not.

let ((rcreate_mm (#a:Type) (r:rid) (init:a) (len:UInt32.t)):(ST (buffer a) ((requires ((fun h0 -> is_eternal_region r)))) ((ensures ((fun h0 b h1 -> /\(/\(rcreate_post_common r init len b h0 h1, is_mm (content b)), freeable b))))))):rcreate_common r init len true

This function allocates a buffer into a manually-managed buffer in a heap * region, meaning that the client must call rfree in order to avoid memory * leaks. It translates to C as a straight malloc.

let ((rfree (#a:Type) (b:buffer a)):(ST unit ((requires ((fun h0 -> /\(live h0 b, freeable b))))) ((ensures ((fun h0 _ h1 -> /\(/\(is_mm (content b), is_eternal_region (frameOf b)), ==(h1, HS.free (content b) h0)))))))):rfree b.content

This function frees a buffer allocated with rcreate_mm. It translates to C as a regular free.

let ((lemma_aux_0 (#a:Type) (b:buffer a) (n:n:UInt32.t:{<(v n, length b)}) (z:a) (h0:mem) (tt:Type) (bb:buffer tt)):(Lemma ((requires (/\(/\(live h0 b, live h0 bb), disjoint b bb)))) ((ensures (/\(/\(live h0 b, live h0 bb), (let  h1 = HS.upd h0 b.content (Seq.upd (sel h0 b) (+(idx b, v n)) z) in ==(as_seq h0 bb, as_seq h1 bb)))))))):Heap.lemma_distinct_addrs_distinct_preorders (); Heap.lemma_distinct_addrs_distinct_mm ()

REMARK: the proof of this lemma relies crucially on the a == a' condition // in disjoint, and on the pattern in Seq.slice_upd

val eqb:Unidentified product: [#a:eqtype] Unidentified product: [b1:buffer a] Unidentified product: [b2:buffer a] Unidentified product: [len:len:UInt32.t:{/\(<=(v len, length b1), <=(v len, length b2))}] (ST bool ((requires ((fun h -> /\(live h b1, live h b2))))) ((ensures ((fun h0 z h1 -> /\(==(h1, h0), (<==>(z, equal h0 (sub b1 0 len) h0 (sub b2 0 len)))))))))

val op_Array_Access:Unidentified product: [#a:Type] Unidentified product: [b:buffer a] Unidentified product: [n:n:UInt32.t:{<(v n, length b)}] (Stack a ((requires ((fun h -> live h b)))) ((ensures ((fun h0 z h1 -> /\(==(h1, h0), ==(z, Seq.index (as_seq h0 b) (v n))))))))

// Defining operators for buffer accesses as specified at // https://github.com/FStarLang/FStar/wiki/Parsing-and-operator-precedence //

val blit:Unidentified product: [#t:Type] Unidentified product: [a:buffer t] Unidentified product: [idx_a:idx_a:UInt32.t:{<=(v idx_a, length a)}] Unidentified product: [b:b:buffer t:{disjoint a b}] Unidentified product: [idx_b:idx_b:UInt32.t:{<=(v idx_b, length b)}] Unidentified product: [len:len:UInt32.t:{/\(<=(+(v idx_a, v len), length a), <=(+(v idx_b, v len), length b))}] (Stack unit ((requires ((fun h -> /\(live h a, live h b))))) ((ensures ((fun h0 _ h1 -> /\(/\(/\(/\(/\(/\(/\(live h0 b, live h0 a), live h1 b), live h1 a), modifies_1 b h0 h1), ==(Seq.slice (as_seq h1 b) (v idx_b) (+(v idx_b, v len)), Seq.slice (as_seq h0 a) (v idx_a) (+(v idx_a, v len)))), ==(Seq.slice (as_seq h1 b) 0 (v idx_b), Seq.slice (as_seq h0 b) 0 (v idx_b))), ==(Seq.slice (as_seq h1 b) (+(v idx_b, v len)) (length b), Seq.slice (as_seq h0 b) (+(v idx_b, v len)) (length b))))))))

val fill:Unidentified product: [#t:Type] Unidentified product: [b:buffer t] Unidentified product: [z:t] Unidentified product: [len:len:UInt32.t:{<=(v len, length b)}] (Stack unit ((requires ((fun h -> live h b)))) ((ensures ((fun h0 _ h1 -> /\(/\(/\(/\(live h0 b, live h1 b), modifies_1 b h0 h1), ==(Seq.slice (as_seq h1 b) 0 (v len), Seq.create (v len) z)), ==(Seq.slice (as_seq h1 b) (v len) (length b), Seq.slice (as_seq h0 b) (v len) (length b))))))))

module FStar.Buffer