Merge pull request #3617 from mtzguido/release

Fixes for binary package

.ci/corecryptotest_reduce_keysize.sh

@@ -2,8 +2,8 @@
 set -e
 
 # For CI, use keysize_small
-sed -i.bak 's/let keysize = keysize_large/let keysize = keysize_small/' ucontrib/CoreCrypto/ml/Tests.ml
-sed -i.bak 's/let dh_param_size = dh_param_size_large/let dh_param_size = dh_param_size_small/' ucontrib/CoreCrypto/ml/Tests.ml
+sed -i.bak 's/let keysize = keysize_large/let keysize = keysize_small/' contrib/CoreCrypto/ml/Tests.ml
+sed -i.bak 's/let dh_param_size = dh_param_size_large/let dh_param_size = dh_param_size_small/' contrib/CoreCrypto/ml/Tests.ml
 
-# We leave ucontrib/CoreCrypto/ml/Tests.ml modified, unstaged.
+# We leave contrib/CoreCrypto/ml/Tests.ml modified, unstaged.
 # The CI teardown will forget this happened.

.docker/emacs/.emacs

@@ -8,14 +8,14 @@
 
 
 ;;set fstar includes, these should work for most tutorial examples, except those using hyperheap
-(setq fstar-subp-prover-args '("--include" "/home/build/FStar/ucontrib/Platform/fst" "--include" "/home/build/FStar/ucontrib/CoreCrypto/fst"))
+(setq fstar-subp-prover-args '("--include" "/home/build/FStar/contrib/Platform/fst" "--include" "/home/build/FStar/contrib/CoreCrypto/fst"))
 
 
 ;;this is what the above corresponds to on the command line:
-;fstar --include /home/FStar/FStar/ucontrib/Platform/fst --include /home/FStar/FStar/ucontrib/CoreCrypto/fst
+;fstar --include /home/FStar/FStar/contrib/Platform/fst --include /home/FStar/FStar/contrib/CoreCrypto/fst
 
 ;;set fstar includes, these work for the the Encrypt-then-MAC example:
-;(setq fstar-subp-prover-args '("--include" "/home/FStar/FStar/ulib/hyperheap" "--include" "/home/FStar/FStar/ucontrib/Platform/fst" "--include" "/home/FStar/FStar/ucontrib/CoreCrypto/fst"))
+;(setq fstar-subp-prover-args '("--include" "/home/FStar/FStar/ulib/hyperheap" "--include" "/home/FStar/FStar/contrib/Platform/fst" "--include" "/home/FStar/FStar/contrib/CoreCrypto/fst"))
 
 ;;this is what the above corresponds to on the command line:
-;fstar --include /home/FStar/FStar/ulib/hyperheap --include /home/FStar/FStar/ucontrib/Platform/fst --include /home/FStar/FStar/ucontrib/CoreCrypto/fst
+;fstar --include /home/FStar/FStar/ulib/hyperheap --include /home/FStar/FStar/contrib/Platform/fst --include /home/FStar/FStar/contrib/CoreCrypto/fst

.nix/fstar.nix

@@ -12,7 +12,7 @@ stdenv.mkDerivation {
     "doc.*"
     "examples.*"
     "src(/ocaml-output(/Makefile)?)?"
-    "ucontrib.*"
+    "contrib.*"
     "mk.*"
   ];
 

CHANGES.md

@@ -872,7 +872,7 @@ Date:   Mon Apr 30 16:57:21 2018 -0700
   abstract alias for a 21 bit integer represented within a
   FStar.UInt32.t.
 
-* ucontrib/Platform/fst/*: These modules are deprecated. Their
+* contrib/Platform/fst/*: These modules are deprecated. Their
   functionality is now moved to FStar.Bytes, FStar.Error, FStar.Tcp,
   FStar.Udp, and FStar.Date.
 

contrib/CoreCrypto/fst/CoreCrypto.fst

@@ -15,9 +15,7 @@
 *)
 module CoreCrypto
 
-open FStar.Bytes
-
-assume val now: unit -> EXT UInt32.t
+open Platform.Bytes
 
 (* ------------ Hashing ------------ *)
 type hash_alg =
@@ -62,7 +60,40 @@ let blockSize = function
   | AES_128_CBC  -> 16
   | AES_256_CBC  -> 16
 
-include CryptoTypes
+(* Authenticated Encryption for TLS.
+   Note that their AAD contents depends on the protocol version. *)
+
+type aead_cipher =
+  | AES_128_GCM
+  | AES_256_GCM
+  | CHACHA20_POLY1305
+  | AES_128_CCM   // "Counter with CBC-Message Authentication Code"
+  | AES_256_CCM
+  | AES_128_CCM_8 // variant with truncated 8-byte tags
+  | AES_256_CCM_8
+
+// the key materials consist of an encryption key, a static IV, and an authentication key.
+
+let aeadKeySize = function
+  | AES_128_CCM       -> 16
+  | AES_128_CCM_8     -> 16
+  | AES_128_GCM       -> 16
+  | AES_256_CCM       -> 32
+  | AES_256_CCM_8     -> 32
+  | AES_256_GCM       -> 32
+  | CHACHA20_POLY1305 -> 32
+
+let aeadRealIVSize (a:aead_cipher) = 12
+
+// the ciphertext ends with an authentication tag
+let aeadTagSize = function
+  | AES_128_CCM_8     ->  8
+  | AES_256_CCM_8     ->  8
+  | AES_128_CCM       -> 16
+  | AES_256_CCM       -> 16
+  | AES_128_GCM       -> 16
+  | AES_256_GCM       -> 16
+  | CHACHA20_POLY1305 -> 16
 
 //16-09-12 added precise concrete spec, matching what we implement in low-level/crypto
 //16-09-12 for robustness, we should at least test it when using external crypto.
@@ -134,11 +165,7 @@ assume val stream_decryptor : stream_cipher -> bytes -> EXT cipher_stream
 assume val stream_process : cipher_stream -> bytes -> EXT bytes
 assume val stream_fini : cipher_stream -> EXT unit
 
-assume val init : unit -> EXT int
-assume val zero : l:nat -> EXT (lbytes l)
 assume val random : l:nat -> EXT (lbytes l)
-assume val random32 : l:UInt32.t -> EXT (lbytes32 l) 
-// 18-02-25 we should probably keep just the latter
 
 assume val rsa_gen_key : int -> EXT (k:rsa_key{Some? k.rsa_prv_exp})
 assume val rsa_encrypt : rsa_key -> rsa_padding -> bytes -> EXT bytes
@@ -198,7 +225,7 @@ assume val ec_gen_key: p:ec_params
                   length k.ec_point.ecx = ec_bytelen k.ec_params.curve /\
                   length k.ec_point.ecy = ec_bytelen k.ec_params.curve})
 
-//TODO: keep also abstract OpenSSL representation for efficiency?
+//TODO: keep also abtsract OpenSSL representation for efficiency?
 type key =
   | KeyRSA of rsa_key
   | KeyDSA of dsa_key

contrib/CoreCrypto/fst/DHDB.fst

@@ -17,14 +17,14 @@ module DHDB
 open Platform.Bytes
 open CoreCrypto
 
-type key   = bytes * bytes // p, g
-type value = bytes * bool  // q, safe_prime?
+type key   = bytes & bytes // p, g
+type value = bytes & bool  // q, safe_prime?
 
 assume new type dhdb : Type0
 
 assume val defaultFileName: string
 assume val defaultDHPrimeConfidence: int
-assume val defaultPQMinLength: nat * nat
+assume val defaultPQMinLength: nat & nat
 
 assume val create: string -> dhdb
 assume val select: dhdb -> key -> option value 
@@ -33,6 +33,6 @@ assume val remove: dhdb -> key -> dhdb
 assume val keys  : dhdb -> list key 
 assume val merge : dhdb -> string -> dhdb
 
-assume val dh_check_params: dhdb -> int -> (int * int) -> bytes -> bytes -> option (dhdb * dh_params)
+assume val dh_check_params: dhdb -> int -> (int & int) -> bytes -> bytes -> option (dhdb & dh_params)
 assume val dh_check_element: dh_params -> bytes -> bool
-assume val load_default_params: string -> dhdb -> (int * int) -> (dhdb * dh_params)
+assume val load_default_params: string -> dhdb -> (int & int) -> (dhdb & dh_params)

doc/Makefile.include

@@ -2,7 +2,7 @@
 
 ifdef FSTAR_HOME
    FSTAR_ULIB=$(shell if test -d $(FSTAR_HOME)/ulib ; then echo $(FSTAR_HOME)/ulib ; else echo $(FSTAR_HOME)/lib/fstar ; fi)
-   FSTAR_CONTRIB=$(shell if test -d $(FSTAR_HOME)/ucontrib ; then echo $(FSTAR_HOME)/ucontrib ; else echo $(FSTAR_HOME)/share/fstar/contrib ; fi)
+   FSTAR_CONTRIB=$(shell if test -d $(FSTAR_HOME)/contrib ; then echo $(FSTAR_HOME)/contrib ; else echo $(FSTAR_HOME)/share/fstar/contrib ; fi)
 else
    # fstar.exe assumed to be in some bin/ directory
    # included in the PATH (e.g. opam package, /usr or /usr/local)

examples/crypto/Makefile

@@ -1,8 +1,8 @@
 FSTAR_ROOT ?= ../..
 include $(FSTAR_ROOT)/mk/test.mk
 
-OTHERFLAGS += --include $(FSTAR_ROOT)/ucontrib/Platform/fst
-OTHERFLAGS += --include $(FSTAR_ROOT)/ucontrib/CoreCrypto/fst
+OTHERFLAGS += --include $(FSTAR_ROOT)/contrib/Platform/fst
+OTHERFLAGS += --include $(FSTAR_ROOT)/contrib/CoreCrypto/fst
 
 all: # RPC.ml CntProtocol.ml
 

examples/old/tls-record-layer/LowCProvider/Makefile

@@ -1,5 +1,5 @@
 FSTAR_HOME = ../../..
-CONTRIB=ucontrib
+CONTRIB=contrib
 PLATFORM = $(FSTAR_HOME)/$(CONTRIB)/Platform/ml
 CORECRYPTO = $(FSTAR_HOME)/$(CONTRIB)/CoreCrypto/ml
 INCLUDE=-package batteries,zarith -I $(PLATFORM) -I $(CORECRYPTO)

examples/old/tls-record-layer/Makefile

@@ -328,7 +328,7 @@ ocaml-test.exe: ocaml-test-extract
 	$(OCAMLOPT) -I tmp -I crypto/ml -I $(AEAD_ODIR) $(OCAML_FILES) -o ocaml-test.exe
 	./ocaml-test.exe
 
-OPENSSL_HOME=../../ucontrib/CoreCrypto/ml/openssl
+OPENSSL_HOME=../../contrib/CoreCrypto/ml/openssl
 #OPENSSL_HOME=/usr/local/Cellar/openssl\@1.1/1.1.0c
 #CC=gcc-6 
 

examples/old/tls-record-layer/README.md

@@ -1,4 +1,4 @@
 To compile a 32-bit version of OpenSSL and run the tests in 32-bit mode:
 
-jonathan@chartreuse:~/Code/fstar/ucontrib/CoreCrypto/ml/openssl ((174ec01...)) $ KERNEL_BITS=32 ./config no-asm -m32
+jonathan@chartreuse:~/Code/fstar/contrib/CoreCrypto/ml/openssl ((174ec01...)) $ KERNEL_BITS=32 ./config no-asm -m32
 jonathan@chartreuse:~/Code/fstar/examples/low-level (c_record_aead) $ make test-perf.exe CFLAGS=-m32 KOPTS="-ccopt -m32" -B

src/ocaml-output/Makefile

@@ -80,10 +80,12 @@ install:
 .PHONY: install-sides
 install-sides:
 	@# Then the examples (those now work from any F* installation flavor, sources, binary package or opam)
-	@# ucontrib is needed by examples/crypto
+	@# contrib is needed by examples/crypto
 	$(call install_dir,examples,share/fstar/examples)
-	$(call install_dir,ucontrib,share/fstar/contrib)
+	$(call install_dir,contrib,share/fstar/contrib)
 	$(call install_dir,mk,share/fstar/mk)
+	@echo '# This line added only for the binary package, to use the fstar.exe in the package' >> $(PREFIX)/share/fstar/mk/test.mk
+	@echo 'FSTAR_EXE := $$(abspath $$(FSTAR_ROOT)/../../bin/fstar.exe)' >> $(PREFIX)/share/fstar/mk/test.mk
 	@# Then the tutorial
 ifeq ($(MADOKO),Madoko)
 	@# Build the tutorial first

tests/bug-reports/closed/Bug1052.fst

@@ -17,4 +17,4 @@ module Bug1052
 
 open FStar.All
 
-(* fstar.exe --fstar_home /home/hritcu/Projects/fstar/pub --include doc/tutorial/code/solutions --include ucontrib/Platform/fst --include ucontrib/CoreCrypto/fst --smt /home/hritcu/Apps/z3-4.5.0-x64-ubuntu-14.04/bin/z3 blah.fst *)
+(* fstar.exe --fstar_home /home/hritcu/Projects/fstar/pub --include doc/tutorial/code/solutions --include contrib/Platform/fst --include contrib/CoreCrypto/fst --smt /home/hritcu/Apps/z3-4.5.0-x64-ubuntu-14.04/bin/z3 blah.fst *)