nikswamy
nikswamy
If one writes `UINT32 t[:byte-size n]`, we actually generate a while-loop to validate each UINT32 advancing by 4 bytes each time. This is inefficient, since one could instead just check...
I sporadically get these warnings: ``` Warning (emacs): Unknown status "protocol-violation" from F* subprocess (response was ["JSON decoding failed: expected string, got null"]) Warning (emacs): Unknown status "protocol-violation" from F*...
```fstar type value = bool let rec array_cmp (l1:list value) (l2:list value) : bool = match l1, l2 with | hd1::tl1, hd2::tl2 -> array_cmp tl1 tl2 | _ -> false...
1. Fails pointing to the equality and claiming that an SMT query failed ```pulse fn value_of (#a:Type) (r:ref a) requires pts_to r 'v returns v:a ensures pts_to r 'v **...
We need a way to distinguish stack references vs heap references to prevent the user from trying to call free on a stack-allocated ref
Reflecting a conversation with @mtzguido We are consider a three-point lattice of Ghost < Unobservable < Atomic and indexing a new Pulse computation type with these labels as follows: ```...
The checker eagerly eliminates `pure _` in the vprop context, but only if the `pure _` is not hidden beneath a binder. This leads to surprises, explaining the two surprises...
* Add support for Dv and general recursion in FStar.Reflection.Typing * Add a typing rule for Pulse recursion targeting the Dv rule in reflection typing.
Pulse issues separate SMT queries for every proof obligation, effectively behaving like `--split_queries always`. This can be needlessly slow when a program has many small queries. We should add support...
```pulse fn initialize_context' (sid:sid_t) (uds:A.larray U8.t (US.v uds_len)) (#p:perm) (#uds_bytes:Ghost.erased (Seq.seq U8.t)) requires A.pts_to uds #p uds_bytes returns _:option ctxt_hndl_t ensures A.pts_to uds #p uds_bytes { rewrite emp as (session_state_perm...