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

WIP: allow certain recursive axioms #3507

Draft
wants to merge 2 commits into
base: master
Choose a base branch
from
Draft

WIP: allow certain recursive axioms #3507

wants to merge 2 commits into from

Conversation

ana-pantilie
Copy link
Contributor

@ana-pantilie ana-pantilie commented Feb 17, 2023

Allow axioms of the form:

   rule X <=Int Y => X ==Int Y
      requires Y <=Int X
      [simplification]

Review checklist

The author performs the actions on the checklist. The reviewer evaluates the work and checks the boxes as they are completed.

  • Summary. Write a summary of the changes. Explain what you did to fix the issue, and why you did it. Present the changes in a logical order. Instead of writing a summary in the pull request, you may push a clean Git history.
  • Documentation. Write documentation for new functions. Update documentation for functions that changed, or complete documentation where it is missing.
  • Tests. Write unit tests for every change. Write the unit tests that were missing before the changes. Include any examples from the reported issue as integration tests.
  • Clean up. The changes are already clean. Clean up anything near the changes that you noticed while working. This does not mean only spatially near the changes, but logically near: any code that interacts with the changes!

@ana-pantilie ana-pantilie self-assigned this Feb 17, 2023
@github-actions
Copy link

name diff_allocated_bytes diff_max_live_bytes
test/regression-evm/test-lemmas.sh -0.000031 0.000029
test/regression-evm/test-flipper-addu48u48-fail-rough.sh -0.000002 -0.000007
test/regression-evm/test-storagevar03.sh -0.000002 0.000083
test/regression-evm/test-functional.sh -0.000008 0
test/regression-evm/test-dsvalue-peek-pass-rough.sh -0.000000 -0.000640
test/regression-evm/test-totalSupply.sh 0.000006 -0.000029
test/regression-evm/test-sum-to-n.sh 0.000001 0
test/regression-wasm/test-memory.sh -0.014884 0
test/regression-wasm/test-loops.sh 0.028663 -0.000041
test/regression-wasm/test-simple-arithmetic.sh 0.008559 0.000059
test/regression-wasm/test-locals.sh -0.000016 0
test/regression-wasm/test-wrc20.sh -0.078049 0

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant