Between Rocq & A Hard Case

Every developer wants their code to be memory safe, the threads and processes to never deadlock, and for no buffer to underflow. Our design aims to make supported checks routine in concurrent Clef, with as little annotation and handwritten proof as possible. The language, the Program Semantic Graph (PSG), and the elaboration and saturation pipeline that builds it provide the setting; the proof layer that reads obligations off that graph and discharges them is upcoming work in the compiler scaffold. Clef Compiler Services (CCS) is intended to establish facts during development and carry their justification through Composer’s lowering pipeline. Relational and probabilistic proofs extend that ambition to specialist domains. The proof generation, semantic bridges, and artifact checks described below are design requirements, not a report of a delivered end-to-end cryptographic verifier. The code and proof blocks illustrate the proposed surface.

The scenario is specific: an engineer implementing a signature scheme needs an unforgeability argument, while an engineer implementing encryption may need a confidentiality argument. EUF-CMA concerns forging a signature after chosen-message signing queries; IND-CCA2 concerns distinguishing encryptions despite the permitted adaptive decryption queries. Neither is a synonym for a signing routine leaking nothing. Side-channel resistance is a further claim about observations such as timing, branches, and memory accesses under a stated machine model. Safety-critical control raises its own functional, timing, and assurance obligations; no single relational theorem decides certification. What follows is how we intend Composer to help connect these different obligations without making the specialist start every proof from scratch.

The everyday goal is to make dimensional, memory, and supported deadlock checks part of ordinary concurrent Clef. The same CCS machinery should serve specialist proofs by retaining the structural facts they consume. This is an automation strategy: a range or ownership fact can supply a premise, but it does not itself establish a security game, a probability model, or a termination theorem.

A security argument for an abstract signature scheme leaves a separate obligation: connecting that scheme to the implementation and the binary that eventually runs. A compiler transformation can also affect an implementation’s leakage behavior, for example by turning a select into a conditional jump or introducing a secret-indexed access. Functional preservation and preservation of an observation model therefore need their own accounts. The guarantee we want is the one that holds for the code that runs, under the assumptions actually checked.

The Symbolic Software analysis of the hax pipeline illustrates why verification scope and translation assumptions deserve scrutiny. Its reported cases distinguish missing modeled behavior, admitted assumptions, and properties outside a proof’s scope; its rejection-loop examples did not pass full verification. That is not evidence that F* cannot express probabilistic security, or that retaining a graph automatically prevents the same gaps. The engineering lesson applies to our own design: state the property, check its premises, and establish correspondence between the modeled computation and the deployed artifact. Our earlier discussions, The Dangers of Unearned Press and Case Studies in Consequence, should be read with that same standard.

Maintaining the Chain

The small sampler below is an illustration, not an ML-DSA signing implementation. Its word operations use unsigned arithmetic modulo $2^{32}$. A branchless source expression is useful structure for a verifier; it is not yet a constant-time theorem about a target instruction sequence.

module Clef.Cryptography.ConstantTime

// all-ones mask -> a, all-zeros mask -> b. selection is arithmetic,
// control flow does not depend on the secret.
let ctSelect (mask: uint32) (a: uint32) (b: uint32) : uint32 =
    b ^^^ ((a ^^^ b) &&& mask)

// 0xFFFFFFFF if x < bound, else 0. no early exit.
let ctBelow (x: uint32) (bound: uint32) : uint32 =
    let diff = x - bound
    let borrow = ((~~~x &&& bound) ||| (~~~(x ^^^ bound) &&& diff)) >>> 31
    0u - borrow

This sampler draws a 32-bit candidate and accepts it when it is below a positive bound. Under independent uniform draws, its accepted values are uniform in the requested interval. That probability model is a premise, not something inferred from the type unit -> uint32. The code also needs 0 <= n <= output.Length, initialized, exclusively owned output storage, and a stream call that returns without changing that storage. The loop count and write index depend on acceptance, even though selection uses a mask. If those observations depend on a secret, branchless arithmetic does not remove the leak. An actual signature sampler requires a separate argument about its secret inputs, rejection rule, and allowed observations.

