Concrete Documentation | Concrete Documentation

Concrete documentation

Concrete

A small systems language where source code carries evidence about authority, assumptions, tests, and Lean-checked proofs.

Project status: experimental. Compiler correctness and backend correctness are not fully proved today.

1. Abstract

Concrete is a no-GC systems language with linear ownership and explicit capabilities. Its compiler is written in Lean and maintains a registry connecting source functions to proof artifacts, assumptions, test oracles, policy files, and drift checks.

The immediate claim is narrow: the toolchain should not let evidence silently lie. If a function body changes, authority widens, allocation appears, or a proof no longer matches the source, normal reports and CI gates should show that change.

2. Evidence Model

Concrete separates claim classes instead of reducing everything to one green badge. The current audit vocabulary is deliberately explicit:

Claim	Status class	Current meaning
Capabilities	enforced	Function authority is tracked and reported.
User theorems	Lean kernel	Attached theorems are checked by Lean.
Proof drift	CI gated	Body/spec fingerprints downgrade stale proofs.
Oracle behavior	tested	Flagships carry differential or reference tests.
Extraction soundness	partial	Some source-to-ProofCore rules are proved; work continues.
LLVM/backend	trusted	Generated binary correctness is still in the trusted base.

3. Running Example

The narrow real-crypto example is a constant-time tag comparison. Its proof does not claim machine-level constant time. It proves a source property and names the remaining timing assumptions.

fn ct_compare(a: [u8; 16], b: [u8; 16]) -> Int {
    let diff: u8 = 0;
    let i: Int = 0;

    while i < 16 {
        set diff = diff | (a[i] ^ b[i]);
        set i = i + 1;
    }

    if diff == 0 { return 1; }
    return 0;
}

Listing 1. Source code stays ordinary: fixed arrays, byte operations, bounded loop, no allocation, no ambient authority.

$ concrete audit examples/constant_time_tag/src/main.con

proof:
  ct_compare_same_tag_correct: proved_by_lean
  coverage: one_direction

authority:
  capabilities: none
  allocation: none
  trusted code: none

assumptions:
  machine-level constant-time: assumed
  backend timing preservation: trusted

Listing 2. Audit output keeps proved facts separate from assumptions and trusted backend behavior.

4. Current Status

Example	Status	Purpose
parse_validate	graduated	Parser/protocol validation evidence.
crypto_verify	graduated	Authentication scaffolding with a toy MAC.
fixed_capacity	graduated	Bounded mutable state and array-update proofs.
constant_time_tag	graduated	Narrow real-crypto source proof with timing assumptions.
hmac_sha256	candidate	Larger SHA-256/HMAC refinement target.

5. HMAC Work

HMAC-SHA256 is the active proof target. The implementation and oracle tests exist; the remaining graduation work is the refinement chain from extracted Concrete code to an independent SHA-256/HMAC specification.

Round-function refinements: started.
Block-to-words loop refinement: done.
Schedule refinement: in progress.
Compression, hash, and HMAC composition: open.

6. What Concrete Does Not Claim Yet

Concrete is not a verified compiler today. It does not yet prove generated binary correctness, whole-program constant-time behavior, or every source-to-ProofCore extraction rule. Source contracts, generated verification conditions, SMT assistance, ghost state, and gradual runtime checks are roadmap work, not shipped language features.

7. Read Next

Getting startedBuild the compiler and run a program.
Provable subsetWhat can carry Lean-backed evidence today.
SafetyCapabilities, trusted code, Unsafe, and proof boundaries.
PaperResearch-style statement and build notes.
RoadmapActive sequencing and open proof work.