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

return_stt_ghost_noeq #47

Closed
nikswamy opened this issue Jul 28, 2023 · 1 comment
Closed

return_stt_ghost_noeq #47

nikswamy opened this issue Jul 28, 2023 · 1 comment

Comments

@nikswamy
Copy link
Collaborator

@bollu has been writing a data collection script on F* checked files. This uncovered that while we have:

lib/steel/pulse/Pulse.Reflection.Util.fst:let return_stt_ghost_noeq_lid = mk_steel_wrapper_lid "return_stt_ghost_noeq"

and elaborate Pulse terms to actually use this symbol, the symbol doesn't exist in Pulse.Steel.Wrapper.

This would have been caught eventually by a check on the input environment in the DSL checker to make sure that all the symbols needed in the top-level environment are present. But, for now, in the absence of that check, this slipped through.

Thanks Sid!

@nikswamy
Copy link
Collaborator Author

nikswamy commented Aug 8, 2023

Fixed.

@nikswamy nikswamy closed this as completed Aug 8, 2023
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

No branches or pull requests

1 participant