Oracle treatment of uninitialised bits#51
Merged
AnoudAlshnakat merged 11 commits intomainfrom Feb 24, 2026
Merged
Conversation
…nd exec sem, typos
…p shortcutting for now
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR contains a way to treat the unspecified bits that result from e.g. out-directed parameters and gets rid of
ARBeverywhere in HOL4P4. Each unspecified bit is modeled here as an indexed call to an oracle function for random bits, e.g. an uninitialised bitvector of length four would be represented as[oracle 1; oracle 2; oracle 3; oracle 4], whereoracleis the random oracle function. The top-level static environment now contains the random oracle function, as well as a getter and setter for the oracle index. The static environment of the expression-level semantics does not contain the getter and setter, but only the oracle index. Additionally, the expression-level semantics may now return an updated oracle index in addition to the new function frame.Having a separate static environment on the expression-level is also desirable since this allows to eliminate some unused components (parser state map, table map), but this is for a later PR.
Organizationally, this PR also puts the metatheory in a separate subdirectory and adds the compilation of this subdirectory to the CI. This allows for quicker iterations when making changes to the base
holdirectory, e.g. to the architectural models.