changes for nuking Monotonic.RRef

hacl-star · Dec 28, 2017 · 1fb9727 · 1fb9727
1 parent 2e13de9
commit 1fb9727
Show file tree

Hide file tree

Showing 13 changed files with 7 additions and 16 deletions.
diff --git a/secure_api/aead/Crypto.AEAD.Encoding.fst b/secure_api/aead/Crypto.AEAD.Encoding.fst
@@ -9,7 +9,6 @@ open FStar.HyperStack.All
 
 open FStar.UInt32
 open FStar.Ghost
-open FStar.Monotonic.RRef
 
 open FStar.Math.Lib
 open FStar.Math.Lemmas

diff --git a/secure_api/aead/Crypto.AEAD.Encrypt.Ideal.Invariant.fst b/secure_api/aead/Crypto.AEAD.Encrypt.Ideal.Invariant.fst
@@ -6,7 +6,6 @@ open FStar.HyperStack.All
 open FStar.UInt32
 open FStar.HyperStack
 open FStar.HyperStack.ST
-open FStar.Monotonic.RRef
 
 open Crypto.Indexing
 open Flag

diff --git a/secure_api/aead/Crypto.AEAD.Encrypt.Invariant.fst b/secure_api/aead/Crypto.AEAD.Encrypt.Invariant.fst
@@ -7,7 +7,6 @@ open FStar.HyperStack.All
 open FStar.UInt32
 open FStar.Ghost
 open Buffer.Utils
-open FStar.Monotonic.RRef
 
 open Crypto.Indexing
 open Crypto.Symmetric.Bytes

diff --git a/secure_api/aead/Crypto.AEAD.Encrypt.fst b/secure_api/aead/Crypto.AEAD.Encrypt.fst
@@ -6,7 +6,6 @@ open FStar.HyperStack.All
 open FStar.UInt32
 open FStar.Ghost
 open Buffer.Utils
-open FStar.Monotonic.RRef
 
 open Crypto.Indexing
 open Crypto.Symmetric.Bytes

diff --git a/secure_api/aead/Crypto.AEAD.Enxor.Invariant.fst b/secure_api/aead/Crypto.AEAD.Enxor.Invariant.fst
@@ -7,7 +7,6 @@ open FStar.HyperStack.All
 open FStar.UInt32
 open FStar.Ghost
 open Buffer.Utils
-open FStar.Monotonic.RRef
 
 open Crypto.Indexing
 open Crypto.Symmetric.Bytes

diff --git a/secure_api/aead/Crypto.AEAD.EnxorDexor.fst b/secure_api/aead/Crypto.AEAD.EnxorDexor.fst
@@ -6,7 +6,6 @@ open FStar.HyperStack.All
 open FStar.UInt32
 open FStar.Ghost
 open Buffer.Utils
-open FStar.Monotonic.RRef
 
 open Crypto.Indexing
 open Crypto.Symmetric.Bytes

diff --git a/secure_api/aead/Crypto.AEAD.Invariant.fst b/secure_api/aead/Crypto.AEAD.Invariant.fst
@@ -9,7 +9,6 @@ open FStar.HyperStack.All
 open FStar.UInt32
 open FStar.Ghost
 open Buffer.Utils
-open FStar.Monotonic.RRef
 
 open Crypto.Indexing
 open Crypto.Symmetric.Bytes

diff --git a/secure_api/aead/Crypto.AEAD.MAC_Wrapper.Invariant.fst b/secure_api/aead/Crypto.AEAD.MAC_Wrapper.Invariant.fst
@@ -7,7 +7,6 @@ module ST = FStar.HyperStack.ST
 open FStar.UInt32
 open FStar.Ghost
 open Buffer.Utils
-open FStar.Monotonic.RRef
 
 open Crypto.Indexing
 open Crypto.Symmetric.Bytes

diff --git a/secure_api/aead/Crypto.AEAD.Wrappers.CMA.fst b/secure_api/aead/Crypto.AEAD.Wrappers.CMA.fst
@@ -6,7 +6,6 @@ open FStar.HyperStack.All
 open FStar.UInt32
 open FStar.Ghost
 open Buffer.Utils
