nikswamy

This unusual way of writing a dependent pair: ``` module TT let test (a: Type) (b: (a → Type)) (y: (v: a) & b v) = () ``` is accepted...

Meta-issue: Steel inference, framing, and selectors

4

- [x] Move all modules to use the PCM-based memory model (Nik) - [x] Revise the formulation of frame preservation and remove the assume Steel.Effect.Atomic.witness_h_exists (Aseem) - [ ] Add...

F* seems to diverge on this example consuming a lot of memory

1

https://github.com/FStarLang/FStar/blob/master/ulib/experimental/Steel.FractionalAnchoredPreorder.fst#L485

This may be related to the unfolding behavior of vprops. Could it be remedied by using strict_on_arguments? ``` module AVP open FStar.Ghost open Steel.FractionalPermission open Steel.Memory open Steel.Effect.Atomic open Steel.Effect...

When writing Steel specifications in selector style, the specifications themselves need to be framed. Consider this: First some general scaffolding for a test case, defining an abstract indexed vprop `p...

Consider this program: ``` module Repro open Proj assume val t : nat -> Type0 noeq type test = { x:nat; y:t x; } %splice[x_of_test; y_of_test] (mk_projs (`%test) ["x_of_test"; "y_of_test"])...

A memory and data model for miTLS

2

We have in several related branches a prototype implementation of the miTLS memory model https://github.com/mitls/mitls-papers/wiki/The-Memory-Model-of-miTLS (private link) To merge this into the no_hsl branch of miTLS the following work items...

The end of TLSConstants defines a type called config. It contains both - ordinary configuration data - and application callbacks, e.g., ticket_callback, nego_callback, etc. This is passed to create a...

Within TLS, there are several uses of internally determined encryption constructions. For instance, to represent PSK identifiers, we choose an encrypted blob `{ PSK keyid info }K-seal` to represent a...