fixup for secret integers

cryspen · Jan 13, 2024 · 2236a93 · 2236a93
1 parent 9cd40a4
commit 2236a93
Show file tree

Hide file tree

Showing 5 changed files with 20 additions and 11 deletions.
diff --git a/proof-libs/fstar-secret-integers/core/Makefile b/proof-libs/fstar-secret-integers/core/Makefile
@@ -29,7 +29,7 @@
 # (setq fstar-subp-prover-args #'my-fstar-compute-prover-args-using-make)
 #
 
-HAX_LIBS_HOME ?= $(shell git rev-parse --show-toplevel)/proof-libs/fstar
+HAX_LIBS_HOME ?= $(shell git rev-parse --show-toplevel)/proof-libs/fstar-secret-integers
 FSTAR_HOME    ?= $(HAX_LIBS_HOME)/../../../FStar
 HACL_HOME     ?= $(HAX_LIBS_HOME)/../../../hacl-star
 FSTAR_BIN     ?= $(shell command -v fstar.exe 1>&2 2> /dev/null && echo "fstar.exe" || echo "$(FSTAR_HOME)/bin/fstar.exe")

diff --git a/proof-libs/fstar-secret-integers/rust_primitives/Makefile b/proof-libs/fstar-secret-integers/rust_primitives/Makefile
@@ -29,7 +29,7 @@
 # (setq fstar-subp-prover-args #'my-fstar-compute-prover-args-using-make)
 #
 
-HAX_LIBS_HOME ?= $(shell git rev-parse --show-toplevel)/proof-libs/fstar
+HAX_LIBS_HOME ?= $(shell git rev-parse --show-toplevel)/proof-libs/fstar-secret-integers
 FSTAR_HOME    ?= $(HAX_LIBS_HOME)/../../../FStar
 HACL_HOME     ?= $(HAX_LIBS_HOME)/../../../hacl-star
 FSTAR_BIN     ?= $(shell command -v fstar.exe 1>&2 2> /dev/null && echo "fstar.exe" || echo "$(FSTAR_HOME)/bin/fstar.exe")

diff --git a/proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.Arrays.fsti b/proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.Arrays.fsti
@@ -78,6 +78,7 @@ let lemma_slice_append_3 #t (x:t_Slice t) (y:t_Slice t) (z:t_Slice t) (w:t_Slice
         (ensures (x == concat y (concat z w))) =
          assert (Seq.equal x (Seq.append y (Seq.append z w)))
 
+#push-options "--z3rlimit 100"
 let lemma_slice_append_4 #t (x y z w u:t_Slice t) :
   Lemma (requires (range (v (length y) + v (length z) + v (length w) + v (length u)) usize_inttype /\
                    length y +! length z +! length w +! length u == length x /\
@@ -87,5 +88,5 @@ let lemma_slice_append_4 #t (x y z w u:t_Slice t) :
                    u == slice x (length y +! length z +! length w) (length x)))
         (ensures (x == concat y (concat z (concat w u)))) =
          assert (Seq.equal x (Seq.append y (Seq.append z (Seq.append w u))))
-
+#pop-options
 
diff --git a/proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.Integers.fst b/proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.Integers.fst
@@ -22,6 +22,8 @@ let mk_int_equiv_lemma #_ = admit ()
 let mk_int_v_lemma #t a = ()
 let v_mk_int_lemma #t a = ()
 
+let declassify #t #l #l' a = admit()
+
 let add_mod_equiv_lemma #t #l #l' a b =
   LI.add_mod_lemma #_ #(meet l l') (classify a) (classify b)
 

diff --git a/proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.Integers.fsti b/proof-libs/fstar-secret-integers/rust_primitives/Rust_primitives.Integers.fsti
@@ -162,21 +162,27 @@ let cast_mod (#t:inttype) (#t':inttype) (#l:LI.secrecy_level)
     (u1:int_t_l t l) = 
     mk_int_l #t' #l (v u1 @%. t')
 
-/// Arithmetic operations
-/// 
-let add_mod (#t:inttype) 
-            (#l #l':LI.secrecy_level) 
-            (a:int_t_l t l) (b:int_t_l t l') =
-    mk_int_l #t #(meet l l') ((v a + v b) @%. t)
-
 let classify #t #l (#l':LI.secrecy_level{can_flow l l'})
     (a:int_t_l t l)    
     : int_t_l t l' =
     match l,l' with
     | LI.PUB, LI.SEC -> LI.secret #t a
     | LI.PUB, LI.PUB -> a
     | LI.SEC, LI.SEC -> a
-
+
+(* NOTE: Use with extreme care, and clearly document each use case *)
+val declassify #t #l #l'
+    (a:int_t_l t l)    
+    : int_t_l t l'
+
+
+/// Arithmetic operations
+/// 
+let add_mod (#t:inttype) 
+            (#l #l':LI.secrecy_level) 
+            (a:int_t_l t l) (b:int_t_l t l') =
+    mk_int_l #t #(meet l l') ((v a + v b) @%. t)
+
 val add_mod_equiv_lemma: #t:uinttype 
   -> #l:LI.secrecy_level
   -> #l':LI.secrecy_level