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

[PV] Ambiguous field access #1347

Open
jschneider-bensch opened this issue Mar 10, 2025 · 0 comments · May be fixed by #1360
Open

[PV] Ambiguous field access #1347

jschneider-bensch opened this issue Mar 10, 2025 · 0 comments · May be fixed by #1360
Assignees
Labels
bug Something isn't working proverif ProVerif backend

Comments

@jschneider-bensch
Copy link
Contributor

jschneider-bensch commented Mar 10, 2025

If we have the following Rust items, the PV backend will generate ambiguous accessors for them

struct Foo(Vec<u8>);
struct Bar(Vec<u8>);

fn qux(a: Foo, b: Bar) -> bool{
    a.0 == b.0
}

The generated PV shows that the backend generates the same destructor accessor_mwe__0 for both types, which is not supported by ProVerif.

type mwe__t_Foo.

[...]
fun mwe__Foo(bitstring)
    : mwe__t_Foo [data].
reduc forall mwe__0: bitstring;
    accessor_mwe__0(mwe__Foo(mwe__0)) = mwe__0.

type mwe__t_Bar.

[...]
fun mwe__Bar(bitstring)
    : mwe__t_Bar [data].
reduc forall mwe__0: bitstring;
    accessor_mwe__0(mwe__Bar(mwe__0)) = mwe__0.


letfun mwe__qux(a : mwe__t_Foo, b : mwe__t_Bar) =
       core__cmp__f_eq(accessor_mwe__0(a), accessor_mwe__0(b)).

@jschneider-bensch jschneider-bensch added bug Something isn't working proverif ProVerif backend labels Mar 10, 2025
@jschneider-bensch jschneider-bensch self-assigned this Mar 10, 2025
@jschneider-bensch jschneider-bensch linked a pull request Mar 13, 2025 that will close this issue
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working proverif ProVerif backend
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant