add basic import support to compiler; make aead pass checker

Author: franziskuskiefer

Makefile

@@ -2,11 +2,11 @@
 PYTHON?=python3.6
 
 # hacspecs passing compiler checks
-FINISHED_SPECS=poly1305 chacha20 curve25519 curve448 aes
+FINISHED_SPECS=poly1305 chacha20 aead_chacha20poly1305 curve25519 curve448 \
+               aes gf128 aead_aes128gcm
 
 # hacspecs that pass all python checks and can be used in any make target.
-SPECS=$(FINISHED_SPECS) aead_chacha20poly1305 sha2 sha3 \
-      ed25519 p256 gf128 aead_aes128gcm rsapss blake2
+SPECS=$(FINISHED_SPECS) sha2 sha3 ed25519 p256 rsapss blake2
 
 # Don't use these in test. They take too long.
 SLOW_SPECS=wots kyber

compiler/fstar-compiler/specs/Makefile

@@ -2,7 +2,8 @@ FSTAR_HOME?=../../../../FStar
 HACL_HOME?=../../../../hacl-star
 FSTAR=$(FSTAR_HOME)/bin/fstar.exe --include $(HACL_HOME)/lib --include $(HACL_HOME)/lib/fst --expose_interfaces
 
-SPECS=aes.fst gf128.fst chacha20.fst poly1305.fst curve25519.fst curve448.fst
+SPECS=aes.fst gf128.fst aead_chacha20poly1305.fst chacha20.fst poly1305.fst \
+      curve25519.fst curve448.fst
 BROKEN_SPECS=blake2.fst
 LIBS = Lib.IntTypes.fst Lib.RawIntTypes.fst Lib.Sequence.fst Lib.ByteSequence.fst
 LIBS_FILES= $(addprefix $(HACL_HOME)/lib/fst/, $(LIBS)) speclib.fst

compiler/fstar-compiler/to_fstar.ml

@@ -14,7 +14,6 @@ let main () =
   let modulename = Filename.remove_extension (Filename.basename filename) in
   try
     let env =
-        (* T.tt_interface T.Env.empty  *)
         let stream = P.from_file (C.Resource.getlib "speclib.pyi") in
         let speclib = P.parse_intf stream in
         T.tt_interface T.Env.empty speclib

compiler/libs/hacs/core.ml

@@ -54,6 +54,7 @@ module Resource : sig
   val root   : string
   val get    : string -> string
   val getlib : string -> string
+  val getspec: string -> string
 end = struct
   let root : string =
     let mydir = Filename.dirname Sys.executable_name in
@@ -68,6 +69,9 @@ end = struct
 
   let getlib (name : string) =
     get (Format.sprintf "../lib/%s" name)
+
+  let getspec (name : string) =
+    get (Format.sprintf "../specs/%s" name)
 end
 
 (* -------------------------------------------------------------------- *)

compiler/libs/hacs/typing.ml

