-
Notifications
You must be signed in to change notification settings - Fork 50
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
[internal] Fix glob unsoundness #440
Conversation
checking and substituting modules.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Hi Cameron,
I have not read the full code but I think the reference f_norm_mod is not reasonable.
I think the good way to do it, is that in EcCoreFol, adding a module in the substitution should
have this type
f_bind_mod : f_subst -> EcIdent.t -> EcPath.mpath * (EcIdent -> form) (* memory to global formula *) -> f_subst
instead of
f_bind_mod : f_subst -> EcIdent.t -> EcPath.mpath -> f_subst
Then in EcFol, you can add a f_bind_mod that is parametrized by an env allowing to
compute the form of the global.
I have used (EcIdent -> form) but it can be any data structure allowing to build the formula once you have the memory, for example the type "use" defined in EcEnv.ml (which can be move).
But this global reference is for sur a big source of bug.
No worries, I've fixed that following your suggestion. |
@bgregoir With Cameron's fix to your comment, are you happy to go? For me, the PR is ok. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thank a lot for all of this.
Have we try to check is the bug is still present?
Our hope is not but just to be sure....
Yes, this should be checked. But we should also check how badly it impacts projects. |
I’ve checked the examples given in the original issue and they no longer work. I haven’t done anything much broader than that though. |
I'll run a check on SHA3. Beyond that, I think someone will need to put some work on #399 to split off the external checks so it can be run only on PRs without losing dependencies on build jobs (so cachix has a chance to do its work instead of getting slammed with parallel builds). It unfortunately cannot be me right now. |
I tried this on all my developments, and everything works. :-) |
This fixes #102 through eager normalization of module globs at typing and instantiation time.