only use top-level imports in implicit interface, get more tests working

examples/AE.cry

@@ -16,14 +16,18 @@ parameter
   type constraint (fin p, fin n, n >= tagAmount)
 
   // Process a single block using this key and tweak
-  tweak_cipher : K -> Tweak -> [n] -> [n]
+  tweak_cipher : K -> { nonce : [n], state : A, z : [64] } -> [n] -> [n]
 
   // Cost for using the tweak
-  Cost : Int
+  Cost : [64]
 
-  Enc : K -> Tweak -> Node -> Node
+  Enc : K -> { nonce : [n], state : A, z : [64] }
-  Dec : K -> Tweak -> Node -> Node
+          -> { message : [p*n], state : [p*n] }
-  Tag : K -> Tweak -> State -> [n]
+          -> { message : [p*n], state : [p*n] }
+  Dec : K -> { nonce : [n], state : A, z : [64] }
+          -> { message : [p*n], state : [p*n] }
+          -> { message : [p*n], state : [p*n] }
+  Tag : K -> { nonce : [n], state : A, z : [64] } -> [p*n] -> [n]
 
 // The unit at which `Enc` operates
 type Node       = { message : WorkBlock, state : State }

examples/param_modules/AES.cry

@@ -1,38 +1,49 @@
 module AES where
 
-import `AES::Algorithm as AES
+submodule AESAlg = AES::Algorithm where
-import `AES::ExpandKey
+  type Mode = m
+  encRound = AESRound
+  decRound = AESInvRound
+import submodule AESAlg as AES
+
+submodule AESKey = AES::ExpandKey where
+  type Nk = AES::Nk
+  type Nr = AES::Nr
+import submodule AESKey as AES
+
 import AES::TBox
 
-type constraint ValidKey k m = (k == 128 + m * 64, 2 >= m)
+parameter
+  /** 0: AES128, 1: AES192, 2: AES256 */
+  type m : #
+  type k : #
+  type constraint (k == 128 + m * 64, 2 >= m)
 
-type EncKey m = AES::KeySchedule m
+type EncKey = AES::KeySchedule
-type DecKey m = AES::KeySchedule m
+type DecKey = AES::KeySchedule
 
 
-encrypt : {k,m} ValidKey k m => [k] -> [128] -> [128]
+encrypt : [k] -> [128] -> [128]
 encrypt k = encryptWithSchedule (expandKeyEnc k)
 
-decrypt : {k,m} ValidKey k m => [k] -> [128] -> [128]
+decrypt : [k] -> [128] -> [128]
 decrypt k = decryptWithSchedule (expandKeyDec k)
 
 
-expandKeyEnc : {k,m} ValidKey k m => [k] -> EncKey m
+expandKeyEnc : [k] -> EncKey
-expandKeyEnc = expandKey`{Nk = AES::Nk m, Nr = AES::Nr m}
+expandKeyEnc = AES::expandKey
 
-encryptWithSchedule : {k,m} ValidKey k m => EncKey m -> [128] -> [128]
+encryptWithSchedule : EncKey -> [128] -> [128]
-encryptWithSchedule = AES::encrypt params
+encryptWithSchedule = AES::encrypt
 
 
 
-expandKeyDec : {k,m} ValidKey k m => [k] -> EncKey m
+expandKeyDec : [k] -> EncKey
-expandKeyDec k = makeDecKey (expandKey`{Nk = AES::Nk m, Nr = AES::Nr m} k)
+expandKeyDec k = makeDecKey (AES::expandKey k)
 
-decryptWithSchedule : {k,m} ValidKey k m => DecKey m -> [128] -> [128]
+decryptWithSchedule : DecKey -> [128] -> [128]
-decryptWithSchedule = AES::decrypt params
+decryptWithSchedule = AES::decrypt
 
 
-params = { encRound = AESRound, decRound = AESInvRound }
-
 property test k pt = decrypt k (encrypt k pt) == pt
 

examples/param_modules/AES_GCM_SIV_Test.cry