// Illustrative unsigned-word sampler; assumes IID uniform 32-bit draws.
// Requires bound > 0 and 0 <= n <= output.Length.
// The initialized output buffer is exclusively owned; stream returns and preserves it.
// Acceptance controls the loop count and addresses, despite masked selection.
let sampleUniform (stream: unit -> uint32) (bound: uint32)
                  (n: int) (output: uint32[]) : unit =
    let mutable filled = 0
    while filled < n do
        let cand = stream ()
        let accept = ctBelow cand bound
        output.[filled] <- ctSelect accept cand output.[filled]
        filled <- filled + int (accept &&& 1u)

Our aim is for CCS to derive supported obligations from the routine’s structure and instantiate applicable proof rules. The security specification still has to say what an adversary can observe and what property is required. Library lemmas, annotations, or an interactive proof may be needed when automatic discharge stops. Connecting a generated proof to the emitted binary is further work, with its own semantics and validation obligations. That posture, where the compiler reduces the burden of proof while making the remaining obligations visible, is the one Fearless Concurrency Gets Real develops for memory and liveness.

Negative-Cost Verification

Stroustrup’s now-famous “negative-cost abstraction” describes how high-level structure can help an optimizer produce better machine code. Our use of “negative-cost verification” is an engineering ambition in the same spirit: dimensions, ranges, escape behavior, and grades can justify representation and placement choices for a hardware substrate. Proof construction still costs resources, and whether its optimization benefits outweigh that cost needs measurement. The Native Type Universe gives us structure to exploit; it does not establish a performance result by itself.

The usual pitch is that proof is a cost the developer accepts directly: write the annotations, cycle proof terms on top of debugging, and accept the slowdown, then eventually collect the warrant. We took the opposite position. A large share of the proof work is meant to be automated as structural support the compiler derives from the program already written, and that automation is an accelerant rather than a tax.

It is meant to move development forward, because the obligations will be discharged as the program is elaborated, surfaced in the editor at the point of writing. We want the most common proof terms to be a design-time element in order to support correctness, a property that identifies issues immediately instead of after a separate verification pass, a failed audit, or worse, a production incident. The feedback loop that formal methods usually defer to the far end of a project sits at the moment of authorship instead. We saw this in F*’s design and, absent of the annotation burden, we really appreciated the design-time feedback it provided. Along those lines, our approach should lighten the annotation burden, because the structural facts that higher obligations consume, the dimensions and lifetimes and escape behavior and grade, are inferred from the code’s own structure where a conventional workflow demands them as explicit declarations. The annotations a conventional verified-programming workflow makes the developer write are, in the cases our algebra covers, derived by the compiler instead of requiring the developer to hand-roll the full assembly of proof terms directly.

That ambition carries all the way to the top tier. Automating local premises can reduce the work a domain expert needs to reach a relational guarantee. Tier 3 library lemmas may already be proved in Rocq, so the proof-assistant dependency does not begin exclusively at Tier 4. The specialist still owns the security definition, the choice of applicable theorem, and any premises the compiler cannot establish.

What spans, and what stays local

Many obligations the compiler is intended to check directly in the PSG concern dimensions, ranges, escape classes, or integer widths. We aim to encode supported cases in specified decidable theories, such as linear arithmetic and fixed-width bit-vectors. Decidability does not promise microsecond answers or polynomial complexity for every combination of those theories. The Decidability Sweet Spot explains the intended scope, and Formal Verification as Compilation Byproduct describes how deriving these obligations could reduce the developer’s annotation burden.

Some properties are not local. A circular wait is a relationship among actors. For a finite, completely modeled wait-for graph, assigning integer ranks that strictly increase along every edge is equivalent to acyclicity. Deadlock Freedom as an Obligation uses that idea: extract the wait edges, then check $r(u) < r(v)$ for each edge. Extending the result to program deadlock freedom requires the operational model to account for all relevant waits and resources. Acyclicity alone does not establish that a sampler terminates, a message is delivered, or an actor is eventually scheduled.