@@ -65,6 +65,7 @@ let stdlib =
   ((["bytes"],"from_uint128_be"), ([Some (`Exact (tword128))], (fs1 (fun _aty -> bytes_t)), Ident.make "bytes_from_uint128_be"));
   ((["bytes"],"to_uint64_le"), ([Some (`Exact bytes_t)], (fs1 (fun _aty -> tword64)), Ident.make "bytes_to_uint64_le"));
   ((["bytes"],"from_uint64_le"), ([Some (`Exact (tword64))], (fs1 (fun _aty -> bytes_t)), Ident.make "bytes_from_uint64_le"));
+  ((["bytes"],"from_uint64_be"), ([Some (`Exact (tword64))], (fs1 (fun _aty -> bytes_t)), Ident.make "bytes_from_uint64_be"));
 
   (*  (([],"natmod"), ([Some (`Approx PInt); Some (`Approx PInt)], (fun [aty;bty] -> TInt (`Natm (EUInt Big_int.zero))), Ident.make "natmod"));*)
   ((["natmod"],"to_nat"), ([Some (`Approx PInt)], (fs1 (fun _aty -> nat_t)), Ident.make "natmod_to_nat"));
@@ -167,6 +168,7 @@ module Env : sig
   module Procs : sig
     val get  : env -> symbol -> pdecl option
     val bind : env -> symbol -> hotype list * type_ -> env * ident
+    val add  : env -> pdecl -> env
   end
 end = struct
   type tdecl = { tname : ident; tdef  : type_; }
@@ -372,6 +374,8 @@ end = struct
       let decl = { pname = Ident.make f; psig = sig_; pret = ret } in
       let env  = { env with e_procs = Mstr.add f decl env.e_procs } in
       (env, decl.pname)
+    let add (env : env) (p : pdecl) =
+      { env with e_procs = Mstr.add (Ast.Ident.to_string p.pname) p env.e_procs }
   end
 
   let empty =
@@ -1009,8 +1013,27 @@ and tt_module (env : env) (nm : pident list) =
   in resolve (env, []) nm
 
 (* -------------------------------------------------------------------- *)
-and tt_import (env : env) (_ : pimport) =
-  env
+and tt_import (e : env) (imp : pimport) =
+  let impmod, impdec = imp in
+  let impmodpath, impmod2 = impmod in
+  if (unloc impmod2) = "speclib" then
+    e
+  else (
+    (* TODO: use path to read import *)
+    let _ = (String.concat " " (List.map unloc impmodpath)) in
+    let importeddeclarations = (List.map (fun x ->
+      match x with | None -> "" | Some y -> unloc y) (Option.get impdec)) in
+    let (pi : Env.env * Env.env Ast.program) =
+      let stream = Reader.from_file (Resource.getspec (unloc impmod2 ^ ".py")) in
+      let past   = Reader.parse_spec stream in
+      tt_program e past
+    in
+    let new_env, _ = pi in
+    let newdecls = List.map (fun d ->
+      Env.Procs.get new_env d) importeddeclarations in
+    let newdecls = List.map Option.get newdecls in
+    List.fold_left Env.Procs.add e newdecls
+  )
 
 (* -------------------------------------------------------------------- *)
 and tt_tydecl (env : env) ((x, ty) : pident * pexpr) : env * tydecl =
@@ -1054,7 +1077,7 @@ and tt_annotation (env : env) (att : pexpr) : ident * hoexpr list =
   | PEVar ([],x) when unloc x = "typechecked" ->
       (Ident.make "typechecked", [])
   | PECall (x, args) when qunloc x = ([],"contract3") || qunloc x = ([],"contract") ->
-      let es, tys = List.split (List.map (tt_expr env) args) in
+      let es, _ = List.split (List.map (tt_expr env) args) in
       (Ident.make "contract3", List.map (fun x -> `Expr x) es)
   | _ ->
       error ~loc:(loc att) env UnsupportedAnnotation
@@ -1124,7 +1147,7 @@ and tt_procdef (env : env) (pf : pprocdef) : env * env procdef =
   in (env, aout)
 
 (* -------------------------------------------------------------------- *)
-let tt_topdecl1 (env : env) = function
+and tt_topdecl1 (env : env) = function
   | PTImport info ->
       (tt_import  env info, [])
 
@@ -1138,7 +1161,7 @@ let tt_topdecl1 (env : env) = function
       let env, x = tt_vardecl env ((x, ty), e) in (env, [TD_VarDecl x])
 
 (* -------------------------------------------------------------------- *)
-let tt_intf1 (env : env) = function
+and tt_intf1 (env : env) = function
   | IPTTypeAlias (x, ty) ->
       let env, _ = tt_tydecl env (x, ty) in env
 
@@ -1158,10 +1181,10 @@ let tt_intf1 (env : env) = function
       else Env.Mod.bindnm env (nmunloc nm) senv
 
 (* -------------------------------------------------------------------- *)
-let tt_interface (env : env) (i : pintf) : env =
+and tt_interface (env : env) (i : pintf) : env =
   List.fold_left tt_intf1 env i
 
 (* -------------------------------------------------------------------- *)
-let tt_program (env : env) (p : pspec) : env * env program =
+and tt_program (env : env) (p : pspec) : env * env program =
   let env, prgm = List.fold_left_map tt_topdecl1 env p in
   (env, List.flatten prgm)

specs/aead_aes128gcm.py

@@ -7,18 +7,19 @@
 key_t    = bytes_t(16)
 nonce_t  = bytes_t(12)
 tag_t    = bytes_t(16)
+block_t  = bytes_t(16)
 
 @typechecked
 def padded_aad_msg(aad:vlbytes_t,msg:vlbytes_t) -> tuple_t(int,vlbytes_t):
-    laad : int = len(aad)
-    lmsg : int = len(msg)
+    laad : int = array.length(aad)
+    lmsg : int = array.length(msg)
     pad_aad : int = laad
     if laad % 16 > 0:
         pad_aad = laad + (16 - (laad % 16))
     pad_msg : int = lmsg
     if lmsg % 16 > 0:
         pad_msg = lmsg + (16 - (lmsg % 16))
-    to_mac = bytes(array.create(pad_aad + pad_msg + 16,uint8(0)))
+    to_mac : vlbytes_t = bytes(array.create(pad_aad + pad_msg + 16,uint8(0)))
     to_mac[0:laad] = aad
     to_mac[pad_aad:pad_aad+lmsg] = msg
     to_mac[pad_aad+pad_msg:pad_aad+pad_msg+8] = bytes.from_uint64_be(uint64(laad * 8))
@@ -27,24 +28,26 @@ def padded_aad_msg(aad:vlbytes_t,msg:vlbytes_t) -> tuple_t(int,vlbytes_t):
 
 @typechecked
 def aead_aes128gcm_encrypt(key:key_t,nonce:nonce_t,aad:vlbytes_t,msg:vlbytes_t) -> tuple_t(vlbytes_t,tag_t):
-    nonce0 = bytes(array.create(12,uint8(0)))
+    nonce0 : vlbytes_t = bytes(array.create(12,uint8(0)))
     mac_key : block_t = aes128_ctr_keyblock(key,nonce0,uint32(0))
     tag_mix : block_t = aes128_ctr_keyblock(key,nonce,uint32(1))
     ciphertext : vlbytes_t = aes128_encrypt(key,nonce,uint32(2),msg)
     to_mac : vlbytes_t
-    _, to_mac = padded_aad_msg(aad,ciphertext)
+    l: int # TODO: unused variable but _ is not supported by the compiler yet.
+    l, to_mac = padded_aad_msg(aad,ciphertext)
     mac : tag_t = gmac(to_mac,mac_key)
     mac = xor_block(mac,tag_mix)
     return ciphertext, mac
 
 @typechecked
 def aead_aes128gcm_decrypt(key:key_t,nonce:nonce_t,aad:vlbytes_t,
                            ciphertext:vlbytes_t,tag:tag_t) -> vlbytes_t:
-    nonce0 = bytes(array.create(12,uint8(0)))
+    nonce0 : vlbytes_t = bytes(array.create(12,uint8(0)))
     mac_key : block_t = aes128_ctr_keyblock(key,nonce0,uint32(0))
     tag_mix : block_t = aes128_ctr_keyblock(key,nonce,uint32(1))
     to_mac : vlbytes_t
-    _, to_mac = padded_aad_msg(aad,ciphertext)
+    l: int # TODO: unused variable but _ is not supported by the compiler yet.
+    l, to_mac = padded_aad_msg(aad,ciphertext)
     mac : tag_t = gmac(to_mac,mac_key)
     mac = xor_block(mac,tag_mix)
     if mac == tag:

specs/aead_chacha20poly1305.py

@@ -7,6 +7,7 @@
 key_t    = bytes_t(32)
 nonce_t  = bytes_t(12)
 tag_t    = bytes_t(16)
+block_t  = bytes_t(64)
 
 @typechecked
 def padded_aad_msg(aad:vlbytes_t,msg:vlbytes_t) -> tuple_t(int,vlbytes_t):
@@ -44,7 +45,8 @@ def aead_chacha20poly1305_decrypt(key:key_t,nonce:nonce_t,
     keyblock0: block_t = chacha20_block(key, uint32(0), nonce)
     mac_key: bytes_t = keyblock0[0:32]
     to_mac: vlbytes_t
-    _, to_mac = padded_aad_msg(aad,ciphertext)
+    l: int # TODO: unused variable but _ is not supported by the compiler yet.
+    l, to_mac = padded_aad_msg(aad,ciphertext)
     mac: tag_t = poly1305_mac(to_mac,mac_key)
     if mac == tag:
         msg: vlbytes_t = chacha20_decrypt(key, uint32(1), nonce, ciphertext)