@@ -1,8 +1,11 @@
-import `Common::AES_GCM_SIV
 
+submodule AES_GCM_SIV_0_56_Inst = Common::AES_GCM_SIV where
+  type Mode = 0
+  type AAD = 56
+import submodule AES_GCM_SIV_0_56_Inst as AES_GCM_SIV_0_56
 
 property test0 =
-  aes_gcm_siv
+  AES_GCM_SIV_0_56::aes_gcm_siv
     { key   = 0xee8e1ed9ff2540ae8f2ba9f50bc2f27c
     , nonce = 0x752abad3e0afb5f434dc4310
     , aad   = join "example"
@@ -12,8 +15,14 @@ property test0 =
   0x5d349ead175ef6b1def6fd #
   0x4fbcdeb7e4793f4a1d7e4faa70100af1
 
+
+submodule AES_GCM_SIV_0_0_Inst = Common::AES_GCM_SIV where
+  type Mode = 0
+  type AAD = 0
+import submodule AES_GCM_SIV_0_0_Inst as AES_GCM_SIV_0_0
+
 property test1 =
-  aes_gcm_siv
+  AES_GCM_SIV_0_0::aes_gcm_siv
     { key   = 0x01000000000000000000000000000000
     , nonce = 0x030000000000000000000000
     , aad   = []
@@ -23,7 +32,7 @@ property test1 =
   0xdc20e2d83f25705bb49e439eca56de25
 
 property test2 =
-  aes_gcm_siv
+  AES_GCM_SIV_0_0::aes_gcm_siv
     { key   = 0x01000000000000000000000000000000
     , nonce = 0x030000000000000000000000
     , aad   = []
@@ -34,7 +43,7 @@ property test2 =
   0x5b287c22493a364c
 
 property test3 =
-  aes_gcm_siv
+  AES_GCM_SIV_0_0::aes_gcm_siv
     { key   = 0x01000000000000000000000000000000
     , nonce = 0x030000000000000000000000
     , aad   = []
@@ -45,7 +54,7 @@ property test3 =
   0x57391a0bc4fdec8b0d106639
 
 property test4 =
-  aes_gcm_siv
+  AES_GCM_SIV_0_0::aes_gcm_siv
     { key   = 0x01000000000000000000000000000000
     , nonce = 0x030000000000000000000000
     , aad   = []
@@ -56,7 +65,7 @@ property test4 =
   0x303aaf90f6fe21199c6068577437a0c4
 
 property test5 =
-  aes_gcm_siv
+  AES_GCM_SIV_0_0::aes_gcm_siv
     { key   = 0x01000000000000000000000000000000
     , nonce = 0x030000000000000000000000
     , aad   = []
@@ -69,7 +78,7 @@ property test5 =
   0x1a8e45dcd4578c667cd86847bf6155ff
 
 property test6 =
-  aes_gcm_siv
+  AES_GCM_SIV_0_0::aes_gcm_siv
     { key   = 0x01000000000000000000000000000000
     , nonce = 0x030000000000000000000000
     , aad   = []
@@ -84,7 +93,7 @@ property test6 =
   0x5e6e311dbf395d35b0fe39c2714388f8
 
 property test7 =
-  aes_gcm_siv
+  AES_GCM_SIV_0_0::aes_gcm_siv
     { key   = 0x01000000000000000000000000000000
     , nonce = 0x030000000000000000000000
     , aad   = []
@@ -100,8 +109,14 @@ property test7 =
   0x36697f25b4cd169c6590d1dd39566d3f #
   0x8a263dd317aa88d56bdf3936dba75bb8
 
+
+submodule AES_GCM_SIV_0_8_Inst = Common::AES_GCM_SIV where
+  type Mode = 0
+  type AAD = 8
+import submodule AES_GCM_SIV_0_8_Inst as AES_GCM_SIV_0_8
+
 property test8 =
- aes_gcm_siv
+ AES_GCM_SIV_0_8::aes_gcm_siv
     { key   = 0x01000000000000000000000000000000
     , nonce = 0x030000000000000000000000
     , aad   = 0x01
@@ -112,7 +127,7 @@ property test8 =
   0x790d99759abd1508
 
 property test9 =
-  aes_gcm_siv
+  AES_GCM_SIV_0_8::aes_gcm_siv
     { key   = 0x01000000000000000000000000000000
     , nonce = 0x030000000000000000000000
     , aad   = 0x01
@@ -123,7 +138,7 @@ property test9 =
   0x02745aaa3a0c469fad9e075a
 
 property test10 =
-  aes_gcm_siv
+  AES_GCM_SIV_0_8::aes_gcm_siv
     { key   = 0x01000000000000000000000000000000
     , nonce = 0x030000000000000000000000
     , aad   = 0x01
@@ -134,7 +149,7 @@ property test10 =
   0x8f8936ec039e4e4bb97ebd8c4457441f
 
 property test11 =
-  aes_gcm_siv
+  AES_GCM_SIV_0_8::aes_gcm_siv
     { key   = 0x01000000000000000000000000000000
     , nonce = 0x030000000000000000000000
     , aad   = 0x01
@@ -147,7 +162,7 @@ property test11 =
   0xe6af6a7f87287da059a71684ed3498e1
 
 property test12 =
-  aes_gcm_siv
+  AES_GCM_SIV_0_8::aes_gcm_siv
     { key   = 0x01000000000000000000000000000000
     , nonce = 0x030000000000000000000000
     , aad   = 0x01
@@ -162,7 +177,7 @@ property test12 =
   0x6a8cc3865f76897c2e4b245cf31c51f2
 
 property test13 =
-  aes_gcm_siv
+  AES_GCM_SIV_0_8::aes_gcm_siv
     { key   = 0x01000000000000000000000000000000
     , nonce = 0x030000000000000000000000
     , aad   = 0x01
@@ -179,8 +194,13 @@ property test13 =
   0xcdc46ae475563de037001ef84ae21744
 
 
+submodule AES_GCM_SIV_0_96_Inst = Common::AES_GCM_SIV where
+  type Mode = 0
+  type AAD = 96
+import submodule AES_GCM_SIV_0_96_Inst as AES_GCM_SIV_0_96
+
 property test14 =
-  aes_gcm_siv
+  AES_GCM_SIV_0_96::aes_gcm_siv
     { msg = 0x02000000
     , aad = 0x010000000000000000000000
     , key = 0x01000000000000000000000000000000
@@ -190,8 +210,14 @@ property test14 =
   0xa8fe3e8707eb1f84fb28f8cb73de8e99 #
   0xe2f48a14
 
+
+submodule AES_GCM_SIV_0_144_Inst = Common::AES_GCM_SIV where
+  type Mode = 0
+  type AAD = 144
+import submodule AES_GCM_SIV_0_144_Inst as AES_GCM_SIV_0_144
+
 property test15 =
-  aes_gcm_siv
+  AES_GCM_SIV_0_144::aes_gcm_siv
     { msg = 0x03000000000000000000000000000000 #
             0x04000000
     , aad = 0x01000000000000000000000000000000 #
@@ -205,8 +231,13 @@ property test15 =
   0xfe106514
 
 
+submodule AES_GCM_SIV_0_160_Inst = Common::AES_GCM_SIV where
+  type Mode = 0
+  type AAD = 160
+import submodule AES_GCM_SIV_0_160_Inst as AES_GCM_SIV_0_160
+
 property test16 =
-  aes_gcm_siv
+  AES_GCM_SIV_0_160::aes_gcm_siv
     { msg =   0x03000000000000000000000000000000 #
               0x0400
     , aad   = 0x01000000000000000000000000000000 #
@@ -219,8 +250,9 @@ property test16 =
   0x2adabff9b2ef00fb47920cc72a0c0f13 #
   0xb9fd
 
+
 property test16' =
-  aes_gcm_siv
+  AES_GCM_SIV_0_0::aes_gcm_siv
    { msg = []
    , aad = []
    , key = 0xe66021d5eb8e4f4066d4adb9c33560e4
@@ -228,8 +260,14 @@ property test16' =
    }
    == 0xa4194b79071b01a87d65f706e3949578
 
+
+submodule AES_GCM_SIV_0_40_Inst = Common::AES_GCM_SIV where
+  type Mode = 0
+  type AAD = 40
+import submodule AES_GCM_SIV_0_40_Inst as AES_GCM_SIV_0_40
+
 property test17 =
-  aes_gcm_siv
+  AES_GCM_SIV_0_40::aes_gcm_siv
    { msg = 0x7a806c
    , aad = 0x46bb91c3c5
    , key = 0x36864200e0eaf5284d884a0e77d31646
@@ -239,8 +277,13 @@ property test17 =
       0xa428a8
 
 
+submodule AES_GCM_SIV_0_80_Inst = Common::AES_GCM_SIV where
+  type Mode = 0
+  type AAD = 80
+import submodule AES_GCM_SIV_0_80_Inst as AES_GCM_SIV_0_80
+
 property test18 =
-  aes_gcm_siv
+  AES_GCM_SIV_0_80::aes_gcm_siv
    { msg = 0xbdc66f146545
    , aad = 0xfc880c94a95198874296
    , key = 0xaedb64a6c590bc84d1a5e269e4b47801
@@ -250,8 +293,13 @@ property test18 =
       0x743dba20f966
 
 
+submodule AES_GCM_SIV_0_120_Inst = Common::AES_GCM_SIV where
+  type Mode = 0
+  type AAD = 120
+import submodule AES_GCM_SIV_0_120_Inst as AES_GCM_SIV_0_120
+
 property test19 =
-  aes_gcm_siv
+  AES_GCM_SIV_0_120::aes_gcm_siv
    { msg = 0x1177441f195495860f
    , aad = 0x046787f3ea22c127aaf195d1894728
    , key = 0xd5cc1fd161320b6920ce07787f86743b
@@ -262,7 +310,7 @@ property test19 =
 
 
 property test20 =
-  aes_gcm_siv
+  AES_GCM_SIV_0_160::aes_gcm_siv
    { msg = 0x9f572c614b4745914474e7c7
    , aad = 0xc9882e5386fd9f92ec489c8fde2be2cf #
            0x97e74e93
@@ -272,8 +320,14 @@ property test20 =
    == 0xf54673c5ddf710c745641c8bc1dc2f87 #
       0x1fb7561da1286e655e24b7b0
 
+
+submodule AES_GCM_SIV_0_200_Inst = Common::AES_GCM_SIV where
+  type Mode = 0
+  type AAD = 200
+import submodule AES_GCM_SIV_0_200_Inst as AES_GCM_SIV_0_200
+
 property test21 =
-  aes_gcm_siv
+  AES_GCM_SIV_0_200::aes_gcm_siv
    { msg = 0x0d8c8451178082355c9e940fea2f58
    , aad = 0x2950a70d5a1db2316fd568378da107b5 #
            0x2b0da55210cc1c1b0a
@@ -284,8 +338,13 @@ property test21 =
            0xb3449b9f39552de99dc214a1190b0b
 
 
+submodule AES_GCM_SIV_0_240_Inst = Common::AES_GCM_SIV where
+  type Mode = 0
+  type AAD = 240
+import submodule AES_GCM_SIV_0_240_Inst as AES_GCM_SIV_0_240
+
 property test22 =
-  aes_gcm_siv
+  AES_GCM_SIV_0_240::aes_gcm_siv
    { msg = 0x6b3db4da3d57aa94842b9803a96e07fb #
            0x6de7
    , aad = 0x1860f762ebfbd08284e421702de0de18 #
@@ -298,8 +357,13 @@ property test22 =
            0xdb84
 
 
+submodule AES_GCM_SIV_0_280_Inst = Common::AES_GCM_SIV where
+  type Mode = 0
+  type AAD = 280
+import submodule AES_GCM_SIV_0_280_Inst as AES_GCM_SIV_0_280
+
 property test23 =
-  aes_gcm_siv
+  AES_GCM_SIV_0_280::aes_gcm_siv
    { msg = 0xe42a3c02c25b64869e146d7b233987bd #
            0xdfc240871d
    , aad = 0x7576f7028ec6eb5ea7e298342a94d4b2 #
@@ -312,8 +376,14 @@ property test23 =
       0xb3ee197d052d15506c84a9edd65e13e9 #
       0xd24a2a6e70
 
+
+submodule AES_GCM_SIV_1_0_Inst = Common::AES_GCM_SIV where
+  type Mode = 1
+  type AAD = 0
+import submodule AES_GCM_SIV_1_0_Inst as AES_GCM_SIV_1_0
+
 property test24 =
-  aes_gcm_siv
+  AES_GCM_SIV_1_0::aes_gcm_siv
    { msg = []
    , aad = []
    , key = 0x01000000000000000000000000000000 #
@@ -322,9 +392,8 @@ property test24 =
    }
    == 0x07f5f4169bbf55a8400cd47ea6fd400f
 
-
 property test25 =
-  aes_gcm_siv
+  AES_GCM_SIV_1_0::aes_gcm_siv
    { msg = 0x0100000000000000
    , aad = []
    , key = 0x01000000000000000000000000000000 #
@@ -335,7 +404,7 @@ property test25 =
       0x61e0b97427e3df28
 
 property test26 =
-  aes_gcm_siv
+  AES_GCM_SIV_1_0::aes_gcm_siv
    { msg = 0x010000000000000000000000
    , aad = []
    , key = 0x01000000000000000000000000000000 #
@@ -346,7 +415,7 @@ property test26 =
       0xae6559e48fd10f6e5c9ca17e
 
 property test27 =
-  aes_gcm_siv
+  AES_GCM_SIV_1_0::aes_gcm_siv
    { msg = 0x01000000000000000000000000000000
    , aad = []
    , key = 0x01000000000000000000000000000000 #
@@ -356,9 +425,8 @@ property test27 =
    == 0x85a01b63025ba19b7fd3ddfc033b3e76 #
       0xc9eac6fa700942702e90862383c6c366
 
-
 property test28 =
-  aes_gcm_siv
+  AES_GCM_SIV_1_0::aes_gcm_siv
    { msg = 0x01000000000000000000000000000000 #
            0x02000000000000000000000000000000
    , aad = []
@@ -370,9 +438,8 @@ property test28 =
       0x21ec9cf850948a7c86c68ac7539d027f #
       0xe819e63abcd020b006a976397632eb5d
 
-
 property test29 =
-  aes_gcm_siv
+  AES_GCM_SIV_1_0::aes_gcm_siv
    { msg = 0x01000000000000000000000000000000 #
            0x02000000000000000000000000000000 #
            0x03000000000000000000000000000000
@@ -387,9 +454,8 @@ property test29 =
       0x9cf6c748837b61f6ee3adcee17534ed5 #
       0x790bc96880a99ba804bd12c0e6a22cc4
 
-
 property test30 =
-  aes_gcm_siv
+  AES_GCM_SIV_1_0::aes_gcm_siv
    { msg = 0x01000000000000000000000000000000 #
            0x02000000000000000000000000000000 #
            0x03000000000000000000000000000000 #
@@ -406,8 +472,13 @@ property test30 =
       0x112864c269fc0d9d88c61fa47e39aa08
 
 
+submodule AES_GCM_SIV_1_8_Inst = Common::AES_GCM_SIV where
+  type Mode = 1
+  type AAD = 8
+import submodule AES_GCM_SIV_1_8_Inst as AES_GCM_SIV_1_8
+
 property test31 =
-  aes_gcm_siv
+  AES_GCM_SIV_1_8::aes_gcm_siv
    { msg = 0x0200000000000000
    , aad = 0x01
    , key = 0x01000000000000000000000000000000 #
@@ -417,9 +488,8 @@ property test31 =
    == 0x1de22967237a813291213f267e3b452f #
       0x02d01ae33e4ec854
 
-
 property test32 =
-  aes_gcm_siv
+  AES_GCM_SIV_1_8::aes_gcm_siv
    { msg = 0x020000000000000000000000
    , aad = 0x01
    , key = 0x01000000000000000000000000000000 #
@@ -429,9 +499,8 @@ property test32 =
    == 0x163d6f9cc1b346cd453a2e4cc1a4a19a #
       0xe800941ccdc57cc8413c277f
 
-
 property test33 =
-  aes_gcm_siv
+  AES_GCM_SIV_1_8::aes_gcm_siv
    { msg = 0x02000000000000000000000000000000
    , aad = 0x01
    , key = 0x01000000000000000000000000000000 #
@@ -441,9 +510,8 @@ property test33 =
    == 0xc91545823cc24f17dbb0e9e807d5ec17 #
       0xb292d28ff61189e8e49f3875ef91aff7
 
-
 property test34 =
-  aes_gcm_siv
+  AES_GCM_SIV_1_8::aes_gcm_siv
    { msg = 0x02000000000000000000000000000000 #
            0x03000000000000000000000000000000
    , aad = 0x01
@@ -455,9 +523,8 @@ property test34 =
       0x6f255510aa654f920ac81b94e8bad365 #
       0xaea1bad12702e1965604374aab96dbbc
 
-
 property test35 =
-  aes_gcm_siv
+  AES_GCM_SIV_1_8::aes_gcm_siv
    { msg = 0x02000000000000000000000000000000 #
            0x03000000000000000000000000000000 #
            0x04000000000000000000000000000000
@@ -471,9 +538,8 @@ property test35 =
       0xfbca3b5f749cdf564527f2314f42fe25 #
       0x03332742b228c647173616cfd44c54eb
 
-
 property test36 =
-  aes_gcm_siv
+  AES_GCM_SIV_1_8::aes_gcm_siv
    { msg = 0x02000000000000000000000000000000 #
            0x03000000000000000000000000000000 #
            0x04000000000000000000000000000000 #
@@ -490,8 +556,13 @@ property test36 =
       0x5bde0285037c5de81e5b570a049b62a0
 
 
+submodule AES_GCM_SIV_1_96_Inst = Common::AES_GCM_SIV where
+  type Mode = 1
+  type AAD = 96
+import submodule AES_GCM_SIV_1_96_Inst as AES_GCM_SIV_1_96
+
 property test37 =
-  aes_gcm_siv
+  AES_GCM_SIV_1_96::aes_gcm_siv
    { msg = 0x02000000
    , aad = 0x010000000000000000000000
    , key = 0x01000000000000000000000000000000 #
@@ -502,8 +573,13 @@ property test37 =
       0x661b74cf
 
 
+submodule AES_GCM_SIV_1_144_Inst = Common::AES_GCM_SIV where
+  type Mode = 1
+  type AAD = 144
+import submodule AES_GCM_SIV_1_144_Inst as AES_GCM_SIV_1_144
+
 property test38 =
-  aes_gcm_siv
+  AES_GCM_SIV_1_144::aes_gcm_siv
    { msg = 0x03000000000000000000000000000000 #
            0x04000000
    , aad = 0x01000000000000000000000000000000 #
@@ -517,8 +593,13 @@ property test38 =
       0xcabfe307
 
 
+submodule AES_GCM_SIV_1_160_Inst = Common::AES_GCM_SIV where
+  type Mode = 1
+  type AAD = 160
+import submodule AES_GCM_SIV_1_160_Inst as AES_GCM_SIV_1_160
+
 property test39 =
-  aes_gcm_siv
+  AES_GCM_SIV_1_160::aes_gcm_siv
    { msg = 0x03000000000000000000000000000000 #
            0x0400
    , aad = 0x01000000000000000000000000000000 #
@@ -531,8 +612,9 @@ property test39 =
       0xa075cfcdf5042112aa29685c912fc205 #
       0x6543
 
+
 property test40 =
-  aes_gcm_siv
+  AES_GCM_SIV_1_0::aes_gcm_siv
    { msg = []
    , aad = []
    , key = 0xe66021d5eb8e4f4066d4adb9c33560e4 #
@@ -542,8 +624,13 @@ property test40 =
    == 0x169fbb2fbf389a995f6390af22228a62
 
 
+submodule AES_GCM_SIV_1_40_Inst = Common::AES_GCM_SIV where
+  type Mode = 1
+  type AAD = 40
+import submodule AES_GCM_SIV_1_40_Inst as AES_GCM_SIV_1_40
+
 property test41 =
-  aes_gcm_siv
+  AES_GCM_SIV_1_40::aes_gcm_siv
    { msg = 0x671fdd
    , aad = 0x4fbdc66f14
    , key = 0xbae8e37fc83441b16034566b7a806c46 #
@@ -554,8 +641,13 @@ property test41 =
       0x19719d
 
 
+submodule AES_GCM_SIV_1_80_Inst = Common::AES_GCM_SIV where
+  type Mode = 1
+  type AAD = 80
+import submodule AES_GCM_SIV_1_80_Inst as AES_GCM_SIV_1_80
+
 property test42 =
-  aes_gcm_siv
+  AES_GCM_SIV_1_80::aes_gcm_siv
    { msg = 0x195495860f04
    , aad = 0x6787f3ea22c127aaf195
    , key = 0x6545fc880c94a95198874296d5cc1fd1 #
@@ -566,8 +658,13 @@ property test42 =
       0xc12020ec8c2c
 
 
+submodule AES_GCM_SIV_1_120_Inst = Common::AES_GCM_SIV where
+  type Mode = 1
+  type AAD = 120
+import submodule AES_GCM_SIV_1_120_Inst as AES_GCM_SIV_1_120
+
 property test43 =
-  aes_gcm_siv
+  AES_GCM_SIV_1_120::aes_gcm_siv
    { msg = 0xc9882e5386fd9f92ec
    , aad = 0x489c8fde2be2cf97e74e932d4ed87d
    , key = 0xd1894728b3fed1473c528b8426a58299 #
@@ -579,7 +676,7 @@ property test43 =
 
 
 property test44 =
-  aes_gcm_siv
+  AES_GCM_SIV_1_160::aes_gcm_siv
    { msg = 0x1db2316fd568378da107b52b
    , aad = 0x0da55210cc1c1b0abde3b2f204d1e9f8 #
            0xb06bc47f
@@ -591,8 +688,13 @@ property test44 =
       0x587f64979f21826706d497d5
 
 
+submodule AES_GCM_SIV_1_200_Inst = Common::AES_GCM_SIV where
+  type Mode = 1
+  type AAD = 200
+import submodule AES_GCM_SIV_1_200_Inst as AES_GCM_SIV_1_200
+
 property test45 =
-  aes_gcm_siv
+  AES_GCM_SIV_1_200::aes_gcm_siv
    { msg = 0x21702de0de18baa9c9596291b08466
    , aad = 0xf37de21c7ff901cfe8a69615a93fdf7a #
            0x98cad481796245709f
@@ -604,8 +706,13 @@ property test45 =
       0x080d28f6ebb5d3648ce97bd5ba67fd
 
 
+submodule AES_GCM_SIV_1_240_Inst = Common::AES_GCM_SIV where
+  type Mode = 1
+  type AAD = 240
+import submodule AES_GCM_SIV_1_240_Inst as AES_GCM_SIV_1_240
+
 property test46 =
-  aes_gcm_siv
+  AES_GCM_SIV_1_240::aes_gcm_siv
    { msg = 0xb202b370ef9768ec6561c4fe6b7e7296 #
            0xfa85
    , aad = 0x9c2159058b1f0fe91433a5bdc20e214e #
@@ -619,8 +726,13 @@ property test46 =
       0x0a49
 
 
+submodule AES_GCM_SIV_1_280_Inst = Common::AES_GCM_SIV where
+  type Mode = 1
+  type AAD = 280
+import submodule AES_GCM_SIV_1_280_Inst as AES_GCM_SIV_1_280
+
 property test47 =
-  aes_gcm_siv
+  AES_GCM_SIV_1_280::aes_gcm_siv
    { msg = 0xced532ce4159b035277d4dfbb7db6296 #
            0x8b13cd4eec
    , aad = 0x734320ccc9d9bbbb19cb81b2af4ecbc3 #
@@ -636,7 +748,7 @@ property test47 =
 
 
 property test48 =
-  aes_gcm_siv
+  AES_GCM_SIV_1_0::aes_gcm_siv
    { msg = 0x00000000000000000000000000000000 #
            0x4db923dc793ee6497c76dcc03a98e108
    , aad = []
@@ -648,9 +760,8 @@ property test48 =
       0xc537703b5ba70324a6793a7bf218d3ea #
       0xffffffff000000000000000000000000
 
-
 property test49 =
-  aes_gcm_siv
+  AES_GCM_SIV_1_0::aes_gcm_siv
    { msg = 0xeb3640277c7ffd1303c7a542d02d3e4c #
            0x0000000000000000
    , aad = []
@@ -665,7 +776,7 @@ property test49 =
 
 
 property test50 =
-  aes_gcm_siv
+  AES_GCM_SIV_0_0::aes_gcm_siv
     { msg = 0x01000000000000000000000000000000 #
             0x02000000000000000000000000000000 #
             0x03000000000000000000000000000000 #

examples/param_modules/Common/AES_GCM_SIV.cry

@@ -10,7 +10,10 @@ https://tools.ietf.org/html/draft-irtf-cfrg-gcmsiv-06
 
 module Common::AES_GCM_SIV where
 
-import AES as AES
+submodule AESInst = AES where
+  type m = (2 * Mode)
+  type k = K
+import submodule AESInst as AES
 
 parameter
   /** 0: use AES128, 1: use AES256 */
@@ -22,7 +25,7 @@ parameter
 
 
 type K  = 128 + 128 * Mode
-type KS = AES::EncKey (2 * Mode)
+type KS = AES::EncKey
 
 
 /** Note the weird byte-swapping business (also in `blockify` and `unblockify`)

examples/param_modules/GCM_AES_Tests.cry

@@ -1,12 +1,31 @@
 module GCM_AES_Tests where
 
-import `Common::GCM as GCM
+submodule AES128_Inst = AES where
-import AES as AES
+  type m = 0
+  type k = 128
+import submodule AES128_Inst as AES128
 