A signing-service sketch is a useful place to see this. A signer actor fans the work out: it asks a sampler worker for the rejection-sampled vector and a hasher for the challenge, and it blocks on each reply. Nothing here is annotated for liveness.

let sampler = spawn SamplerActor
let hasher  = spawn HasherActor

let signRequest (params: SamplingParameters) (msg: Message) (sk: SecretKey) = actor {
    let! y = sampler.PostAndReply (Sample params.bound params.n)   // signer -> sampler
    let! c = hasher.PostAndReply  (Challenge msg y.commit)  // signer -> hasher
    return assemble y c sk
}

Each let! … = callee.PostAndReply … suspends the signer until the callee answers, so each is one wait-for edge with the callee at its head. Reading the saturated graph, the compiler would collect those edges over the enclosing region and emit the acyclicity obligation. No edge is written by the developer; each falls out of a PostAndReply the code already contains.

// witnessed from the PSG read of signRequest and its callees.
%e0 = wait_edge { from = @signer, to = @sampler }   // from `let! y = sampler.PostAndReply ...`
%e1 = wait_edge { from = @signer, to = @hasher  }   // from `let! c = hasher.PostAndReply ...`
// Schematic finite encoding: one rank inequality per extracted edge.
smt.assert (lt (rank @signer) (rank @sampler))
smt.assert (lt (rank @signer) (rank @hasher))
smt.check   // sat: check the rank witness for every modeled edge.
            // unsat: diagnose a cycle in this finite wait graph.
             

A signer that fans out to leaf workers has a rank: the workers sit above the signer in the ordering and never call back, so a rank witness exists for the modeled edges. The priority a developer would otherwise hand-write is that rank. No actor carries the broader-program fact; each carries its own wait edge, and our analysis gathers them at the enclosing region.

This acyclicity check is a spanning concern: it reaches across the finite wait graph and consumes local facts as premises while staying in a decidable fragment.

‘Spanning’ is not the same as ’exotic’ in that conceptual frame.

The semantic graph is intended to retain the facts needed by those checks and connect them to the region they describe. The Compilation Sheaf develops the proposed local-to-global account. Its usefulness depends on proving the composition and preservation rules for the actual semantics; storing the facts together is not itself that proof.

Where the target set widens

The theories the framework targets are not fixed. Integer-linear arithmetic is one workhorse; rational dimensional exponents motivate rational linear equations and, where appropriate, linear real arithmetic. That widening is discussed in the negative and fractional types pre-print and Getting Real with Fidelity Framework. Solving those algebraic constraints is distinct from measure-theoretic probability over real-valued random variables. Complexity also depends on the exact fragment: rational linear systems, integer constraints, Boolean combinations, and bit-vectors do not share a blanket polynomial bound. The Fixed-Point Scaffolding pre-print describes the intended connection to lowering; each extension still needs an explicit supported theory and preservation argument.

For these supported fragments, neither ‘spanning’ nor reaching into the reals steps away from the obligations the compiler is designed to discharge automatically. This commitment to shaping routine obligations for supported decidable theories is something we arrived at on our own, but the practical ambition has good company. The Dafny language has a much longer history of bringing automated verification into ordinary programming, by a different road.

As anyone who has followed our work knows, a significant influence beyond F# is the F* language. Through our research we saw side-long references to Dafny as a separate SMT-backed verification tradition. We didn’t realize the sympathies between our work and the established art in Dafny until quite recently, after several of our papers were already written. That kinship deserves a precise account: Dafny’s full verification language admits quantified specifications, and its SMT verification can return unknown or time out; it is not confined to a decidable fragment. The reference manual makes those limits explicit. Its verification guidance also shows how intermediate assertions, lemmas and careful control of the available facts can help automatic proof succeed. We arrived through dimensional algebra at a related practical goal: make the routine obligations predictable enough for automatic discharge, and retain the premises that justify them. That shared engineering concern is what makes the comparison useful to us.

