Some comments

share/steel/examples/pulse/dice/common/HashTable.fst

@@ -28,25 +28,49 @@ type ht_sig = {
 
 let mk_ht_sig sz kt vt hashf = { sz; kt; vt; hashf }
 
-noeq
-type ht_t (s:ht_sig) = {
-  contents : A.larray (cell s.kt s.vt) s.sz;
-}
+// No functional correctness specs yet
+
+assume val ht_t (s:ht_sig) : Type0
+
+assume val ht_perm (#s:ht_sig) (tbl:ht_t s) : vprop
+
+// when we add functional correctness the lock permission will reflect it
+type ht_ref_t (s:ht_sig) = tbl:ht_t s & L.lock (ht_perm s)
+
+// noeq
+// type ht_t (s:ht_sig) = {
+//   contents : A.larray (cell s.kt s.vt) s.sz;
+// }
 
 // check out ephemeral ht itf
-type ht_ref_t (s:ht_sig) = r:R.ref (ht_t s) & L.lock (exists_ (fun ht -> R.pts_to r full_perm ht))
+// type ht_ref_t (s:ht_sig) = r:R.ref (ht_t s) & L.lock (exists_ (fun ht -> R.pts_to r full_perm ht))
 
 // Hash table interface
 
-assume val new_table (#s:ht_sig) : ht_t s
+assume val new_table (s:ht_sig)
+  : stt (ht_t s) emp (ht_perm #s)
+
+assume val store (#s:ht_sig) (tbl:ht_t s) (k:s.kt) (v:s.vt)
+  : stt unit (ht_perm tbl) (ht_perm tbl)
+
+assume val get #s (tbl:ht_t s) (k:s.kt)
+  : stt (option s.vt) (ht_perm tbl) (ht_perm tbl)
+
+assume val delete #s (tbl:ht_t s) (k:s.kt)
+  : stt unit (ht_perm tbl) (ht_perm tbl)
+
+assume val destroy #s (tbl:ht_t s)
+  : stt unit (ht_perm tbl) (fun _ -> emp)
+
+// assume val new_table (#s:ht_sig) : ht_t s
 
-assume val store (#s:ht_sig) (ht:ht_t s) (k:s.kt) (v:s.vt) : unit
+// assume val store (#s:ht_sig) (ht:ht_t s) (k:s.kt) (v:s.vt) : unit
 
-assume val get (#s:ht_sig) (ht:ht_t s) (k:s.kt) : s.vt
+// assume val get (#s:ht_sig) (ht:ht_t s) (k:s.kt) : s.vt
 
-assume val delete (#s:ht_sig) (ht:ht_t s) (k:s.kt) : unit
+// assume val delete (#s:ht_sig) (ht:ht_t s) (k:s.kt) : unit
 
-assume val destroy (#s:ht_sig) (ht:ht_t s) : unit
+// assume val destroy (#s:ht_sig) (ht:ht_t s) : unit
 
 // Session ID types
 

share/steel/examples/pulse/dice/dpe/DPE.fst

@@ -25,6 +25,10 @@ friend Pulse.Steel.Wrapper
 
 (* L1 Context -- to be moved *)
 
+//
+// I think we should also store public keys,
+//   and device ID keys in the context
+//
 noeq
 type l1_context = { aliasKey_priv: A.larray U8.t 32;
                     aliasKeyCRT: A.array U8.t;
@@ -69,6 +73,17 @@ type repr_t =
   | Engine_repr : r:engine_record_repr -> repr_t
   | L0_repr     : r:l0_record_repr -> repr_t
 
+//
+// An alternative style here would be to write it as:
+// let record_perm (t_rec : record_t) : vprop =
+//   match t_rec with
+//   | Engine_record r ->
+//     (exists s. pts_to r.l0_image_header s) *
+//     ...
+//
+// I wonder what are the pros and cons
+// Perhaps a record repr makes it easier to keep pure invariants?
+//
 let record_perm (t_rec:record_t) (t_rep:repr_t) : vprop = 
   match t_rec with
   | Engine_record r -> (
@@ -98,6 +113,12 @@ fn alloc_ht (#s:ht_sig)
   returns _:ht_ref_t s
   ensures emp
 {
+  //
+  // since the table is imperative,
+  // we will just call create table here,
+  //   which will return us a table and its permission
+  // we will add the permission to the lock as we are doing below
+  //
   let ht = new_table #s;
   let ht_ref = W.alloc #(ht_t s) ht;
   let lk = W.new_lock (exists_ (fun _ht -> R.pts_to ht_ref full_perm _ht));
@@ -176,6 +197,11 @@ fn close_session (sid:nat)
   W.acquire #(exists_ (fun n -> R.pts_to (dfst cht_ref) full_perm n)) l_cht;
   let cht = !(dfst cht_ref);
 
+  //
+  // in the imperative table spec,
+  // we will call destroy (releasing memory) and then the permissions will go away
+  // so we won't have to call W.release
+  //
   destroy cht;
   W.release #(exists_ (fun n -> R.pts_to (dfst cht_ref) full_perm n)) l_cht;
 
@@ -184,7 +210,12 @@ fn close_session (sid:nat)
 }
 ```
 
-// TODO: 
+//
+// TODO:
+//
+// we should type it as a stateful function,
+// else the solver may reason that it will always return the same value
+// 
 assume val prng (_:unit) : nat
 
 ```pulse
@@ -280,9 +311,21 @@ fn init_l1_ctxt (aliasKey_priv: A.larray U8.t 32) (aliasKeyCRT: A.array U8.t) (d
   Create a context in the initial state (engine context) and store the context
   in the current session's context table. 
 *)
+
+//
+// I think we should copy the array in DPE state,
+//   i.e. create a new UDS array, copy the contents,
+//   and store the new array on our state
+//
+// I am thinking cases  when DPE is running inside isolated
+//   environments
+//
+// (If we do so, we only need read-only permission on the input array.)
+//
+
 ```pulse
 fn initialize_context (sid:nat) (uds:A.larray U8.t (US.v uds_len))
-  requires (
+  requires 
     A.pts_to uds full_perm uds_bytes ** 
     uds_is_enabled **
     pure (A.is_full_array uds)