-gcmEncrypt = GCM::encrypt { E = AES::encrypt }
+submodule AES192_Inst = AES where
+  type m = 1
+  type k = 192
+import submodule AES192_Inst as AES192
+
+submodule AES256_Inst = AES where
+  type m = 2
+  type k = 256
+import submodule AES256_Inst as AES256
+
+
+submodule GCM_128_96_0_128_Inst = Common::GCM where
+  type K = 128
+  type IV = 96
+  type AAD = 0
+  type T = 128
+  E = AES128::encrypt
+import submodule GCM_128_96_0_128_Inst as GCM_128_96_0_128
 
 property test1 =
-  gcmEncrypt
+  GCM_128_96_0_128::encrypt
     { key = 0x00000000000000000000000000000000
     , pt  = []
     , iv  = 0x000000000000000000000000
@@ -18,7 +37,7 @@ property test1 =
   }
 
 property test2 =
-  gcmEncrypt
+  GCM_128_96_0_128::encrypt
     { key = 0x00000000000000000000000000000000
     , pt  = 0x00000000000000000000000000000000
     , iv  = 0x000000000000000000000000
@@ -29,9 +48,8 @@ property test2 =
   , tag = 0xab6e47d42cec13bdf53a67b21257bddf
   }
 
-
 property test3 =
