Here's a generalization that produces a slower cipher that's more com…

Sort.cry

@@ -0,0 +1,110 @@
+/*
+> 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? */
+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
+    [ 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
+
+/**
+ * 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) =>
+    [m+n]a -> [m+n]a
+merge s =
+    if `(min m n) == 0 then s
+     | 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} (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) => [n]a -> [n]a
+sort s =
+    if `n <= 1 then s
+    else merge`{n/2} ((sort f) # (sort 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) => [n]a -> Bit
+sort_sorts s = is_sorted (sort 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')
+    ]

Substitution.cry

@@ -0,0 +1,166 @@
+/*
+> "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
+
+
+/** Enumerate characters, then sort by character comparison */
+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)
+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]))
+... :-(
+*/

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...])