Inferred specs

Motivation+

Rust does not infer function signatures, on purpose. A signature is the contract with callers. If the compiler inferred it from the body, an edit to the body could change the API without anyone noticing. Rust lets this happen in one place, the auto traits of an impl Trait return type, and it is a known way to break callers.¹²+

Specs from RFC 0003 are contracts too, and the same argument says to write them all by hand. But most functions are small, and their spec says what the body already says. Writing it twice is noise, and the written copy is the one that goes stale.+

fn max(a: u32, b: u32) -> u32 {
  Silent
    if a >= b { a } else { b }
}

Unison shows a way out. Its code is content-addressed: a definition is named by the hash of its content, and callers point at that hash. Types are inferred once, then stored with the definition and shown, not recomputed. A changed body is a new definition with a new hash, so it cannot silently change what an old caller was checked against.³+

This works because Unison has no source files. The codebase is a database of definitions, and text is only a view of it. Inferred facts are part of the stored definition, so you see them by looking the definition up, and the tool prints them as if they were written. In Rust the text file is the source of truth, so anything not written in it is invisible and gets recomputed on every build. That is why Rust asks you to write signatures out. ra-jit takes the Unison half it needs: the text stays the source for code, and inferred specs live in a store keyed by hash, which the editor and ra-jit show print next to the definition.³+

This RFC applies the same idea to specs. Infer them, show them, and freeze them under the function's hash. Inference saves the writing. Freezing keeps the contract.+

Design sketch+

Inside a crate, no spec+

RFC 0003 translates every function's MIR to a Lean definition. A caller's proof can unfold that definition and reason about the body directly. Within one crate, max needs no ensures: a caller that needs max(a, b) >= a gets it by unfolding max, and omega does the rest.⁴+

This works because the caller and the body are rebuilt together. When max changes, ra-jit rechecks every proof that unfolded it, in the same edit loop.+

At boundaries, infer+

Unfolding stops working at a boundary, where the body is not something a caller should see, or cannot be unfolded at all:+

• pub items. A caller in another crate should depend on a promise, not on today's body.+

  No comments yet.

  Comments are not set up yet.

• Recursion. Unfolding a recursive function does not terminate. It needs a spec to reason about calls to itself.+

  No comments yet.

  Comments are not set up yet.

• Loops. A loop becomes a recursive function in Lean, so it needs an invariant, as in RFC 0003.+

  No comments yet.

  Comments are not set up yet.

• Opaque code. unsafe blocks, extern functions and FFI cannot be translated. Their specs are assumed, so inference here only proposes one for a person to accept.+

  No comments yet.

  Comments are not set up yet.

At each boundary, ra-jit infers a spec with three tools, cheapest first:+

1. Abstract interpretation. A fixed set of domains: integer intervals, relations between lengths and indices, and whether a pointer or Option can be empty. It is fast, always terminates, and gives facts like result <= v.len().⁵+

   No comments yet.

   Comments are not set up yet.

2. Strongest postcondition. For small, loop-free bodies, run the body symbolically and simplify what comes out. For max, this gives result == if a >= b then a else b.+

   No comments yet.

   Comments are not set up yet.

3. Proposed by a language model. For the rest, a model reads the body and proposes ensures clauses and loop invariants. Lean must prove each one. A proposal Lean rejects is dropped. The model is a source of guesses, never of truth.⁶⁷+

   No comments yet.

   Comments are not set up yet.

The editor shows inferred specs as inlay hints, after the signature, in the same syntax as a written spec. They look like code the author could have typed, and one action turns a hint into written text.+

pub fn max(a: u32, b: u32) -> u32
    // inferred: ensures result >= a, result >= b, result == a || result == b
{
    if a >= b { a } else { b }
}

Freeze it+

An inferred spec is recorded, not recomputed. The record is keyed by the function's content hash: the hash of its MIR and of the recorded specs of what it calls. It holds the spec and how it was found. The set of records works like Cargo.lock: it is written by the tool, read by the tool, and changes only as a reviewed diff.+

