From 2a63c7e4f57c66c64436ffd6f520726d58d4335d Mon Sep 17 00:00:00 2001
From: WeeknightMVP <benk7405@hotmail.com>
Date: Thu, 13 Aug 2020 13:05:35 -0400
Subject: [PATCH 1/4] Here's a generalization that produces a slower cipher
 that's more complicated and harder to reason about!

---
 Sort.cry         | 111 +++++++++++++++++++++++++++++++
 Substitution.cry | 170 +++++++++++++++++++++++++++++++++++++++++++++++
 Util.cry         |  42 ++++++++++++
 3 files changed, 323 insertions(+)
 create mode 100644 Sort.cry
 create mode 100644 Substitution.cry
 create mode 100644 Util.cry

diff --git a/Sort.cry b/Sort.cry
new file mode 100644
index 0000000..91b593b
--- /dev/null
+++ b/Sort.cry
@@ -0,0 +1,111 @@
+/*
+> HEAR the sledges with the bells —
+> Silver bells!
+> What a world of merriment their melody foretells!
+> How they tinkle, tinkle, tinkle,
+> In the icy air of night!
+> While the stars that oversprinkle
+> All the heavens, seem to twinkle
+> With a crystalline delight;
+> Keeping time, time, time,
+> In a sort of Runic rhyme,
+> To the tintinabulation that so musically wells
+> From the bells, bells, bells, bells,
+> Bells, bells, bells —
+> From the jingling and the tinkling of the bells.
+> 
+> - from _The Bells_ by Edgar Allan Poe
+
+* ("tintinabulation" is spelled "tintinnabulation"; did Poe know?)
+*/
+
+module Sort where
+
+/** Is the list sorted by `P: a -> a -> Bit`? */
+is_sorted_by_pred: {n, a} fin n => (a -> a -> Bit) -> [n]a -> Bit
+is_sorted_by_pred P list =
+    `n != 0 ==> ~0 == [ P a b | a <- take`{max n 1 - 1} list | b <- tail (list # [undefined]) ]
+
+/** test vectors for `is_sorted_by_pred` */
+property is_sorted_by_pred_test = and
+    [ v ""
+    , v"A"
+    , v "AA"
+    , v "AB"
+    , v "ABB"
+    , v "AEGILOPS"
+    , v ['A'..'Z']
+    , ~ v "BA"
+    , ~ v "BAA"
+    , ~ v "CAB"
+    ]
+  where
+    v: {n} fin n => String n -> Bit
+    v = is_sorted_by_pred (<=)
+
+/**
+ * Merge two finite sequences by repeatedly taking the lesser of
+ * their heads until at least one is empty
+ */
+merge:
+    {m, n, a} (fin m, fin n, Cmp a) =>
+    (a -> a -> Bit) -> [m+n]a -> [m+n]a
+merge P s =
+    if `(min m n) == 0 then s
+     | P hf hr then
+        (take`{min 1 m} [hf]) # merge`{max m 1 - 1, n} P (tf # r)
+    else 
+        (take`{min 1 n} [hr]) # merge`{m, max n 1 - 1} P (f # tr)
+  where
+    (f, r) = splitAt`{m} s
+    [hf] # tf = take`{max 1 m} (f # [undefined])
+    [hr] # tr = take`{max 1 n} (r # [undefined])
+
+/** Sort a finite sequence by recursively sorting/merging subsequences */
+sort: {n, a} (fin n, Cmp a) => (a -> a -> Bit) -> [n]a -> [n]a
+sort P s =
+    if `n <= 1 then s
+    else merge`{n/2} P ((sort P f) # (sort P r)) 
+    where (f, r) = splitAt`{n/2} s
+
+/** test vectors for `sort` */
+property sort_test = and
+    [ v "" == ""
+    , v "A" == "A"
+    , v "AB" == "AB"
+    , v "BA" == "AB"
+    , v "SPOILAGE" == "AEGILOPS"
+    , v "GLIBJOCKSQUIZNYMPHTOVEXDWARF" == "ABCDEFGHIIJKLMNOOPQRSTUVWXYZ"
+    ]
+  where
+    v : {n} fin n => String n -> String n
+    v x = sort (<=) x
+
+/** Does `sort` indeed sort a sequence by `P: a -> a -> Bit`? */
+sort_sorts: {n, a} (fin n, Cmp a) => (a -> a -> Bit) -> [n]a -> Bit
+sort_sorts P s = is_sorted_by_pred P (sort P s)
+
+
+/** auxiliary binary search for `index` */
+index': {n, a, l, r} (fin n, fin l, fin r, Cmp a) => [n]a -> a -> Integer
+index' s x =
+    if `l > `r then error ":-("
+     | sm == x then `m
+     | sm < x  then index'`{n, a, m+1, r} s x
+               else index'`{n, a, l, (max 1 m)-1} s x
+  where
+    type m = (l + r) / 2
+    sm = s @ `m
+    (f, r) = splitAt`{n} s
+
+/** index of item `x` in sorted sequence `s` */
+index: {n, a} (fin n, Cmp a) => [n]a -> a -> Integer
+index s x = index'`{n, a, 0, max 1 n - 1} s x
+
+/** test vectors for `index` */
+property index_test = and
+    [ index "A" 'A' == 0
+    , index "AB" 'A' == 0
+    , index "AB" 'B' == 1
+    , index ['A'..'Z'] 'Z' == toInteger ('Z' - 'A')
+    ]
diff --git a/Substitution.cry b/Substitution.cry
new file mode 100644
index 0000000..35329e1
--- /dev/null
+++ b/Substitution.cry
@@ -0,0 +1,170 @@
+/*
+> "But," said I, returning him the slip, "I am as much in the dark as 
+> ever. Were all the jewels of Golconda awaiting me on my solution of 
+> this enigma, I am quite sure that I should be unable to earn them."
+> 
+> "And yet," said Legrand, "the solution is by no means so difficult 
+> as you might be led to imagine from the first hasty inspection of 
+> the characters. These characters, as any one might readily guess, 
+> form a cipher -- that is to say, they convey a meaning; but then, 
+> from what is known of Kidd, I could not suppose him capable of 
+> constructing any of the more abstruse cryptographs. I made up my 
+> mind, at once, that this was of a simple species -- such, however, 
+> as would appear, to the crude intellect of the sailor, absolutely 
+> insoluble without the key."
+> 
+> - from _The Gold-Bug_ by Edgar Allan Poe
+*/
+
+module Substitution where
+
+import Sort
+import Util
+
+// A message is a number `n` of characters of arbitrary type `a`
+type Message m a = [m]a
+
+/** 
+ * A substitution key comprises:
+ *   * a `from` alphabet of `n` plaintext characters of arbitrary type `a`
+ *   * a `substitution` defining ciphertext characters per plaintext
+       (of a possibly different arbitrary type), and 
+ *   * a pre-computed permutation mapping `pi`
+ */
+type Key n a b =
+    { fromByTo : [n]a
+    , from     : [n]a
+    , toByFrom : [n]b
+    , to       : [n]b
+    }
+
+/**
+ * Given `from` and `to` alphabets, index `from` and `to` into 
+ * sorted alphabets and permutation mappings to produce `key`
+ */
+genKey: {n, a, b} (fin n, Cmp a, Cmp b) => [n]a -> [n]b -> Key n a b
+genKey from to =
+    { fromByTo = from @@ toByChar.1
+    , from     = fromByChar.0
+    , toByFrom = to @@ fromByChar.1
+    , to       = toByChar.0
+    }
+  where
+    fromByChar = indexByChar from
+    toByChar   = indexByChar to
+
+/** Encrypt plaintext `msg` by substitution `key` */
+encrypt: {n, a, b, m} (fin n, Cmp a) => Key n a b -> Message m a -> Message m b
+encrypt key msg =
+    toByFrom @@ ( map (index from) msg )
+  where
+    { fromByTo = _
+    , from     = from
+    , toByFrom = toByFrom
+    , to       = _
+    } = key
+
+/** Decrypt ciphertext by substitution `key` */
+decrypt: {n, a, b, m} (fin n, Cmp b) => Key n a b -> Message m b -> Message m a
+decrypt key msg =
+    fromByTo @@ ( map (index to) msg )
+  where
+    { fromByTo = fromByTo
+    , from     = _
+    , toByFrom = _
+    , to       = to
+    } = key
+
+
+/** comparison over enumerated characters */
+byChar: {_a} Cmp _a => (_a, Integer) -> (_a, Integer) -> Bit
+byChar (c, _) (c', _) = c <= c'
+
+/** Enumerate characters, then sort by character comparison */
+indexByChar: {_n, _a} (fin _n, Cmp _a) => [_n]_a -> [_n](_a, Integer)
+indexByChar x = sort byChar (enumerate x)
+
+
+// from [English Wikipedia - Substitution cipher](https://en.wikipedia.org/wiki/Substitution_cipher)
+wikiKey = genKey
+    "ABCDEFGHIJKLMNOPQRSTUVWXYZ"
+    "ZEBRASCDFGHIJKLMNOPQTUVWXY"
+wikiMsg  = "FLEEATONCEWEAREDISCOVERED"
+wikiGram = "SIAAZQLKBAVAZOARFPBLUAOAR"
+property wikiTest = and
+    [ encrypt wikiKey wikiMsg  == wikiGram
+    , decrypt wikiKey wikiGram == wikiMsg
+    ]
+
+// from [Simple English Wikipedia - Substitution cipher](https://simple.wikipedia.org/wiki/Substitution_cipher)
+simpleKey = genKey
+    "ABCDEFGHIJKLMNOPQRSTUVWXYZ"
+    "THANKYOUVERMPZXWSQBCDFGIJL"  // <- P was erroneously U
+simpleMsg  = "JACKANDJILLWENTUPTHEHILL"
+simpleGram = "ETARTZNEVMMGKZCDWCUKUVMM"
+property simpleTest = and
+    [ encrypt simpleKey simpleMsg  == simpleGram
+    , decrypt simpleKey simpleGram == simpleMsg
+    ]
+
+notSoSimpleKey = genKey         // not provided in article
+    "abcdefghijklmnoprstuvwxyz" // no "q"
+    "EKGHIJYLMNAPZWSCVRXTOQBFU" // no "D"
+notSoSimpleGram =
+    "LIVITCSWPIYVEWHEVSRIQMXLEYVEOIEWHRXEXIPFEMVEWHKVSTYLXZIXLIKIIXPIJVSZEYPERRGERIM" #
+    "WQLMGLMXQERIWGPSRIHMXQEREKIETXMJTPRGEVEKEITREWHEXXLEXXMZITWAWSQWXSWEXTVEPMRXRSJ" #
+    "GSTVRIEYVIEXCVMUIMWERGMIWXMJMGCSMWXSJOMIQXLIVIQIVIXQSVSTWHKPEGARCSXRWIEVSWIIBXV" #
+    "IZMXFSJXLIKEGAEWHEPSWYSWIWIEVXLISXLIVXLIRGEPIRQIVIIBGIIHMWYPFLEVHEWHYPSRRFQMXLE" #
+    "PPXLIECCIEVEWGISJKTVWMRLIHYSPHXLIQIMYLXSJXLIMWRIGXQEROIVFVIZEVAEKPIEWHXEAMWYEPP" #
+    "XLMWYRMWXSGSWRMHIVEXMSWMGSTPHLEVHPFKPEZINTCMXIVJSVLMRSCMWMSWVIRCIGXMWYMXXLIYSPH" #
+    "KTY"
+notSoSimpleMsg =
+    "hereuponlegrandarosewithagraveandstatelyairandbroughtmethebeetlefromaglasscasei" #
+    "nwhichitwasencloseditwasabeautifulscarabaeusandatthattimeunknowntonaturalistsof" #
+    "courseagreatprizeinascientificpointofviewthereweretworoundblackspotsnearoneextr" #
+    "emityofthebackandalongoneneartheotherthescaleswereexceedinglyhardandglossywitha" #
+    "lltheappearanceofburnishedgoldtheweightoftheinsectwasveryremarkableandtakingall" #
+    "thingsintoconsiderationicouldhardlyblamejupiterforhisopinionrespectingitthegold" #
+    "bug"
+property notSoSimpleTest = and
+    [ encrypt notSoSimpleKey notSoSimpleMsg  == notSoSimpleGram
+    , decrypt notSoSimpleKey notSoSimpleGram == notSoSimpleMsg
+    ]
+
+// from _The Gold-Bug_, ASCII-fied
+pewterBug = genKey
+    "ABCDEFGHILMNOPRSTUVY"
+    "52-+8134609*#.();?&:"  // ASCII-fied cipher alphabet
+pewterMsg =
+    "AGOODGLASSINTHEBISHOPSHOSTEL"          #
+    "INTHEDEVILSSEATFORTYONEDEGREES"        #
+    "ANDTHIRTEENMINUTESNORTHEASTANDBYNORTH" #
+    "MAINBRANCHSEVENTHLIMBEASTSIDE"         #
+    "SHOOTFROMTHELEFTEYEOFTHEDEATHSHEAD"    #
+    "ABEELINEFROMTHETREE"                   #
+    "THROUGHTHESHOTFIFTYFEETOUT"
+pewterGram =
+    "53##+305))6*;4826)4#.)4#);80"   #
+    "6*;48+8&60))85;1#(;:#*8+83(88)" #
+    "5*+;46(;88*96*?;8)*#(;485);5*+" #
+    "2:*#(;4956*2(5*-4)8&8*;40692"   #
+    "85);)6+8)4##;1(#9;48081;8:8#1"  #
+    ";48+85;4)485+528806*81(#9;48"   #
+    ";(88;4(#?34;48)4#;161;:188;#?;"
+property pewterTest = and
+    [ encrypt pewterBug pewterMsg  == pewterGram
+    , decrypt pewterBug pewterGram == pewterMsg
+    ]
+
+
+/** Decryption with same key recovers plaintext */
+recovery:
+    {n, a, b, m}
+    (fin n, Cmp a, Cmp b, fin m) =>
+    Key n a b -> Message m a -> Bit
+recovery key msg = decrypt key (encrypt key msg) == msg
+
+/*
+> :prove recovery`{m=1} (genKey ['A'..'Z' :Char] (reverse ['A'..'Z' :Char]))
+... :-(
+*/
diff --git a/Util.cry b/Util.cry
new file mode 100644
index 0000000..2b01139
--- /dev/null
+++ b/Util.cry
@@ -0,0 +1,42 @@
+/*
+> It seems somewhat strange that a study of such obvious utility, and 
+> one which so long ago attained its due place in the seminaries of 
+> Europe, should need recommending in this country at this late day.
+> - Edgar Allan Poe, endorsing Natural History as a field of study.
+*/
+module Util where
+
+/** enumerate `seq` by `Integer` index */
+enumerate: {n, a} fin n => [n]a -> [n](a, Integer)
+enumerate seq =
+    zip seq (take [0...])
+
+
+// not used
+
+/** Is s a finite sequence of unique items? */
+is_set: {n, a} (fin n, Eq a) => [n]a -> Bit
+is_set s =
+    `n != 0
+    ==> ~ (elem (head (s # [undefined])) (drop`{min 1 n} s))
+    /\ is_set (drop`{min 1 n} s)
+
+/** test vectors for `is_set` */
+property is_set_test = and
+    [   is_set ""
+    ,   is_set "A"
+    ,   is_set "AB"
+    ,   is_set "BA"
+    , ~ is_set "AA"
+    , ~ is_set "AAB"
+    , ~ is_set "ABA"
+    , ~ is_set "ABB"
+    ]
+
+
+/** inverse of permutation mapping `pi` */
+inverse:
+    {n, w}
+    (fin n, Integral w, Literal 0 w) =>
+    [n]w -> [n]w
+inverse pi = updates pi pi (take [0...])

From 4ff3edd970d26173a1ca1e41aad8d97cf3a36395 Mon Sep 17 00:00:00 2001
From: WeeknightMVP <benk7405@hotmail.com>
Date: Thu, 13 Aug 2020 15:14:09 -0400
Subject: [PATCH 2/4] Simplified by-character sort to use `<=`, which applies
 to tuples

---
 Sort.cry         | 2 +-
 Substitution.cry | 6 +-----
 2 files changed, 2 insertions(+), 6 deletions(-)

diff --git a/Sort.cry b/Sort.cry
index 91b593b..bf00d03 100644
--- a/Sort.cry
+++ b/Sort.cry
@@ -24,7 +24,7 @@ module Sort where
 /** Is the list sorted by `P: a -> a -> Bit`? */
 is_sorted_by_pred: {n, a} fin n => (a -> a -> Bit) -> [n]a -> Bit
 is_sorted_by_pred P list =
-    `n != 0 ==> ~0 == [ P a b | a <- take`{max n 1 - 1} list | b <- tail (list # [undefined]) ]
+    `n != 0 ==> and [ P x x' | x <- take`{max n 1 - 1} list | x' <- tail (list # [undefined]) ]
 
 /** test vectors for `is_sorted_by_pred` */
 property is_sorted_by_pred_test = and
diff --git a/Substitution.cry b/Substitution.cry
index 35329e1..a0f1622 100644
--- a/Substitution.cry
+++ b/Substitution.cry
@@ -76,13 +76,9 @@ decrypt key msg =
     } = key
 
 
-/** comparison over enumerated characters */
-byChar: {_a} Cmp _a => (_a, Integer) -> (_a, Integer) -> Bit
-byChar (c, _) (c', _) = c <= c'
-
 /** Enumerate characters, then sort by character comparison */
 indexByChar: {_n, _a} (fin _n, Cmp _a) => [_n]_a -> [_n](_a, Integer)
-indexByChar x = sort byChar (enumerate x)
+indexByChar x = sort (<=) (enumerate x)
 
 
 // from [English Wikipedia - Substitution cipher](https://en.wikipedia.org/wiki/Substitution_cipher)

From 7839dc4f2fbf79cd49f51517ecb3e661a820df8c Mon Sep 17 00:00:00 2001
From: WeeknightMVP <benk7405@hotmail.com>
Date: Thu, 13 Aug 2020 15:42:04 -0400
Subject: [PATCH 3/4] Removed extraneous predicate abstraction from sorts

---
 Sort.cry         | 40 ++++++++++++++++++++++------------------
 Substitution.cry |  4 ++--
 2 files changed, 24 insertions(+), 20 deletions(-)

diff --git a/Sort.cry b/Sort.cry
index bf00d03..a382d7d 100644
--- a/Sort.cry
+++ b/Sort.cry
@@ -21,13 +21,17 @@
 
 module Sort where
 
-/** Is the list sorted by `P: a -> a -> Bit`? */
-is_sorted_by_pred: {n, a} fin n => (a -> a -> Bit) -> [n]a -> Bit
-is_sorted_by_pred P list =
-    `n != 0 ==> and [ P x x' | x <- take`{max n 1 - 1} list | x' <- tail (list # [undefined]) ]
+/** Is the list sorted? */
+is_sorted: {n, a} (fin n, Cmp a) => [n]a -> Bit
+is_sorted list =
+    `n != 0 ==>
+    and [ x <= x'
+        | x <- take`{max n 1 - 1} list
+        | x' <- tail (list # [undefined])
+        ]
 
-/** test vectors for `is_sorted_by_pred` */
-property is_sorted_by_pred_test = and
+/** test vectors for `is_sorted` */
+property is_sorted_test = and
     [ v ""
     , v"A"
     , v "AA"
@@ -41,7 +45,7 @@ property is_sorted_by_pred_test = and
     ]
   where
     v: {n} fin n => String n -> Bit
-    v = is_sorted_by_pred (<=)
+    v = is_sorted
 
 /**
  * Merge two finite sequences by repeatedly taking the lesser of
@@ -49,23 +53,23 @@ property is_sorted_by_pred_test = and
  */
 merge:
     {m, n, a} (fin m, fin n, Cmp a) =>
-    (a -> a -> Bit) -> [m+n]a -> [m+n]a
-merge P s =
+    [m+n]a -> [m+n]a
+merge s =
     if `(min m n) == 0 then s
-     | P hf hr then
-        (take`{min 1 m} [hf]) # merge`{max m 1 - 1, n} P (tf # r)
+     | hf <= hr then
+        (take`{min 1 m} [hf]) # merge`{max m 1 - 1, n} (tf # r)
     else 
-        (take`{min 1 n} [hr]) # merge`{m, max n 1 - 1} P (f # tr)
+        (take`{min 1 n} [hr]) # merge`{m, max n 1 - 1} (f # tr)
   where
     (f, r) = splitAt`{m} s
     [hf] # tf = take`{max 1 m} (f # [undefined])
     [hr] # tr = take`{max 1 n} (r # [undefined])
 
 /** Sort a finite sequence by recursively sorting/merging subsequences */
-sort: {n, a} (fin n, Cmp a) => (a -> a -> Bit) -> [n]a -> [n]a
-sort P s =
+sort: {n, a} (fin n, Cmp a) => [n]a -> [n]a
+sort s =
     if `n <= 1 then s
-    else merge`{n/2} P ((sort P f) # (sort P r)) 
+    else merge`{n/2} ((sort f) # (sort r))
     where (f, r) = splitAt`{n/2} s
 
 /** test vectors for `sort` */
@@ -79,11 +83,11 @@ property sort_test = and
     ]
   where
     v : {n} fin n => String n -> String n
-    v x = sort (<=) x
+    v x = sort x
 
 /** Does `sort` indeed sort a sequence by `P: a -> a -> Bit`? */
-sort_sorts: {n, a} (fin n, Cmp a) => (a -> a -> Bit) -> [n]a -> Bit
-sort_sorts P s = is_sorted_by_pred P (sort P s)
+sort_sorts: {n, a} (fin n, Cmp a) => [n]a -> Bit
+sort_sorts s = is_sorted (sort s)
 
 
 /** auxiliary binary search for `index` */
diff --git a/Substitution.cry b/Substitution.cry
index a0f1622..8a80101 100644
--- a/Substitution.cry
+++ b/Substitution.cry
@@ -77,8 +77,8 @@ decrypt key msg =
 
 
 /** Enumerate characters, then sort by character comparison */
-indexByChar: {_n, _a} (fin _n, Cmp _a) => [_n]_a -> [_n](_a, Integer)
-indexByChar x = sort (<=) (enumerate x)
+indexByChar: {n, a} (fin n, Cmp a) => [n]a -> [n](a, Integer)
+indexByChar x = sort (enumerate x)
 
 
 // from [English Wikipedia - Substitution cipher](https://en.wikipedia.org/wiki/Substitution_cipher)

From f8a82d65b322069b87780d38072db63e3f6f9175 Mon Sep 17 00:00:00 2001
From: WeeknightMVP <benk7405@hotmail.com>
Date: Sat, 15 Aug 2020 01:18:05 -0400
Subject: [PATCH 4/4] Incorporated a smarter person's suggestion for
 `is_sorted`

---
 Sort.cry | 9 ++-------
 1 file changed, 2 insertions(+), 7 deletions(-)

diff --git a/Sort.cry b/Sort.cry
index a382d7d..a0549da 100644
--- a/Sort.cry
+++ b/Sort.cry
@@ -22,13 +22,8 @@
 module Sort where
 
 /** Is the list sorted? */
-is_sorted: {n, a} (fin n, Cmp a) => [n]a -> Bit
-is_sorted list =
-    `n != 0 ==>
-    and [ x <= x'
-        | x <- take`{max n 1 - 1} list
-        | x' <- tail (list # [undefined])
-        ]
+is_sorted : {n, a} (fin n, Cmp a) => [n]a -> Bit
+is_sorted xs = and [a <= b | a <- xs | b <- drop`{min n 1} xs]
 
 /** test vectors for `is_sorted` */
 property is_sorted_test = and