From 6d2eca25311133f16be54386d3ee894c152cad7e Mon Sep 17 00:00:00 2001
From: niv vaknin <niv@certora.com>
Date: Sun, 22 Dec 2024 12:34:19 +0200
Subject: [PATCH 1/3] niv/CERT 7810 part1: Soroban Example

---
 .gitignore                                    |    2 +-
 Soroban/hello_world/Cargo.lock                | 1524 +++++++++++++++++
 Soroban/hello_world/Cargo.toml                |   34 +
 Soroban/hello_world/README.md                 |  103 ++
 Soroban/hello_world/certora_build.py          |  101 ++
 .../hello_world/hello_world_new_fromat.conf   |    6 +
 .../hello_world/hello_world_old_format.conf   |    8 +
 Soroban/hello_world/justfile                  |   21 +
 .../soroban_hello_world_contract.wasm         |  Bin 0 -> 29459 bytes
 Soroban/hello_world/src/lib.rs                |   15 +
 Soroban/hello_world/src/test.rs               |   17 +
 11 files changed, 1830 insertions(+), 1 deletion(-)
 create mode 100644 Soroban/hello_world/Cargo.lock
 create mode 100644 Soroban/hello_world/Cargo.toml
 create mode 100644 Soroban/hello_world/README.md
 create mode 100755 Soroban/hello_world/certora_build.py
 create mode 100644 Soroban/hello_world/hello_world_new_fromat.conf
 create mode 100644 Soroban/hello_world/hello_world_old_format.conf
 create mode 100644 Soroban/hello_world/justfile
 create mode 100755 Soroban/hello_world/soroban_hello_world_contract.wasm
 create mode 100644 Soroban/hello_world/src/lib.rs
 create mode 100644 Soroban/hello_world/src/test.rs

diff --git a/.gitignore b/.gitignore
index f2fa7fa3..8970f2b8 100644
--- a/.gitignore
+++ b/.gitignore
@@ -9,4 +9,4 @@
 **/cache/
 **/emv*
 **/collect.json
