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.

Sign up for GitHub

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

Jump to bottom

Verify mulWad functions correctness #1

Merged
merged 48 commits into from
Oct 10, 2023
Merged

Verify mulWad functions correctness #1

merged 48 commits into from
Oct 10, 2023

Conversation

JuanCoRo
Copy link
Member

This PR verifies the correctness of the mulWad and mulWadUp functions. In particular:

  • Adds the necessary lemmas for the proofs to succeed
  • Increases --smt-timeout for default proof execution to 100000
  • Refines the specs to include all uint256 range of inputs

@JuanCoRo JuanCoRo marked this pull request as ready for review September 26, 2023 17:50
F-WRunTime and others added 24 commits September 26, 2023 21:54
@F-WRunTime
Merge branch 'master' into mulWad-proofs
e999f9a
@F-WRunTime
Re-push to rebuild with CI changes
a113156
@F-WRunTime
Merge branch 'master' into mulWad-proofs
2ff5a86
@F-WRunTime
Update action.yml
cdf27d2
@F-WRunTime
login to pull private image form docker
303be37
@F-WRunTime
Define the ubuntu user
199a501
@F-WRunTime
WRong path
aa4162b
@F-WRunTime
Run direct
20ec144
@F-WRunTime
Check copy directory
05b4ae7
@F-WRunTime
call just the script
850d31e
@F-WRunTime
Remove interactive shell
28d558a
@F-WRunTime
List directory
ad9eea1
@F-WRunTime
Fix user chown
0f88bd4
@F-WRunTime
Change permissions
bfc204f
@F-WRunTime
Wrong workspace
1c847c3
@F-WRunTime
Matching release version used in docker iamge
53a4892
@F-WRunTime
Test env
f00e822
@F-WRunTime
Test env
7a740e7
@F-WRunTime
Test env
d15f2cc
@F-WRunTime
Test env
366fa4b
@F-WRunTime
Test env
1af256a
@F-WRunTime
Transition to use docker images at build time based on a base image w…
6eaea5b 
…/ kup & Foundry installed
@F-WRunTime
mount syntax
e6488b0
@F-WRunTime
Misplanned user permissions post start container
7c63d41
F-WRunTime and others added 19 commits October 5, 2023 10:54
@F-WRunTime
updating dockerfile to force foundry binaries to path
dc8992c
@F-WRunTime
Final clean up of test code
cf55942
@F-WRunTime
Missing v in control version
2c26e45
@F-WRunTime
Go to altest kontrol release, revert docker kup usage to kontrol image
19cd2e8
@F-WRunTime
Wrong image name
02ab5a1
@F-WRunTime
Docker login method update creds
546d04a
@F-WRunTime
Wrong registry
40f433e
@F-WRunTime
missed revert user to 'user'
0e93fd8
@JuanCoRo
Remove tweaks that are now part of Kontrol's default behavior
49e0b50
@F-WRunTime
Adding dockerfile if we need to control z3 install, cleaning docker b…
67328fb 
…uild action
@F-WRunTime
--name > --tag
e02a0ca
@F-WRunTime
Kontrol version does not resolve
e115991
@F-WRunTime
need to set variable name
19f3c4c
@F-WRunTime
Do not build Image
1b65597
@F-WRunTime
Remove dockerfile
ca2291c
@F-WRunTime
Return to kontrol-kup
e234dc3
@F-WRunTime
Revert "Return to kontrol-kup"
c456c41 
This reverts commit e234dc3.
@JuanCoRo
Fix working solc version
e6a2ef0
@JuanCoRo
Replace KevmUtil in favor of KontrolCheats library
e2889c8
@rv-jenkins rv-jenkins merged commit f9bbd54 into master Oct 10, 2023
1 check passed
@rv-jenkins rv-jenkins deleted the mulWad-proofs branch October 10, 2023 17:24
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@F-WRunTime F-WRunTime F-WRunTime approved these changes

Assignees
No one assigned
Labels
automerge
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@JuanCoRo @F-WRunTime @rv-jenkins