EasyCrypt / easycrypt

EasyCrypt: Computer-Aided Cryptographic Proofs
MIT License
321 stars 49 forks source link

New feature: "inline" tuple assignments #498

Closed mbbarbosa closed 10 months ago

mbbarbosa commented 11 months ago

Tuple assignments, namely those that result from the inline tactic, can be an obstacle to applying the swap technique, as they bind together potentially unrelated sequences of statements.

The new feature would allow transforming a tuple assignment into a sequence of assignments for the individual components. This could and probably should due to potential impact on the cost logic be restricted to cases where the both the lvalue and the assigned expression are syntactically tuples, i.e., to cases where we have:

(lv1,...,lvn) <- (e1,...,en);

which would be inlined to

lv1 <- e1;
...
lvn <- en