Closed WeeknightMVP closed 1 year ago
Closing as newtype
is obsolete, per #815.
In the current functors-merge
branch, BlockCipher_
loads successfully, whereas _XORCipher_
reports another error:
Parse error at .../_XORCipher_.cry:4:10--4:19
Instantiation of a parameterized module may not itself be parameterized
This can be remediated by separating the functor and instantiation components of _XORCipher_
. Updating the example...
interface module I_BlockCipher where
type Key: *
type Block: *
type constraint Cmp Block
type Op = Key -> Block -> Block
encrypt: Op
decrypt: Op
module F_BlockCipher where
import interface I_BlockCipher as I
newtype BlockCipher = { encrypt: I::Op, decrypt: I::Op }
blockCipher = BlockCipher { encrypt = I::encrypt, decrypt = I::decrypt }
interface module I_XORCipher where
type KeyBlock: *
type Key = KeyBlock
type Block = KeyBlock
type constraint (Cmp KeyBlock, Logic KeyBlock)
module F_XORCipher where
import interface I_XORCipher as I
submodule P_BlockCipher where
type Key = I::KeyBlock
type Block = I::KeyBlock
encrypt = (^)`{I::KeyBlock}
decrypt = (^)`{I::KeyBlock}
submodule BlockCipher = F_BlockCipher { submodule P_BlockCipher }
...these modules load without crashing. However, when I try a concrete example...
module P_XOR32Cipher where
type KeyBlock = [32]
module XOR32Cipher where
import F_XORCipher { P_XOR32Cipher } (P_BlockCipher, BlockCipher)
import submodule P_BlockCipher (Key, Block)
import submodule BlockCipher (blockCipher)
(key, block) = random 0 : (Key, Block)
test : Bool
test = blockCipher.decrypt key (blockCipher.encrypt key block) == block
...the REPL reports type matching errors:
Cryptol> :m XOR32Cipher
Loading module Cryptol
Loading interface module I_XORCipher
Loading interface module I_BlockCipher
Loading module F_BlockCipher
Loading module F_XORCipher
Loading module P_XOR32Cipher
Loading module XOR32Cipher
[error] at .../XOR32Cipher.cry:9:10--9:29:
Inferred type is not sufficiently polymorphic.
Quantified variable: F_BlockCipher::I::Key
cannot match type: [32]
Context: ERROR -> _
When checking type of field 'decrypt'
where
F_BlockCipher::I::Key is module parameter F_BlockCipher::I::Key at .../I_BlockCipher.cry:2:8--2:11
[error] at .../XOR32Cipher.cry:9:10--9:29:
Inferred type is not sufficiently polymorphic.
Quantified variable: F_BlockCipher::I::Block
cannot match type: [32]
Context: _ -> _ -> ERROR
When checking type of field 'decrypt'
where
F_BlockCipher::I::Block is module parameter F_BlockCipher::I::Block at .../I_BlockCipher.cry:4:8--4:13
[error] at .../XOR32Cipher.cry:9:35--9:54:
The type ?a is not sufficiently polymorphic.
It cannot depend on quantified variables: F_BlockCipher::I::Block
Context: _ -> _ -> ERROR
When checking type of field 'encrypt'
where
?a is type of function argument at .../XOR32Cipher.cry:9:10--9:74
F_BlockCipher::I::Block is module parameter F_BlockCipher::I::Block at .../I_BlockCipher.cry:4:8--4:13
I've seen other examples where newtype
still crashes, though.
Here is a minimized version of the problematic example:
submodule F where
parameter
type T : *
newtype NT = { field : T }
nt = NT { field = undefined }
submodule M where
import submodule F where
type T = [32]
test = nt.field
My current hypothesis is that the problem is that newtype values are not instantiated correctly.
Consider a parameterized block cipher specification and nested instantiation:
BlockCipher_.cry
_XORCipher_.cry
_XOR32Cipher.cry
Alas, uncommenting the indicated line in
BlockCipher_
causes a crash when loading_XOR32Cipher
:Modifying
_XOR32Cipher
to instantiateBlockCipher_
directly (with the same line uncommented) causes a similar crash.Given this issue, achieving the desired effect (to export an encapsulated block cipher instance, e.g. as a parameter for cipher modes) requires exporting aliases for
BlockCipher_
parameters...BlockCipher_.cry
...and wrapping
_XOR32Cipher
: