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

Add ability to set assertions for values on the stack and assumptions for data placeholders #18

Merged
merged 1 commit into from
Nov 15, 2023

Conversation

dgpv
Copy link
Owner

@dgpv dgpv commented Nov 4, 2023

No description provided.

@dgpv
Copy link
Owner Author

dgpv commented Nov 4, 2023

Should fix #15

@dgpv
Copy link
Owner Author

dgpv commented Nov 4, 2023

This is incomplete because no automatic tests are added yet. For now it just passes a few manual tests I've done, and seems to work.

It might take a while until I find time to work on automatic tests, and meanwhile this might be interesting to those who wish to experiment with these assertions, so I'm putting this PR to public.

@ajtowns you might want to check this out - IIRC you mentioned that something like this could be useful to you.

I would appreciate any comments regarding the usefulness of this limited form of assertions and the ergonomics of their usage.

Later, #14 can be resolved by using assertions to place constraints on args of PICK or ROLL and when these args are analyzed, just generate their possible values repeatedly until certain specified limit. Afterwards, use the generated values to create separate execution paths.

@dgpv
Copy link
Owner Author

dgpv commented Nov 4, 2023

The format for the assertions is described in the updated README.md

README.md Outdated Show resolved Hide resolved
@dgpv dgpv changed the title Add ability to set assertions for values on the stack Add ability to set assertions for values on the stack and assumptions for data placeholders Nov 7, 2023
@dgpv
Copy link
Owner Author

dgpv commented Nov 7, 2023

Added distinction between assumptions and assertions

// bsst-assume($name): ... and // bsst-assume-size($name): ... set assumed constraints on data placeholder $name.

The README section about assertions and assumptions is updated accordingly.

No tests still.

@dgpv dgpv force-pushed the value-assertions branch 2 times, most recently from 1af33b1 to 20beb06 Compare November 10, 2023 13:21
@dgpv
Copy link
Owner Author

dgpv commented Nov 10, 2023

Rebased on main, squashed.

Started adding tests.

@dgpv
Copy link
Owner Author

dgpv commented Nov 13, 2023

It seems to be relatively easy to add an ability to use data placeholders and data references within assertions (like, // bsst-assert: >=&someref <$somedata). But I hesitate to add this, as I fear feature creep. Data placeholders or references with only comparison and without full-blown arithmetic on them seems not very useful, but I did not want to add expression parser, I want to avoid code bloat and any external dependencies. I expect that complex assertions can be dealt with via analysis plugins (#19) if these are implemented.

Still, if someone can show how assertions that use data placeholders/references without any arithmetic on them might be practically useful enough to have them available in the "simplified assertions", I might consider adding this feature

@dgpv
Copy link
Owner Author

dgpv commented Nov 13, 2023

By the way, using data references with asserts might be useful in another way, to refer to previous values on the stack, like this:

         // bsst-assume($a): le64(20) le64(21)
        $a DUP
        le64(1) ADD64 VERIFY le64(3) DIV64 VERIFY
        SWAP // =>remainder
        le64(0) EQUAL VERIFY
        // bsst-assert(&remainder): le64(0)
        // bsst-assert-size(&remainder): 8
        // bsst-assert: le64(7)
        DROP

Since it has obvious practical value, I have added this feature (// bsst-assert(&ref): / // bsst-assert-size(&ref):)

@dgpv
Copy link
Owner Author

dgpv commented Nov 14, 2023

Added tests.

Values on top of the stack can be constrained with assertions
Data placeholders can be constrained with assumptions
@dgpv
Copy link
Owner Author

dgpv commented Nov 14, 2023

Added ability to apply assertions to witnesses: // bsst-assert(wit0): >3, // bsst-assert-size(wit1): 64 65 etc.

Can be used to ensure that restrictions that the script put on its witnesses are as expected

@dgpv dgpv merged commit 0b6506b into main Nov 15, 2023
@dgpv dgpv deleted the value-assertions branch November 15, 2023 12:18
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.

2 participants