The intermediate assertion is a useful primitive to think with. We can read it as a cut: establish an intermediate fact, then use it to establish the goal. In Clef’s design, that suggests a mode shift within the same tier, with a splitting obligation and no change in verification strength. Clef’s lower-tier design calls for CCS to derive obligations by applying the program’s operations and guards together with applicable library laws and platform declarations, retaining and checking their premises in the Program Semantic Graph. The developer supplies an additional annotation when a needed fact or relationship cannot be established from that context. Where a stronger judgment needs a transition between tiers, the design requires a justified rule and checked premises, even when the compiler can select and instantiate the rule automatically.

Dafny also helps sharpen the question we keep asking about compilation: what connects a property verified at the source to the behavior of the emitted program? A source proof needs that connection through the compiler and the selected runtime or target, whatever language supplies the proof. Clef’s preservation requirement is that the source property and its justification survive a lowering by an established preservation argument, or that the affected obligation be re-checked at that edge. Composer’s design carries the relevant facts through its middle end, using MLIR’s SMT dialect for supported obligations. The lowering checks are being developed against this requirement. The lessons Dafny offers reinforce our interest in making proof practical while keeping the source-to-artifact correspondence explicit.

The relational concern

A relational proof concerns multiple executions or computations. A constant-time argument might compare their observable traces when public inputs agree and secrets differ. A cryptographic game argument instead quantifies over adversaries and compares event probabilities, often through reductions to hardness assumptions. These are related techniques, not interchangeable guarantees. A signature need not have identical outputs for different secret keys to be unforgeable.

Our routine solver tier is not intended to supply a general probability semantics or discover arbitrary couplings. Particular finite probability obligations can be encoded into arithmetic, and some relational checks can be automated. General probabilistic program proofs require additional definitions, rules, and proofs; the boundary is the supported encoding and proof method, not a universal impossibility of expressing distributions with refinement types.

That distinction matters for F*. RF*, a relational extension of F*, already demonstrated probabilistic relational verification for cryptographic implementations. Its relational refinement system was given a semantic soundness proof in Coq. This is a research result, not evidence that Fidelity’s current backend provides the same integration. It does rule out the claim that F* or refinement types inherently have nowhere to put a distribution or a coupling. Likewise, equality of results under a shared random tape can be useful in a probabilistic proof; it does not mean the modeled program is deterministic in its externally supplied randomness.

Probabilistic relational Hoare logic (pRHL) is a program logic formalized in systems such as CertiCrypt and used by EasyCrypt. It is not built into Rocq’s kernel. A pRHL judgment relates modeled computations through a specified precondition and postcondition; equality of output distributions is one possible conclusion with suitable premises. Computational-security claims must specify adversary classes and resource bounds; claims based on hardness assumptions also require the relevant reduction. Sending a statement to Rocq supplies none of those automatically.

Here is a smaller obligation our sampler could support. It concerns the distribution of returned samples, not the secrecy of an ML-DSA signing key. The notation is proposed Clef proof syntax; it is not an implemented compiler feature or a checked theorem.

[<Tier4.Relational>]
let samplerMatchesIdeal =
    relating (run_left  = sampleUniform stream bound n output)
             (run_right = idealUniformVector bound n)
    requires (0u < bound && 0 <= n && n <= output.Length)
    requires (iidUniform32 stream && streamCallsReturn stream)
    requires (exclusiveInitializedBuffer output && streamPreservesBuffer stream output)
    couples  (acceptedSubsequence stream ~ run_right)
    consumes Tier3.rejectionTerminates stream bound n
    consumes Tier2.memorySafe sampleUniform
    ensures  (distribution (outputPrefix (finalState run_left) n)
              = distribution run_right)
    dispatch_to Rocq

The relating clause names the computations; couples asks for a coupling with the required marginals and output relation. The consumes clauses identify premises whose proof must be available. Instantiating a named lemma must check that its language semantics, randomness model, and concrete program match this obligation. A separate side-channel theorem would specify traces and public inputs; the output-distribution theorem above would not establish it.

