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

Fixes for MInt serialization into the proof trace #1152

Closed
wants to merge 4 commits into from

Conversation

theo25
Copy link
Collaborator

@theo25 theo25 commented Sep 27, 2024

This PR fixes two issues related with the serialization of MInts in the proof trace:

  • We add support for parametric sorts in the KORE rich header generation algorithm, because MInt sorts are indeed parametric. To do that we need to have an invariant of topological sorting of the ordinals of sorts, i.e. every sort needs to have an ordinal greater than the ordinals of all its parameters. We can guarantee that by generating the sort ordinals in this way, since all parametric sorts are known statically at compile time.
  • We fix a bug on how we pass arguments to the emit_*_to_proof_trace functions that emit various events to the proof trace. Previously, when these functions needed to emit a KORE term as part of an event, they would accept a pointer to said KORE term as argument, an in case the term was a boolean or machine integer, that pointer would be cast to the actual value. However for machine integers longer than 64 bits, the pointer data type (which is 64 bit long) is not enough to store the machine integer value. We fix this by passing an actual pointer to the machine integer value in the case where the machine integer is longer than 64 bits.

@rv-jenkins rv-jenkins changed the base branch from master to develop September 27, 2024 20:36
@theo25
Copy link
Collaborator Author

theo25 commented Oct 1, 2024

Closing this because I cannot push to this branch anymore. I have a more up-to-date branch in my fork and I will open a new PR from that.

@theo25 theo25 closed this Oct 1, 2024
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.

1 participant