Repository navigation
Insecure core with stall support, src/Core layout, and the 4 KiB cache's functional proof - #24
Merged
Merged
Conversation
A request is now MemFetch addr, MemRead addr size or MemWrite addr size val, so the combinations the core never produces (fetches of other sizes, fetches carrying a value) can no longer be expressed. obsOf maps the constructors one-to-one onto the observations. Co-Authored-By: Claude Opus 5.5 <[email protected]>
The core, register file, memory interface and proofs are now concrete over plain words. PubSec, noSecrets, SecurityViolation, the secret memory map and the --secure-memory mode are gone. The mark_memory_region syscall is kept as a no-op returning 0, so the benchmarks built with SECURE_VAR still run. The leakage model's comment now states what the theorem gives without the secrecy checks. Co-Authored-By: Claude Opus 5.5 <[email protected]>
It writes the given size, one, two or four bytes, not a word. Co-Authored-By: Claude Opus 5.5 <[email protected]>
It is what decode emits when it has no instruction this cycle; the name now says that rather than the cause one stage away. The leakage simulator's StallMemoryBusBusy becomes StallNoInstruction to match. Co-Authored-By: Claude Opus 5.5 <[email protected]>
Every other memory operation (ramRead, ramWrite, MemRead, MemWrite) takes the address before the size; memWrite and the Vec write behind it now do too. Co-Authored-By: Claude Opus 5.5 <[email protected]>
For ecall and ebreak, execute now puts pc + 4 into stateMeRes, which reaches writeback through stateWbRes like any other result; stateHaltNextPc, which skipped the memory stage, is gone. It was a separate field because, with the f parameter, the result registers could hold a secret word. Co-Authored-By: Claude Opus 5.5 <[email protected]>
…f flag All proof modules now live in proof/. The flag still decides whether the solver modules are built: they are listed only under flag(smt-proof), and other-modules is empty so hpack no longer picks up every module in proof/ on its own. Co-Authored-By: Claude Opus 5.5 <[email protected]>
Ideal memory is the specification the core runs against, as the ISA is the specification it computes against; it now lives in src next to the other memory modules, as idealServe, and stepSysOut uses it instead of a local copy. No change in behaviour. Co-Authored-By: Claude Opus 5.5 <[email protected]>
src/ISA.hs, src/Instruction.hs and src/RegFile.hs become Core.ISA, Core.Instruction and Core.RegFile, next to Core itself, as memory's modules sit under Memory. Imports, qualified uses and Haddock references follow. stack test with the solver passes: 155 of 155. Co-Authored-By: Claude Opus 5.5 <[email protected]>
The cache branch's work, squashed onto kristina-insecure-core. The shared code is adapted: Input keeps the ready flag, the core's stall support (stateLoadInFlight, ctrlMeHadInFlight) is concrete over words, idealServe answers with the new MemAccess constructors, and readResp is gone from src/ - ideal memory answers with the whole word, as on main. The cache files themselves (Memory.Cache4K, Memory.Cache4KServer, Proof.Cache.*, Proof.SMT.Cache*, Cache4KSpec, CompositionSpec) are carried over unchanged and are still being rewritten, so the branch does not build yet. The unsquashed history is on kristina-cache-old. Co-Authored-By: Claude Opus 5.5 <[email protected]>
Input is now Input {inputMem :: Maybe Word}: Nothing while memory's answer is
not ready, replacing the separate inputMemReady flag. Decode treats Nothing
like a cycle without a fetch; a load's writeback waits for Just.
Co-Authored-By: Claude Opus 5.5 <[email protected]>
Co-Authored-By: Claude Opus 5.5 <[email protected]>
…helpers Co-Authored-By: Claude Opus 5.5 <[email protected]>
Co-Authored-By: Claude Opus 5.5 <[email protected]>
Co-Authored-By: Claude Opus 5.5 <[email protected]>
Co-Authored-By: Claude Opus 5.5 <[email protected]>
It states a property of the cache that only the proof and the tests use, so it belongs next to srvInvAt rather than in the cache's source. Co-Authored-By: Claude Opus 5.5 <[email protected]>
Whether a load is in flight is already determined by the pipeline: a load is in writeback and its answer has not arrived. Writeback now raises ctrlWbLoadInFlight in that case, and the other stages hold while it is set, so the stall has a single writer and needs no extra state. The invariant's in-flight conjuncts, kLoadInFlight and the test generators' flag go with it. Every stage wrapper and Fresh body is documented. Co-Authored-By: Claude Opus 5.5 <[email protected]>
The field is gone from the core (the resume address now travels in the result registers); remove its last two mentions in the cache files. Co-Authored-By: Claude Opus 5.5 <[email protected]>
…akage The core's functional proof (Machine, Driver, Invariant, Obligation, Induction, and its symbolic state System) now lives in Proof.Core.Functional, and its leakage proof in Proof.Core.Leakage, which builds on it. The cache's array embeddings move next to the cache proof as Proof.Cache.Array and Proof.Cache.Axioms. Proof.Machine is gone: ideal memory comes from Memory.Ideal, running moves into Cache4KSpec, its only user, and the unused readMemWord is dropped. No proof logic changes. Co-Authored-By: Claude Opus 5.5 <[email protected]>
Proof.Cache.Functional.Driver has the cache's driver: a case table giving the cycles after a request until the cache's answer is final, and driverRef, its operational reading, with driverRef == Just (driver + 1) as for the core. Proof.Cache.Functional.Machine has serveN, which serves the request and then that many cycles without one. hop is gone; its uses combine the two. Memory.Cache4KServer exports CacheSrvState so the driver can see a stall. Co-Authored-By: Claude Opus 5.5 <[email protected]>
Link 2 of the chain ISA -> core + ideal memory -> core + cache, in Proof.Cache.Functional: the cached system (Machine), its driver, the invariant relating it to the ideal system (cacheInvAt), and one step obligation per hop length (0, penalty, 2 * penalty). The obligations start from the ideal system and build the cached one with cachedOf, whose cache is coherent by construction: valid lines hold memory's words, invalid lines arbitrary ones. Base case, steps and probes are valid under Bitwuzla, and the steps' premises are satisfiable. The construction needs a new embedding of the data array (Proof.Cache.SMT: DataC, coherentAxioms, RawData), all arrays so that the solver can share it; the cache plumbing moves into Proof.Cache.SMT. The earlier cache-only proof moves to Proof.Cache.Server.Functional, and the core-side composition obligations to Proof.CachedCore; both are still to be reworked or dropped, together with the cache's leakage proof, so the full solver build does not pass yet. Along the way: - serve answers writes and idle cycles with Just 0, and idealServe narrows reads to their size, so that Nothing means only "not ready"; - Input derives Eq; initCacheSrv is the cache server at start; - the core's fields and variables are renamed (sysCore, core/inp/mem), the base cases take the start PC first, indStepObligation is now indStepObligation0, and initSys moves into the tests; - Cache4K names addresses addr and set indices si; - unused imports and redundant brackets are removed. Co-Authored-By: Claude Opus 5.5 <[email protected]>
Proof.CachedCore is dropped: its stall and wait obligations are part of link 2's steps now. Server4K, Induction4K and the cache-only proof under Proof.Cache.Server are taken off the module lists, and Cache4KSpec and CompositionSpec off the test suite's (now explicit) module list; they are still written against the cache's old interface and wait for the cache's leakage proof. Link 2 (Proof.Cache.Functional.Induction) is registered and its results are checked in Spec.hs. stack test with the solver passes: 163 of 163. Co-Authored-By: Claude Opus 5.5 <[email protected]>
Writeback now holds on every Nothing, not only for a load, and with it the whole pipeline: the core keeps its state and makes no request, whichever request memory delays. This is the core's side of a contract with any memory, not just the 4 KiB cache, which delays data reads only. The stall line ctrlWbLoadInFlight becomes ctrlMemNotReady. Ideal memory always answers, so the core's proofs are unchanged in content; stack test with the solver passes: 163 of 163. Co-Authored-By: Claude Opus 5.5 <[email protected]>
The lines only carry values within a cycle; resetting them at its end too means none of them survives it, so a cycle in which the pipeline holds leaves the core's state exactly as it was. The core can then state that it waits for memory as plain equality of states, without a notion of "the same up to control lines". stack test with the solver passes: 163 of 163. Co-Authored-By: Claude Opus 5.5 <[email protected]>
…roof The core and the cache are now to be composed through a contract (the core waits after a request; memory answers Nothing only while a request is outstanding), so the cache's proof is standalone again. Link 2 stays in Proof.Cache.Functional as material to adapt, but off the module lists and out of Spec.hs. CoherentOps and mkDataMem, which the coherent-cache axioms need, move into the standalone proof's Obligation, which is listed again together with its Driver and Invariant; its Induction stays unlisted until its steps are adapted. stack test with the solver passes: 155 of 155. Co-Authored-By: Claude Opus 5.5 <[email protected]>
…ache The cache is proved correct on its own again, against ideal memory with a delay, in Proof.Cache.Functional: its driver, its invariant srvInvAt (ready, memory as ideal memory at a witness byte, coherent at a witness word), and one step per hop length (0, penalty, 2 * penalty) from a ready server whose cache is coherent by construction (CoherentOps, mkDataMem). The earlier cache-only proof under Proof.Cache.Server and the cached system's Machine are gone; the coherent-cache axioms now name mkDataMem from Obligation. Proof.Cache.Functional.Contract states what core and cache promise beyond that, asymmetrically: the core waits after a request (waitsAfterRequest: given no answer, no request and the same state, the register file at a witness), and the cache answers Nothing only while a request is outstanding (readyUnderInv: the invariant implies readiness; readyIdleNoWait: a ready server asked nothing has driver 0). Naming made uniform: the Induction modules are now Solver; a statement is named without "Obligation" (baseCase, indStep0, ...), and the solver property that checks it adds a P (baseCaseP, indStep0P, ...), probes included. The core's invariant used by the proofs is invAt (was invAtFree; the list form is invAtList), and every base case, step and wrapper takes its witnesses first. stack test with the solver passes: 166 of 166. Co-Authored-By: Claude Opus 5.5 <[email protected]>
The flush that isaAt applies gets names of its own: flushedRegFile and flushedMem, the core's register file and memory with the writes still in the pipeline applied. Two new properties in the core's functional proof say that the invariant relating the core to the ISA implies that the ISA's register file and memory are exactly these (regFileUnderInv, memUnderInv, at the witnesses), for any ISA state, not only one derived from the core. stack test with the solver passes: 168 of 168. 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.
This brings the insecure line into
main, so that further cache work can build on it.The core
Accesslayer and its parameterfare gone (agreed 2026-10-21). The secure core stays reachable on the branchsecure-core.MemAccessis a sum type (MemFetch,MemRead,MemWrite);memWritetakes the address first.Maybe Word:Nothingmeans memory has not answered yet.Nothing(ctrlMemNotReady), and the control lines are reset at the end of every cycle as well, so a stall leaves the core's state exactly as it was.src/Core/holdsCore.ISA,Core.Instruction,Core.RegFile; ideal memory, memory's specification, isMemory.Ideal.The proofs
proof/, the solver modules behind thesmt-proofflag; the core's are grouped underProof.Core.FunctionalandProof.Core.Leakage. Solver modules are calledSolver; a statement is named without "Obligation" (baseCase,indStep0, …), and the solver property checking it adds aP.regFileUnderInv,memUnderInv).Proof.Cache.Functional), starting from a cache coherent by construction (mkData, embedded bycoherentAxiomsas all-arrayDataC).Proof.Cache.Functional.Contractstates what core and cache promise each other: the core waits after a request; the cache answersNothingonly while a request is outstanding. All its properties are proved.Not yet
Proof.Cache.Server4K,Proof.Cache.Induction4K,Cache4KSpec,CompositionSpec) is on the old interface and off the module lists until it is redone.stack testwith the solver passes locally: 168 of 168.🤖 Generated with Claude Code