The proposed tier shifts are applications of such checked rules. A branchless loop can still run forever. For the 32-bit sampler, independent uniform draws give acceptance probability $p = \mathrm{bound}/2^{32} > 0$, provided each stream call returns. That supports almost-sure termination for finite nonnegative n and the negative-binomial expectation $n/p$. More general samplers need their own progress premises: a uniform positive lower bound on the conditional acceptance probability can support a bound, but merely having some positive chance on each attempt need not imply almost-sure termination.

// Proposed statement; the probability model and theorem need formalization.
[<Tier3.Lemma>]
let rejectionTerminates (stream: unit -> uint32) (bound: uint32) (n: int) =
    requires (0u < bound && 0 <= n)
    requires (iidUniform32 stream && streamCallsReturn stream)
    ensures  (terminatesAlmostSurely (rejectionLoop stream bound n))
    ensures  (expectedIterations (rejectionLoop stream bound n)
              = toRational n * 4294967296 / toRational bound)
    discharge_via NegativeBinomial

Almost-sure termination permits exceptional infinite random sequences; it is not a worst-case iteration bound. A real stream implementation also needs a justified relationship to the probability model. The compiler may recognize an instance of a proved termination lemma, but a Tier 2 mask or range fact cannot create that theorem. If the lemma is proved in Rocq, Rocq is already part of the proof dependency at Tier 3.

Rocq’s constructive foundation does not forbid classical probability. Its standard library provides classical logic and reals, and MathComp Analysis includes measure theory and probability measures. Lean’s Mathlib makes extensive mathematical infrastructure available too. Connecting that mathematics to a particular Iris program logic requires a matching semantics, inference rules, and soundness or adequacy proofs; the presence of a library alone does not supply the integration. This distinction lets us take the new Iris-Lean work seriously without turning its continuous-probability case study into a claim that Rocq lacks cryptographic mathematics.

Our automation target is correspondingly specific: instantiate proved domain rules where applicable, discharge supported arithmetic leaves, and expose unresolved obligations. The trusted dependencies include the encoding and verification machinery, the selected libraries and their assumptions, and any solver results accepted without checked certificates. The proof assistant’s kernel does not enter at a single universal boundary between Tier 3 and Tier 4.

Bracketing pRHL with the lowering machinery

The design proposes two checkpoints: one for the source-level model and another for the emitted artifact. They require a semantic bridge between them.

The first would run after front-end elaboration, before lowering. A Rocq development would receive an encoding of the relevant program semantics and its established premises, not the program’s meaning merely by virtue of having access to the PSG. The Mode Shifts proposal describes how supported obligations could be routed and composed. Building and validating those encodings remains part of the implementation work.

During lowering, Composer is intended to carry supported facts and their justifications, including suitable encodings through MLIR’s SMT dialect. A transformation may affect termination, randomness, observations, or adversary interfaces as well as local arithmetic. The relational theorem therefore needs a proved preservation result, a checked translation validation result, or a new proof about the transformed program. Rechecking local ranges alone does not establish preservation of an arbitrary cryptographic relation.

The second checkpoint would check the emitted artifact and its associated evidence. From Proofs to Silicon proposes a release certificate recording the artifact, theorem, and evidence. Hashing a binary together with a witness binds their identities; it does not prove that the witness describes that binary’s behavior. An independent checker needs the relevant target semantics and a checked correspondence theorem or validation result, including the chosen leakage model where the claim concerns side channels. The certificate format and the checker must make those dependencies available. This is a planned capability, not something established by the existence of a .proofcert field or a tier label.

The same discipline applies to lower-tier premises. We intend supported arithmetic premises to be re-established by kernel-checked proofs, and solver certificates to be reconstructed by a checked procedure where one is available. Until that path exists for the selected solver and theory, a solver verdict remains a trusted dependency. An auditor should inspect the theorem statement, its explicit hypotheses, and Rocq’s Print Assumptions output. Standard classical axioms, abstract parameters, cryptographic hardness assumptions, and admitted proof gaps are different categories and must be reported as such. A successful kernel check does not establish the truth of arbitrary assumptions or the fidelity of an unproved encoding.

