Possibly incorrect definition of gostCorrect64

[RyanGlScott]

Primitive::Symmetric::Cipher::Block::GOST currently contains two property definitions:

• cryptol-specs/Primitive/Symmetric/Cipher/Block/GOST.cry

  Line 116 in dd86f27

  property gostCorrect key m = gostDecrypt(key, gostEncrypt(key, m)) == m

• cryptol-specs/Primitive/Symmetric/Cipher/Block/GOST.cry

  Line 130 in dd86f27

  property gostCorrect64 key m = gostDecrypt64( key, gostEncrypt64(key, m)) == m

Somewhat surprisingly, Cryptol is able to :check gostCorrect successfully, but :check gostCorrect64 fails:

$ ~/Software/cryptol-3.2.0/bin/cryptol Primitive/Symmetric/Cipher/Block/GOST.cry
┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻  
┃  ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃  
┗━╸╹┗╸ ╹ ╹   ╹ ┗━┛┗━╸
version 3.2.0 (1bcb75c)
https://cryptol.net  :? for help

Loading module Cryptol
Loading module Primitive::Symmetric::Cipher::Block::GOST
Primitive::Symmetric::Cipher::Block::GOST> :check gostCorrect
Using random testing.
Passed 100 tests.
Expected test coverage: 0.00% (100 of 2^^320 values)
Primitive::Symmetric::Cipher::Block::GOST> :check gostCorrect64
Using random testing.
Counterexample 
gostCorrect64 0x9a360787e10534d8 0x557b24e838302254 = False

I believe the reason why this is the case is because gostDecrypt64 and gostEncrypt64 (on top of which gostCorrect64 is defined) swaps the order of the arguments:

cryptol-specs/Primitive/Symmetric/Cipher/Block/GOST.cry

Lines 119 to 127 in dd86f27

	// Helper functions to perform analysis
	gostEncrypt64: ([BlockSize],[BlockSize]) -> [BlockSize]
	gostEncrypt64 (pt, key) = gostEncrypt(key', pt)
	where key' = key # zero
	gostDecrypt64 : ([BlockSize], [BlockSize]) -> [BlockSize]
	gostDecrypt64 (ct, key) = gostDecrypt(key', ct)
	where key' = key #zero

I believe that these should actually be:

diff --git a/Primitive/Symmetric/Cipher/Block/GOST.cry b/Primitive/Symmetric/Cipher/Block/GOST.cry
index 38b067a..28dbd1a 100644
--- a/Primitive/Symmetric/Cipher/Block/GOST.cry
+++ b/Primitive/Symmetric/Cipher/Block/GOST.cry
@@ -119,11 +119,11 @@ property gostCorrect key m = gostDecrypt(key, gostEncrypt(key, m)) == m
 // Helper functions to perform analysis
 
 gostEncrypt64: ([BlockSize],[BlockSize]) -> [BlockSize]
-gostEncrypt64 (pt, key)  = gostEncrypt(key', pt)
+gostEncrypt64 (key, pt)  = gostEncrypt(key', pt)
              where key' = key # zero
 
 gostDecrypt64 : ([BlockSize], [BlockSize]) -> [BlockSize]
-gostDecrypt64 (ct, key)  = gostDecrypt(key', ct)
+gostDecrypt64 (key, ct)  = gostDecrypt(key', ct)
              where key' = key #zero
 

If I apply that change, then :check gostCorrect64 passes. Can someone confirm if this is the right fix?