module FStar.BufferNG

fsdoc: no-summary-found

fsdoc: no-comment-found

val create:#a:typ -> init:P.type_of_typ a -> len:UInt32.t -> (HST.StackInline (buffer a) ((requires ((fun h -> >(UInt32.v len, 0))))) ((ensures ((fun (h0:HS.mem) b h1 -> /\(/\(/\(/\(/\(/\(>(UInt32.v len, 0), unused_in b h0), live h1 b), ==(length b, UInt32.v len)), ==(frameOf b, (HS.get_tip h0))), P.modifies_0 h0 h1), ==(as_seq h1 b, Seq.create (UInt32.v len) init)))))))

Concrete getters and setters

val blit:Unidentified product: [#t:typ] Unidentified product: [a:buffer t] Unidentified product: [idx_a:UInt32.t] Unidentified product: [b:b:buffer t:{disjoint a b}] Unidentified product: [idx_b:UInt32.t] Unidentified product: [len:len:UInt32.t:{/\(<=(+(UInt32.v idx_a, UInt32.v len), length a), <=(+(UInt32.v idx_b, UInt32.v len), length b))}] (HST.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), P.modifies (P.loc_buffer (gsub b idx_b len)) h0 h1), ==(Seq.slice (as_seq h1 b) (UInt32.v idx_b) (+(UInt32.v idx_b, UInt32.v len)), Seq.slice (as_seq h0 a) (UInt32.v idx_a) (+(UInt32.v idx_a, UInt32.v len)))), ==(Seq.slice (as_seq h1 b) 0 (UInt32.v idx_b), Seq.slice (as_seq h0 b) 0 (UInt32.v idx_b))), ==(Seq.slice (as_seq h1 b) (+(UInt32.v idx_b, UInt32.v len)) (length b), Seq.slice (as_seq h0 b) (+(UInt32.v idx_b, UInt32.v len)) (length b))))))))

Corresponds to memcpy

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

Corresponds to memset