-  gcmEncrypt
+  GCM_128_96_0_128::encrypt
     { key = 0xfeffe9928665731c6d6a8f9467308308
     , pt  = 0xd9313225f88406e5a55909c5aff5269a #
             0x86a7a9531534f7da2e4c303d8a318a72 #
@@ -49,8 +67,16 @@ property test3 =
   }
 
 
+submodule GCM_128_96_160_128_Inst = Common::GCM where
+  type K = 128
+  type IV = 96
+  type AAD = 160
+  type T = 128
+  E = AES128::encrypt
+import submodule GCM_128_96_160_128_Inst as GCM_128_96_160_128
+
 property test4 =
-  gcmEncrypt
+  GCM_128_96_160_128::encrypt
     { key = 0xfeffe9928665731c6d6a8f9467308308
     , pt  = 0xd9313225f88406e5a55909c5aff5269a #
             0x86a7a9531534f7da2e4c303d8a318a72 #
@@ -68,8 +94,17 @@ property test4 =
   , tag = 0x5bc94fbc3221a5db94fae95ae7121a47
   }
 
+
+submodule GCM_128_64_160_128_Inst = Common::GCM where
+  type K = 128
+  type IV = 64
+  type AAD = 160
+  type T = 128
+  E = AES128::encrypt
+import submodule GCM_128_64_160_128_Inst as GCM_128_64_160_128
+
 property test5 =
