changes for nuking Monotonic.RRef

project-everest · Dec 28, 2017 · 73299b7 · 73299b7
1 parent 16e286d
commit 73299b7
Show file tree

Hide file tree

Showing 5 changed files with 22 additions and 25 deletions.
diff --git a/src/tls/AEADOpenssl.fst b/src/tls/AEADOpenssl.fst
@@ -10,7 +10,6 @@ open TLSConstants
 open TLSInfo
 
 module MM = FStar.Monotonic.Map
-module MR = FStar.Monotonic.RRef
 module HS = FStar.HyperStack
 
 type id = i:id{~(PlaintextID? i) /\ AEAD? (aeAlg_of_id i)}

diff --git a/src/tls/Nonce.fst b/src/tls/Nonce.fst
@@ -6,7 +6,6 @@ open FStar.HyperStack.ST
 
 module HS = FStar.HyperStack
 module MM = FStar.Monotonic.Map
-module MR = FStar.Monotonic.RRef
 module ST = FStar.HyperStack.ST
 
 type random = lbytes 32
@@ -23,7 +22,7 @@ let timestamp () =
 
 // ex_rid: The type of a region id that is known 
 //         to exist in the current heap and in every future one
-type ex_rid = MR.ex_rid
+type ex_rid = ST.ex_rid
 
 // MM.map provide a dependent map type; 
 // In this case, we don't need the dependencey
@@ -56,18 +55,18 @@ let fresh_region (r:ex_rid) (h:HS.mem) =
   forall n. Some r <> MM.sel (HS.sel h nonce_rid_table) n 
 
 //A nonce n is registered to region r, if the table contains n -> Some r; 
-//This mapping is stable (that's what the MR.witnessed means)
-let registered (n:random) (r:MR.rid) = 
-  witnessed (MR.rid_exists r) /\
+//This mapping is stable (that's what the witnessed means)
+let registered (n:random) (r:ST.erid) = 
+  witnessed (ST.region_contains_pred r) /\
   witnessed (MM.contains nonce_rid_table n r)
 
-let testify (n:random) (r:MR.rid)
+let testify (n:random) (r:ST.erid)
   : ST unit (requires (fun h -> registered n r))
 	    (ensures (fun h0 _ h1 -> 
 		 h0==h1 /\
 	         registered n r /\ 
 		 MM.contains nonce_rid_table n r h1))
-  = MR.testify (MM.contains nonce_rid_table n r)
+  = testify (MM.contains nonce_rid_table n r)
 
 //Although the table only maps nonces to rids, externally, we also 
 //want to associate the nonce with a role. Within this module
