Skip to content

Commit a2d0dd0

Browse files
ehildenbehildenb
authored
Re enable proofs which were disabled on accident (#431)
* Makefile: correct target names * tests/specs/*: remove whitespace errors
1 parent ac35fce commit a2d0dd0

Some content is hidden

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

52 files changed

+66
-66
lines changed

‎Makefile

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -56,7 +56,7 @@ distclean: clean
5656

5757
clean-submodules: distclean
5858
rm -rf $(DEPS_DIR)/k/make.timestamp $(DEPS_DIR)/metropolis/*.sty \
59-
tests/ethereum-tests/make.timestamp tests/proofs/make.timestamp $(DEPS_DIR)/plugin/make.timestamp \
59+
tests/ethereum-tests/make.timestamp $(DEPS_DIR)/plugin/make.timestamp \
6060
$(DEPS_DIR)/libff/build
6161
cd $(DEPS_DIR)/k && mvn clean --quiet
6262
cd $(DEPS_DIR)/secp256k1 && make distclean || true
@@ -356,8 +356,8 @@ CHECK:=git --no-pager diff --no-index --ignore-all-space
356356
KEVM_MODE:=NORMAL
357357
KEVM_SCHEDULE:=PETERSBURG
358358

359-
test-all: test-all-conformance test-all-proof test-interactive test-parse
360-
test: test-conformance test-proof test-interactive test-parse
359+
test-all: test-all-conformance test-prove test-interactive test-parse
360+
test: test-conformance test-prove test-interactive test-parse
361361

362362
split-tests: tests/ethereum-tests/make.timestamp
363363

@@ -445,10 +445,10 @@ test-bchain: $(quick_bchain_tests:=.run)
445445

446446
# Proof Tests
447447

448-
proof_specs_dir:=tests/specs
449-
proof_tests=$(wildcard $(proof_specs_dir)/*/*-spec.k)
448+
prove_specs_dir:=tests/specs
449+
prove_tests=$(wildcard $(prove_specs_dir)/*/*-spec.k)
450450

451-
test-prove: $(test_prove_specs:=.prove)
451+
test-prove: $(prove_tests:=.prove)
452452
test-klab-prove: $(smoke_tests_prove:=.klab-prove)
453453

454454
# Parse Tests

‎tests/specs/bihu/evm-data-map-concrete.k

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -4,14 +4,14 @@ module EVM-DATA-MAP-CONCRETE [symbolic]
44
imports K-REFLECTION
55
imports EVM-DATA
66
imports EDSL
7-
7+
88
// Same rules exist in KEVM, but are marked [concrete]. Allowing them for symbolic arguments here.
99

1010
rule #lookup( (KEY |-> VAL) M, KEY ) => VAL
1111
rule #lookup( M, KEY ) => 0 requires notBool KEY in_keys(M)
12-
12+
1313
rule #range(WM, START, WIDTH) => #range(WM, START +Int WIDTH -Int 1, WIDTH, .WordStack)
14-
14+
1515
rule WM[ N := W : WS ] => (WM[N <- W])[N +Int 1 := WS]
1616

1717
//semantics of #buf

‎tests/specs/ds-token-erc20/allowance-spec.k

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -101,7 +101,7 @@ _:Map </storage>
101101
andBool 0 <=Int OWNER andBool OWNER <Int (2 ^Int 160)
102102
andBool 0 <=Int SPENDER andBool SPENDER <Int (2 ^Int 160)
103103
andBool 0 <=Int ALLOWANCE andBool ALLOWANCE <Int (2 ^Int 256)
104-
104+
105105

106106
endmodule
107107

‎tests/specs/ds-token-erc20/approve-failure-spec.k

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -102,7 +102,7 @@ _:Map </storage>
102102
andBool 0 <=Int VALUE andBool VALUE <Int (2 ^Int 256)
103103
andBool 0 <=Int STOPPED andBool STOPPED <Int (2 ^Int 256)
104104
andBool STOPPED ==Int 1 <<Int (20 *Int 8)
105-
105+
106106

107107
endmodule
108108

‎tests/specs/ds-token-erc20/approve-success-spec.k

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -107,7 +107,7 @@ andBool 0 <=Int STOPPED andBool STOPPED <Int (2 ^Int 256)
107107
andBool STOPPED ==Int 0
108108
andBool 0 <=Int ORIG_VAL andBool ORIG_VAL <Int (2 ^Int 256)
109109
andBool #hashedLocation("Solidity", 4, .IntList) =/=Int #hashedLocation("Solidity", 2, CALLER_ID SPENDER)
110-
110+
111111

112112
endmodule
113113

‎tests/specs/ds-token-erc20/balanceOf-spec.k

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -100,7 +100,7 @@ _:Map </storage>
100100
andBool 0 <=Int CALL_DEPTH andBool CALL_DEPTH <Int 1024
101101
andBool 0 <=Int OWNER andBool OWNER <Int (2 ^Int 160)
102102
andBool 0 <=Int BAL andBool BAL <Int (2 ^Int 256)
103-
103+
104104

105105
endmodule
106106

‎tests/specs/ds-token-erc20/evm-data-map-concrete.k

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -4,14 +4,14 @@ module EVM-DATA-MAP-CONCRETE [symbolic]
44
imports K-REFLECTION
55
imports EVM-DATA
66
imports EDSL
7-
7+
88
// Same rules exist in KEVM, but are marked [concrete]. Allowing them for symbolic arguments here.
99

1010
rule #lookup( (KEY |-> VAL) M, KEY ) => VAL
1111
rule #lookup( M, KEY ) => 0 requires notBool KEY in_keys(M)
12-
12+
1313
rule #range(WM, START, WIDTH) => #range(WM, START +Int WIDTH -Int 1, WIDTH, .WordStack)
14-
14+
1515
rule WM[ N := W : WS ] => (WM[N <- W])[N +Int 1 := WS]
1616

1717
//semantics of #buf

‎tests/specs/ds-token-erc20/totalSupply-spec.k

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -99,7 +99,7 @@ _:Map </storage>
9999
andBool 0 <=Int ORIGIN_ID andBool ORIGIN_ID <Int (2 ^Int 160)
100100
andBool 0 <=Int CALL_DEPTH andBool CALL_DEPTH <Int 1024
101101
andBool 0 <=Int TOTAL andBool TOTAL <Int (2 ^Int 256)
102-
102+
103103

104104
endmodule
105105

‎tests/specs/ds-token-erc20/transfer-failure-1-a-spec.k

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -113,7 +113,7 @@ andBool #hashedLocation("Solidity", 1, CALLER_ID) =/=Int #hashedLocation("Solidi
113113
andBool #hashedLocation("Solidity", 4, .IntList) =/=Int #hashedLocation("Solidity", 1, TO_ID)
114114
andBool #hashedLocation("Solidity", 4, .IntList) =/=Int #hashedLocation("Solidity", 1, CALLER_ID)
115115
andBool VALUE >Int BAL_FROM
116-
116+
117117

118118
endmodule
119119

‎tests/specs/ds-token-erc20/transfer-failure-1-b-spec.k

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -113,7 +113,7 @@ andBool #hashedLocation("Solidity", 1, CALLER_ID) =/=Int #hashedLocation("Solidi
113113
andBool #hashedLocation("Solidity", 4, .IntList) =/=Int #hashedLocation("Solidity", 1, TO_ID)
114114
andBool #hashedLocation("Solidity", 4, .IntList) =/=Int #hashedLocation("Solidity", 1, CALLER_ID)
115115
andBool BAL_TO +Int VALUE >=Int (2 ^Int 256)
116-
116+
117117

118118
endmodule
119119

0 commit comments

Comments
 (0)