From e15e89cfa3f0ff4e8359e66e96181536a99c7359 Mon Sep 17 00:00:00 2001 From: autistic-symposium-helper <138340846+autistic-symposium-helper@users.noreply.github.com> Date: Mon, 4 Nov 2024 18:49:58 +0700 Subject: [PATCH] add a bunch of resources on formal verification --- hacking_tools/formal_ verification/README.md | 38 ++++++++++++++++++++ 1 file changed, 38 insertions(+) create mode 100644 hacking_tools/formal_ verification/README.md diff --git a/hacking_tools/formal_ verification/README.md b/hacking_tools/formal_ verification/README.md new file mode 100644 index 0000000..6497181 --- /dev/null +++ b/hacking_tools/formal_ verification/README.md @@ -0,0 +1,38 @@ +## formal verification + +
+ +### tl; dr + +
+ +#### yul + +
+ +* yul (previously also called julia) is an intermediate statically-typed language that can be compiled to bytecode for different backends. +* it's a good target for high-level optimisation stages, as it provides flexibility, speed, and interoperates easily with high-level solidity. +* programs written in yul are readable even if the code is generated by a compiler from solidity. +* because yul needs to be compiled to bytecode, it requires additional time to complete the entire compilation process, making it time-consuming during development. + +
+ +

+ +

+ +
+ +---- + +### external resources + +
+ +* **[lean prover](https://leanprover.github.io/)** +* **[solidity docs on yul](https://docs.soliditylang.org/en/v0.8.18/yul.html)** +* **[evm.codes (evm opcodes, by fork)](https://www.evm.codes/?fork=arrowGlacier)** +* **[solady, optimized solidy snippets](https://github.com/Vectorized/solady)** +* **[the darks arts of yul, by vectorized](https://www.youtube.com/watch?v=ew3pfnb2_V8)** +* **[optimising gas efficient whitelist contract in yul, by 0xmonsoon](https://mirror.xyz/0xCdC75C7d65d5c4cD0329DA74f979C6E1613d57A5/0ZsbpDeEzQhqFNRnsJhhkmPg1oXJCxH0SMkr5EZbaNc)** +* **[ethernaut solutions in yul](https://github.com/teddav/ethernaut-yul/)**