@@ -105,7 +104,7 @@ let lookup role n = MM.lookup nonce_rid_table n
 (* Would be nice to make this a local let in new_region.
    Except, implicit argument inference for testify_forall fails *)
 private let nonce_rids_exists  (m:MM.map' random n_rid) = 
-    forall (n:random{Some? (MM.sel m n)}). witnessed (MR.rid_exists (Some?.v (MM.sel m n)))
+    forall (n:random{Some? (MM.sel m n)}). witnessed (ST.region_contains_pred (Some?.v (MM.sel m n)))
 
 (* 
    A convenient wrapper around FStar.ST.new_region, 
@@ -115,7 +114,7 @@ private let nonce_rids_exists  (m:MM.map' random n_rid) =
    underneath quantifiers. So, one should really use this version of new_region 
    for every dynamic region allocation in TLS.
 *)   
-val new_region: parent:MR.rid -> ST ex_rid 
+val new_region: parent:ST.erid -> ST ex_rid 
   (requires (fun h -> True))
   (ensures (fun h0 r h1 -> 
 	      HS.extends r parent /\
@@ -125,8 +124,10 @@ let new_region parent =
   recall nonce_rid_table;
   let m0 = !nonce_rid_table in 
   let tok : squash (nonce_rids_exists m0) = () in   
-  MR.testify_forall tok;
-  MR.ex_rid_of_rid (new_region parent)
+  testify_forall tok;
+  let r = new_region parent in
+  ST.witness_region r;
+  r
 
 // a constant value, with negligible probability of being sampled, excluded by idealization
 let noCsr : bytes = CoreCrypto.random 64 

diff --git a/src/tls/PSK.fst b/src/tls/PSK.fst
@@ -10,7 +10,6 @@ open TLSError
 open TLSConstants
 
 module MM = FStar.Monotonic.Map
-module MR = FStar.Monotonic.RRef
 module HS = FStar.HyperStack
 module ST = FStar.HyperStack.ST
 
@@ -78,7 +77,7 @@ let psk_value (i:pskid) : ST (app_psk i)
   (ensures (fun h0 _ h1 -> modifies_none h0 h1))
   =
   recall app_psk_table;
-  MR.testify (MM.defined app_psk_table i);
+  testify (MM.defined app_psk_table i);
   match MM.lookup app_psk_table i with
   | Some (psk, _, _) -> psk
 
@@ -87,7 +86,7 @@ let psk_info (i:pskid) : ST (pskInfo)
   (ensures (fun h0 _ h1 -> modifies_none h0 h1))
   =
   recall app_psk_table;
-  MR.testify (MM.defined app_psk_table i);
+  testify (MM.defined app_psk_table i);
   match MM.lookup app_psk_table i with
   | Some (_, ctx, _) -> ctx
 
@@ -100,8 +99,8 @@ let psk_lookup (i:psk_identifier) : ST (option pskInfo)
   recall app_psk_table;
   match MM.lookup app_psk_table i with
   | Some (_, ctx, _) ->
-    assume(MR.stable_on_t app_psk_table (MM.defined app_psk_table i));
-    MR.witness app_psk_table (MM.defined app_psk_table i);
+    assume(stable_on_t app_psk_table (MM.defined app_psk_table i));
+    mr_witness app_psk_table (MM.defined app_psk_table i);
     Some ctx
   | None -> None
 
@@ -141,8 +140,8 @@ let gen_psk (i:psk_identifier) (ctx:pskInfo)
   MM.contains_stable app_psk_table i add;
   let h = get () in
   cut(MM.sel (sel h app_psk_table) i == Some add);
-  assume(MR.stable_on_t app_psk_table (honest_st i));
-  MR.witness app_psk_table (honest_st i)
+  assume(stable_on_t app_psk_table (honest_st i));
+  mr_witness app_psk_table (honest_st i)
 
 let coerce_psk (i:psk_identifier) (ctx:pskInfo) (k:app_psk i)
   : ST unit
@@ -181,7 +180,7 @@ let verify_hash_ae (i:pskid) (ha:hash_alg) (ae:aeadAlg) : ST bool
     b ==> compatible_hash_ae i ha ae))
   =
   recall app_psk_table;
-  MR.testify (MM.defined app_psk_table i);
+  testify (MM.defined app_psk_table i);
   match MM.lookup app_psk_table i with
   | Some x ->
     let h = get() in
@@ -191,8 +190,8 @@ let verify_hash_ae (i:pskid) (ha:hash_alg) (ae:aeadAlg) : ST bool
     if pskInfo_hash ctx = ha && pskInfo_ae ctx = ae then
      begin
       cut(compatible_hash_ae_st i ha ae h);
-      assume(MR.stable_on_t app_psk_table (compatible_hash_ae_st i ha ae));
-      MR.witness app_psk_table (compatible_hash_ae_st i ha ae);
+      assume(stable_on_t app_psk_table (compatible_hash_ae_st i ha ae));
+      mr_witness app_psk_table (compatible_hash_ae_st i ha ae);
       true
      end
     else false

diff --git a/src/tls/StreamAE.fst b/src/tls/StreamAE.fst
@@ -9,7 +9,6 @@ open FStar.HyperStack
 open FStar.HyperStack.ST
 open FStar.Seq
  // for e.g. found
-open FStar.Monotonic.RRef
 open FStar.Monotonic.Seq
 
 open Platform.Error
@@ -23,7 +22,7 @@ open StreamPlain
 module AEAD = AEADProvider
 module HS = FStar.HyperStack
 
-type rid = FStar.Monotonic.RRef.rid
+type rid = FStar.HyperStack.ST.erid
 
 type id = i:id { ID13? i }
 

diff --git a/src/tls/TLSInfo.fst b/src/tls/TLSInfo.fst
@@ -17,7 +17,6 @@ open TLSConstants
 
 module CC = CoreCrypto
 module MM = FStar.Monotonic.Map
-module MR = FStar.Monotonic.RRef
 
 let default_cipherSuites = [
   TLS_AES_128_GCM_SHA256;