Enforcements for "all valid paths" must be shown once, but sometimes still shown for particular paths

[dgpv]

          > > I'm doing the first case, so hiding the impossible things would be good for me right now, but the second case is definitely a real thing too.

I would say that 'always-true' enforcements are not "impossible" things. They might be called "irrelevant" in some narrow context.

If I do (echo 'DUP 12 EQUALVERIFY'; cat varpow) | ./bsst-cli --explicitly-enabled-opcodes=CAT | less then I see:

==============================
Enforced constraints per path:
==============================

All valid paths:
----------------

        EQUAL(12, wit0) @ 2:L1
        GREATERTHANOREQUAL(wit0, 0) @ 6:L3
        LESSTHAN(wit0, 64) @ 10:L4
        CSV(SUB(640, ADD(ADD(ADD(ADD(wit0, wit0), ADD(wit0, wit0)), ADD(ADD(wit0, wit0), ADD(wit0, wit0))), ADD(wit0, wit0)))) @ 23:L12
        EQUAL(1, SIZE(wit1)) @ 63:L22
        LESSTHAN(SUB(wit1.1, 256), 16) @ 123:L35
        EQUAL(32, SIZE(wit5)) @ 132:L41
        EQUAL(64, SIZE(wit6)) @ 136:L42
        EQUAL(wit2.wit1.x('').x('00'), HASH256(wit4.wit6.wit3)) @ 142:L43
        CHECKSIG(wit6, wit5) @ END

IF GREATERTHANOREQUAL(wit0, 32) @ 30:L16 : False
------------------------------------------------

        EQUAL(12, wit0) @ 2:L1
        GREATERTHANOREQUAL(wit0, 0) @ 6:L3
        LESSTHAN(wit0, 64) @ 10:L4
        CSV(SUB(640, ADD(ADD(ADD(ADD(wit0, wit0), ADD(wit0, wit0)), ADD(ADD(wit0, wit0), ADD(wit0, wit0))), ADD(wit0, wit0)))) @ 23:L12
        EQUAL(1, SIZE(wit1)) @ 63:L22
        LESSTHAN(SUB(wit1.1, 256), 16) @ 123:L35
        EQUAL(32, SIZE(wit5)) @ 132:L41
        EQUAL(64, SIZE(wit6)) @ 136:L42
        EQUAL(wit2.wit1.x('').x('00'), HASH256(wit4.wit6.wit3)) @ 142:L43
        CHECKSIG(wit6, wit5) @ END

but that's just telling me the same thing twice, which is confusing -- there's only that one valid path, so everything is all-valid-paths.

I then also see a whole lot of Failures per path: which seems redundant, since they're just different violations of the constraints from the valid paths.

If you do not care about the facts that script might be doing something irrelevant, like checking a condition that is always true, then ignoring them doe not do harm.

Well, bsst isn't really for performance analysis? Like, if I say DUP DROP DUP DROP 2DUP 2DROP DUP DROP, it's not meant to tell me I'm being daft, right?

I think there's an aliasing-ish bug too:

DUP 99 GREATERTHAN IF 1000 ADD ENDIF
50 LESSTHAN IF 10 ELSE 20 ENDIF
CHECKSEQUENCEVERIFY

has the constraints are reported as:

IF LESSTHAN(ADD(1000, wit0), 50) @ 9:L3 : True
----------------------------------------------

        CSV(10) @ 14:L3
        BOOL(10) @ END

IF LESSTHAN(ADD(1000, wit0), 50) @ 9:L3 : False
-----------------------------------------------

        CSV(20) @ 14:L3
        BOOL(20) @ END

but it's only ADD(1000, wit0) conditionally, at other times it's just wit0. Assigning a reference and indicating the reference value is conditional on paths would probably be ideal?

Originally posted by @ajtowns in https://github.com/dgpv/bsst/issues/33#issuecomment-2123698550