Repository navigation
Functional leakage invariants, and case on its own line - #26
Merged
Merged
Conversation
The core's simulator invariant left parts of the simulator open: its control lines, and in its memory stage the whole leak of the instruction, of which the stage only uses whether it loads or stores, at what size and address. The memory stage now keeps just that (SimMemAccess: SimNoAccess, SimLoad, SimStore; the field is simStateMeAccess), and simInv pins it to the core's memory stage and the control lines to simInitCtrl, where every cycle leaves them. The simulator behaves as before. New properties: the three leakage invariants are functional. simInvFunctional (two simulators related to the same system are equal), srvSimInvFunctional and cachedSimInvFunctional (two simulators related to the same server or cached system agree at the witness set). Their solver checks are added to the three leakage Solvers and to Spec.hs. stack test without the solver passes: 164 of 164; the three leakage Solvers type-check. The solver run is still to come. Co-Authored-By: Claude Opus 5.5 <[email protected]>
A definition (or let or where binding) whose body is a case now reads
f x =
case x of
A -> ...
instead of starting the case after the =, as most of the code already did.
Layout only, across src/, proof/ and test/; one-line cases stay as they are.
stack test without the solver passes: 164 of 164; every solver module
type-checks.
Co-Authored-By: Claude Opus 5.5 <[email protected]>
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
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.
Follows #25. Two commits:
SimMemAccess:SimNoAccess,SimLoad size addr,SimStore size addr), the only part of its leak that stage uses. It behaves as before.simInvnow requires the simulator's memory access to be the one the core's memory stage determines, and its control lines to be at rest (simInitCtrl).simInvFunctional(two simulators related to the same system are equal),srvSimInvFunctionalandcachedSimInvFunctional(two simulators related to the same server, or to the same cached system, agree at the witness set). They are checked in the three leakage Solvers and inSpec.hs.src/,proof/andtest/.Verification
stack testwithout the solver: 164 of 164. Every solver module type-checks.🤖 Generated with Claude Code