chore: Lean specification draft

.gitignore

@@ -1,4 +1,5 @@
 target
 export
 gates_report.json
-node_modules
+node_modules
+.lake

lampe/lake-manifest.json

@@ -0,0 +1,115 @@
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/reilabs/lampe",
+   "type": "git",
+   "subDir": "stdlib/lampe",
+   "scope": "",
+   "rev": "919a38712d22d05fc83e59af17ef57077abda1e0",
+   "name": "«std-1.0.0-beta.14»",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": false,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/reilabs/lampe",
+   "type": "git",
+   "subDir": "Lampe",
+   "scope": "",
+   "rev": "919a38712d22d05fc83e59af17ef57077abda1e0",
+   "name": "Lampe",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/batteries",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "756e3321fd3b02a85ffda19fef789916223e578c",
+   "name": "batteries",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.29.1",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/mathlib4",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "5e932f97dd25535344f80f9dd8da3aab83df0fe6",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.29.1",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/plausible",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "83e90935a17ca19ebe4b7893c7f7066e266f50d3",
+   "name": "plausible",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843",
+   "name": "LeanSearchClient",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/import-graph",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "48d5698bc464786347c1b0d859b18f938420f060",
+   "name": "importGraph",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "4dd0959c44d1af0462bd604d0f87c5781307d709",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v0.0.95+lean-v4.29.1",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "7152850e7b216a0d409701617721b6e469d34bf6",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "707efb56d0696634e9e965523a1bbe9ac6ce141d",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover",
+   "rev": "7802da01beb530bf051ab657443f9cd9bc3e1a29",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.29.0",
+   "inherited": true,
+   "configFile": "lakefile.toml"}],
+ "name": "«sha256-0.0.0»",
+ "lakeDir": ".lake"}

lampe/lakefile.toml

@@ -0,0 +1,23 @@
+# Generated by lampe
+name = "sha256-0.0.0"
+version = "0.0.0"
+defaultTargets = ["sha256-0.0.0"]
+# Large extracted test-vector array literals need a deeper elaborator stack (reilabs/lampe#270).
+moreLeanArgs = ["--tstack=262144"]
+
+[[lean_lib]]
+name = "«sha256-0.0.0»"
+leanOptions = {maxRecDepth = 131072}
+
+[[require]]
+name = "Lampe"
+git = "https://github.com/reilabs/lampe"
+rev = "main"
+subDir = "Lampe"
+
+[[require]]
+name = "std-1.0.0-beta.14"
+git = "https://github.com/reilabs/lampe"
+rev = "main"
+subDir = "stdlib/lampe"
+

lampe/lean-toolchain

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

lampe/sha256-0.0.0.lean

@@ -0,0 +1,3 @@
+
+import «sha256-0.0.0».Extracted
+import «sha256-0.0.0».Spec

lampe/sha256-0.0.0/Extracted.lean

@@ -0,0 +1,26 @@
+-- Generated by lampe
+
+import «sha256-0.0.0».Extracted.GeneratedTypes
+import «sha256-0.0.0».Extracted.Lib
+import «sha256-0.0.0».Extracted.Sha224
+import «sha256-0.0.0».Extracted.Sha224.Constants
+import «sha256-0.0.0».Extracted.Sha224.OracleTests
+import «sha256-0.0.0».Extracted.Sha224.Tests
+import «sha256-0.0.0».Extracted.Sha256
+import «sha256-0.0.0».Extracted.Sha256.Constants
+import «sha256-0.0.0».Extracted.Sha256.OracleTests
+import «sha256-0.0.0».Extracted.Sha256.Tests
+import «std-1.0.0-beta.14».Extracted
+
+namespace «sha256-0.0.0»
+
+def env := Lib.env
+  ++ Sha224.Constants.env
+  ++ Sha224.OracleTests.env
+  ++ Sha224.Tests.env
+  ++ Sha224.env
+  ++ Sha256.Constants.env
+  ++ Sha256.OracleTests.env
+  ++ Sha256.Tests.env
+  ++ Sha256.env
+  ++ «std-1.0.0-beta.14».env

lampe/sha256-0.0.0/Extracted/GeneratedTypes.lean