-  gcmEncrypt
+  GCM_128_64_160_128::encrypt
     { key = 0xfeffe9928665731c6d6a8f9467308308
     , pt  = 0xd9313225f88406e5a55909c5aff5269a #
             0x86a7a9531534f7da2e4c303d8a318a72 #
@@ -87,8 +122,17 @@ property test5 =
   , tag = 0x3612d2e79e3b0785561be14aaca2fccb
   }
 
+
+submodule GCM_128_480_160_128_Inst = Common::GCM where
+  type K = 128
+  type IV = 480
+  type AAD = 160
+  type T = 128
+  E = AES128::encrypt
+import submodule GCM_128_480_160_128_Inst as GCM_128_480_160_128
+
 property test6 =
-  gcmEncrypt
+  GCM_128_480_160_128::encrypt
     { key = 0xfeffe9928665731c6d6a8f9467308308
     , pt  = 0xd9313225f88406e5a55909c5aff5269a #
             0x86a7a9531534f7da2e4c303d8a318a72 #
@@ -109,8 +153,17 @@ property test6 =
   , tag = 0x619cc5aefffe0bfa462af43c1699d050
   }
 
+
+submodule GCM_192_96_0_128_Inst = Common::GCM where
+  type K = 192
+  type IV = 96
+  type AAD = 0
+  type T = 128
+  E = AES192::encrypt
+import submodule GCM_192_96_0_128_Inst as GCM_192_96_0_128
+
 property test7 =
