Repository navigation
Cache leakage proof, link 2 restored, and the cache tests - #25
Merged
Merged
Conversation
… lines Output's field is now outputMem, matching Input's inputMem. TagArr and DataArr get Eq through the OPAQUE tagEq and dataEq, so that cache states can be compared whole (the proof replaces both by SMT array equality). The cache server's header and comments describe the cache as it now behaves: a read is answered from the cache after filling each of its lines that misses, and a write is merged byte by byte into the lines that hold its block. Long lines in src/ are wrapped at 80 columns. Part of a series; it builds together with the commits that follow, the last of which is tested. Co-Authored-By: Claude Opus 5.5 <[email protected]>
The driver no longer counts Nop Halted as a bubble while the core has not halted yet (isBubble looks at stateHalt). The leakage simulator gets two pending-halt states, PendingHaltFirstCycle and PendingHaltSecondCycle, so it follows the core through the cycles before a halt, and resets its control lines at the end of every cycle, as the core does. The core's invariant gives its ISA state a name, isaOf (was isaAt in Obligation), with archPc, archRegFile and archMem, and sysInvAt for the invariant at the ISA state the system determines. New properties: the driver and the simulator's driver agree with their operational readings on initial states (driverMatchesSpecInit, simDriverMatchesSpecInit), and the simulator's driver does on every state related to the core by both invariants (simDriverMatchesSpec, which takes the instruction's leakage and assumes sysInvAt). The obligations run hops through helpers (stepSysN, stepSysOutN, simCircuitN), and the leakage steps compare traces of their own Trace type, whose derived equality the solver can unroll. Proof.SMT gets equality on register files and memories (eqRA, eqM) and an embedding of toInteger on Unsigned. Every property of Proof.Core.Functional.Solver and Proof.Core.Leakage.Solver is valid, each module run on its own. Part of a series; see the last commit. Co-Authored-By: Claude Opus 5.5 <[email protected]>
The standalone cache proof moves to Proof.Cache.Server.Functional and gains its leakage half, Proof.Cache.Server.Leakage: an attacker model (the request's observation, and whether the cache answers), a simulator on the tags alone, its driver and the invariant relating it to the server (srvSimInvAt, with simOf, the simulator a server determines). The contract between core and cache is generic in memory: srvReady is defined by behaviour, srvDriverSpec is the operational reading of a memory's driver, and srvReadyIffAnswered, srvReadyUnderInv, srvDriverMatchesSpec and corePatient state what each side promises. Link 2, the core behind the cache refining the core behind ideal memory, is back under Proof.Cache.CachedCore, in a functional half (cachedInvAt, one step per hop length) and a leakage half (a simulator that adds the cycles the core waits, cachedSimInvAt, simCachedOf). Its obligations follow from the contract and the standalone proofs, and are kept as sanity checks. The old Proof.Cache.Server4K and Proof.Cache.Induction4K, superseded by these, are deleted. Every property of the four cache solver modules is valid, each run on its own. Part of a series; see the last commit. Co-Authored-By: Claude Opus 5.5 <[email protected]>
Cache4KSpec now tests the cache alone: reads across two lines, and concrete runs of the server. CacheProofSpec is the cache's counterpart of ProofSpec: the cache's and link 2's obligations and the contract on random states, and end-to-end runs of real programs on the core behind the cache, which check what no single proof states, that link 1 and link 2 compose (the stutter steps, the bus trace from the two simulators, secret-free programs). The helpers of CompositionSpec move there, and CompositionSpec, whose own tests the contract supersedes, is deleted. Both test modules and all proof modules are listed in package.yaml again. The six solver modules, each run on its own, are valid throughout; stack test without the solver passes: 164 of 164. Co-Authored-By: Claude Opus 5.5 <[email protected]>
…f/Memory/Cache4K The core's modules all live in src/Core now, as memory's live in src/Memory: Core, the pipeline, becomes Core.Pipeline. Files that write Core.x import it as Core, so only their import lines change. The ALU and branch semantics (alu, branch and the shift wrappers sllWord, srlWord, sraWord) move out of the pipeline into Core.Alu. The ISA imports them from there and no longer depends on the pipeline. The proofs follow the same layout. The cache's proof moves from Proof/Cache to Proof/Memory/Cache4K, after src/Memory/Cache4K. The SMT embeddings are split: memory's array, toInteger on Unsigned and the base axioms stay shared in Proof/SMT (axioms, memAxioms); the core's register file and shifts move to Proof/Core/SMT, whose arrayAxioms adds them on top. Comment references follow, rewrapped to 80 columns. stack test without the solver passes: 164 of 164; every solver module type-checks with the solver flag. The solver run is in progress. Co-Authored-By: Claude Opus 5.5 <[email protected]>
proof/README.md: what each folder under proof/Proof proves (link 1 under Core, the standalone cache and link 2 under Memory/Cache4K, the shared SMT embeddings), the kinds of module a proof folder is split into, and that only the Solver modules run the solver, one module at a time. 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 #24. Four commits:
outMemtooutputMem, give the cache arrays equality, wrap long lines.Output's field matchesInput'sinputMem.TagArrandDataArrgetEqthrough the OPAQUEtagEq/dataEq, which the proof replaces with SMT array equality. The cache server's comments describe the cache as it now behaves.Nop Haltedcounts as a bubble only while the core hasn't halted.isaOf.Proof.Cache.Server.{Functional,Leakage}is the standalone cache: driver, invariant and steps, plus the attacker model and a simulator on the tags.Proof.Cache.CachedCore.{Functional,Leakage}.Cache4KSpectests the cache alone.CacheProofSpec, the cache's counterpart ofProofSpec, tests the cache's and link 2's obligations on random states and runs real programs end to end, checking that link 1 and link 2 compose.Proof.Cache.Server4K,Proof.Cache.Induction4KandCompositionSpecare deleted.Verification
stack testwithout the solver: 164 of 164.🤖 Generated with Claude Code