Add crypto-square exercise (#49)

Author: keiravillekode

config.json

@@ -297,6 +297,14 @@
         "prerequisites": [],
         "difficulty": 4
       },
+      {
+        "slug": "crypto-square",
+        "name": "Crypto Square",
+        "uuid": "15a4f6f9-be4b-48bb-927d-fe337c5434b6",
+        "practices": [],
+        "prerequisites": [],
+        "difficulty": 5
+      },
       {
         "slug": "nth-prime",
         "name": "Nth Prime",

exercises/practice/crypto-square/.docs/instructions.md

@@ -0,0 +1,71 @@
+# Instructions
+
+Implement the classic method for composing secret messages called a square code.
+
+Given an English text, output the encoded version of that text.
+
+First, the input is normalized: the spaces and punctuation are removed from the English text and the message is down-cased.
+
+Then, the normalized characters are broken into rows.
+These rows can be regarded as forming a rectangle when printed with intervening newlines.
+
+For example, the sentence
+
+```text
+"If man was meant to stay on the ground, god would have given us roots."
+```
+
+is normalized to:
+
+```text
+"ifmanwasmeanttostayonthegroundgodwouldhavegivenusroots"
+```
+
+The plaintext should be organized into a rectangle as square as possible.
+The size of the rectangle should be decided by the length of the message.
+
+If `c` is the number of columns and `r` is the number of rows, then for the rectangle `r` x `c` find the smallest possible integer `c` such that:
+
+- `r * c >= length of message`,
+- and `c >= r`,
+- and `c - r <= 1`.
+
+Our normalized text is 54 characters long, dictating a rectangle with `c = 8` and `r = 7`:
+
+```text
+"ifmanwas"
+"meanttos"
+"tayonthe"
+"groundgo"
+"dwouldha"
+"vegivenu"
+"sroots  "
+```
+
+The coded message is obtained by reading down the columns going left to right.
+
+The message above is coded as:
+
+```text
+"imtgdvsfearwermayoogoanouuiontnnlvtwttddesaohghnsseoau"
+```
+
+Output the encoded text in chunks that fill perfect rectangles `(r X c)`, with `c` chunks of `r` length, separated by spaces.
+For phrases that are `n` characters short of the perfect rectangle, pad each of the last `n` chunks with a single trailing space.
+
+```text
+"imtgdvs fearwer mayoogo anouuio ntnnlvt wttddes aohghn  sseoau "
+```
+
+Notice that were we to stack these, we could visually decode the ciphertext back in to the original message:
+
+```text
+"imtgdvs"
+"fearwer"
+"mayoogo"
+"anouuio"
+"ntnnlvt"
+"wttddes"
+"aohghn "
+"sseoau "
+```

exercises/practice/crypto-square/.meta/Example.lean

@@ -0,0 +1,30 @@
+namespace CryptoSquare
+
+def countAlphanum (plaintext : String) : Nat := Id.run do
+  let mut count := 0
+  for c in plaintext.toList do
+    if Char.isAlphanum c then
+      count := count + 1
+  return count
+
+def squareRoot (radicand : Nat) : Nat := Id.run do
+  for guess in [0:radicand] do
+    if guess * guess >= radicand then return guess
+  return radicand
+
+def ciphertext (plaintext : String) : String :=
+  let length := countAlphanum plaintext
+  if length == 0 then ""
+  else Id.run do
+    let columns := squareRoot length
+    let rows := (length + columns - 1) / columns
+    let mut chars := Array.replicate ((rows * columns) + columns - 1) ' '
+    let mut count := 0
+    for c in (String.toLower plaintext).toList do
+      if Char.isAlphanum c then
+        let index := (count % columns) * (rows + 1) + (count / columns)
+        chars := chars.set! index c
+        count := count + 1
+    return chars.toList.asString
+
+end CryptoSquare

exercises/practice/crypto-square/.meta/config.json

@@ -0,0 +1,19 @@
+{
+  "authors": [
+    "keiravillekode"
+  ],
+  "files": {
+    "solution": [
+      "CryptoSquare.lean"
+    ],
+    "test": [
+      "CryptoSquareTest.lean"
+    ],
+    "example": [
+      ".meta/Example.lean"
+    ]
+  },
+  "blurb": "Implement the classic method for composing secret messages called a square code.",
+  "source": "J Dalbey's Programming Practice problems",
+  "source_url": "https://users.csc.calpoly.edu/~jdalbey/103/Projects/ProgrammingPractice.html"
+}

exercises/practice/crypto-square/.meta/tests.toml

@@ -0,0 +1,39 @@
+# This is an auto-generated file.
+#
+# Regenerating this file via `configlet sync` will:
+# - Recreate every `description` key/value pair
+# - Recreate every `reimplements` key/value pair, where they exist in problem-specifications
+# - Remove any `include = true` key/value pair (an omitted `include` key implies inclusion)
+# - Preserve any other key/value pair
+#
+# As user-added comments (using the # character) will be removed when this file
+# is regenerated, comments can be added via a `comment` key.
+
+[407c3837-9aa7-4111-ab63-ec54b58e8e9f]
+description = "empty plaintext results in an empty ciphertext"
+
+[aad04a25-b8bb-4304-888b-581bea8e0040]
+description = "normalization results in empty plaintext"
+
+[64131d65-6fd9-4f58-bdd8-4a2370fb481d]
+description = "Lowercase"
+
+[63a4b0ed-1e3c-41ea-a999-f6f26ba447d6]
+description = "Remove spaces"
+
+[1b5348a1-7893-44c1-8197-42d48d18756c]
+description = "Remove punctuation"
+
+[8574a1d3-4a08-4cec-a7c7-de93a164f41a]
+description = "9 character plaintext results in 3 chunks of 3 characters"
+
+[a65d3fa1-9e09-43f9-bcec-7a672aec3eae]
+description = "8 character plaintext results in 3 chunks, the last one with a trailing space"
+
+[fbcb0c6d-4c39-4a31-83f6-c473baa6af80]
+description = "54 character plaintext results in 7 chunks, the last two with trailing spaces"
+include = false
+
+[33fd914e-fa44-445b-8f38-ff8fbc9fe6e6]
+description = "54 character plaintext results in 8 chunks, the last two with trailing spaces"
+reimplements = "fbcb0c6d-4c39-4a31-83f6-c473baa6af80"

exercises/practice/crypto-square/CryptoSquare.lean

@@ -0,0 +1,6 @@
+namespace CryptoSquare
+
+def ciphertext (plaintext : String) : String :=
+  sorry
+
+end CryptoSquare

exercises/practice/crypto-square/CryptoSquareTest.lean

@@ -0,0 +1,26 @@
+import LeanTest
+import CryptoSquare
+
+open LeanTest
+
+def cryptoSquareTests : TestSuite :=
+  (TestSuite.empty "CryptoSquare")
+  |>.addTest "empty plaintext results in an empty ciphertext" (do
+      return assertEqual "" (CryptoSquare.ciphertext ""))
+  |>.addTest "normalization results in empty plaintext" (do
+      return assertEqual "" (CryptoSquare.ciphertext "... --- ..."))
+  |>.addTest "Lowercase" (do
+      return assertEqual "a" (CryptoSquare.ciphertext "A"))
+  |>.addTest "Remove spaces" (do
+      return assertEqual "b" (CryptoSquare.ciphertext "  b "))
+  |>.addTest "Remove punctuation" (do
+      return assertEqual "1" (CryptoSquare.ciphertext "@1,%!"))
+  |>.addTest "9 character plaintext results in 3 chunks of 3 characters" (do
+      return assertEqual "tsf hiu isn" (CryptoSquare.ciphertext "This is fun!"))
+  |>.addTest "8 character plaintext results in 3 chunks, the last one with a trailing space" (do
+      return assertEqual "clu hlt io " (CryptoSquare.ciphertext "Chill out."))
+  |>.addTest "54 character plaintext results in 8 chunks, the last two with trailing spaces" (do
+      return assertEqual "imtgdvs fearwer mayoogo anouuio ntnnlvt wttddes aohghn  sseoau " (CryptoSquare.ciphertext "If man was meant to stay on the ground, god would have given us roots."))
+
+def main : IO UInt32 := do
+  runTestSuitesWithExitCode [cryptoSquareTests]

exercises/practice/crypto-square/lakefile.toml

@@ -0,0 +1,15 @@
+name = "crypto-square"
+version = "0.1.0"
+defaultTargets = ["CryptoSquareTest"]
+testDriver = "CryptoSquareTest"
+
+[[lean_lib]]
+name = "LeanTest"
+srcDir = "vendor/LeanTest"
+
+[[lean_lib]]
+name = "CryptoSquare"
+
+[[lean_exe]]
+name = "CryptoSquareTest"
+root = "CryptoSquareTest"

exercises/practice/crypto-square/lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:v4.25.2

exercises/practice/crypto-square/vendor/LeanTest/LeanTest.lean

@@ -0,0 +1,4 @@
+-- This module serves as the root of the `LeanTest` library.
+-- Import modules here that should be built as part of the library.
+import LeanTest.Assertions
+import LeanTest.Test