-open FStar.Monotonic.RRef
 
 open Crypto.Indexing
 open Crypto.Symmetric.Bytes
@@ -26,7 +25,6 @@ module CMA = Crypto.Symmetric.UF1CMA
 module Seq = FStar.Seq
 module MAC = Crypto.Symmetric.MAC
 module EncodingWrapper = Crypto.AEAD.Wrappers.Encoding
-module RR = FStar.Monotonic.RRef
 module BufferUtils = Crypto.AEAD.BufferUtils
 
 (*** UF1CMA.mac ***)
@@ -330,7 +328,10 @@ let found_entry (#i:id) (n:Cipher.iv (Cipher.algi i)) (st:aead_state i Reader)
 (*+ verify_liveness: 
 	 liveness pre-condition for UF1CMA.verify
   **)	
-
+
+(*
+ * AR: 12/29: TODO: is this rid eternal? if so, use erid from HST
+ *)
 let verify_liveness (#i:CMA.id) (r:rid) (ak:CMA.state i) (tag:lbuffer (v MAC.taglen)) (h:mem) = 
   ak_live CMA.(ak.region) ak h /\
   Buffer.live h tag

diff --git a/secure_api/aead/Crypto.AEAD.Wrappers.Encoding.fst b/secure_api/aead/Crypto.AEAD.Wrappers.Encoding.fst
@@ -10,7 +10,6 @@ open FStar.HyperStack.All
 open FStar.UInt32
 open FStar.Ghost
 open Buffer.Utils
-open FStar.Monotonic.RRef
 
 open FStar.Math.Lib
 open FStar.Math.Lemmas

diff --git a/secure_api/aead/Crypto.AEAD.Wrappers.PRF.fst b/secure_api/aead/Crypto.AEAD.Wrappers.PRF.fst
@@ -5,7 +5,6 @@ module ST = FStar.HyperStack.ST
 open FStar.HyperStack.All
 open FStar.UInt32
 open FStar.HyperStack
-open FStar.Monotonic.RRef
 
 open Crypto.Indexing
 open Flag

diff --git a/secure_api/prf/Crypto.Symmetric.PRF.fst b/secure_api/prf/Crypto.Symmetric.PRF.fst
@@ -22,7 +22,6 @@ open FStar.HyperStack.All
 open FStar.Ghost
 open FStar.UInt8
 open FStar.UInt32
-open FStar.Monotonic.RRef
 
 open Crypto.Indexing
 open Crypto.Symmetric.Bytes
@@ -36,6 +35,8 @@ module CMA   = Crypto.Symmetric.UF1CMA
 module Block = Crypto.Symmetric.Cipher
 
 
+type rid = ST.erid
+
 // PRF TABLE
 
 let blocklen i = Block.blocklen (cipherAlg_of_id i)

diff --git a/secure_api/uf1cma/Crypto.Symmetric.UF1CMA.fst b/secure_api/uf1cma/Crypto.Symmetric.UF1CMA.fst
@@ -28,7 +28,6 @@ open Crypto.Indexing
 open Flag
 
 module HS = FStar.HyperStack
-module RR = FStar.Monotonic.RRef
 module MAC = Crypto.Symmetric.MAC
 
 
@@ -562,7 +561,7 @@ let verify_ensures (#i:id) (st:state i) (acc:accBuffer i) (tag:MAC.tagB)
 
 (** Auxiliary lemma to propagate `ilog st.log` and `alog acc` in `verify` *)
 private val modifies_verify_aux: #a:Type -> #b:Type -> #c:Type -> #d:Type ->
-  #r:RR.rid -> #rel:Preorder.preorder c -> mref:ST.m_rref r c rel -> ref:HS.reference d ->
+  #r:erid -> #rel:Preorder.preorder c -> mref:ST.m_rref r c rel -> ref:HS.reference d ->
   buf1:Buffer.buffer a -> buf2:Buffer.buffer b ->
   h0:mem -> h1:mem -> h2:mem -> h3:mem -> Lemma
   (requires (