# specs.lock: one record per function at a boundary
[spec."mycrate::max"]
body    = "blake3:9f2c…"   # hash of the MIR and callee specs
ensures = ["result >= a", "result >= b", "result == a || result == b"]
found   = "strongest postcondition"
proof   = "blake3:41ab…"   # the Lean proof term, checked

Records are stored as content-addressed blocks. A record names its callees' records by hash, so the records form a Merkle DAG, and two machines that agree on a hash agree on everything under it. The store would be shaped like the rest of ra-jit's state: each record an entity, each dependency a pair pointing at a hash. That design belongs to its own RFC; this one needs only that records are immutable and addressed by hash.+

Callers in other crates depend on the record, not the body. Their proofs use the recorded ensures as an axiom about the callee, and the proof cache keys on the record's hash. A body edit that keeps the spec changes nothing for them.⁸+

Edits that change the spec+

After an edit, ra-jit checks the recorded spec against the new body. If it still holds, the record keeps its spec and gets the new body hash. If it no longer holds, ra-jit infers again and shows the change as a diff on the spec:+

  pub fn max(a: u32, b: u32) -> u32
-     // inferred: ensures result >= a, result >= b, result == a || result == b
+     // inferred: ensures result >= a
  2 callers relied on the removed clauses:
    geom::clamp       uses result >= b
    stats::running    uses result == a || result == b

The author accepts the diff or fixes the body. Accepting it updates the record and flags every caller whose proof used a removed clause; their proofs fail until they are fixed. A spec that gets stronger is accepted without asking, since no caller can break. Nothing is ever silently wrong: a caller is checked against a spec that held for the body it calls, or the build says why not.+

A written spec wins+

A written ensures turns inference off for that clause. It pins the promise: the body must prove it, and an edit that breaks it is a proof failure, not a diff to accept. Write a spec when the promise is part of the API, and let inference cover the rest.+

Effects follow the same rule. A written / Fs pins what a function may touch. Whether an unwritten one is inferred and recorded the same way is an open issue below.⁹+

Which spec to infer+

The strongest spec of a function is its body: it says exactly what the function does. It is also useless as a contract. Every caller would depend on every detail, and every edit would be a breaking change. That is the problem Rust avoids by not inferring signatures.+

The weakest spec, true, promises nothing, and no caller can use it. Inference aims between them: the weakest spec that the callers' proofs need, plus facts that are cheap and stable, like bounds and lengths. Concretely:+

• What callers use. Inside a workspace, ra-jit knows which facts callers' proofs used. Those are kept.+

  No comments yet.

  Comments are not set up yet.

• What the fixed domains give. Intervals and length relations are short, and they rarely change when a body is refactored.+

  No comments yet.

  Comments are not set up yet.

• Not the body restated. A clause that just repeats the body, like result == if a >= b then a else b, is shown in the editor but not recorded. For max, the recorded spec is the three clauses above, not the if.+

  No comments yet.

  Comments are not set up yet.

What it buys+

• Proofs about ordinary code without writing specs for it.+

  No comments yet.

  Comments are not set up yet.

• Contracts that do not drift: a recorded spec changes only through a diff someone accepted.+

  No comments yet.

  Comments are not set up yet.

• Callers in other crates check against a small, recorded promise, and a body edit that keeps it rechecks nothing.+

  No comments yet.

  Comments are not set up yet.

• Review of behaviour changes: a pull request that weakens a public spec shows it, and names the callers it affects.+

  No comments yet.

  Comments are not set up yet.

• A safe use for language models: they propose, Lean checks, and only the checked result is kept.+

  No comments yet.

  Comments are not set up yet.

Prior art+

• Unison: the big idea: code named by the hash of its content, typechecked once and stored. The freezing here follows it.+

  No comments yet.

  Comments are not set up yet.

