Added examples/experimental/math-puzzle

This PR adds the `examples` folder in `language/documentation`.

`math-puzzle` is added to the `examples/experimental` directory.

TODO:
- make `examples` a cargo project
- add the document generation and the test features to the `examples` project

Closes: aptos-labs#10023

language/documentation/examples/math-puzzle/Move.toml

@@ -0,0 +1,3 @@
+[package]
+name = "math-puzzle"
+version = "0.0.0"

language/documentation/examples/math-puzzle/README.md

@@ -0,0 +1,63 @@
+# Math Puzzle
+
+This package contains an example that solves a math puzzle using Move Prover.
+
+## Puzzle description
+
+```
+Find a,b,...,h such that:
+
+1 <= a,b,...,h <= 9
+
+    a b c
+  +   d e
+  -------
+    f g h
+
+a is the double of c
+b is less than h
+c is equal to e
+d is equal to f
+e is less than or equal to 3
+f is odd
+g is even
+h is greater than or equal to 5
+```
+
+## Solving the puzzle using Move Prover
+
+In `sources/puzzlie.move`, the function `Puzzle::puzzle` is constructed to take 8 numbers (i.e., `a`, `b`, ..., `h`) and abort if the input does not satisfy any rule of the puzzle. In addition, the spec block for the function is added to assert that the function always aborts, in other words, there is no input that satisfies all the rule. The Move Prover will disprove the function specification giving a counter-example which satisfies all of the puzzle rules. It will become the solution of the puzzle.
+
+Use the following command to run Move Prover:
+```
+move package prove
+```
+
+The following is the expected output of Move Prover:
+```
+    error: function does not abort under this condition
+    |- /Users/jkpark/puzzle.move:53:9
+    |
+ 36 |         aborts_if true;
+    |         ^^^^^^^^^^^^^^^
+    |
+    =     at /Users/jkpark/puzzle.move:28: puzzle
+    =         a = 6
+    =         b = 5
+    =         c = 3
+    =         d = 7
+    =         e = 3
+    =         f = 7
+    =         g = 2
+    =         h = 6
+    ...
+```
+
+## Solution
+
+```
+    a b c        6 5 3
+  +   d e      +   7 3
+  -------      -------
+    f g h        7 2 6
+```

language/documentation/examples/math-puzzle/sources/puzzle.move

@@ -0,0 +1,33 @@
+module 0x42::Puzzle {
+    fun assert0(b: bool) {
+        assert!(b, 0);
+    }
+
+    fun puzzle(a: u64, b: u64, c: u64, d: u64, e: u64, f: u64, g: u64, h: u64) {
+        assert0(1 <= a && a <= 9);         // 1 <= a <= 9
+        assert0(1 <= b && b <= 9);         // 1 <= b <= 9
+        assert0(1 <= c && c <= 9);         // 1 <= c <= 9
+        assert0(1 <= d && d <= 9);         // 1 <= d <= 9
+        assert0(1 <= e && e <= 9);         // 1 <= e <= 9
+        assert0(1 <= f && f <= 9);         // 1 <= f <= 9
+        assert0(1 <= g && g <= 9);         // 1 <= g <= 9
+        assert0(1 <= h && h <= 9);         // 1 <= h <= 9
+
+        assert0(a == c*2);                 // a is the double of c
+        assert0(b < h);                    // b is less than h
+        assert0(c == e);                   // c is equal to e
+        assert0(d == f);                   // d is equal to f
+        assert0(e <= 3);                   // e is less than or equal to 3
+        assert0(f % 2 == 1);               // f is odd
+        assert0(g % 2 == 0);               // g is even
+        assert0(h >= 5);                   // h is greater than or equal to 5
+
+        assert0((c+e)%10 == h);            //      a b c
+        let carry = (c+e)/10;              //    +   d e
+        assert0((b+d+carry)%10 == g);      //    -------
+        assert0(a+(b+d+carry)/10 == f);    //      f g h
+    }
+    spec puzzle {
+        aborts_if true;                    // specifies that this fun always aborts.
+    }
+}