-  gcmEncrypt
+  GCM_192_96_0_128::encrypt
     { key = 0x00000000000000000000000000000000 #
             0x0000000000000000
     , pt  = []
@@ -123,7 +176,7 @@ property test7 =
   }
 
 property test8 =
-  gcmEncrypt
+  GCM_192_96_0_128::encrypt
     { key = 0x00000000000000000000000000000000 #
             0x0000000000000000
     , pt  = 0x00000000000000000000000000000000
@@ -136,7 +189,7 @@ property test8 =
   }
 
 property test9 =
-  gcmEncrypt
+  GCM_192_96_0_128::encrypt
     { key = 0xfeffe9928665731c6d6a8f9467308308 #
             0xfeffe9928665731c
     , pt  = 0xd9313225f88406e5a55909c5aff5269a #
@@ -154,8 +207,17 @@ property test9 =
   , tag = 0x9924a7c8587336bfb118024db8674a14
   }
 
+
+submodule GCM_192_96_160_128_Inst = Common::GCM where
+  type K = 192
+  type IV = 96
+  type AAD = 160
+  type T = 128
+  E = AES192::encrypt
+import submodule GCM_192_96_160_128_Inst as GCM_192_96_160_128
+
 property test10 =
-  gcmEncrypt
+  GCM_192_96_160_128::encrypt
     { key = 0xfeffe9928665731c6d6a8f9467308308 #
             0xfeffe9928665731c
     , pt  = 0xd9313225f88406e5a55909c5aff5269a #
@@ -174,8 +236,17 @@ property test10 =
   , tag = 0x2519498e80f1478f37ba55bd6d27618c
   }
 
+
+submodule GCM_192_64_160_128_Inst = Common::GCM where
+  type K = 192
+  type IV = 64
+  type AAD = 160
+  type T = 128
+  E = AES192::encrypt
+import submodule GCM_192_64_160_128_Inst as GCM_192_64_160_128
+
 property test11 =
-  gcmEncrypt
+  GCM_192_64_160_128::encrypt
     { key = 0xfeffe9928665731c6d6a8f9467308308 #
             0xfeffe9928665731c
     , pt  = 0xd9313225f88406e5a55909c5aff5269a #
@@ -194,8 +265,17 @@ property test11 =
   , tag = 0x65dcc57fcf623a24094fcca40d3533f8
   }
 
+
+submodule GCM_192_480_160_128_Inst = Common::GCM where
+  type K = 192
+  type IV = 480
+  type AAD = 160
+  type T = 128
+  E = AES192::encrypt
+import submodule GCM_192_480_160_128_Inst as GCM_192_480_160_128
+
 property test12 =
