Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

wow let's formally verify the solc optimizer #47

Open
wants to merge 110 commits into
base: master
Choose a base branch
from
Open
Changes from 1 commit
Commits
Show all changes
110 commits
Select commit Hold shift + click to select a range
6ce35e6
end.cage-deficit typo
rainbreak Jul 12, 2019
3b42add
end.cage remove lemmas
rainbreak Jul 12, 2019
97c8efb
end.cage timeouts
rainbreak Jul 12, 2019
f1a3441
end.cage: add lemmas and preconditions
rainbreak Jul 12, 2019
06accab
end.cage: missing vars and ranges
rainbreak Jul 12, 2019
8e7d7f1
end.cage: vow.vat == end.vat
rainbreak Jul 12, 2019
0f47c81
add fail gas estimation for drip of {Jug, Pot}
mhhf Jul 12, 2019
991f8ce
lemmas; how I think they should be
MrChico Jul 10, 2019
2e53ba7
flush some dirty lemmas to resources.k
MrChico Jul 11, 2019
22a5773
end.cage: vow=/=vat in all cases
rainbreak Jul 12, 2019
ab36b19
big timeouts for remaining proofs
rainbreak Jul 12, 2019
dcc76b4
end.skip: missing vat,ilk matching
rainbreak Jul 12, 2019
1d0774d
frob-same typos
rainbreak Jul 12, 2019
1cb538c
bite: vat,ilk matching assumption
rainbreak Jul 12, 2019
aeff513
update to new dapp build output
rainbreak Jul 12, 2019
0be1b17
rename posMinSInt256 to pow255
rainbreak Jul 12, 2019
8795adf
whitespace
rainbreak Jul 13, 2019
863712b
subuu, adduu lemmas
MrChico Jul 13, 2019
599d200
frob-same long timeout
rainbreak Jul 13, 2019
0b51f25
dirty_lemmas: lemma for SDIV with negative second arg
MrChico Jul 13, 2019
aeb869e
end.cage: incorrect lemma name, iff
rainbreak Jul 14, 2019
bbcb3f4
lemmas: remove bad SDIV lemma
MrChico Jul 14, 2019
21b00c5
vat.frob-diff, flapper.tend extra long timeouts
rainbreak Jul 14, 2019
0db94b3
dss.md: try to fix End.skip spec
livnev Jul 14, 2019
fc0e1c4
fix drip fail gas
mhhf Jul 15, 2019
50f1b41
rules.k: SDIV with positive second argument lemma
MrChico Jul 15, 2019
2c676dc
config: increased memory for hard proofs
rainbreak Jul 15, 2019
339f725
dss.md/End.skip: add Rate_i condition for mului
livnev Jul 15, 2019
07542b1
timeouts: bite
rainbreak Jul 15, 2019
573c272
bite: grab preconditions
rainbreak Jul 15, 2019
74762ad
bite: constrain cat gem balance
rainbreak Jul 16, 2019
205ae90
bite: kick preconditions
rainbreak Jul 16, 2019
0171539
timeouts: skip
rainbreak Jul 16, 2019
34eada9
DSToken.transferFrom: don't assume src =/= CALLER_ID
MrChico Jul 17, 2019
8b5df14
correct a -Word lemma and add a -Word lemma
MrChico Jul 17, 2019
6aad5b2
add some dirty lemas which might solve some stuff
mhhf Jul 17, 2019
4d70b6b
adapt lemmas to new arith. normalform
mhhf Jul 19, 2019
edba713
dirty_lemmas: simplify 0 <= X >= 0 to X == 0
MrChico Jul 19, 2019
e897a75
change martin rules to solve constrains on the z3 level
mhhf Jul 20, 2019
b6def59
fix drip lemma
mhhf Jul 20, 2019
1d4b4cc
update some dirty lemmas, i totally screwed up once
mhhf Jul 21, 2019
afe4d77
fix codependend stuff in drip of Jug
mhhf Jul 21, 2019
6bb5a88
inRangeSInt( 0 -Int X) if X <= pow255
MrChico Jul 21, 2019
6bdadf2
dss: End.skim: switch position of Art_iu and Rate
MrChico Jul 21, 2019
b106396
add rule for drip of Jug
mhhf Jul 21, 2019
771f582
remove redundant rule
mhhf Jul 21, 2019
750850f
oops
mhhf Jul 21, 2019
b858c5b
Remove bad rule in dirty lemmaS
MrChico Jul 22, 2019
0c60237
adapt some 0 - X lemmas
mhhf Jul 22, 2019
0115eb2
Flipper is not Vat in skip
mhhf Jul 22, 2019
02ee7a9
support reasoning about A == 0 from z3 to k
mhhf Jul 22, 2019
77de191
jug.drip: remove redundant iff, add fold lemma
rainbreak Jul 24, 2019
452c02c
end.skim,bail: redundant iff conditions
rainbreak Jul 24, 2019
863ff49
long timeouts/memory for cat.bite,end.cage
rainbreak Jul 24, 2019
42129cd
desperatelly try to make skip of End work
mhhf Jul 23, 2019
9d85dee
fix drip of jug pass gas
mhhf Jul 24, 2019
61a071e
Cat_bite-full_pass improvement
mhhf Jul 25, 2019
f6729b5
End_cage*_fail_rough gas lemmas to speed up gas lemma speedup
mhhf Jul 26, 2019
d31c425
do stuff
mhhf Jul 26, 2019
2717a9b
cat.bite: correct min branching, int ranges
rainbreak Jul 26, 2019
f374109
fuck you gas expressions, i'll do it the dirty way
mhhf Jul 27, 2019
00b07d9
typo in bite-full of Cat
mhhf Jul 27, 2019
ee00c86
cat.bite-full typo
rainbreak Jul 27, 2019
a8935a0
cat bite-lump should be run as well
mhhf Jul 27, 2019
0728449
fix typo in skip of End
mhhf Jul 28, 2019
22566e6
increase timeout for cat_bite pass
mhhf Jul 28, 2019
008d6b8
Add lemmas for Vat_fork-same_fail and extend gas reach simplification
mhhf Jul 29, 2019
a670da5
redo Cat_bite-lump_pass due to gas
mhhf Jul 29, 2019
b577571
give End_skip_pass room to breathe
mhhf Jul 29, 2019
2b554b9
dafuq are you doing End_skip_fail_rough?
mhhf Jul 29, 2019
e4e8c80
Cat_bite-full_fail_rough dirty lemmas
mhhf Jul 29, 2019
4149528
Cat_bite-lump_fail - biggest spec ever
mhhf Jul 29, 2019
762686a
vat.frob: remove redundant condition
rainbreak Jul 29, 2019
56f8d4d
vat.frob: split specs on dink,dart!=0
rainbreak Jul 29, 2019
5193ac0
vat.frob-diff distinct names
rainbreak Jul 29, 2019
fe041cd
fork-same longer timeout
rainbreak Jul 29, 2019
cf74079
dss: bump to fixed frob
MrChico Jul 30, 2019
88e8f47
dss: bump to include external functions
rainbreak Jul 30, 2019
944bfd5
bump dss for real
rainbreak Jul 30, 2019
3795ee5
dirty_lemmas: correct sgninterp lemma range
MrChico Aug 1, 2019
86ded61
split frob-same on dart==0
rainbreak Aug 2, 2019
a8df014
bump dss
rainbreak Aug 3, 2019
2f62c18
rate != 0 for initialised ilks
rainbreak Aug 3, 2019
9c8778e
specialise skip to nonzero tab / rate
rainbreak Aug 3, 2019
f64dd21
Revert "bump dss"
rainbreak Aug 3, 2019
b36edfb
bump dss
rainbreak Aug 3, 2019
a735b8f
remove unused vars
rainbreak Aug 3, 2019
088acdf
further specialise frob-same
rainbreak Aug 3, 2019
27a0244
timeouts
rainbreak Aug 3, 2019
4214b3a
match frob-diff and frob-same layout
rainbreak Aug 3, 2019
c50c35e
remove excess conditions
rainbreak Aug 3, 2019
d80732c
longer timeouts
rainbreak Aug 3, 2019
f133147
skim,bail: remove redundant conditions
rainbreak Aug 4, 2019
7ce177c
more memory for skim,bail
rainbreak Aug 4, 2019
c50d8ca
skip: remove redundant conditions
rainbreak Aug 4, 2019
19799d5
skip: remove redundant condition
rainbreak Aug 4, 2019
afd7dac
lemma for skim, bail rate * -art
rainbreak Aug 6, 2019
0cd07e8
Revert "skip: remove redundant condition"
rainbreak Aug 6, 2019
0942633
timeouts
rainbreak Aug 6, 2019
2742a8b
another skim lemma
rainbreak Aug 6, 2019
13783ab
be explicit with skim,bail term
rainbreak Aug 6, 2019
7414be6
skim lemma matching
rainbreak Aug 7, 2019
e0f379c
frob zero-dink
rainbreak Aug 7, 2019
769908d
explicit lemma for skim,bail
rainbreak Aug 7, 2019
413de94
fix bite-full of Cat lemma dirty, hope this will work
mhhf Aug 13, 2019
939c16e
bite: use explicit int range
rainbreak Aug 14, 2019
dcdf34c
bite: force lemma application with no preconditions
rainbreak Aug 14, 2019
009b4fe
remove unrestricted lemma
mhhf Aug 15, 2019
d8040c0
Makefile: enable solc optimizer when building
livnev Aug 21, 2019
61bfbbc
flush dirty_lemmas.k.md
livnev Aug 23, 2019
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
config: increased memory for hard proofs
  • Loading branch information
rainbreak committed Jul 15, 2019

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
commit 2c676dc884080de07796b3dc671c29ec63e144a5
5 changes: 5 additions & 0 deletions config.json
Original file line number Diff line number Diff line change
@@ -92,6 +92,11 @@
"End_cage-deficit_fail_rough": "16h",
"End_cage-balance_fail_rough": "16h"
},
"memory" : {
"Vat_frob-diff_fail_rough": "20G",
"Vat_frob-same_fail_rough": "20G",
"Flapper_tend_fail_rough": "20G"
},
"dapp_root": "./dss",
"host": "127.0.0.1:8080"
}