• Robin Milner, A theory of type polymorphism in programming (1978) and Damas and Milner, Principal type-schemes for functional programs (1982): ML infers every type, and each well-typed term has a most general one.+

  No comments yet.

  Comments are not set up yet.

• OCaml infers a module's types, and an .mli file states its interface when the author wants to pin it (OCaml manual: the module system). ocamlc -i prints the inferred one (OCaml manual: batch compilation). Written specs overriding inferred ones follows this split.+

  No comments yet.

  Comments are not set up yet.

• The Rust Programming Language: functions: Rust requires types in signatures, by design. RFC 1522: conservative impl Trait: the one place a signature leaks something from the body, auto traits through impl Trait.+

  No comments yet.

  Comments are not set up yet.

• Rondon, Kawaguchi and Jhala, Liquid types (PLDI 2008) and LiquidHaskell: refinement types inferred by combining Hindley-Milner with predicate abstraction.+

  No comments yet.

  Comments are not set up yet.

• Flux and Lehmann et al., Flux: Liquid Types for Rust: refinement types for Rust, which infer loop annotations by liquid inference.+

  No comments yet.

  Comments are not set up yet.

• Infer: separation logic and bi-abduction: Facebook Infer analyses each procedure on its own, with bi-abduction finding the missing parts of its precondition, which is what lets it scale to large programs.+

  No comments yet.

  Comments are not set up yet.

• Daikon: likely invariants, found by watching a program run. A source of guesses, like a language model, that a prover must still check.+

  No comments yet.

  Comments are not set up yet.

• IKOS: a sound abstract interpreter for C and C++, the kind of tool the fixed domains here would follow.+

  No comments yet.

  Comments are not set up yet.

• AutoSpec: specification synthesis by LLMs with static analysis and verification, SpecGen: formal program specifications via LLMs and nl2postcond: natural language intent to postconditions: language models proposing specs, with a verifier or tests deciding which to keep.+

  No comments yet.

  Comments are not set up yet.

Open issues+

References

1. The Rust Programming Language: functions Type annotations in signatures are required, a deliberate decision in Rust's design.
2. RFC 1522: conservative impl Trait Auto traits like Send leak from the body through an impl Trait return type.
3. Unison: the big idea Code identified by the hash of its content.
4. Aeneas Translates safe Rust to Lean as pure functions; &mut becomes a value and a backward function.
5. IKOS NASA's static analyzer for C and C++, based on abstract interpretation.
6. AutoSpec: specification synthesis by LLMs with static analysis and verification An LLM proposes candidate specs; each round keeps only those the verifier accepts.
7. SpecGen: formal program specifications via LLMs LLM-generated specs for Java, mutated and filtered until they verify.
8. ra-jit: the function cache #[ra_jit::cache], and what makes a function ineligible.
9. Koka Effect types and handlers, compiled without a runtime for effects.
10. Robin Milner, A theory of type polymorphism in programming (1978) Algorithm W: ML infers every type.
11. Damas and Milner, Principal type-schemes for functional programs (1982) Every well-typed ML term has a most general type.
12. OCaml manual: the module system An .mli file states a compilation unit's interface.
13. OCaml manual: batch compilation ocamlc -i prints the interface the compiler inferred.
14. Rondon, Kawaguchi and Jhala, Liquid types (PLDI 2008) Hindley-Milner inference plus predicate abstraction infers refinement types.
15. LiquidHaskell Refinement types for Haskell, as a GHC plugin.
16. Flux Refinement types for Rust.
17. Lehmann et al., Flux: Liquid Types for Rust Synthesizes loop annotations by liquid inference.
18. Infer: separation logic and bi-abduction Bi-abduction splits the analysis of a large program into small independent analyses of its procedures.
19. Daikon Reports likely invariants observed in runs of a program.
20. nl2postcond: natural language intent to postconditions Endres et al.: can LLMs turn intent in comments into checkable postconditions?