-  gcmEncrypt
+  GCM_192_480_160_128::encrypt
     { key = 0xfeffe9928665731c6d6a8f9467308308 #
             0xfeffe9928665731c
     , pt  = 0xd9313225f88406e5a55909c5aff5269a #
@@ -217,8 +297,17 @@ property test12 =
   , tag = 0xdcf566ff291c25bbb8568fc3d376a6d9
   }
 
+
+submodule GCM_256_96_0_128_Inst = Common::GCM where
+  type K = 256
+  type IV = 96
+  type AAD = 0
+  type T = 128
+  E = AES256::encrypt
+import submodule GCM_256_96_0_128_Inst as GCM_256_96_0_128
+
 property test13 =
-  gcmEncrypt
+  GCM_256_96_0_128::encrypt
     { key = 0x00000000000000000000000000000000 #
             0x00000000000000000000000000000000
     , pt  = []
@@ -231,7 +320,7 @@ property test13 =
   }
 
 property test14 =
-  gcmEncrypt
+  GCM_256_96_0_128::encrypt
     { key = 0x00000000000000000000000000000000 #
             0x00000000000000000000000000000000
     , pt  = 0x00000000000000000000000000000000
@@ -244,7 +333,7 @@ property test14 =
   }
 
 property test15 =
-  gcmEncrypt
+  GCM_256_96_0_128::encrypt
     { key = 0xfeffe9928665731c6d6a8f9467308308 #
             0xfeffe9928665731c6d6a8f9467308308
     , pt  = 0xd9313225f88406e5a55909c5aff5269a #
@@ -262,8 +351,17 @@ property test15 =
   , tag = 0xb094dac5d93471bdec1a502270e3cc6c
   }
 
+
+submodule GCM_256_96_160_128_Inst = Common::GCM where
+  type K = 256
+  type IV = 96
+  type AAD = 160
+  type T = 128
+  E = AES256::encrypt
+import submodule GCM_256_96_160_128_Inst as GCM_256_96_160_128
+
 property test16 =
-  gcmEncrypt
+  GCM_256_96_160_128::encrypt
     { key = 0xfeffe9928665731c6d6a8f9467308308 #
             0xfeffe9928665731c6d6a8f9467308308
     , pt  = 0xd9313225f88406e5a55909c5aff5269a #
@@ -282,8 +380,17 @@ property test16 =
   , tag = 0x76fc6ece0f4e1768cddf8853bb2d551b
   }
 
+
+submodule GCM_256_64_160_128_Inst = Common::GCM where
+  type K = 256
+  type IV = 64
+  type AAD = 160
+  type T = 128
+  E = AES256::encrypt
+import submodule GCM_256_64_160_128_Inst as GCM_256_64_160_128
+
 property test17 =
-  gcmEncrypt
+  GCM_256_64_160_128::encrypt
     { key = 0xfeffe9928665731c6d6a8f9467308308 #
             0xfeffe9928665731c6d6a8f9467308308
     , pt  = 0xd9313225f88406e5a55909c5aff5269a #
@@ -302,8 +409,17 @@ property test17 =
   , tag = 0x3a337dbf46a792c45e454913fe2ea8f2
   }
 
+
+submodule GCM_256_480_160_128_Inst = Common::GCM where
+  type K = 256
+  type IV = 480
+  type AAD = 160
+  type T = 128
+  E = AES256::encrypt
+import submodule GCM_256_480_160_128_Inst as GCM_256_480_160_128
+
 property test18 =
