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

Track more precisely tuple to tuple assignments in sim #667

Merged
merged 1 commit into from
Dec 13, 2024

Conversation

cassiersg
Copy link
Contributor

Fixes #666

@cassiersg cassiersg marked this pull request as draft December 10, 2024 17:22
@cassiersg
Copy link
Contributor Author

@strub @bgregoir here it is.

@cassiersg
Copy link
Contributor Author

@bgregoir Unfortunately it seems that now that we introduce intermediate variables, sim fails again:

module T = {
  proc test(x: int): int = {
    var l: int;
    (l, x) <- (0, x);
    return l;
  }
}.

equiv t: T.test ~ T.test : true ==> res{1} = res{2}.
proof.
proc.
sim.
qed.

results in

forall &1 &2, true => ={ 0}

(where 0 is the new variable we introduced).

Do you see what's wrong with the code? Or do you have suggestions on how to debug this ?

@bgregoir
Copy link
Contributor

I think the order of the list should be reversed (remember rev) :
(mk_assigns lvs' es) @ (mk_assigns lvs (lvs2expr lvs')) -->
((mk_assigns lvs (lvs2expr lvs') @ (mk_assigns lvs' es))
or
rev ((mk_assigns lvs' es) @ (mk_assigns lvs (lvs2expr lvs')))

@cassiersg
Copy link
Contributor Author

Thanks that was the issue indeed. Now all gimli CT proof work.

@cassiersg
Copy link
Contributor Author

cassiersg commented Dec 11, 2024

Now you can criticize me (constructively) for using the variable name hack.

@bgregoir
Copy link
Contributor

I would love to do that. Unfortunately I don't know how we can propose a nicer solution without an important modification of the code. We need to have the memories of the two current functions to be able to create fresh names properly.

@cassiersg
Copy link
Contributor Author

I'm fine with leaving this as-is, if it is sound.

@bgregoir
Copy link
Contributor

I think we should use this function :
let me, anames = EcMemory.bindall_fresh f.f_sig.fs_anames me in
like in ecPhlInline.ml.
But we need a memenv (in fact 2), we can discuss of this tomorrow.

@cassiersg cassiersg marked this pull request as ready for review December 13, 2024 08:27
@cassiersg
Copy link
Contributor Author

@bgregoir This is now ready.

src/phl/ecPhlEqobs.ml Outdated Show resolved Hide resolved
@bgregoir bgregoir merged commit 22fe124 into EasyCrypt:main Dec 13, 2024
15 checks passed
@cassiersg cassiersg deleted the sim_tuple_assign branch December 13, 2024 10:11
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.

Tuple desctructuring with sim
3 participants