Skip to content

Commit 54a1790

Browse files
palinatolmachpalinatolmach
committed
Add Wonderland demo tests
1 parent c47e437 commit 54a1790

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

70 files changed

+27993
-0
lines changed

‎wonderland/.gitignore

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
# Compiler files
2+
cache/
3+
out/
4+
5+
# Ignores development broadcast logs
6+
!/broadcast
7+
/broadcast/*/31337/
8+
/broadcast/**/dry-run/
9+
10+
# Docs
11+
docs/
12+
13+
# Dotenv file
14+
.env

‎wonderland/KONTROL.md

Lines changed: 54 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,54 @@
1+
2+
## Kontrol
3+
4+
**Kontrol grants developers the ability to perform formal verification without learning a new language or tool.**
5+
6+
## Documentation
7+
8+
https://docs.runtimeverification.com/kontrol/cheatsheets/kontrol-cheatsheet
9+
10+
## Usage
11+
12+
### Build
13+
14+
```shell
15+
$ kontrol build
16+
```
17+
18+
### Test
19+
20+
```shell
21+
$ kontrol prove --match-test 'ContractName.TestName()'
22+
```
23+
24+
### List
25+
26+
```shell
27+
$ kontrol list
28+
```
29+
30+
### Show
31+
32+
```shell
33+
$ kontrol show --match-test 'ContractName.TestName()'
34+
```
35+
36+
### Explore KCFG
37+
38+
```shell
39+
$ kontrol view-kcfg 'ContractName.TestName()'
40+
```
41+
42+
### Clean
43+
44+
```shell
45+
$ kontrol clean
46+
```
47+
48+
49+
### Help
50+
51+
```shell
52+
$ kontrol --help
53+
$ kontrol command --help
54+
```

‎wonderland/README.md

Lines changed: 66 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,66 @@
1+
## Foundry
2+
3+
**Foundry is a blazing fast, portable and modular toolkit for Ethereum application development written in Rust.**
4+
5+
Foundry consists of:
6+
7+
- **Forge**: Ethereum testing framework (like Truffle, Hardhat and DappTools).
8+
- **Cast**: Swiss army knife for interacting with EVM smart contracts, sending transactions and getting chain data.
9+
- **Anvil**: Local Ethereum node, akin to Ganache, Hardhat Network.
10+
- **Chisel**: Fast, utilitarian, and verbose solidity REPL.
11+
12+
## Documentation
13+
14+
https://book.getfoundry.sh/
15+
16+
## Usage
17+
18+
### Build
19+
20+
```shell
21+
$ forge build
22+
```
23+
24+
### Test
25+
26+
```shell
27+
$ forge test
28+
```
29+
30+
### Format
31+
32+
```shell
33+
$ forge fmt
34+
```
35+
36+
### Gas Snapshots
37+
38+
```shell
39+
$ forge snapshot
40+
```
41+
42+
### Anvil
43+
44+
```shell
45+
$ anvil
46+
```
47+
48+
### Deploy
49+
50+
```shell
51+
$ forge script script/Counter.s.sol:CounterScript --rpc-url <your_rpc_url> --private-key <your_private_key>
52+
```
53+
54+
### Cast
55+
56+
```shell
57+
$ cast <subcommand>
58+
```
59+
60+
### Help
61+
62+
```shell
63+
$ forge --help
64+
$ anvil --help
65+
$ cast --help
66+
```

‎wonderland/foundry.toml

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
[profile.default]
2+
src = "src"
3+
out = "out"
4+
libs = ["lib"]
5+
6+
# See more config options https://github.com/foundry-rs/foundry/blob/master/crates/config/README.md#all-options
7+
8+
extra_output = ['storageLayout']

‎wonderland/kontrol.toml

Lines changed: 41 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,41 @@
1+
[build.default]
2+
foundry-project-root = '.'
3+
regen = false
4+
rekompile = false
5+
verbose = false
6+
debug = false
7+
require = 'lemmas.k'
8+
module-import = 'TestBase:KONTROL-LEMMAS'
9+
auxiliary-lemmas = true
10+
11+
[prove.default]
12+
foundry-project-root = '.'
13+
verbose = false
14+
debug = false
15+
max-depth = 25000
16+
reinit = false
17+
cse = false
18+
workers = 4
19+
failure-information = true
20+
counterexample-information = true
21+
minimize-proofs = false
22+
fail-fast = true
23+
smt-timeout = 1000
24+
break-every-step = false
25+
break-on-jumpi = false
26+
break-on-calls = false
27+
break-on-storage = false
28+
break-on-basic-blocks = false
29+
break-on-cheatcodes = false
30+
run-constructor = false
31+
symbolic-immutables = true
32+
33+
[show.default]
34+
foundry-project-root = '.'
35+
verbose = false
36+
debug = false
37+
use-hex-encoding = false
38+
39+
[view-kcfg.default]
40+
foundry-project-root = '.'
41+
use-hex-encoding = false

‎wonderland/lemmas.k

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
requires "foundry.md"
2+
3+
module KONTROL-LEMMAS
4+
5+
// Your lemmas go here
6+
// Not sure what to do next? Try checking the documentation for writing lemmas: https://docs.runtimeverification.com/kontrol/guides/advancing-proofs/kevm-lemmas
7+
8+
imports FOUNDRY
9+
10+
/*
11+
rule bool2Word ( X ) => 1 requires X [simplification]
12+
rule bool2Word ( X ) => 0 requires notBool X [simplification]
13+
*/
14+
endmodule

‎wonderland/lib/forge-std/.gitattributes

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
src/Vm.sol linguist-generated

‎wonderland/lib/forge-std/.github/workflows/ci.yml

Lines changed: 128 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,128 @@
1+
name: CI
2+
3+
on:
4+
workflow_dispatch:
5+
pull_request:
6+
push:
7+
branches:
8+
- master
9+
10+
jobs:
11+
build:
12+
runs-on: ubuntu-latest
13+
steps:
14+
- uses: actions/checkout@v4
15+
16+
- name: Install Foundry
17+
uses: foundry-rs/foundry-toolchain@v1
18+
with:
19+
version: nightly
20+
21+
- name: Print forge version
22+
run: forge --version
23+
24+
# Backwards compatibility checks:
25+
# - the oldest and newest version of each supported minor version
26+
# - versions with specific issues
27+
- name: Check compatibility with latest
28+
if: always()
29+
run: |
30+
output=$(forge build --skip test)
31+
if echo "$output" | grep -q "Warning"; then
32+
echo "$output"
33+
exit 1
34+
fi
35+
36+
- name: Check compatibility with 0.8.0
37+
if: always()
38+
run: |
39+
output=$(forge build --skip test --use solc:0.8.0)
40+
if echo "$output" | grep -q "Warning"; then
41+
echo "$output"
42+
exit 1
43+
fi
44+
45+
- name: Check compatibility with 0.7.6
46+
if: always()
47+
run: |
48+
output=$(forge build --skip test --use solc:0.7.6)
49+
if echo "$output" | grep -q "Warning"; then
50+
echo "$output"
51+
exit 1
52+
fi
53+
54+
- name: Check compatibility with 0.7.0
55+
if: always()
56+
run: |
57+
output=$(forge build --skip test --use solc:0.7.0)
58+
if echo "$output" | grep -q "Warning"; then
59+
echo "$output"
60+
exit 1
61+
fi
62+
63+
- name: Check compatibility with 0.6.12
64+
if: always()
65+
run: |
66+
output=$(forge build --skip test --use solc:0.6.12)
67+
if echo "$output" | grep -q "Warning"; then
68+
echo "$output"
69+
exit 1
70+
fi
71+
72+
- name: Check compatibility with 0.6.2
73+
if: always()
74+
run: |
75+
output=$(forge build --skip test --use solc:0.6.2)
76+
if echo "$output" | grep -q "Warning"; then
77+
echo "$output"
78+
exit 1
79+
fi
80+
81+
# via-ir compilation time checks.
82+
- name: Measure compilation time of Test with 0.8.17 --via-ir
83+
if: always()
84+
run: forge build --skip test --contracts test/compilation/CompilationTest.sol --use solc:0.8.17 --via-ir
85+
86+
- name: Measure compilation time of TestBase with 0.8.17 --via-ir
87+
if: always()
88+
run: forge build --skip test --contracts test/compilation/CompilationTestBase.sol --use solc:0.8.17 --via-ir
89+
90+
- name: Measure compilation time of Script with 0.8.17 --via-ir
91+
if: always()
92+
run: forge build --skip test --contracts test/compilation/CompilationScript.sol --use solc:0.8.17 --via-ir
93+
94+
- name: Measure compilation time of ScriptBase with 0.8.17 --via-ir
95+
if: always()
96+
run: forge build --skip test --contracts test/compilation/CompilationScriptBase.sol --use solc:0.8.17 --via-ir
97+
98+
test:
99+
runs-on: ubuntu-latest
100+
steps:
101+
- uses: actions/checkout@v4
102+
103+
- name: Install Foundry
104+
uses: foundry-rs/foundry-toolchain@v1
105+
with:
106+
version: nightly
107+
108+
- name: Print forge version
109+
run: forge --version
110+
111+
- name: Run tests
112+
run: forge test -vvv
113+
114+
fmt:
115+
runs-on: ubuntu-latest
116+
steps:
117+
- uses: actions/checkout@v4
118+
119+
- name: Install Foundry
120+
uses: foundry-rs/foundry-toolchain@v1
121+
with:
122+
version: nightly
123+
124+
- name: Print forge version
125+
run: forge --version
126+
127+
- name: Check formatting
128+
run: forge fmt --check

‎wonderland/lib/forge-std/.github/workflows/sync.yml

Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
name: Sync Release Branch
2+
3+
on:
4+
release:
5+
types:
6+
- created
7+
8+
jobs:
9+
sync-release-branch:
10+
runs-on: ubuntu-latest
11+
if: startsWith(github.event.release.tag_name, 'v1')
12+
steps:
13+
- name: Check out the repo
14+
uses: actions/checkout@v4
15+
with:
16+
fetch-depth: 0
17+
ref: v1
18+
19+
# The email is derived from the bots user id,
20+
# found here: https://api.github.com/users/github-actions%5Bbot%5D
21+
- name: Configure Git
22+
run: |
23+
git config user.name github-actions[bot]
24+
git config user.email 41898282+github-actions[bot]@users.noreply.github.com
25+
26+
- name: Sync Release Branch
27+
run: |
28+
git fetch --tags
29+
git checkout v1
30+
git reset --hard ${GITHUB_REF}
31+
git push --force

‎wonderland/lib/forge-std/.gitignore

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
cache/
2+
out/
3+
.vscode
4+
.idea

0 commit comments

Comments
 (0)