example: specification of a left pad string padding function

examples/games/lets_prove_leftpad/README.md

@@ -0,0 +1,81 @@
+# Overview
+
+This is a formal specification and correctness proof of the `leftpad` string padding function. The model implements and verifies a function that pads a string to a specified length by adding a specified character to the beginning of the string.
+
+# Objective
+
+Prove the correctness of the `leftpad` function by demonstrating that it satisfies three key invariants:
+
+1. The length of the output is the maximum of the desired length and the input string's length
+2. The prefix consists only of padding characters
+3. The suffix is the original input string
+
+# Components
+
+## Constants
+
+- `MAX_UINT`: Maximum length (2^8 - 1) for input/output strings
+- `CHARS`: Set of valid characters (including digits, letters, and punctuation)
+
+## Variables
+
+- `n`: Desired length of the padded string
+- `char`: Character to use for padding
+- `input`: The input string (represented as a list of characters)
+- `output`: The resulting padded string
+
+## Helper Functions
+
+- `max`: Returns the maximum of two integers
+- `repeat`: Generates a list by repeating a character a specified number of times
+- `take`: Returns the first `n` characters of a list
+- `drop`: Returns all but the first n characters of a list
+
+## Main Function
+
+- `leftpad`: Pads the input string with the specified character to reach the desired length
+
+# Invariants
+
+The model proves three key properties about the `leftpad` function:
+
+## 1. Length Invariant
+
+```
+output.length() == max(n, input.length())
+```
+
+The output length is always the maximum of the desired length and the input string's length.
+
+## 2. Prefix Invariant
+
+When padding is needed (`n > input.length()`), the prefix consists only of padding characters:
+
+```
+output.take(n - input.length()) == repeat(char, n - input.length())
+```
+
+## 3. Suffix Invariant
+
+The suffix of the output matches the input string:
+
+```
+if (n > input.length())
+  output.drop(n - input.length()) == input
+else
+  output == input
+```
+
+# Usage
+
+- **Initialization:** The model starts with a simple example: padding "foo" with "!"
+- **Step Actions:** The model explores different combinations of:
+  - Input strings of varying lengths
+  - Different padding characters
+  - Different desired lengths
+
+## Running the Model
+
+```
+quint run lets_prove_leftpad.qnt
+```

examples/games/lets_prove_leftpad/lets_prove_leftpad.qnt

@@ -0,0 +1,119 @@
+/**
+ * A formal specification and proof of the leftpad string padding function.
+ * This model implements and verifies a function that pads a string to a specified
+ * length by adding a specified character to the beginning of the string.
+ *
+ * Carlos Rodriguez, Informal Systems, 2025
+ */
+
+module LeftPad {
+  /// Maximum length of the input string or padded string
+  pure val MAX_UINT = 2^8 - 1
+
+  /// Characters that can be used for input or padding
+  pure val CHARS = Set(
+    // Digits
+    "0", "1", "2", "3", "4", "5", "6", "7", "8", "9",
+
+    // Uppercase Letters
+    "A", "B", "C", "D", "E", "F", "G", "H", "I", "J",
+    "K", "L", "M", "N", "O", "P", "Q", "R", "S", "T",
+    "U", "V", "W", "X", "Y", "Z",
+
+    // Lowercase Letters
+    "a", "b", "c", "d", "e", "f", "g", "h", "i", "j",
+    "k", "l", "m", "n", "o", "p", "q", "r", "s", "t",
+    "u", "v", "w", "x", "y", "z",
+
+    // Punctuation Symbols
+    "!", "#", "$", "%", "&", "'", "(", ")", "*", "+", 
+    ",", "-", ".", "/", ":", ";", "<", "=", ">", "?",
+    "@", "[", "\\", "]", "^", "_", "`", "{", "|", "}",
+    "~"
+  )
+
+  // State
+  var n: int // Desired length
+  var char: str // Padding character
+  var input: List[str] // Input string
+  var output: List[str] // Output padded string
+
+  /// Returns the maximum of two integers
+  pure def max(x: int, y: int): int =
+    if (x > y) x else y
+
+  /// Generates a list of characters by repeating a character a number of times
+  pure def repeat(c: str, times: int): List[str] =
+    range(0, times).foldl([], (acc, _) => acc.append(c))
+
+  /// Takes the first n characters of a list of characters
+  pure def take(s: List[str], n: int): List[str] =
+    range(0, n).foldl([], (acc, i) => if (i < s.length()) acc.append(s.nth(i)) else acc)
+
+  /// Drops the first n characters of a list of characters
+  pure def drop(s: List[str], n: int): List[str] =
+    range(n, s.length()).foldl([], (acc, i) => acc.append(s.nth(i)))
+
+  /// The main padding function that adds padding characters to the beginning of a string
+  action leftpad(s: List[str], char: str, n: int): bool = all {
+    output' = if (s.length() >= n)
+      s
+    else
+      repeat(char, n - s.length()).concat(s)
+  }
+
+  /// Initialize the state with a simple example: padding "foo" with "!"
+  action init = {
+    val string = List("f", "o", "o")
+    all {
+      n' = 0,
+      char' = "!",
+      input' = string,
+      output' = string,
+    }
+  }
+
+  /// Step explores different combinations of inputs, padding chars and desired lengths
+  action step = all {
+    // Input string
+    nondet inputChar = CHARS.oneOf()
+    nondet inputLen = 0.to(MAX_UINT).oneOf()
+    val string = repeat(inputChar, inputLen)
+    // Padding character
+    nondet paddingChar = CHARS.oneOf()
+    // Desired length
+    nondet len = 0.to(MAX_UINT).oneOf()
+    all {
+      input' = string,
+      char' = paddingChar,
+      n' = len,
+      leftpad(string, paddingChar, len)
+    }
+  }
+
+  // Invariants
+
+  /// 1. The length of the output is max(n, len(input))
+  val lengthInvariant = output.length() == max(n, input.length())
+
+  /// 2. The prefix of the output is padding characters and nothing but padding characters
+  val prefixInvariant = {
+    val paddingLength = n - input.length()
+    if (paddingLength > 0)
+      output.take(paddingLength) == repeat(char, paddingLength)
+    else
+      true // No padding means no prefix to check
+  }
+
+  /// 3. The suffix of the output is the original string
+  val suffixInvariant = {
+    val paddingLength = n - input.length()
+    if (paddingLength > 0)
+      output.drop(paddingLength) == input
+    else
+      output == input // If no padding is added, the output is the original string
+  }
+
+  /// Safety property: The function satisfies all invariants
+  val correctness = lengthInvariant and prefixInvariant and suffixInvariant
+}