A backend that turns a select into a secret-dependent branch is an example of what a target-level observation check should detect. That requires checking the relevant instructions under the observation model, or a preservation theorem strong enough to cover them. Re-running a source theorem cannot see an unmodeled binary change. Artifact-level verification, including any later hardware synthesis, is therefore a substantive engineering requirement wherever the release claim extends to those stages. Its cost and scope depend on the target and the property.

Why ‘TCB size’ matters

A guarantee depends on its trusted computing base (TCB), its mathematical assumptions, and the correspondence between its model and its subject. Our two-checkpoint design aims to make those dependencies explicit and reduce the amount of translation machinery that must simply be trusted. A compiler pass can leave the trusted base for a particular property when an independently checked preservation or validation argument covers it. The existence of a second checkpoint alone does not accomplish that.

The distinction is already explicit in F*’s documentation: ordinary SMT-backed verification trusts both its encoding and the solver. A Rocq proof can reduce that dependency when it reconstructs the relevant evidence, but it still needs the right statement and an audited assumption set. This is why our tier labels describe proof methods and intended obligations, rather than a universal ranking of certainty.

The shape of things to come

Our design seeks to automate supported routine obligations and reuse proved rules for more demanding properties. Some spanning checks remain in decidable fragments; some Tier 3 lemmas already require richer mathematics; cryptographic game proofs add their own semantics and assumptions. Linear real arithmetic is not measure theory, and probabilistic reasoning is not the only reason a proof may require specialist work.

What remains to be built includes the concrete proof-library integrations, semantics-preserving encodings, rule instantiation with checked premises, and source-to-artifact evidence for the properties we intend to claim. Reducing the specialist’s proof burden is the goal. It does not remove the need to state the security property or justify how the deployed implementation satisfies it.

Rocq, formerly Coq, is a proof assistant whose kernel checks proofs in its type theory. Its role in CompCert and the Verified Software Toolchain makes it a serious foundation for this work, not a ready-made verification layer for Fidelity. We plan to use it both for suitable domain lemmas and for independently checkable proof artifacts. Its logical language, Gallina, is based on the Calculus of Inductive Constructions; Rocq’s implementation uses OCaml, but Gallina is not an ML-family language descended from OCaml. The connection that matters is the ability to state definitions, construct proofs, and inspect their assumptions precisely. The title is a small joke on the name. The choice behind it carries a concrete responsibility: make every claimed guarantee traceable to the theorem, the program, and the evidence an independent checker can actually check.

The deeper treatments live in the framework’s design documentation and pre-prints, collected in A Deeper Dive: the decidability sweet spot, the deadlock freedom as an obligation, the compilation sheaf, the mode-shifts proposal, and the artifact certificate.

References

[1] K. R. M. Leino, “Dafny: An automatic program verifier for functional correctness,” in Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-16), pp. 348-370, Springer, 2010.

[2] G. Barthe, B. Grégoire, and S. Zanella-Béguelin, “Formal certification of code-based cryptographic proofs,” in Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 90-101, 2009.

[3] Symbolic Software, “The Verification Facade: Structural Gaps in Cryspen’s Hax Pipeline,” symbolic.software, 2026.

[4] X. Leroy, “Formal verification of a realistic compiler,” Communications of the ACM, vol. 52, no. 7, pp. 107-115, 2009.

[5] P. Wadler, “Theorems for free!” in Proceedings of the Fourth International Conference on Functional Programming Languages and Computer Architecture, pp. 347-359, ACM, 1989.

[6] H. Haynes, “Fixed-Point Scaffolding in the Clef Programming Language,” arXiv:2606.02854, 2026.

[7] H. Haynes, “Negative and Fractional Types in the Fidelity Framework,” arXiv:2606.04352, 2026.

[8] N. Swamy, C. Hriţcu, C. Keller, A. Rastogi, A. Delignat-Lavaud, S. Forest, K. Bhargavan, C. Fournet, P.-Y. Strub, M. Kohlweiss, J.-K. Zinzindohoué, and S. Zanella-Béguelin, “Dependent Types and Multi-Monadic Effects in F*,” in Proceedings of the 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ‘16), pp. 256-270, 2016.