-  gcmEncrypt
+  GCM_256_480_160_128::encrypt
     { key = 0xfeffe9928665731c6d6a8f9467308308 #
             0xfeffe9928665731c6d6a8f9467308308
     , pt  = 0xd9313225f88406e5a55909c5aff5269a #

examples/param_modules/SHA.cry

@@ -1,44 +1,9 @@
 module SHA where
 
-import `Common::SHA
+import SHA256 as SHA256
 
 sha256 : {n} (64 >= width n) => [n] -> [256]
-sha256 = sha
+sha256 = SHA256::sha
-  { SIGMA_0 = \x -> (x >>> 2) ^ (x >>> 13) ^ (x >>> 22)
-  , SIGMA_1 = \x -> (x >>> 6) ^ (x >>> 11) ^ (x >>> 25)
-  , sigma_0 = \x -> (x >>> 7) ^ (x >>> 18) ^ (x >> 3)
-  , sigma_1 = \x -> (x >>> 17) ^ (x >>> 19) ^ (x >> 10)
-
-  , H0 = [ 0x6a09e667, 0xbb67ae85, 0x3c6ef372, 0xa54ff53a
-         , 0x510e527f, 0x9b05688c, 0x1f83d9ab, 0x5be0cd19
-         ]
-
-  , K = [ 0x428a2f98, 0x71374491, 0xb5c0fbcf, 0xe9b5dba5
-        , 0x3956c25b, 0x59f111f1, 0x923f82a4, 0xab1c5ed5
-
-        , 0xd807aa98, 0x12835b01, 0x243185be, 0x550c7dc3
-        , 0x72be5d74, 0x80deb1fe, 0x9bdc06a7, 0xc19bf174
-
-        , 0xe49b69c1, 0xefbe4786, 0x0fc19dc6, 0x240ca1cc
-        , 0x2de92c6f, 0x4a7484aa, 0x5cb0a9dc, 0x76f988da
-
-        , 0x983e5152, 0xa831c66d, 0xb00327c8, 0xbf597fc7
-        , 0xc6e00bf3, 0xd5a79147, 0x06ca6351, 0x14292967
-
-        , 0x27b70a85, 0x2e1b2138, 0x4d2c6dfc, 0x53380d13
-        , 0x650a7354, 0x766a0abb, 0x81c2c92e, 0x92722c85
-
-        , 0xa2bfe8a1, 0xa81a664b, 0xc24b8b70, 0xc76c51a3
-        , 0xd192e819, 0xd6990624, 0xf40e3585, 0x106aa070
-
-        , 0x19a4c116, 0x1e376c08, 0x2748774c, 0x34b0bcb5
-        , 0x391c0cb3, 0x4ed8aa4a, 0x5b9cca4f, 0x682e6ff3
-
-        , 0x748f82ee, 0x78a5636f, 0x84c87814, 0x8cc70208
-        , 0x90befffa, 0xa4506ceb, 0xbef9a3f7, 0xc67178f2
-        ]
-  }
-
 
 
 property katsPass = ~zero == [test == kat | (test,kat) <- sha256tests ]

src/Cryptol/Parser/ParserUtils.hs

@@ -1067,7 +1067,9 @@ desugarTopDs ownerName = go emptySig
         in
         case d of
 
-          DImport i        -> cont [d] (addI i sig)
+          DImport i | ImpTop _ <- iModule (thing i) ->
+            cont [d] (addI i sig)
+
           DParamDecl _ ds' -> cont [] (jnSig ds' sig)
 
           DModule tl | NestedModule mo <- tlValue tl ->

tests/examples/allexamples.icry.stdout

@@ -1,5 +1,6 @@
 Loading module Cryptol
 Loading module Cryptol
+Loading interface module Main$interface
 Loading module Main
 Loading module Cryptol
 Loading module AES
@@ -86,40 +87,70 @@ Loading module AES::SubBytePlain
 Loading module AES::SBox
 Loading module AES::SubByteSBox
 Loading module AES::Round
-Loading module AES::Algorithm
-Loading module AES::ExpandKey
 Loading module AES::TBox
+Loading interface module AES$interface
+Loading interface module AES::Algorithm$interface
+Loading module AES::Algorithm
+Loading interface module AES::ExpandKey$interface
+Loading module AES::ExpandKey
 Loading module AES
+[warning] at param_modules/AES/Algorithm.cry:25:6--25:8
+    Unused name: AES::AESAlg::Nk
+[warning] at param_modules/AES/Algorithm.cry:28:6--28:8
+    Unused name: AES::AESAlg::Nr
 Loading module Cryptol
+Loading interface module Common::AES_GCM_SIV$interface
 Loading module AES::GF28
 Loading module AES::State
 Loading module AES::SubBytePlain
 Loading module AES::SBox
 Loading module AES::SubByteSBox
 Loading module AES::Round
-Loading module AES::Algorithm
-Loading module AES::ExpandKey
 Loading module AES::TBox
+Loading interface module AES$interface
+Loading interface module AES::Algorithm$interface
+Loading module AES::Algorithm
+Loading interface module AES::ExpandKey$interface
+Loading module AES::ExpandKey
 Loading module AES
 Loading module Common::AES_GCM_SIV
 Loading module Main
+[warning] at param_modules/AES/Algorithm.cry:25:6--25:8
+    Unused name: AES::Nk
+[warning] at param_modules/AES/Algorithm.cry:28:6--28:8
+    Unused name: AES::Nr
+[warning] at param_modules/AES.cry:22:6--22:12
+    Unused name: Common::AES_GCM_SIV::AESInst::EncKey
 Loading module Cryptol
-Loading module Common::GCM
 Loading module AES::GF28
 Loading module AES::State
 Loading module AES::SubBytePlain
 Loading module AES::SBox
 Loading module AES::SubByteSBox
 Loading module AES::Round
-Loading module AES::Algorithm
-Loading module AES::ExpandKey
 Loading module AES::TBox
+Loading interface module AES$interface
+Loading interface module AES::Algorithm$interface
+Loading module AES::Algorithm
+Loading interface module AES::ExpandKey$interface
+Loading module AES::ExpandKey
 Loading module AES
+Loading interface module Common::GCM$interface
+Loading module Common::GCM
 Loading module GCM_AES_Tests
+[warning] at param_modules/AES/Algorithm.cry:25:6--25:8
+    Unused name: AES::AESAlg::Nk
+[warning] at param_modules/AES/Algorithm.cry:28:6--28:8
+    Unused name: AES::AESAlg::Nr
 Loading module Cryptol
+Loading module SHA256$argument
+Loading interface module Common::SHA$interface
 Loading module Common::SHA
+Loading module SHA256
 Loading module SHA
 Loading module Cryptol
+Loading module SHA256$argument
+Loading interface module Common::SHA$interface
 Loading module Common::SHA
 Loading module SHA256
 Loading module Cryptol

tests/issues/issue103.icry.stdout

@@ -10,5 +10,4 @@ Testing... ERROR for the following inputs:
 invalid sequence index: 1
 -- Backtrace --
 (Cryptol::@) called at issue103.icry:2:11--2:21
-<interactive>::f called at issue103.icry:3:9--3:10
 <interactive>::it called at issue103.icry:3:8--3:23

tests/issues/issue565.icry

@@ -1 +0,0 @@
-:l issue565/I.cry

tests/issues/issue565.icry.stdout

@@ -1,5 +0,0 @@
-Loading module Cryptol
-Loading module Cryptol
-Loading module T
-
-[error] Module T does not have parameters.

tests/issues/issue565/I.cry

@@ -1,3 +0,0 @@
-module I where
-
-import `T

tests/issues/issue565/T.cry

@@ -1,3 +0,0 @@
-module T where
-
-x = True

tests/issues/issue796.icry.stdout

@@ -1,4 +1,4 @@
 Loading module Cryptol
-Loading module Cryptol
+
-Loading module Issue796_Sig
+Parse error at Issue796.cry:4:8--4:10
-Loading module Issue796
+  Module argument may not be a functor

tests/issues/issue883.icry.stdout

@@ -1,5 +1,7 @@
 Loading module Cryptol
 Loading module Cryptol
+Loading module Issue883_Impl$argument
+Loading interface module Issue883_Sig$interface
 Loading module Issue883_Sig
 Loading module Issue883_Impl
 Loading module Issue883

tests/issues/issue883_A.icry.stdout

@@ -1,3 +1,4 @@
 Loading module Cryptol
 Loading module Cryptol
+Loading interface module Issue883_A$interface
 Loading module Issue883_A

tests/modsys/functors/T018.cry

@@ -0,0 +1,11 @@
+module T1 where
+
+parameter
+  anything : Bit
+
+submodule A where
+  x = 0x02
+
+import submodule A
+
+y = x

tests/modsys/functors/T018.icry

@@ -0,0 +1,2 @@
+:load T018.cry
+y

tests/modsys/functors/T018.icry.stdout

@@ -0,0 +1,7 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading interface module T1$interface
+Loading module T1
+
+Expression depends on definitions from a parameterized module:
+  T1::y