-
+**/target/
diff --git a/Soroban/hello_world/Cargo.lock b/Soroban/hello_world/Cargo.lock
new file mode 100644
index 00000000..bcbc6bec
--- /dev/null
+++ b/Soroban/hello_world/Cargo.lock
@@ -0,0 +1,1524 @@
+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+version = 4
+
+[[package]]
+name = "addr2line"
+version = "0.24.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "dfbe277e56a376000877090da837660b4427aad530e3028d44e0bffe4f89a1c1"
+dependencies = [
+ "gimli",
+]
+
+[[package]]
+name = "adler2"
+version = "2.0.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "512761e0bb2578dd7380c6baaa0f4ce03e84f95e960231d1dec8bf4d7d6e2627"
+
+[[package]]
+name = "android-tzdata"
+version = "0.1.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e999941b234f3131b00bc13c22d06e8c5ff726d1b6318ac7eb276997bbb4fef0"
+
+[[package]]
+name = "android_system_properties"
+version = "0.1.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "819e7219dbd41043ac279b19830f2efc897156490d7fd6ea916720117ee66311"
+dependencies = [
+ "libc",
+]
+
+[[package]]
+name = "arbitrary"
+version = "1.3.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "7d5a26814d8dcb93b0e5a0ff3c6d80a8843bafb21b39e8e18a6f05471870e110"
+dependencies = [
+ "derive_arbitrary",
+]
+
+[[package]]
+name = "autocfg"
+version = "1.4.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ace50bade8e6234aa140d9a2f552bbee1db4d353f69b8217bc503490fc1a9f26"
+
+[[package]]
+name = "backtrace"
+version = "0.3.74"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8d82cb332cdfaed17ae235a638438ac4d4839913cc2af585c3c6746e8f8bee1a"
+dependencies = [
+ "addr2line",
+ "cfg-if",
+ "libc",
+ "miniz_oxide",
+ "object",
+ "rustc-demangle",
+ "windows-targets",
+]
+
+[[package]]
+name = "base16ct"
+version = "0.2.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "4c7f02d4ea65f2c1853089ffd8d2787bdbc63de2f0d29dedbcf8ccdfa0ccd4cf"
+
+[[package]]
+name = "base32"
+version = "0.4.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "23ce669cd6c8588f79e15cf450314f9638f967fc5770ff1c7c1deb0925ea7cfa"
+
+[[package]]
+name = "base64"
+version = "0.13.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9e1b586273c5702936fe7b7d6896644d8be71e6314cfe09d3167c95f712589e8"
+
+[[package]]
+name = "base64"
+version = "0.22.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "72b3254f16251a8381aa12e40e3c4d2f0199f8c6508fbecb9d91f575e0fbb8c6"
+
+[[package]]
+name = "base64ct"
+version = "1.6.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8c3c1a368f70d6cf7302d78f8f7093da241fb8e8807c05cc9e51a125895a6d5b"
+
+[[package]]
+name = "block-buffer"
+version = "0.10.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "3078c7629b62d3f0439517fa394996acacc5cbc91c5a20d8c658e77abd503a71"
+dependencies = [
+ "generic-array",
+]
+
+[[package]]
+name = "bumpalo"
+version = "3.16.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "79296716171880943b8470b5f8d03aa55eb2e645a4874bdbb28adb49162e012c"
+
+[[package]]
+name = "byteorder"
+version = "1.5.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1fd0f2584146f6f2ef48085050886acf353beff7305ebd1ae69500e27c67f64b"
+
+[[package]]
+name = "bytes-lit"
+version = "0.0.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "0adabf37211a5276e46335feabcbb1530c95eb3fdf85f324c7db942770aa025d"
+dependencies = [
+ "num-bigint",
+ "proc-macro2",
+ "quote",
+ "syn",
+]
+
+[[package]]
+name = "cc"
+version = "1.2.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "c31a0499c1dc64f458ad13872de75c0eb7e3fdb0e67964610c914b034fc5956e"
+dependencies = [
+ "shlex",
+]
+
+[[package]]
+name = "certora"
+version = "0.1.0"
+source = "git+https://github.com/Certora/solana-cvt.git?branch=dev-soroban#227e84ab10ae627584b087e95f41270704b584f7"
+dependencies = [
+ "stubs",
+]
+
+[[package]]
+name = "cfg-if"
+version = "1.0.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd"
+
+[[package]]
+name = "chrono"
+version = "0.4.39"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "7e36cc9d416881d2e24f9a963be5fb1cd90966419ac844274161d10488b3e825"
+dependencies = [
+ "android-tzdata",
+ "iana-time-zone",
+ "num-traits",
+ "serde",
+ "windows-targets",
+]
+
+[[package]]
+name = "const-oid"
+version = "0.9.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "c2459377285ad874054d797f3ccebf984978aa39129f6eafde5cdc8315b612f8"
+
+[[package]]
+name = "core-foundation-sys"
+version = "0.8.7"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "773648b94d0e5d620f64f280777445740e61fe701025087ec8b57f45c791888b"
+
+[[package]]
+name = "cpufeatures"
+version = "0.2.16"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "16b80225097f2e5ae4e7179dd2266824648f3e2f49d9134d584b76389d31c4c3"
+dependencies = [
+ "libc",
+]
+
+[[package]]
+name = "crate-git-revision"
+version = "0.0.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "c521bf1f43d31ed2f73441775ed31935d77901cb3451e44b38a1c1612fcbaf98"
+dependencies = [
+ "serde",
+ "serde_derive",
+ "serde_json",
+]
+
+[[package]]
+name = "crypto-bigint"
+version = "0.5.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "0dc92fb57ca44df6db8059111ab3af99a63d5d0f8375d9972e319a379c6bab76"
+dependencies = [
+ "generic-array",
+ "rand_core",
+ "subtle",
+ "zeroize",
+]
+
+[[package]]
+name = "crypto-common"
+version = "0.1.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1bfb12502f3fc46cca1bb51ac28df9d618d813cdc3d2f25b9fe775a34af26bb3"
+dependencies = [
+ "generic-array",
+ "typenum",
+]
+
+[[package]]
+name = "ctor"
+version = "0.2.9"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "32a2785755761f3ddc1492979ce1e48d2c00d09311c39e4466429188f3dd6501"
+dependencies = [
+ "quote",
+ "syn",
+]
+
+[[package]]
+name = "curve25519-dalek"
+version = "4.1.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "97fb8b7c4503de7d6ae7b42ab72a5a59857b4c937ec27a3d4539dba95b5ab2be"
+dependencies = [
+ "cfg-if",
+ "cpufeatures",
+ "curve25519-dalek-derive",
+ "digest",
+ "fiat-crypto",
+ "rustc_version",
+ "subtle",
+ "zeroize",
+]
+
+[[package]]
+name = "curve25519-dalek-derive"
+version = "0.1.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f46882e17999c6cc590af592290432be3bce0428cb0d5f8b6715e4dc7b383eb3"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn",
+]
+
+[[package]]
+name = "darling"
+version = "0.20.10"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "6f63b86c8a8826a49b8c21f08a2d07338eec8d900540f8630dc76284be802989"
+dependencies = [
+ "darling_core",
+ "darling_macro",
+]
+
+[[package]]
+name = "darling_core"
+version = "0.20.10"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "95133861a8032aaea082871032f5815eb9e98cef03fa916ab4500513994df9e5"
+dependencies = [
+ "fnv",
+ "ident_case",
+ "proc-macro2",
+ "quote",
+ "strsim",
+ "syn",
+]
+
+[[package]]
+name = "darling_macro"
+version = "0.20.10"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d336a2a514f6ccccaa3e09b02d41d35330c07ddf03a62165fcec10bb561c7806"
+dependencies = [
+ "darling_core",
+ "quote",
+ "syn",
+]
+
+[[package]]
+name = "der"
+version = "0.7.9"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f55bf8e7b65898637379c1b74eb1551107c8294ed26d855ceb9fd1a09cfc9bc0"
+dependencies = [
+ "const-oid",
+ "zeroize",
+]
+
+[[package]]
+name = "deranged"
+version = "0.3.11"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b42b6fa04a440b495c8b04d0e71b707c585f83cb9cb28cf8cd0d976c315e31b4"
+dependencies = [
+ "powerfmt",
+ "serde",
+]
+
+[[package]]
+name = "derive_arbitrary"
+version = "1.3.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "67e77553c4162a157adbf834ebae5b415acbecbeafc7a74b0e886657506a7611"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn",
+]
+
+[[package]]
+name = "digest"
+version = "0.10.7"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9ed9a281f7bc9b7576e61468ba615a66a5c8cfdff42420a70aa82701a3b1e292"
+dependencies = [
+ "block-buffer",
+ "const-oid",
+ "crypto-common",
+ "subtle",
+]
+
+[[package]]
+name = "downcast-rs"
+version = "1.2.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "75b325c5dbd37f80359721ad39aca5a29fb04c89279657cffdda8736d0c0b9d2"
+
+[[package]]
+name = "ecdsa"
+version = "0.16.9"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ee27f32b5c5292967d2d4a9d7f1e0b0aed2c15daded5a60300e4abb9d8020bca"
+dependencies = [
+ "der",
+ "digest",
+ "elliptic-curve",
+ "rfc6979",
+ "signature",
+]
+
+[[package]]
+name = "ed25519"
+version = "2.2.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "115531babc129696a58c64a4fef0a8bf9e9698629fb97e9e40767d235cfbcd53"
+dependencies = [
+ "pkcs8",
+ "signature",
+]
+
+[[package]]
+name = "ed25519-dalek"
+version = "2.1.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "4a3daa8e81a3963a60642bcc1f90a670680bd4a77535faa384e9d1c79d620871"
+dependencies = [
+ "curve25519-dalek",
+ "ed25519",
+ "rand_core",
+ "serde",
+ "sha2",
+ "subtle",
+ "zeroize",
+]
+
+[[package]]
+name = "either"
+version = "1.13.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "60b1af1c220855b6ceac025d3f6ecdd2b7c4894bfe9cd9bda4fbb4bc7c0d4cf0"
+
+[[package]]
+name = "elliptic-curve"
+version = "0.13.8"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b5e6043086bf7973472e0c7dff2142ea0b680d30e18d9cc40f267efbf222bd47"
+dependencies = [
+ "base16ct",
+ "crypto-bigint",
+ "digest",
+ "ff",
+ "generic-array",
+ "group",
+ "rand_core",
+ "sec1",
+ "subtle",
+ "zeroize",
+]
+
+[[package]]
+name = "equivalent"
+version = "1.0.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5443807d6dff69373d433ab9ef5378ad8df50ca6298caf15de6e52e24aaf54d5"
+
+[[package]]
+name = "escape-bytes"
+version = "0.1.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "2bfcf67fea2815c2fc3b90873fae90957be12ff417335dfadc7f52927feb03b2"
+
+[[package]]
+name = "ethnum"
+version = "1.5.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b90ca2580b73ab6a1f724b76ca11ab632df820fd6040c336200d2c1df7b3c82c"
+
+[[package]]
+name = "ff"
+version = "0.13.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ded41244b729663b1e574f1b4fb731469f69f79c17667b5d776b16cda0479449"
+dependencies = [
+ "rand_core",
+ "subtle",
+]
+
+[[package]]
+name = "fiat-crypto"
+version = "0.2.9"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "28dea519a9695b9977216879a3ebfddf92f1c08c05d984f8996aecd6ecdc811d"
+
+[[package]]
+name = "fnv"
+version = "1.0.7"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "3f9eec918d3f24069decb9af1554cad7c880e2da24a9afd88aca000531ab82c1"
+
+[[package]]
+name = "generic-array"
+version = "0.14.7"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "85649ca51fd72272d7821adaf274ad91c288277713d9c18820d8499a7ff69e9a"
+dependencies = [
+ "typenum",
+ "version_check",
+ "zeroize",
+]
+
+[[package]]
+name = "getrandom"
+version = "0.2.15"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "c4567c8db10ae91089c99af84c68c38da3ec2f087c3f82960bcdbf3656b6f4d7"
+dependencies = [
+ "cfg-if",
+ "js-sys",
+ "libc",
+ "wasi",
+ "wasm-bindgen",
+]
+
+[[package]]
+name = "gimli"
+version = "0.31.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "07e28edb80900c19c28f1072f2e8aeca7fa06b23cd4169cefe1af5aa3260783f"
+
+[[package]]
+name = "group"
+version = "0.13.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f0f9ef7462f7c099f518d754361858f86d8a07af53ba9af0fe635bbccb151a63"
+dependencies = [
+ "ff",
+ "rand_core",
+ "subtle",
+]
+
+[[package]]
+name = "hashbrown"
+version = "0.12.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8a9ee70c43aaf417c914396645a0fa852624801b24ebb7ae78fe8272889ac888"
+
+[[package]]
+name = "hashbrown"
+version = "0.15.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "bf151400ff0baff5465007dd2f3e717f3fe502074ca563069ce3a6629d07b289"
+
+[[package]]
+name = "hex"
+version = "0.4.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "7f24254aa9a54b5c858eaee2f5bccdb46aaf0e486a595ed5fd8f86ba55232a70"
+dependencies = [
+ "serde",
+]
+
+[[package]]
+name = "hex-literal"
+version = "0.4.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "6fe2267d4ed49bc07b63801559be28c718ea06c4738b7a03c94df7386d2cde46"
+
+[[package]]
+name = "hmac"
+version = "0.12.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "6c49c37c09c17a53d937dfbb742eb3a961d65a994e6bcdcf37e7399d0cc8ab5e"
+dependencies = [
+ "digest",
+]
+
+[[package]]
+name = "iana-time-zone"
+version = "0.1.61"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "235e081f3925a06703c2d0117ea8b91f042756fd6e7a6e5d901e8ca1a996b220"
+dependencies = [
+ "android_system_properties",
+ "core-foundation-sys",
+ "iana-time-zone-haiku",
+ "js-sys",
+ "wasm-bindgen",
+ "windows-core",
+]
+
+[[package]]
+name = "iana-time-zone-haiku"
+version = "0.1.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f31827a206f56af32e590ba56d5d2d085f558508192593743f16b2306495269f"
+dependencies = [
+ "cc",
+]
+
+[[package]]
+name = "ident_case"
+version = "1.0.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b9e0384b61958566e926dc50660321d12159025e767c18e043daf26b70104c39"
+
+[[package]]
+name = "indexmap"
+version = "1.9.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "bd070e393353796e801d209ad339e89596eb4c8d430d18ede6a1cced8fafbd99"
+dependencies = [
+ "autocfg",
+ "hashbrown 0.12.3",
+ "serde",
+]
+
+[[package]]
+name = "indexmap"
+version = "2.7.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "62f822373a4fe84d4bb149bf54e584a7f4abec90e072ed49cda0edea5b95471f"
+dependencies = [
+ "equivalent",
+ "hashbrown 0.15.2",
+ "serde",
+]
+
+[[package]]
+name = "indexmap-nostd"
+version = "0.4.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8e04e2fd2b8188ea827b32ef11de88377086d690286ab35747ef7f9bf3ccb590"
+
+[[package]]
+name = "itertools"
+version = "0.11.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b1c173a5686ce8bfa551b3563d0c2170bf24ca44da99c7ca4bfdab5418c3fe57"
+dependencies = [
+ "either",
+]
+
+[[package]]
+name = "itoa"
+version = "1.0.14"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d75a2a4b1b190afb6f5425f10f6a8f959d2ea0b9c2b1d79553551850539e4674"
+
+[[package]]
+name = "js-sys"
+version = "0.3.76"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "6717b6b5b077764fb5966237269cb3c64edddde4b14ce42647430a78ced9e7b7"
+dependencies = [
+ "once_cell",
+ "wasm-bindgen",
+]
+
+[[package]]
+name = "k256"
+version = "0.13.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f6e3919bbaa2945715f0bb6d3934a173d1e9a59ac23767fbaaef277265a7411b"
+dependencies = [
+ "cfg-if",
+ "ecdsa",
+ "elliptic-curve",
+ "sha2",
+]
+
+[[package]]
+name = "keccak"
+version = "0.1.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ecc2af9a1119c51f12a14607e783cb977bde58bc069ff0c3da1095e635d70654"
+dependencies = [
+ "cpufeatures",
+]
+
+[[package]]
+name = "libc"
+version = "0.2.169"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b5aba8db14291edd000dfcc4d620c7ebfb122c613afb886ca8803fa4e128a20a"
+
+[[package]]
+name = "libm"
+version = "0.2.11"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8355be11b20d696c8f18f6cc018c4e372165b1fa8126cef092399c9951984ffa"
+
+[[package]]
+name = "log"
+version = "0.4.22"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a7a70ba024b9dc04c27ea2f0c0548feb474ec5c54bba33a7f72f873a39d07b24"
+
+[[package]]
+name = "memchr"
+version = "2.7.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "78ca9ab1a0babb1e7d5695e3530886289c18cf2f87ec19a575a0abdce112e3a3"
+
+[[package]]
+name = "miniz_oxide"
+version = "0.8.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "4ffbe83022cedc1d264172192511ae958937694cd57ce297164951b8b3568394"
+dependencies = [
+ "adler2",
+]
+
+[[package]]
+name = "nondet"
+version = "0.2.0"
+source = "git+https://github.com/Certora/solana-cvt.git?branch=dev-soroban#227e84ab10ae627584b087e95f41270704b584f7"
+dependencies = [
+ "certora",
+ "stubs",
+]
+
+[[package]]
+name = "num-bigint"
+version = "0.4.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a5e44f723f1133c9deac646763579fdb3ac745e418f2a7af9cd0c431da1f20b9"
+dependencies = [
+ "num-integer",
+ "num-traits",
+]
+
+[[package]]
+name = "num-conv"
+version = "0.1.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "51d515d32fb182ee37cda2ccdcb92950d6a3c2893aa280e540671c2cd0f3b1d9"
+
+[[package]]
+name = "num-derive"
+version = "0.4.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ed3955f1a9c7c0c15e092f9c887db08b1fc683305fdf6eb6684f22555355e202"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn",
+]
+
+[[package]]
+name = "num-integer"
+version = "0.1.46"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "7969661fd2958a5cb096e56c8e1ad0444ac2bbcd0061bd28660485a44879858f"
+dependencies = [
+ "num-traits",
+]
+
+[[package]]
+name = "num-traits"
+version = "0.2.19"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "071dfc062690e90b734c0b2273ce72ad0ffa95f0c74596bc250dcfd960262841"
+dependencies = [
+ "autocfg",
+]
+
+[[package]]
+name = "object"
+version = "0.36.7"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "62948e14d923ea95ea2c7c86c71013138b66525b86bdc08d2dcc262bdb497b87"
+dependencies = [
+ "memchr",
+]
+
+[[package]]
+name = "once_cell"
+version = "1.20.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1261fe7e33c73b354eab43b1273a57c8f967d0391e80353e51f764ac02cf6775"
+
+[[package]]
+name = "p256"
+version = "0.13.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "c9863ad85fa8f4460f9c48cb909d38a0d689dba1f6f6988a5e3e0d31071bcd4b"
+dependencies = [
+ "ecdsa",
+ "elliptic-curve",
+ "primeorder",
+ "sha2",
+]
+
+[[package]]
+name = "paste"
+version = "1.0.15"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "57c0d7b74b563b49d38dae00a0c37d4d6de9b432382b2892f0574ddcae73fd0a"
+
+[[package]]
+name = "pkcs8"
+version = "0.10.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f950b2377845cebe5cf8b5165cb3cc1a5e0fa5cfa3e1f7f55707d8fd82e0a7b7"
+dependencies = [
+ "der",
+ "spki",
+]
+
+[[package]]
+name = "powerfmt"
+version = "0.2.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "439ee305def115ba05938db6eb1644ff94165c5ab5e9420d1c1bcedbba909391"
+
+[[package]]
+name = "ppv-lite86"
+version = "0.2.20"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "77957b295656769bb8ad2b6a6b09d897d94f05c41b069aede1fcdaa675eaea04"
+dependencies = [
+ "zerocopy",
+]
+
+[[package]]
+name = "prettyplease"
+version = "0.2.25"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "64d1ec885c64d0457d564db4ec299b2dae3f9c02808b8ad9c3a089c591b18033"
+dependencies = [
+ "proc-macro2",
+ "syn",
+]
+
+[[package]]
+name = "primeorder"
+version = "0.13.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "353e1ca18966c16d9deb1c69278edbc5f194139612772bd9537af60ac231e1e6"
+dependencies = [
+ "elliptic-curve",
+]
+
+[[package]]
+name = "proc-macro2"
+version = "1.0.92"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "37d3544b3f2748c54e147655edb5025752e2303145b5aefb3c3ea2c78b973bb0"
+dependencies = [
+ "unicode-ident",
+]
+
+[[package]]
+name = "quote"
+version = "1.0.37"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b5b9d34b8991d19d98081b46eacdd8eb58c6f2b201139f7c5f643cc155a633af"
+dependencies = [
+ "proc-macro2",
+]
+
+[[package]]
+name = "rand"
+version = "0.8.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "34af8d1a0e25924bc5b7c43c079c942339d8f0a8b57c39049bef581b46327404"
+dependencies = [
+ "libc",
+ "rand_chacha",
+ "rand_core",
+]
+
+[[package]]
+name = "rand_chacha"
+version = "0.3.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e6c10a63a0fa32252be49d21e7709d4d4baf8d231c2dbce1eaa8141b9b127d88"
+dependencies = [
+ "ppv-lite86",
+ "rand_core",
+]
+
+[[package]]
+name = "rand_core"
+version = "0.6.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ec0be4795e2f6a28069bec0b5ff3e2ac9bafc99e6a9a7dc3547996c5c816922c"
+dependencies = [
+ "getrandom",
+]
+
+[[package]]
+name = "rfc6979"
+version = "0.4.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f8dd2a808d456c4a54e300a23e9f5a67e122c3024119acbfd73e3bf664491cb2"
+dependencies = [
+ "hmac",
+ "subtle",
+]
+
+[[package]]
+name = "rustc-demangle"
+version = "0.1.24"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "719b953e2095829ee67db738b3bfa9fa368c94900df327b3f07fe6e794d2fe1f"
+
+[[package]]
+name = "rustc_version"
+version = "0.4.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "cfcb3a22ef46e85b45de6ee7e79d063319ebb6594faafcf1c225ea92ab6e9b92"
+dependencies = [
+ "semver",
+]
+
+[[package]]
+name = "ryu"
+version = "1.0.18"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f3cb5ba0dc43242ce17de99c180e96db90b235b8a9fdc9543c96d2209116bd9f"
+
+[[package]]
+name = "sec1"
+version = "0.7.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d3e97a565f76233a6003f9f5c54be1d9c5bdfa3eccfb189469f11ec4901c47dc"
+dependencies = [
+ "base16ct",
+ "der",
+ "generic-array",
+ "subtle",
+ "zeroize",
+]
+
+[[package]]
+name = "semver"
+version = "1.0.24"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "3cb6eb87a131f756572d7fb904f6e7b68633f09cca868c5df1c4b8d1a694bbba"
+
+[[package]]
+name = "serde"
+version = "1.0.216"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "0b9781016e935a97e8beecf0c933758c97a5520d32930e460142b4cd80c6338e"
+dependencies = [
+ "serde_derive",
+]
+
+[[package]]
+name = "serde_derive"
+version = "1.0.216"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "46f859dbbf73865c6627ed570e78961cd3ac92407a2d117204c49232485da55e"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn",
+]
+
+[[package]]
+name = "serde_json"
+version = "1.0.134"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d00f4175c42ee48b15416f6193a959ba3a0d67fc699a0db9ad12df9f83991c7d"
+dependencies = [
+ "itoa",
+ "memchr",
+ "ryu",
+ "serde",
+]
+
+[[package]]
+name = "serde_with"
+version = "3.11.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8e28bdad6db2b8340e449f7108f020b3b092e8583a9e3fb82713e1d4e71fe817"
+dependencies = [
+ "base64 0.22.1",
+ "chrono",
+ "hex",
+ "indexmap 1.9.3",
+ "indexmap 2.7.0",
+ "serde",
+ "serde_derive",
+ "serde_json",
+ "serde_with_macros",
+ "time",
+]
+
+[[package]]
+name = "serde_with_macros"
+version = "3.11.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9d846214a9854ef724f3da161b426242d8de7c1fc7de2f89bb1efcb154dca79d"
+dependencies = [
+ "darling",
+ "proc-macro2",
+ "quote",
+ "syn",
+]
+
+[[package]]
+name = "sha2"
+version = "0.10.8"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "793db75ad2bcafc3ffa7c68b215fee268f537982cd901d132f89c6343f3a3dc8"
+dependencies = [
+ "cfg-if",
+ "cpufeatures",
+ "digest",
+]
+
+[[package]]
+name = "sha3"
+version = "0.10.8"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "75872d278a8f37ef87fa0ddbda7802605cb18344497949862c0d4dcb291eba60"
+dependencies = [
+ "digest",
+ "keccak",
+]
+
+[[package]]
+name = "shlex"
+version = "1.3.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "0fda2ff0d084019ba4d7c6f371c95d8fd75ce3524c3cb8fb653a3023f6323e64"
+
+[[package]]
+name = "signature"
+version = "2.2.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "77549399552de45a898a580c1b41d445bf730df867cc44e6c0233bbc4b8329de"
+dependencies = [
+ "digest",
+ "rand_core",
+]
+
+[[package]]
+name = "smallvec"
+version = "1.13.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "3c5e1a9a646d36c3599cd173a41282daf47c44583ad367b8e6837255952e5c67"
+
+[[package]]
+name = "soroban-builtin-sdk-macros"
+version = "21.2.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "2f57a68ef8777e28e274de0f3a88ad9a5a41d9a2eb461b4dd800b086f0e83b80"
+dependencies = [
+ "itertools",
+ "proc-macro2",
+ "quote",
+ "syn",
+]
+
+[[package]]
+name = "soroban-env-common"
+version = "21.2.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "2fd1c89463835fe6da996318156d39f424b4f167c725ec692e5a7a2d4e694b3d"
+dependencies = [
+ "arbitrary",
+ "crate-git-revision",
+ "ethnum",
+ "num-derive",
+ "num-traits",
+ "serde",
+ "soroban-env-macros",
+ "soroban-wasmi",
+ "static_assertions",
+ "stellar-xdr",
+ "wasmparser",
+]
+
+[[package]]
+name = "soroban-env-guest"
+version = "21.2.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "6bfb2536811045d5cd0c656a324cbe9ce4467eb734c7946b74410d90dea5d0ce"
+dependencies = [
+ "soroban-env-common",
+ "static_assertions",
+]
+
+[[package]]
+name = "soroban-env-host"
+version = "21.2.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "2b7a32c28f281c423189f1298960194f0e0fc4eeb72378028171e556d8cd6160"
+dependencies = [
+ "backtrace",
+ "curve25519-dalek",
+ "ecdsa",
+ "ed25519-dalek",
+ "elliptic-curve",
+ "generic-array",
+ "getrandom",
+ "hex-literal",
+ "hmac",
+ "k256",
+ "num-derive",
+ "num-integer",
+ "num-traits",
+ "p256",
+ "rand",
+ "rand_chacha",
+ "sec1",
+ "sha2",
+ "sha3",
+ "soroban-builtin-sdk-macros",
+ "soroban-env-common",
+ "soroban-wasmi",
+ "static_assertions",
+ "stellar-strkey",
+ "wasmparser",
+]
+
+[[package]]
+name = "soroban-env-macros"
+version = "21.2.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "242926fe5e0d922f12d3796cd7cd02dd824e5ef1caa088f45fce20b618309f64"
+dependencies = [
+ "itertools",
+ "proc-macro2",
+ "quote",
+ "serde",
+ "serde_json",
+ "stellar-xdr",
+ "syn",
+]
+
+[[package]]
+name = "soroban-hello-world-contract"
+version = "0.0.0"
+dependencies = [
+ "certora",
+ "nondet",
+ "soroban-sdk",
+]
+
+[[package]]
+name = "soroban-ledger-snapshot"
+version = "21.7.7"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e6edf92749fd8399b417192d301c11f710b9cdce15789a3d157785ea971576fa"
+dependencies = [
+ "serde",
+ "serde_json",
+ "serde_with",
+ "soroban-env-common",
+ "soroban-env-host",
+ "thiserror",
+]
+
+[[package]]
+name = "soroban-sdk"
+version = "21.7.7"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "7dcdf04484af7cc731a7a48ad1d9f5f940370edeea84734434ceaf398a6b862e"
+dependencies = [
+ "arbitrary",
+ "bytes-lit",
+ "ctor",
+ "derive_arbitrary",
+ "ed25519-dalek",
+ "rand",
+ "rustc_version",
+ "serde",
+ "serde_json",
+ "soroban-env-guest",
+ "soroban-env-host",
+ "soroban-ledger-snapshot",
+ "soroban-sdk-macros",
+ "stellar-strkey",
+]
+
+[[package]]
+name = "soroban-sdk-macros"
+version = "21.7.7"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "0974e413731aeff2443f2305b344578b3f1ffd18335a7ba0f0b5d2eb4e94c9ce"
+dependencies = [
+ "crate-git-revision",
+ "darling",
+ "itertools",
+ "proc-macro2",
+ "quote",
+ "rustc_version",
+ "sha2",
+ "soroban-env-common",
+ "soroban-spec",
+ "soroban-spec-rust",
+ "stellar-xdr",
+ "syn",
+]
+
+[[package]]
+name = "soroban-spec"
+version = "21.7.7"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "c2c70b20e68cae3ef700b8fa3ae29db1c6a294b311fba66918f90cb8f9fd0a1a"
+dependencies = [
+ "base64 0.13.1",
+ "stellar-xdr",
+ "thiserror",
+ "wasmparser",
+]
+
+[[package]]
+name = "soroban-spec-rust"
+version = "21.7.7"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a2dafbde981b141b191c6c036abc86097070ddd6eaaa33b273701449501e43d3"
+dependencies = [
+ "prettyplease",
+ "proc-macro2",
+ "quote",
+ "sha2",
+ "soroban-spec",
+ "stellar-xdr",
+ "syn",
+ "thiserror",
+]
+
+[[package]]
+name = "soroban-wasmi"
+version = "0.31.1-soroban.20.0.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "710403de32d0e0c35375518cb995d4fc056d0d48966f2e56ea471b8cb8fc9719"
+dependencies = [
+ "smallvec",
+ "spin",
+ "wasmi_arena",
+ "wasmi_core",
+ "wasmparser-nostd",
+]
+
+[[package]]
+name = "spin"
+version = "0.9.8"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "6980e8d7511241f8acf4aebddbb1ff938df5eebe98691418c4468d0b72a96a67"
+
+[[package]]
+name = "spki"
+version = "0.7.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d91ed6c858b01f942cd56b37a94b3e0a1798290327d1236e4d9cf4eaca44d29d"
+dependencies = [
+ "base64ct",
+ "der",
+]
+
+[[package]]
+name = "static_assertions"
+version = "1.1.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a2eb9349b6444b326872e140eb1cf5e7c522154d69e7a0ffb0fb81c06b37543f"
+
+[[package]]
+name = "stellar-strkey"
+version = "0.0.8"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "12d2bf45e114117ea91d820a846fd1afbe3ba7d717988fee094ce8227a3bf8bd"
+dependencies = [
+ "base32",
+ "crate-git-revision",
+ "thiserror",
+]
+
+[[package]]
+name = "stellar-xdr"
+version = "21.2.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "2675a71212ed39a806e415b0dbf4702879ff288ec7f5ee996dda42a135512b50"
+dependencies = [
+ "arbitrary",
+ "base64 0.13.1",
+ "crate-git-revision",
+ "escape-bytes",
+ "hex",
+ "serde",
+ "serde_with",
+ "stellar-strkey",
+]
+
+[[package]]
+name = "strsim"
+version = "0.11.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "7da8b5736845d9f2fcb837ea5d9e2628564b3b043a70948a3f0b778838c5fb4f"
+
+[[package]]
+name = "stubs"
+version = "0.1.0"
+source = "git+https://github.com/Certora/solana-cvt.git?branch=dev-soroban#227e84ab10ae627584b087e95f41270704b584f7"
+
+[[package]]
+name = "subtle"
+version = "2.6.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "13c2bddecc57b384dee18652358fb23172facb8a2c51ccc10d74c157bdea3292"
+
+[[package]]
+name = "syn"
+version = "2.0.91"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d53cbcb5a243bd33b7858b1d7f4aca2153490815872d86d955d6ea29f743c035"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "unicode-ident",
+]
+
+[[package]]
+name = "thiserror"
+version = "1.0.69"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b6aaf5339b578ea85b50e080feb250a3e8ae8cfcdff9a461c9ec2904bc923f52"
+dependencies = [
+ "thiserror-impl",
+]
+
+[[package]]
+name = "thiserror-impl"
+version = "1.0.69"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "4fee6c4efc90059e10f81e6d42c60a18f76588c3d74cb83a0b242a2b6c7504c1"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn",
+]
+
+[[package]]
+name = "time"
+version = "0.3.37"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "35e7868883861bd0e56d9ac6efcaaca0d6d5d82a2a7ec8209ff492c07cf37b21"
+dependencies = [
+ "deranged",
+ "itoa",
+ "num-conv",
+ "powerfmt",
+ "serde",
+ "time-core",
+ "time-macros",
+]
+
+[[package]]
+name = "time-core"
+version = "0.1.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ef927ca75afb808a4d64dd374f00a2adf8d0fcff8e7b184af886c3c87ec4a3f3"
+
+[[package]]
+name = "time-macros"
+version = "0.2.19"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "2834e6017e3e5e4b9834939793b282bc03b37a3336245fa820e35e233e2a85de"
+dependencies = [
+ "num-conv",
+ "time-core",
+]
+
+[[package]]
+name = "typenum"
+version = "1.17.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "42ff0bf0c66b8238c6f3b578df37d0b7848e55df8577b3f74f92a69acceeb825"
+
+[[package]]
+name = "unicode-ident"
+version = "1.0.14"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "adb9e6ca4f869e1180728b7950e35922a7fc6397f7b641499e8f3ef06e50dc83"
+
+[[package]]
+name = "version_check"
+version = "0.9.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a"
+
+[[package]]
+name = "wasi"
+version = "0.11.0+wasi-snapshot-preview1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9c8d87e72b64a3b4db28d11ce29237c246188f4f51057d65a7eab63b7987e423"
+
+[[package]]
+name = "wasm-bindgen"
+version = "0.2.99"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a474f6281d1d70c17ae7aa6a613c87fce69a127e2624002df63dcb39d6cf6396"
+dependencies = [
+ "cfg-if",
+ "once_cell",
+ "wasm-bindgen-macro",
+]
+
+[[package]]
+name = "wasm-bindgen-backend"
+version = "0.2.99"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5f89bb38646b4f81674e8f5c3fb81b562be1fd936d84320f3264486418519c79"
+dependencies = [
+ "bumpalo",
+ "log",
+ "proc-macro2",
+ "quote",
+ "syn",
+ "wasm-bindgen-shared",
+]
+
+[[package]]
+name = "wasm-bindgen-macro"
+version = "0.2.99"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "2cc6181fd9a7492eef6fef1f33961e3695e4579b9872a6f7c83aee556666d4fe"
+dependencies = [
+ "quote",
+ "wasm-bindgen-macro-support",
+]
+
+[[package]]
+name = "wasm-bindgen-macro-support"
+version = "0.2.99"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "30d7a95b763d3c45903ed6c81f156801839e5ee968bb07e534c44df0fcd330c2"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn",
+ "wasm-bindgen-backend",
+ "wasm-bindgen-shared",
+]
+
+[[package]]
+name = "wasm-bindgen-shared"
+version = "0.2.99"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "943aab3fdaaa029a6e0271b35ea10b72b943135afe9bffca82384098ad0e06a6"
+
+[[package]]
+name = "wasmi_arena"
+version = "0.4.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "104a7f73be44570cac297b3035d76b169d6599637631cf37a1703326a0727073"
+
+[[package]]
+name = "wasmi_core"
+version = "0.13.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "dcf1a7db34bff95b85c261002720c00c3a6168256dcb93041d3fa2054d19856a"
+dependencies = [
+ "downcast-rs",
+ "libm",
+ "num-traits",
+ "paste",
+]
+
+[[package]]
+name = "wasmparser"
+version = "0.116.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a58e28b80dd8340cb07b8242ae654756161f6fc8d0038123d679b7b99964fa50"
+dependencies = [
+ "indexmap 2.7.0",
+ "semver",
+]
+
+[[package]]
+name = "wasmparser-nostd"
+version = "0.100.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d5a015fe95f3504a94bb1462c717aae75253e39b9dd6c3fb1062c934535c64aa"
+dependencies = [
+ "indexmap-nostd",
+]
+
+[[package]]
+name = "windows-core"
+version = "0.52.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "33ab640c8d7e35bf8ba19b884ba838ceb4fba93a4e8c65a9059d08afcfc683d9"
+dependencies = [
+ "windows-targets",
+]
+
+[[package]]
+name = "windows-targets"
+version = "0.52.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9b724f72796e036ab90c1021d4780d4d3d648aca59e491e6b98e725b84e99973"
+dependencies = [
+ "windows_aarch64_gnullvm",
+ "windows_aarch64_msvc",
+ "windows_i686_gnu",
+ "windows_i686_gnullvm",
+ "windows_i686_msvc",
+ "windows_x86_64_gnu",
+ "windows_x86_64_gnullvm",
+ "windows_x86_64_msvc",
+]
+
+[[package]]
+name = "windows_aarch64_gnullvm"
+version = "0.52.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "32a4622180e7a0ec044bb555404c800bc9fd9ec262ec147edd5989ccd0c02cd3"
+
+[[package]]
+name = "windows_aarch64_msvc"
+version = "0.52.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "09ec2a7bb152e2252b53fa7803150007879548bc709c039df7627cabbd05d469"
+
+[[package]]
+name = "windows_i686_gnu"
+version = "0.52.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8e9b5ad5ab802e97eb8e295ac6720e509ee4c243f69d781394014ebfe8bbfa0b"
+
+[[package]]
+name = "windows_i686_gnullvm"
+version = "0.52.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "0eee52d38c090b3caa76c563b86c3a4bd71ef1a819287c19d586d7334ae8ed66"
+
+[[package]]
+name = "windows_i686_msvc"
+version = "0.52.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "240948bc05c5e7c6dabba28bf89d89ffce3e303022809e73deaefe4f6ec56c66"
+
+[[package]]
+name = "windows_x86_64_gnu"
+version = "0.52.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "147a5c80aabfbf0c7d901cb5895d1de30ef2907eb21fbbab29ca94c5b08b1a78"
+
+[[package]]
+name = "windows_x86_64_gnullvm"
+version = "0.52.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "24d5b23dc417412679681396f2b49f3de8c1473deb516bd34410872eff51ed0d"
+
+[[package]]
+name = "windows_x86_64_msvc"
+version = "0.52.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "589f6da84c646204747d1270a2a5661ea66ed1cced2631d546fdfb155959f9ec"
+
+[[package]]
+name = "zerocopy"
+version = "0.7.35"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1b9b4fd18abc82b8136838da5d50bae7bdea537c574d8dc1a34ed098d6c166f0"
+dependencies = [
+ "byteorder",
+ "zerocopy-derive",
+]
+
+[[package]]
+name = "zerocopy-derive"
+version = "0.7.35"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "fa4f8080344d4671fb4e831a13ad1e68092748387dfc4f55e356242fae12ce3e"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn",
+]
+
+[[package]]
+name = "zeroize"
+version = "1.8.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ced3678a2879b30306d323f4542626697a464a97c0a07c9aebf7ebca65cd4dde"
diff --git a/Soroban/hello_world/Cargo.toml b/Soroban/hello_world/Cargo.toml
new file mode 100644
index 00000000..f511b8b6
--- /dev/null
+++ b/Soroban/hello_world/Cargo.toml
@@ -0,0 +1,34 @@
+[package]
+name = "soroban-hello-world-contract"
+version = "0.0.0"
+edition = "2021"
+publish = false
+
+[lib]
+crate-type = ["cdylib"]
+doctest = false
+
+[dependencies]
+soroban-sdk = { version = "21.7.4" }
+nondet = {git = "https://github.com/Certora/solana-cvt.git", branch="dev-soroban", default-features=false}
+certora = {git = "https://github.com/Certora/solana-cvt.git", branch="dev-soroban"}
+
+[dev-dependencies]
+soroban-sdk = { version = "21.7.4", features = ["testutils"] }
+
+[profile.release]
+opt-level = "z"
+overflow-checks = true
+debug = 0
+strip = "symbols"
+debug-assertions = false
+panic = "abort"
+codegen-units = 1
+lto = true
+
+[profile.release-with-logs]
+inherits = "release"
+debug-assertions = true
+
+[features]
+certora = []
diff --git a/Soroban/hello_world/README.md b/Soroban/hello_world/README.md
new file mode 100644
index 00000000..f341f43d
--- /dev/null
+++ b/Soroban/hello_world/README.md
@@ -0,0 +1,103 @@
+# Soroban Hello World Contract Example
+
+This example demonstrates how to use Certora's Prover with a Soroban smart contract. It includes configurations for both the old and new formats to showcase their differences and execution.
+
+---
+
+## Overview
+
+This project includes:
+- A Soroban Hello World contract written in Rust.
+- Configurations for running the Certora Prover with old and new formats.
+- A `certora_build.py` script for compiling and preparing the project for verification.
+
+---
+
+## Contract Details
+
+The contract is located in `lib.rs` and implements a simple `hello` function, which is used to demonstrate the Certora Prover's capabilities.
+
+---
+
+## Configuration Formats
+
+### Old Format
+The old format configuration (`hello_world_old_format.conf`) explicitly specifies the `files` field, pointing to the compiled WebAssembly (`.wasm`) file:
+
+```json
+{
+    "files": [
+        "soroban_hello_world_contract.wasm"
+    ],
+    "process": "emv",
+    "optimistic_loop": true,
+    "rule": "hello"
+}
+```
+
+### New Format
+The new format configuration (`hello_world_new_fromat.conf`) leverages a `build_script` for dynamic building and eliminates the need for hardcoded file paths:
+
+```json
+{
+    "build_script": "./certora_build.py",
+    "process": "emv",
+    "optimistic_loop": true,
+    "rule": "hello"
+}
+```
+
+**Key Difference:**
+- **Old Format:** Requires manual specification of the `.wasm` file.
+- **New Format:** Automatically builds the project using the specified build script.
+
+---
+
+## Execution Examples
+
+### Running with the New Format
+```bash
+certoraRun hello_world_new_fromat.conf
+```
+
+**Expected Output:**
+```
+INFO: Building from script ./certora_build.py
+WARNING: certora-cli-alpha-master
+
+Connecting to server...
+
+Job submitted to server
+
+Manage your jobs at https://vaas-stg.certora.com
+Follow your job and see verification results at https://vaas-stg.certora.com/output/1512/c3effd5d69924d4ab6e5279c5615a9b6?anonymousKey=f9184e62e3c12c47df11f2a16c68fc08acc5c07e
+```
+
+### Running with the Old Format
+```bash
+certoraRun hello_world_old_format.conf
+
+**Expected Output:**
+```
+WARNING: Note: attribute files value in CLI (hello_world_old_format.conf) overrides value stored in conf file (soroban_hello_world_contract.wasm)
+WARNING: certora-cli-alpha-master
+
+Connecting to server...
+
+Job submitted to server
+
+Manage your jobs at https://vaas-stg.certora.com
+Follow your job and see verification results at https://vaas-stg.certora.com/output/1512/4be870495a214f2c955d02268219dd90?anonymousKey=a9907295b95f8c82bd0321fcc070cb894f9499d8
+```
+
+---
+
+## Building the Project
+
+The `certora_build.py` script compiles the contract and prepares it for verification:
+```bash
+python3 certora_build.py
+```
+
+This ensures the `soroban_hello_world_contract.wasm` file is up-to-date and properly configured.
+And must be used when running the old format configuration but is not required for the new format.
diff --git a/Soroban/hello_world/certora_build.py b/Soroban/hello_world/certora_build.py
new file mode 100755
index 00000000..e41ce045
--- /dev/null
+++ b/Soroban/hello_world/certora_build.py
@@ -0,0 +1,101 @@
+#!/usr/bin/env python3
+import argparse
+import json
+import subprocess
+import tempfile
+import sys
+from pathlib import Path
+
+SCRIPT_DIR = Path(__file__).resolve().parent
+
+# Command to run for compiling the rust project.
+COMMAND = "just build"
+
+# JSON FIELDS
+PROJECT_DIR = SCRIPT_DIR
+SOURCES = ["src/**/*.rs", "Cargo.toml"]
+EXECUTABLES = "target/wasm32-unknown-unknown/release/soroban_hello_world_contract.wasm"
+
+VERBOSE = False
+
+def log(msg):
+    if VERBOSE:
+        print(msg, file=sys.stderr)
+
+def run_command(command, to_stdout=False):
+    """Runs the build command and dumps output to temporary files."""
+    log(f"Running '{command}'")
+    try:
+        if to_stdout:
+            result = subprocess.run(
+                command,
+                shell=True,
+                text=True
+            )
+            return None, None, result.returncode
+        else:
+            with tempfile.NamedTemporaryFile(delete=False, mode='w', prefix="certora_build_", suffix='.stdout') as stdout_file, \
+                tempfile.NamedTemporaryFile(delete=False, mode='w', prefix="certora_build_", suffix='.stderr') as stderr_file:
+                # Compile rust project and redirect stdout and stderr to a temp file
+                result = subprocess.run(
+                    command,
+                    shell=True,
+                    stdout=stdout_file,
+                    stderr=stderr_file,
+                    text=True
+                )
+                return stdout_file.name, stderr_file.name, result.returncode
+    except Exception as e:
+        log(f"Error running command '{command}': {e}")
+        return None, None -1
+
+def write_output(output_data, output_file=None):
+    """Writes the JSON output either to a file or dumps it to the console."""
+    if output_file:
+        with open(output_file, 'w') as f:
+            json.dump(output_data, f, indent=4)
+        log(f"Output written to {output_file}")
+    else:
+        print(json.dumps(output_data, indent=4), file=sys.stdout)
+
+def main():
+    parser = argparse.ArgumentParser(description="Compile rust projects and generate JSON output to be used by Certora Prover.")
+    parser.add_argument("-o", "--output", metavar="FILE", help="Path to output JSON to a file.")
+    parser.add_argument("--json", action="store_true", help="Dump JSON output to the console.")
+    parser.add_argument("-l", "--log", action="store_true", help="Show log outputs from cargo build on standard out.")
+    parser.add_argument("-v", "--verbose", action="store_true", help="Be verbose.")
+
+    args = parser.parse_args()
+    global VERBOSE
+    VERBOSE = args.verbose
+
+    to_stdout = args.log
+
+    # Compile rust project and dump the logs to tmp files
+    stdout_log, stderr_log, return_code = run_command(COMMAND, to_stdout)
+
+    if stdout_log is not None:
+        log(f"Temporary log file located at:\n\t{stdout_log}\nand\n\t{stderr_log}")
+
+    # JSON template
+    output_data = {
+        "project_directory": str(PROJECT_DIR),
+        "sources": SOURCES,
+        "executables": EXECUTABLES,
+        "success": True if return_code == 0 else False,
+        "return_code": return_code,
+        "log" : {"stdout": stdout_log, "stderr": stderr_log}
+    }
+
+    # Handle output based on the provided argument
+    if args.output:
+        write_output(output_data, args.output)
+
+    if args.json:
+        write_output(output_data)
+
+    # Needed for mutations: if you run _this_ script inside another script, you can check this returncode and decide what to do
+    sys.exit(0 if return_code == 0 else 1)
+
+if __name__ == "__main__":
+    main()
diff --git a/Soroban/hello_world/hello_world_new_fromat.conf b/Soroban/hello_world/hello_world_new_fromat.conf
new file mode 100644
index 00000000..f9679dd4
--- /dev/null
+++ b/Soroban/hello_world/hello_world_new_fromat.conf
@@ -0,0 +1,6 @@
+{
+    "build_script": "./certora_build.py",
+    "process": "emv",
+    "optimistic_loop": true,
+    "rule": "hello"
+}
diff --git a/Soroban/hello_world/hello_world_old_format.conf b/Soroban/hello_world/hello_world_old_format.conf
new file mode 100644
index 00000000..b4e3d199
--- /dev/null
+++ b/Soroban/hello_world/hello_world_old_format.conf
@@ -0,0 +1,8 @@
+{
+    "files": [
+        "soroban_hello_world_contract.wasm"
+    ],
+    "process": "emv",
+    "optimistic_loop": true,
+    "rule": "hello"
+}
diff --git a/Soroban/hello_world/justfile b/Soroban/hello_world/justfile
new file mode 100644
index 00000000..18f4f386
--- /dev/null
+++ b/Soroban/hello_world/justfile
@@ -0,0 +1,21 @@
+build:
+    RUSTFLAGS="-C strip=none --emit=llvm-ir -C debuginfo=2" cargo build --target=wasm32-unknown-unknown --release --features certora
+
+wasm2wat :=  "wasm2wat"
+wat2wasm := "wat2wasm"
+
+wat: build
+    {{wasm2wat}} target/wasm32-unknown-unknown/release/soroban_hello_world_contract.wasm --generate-names -o foo.wat
+    {{wat2wasm}} foo.wat --debug-names -o bar.wasm
+    {{wasm2wat}} bar.wasm -o soroban_hello_world_contract.wat
+    rm foo.wat bar.wasm
+
+build-llvm:
+    env RUSTFLAGS="--emit=llvm-ir" cargo build --target=wasm32-unknown-unknown --release
+    @echo "See target/wasm32-unknown-unknown/release/deps/soroban_hello_world_contract.ll"
+
+clean:
+    cargo clean
+
+update:
+    cargo update -p nondet
diff --git a/Soroban/hello_world/soroban_hello_world_contract.wasm b/Soroban/hello_world/soroban_hello_world_contract.wasm
new file mode 100755
index 0000000000000000000000000000000000000000..d7b9a25281b9407d9c8c5b94436ce92e8aa2ad5d
GIT binary patch
literal 29459
zcmcIt37A|(wXS=6wq&wQP9UVR;3Ods2$@Xx>;VIlnMpE`S<EC8L3r)$?%OkMdKr3|
z%wz>cSw#U6Tv!xTL;+EhCvH3!L=m5eiinDe%M%n89?u8z^!=ym-rKjkXHee5d`#V{
zQ&p!<ojP^uoKyEU!pfx#A%rn6@J8c^c%v{5zflNtsS&W#lMOw6J9iE3><(MGoSn^w
zqe29#0)}Z;2Mp0rBLhc_?(@&TPt+d~rO(=6bxq1nWwO(zs2;bI$&4_Jun5czhhtXW
z3ft*ez^D(0$8BpO9I<kCz?{1*Fjq9Z`TX<G7hBBwxuRP%Ab-B7H$}bpkE;1iF*{Ni
z3tN#$)}AyL8EY3Tt`00{IA-~RMF!P?<Srwy0Q9wrz=Hn8o9a)gzt~uq2Bc~+D(dS)
zTo$6b$w)5<Ea3W6r4TjMqJOavwMA(E;>LO*>Z%1d;kr4D(Jjnv!q8N6`cfB3|Kiht
zrhcUnT+9`(uRp7P5BkqrDM|tJ4TF&_ScUOc&+kB!g~tK!=K6YM8#r5EzZuy@RcM!z
zTvYVZI#jIy;fv=Z)87DKC*~r=QL4PyD<8dB;c%w8q{-N(CUT6QQ$j2S`UW3*snE|C
zVp$iu3$a|YPly$Zjg^Z%DpvXi6XMu~m_%Sf3%LFo&0IxlBft#|T;(HGh}8;ZgKtIF
z=s`}CKG<<hqLi`B*0o?-gAm6%Osf{+gmV73*K@;l)eu={mC)ftEJuTXIZopGAZpeZ
z7n*zWQlDInnY-&N#Qj6{j;JNl@yvP?0)*{>)Tr+TTf|Q`tD-o2J!B5qx%e~lEP2bD
zh4?N?MxAk25FM@r5Mo~)N1+=;8gpx&;;kl3Cb{;sRv~T%ZlmrSfTB|!*Uq^^fmFk}
zF8<oz2e{vjjO850q`Fl0s6U&r<8KcBfN|c@DEP{Niuq3<S@3Jlt`G|oouI^MxN9Rs
zzSc|wxB1WtNFg^``WhfH=#oa{=?7e(t9a6M<I$KcJ&kr%^eob9x(jIy-HWuA-iWl0
zGDzppB}nJe)ky2<dZhE{BS`1dA*2iF%O_zM&~->pqd_q1bb39~Zn_ilxP|_Jw1-v$
z(n}kV_E9I&t<-~b8$E{F?NpC^Km8T?GiWLDXVR~b-$4%|9iZERd5~fogg7Fqp2v{j
z*y2-972-NbQk`I)nt_!_nCDfWM1uJq_1EQ~7ECjAgOAms!97Th{sIy-5MoIWXX=c(
z#RXGYAwG!;MuYSiEiOOZf*GNFF8Y`cH6j@WescmWT*^%THE0Brl@6v8=b=D5fx)DI
zK^mYotOz4CpIL%cxdXZ1fndXsHiY?zd>E4w@+lw#S!Oks-TWn}RG1&DQ<!%Hr=T8%
z`AIZ1X#hBtJS|LO^{Wjrg%+h$fBJMG!hklQfuedDkFQ8y#-y7+!NyUeJm;tXCWr?J
z(UdG>N|65)l-KM{PXVV($9^r?bqF0FKLzUOi^!aSzZLtD@V|ztm4`4S6IUfxo(8GR
zakgsZNnoqW)~(#s<usTlj!mMrw-*WiEj$yMTCs35dev6FCV+|5RjsVU<2uv=-O1ps
zMkgAdP+dU(LygdmYWmDycUHGEKNc}7PB<AWV_+KZJCO;I^FWA@g`>a<`8Ph8<lit}
zK>i77m0XU6sFrJ&VZX?W(Y;oVtN|JF5NhXWJddnWc<zQg3;7VR8S*}`$dvc5Wjt>H
zyh=7<5v%2P@U}+Y3Y@jF0d&^M6EFn_&%V_PPlu8b-noY4oomVsn;1_JX_X9tSJko|
zX^k9*#MH`B&{iiiSot|Jk94m58Pa<BE2Q(}0UToU<--_df!qwt3uS*3Rz)@+11`w_
z1U)2w4@NAO4<kKFej4e~dR{q*2KcjrWl!G2(us^%*a$kRtF-QU0drW?0bW)!Q|d^y
zCDoRm2PV`kWBnu+E(OK4bpo?06Q5&G!%6^p;1o1xg{C?zW6VONFt#IYjyk^^%|DBp
zY0PdZo)|$aKN*xkBZ?L0A(_HoL)9vly8Bf3RV;Pi<80L`mO7QKTg6hR8qCw<sy$xC
z9EaLDiq+2Lz@*fU(y=pYq@yR%o|TLyc=?kkF?lOKfCLo0VoH>L8(V}0pNHdV5YsdE
z8c!g*`UTLdj;oY$367$`V<<<sK4n}S!boN_=C<at79lc#nj^-K&}vNt<wLrBPCLps
zqkNez|CGzmgKyXA@=G}P)*Qi5AJ*k_+fY6o<-2wHST4U0<uB`UxC7;%qW^bv`LjU1
zW(vtqbh(l1KZW*B>GE2}KZ5d~x%{;81gKuK7v*ZK4azqt`p}7V`82M-59LN(K8EWb
z#CRKYc@2;E0Q#Sz%P*lUj&p^=J%hi34$My@A=W;D1`FPR(ZxLBoS{BguWoR>YVbY7
zUplJF-}wQ5)!iixZwmP9ZYrs3b?P()H~BG6`3ndAD0&?fy3@G7>is2E_xY=uO9p<I
zAxuyIEo1!$em~TRq^Kd4#uVaSC<<r8IS1nRy8*%ex~m86JuFI#E{)(^{v3{LXo=Wj
zAeA3`Ef_7Y#NILGS7CSs<j;_=l9vKrEq~L%TI+sdt#u~a*U4t2bL3Z`A?C^tAzv@w
zgwf~8Gq9`X3x(fWrSRVm;TDp0tRd$@gPFP(rY4VG2W=qacJwvm*RbHGJOg9}belL7
z5!#%K(S^Jdy7!2@3|sTCyc~MrkZd_lh=aQ24**8Xm7rG0uY+<!o{GFF2apEjxk#%V
zs@C~%ehM5tBI_~YVR`cLd>Sgs*RNJ>&Qz4QBQ-SqJ2)UcdUW3qj^4xa1f+-LXQ3kx
z%3F~hkbA(H{qh;$pO(ji+9~-1aAu$UCelgy4v<?=v&d`Azr)~Vm@BCIlBOzw*$KJg
z7@p%0_-3k;C?FrlC{^;8OL)Dm!HjC;Wk_q~`AF+zH_n<ldaMs=JU?RdT27t9czytl
z<gAMc@<GYZ(H?r5<>Wy>$9@9*M>M=k!~cRA3AuVDbCPh@9F`53^&$Bvq~f4_v7Wi{
zL)7lqy>8L#elw^Q@;R)&A=_{+neq>f-n!qR+nfe$j^yaRLR0?e8iqfhWab6T&Xl`>
zKOlEYkgi+y>z2nV3=bnU<lPw2l>0${Kt_>P$!|lhs%1acu12mvS}PAjqUz)|%qtm$
zG|rV@g$UNm6VQI1Yz1rP%X6`I3uF`0h4OOjhz5BZ(nazGv>~|=lq{CLs69%a0r=7K
zSKz=B`F2oyjQj{FTq>W2L`k^^R4vogezbD+U%(s>%L9s&IZ$;_{urYlP%`6iay`&v
zrM`JA&+c}lro0hpm8`-{>on$HtW$0D4vJuoN94U2{jieHL$Vu?gYw&qS+^h7oIe@+
zR7eA<A&+MrEuU3<yNWq1zciou_F+J3<g-})TDcvwu9H`w<sA7E@^j^l;9<SI6X`s8
zFM7?FEr2hO^FiT4c^6tX$TtB0BKbYgL-I4=&tiE5=~1$O9`o&&nBEe(76-sFau?F2
z^4mzItcAU|Ouie^wOn4m5C^v0i*%)2jPzLf^a8lbatUf1<s7tMB~L-RTHb?njeHvL
z<KzWM*UAgf{&+cr^aS}5daaY+Lwch8FN}MV>;~u8%i}=p$(l3MSP*cVof{$9(ley;
z(UheZP?lbmvh=EzrB|aYy;^1I)hSDFj<WRTDod|kS$gx7r8i$$dJB}L*PtvtZQU)F
zmw|8pQ7eA{0s3vNvi_c`Rp#ICP=ZYSzE*bO5PharCb1&lS*QuURxjb=%^*}m?)D3T
zR$E6w_zufnbUP$hf}scHXR(|IWS>%7aV+Yz?t4HBSv!_Q$V;$1hFqn#+}T)8M@=8D
z#Q!+hcUXznA*BQzHT|UCmO<1C*@e`QPeb@jxxLZD_IXDHL7`A)uA_YC_&0wOreC7A
zT6M2kjuRPxqB-Bua2IGqM??CAyp4&_Q@!T|-(GoDwR=R%&g$Zlbo$5Q)9i@+D74XG
znFYTO$t$pL4$A8>$pbP88Qd>#MSfbY#3D_}rPwk1<mI4zQd9oLO8xO8Ea73fU>;**
z{I34^B9?8xTmp7a%g<vUOlb^HY4)9DGEW*Yio=t2n({w`9z!07VN7`rum$9`NULN4
z)K<&qfwM*?0IAj3*80zF%}J)g6$sWh2bEYjT4z8D+2=4*LvBZE%14n_iAA3Q>K7mh
zrb!K;S<r8wu?%_}$TjJFP!*sjQC&rwA;i`6INH?Ee(<N3dNE=hU5E+Hp$-W8T>2AE
z&U(7xwa`g)A@cL-p3Trn^a%0`=@8%z#0qc`#lZ)nYLK;<*rGX#_CbFfO>8nPq4%Kn
z7~+F+Dg6O?Np}FxGHL*1IsFxo6~yXdC0&3Wd@QZ1hfbm{$Xg>d;@n<Er(rc$(?)FG
zH537D$5At=T}w&eIiCIv^qfF%L4F;bg7idM4$LRf!=P|IwIe;5evNbkZA02bFCyJY
zdyqC$8hwLw4Dumjqo{?R1U;?9E@~UG!`n{mK6lW&F|STK4*IW))*{_RL8PZp2<fTx
zEwq0v4S~+h#K-Yz^eo_~(>Bbao0>3-Ei?`J>7jpL$#J7oS8&{DI>2$Gr-6SP{R)un
z)Q!>mX*K3}20a65Jd?fv+ICRSDI7Q2i1iwz_h9XY=(tTn4AY5SLcETyg#_-Td8i$s
zyTS8aG#~KY^g6T|B{m`U&;g9{dI|u37HtLmY`OsW-$45?>vQNq&~`4d_WBoEg7#rz
zseU8zp=r?)%soQA=o_VLkjAK~MhKf82c9_XM}CZ+GlUqYDi}ZsVgY><+2F}un!+ea
zx*fez)Q^^F`Z(s8p`B<sLFWR)c@zgcOUuzKNA0N1Q!i=@#QxDFU4{HUx(e8)Xb<K%
zO{}x`(;p$p2k0|c!Gpvq;}HE8b3aVy0M8Mc3yz&{(49bifk6)e>zfUl2CBCh^d{(z
z3$ZN#e5*m<#3*kwXaY>X$RG{|Tx`%>0537<3k!s})S%Cy<z)uN(EW0Q(jfZn2C=t!
zg+b4u^bUir!9edch*iRs20emxzsjICbhz4}43NFcpy#m}uQBM?p!MAbwS&Re8uTPu
zUT4rzScdl))CehfuR(tT@O=io6>Ii>gT^5;*BkUx?9&?zV!QT6gPMTlCWBZzf54!d
zz?Tmi^h<1un+<vb!`@<0Cm8V|gVuu+9|lPv@FNCYieYax=(A|@QG-}v-Dc41K;Xv=
z`UuARI7;Be?YJ`lm+vs>tDxmhgI1vXCk#3k^ScXNLft0~`ZAW_QwD849=@|d?*I{>
z22OPU4A=_3++$E3O8;umZ4jZ)8uS>X;a-Ct2a`W%&~K}R_`E>^IKKcEfTS-P^hwlx
z2`h%W`w(-4u>YGur(>1BY|w+K`wDo5Nq^O#%dp+PhWVk%{RVv)bbj5SJ(%qS27Mg@
z_YH$A(D_Y+-UB)xH0bA;=C{xi$R5IM0sOW>o3T;<9Zf*)cMSRih<F%N0kZEJbPljQ
zV$dJgBA8;(y8-+@gb0rxU{&yV)S&l6<NVN|Pow)|2F(GNeq>MrL_BWL-DvV-gRTc#
ze`3%LV8Krf`YyQigh4N!EX2>SsE~=D8?;Rd@e6}ENcJSw4^;ospa($NuOJhs`?WzY
zVA8(<U$DggVbCTl+;0tH=j16Y4hVeOpe1<x&Y*rges53@9?ux`8*u3l2K@w&KN|FT
zJpN?Rqj)?EmRAY!oI&qH%l|a!N<5y2wBqq!;4U72Ht35W;=cg|oi7-4>P8`6G^iGj
zzZi57z?ZN_;OGAs^k%T&uh<>n+20H@fckusPR67!FzG93`DT+&LFp|fodNxPp-C@+
zh_{+_7Y2HpNxQ+wi%hx_d-GzGHeqotG3l`m>_3z41<x)siQSaTO*#N|`gW6Uz~c&&
z-ikoTJ52fu9`7{iBs{J(i9=>rnY0Lxt4;b6TE5Gqvmt!fn3O{4-6p*ek84d@4DMcM
z(oJaj9+Q57$9qk>6OZ?q^fNShze#-BUvJW>0N!9y02}B=llG%@lSyC4;{zsr3oSor
z(ye&hY|?f-ZZT;Y$o&wAz*2qKq;F%IA2I2B;ODI-J%I!Aqb5Cz$89Fv4kA8g5<Ai#
zH|ar?Za3*`%dr1Ux)e?BG>PrJPndKIN_UyG!^HkGX&9q_$|M_)yG^<b!+zSNarFC)
zNzXyp?=k7;81`RHdhZ78KcL3rUX!wTe9oj6wER4ng<-z{mSfm2nsf!W)0a%T0FV2?
z-7f4ulh~U4GL{32^A(e}VR61{QVdPLhG{|=?l);24yv!4^bB^u119|&CjAYQBu4nA
zN#Ci){xj)g0DjA)Utyq!OlpFJeA}dNpzhyIdME0>W74&FJZ#ch5cpk_{u?bHF=-D*
z|DH)njPQMvKCm474|L-3s7ar|<A-1?RM2DK{2c5*lWI@E{xfMBr5{72)^Vtgawz@O
zBopSv6DHMQDnB!6EB5Bkfd#-{Kw1HO66B)$FHMRp!2W~upx>`e>chJK#-wxRV*i=M
z*6(k@36!2PiS5&;P5L2P{>~(}FMn@RJ4(-(#NO&3Fe8-yXc9XYe=><LN}t7z2TISG
zG_Mx>&!lex+4ClG80WtrQfTsLtQea7H%3S41z<tlizZ!-(qAC0sC&tz*Q4}5CM7_`
zUrjQA<!_iYO6Lb?ElL*z=qZ%m9H1;pZwU~4AQuMcIh5WSAQL#>7N9(^Toj-Iw7fV#
zzXiFM1W2NEX@G7)>9PP_f~i~{pgAbLJwP?Uaz%hH1(tUN$U^Cz0s0Y2R|bd!G*<=a
z9JIVTKpgsbSAgzC-8BKaAB=o=fYtzbZGdhD@VWq9gqH6K(2Wp=_Xg-g&=c<q(5<L@
ze}FDW-Sr>>bvFcvgBLdj=!c!ye*s#&3HvWV%kcPMfL1_SZw6{SZVAu@b=ZFa;(LP+
zW9}$@BtY!>+!~-QcziTK99Fw6Ko<tE{{m#=@$mq4L-=kF&{v>z?g-Fj=yzv;egWVo
z0yK`tT>-ils^pUaS`G#ODa--=?gr~n`n2QZF&oPwR60h%(FsHnfcv2GG#s0rO?0&X
z4d6n)4Ki)WVQ6|&4g%uf<ntVDE;^QLPep3VDWpyehnLYCQO7Rs0~-%Zb}pSr9m|{7
zrW%wuu_@M6fZqXu7xG4=h8zP8jt9uw54Ac1_5v&vL!OA#spZoRwJ(7&LY@I#V8|7U
zaz4xgG7PvwA+I=E4q=lS@+Ig&A-@3Hj!2GkAC_^<^pFf=wGPV1AtMLmQefCG|B3;o
zWet{LN)qI1pB%y{lk#ntT|pYakeBx(&B=Nwz^rUVdY-%skO_J1df1wd&*ond&7U_Y
z{^;mv1l%|%+52)<gb!g*`wZkv$VZSmJ|4R*fU^(d1Ps_v0_0YM=YkkC+TVcGke4EL
zxWon%+Pn$$JH2>=0-|G0X^iWv1#2r0uDwByiyoGnYneX}V)%nH3oac{0fYT29yP5Z
zR8x}u*nRR}!Qn}{3ae0%tD$9`s3~veGRz#&I;=1_fd_@>fXtu7oFBw0JAn;0=F#`6
z`5yhO3}(c})E-iJ4$8A3MGimt7({!%i4&524~L)ZZUC;Mmp?`$Ltcp0M`RnTjMyV6
zsZ#P*Enmb2tC3eg9%|)zkc~R|BJewLTGrOU;}4d+29!AbXFXp=?f-|Xe*^y=uJXw<
zBW5jEyTM^6oWm{*T0RP{3OR~(G~^G}O#g&70oe!%tdjGQR%?l6Hx})$VM&t%NF9!`
z;w>BTgGxd;27X9BrzC{q^A6|vU?^*Uu4;c9B*f7S?7*T;0sItlZ*g_l&IEi5cBqh@
zNF5s3Sp)oP=pP5d_9-A?tcy@Fc2lyg8jxRuG*-z6kXFkt0dtLf1Zk~&0O=yh7DAo8
z2>ChkQlxWb{aTKNu4&|0DBH#J<@Mmt0=XZMg_6zZ2Fcd*QIf4nl59;bmRBQxw46Zg
z5_tqP93yW;x>R$LT|&_IpG9g}{{!+&hrmA-w`ZFH5WOG&Py0^4O~59IVUWT@jK?6B
zG?Q2!aD0JI=))&4ESo1Yw&a~2Al~U!#5=v3c%Rk~M}lgJ?@H>3cRD1W@vzz9;o(sX
z;^-L6JWM-493877j*e9mN5^W2qhqzi(Xl$>=-3?M=-6D1jm;Jho2H+~GKr&OIE;b6
zia5GnO&lGop(TxsjiY0TqBA{g>Xc#Nvk!(lMhOs~fG!5cR-=2dz2o(|6Jx;z!QOZI
z#<y1v-`E!NTJjAGB#_5tJII5xhBxS5%ntS=IEG`LIj?w#{l)FsQu5mCnex6ciT4H0
zTyDemlh-DVT4yY_q&&DDi%%1mT0Tvx)apB9v90B`*JJUyY$~b(N<y63u^r~M)R_4k
zH;LOjRIzpDwb9r#hncsSX(Nx$ymdxr`>m`!a|2GvdT!71S*5sCO|1EAh&4Z=lgt6O
z_GawMy#lIN6|tUo#$pSwtUc=`7}wB94*hHwzDyg8I`g&d!l!T!*P0@Q7FGB|>bx!y
z-hvPzj@y61p}}Vqh!EySQ8>XZx%cEBYJ<PQ!ZAOv&TPK%ESxFE{7;^MxZ$-(ux}uc
z04=CK3AMKX#Q(P8&l%9UF5Y}P2MS;X!U;0}hm%{7tp7f+*MfP*%7AgQ!o9MG5kPe<
z2iQc9$1XPJI&bpj^4U|5N788J8l#!4y=hZCmEW|fm)|JeylK;c$-EUw+Tr~4gndYy
zn#*J}5i5<CR42pHOe&R0Z`w3zB{yyA$)qRkY%Y;W_hqx0{|7dkyKma`3b6cr>R&a&
zXF>Fj(|kzur6%&z0_@6Xt!Ta%Z~XQavQ{LKOaR=UPULOWOp6_fNn7W7Z7Zg819skW
zYVFvVo!!ng+3ks39xoI3scs|DiIVcJtd-7T9IQ(TygM4r6w-O!sj|^dJ6A|LwOb0&
zy|$Czp~ls{hT?HM>yA2LO*mOCAl-%hcqW_JZ}G^w#+`CcCYK+!vQ|oicjc2hvm<d{
zArS)?hBFxlgf8*K*od9aC(>h1^K2oP-;qe$<w#>LBxxm5EV5gyq?L|3(2?lKgdNp=
zM(~_uUb@9%-ldV3#Tm~|O=PkbR%F0V^-N5QT~oU<nLaC<L^hGKN0N!C9UCcRC++E7
znTbp?Gp1G-bnl)R%VL2*{+af)7)gw!?JVas6BR5vm;s5L9WF$GiE}-f)I=d~_r*eO
zZNV<U8Mr-VMMuW1P+L2fcG}Slc3WRGma|6e=mfxfgIrO`!!4OuQQG<@?Q~v2h9>N+
zS{qf;<YUn%GU=SHKz-?Gc6uUj$8>XyHi8$^Q`VH&YTH{1sR^IZ^rtbiT~lH>YxBBu
zE|VKVmv}O>PYl{)US7*m5)wO-*l+Jiq+@8%pUz_f!^rL6Kff64N#w_4S!<t2q$e|b
z?J#GddIT2G>DHT=RGZ13%8Ol`Xzo^SjXrKL^KRfO|Av^ksc%nk1K(EQVsSU<-hL@%
zh$~q=8AnhRa3)#h3QzvHpxIj_-5~@u{<(6?%B5lGNFE;<SlLl4S+G@EZ&4pJ)CTbI
z^&~Sn+Xd+r;}U<Iz}?F@Wv5x`kA}EvSIOoCWcJF@;Ow|mRVjZRM5?A|7Owf*lySyi
z<(v0tGZWFD#tD{)^{27zP>3hh#u&DyGbnfC`;2{RUSdmOdN8B2BjBi)&teyAaL>4v
z9<z16JDG)gp6;81u#4V|og2*Lbz#`XX3AU8VyG$V5C-$Qmx0~Ad0xRrbN~4}rXbr?
zx;2@}#JXeHa}c$X4^sqh$sUH|Y=BNoX7U206t$4Eo=|Lq88<&PQOx&X9(miX8Oao~
zQLi*mn6hJTmFD@@OeQ~(O{DYCQhYGkMF7urBEwalXbh_&SLhsTNh@E-+S|FAyJ?i(
z61@p)ERDk>5!K~kwl{KoUV?ULSyr5xG#9aUDSmb*fllQxcV@Y*3R-};8;qJ!E1R&8
zht)H)?$O)LCkPI}x7aSk&nX9nM+p-g@JJ#xk+dB;9oWqK+^H;4i@jiDE|GVt2CTF-
zW-A3WQiw+FT+SWD&JRuS0qg@P;pFpkYtkBX;alvnM0$jkKhEs**wzBC0Fc-?)!a6H
z>Db?Cq3OUbQKXa*$NR+(-D$Hrckt!L6BABrY(>DgW0AKO(#mS_D)@*g*MY)2#=K_E
z?sdva&SIVf!q#vqAOia$R&=jZ9Jcb~&SH$@vxz8J8?|A9In~;FU}<pxj>r$#*)bQy
zXX1#BU5W#}I7lK@uC0o7ih$Xwl_<?pSwSry%?@6@2&_jOK+KMY;>j}Eb_59g>zj(&
zcFd0L$z=ELNTd>;I@ATXx}>T%F@|;n7WQ6tkDVAB$6i;dKFLSM6LHorNPK&w8=uK}
zXOS*=vZ#yO>^!#V>k64{A;oQb*r-xQ5Nw<*09y*MdX@GXDNMjBgLQHi%IK%|KQa&!
zsPg@GOam$e23i8gA(T=~`8U3LuJQLTidwNxS#ytAZqc7g6_lsM1#Pz$?LVkqHa}T_
zcE`$=qL1x%bjanQg@&`4SRq>0qP)^mqeGE5*=RhPfG%+I-LY5}3cx9Cna<m89u~R-
zWq*UUf>RusPDL_Fw*cu+k2!@=JL=?i2Sc4sw!fI&4YSRK7PGtCTV0@+^QovlxD6oM
zJ;>Atkl}rqY%&Ii61;%3BDV8ak(jnF=>y0sY8~Mf-3%L6>{_T}Jcn~!F*E_4zXzXj
z_D!+8<Zv=%b0vVXcKvMa``fvI-H>g}9Q{$t1vXh#q3l?y96D*IM(i;@dHm!1p=Cty
z?yc-m0!<fEVQ?qGC>?V`=Ntj>j?VrVta3O+WA@f;Cgs+SMBN-Vias;InwQgov$iVg
z9=FM^DaQ^~2bv4r0kJGSV6k$3p;tbk4V6;X%m;_(1xcFLu2fE-xYgdL&XpW%0p>(b
zU;{d*9y=t_Od38VpMf4rJO?z_Gf`mHXR+l}i?VensRJ2Wa!R0OJ={~vx6nmUIGjwR
z_l9#2|5@k}BaZj1cQFK?J^zH2#H@6UA5=E>wj?4mXz3B^0!sH!cXo_Ll+Rgr>nM;i
zkGiwb@dT`4@Q_{ZoX@RM_JV8t>w@3N))4gbl)8qLA7L80#fs_7u5qZV@k|odcg&u$
zbK+%95%_(x8X+?*FFbYxMwAldlL-HXntS0wYDgLTeA`Rcdwi^@arwp-N`134>kQ+I
z>%bwetQfGSiolWRjHK{6;af*tbO-I5vZDnSpdD5ktzgQtfj?luUdG>!gbpPoP&G8+
z?w3LYVw7cA*`#-IpoFKub>4(apxdq7NFn03@p)zXY=>m}OzYt!2Z*qNRh$Sl1K9P@
zJ)Zo+C{YdsQ-THGf*@4PZSEBKcyqI^bmT-79t`3z;at8D$%&1-VVmYQX035+a@tB{
z6C0bNR(3425r)ae=(ru-3*RlbF_%FI$l4H{%x~ywX>V`o>WYOTEp|(+!`>JQb=aM)
z)<%txV~8S#^$brS6D?%3!e^cK+PP>pF#!VLX=pDCXQM9m+9@j?bBcYFupO~B{ZL~T
z*JF7cJfc76=2W<l<rVIl7cm89oGNxUZ6#Ig6MS`^`Z2S2FpSCbApN;q!Om(I)yZog
z)hYBq08qb8nUz_ASODe(z|e%k3tz3wARn60T2^4IIyrrayY_w2fm8|@=HSd;h_2N-
zXc)hh0IS;b2AodCvR|V>k!x#uu#k#?RM0$v2aHaRW`w6=SR(s89E5xfSUeRcq@@kt
zU4Za%G5z*=$T)|Rh^8h~EDw*0Sv&2uC&YdUOSjK@gAs)irwZ`^ye9j+Za81rZGe^d
zXm03gXu{_@qTn-$x#V{lQ3mZ0o1)JQkmHviSAyR$;Q=llc)C!kfdPA2or?O>g#}>d
z)$&?;>jg*!3jwS2;sC64#Q?<Vpu8YtXEQ%g<#(-gr%JcVhpha_;i?(kDO6O9%H|B<
znkB5@xe@FN$6o4ZT!@Qi#MyQ>!*Y}n{8JtLD;~;f6}!`W)0ur~Fa}O^+84MC+lYq&
z;#$7ND-@rAY0Cwnj@*QmkB<92;ThQKfJRfUk>Q#NZus4fc{P=>L4P>Zi@QMDk{K(u
z%NiSl7gh9vcqq752==gk6F3#di>9S(w)lho!gVvSRR$8+_i!uR9SV&F^#cn-`60Z=
z1~VzQ<P78m;>2jGcxv(3qp2PXIvys2YvMDsj0Ucr%tYM*oQVIKh&U@P8@HnNsMfw%
zG2EgsJs?4JXAyGl&7>^k9ZI%mQnmvD2gcGO58Em2%9L~9tCa%KDQ-;*XeNysS|X9+
z!US{HZNXj%&s^DE>>QvXp2((nPb5;_R`1Sd9FS6^#iGtx>2xNqdWex}sK%6FyrU`5
z&K}A@Az9SZh<?nl3pt)1=4ez|+)%?JxQi)b@TlS|8nJ~Fc(%%a6wJV_g=7-3|4dS4
zRFsJ!p2IqlLj2Ja3|-RQb)MZ!ontT4fngdB%*(;WbU<#V#CjEd=M}6Zm>+eGf0Ra|
zI6%bimJmPs^<yZDmB%#pdYdvA+v_PMt>bws;cUS%qH;+)JqCbtNpq$hjaqv_7w-ob
zsPAbMWIMtlLY?0Oxv?T2)l$3nT8cgXYb4Ai3u#Cu*-=Q3%}}42@K?J*cW0OJk|;0U
zX8?MkJ)DV{GGo;=2yB8xeA>Bef)>C!M)`_@ua=wuOgn>}cD@^@Y*05>p-8soRiv3O
z{h&DDr&SoFs*R%_Ro*=!t)wbK+r&Vb$~%^V%6p*|RpJ9D%4Vx7`4k;fuoEUj0$!7<
zQ|BODF55k2`qJD_SC$_VGqr&dRBX~-P)|0K%i-vYGlQLIPOlvog&bxKSaB!wQO9;1
z!(s2MSQH!mTyWG>5w<&RPXQZZS*i)Hz+eM#;1!lvjw6XGKL|wz5W<oLn2g9(99&Ms
z5?2lB{B{d1FnvW9)HY{)mq5@0h?|4e*b1m}<VF|x$kVwVrCWOKBz$uAuH6~pIMi|X
zm<MqbrP_qh?Mju~T9Ls8k0qdnK@VS??ohe1ds9r31=JQ>;lDEB-ktUEIC$Xf8+9$E
zNb?RWC9E*CnRm{;f#7!-U=pQc11jTN7LYPwp^_C8_9${}Yr#8FFE_x-@b0<U<8nr2
z$7foVc?flZt4i7mfQzR}-tDcfa}EIxG?W0;y@i6P_4h6;6v*W!p9Q*?y618VDn#nE
zb8Hb^s)!3Xjg;0=`Thy+pt2R#nu4+wqcZ+@i30fT4+W?=WnKG1)p`fKDyc2T$CN6S
zoE;h$Yh<1C31_jZCpx-~x?*?yNmpW24bFBunVGP4Plxx~P3HZsz}m4;i|H8Pyu=PR
zjbF<`36i3P<3r+vb#*5{QCQ9tTtQV)+|?Rk*_CC#ZdFtytUug&%yf<GOwqqLaDzG%
zwAq8=-2$Zra(PyQ#nZ?053p7J`8=P~a2Dd&I6G~=1)a2gpza9VX}p-AK+cXIw9unC
zi(Lg=YO%^hXflf1PL5RY5{RL6a$0R`yfUHyP%gM*VV~0tDXF^@|EAOHB)FxM^@2r1
zh5S%_C*QT|*D9R%FIfA-3UOA|sbX^dr)zm5EqY!bFJv)G_p-y;>&MC=Rz4Q48hj^p
zX<PSRSF66#x^g_OxVx?R)Pt5#dNt+(`CbFc%wvC1c+0GHwrk67*_<FPc3eM)ilM7v
zTo>Z;L^OeM;5w+oh@XD=PCJh94X-EHl&Q3-+<-M5vEj+6H;r)Ysx~=&PrGZz>JlB{
zS_has-bLc@zR!{N0eud&AL@6keQ;z;9Bf}z$!)9}uY{hGOIKB0bi937Dng*Xx|emt
zeeGT*%;{@Y>b6%@cwV}%rb7Sw>MEteSLr*GeNa!|`(U2m=7UxG{=Q1r^74UZGj4oM
zDsN!blK4XfzSim}QVC0|^JZ9S{mb0OD$Fy75PUc)h%VlYC<Mijg0GW0)>XAWp<qzB
z>Qh0TAfT^>bNm$5xq5}HBt}xKb8%@`Im)`a0#v%!9p3m*lpS5#tSjfG=QLGT%ouv%
zu;MT-+HDcbW+uXkba)~Omt63Hf^g<mjtdKYjmUF{Rm_fBDRB1$;t3k4yg_d0hZSG>
zW4E6@Vr3Jl0^XOgd`0h-KvjtdAKrIzvTW+((sp+mL53b!qod8LV#d`L>NOl45f<GT
zvocN{vnMz9jSeVxDq&|g?t(trxDP)2M&C`S7|kSNtWdRa=Nz^=x~szd+RK8O%da7o
zK=@^(5&#?)hVW}lb_@<g3U3a^aFGJDR^RrZ#IOG3y*qXIjU`3x0>s3ax?YE|?SwvJ
zh-e^Wjxz4&gW7LYZ}G6>otnrZ^p85{Jt!yk4FKcT{wNB{{s6>v+>{ULxp*EF>IaLB
zfz&YzdIzi|%#;*knA&P3;MH+PznQ2a+71w?A(3itJKmp;$?(C&_#8h$D<}Z4HP!uu
zdf&l)`2lt!Q|fsop0nWu%QRX1ZfDVthBe^U?m*Os<=wS(`eS7WvbQB;$~VzU8j<<(
zcAmOL4LdP-plk6B*@_Mt6TpMm8r-^UF9QVUFN*o4SU{q_SFHHJPegt1U}zUdg_odB
z(rn!MEI-_Tpu}nMP1OM_%9{?+5%?dtLxQ-d7h;v{@ecFzRO>_qbzS5l!xh+@y((#S
z>AkAxcyC+<k+l4FBzv?)byiw(Ij^8atIK^A&kZX2)?T$Ns&Zd&hIy><@SOvjXppL`
zHG>ZLKi^e3mtcrEckkTUeO7p+|Lnf-uCs>w!eJ#+uSd<ua9>aO^}Rd8TL;4f{e!#8
zK)roE{R7=QM#{juc6JYrZ0*|#aNpo)c%W}rHzO%)wY_i0jv?QwtJ}-LvPN5W?<@z6
z^z90F_kx<TrZd4@O2S)r4h@vGXVf#nN6s49GPI+tanFwKJzKha&J^LZ2ZO<!R;6JC
z_=0U^H}S#N(pd*P#yewOR#&7o*w$=!cG>ZGUj>#n6$K78mvUTF0tBt0SfshND`<7K
zMcO-BG=fm4ONLL`d#}9&ThtALE0b-i4N$drMD14GU3PSKcE*}*Tha1&P<54(r4|mT
z?6&q$w7spRrK7Dm+G@pSomQx{zq=?v5w)ULS9@nyv?~~CjkU~<qO%l*l7Zd3wh!%u
z(DnjRygd@?47G+@;*n6ar9E0nOT|L91jFH;p+Qj7vnzaN-&x^~P)AEgOM7d3q@%sP
zts?}qomQ}`9rMGw#q8#;NF`cl<yvN-k7X1%A{}jA(O_3cbG*Z{+oINNID%z!<o(9o
zyJ8)kai%QT($dz+-AlG*_wew}q0w^aVD~^ds2kgDPxoL?Iebg^4h=1nY-eU=i|1~6
zP!?*lt=5)US1cN{TRS?tfcPIm;qE1%Xl{)(x5Q#mJ09tb1v@$vikFwh4(Em}*ql(F
zC%?uIOl_fHYpm0@>|jeU)NZ#|5>p`nA#B}B0dSYTHDY%}+hXySXji1UEz(wraOS1=
z*bJiD?P!}7Z|{h7b^%jxRvhI^&#DRC<1Jm0SVv2X-PY0E6|!1qB>_C~Yif6cDeVS4
zmfao?LUDv3$-(wcjR$%_y#x_#Eq%os?ISG~_CmBJ)C{vG+NRsLsdpQKEhX<x1iMN*
zt9u?E5vv&w1#w!pwY9ah&Q3X$rJwTdl0DrViMMvNx3x#xBdwjWmRYBdja-66?+Bhq
zTSpiAw|3br&26!+Suq65G@Lq0&>td&jcYYG$GgzGeb)Y=G76k61q>Y)KC@}<vfAxf
zXNzqGXPZO01n~al?x8L#*45b_?6O+pI0I(u9xBs6-r2@DI%AR6mPjnv+8k>OT8yKF
zU8TCTtg^Tu!vA_cY*_U!ZShMZj!ZfRt8VEQD!mrRV#(q?al9xqy)l=KZiG)|Pc=n3
z{GMw{WHvxxJ7S?wBx2#zY!1dZ;sSI73?RItxS_cz)D-Lzg-(GV)#qD2!54h9n?|o}
zAm>osfU|u=DA?4|)FJwZC)>qtTtPve1;3{%`Z*~Ckr|$BWe*0g1$HMV@Wn<U)e0{K
zxj~iV_mtU{Y!!v}R)qr(*s)0Uy&6Lqguie&W#dD)Sc_}hE8A9i6Y8s&7Qczh#_1>^
z&R1fvc-5^3e_%BlDt%WGWhcN<hA^Z(Ccavop~mx2)KDRiSE($0r{#?GN|~x@w}g1w
zNE7(eQ%43jsC<1|#=#&6c38++mxsuE5oSg2XwZvKGLK!@j64a>V1Dz&z+Rv!a{x5Z
zXQ(3%hgLIl(d}KvLeN&`AXPNbqw25Aipw0Vyc5INK4R2*xTAVb3);L&Tg}}8c6xGy
z`Yed|0k+&f13!FweD>=O5DquPAt?FibhLS983%X@b^5x%y*E;?YXe&1$hs!5v&Oha
z(=DJ)aIL@}F>+b0mC9<Ah|)kx@h<Od=v2?#thFUCR-#oYp#b<6)T?$wLw-OXR7y#i
zKWTP=ifZpw4z!wa;#+W!v@a3MkI&YCuMTk+gX)UgSpUersFgDv(94wQNR|)glIT>p
z%;htJX(-zl`u=Lhk<=X!YG%5l@ORKlwKZWUV}5XvVuZj@QMS!hQ?;9B;hg@;88;(I
z_QlbhkE&!M(uCJVPsa<P`t$Xf+^;6v?zAG&wotS!(h=|Ih;4|D6`Gp=8C%G|Mb%ka
zK_E7AShZ@hVV1!Yg(cG54u2;4&!MV#bk0l<>YG}l9bIu4*3DL1duLlK-m86i{`?=`
z#od_7#GKXQcYT{+M|QSG+FGK~SZhm1d*|O9_LbQV*bAjbO6mMj?R;m^6l?A5Xbr|<
zc0AS=vD;c+T{`?4yhOv6(&Gv+%ZF~(WCc6hIv^jdu~=s$ZU<jwy7c|%2E1;oRep0B
zLAst_$8ECksaZ#)xw+MDvm^2Lze~w07ZAsjDJ8)HV))LENHh{^LBz#wk2Jr!jDVfT
zvJz}+Ybs-bu4w}ItzZ;BR4fu|ZEpQ14*#mDq>8l_QM@oe*0^KG=s@E-ey=RrIH})~
zY=m9i)zsX$E*R>Hw?w+S+8aa7q1Fw}?Hhv4C!Q!yit^Vyjq6Ut50ETCULDmr+?`A|
z>)#$xsq_E4^FfYX<Ti##r(oTA?eT*%_?PjJl~h(|b0AFPsnMkA0@Au{4(du*Z`A(4
znzopQa7VPQITGx&TB9M}z%5;^!In<Aym33$)*f$;#iOnG9l@&lCjGzD<F_VW3w%}l
z<COTV7~?Ms=JNx;pMsy@5e7~c{I0M%TDUB#=gbw=CVrm^|1UqIy5R_ZXvHw_!$&}X
zpJkZ=0sr3w{#mv9*JAL)GBb=@Mz{)OLgVU5m^=ym<dq2gUKszt6h5Y=aM7#-&1&Jk
z^4+gL)$p;rB(T9VFhK^$=il22%rmO+|6G|Hpi`?1EXzb(O@=vACGhKIGw`MKBNN7_
z{=MC(O7nXzt5><&cSiGpFY%1QDpB!2hBUO)n;Q{pdnF;9fDx`GLo5vAqZfRt99Eys
zL+A(QOsLO9u`$g$-me9`vSC#1#C8?)P{m(>+p!IiX`@<g;gv7Db;ZdG@xCd(s}0BT
eoj<<&&Y9~MI^VKx7}MXBt*^`B;%$RHmH%HkpQ@Aq

literal 0
HcmV?d00001

diff --git a/Soroban/hello_world/src/lib.rs b/Soroban/hello_world/src/lib.rs
new file mode 100644
index 00000000..e0bc7f67
--- /dev/null
+++ b/Soroban/hello_world/src/lib.rs
@@ -0,0 +1,15 @@
+#![no_std]
+use soroban_sdk::{contract, contractimpl, symbol_short, vec, Env, Symbol, Vec};
+use certora::assert;
+
+#[contract]
+pub struct HelloContract;
+
+#[contractimpl]
+impl HelloContract {
+    pub fn hello(env: Env)  {
+        certora::assert!(false);
+    }
+}
+
+mod test;
diff --git a/Soroban/hello_world/src/test.rs b/Soroban/hello_world/src/test.rs
new file mode 100644
index 00000000..e72c6bb9
--- /dev/null
+++ b/Soroban/hello_world/src/test.rs
@@ -0,0 +1,17 @@
+#![cfg(test)]
+
+use super::*;
+use soroban_sdk::{symbol_short, vec, Env};
+
+#[test]
+fn test() {
+    let env = Env::default();
+    let contract_id = env.register_contract(None, HelloContract);
+    let client = HelloContractClient::new(&env, &contract_id);
+
+    let words = client.hello(&symbol_short!("Dev"));
+    assert_eq!(
+        words,
+        vec![&env, symbol_short!("Hello"), symbol_short!("Dev"),]
+    );
+}

From 52c0e0501d515c2d2bc70d08daffd513f4bd6de3 Mon Sep 17 00:00:00 2001
From: niv vaknin <niv@certora.com>
Date: Sun, 22 Dec 2024 15:36:40 +0200
Subject: [PATCH 2/3] Address comments

---
 Soroban/hello_world/README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Soroban/hello_world/README.md b/Soroban/hello_world/README.md
index f341f43d..72a9010a 100644
--- a/Soroban/hello_world/README.md
+++ b/Soroban/hello_world/README.md
@@ -48,7 +48,7 @@ The new format configuration (`hello_world_new_fromat.conf`) leverages a `build_
 ```
 
 **Key Difference:**
-- **Old Format:** Requires manual specification of the `.wasm` file.
+- **Old Format:** Requires manual compilation and specification of the `.wasm` file.
 - **New Format:** Automatically builds the project using the specified build script.
 
 ---

From 171fef216ad93b1c07394c51ef42bebf9d12dc37 Mon Sep 17 00:00:00 2001
From: niv vaknin <niv@certora.com>
Date: Sun, 22 Dec 2024 16:19:03 +0200
Subject: [PATCH 3/3] Address comments

---
 Soroban/hello_world/README.md | 38 +++++++++++++++++++++++++++++++++++
 1 file changed, 38 insertions(+)

diff --git a/Soroban/hello_world/README.md b/Soroban/hello_world/README.md
index 72a9010a..29cb9418 100644
--- a/Soroban/hello_world/README.md
+++ b/Soroban/hello_world/README.md
@@ -101,3 +101,41 @@ python3 certora_build.py
 
 This ensures the `soroban_hello_world_contract.wasm` file is up-to-date and properly configured.
 And must be used when running the old format configuration but is not required for the new format.
+
+---
+
+## Build Script: Inputs and Outputs
+The build script serves as a bridge between the project and the Certora Prover, handling compilation and providing necessary metadata. It must:
+1. Compile the project
+2. Return a JSON object with project details
+3. Handle build failures appropriately
+
+### Inputs
+- `-o/--output`: Specifies output JSON file path
+- `--json`: Dumps JSON to console
+- `-l/--log`: Shows build logs
+- `-v/--verbose`: Enables verbose mode
+
+### Outputs
+## Case using --json
+
+Print to stdout JSON structure containing:
+```json
+{
+    "project_directory": "<path>",
+    "sources": ["src/**/*.rs", "Cargo.toml"],
+    "executables": "target/.../contract.wasm",
+    "success": true/false,
+    "return_code": 0/or non-zero,
+    "log": {
+        "stdout": "path/to/stdout",
+        "stderr": "path/to/stderr"
+    }
+}
+```
+## Case using --output
+Save JSON structure to file specified by `--output` flag.
+
+## Case not using --json or --output
+return 0 if build was successful, 1 otherwise.
+Note: This case is mandatory for the build script to work properly in Mutation Testing.