@@ -0,0 +1,21 @@
+-- Generated by lampe
+
+import «std-1.0.0-beta.14».Extracted.GeneratedTypes
+import Lampe
+
+open Lampe
+
+set_option linter.unusedVariables false
+
+noir_type_alias «sha256-0.0.0»::sha256::constants::BLOCK_BYTE_PTR<> := u32;
+
+noir_type_alias «sha256-0.0.0»::sha256::constants::INT_BLOCK<> := Array<u32, 16: u32>;
+
+noir_type_alias «sha256-0.0.0»::sha256::constants::HASH<> := Array<u8, 32: u32>;
+
+noir_type_alias «sha256-0.0.0»::sha256::constants::MSG_BLOCK<> := @«sha256-0.0.0»::sha256::constants::INT_BLOCK<>;
+
+noir_type_alias «sha256-0.0.0»::sha224::constants::HASH_SHA224<> := Array<u8, 28: u32>;
+
+noir_type_alias «sha256-0.0.0»::sha256::constants::STATE<> := Array<u32, 8: u32>;
+

lampe/sha256-0.0.0/Extracted/Lib.lean

@@ -0,0 +1,12 @@
+-- Generated by lampe
+
+import «sha256-0.0.0».Extracted.GeneratedTypes
+import Lampe
+
+open Lampe
+
+set_option linter.unusedVariables false
+
+def «sha256-0.0.0».Lib.env : Env := Env.mk
+  []
+  []

lampe/sha256-0.0.0/Extracted/Sha224.lean

