The ANF process has a big problem, because it is separate from EPP. If A transmits 'v' and B already knows 'v', then this code completely ignores that and does not introduce an assertion that the transmitted value is the same as the value already known. The correct behavior can be implemented manually by programmers, by not sharing names, but it would be more robust if this was done automatically. Unfortunately, the renaming environment in ANF does not track what each party knows, so it can't do this. One strategy would be to change XLRenaming to (Role -> XLVar -> ILArg) and record a separate renaming environment for everyone. This would be quite awkward, especially because the Contract role is really "everyone".
We can get by without this for now, but it is really error-prone.
The ANF process has a big problem, because it is separate from EPP. If A transmits 'v' and B already knows 'v', then this code completely ignores that and does not introduce an assertion that the transmitted value is the same as the value already known. The correct behavior can be implemented manually by programmers, by not sharing names, but it would be more robust if this was done automatically. Unfortunately, the renaming environment in ANF does not track what each party knows, so it can't do this. One strategy would be to change
XLRenamingto(Role -> XLVar -> ILArg)and record a separate renaming environment for everyone. This would be quite awkward, especially because theContractrole is really "everyone".We can get by without this for now, but it is really error-prone.