Possibility to see the counter-example generated by the SMT solver

[acmLL]

I think that it would be interesting to see the counter-example generated by the SMT solver. The "False" is already helpful but a counter-example can help the specifier to improve the annotations. Thanks!

[langfield]

Yes we certainly have talked about this, and I believe it is on our to-do list, haha.

I am definitely not an SMT expert, but we do allow the dumping of queries with the --output-queries flag, and it is possible with e.g. z3 to manually see the satisfying inputs using the get-value function.

As an aside, I don't suppose you'd be interested in becoming a contributor and working on a feature like this with us? We'd be sure to give you as much as help as possible getting you up-to-speed! 😁

[acmLL]

Hey, @langfield . Thank you very much for your promptly reply! I am a professor and not a Dev :-( Probably I will not speed up the development of horus... :-( Best!

P.S.: By the way, what math.cairo lib does horus-compile use? I saw that it has its own math.cairo file...

[langfield]

No worries!

Can you link me to the math.cairo file you're referring to? Or the relevant line?

[acmLL]

I am trying to use horus on this

%lang starknet

from starkware.cairo.common.uint256 import Uint256

from contracts.lib.aliases import ray, ufelt, wad
from contracts.lib.wad_ray import WadRay

// @post -WadRay.BOUND <= $Return.res and $Return.res < WadRay.BOUND
func main_{range_check_ptr}(a, b: felt) -> (res: felt) {
    return (res=WadRay.wmul(a, b));
}

And the cairo program WadRay imports the math.cairo (which is not annotated) using this

from starkware.cairo.common.math import (
    abs_value,
    assert_le,
    assert_nn_le,
    sign,
    signed_div_rem,
    unsigned_div_rem,
)

I do not know if horus is using the above math.cairo or the one located in golden/tou_amm (which is annotated with pre/post) or horus-compile/tests/golden (which is also annotated).

If horus uses the math.cairo from starkware, should I annotate the imported functions? Thanks!

[langfield]

Ah, now I understand. So the horus-compile tools behaves more or less like starknet-compile. It will look for math.cairo in the current working directory if it's imported like from math import assert_le. Otherwise, it will use the version installed with the python package cairo-lang.

So no, it will not use math.cairo from the toy_amm/ directory unless your import is like from math ... and you run it in the toy_amm/ directory.

[acmLL]

Thanks, @langfield . Can I annotate the math.cairo that comes with the distribution (working directory or python package)? I know that horus calculates default pre/post-conditions but...

[langfield]

Best practice would probably be to make a copy of the file, import it from the current working directory, and annotate the copy.

---

From: acmLL @.> Sent: Monday, February 13, 2023 8:56:00 AM To: NethermindEth/horus-checker @.> Cc: langfield @.>; Mention @.> Subject: Re: [NethermindEth/horus-checker] Possibility to see the counter-example generated by the SMT solver (Issue #169)

Thanks, @langfield . Can I annotate the math. cairo that comes with the distribution (working directory or python package)? I know that horus calculates default pre/post-conditions but. . . — Reply to this email directly, view it on GitHub,

Thanks, @langfieldhttps://urldefense.com/v3/__https://github.com/langfield__;!!KGKeukY!33yFkNDSDUV_LBOiM-OaH4OwDdJpgc90GNEChIq02jOzPpqmttQnm28shQk_5hp3y1CyLOKtamOXxoiOY85jpVusJEewEw$ . Can I annotate the math.cairo that comes with the distribution (working directory or python package)? I know that horus calculates default pre/post-conditions but...

— Reply to this email directly, view it on GitHubhttps://urldefense.com/v3/__https://github.com/NethermindEth/horus-checker/issues/169*issuecomment-1427980255__;Iw!!KGKeukY!33yFkNDSDUV_LBOiM-OaH4OwDdJpgc90GNEChIq02jOzPpqmttQnm28shQk_5hp3y1CyLOKtamOXxoiOY85jpVuCuV5JCA$, or unsubscribehttps://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AISQNI44XJ4TF7ZN3OLTFETWXI4PBANCNFSM6AAAAAAUWOMA34__;!!KGKeukY!33yFkNDSDUV_LBOiM-OaH4OwDdJpgc90GNEChIq02jOzPpqmttQnm28shQk_5hp3y1CyLOKtamOXxoiOY85jpVvy1CphOQ$. You are receiving this because you were mentioned.Message ID: @.***>

[acmLL]

Great! Thanks!

[langfield]

If you really wanted the installed version annotated, I'd recommend installing that python package as editable from a local copy of the repository, and editing it there.

---

From: acmLL @.> Sent: Monday, February 13, 2023 8:56:00 AM To: NethermindEth/horus-checker @.> Cc: langfield @.>; Mention @.> Subject: Re: [NethermindEth/horus-checker] Possibility to see the counter-example generated by the SMT solver (Issue #169)

Thanks, @langfield . Can I annotate the math. cairo that comes with the distribution (working directory or python package)? I know that horus calculates default pre/post-conditions but. . . — Reply to this email directly, view it on GitHub,

Thanks, @langfieldhttps://urldefense.com/v3/__https://github.com/langfield__;!!KGKeukY!33yFkNDSDUV_LBOiM-OaH4OwDdJpgc90GNEChIq02jOzPpqmttQnm28shQk_5hp3y1CyLOKtamOXxoiOY85jpVusJEewEw$ . Can I annotate the math.cairo that comes with the distribution (working directory or python package)? I know that horus calculates default pre/post-conditions but...

— Reply to this email directly, view it on GitHubhttps://urldefense.com/v3/__https://github.com/NethermindEth/horus-checker/issues/169*issuecomment-1427980255__;Iw!!KGKeukY!33yFkNDSDUV_LBOiM-OaH4OwDdJpgc90GNEChIq02jOzPpqmttQnm28shQk_5hp3y1CyLOKtamOXxoiOY85jpVuCuV5JCA$, or unsubscribehttps://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AISQNI44XJ4TF7ZN3OLTFETWXI4PBANCNFSM6AAAAAAUWOMA34__;!!KGKeukY!33yFkNDSDUV_LBOiM-OaH4OwDdJpgc90GNEChIq02jOzPpqmttQnm28shQk_5hp3y1CyLOKtamOXxoiOY85jpVvy1CphOQ$. You are receiving this because you were mentioned.Message ID: @.***>

[acmLL]

Ok, @langfield . Thank you very much for your attention! Best!