@@ -0,0 +1,52 @@
+-- Generated by lampe
+
+import «sha256-0.0.0».Extracted.GeneratedTypes
+import Lampe
+
+open Lampe
+
+set_option linter.unusedVariables false
+
+noir_def «sha256-0.0.0»::sha224::sha224_var<N: u32>(msg: Array<u8, N: u32>, message_size: u32) -> @«sha256-0.0.0»::sha224::constants::HASH_SHA224<> := {
+  (#_assert returning Unit)((#_uLeq returning bool)(message_size, uConst!(N: u32)));
+  if (#_isUnconstrained returning bool)() then {
+    («sha256-0.0.0»::sha224::__sha224_var<N: u32> as λ(Array<u8, N: u32>, u32) -> @«sha256-0.0.0»::sha224::constants::HASH_SHA224<>)(msg, message_size)
+  } else {
+    let (h, msg_block) = («sha256-0.0.0»::sha256::process_full_blocks<N: u32> as λ(Array<u8, N: u32>, u32, @«sha256-0.0.0»::sha256::constants::STATE<>) -> Tuple<@«sha256-0.0.0»::sha256::constants::STATE<>, @«sha256-0.0.0»::sha256::constants::MSG_BLOCK<> >)(msg, message_size, («sha256-0.0.0»::sha224::constants::INITIAL_STATE_SHA224<> as λ() -> @«sha256-0.0.0»::sha256::constants::STATE<>)());
+    let hash = («sha256-0.0.0»::sha256::finalize_sha256_blocks<> as λ(u32, @«sha256-0.0.0»::sha256::constants::STATE<>, @«sha256-0.0.0»::sha256::constants::MSG_BLOCK<>) -> @«sha256-0.0.0»::sha256::constants::HASH<>)(message_size, h, msg_block);
+    let hash_sha224 = (#_ref returning & @«sha256-0.0.0»::sha224::constants::HASH_SHA224<>)((#_mkRepeatedArray returning Array<u8, 28: u32>)((0: u8)));
+    for i in (0: u32) .. (28: u32) do {
+      (hash_sha224[i]: u8) = (#_arrayIndex returning u8)(hash, (#_cast returning u32)(i));
+      #_skip
+    };
+    (#_readRef returning Array<u8, 28: u32>)(hash_sha224)
+  }
+}
+
+noir_def «sha256-0.0.0»::sha224::__sha224_var<N: u32>(msg: Array<u8, N: u32>, message_size: u32) -> @«sha256-0.0.0»::sha224::constants::HASH_SHA224<> := {
+  (#_fresh returning @«sha256-0.0.0»::sha224::constants::HASH_SHA224<>)()
+}
+
+noir_def «sha256-0.0.0»::sha224::partial_sha224_var_end<N: u32>(h: Array<u32, 8: u32>, msg: Array<u8, N: u32>, message_size: u32, real_message_size: u32) -> @«sha256-0.0.0»::sha224::constants::HASH_SHA224<> := {
+  let hash = («sha256-0.0.0»::sha256::partial_sha256_var_end<N: u32> as λ(Array<u32, 8: u32>, Array<u8, N: u32>, u32, u32) -> Array<u8, 32: u32>)(h, msg, message_size, real_message_size);
+  let hash_sha224 = (#_ref returning & @«sha256-0.0.0»::sha224::constants::HASH_SHA224<>)((#_mkRepeatedArray returning Array<u8, 28: u32>)((0: u8)));
+  for i in (0: u32) .. (28: u32) do {
+    (hash_sha224[i]: u8) = (#_arrayIndex returning u8)(hash, (#_cast returning u32)(i));
+    #_skip
+  };
+  (#_readRef returning Array<u8, 28: u32>)(hash_sha224)
+}
+
+noir_def «sha256-0.0.0»::sha224::equivalence_test::test_implementations_agree<>(msg: Array<u8, 100: u32>, message_size: u32) -> Unit := {
+  let message_size = (#_uRem returning u32)(message_size, (100: u32));
+  let unconstrained_sha224 = {
+    («sha256-0.0.0»::sha224::__sha224_var<100: u32> as λ(Array<u8, 100: u32>, u32) -> @«sha256-0.0.0»::sha224::constants::HASH_SHA224<>)(msg, message_size)
+  };
+  let sha224 = («sha256-0.0.0»::sha224::sha224_var<100: u32> as λ(Array<u8, 100: u32>, u32) -> @«sha256-0.0.0»::sha224::constants::HASH_SHA224<>)(msg, message_size);
+  (#_assert returning Unit)(((Array<u8, 28: u32> as «std-1.0.0-beta.14»::cmp::Eq<>)::eq<> as λ(Array<u8, 28: u32>, Array<u8, 28: u32>) -> bool)(sha224, unconstrained_sha224));
+  #_skip
+}
+
+def «sha256-0.0.0».Sha224.env : Env := Env.mk
+  [«sha256-0.0.0::sha224::sha224_var», «sha256-0.0.0::sha224::__sha224_var», «sha256-0.0.0::sha224::partial_sha224_var_end», «sha256-0.0.0::sha224::equivalence_test::test_implementations_agree»]
+  []

lampe/sha256-0.0.0/Extracted/Sha224/Constants.lean

@@ -0,0 +1,14 @@
+-- Generated by lampe
+
+import «sha256-0.0.0».Extracted.GeneratedTypes
+import Lampe
+
+open Lampe
+
+set_option linter.unusedVariables false
+
+noir_global_def «sha256-0.0.0»::sha224::constants::INITIAL_STATE_SHA224: @«sha256-0.0.0»::sha256::constants::STATE<> = (#_mkArray returning Array<u32, 8: u32>)((3238371032: u32), (914150663: u32), (812702999: u32), (4144912697: u32), (4290775857: u32), (1750603025: u32), (1694076839: u32), (3204075428: u32));
+
+def «sha256-0.0.0».Sha224.Constants.env : Env := Env.mk
+  [«sha256-0.0.0::sha224::constants::INITIAL_STATE_SHA224»]
+  []

lampe/sha256-0.0.0/Extracted/Sha224/OracleTests.lean

@@ -0,0 +1,36 @@
+-- Generated by lampe
+
+import «sha256-0.0.0».Extracted.GeneratedTypes
+import Lampe
+
+open Lampe
+
+set_option linter.unusedVariables false
+
+noir_def «sha256-0.0.0»::sha224::oracle_tests::sha224_hash_oracle<>(input: Vector<u8>) -> Array<u8, 28: u32> := {
+  (#_fresh returning Array<u8, 28: u32>)()
+}
+
+noir_def «sha256-0.0.0»::sha224::oracle_tests::get_sha224_hash<>(input: Vector<u8>) -> Array<u8, 28: u32> := {
+  (#_fresh returning Array<u8, 28: u32>)()
+}
+
+noir_def «sha256-0.0.0»::sha224::oracle_tests::test_sha224_1<>(input: Array<u8, 1: u32>) -> Unit := {
+  (#_fresh returning Unit)()
+}
+
+noir_def «sha256-0.0.0»::sha224::oracle_tests::test_sha224_63<>(input: Array<u8, 63: u32>) -> Unit := {
+  (#_fresh returning Unit)()
+}
+
+noir_def «sha256-0.0.0»::sha224::oracle_tests::test_sha224_511<>(input: Array<u8, 511: u32>) -> Unit := {
+  (#_fresh returning Unit)()
+}
+
+noir_def «sha256-0.0.0»::sha224::oracle_tests::test_sha224_512<>(input: Array<u8, 512: u32>) -> Unit := {
+  (#_fresh returning Unit)()
+}
+
+def «sha256-0.0.0».Sha224.OracleTests.env : Env := Env.mk
+  [«sha256-0.0.0::sha224::oracle_tests::sha224_hash_oracle», «sha256-0.0.0::sha224::oracle_tests::get_sha224_hash», «sha256-0.0.0::sha224::oracle_tests::test_sha224_1», «sha256-0.0.0::sha224::oracle_tests::test_sha224_63», «sha256-0.0.0::sha224::oracle_tests::test_sha224_511», «sha256-0.0.0::sha224::oracle_tests::test_sha224_512»]
+  []