Concrete documentation

1. Abstract

Concrete's claim is the composition: systems control and evidence accounting in the same toolchain. It combines no GC systems code, linear ownership, explicit capabilities, contracts in source, Lean checked proof links, drift detection, and audit reports that refuse to hide trust.

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. What Makes It Different

Most nearby systems pick only part of this shape: Rust has strong ownership but external proofs; Zig and C give excellent control but little built in evidence tracking; SPARK, Dafny, F*, and Why3 have strong verification but are usually SMT heavy and not shaped like a small no GC systems language; Lean and Coq have excellent proof kernels but are not ordinary systems languages.

1. No GC systems code: fixed arrays, explicit control, no hidden runtime story by default.
2. Linear ownership plus explicit capabilities: functions show what they can touch.
3. Proofs attached to source: contracts and source linked Lean evidence can go stale when bodies drift.
4. Multiple evidence classes, not one green badge: Lean proof, kernel decision, SMT with named solver trust, oracle test, enforced, assumed, trusted, partial, stale, and vacuous are distinct.
5. Audit first philosophy: reports say what is proved, enforced, tested, assumed, and trusted.
6. Lean as compiler and proof substrate: selected user proofs are checked by Lean's kernel, and compiler soundness work can live in the same ecosystem.

3. Claim Shapes

The audit class matters as much as the code. A Lean theorem, a kernel decision procedure, an oracle test, and an external solver do not mean the same thing.

#[proof_by(Examples.ConstantTimeTag.Proofs.ct_compare_same_tag_correct)]
#[ensures_proof(Examples.ConstantTimeTag.Proofs.ct_compare_different_tag_correct)]
#[proof_coverage(iff)]
#[ensures((a == b && result == 1) || (a != b && result == 0))]
fn ct_compare(a: [u8; 16], b: [u8; 16]) -> i32 {
    let mut diff: u8 = 0;
    for (let mut i: i32 = 0; i < 16; i = i + 1) {
        diff = diff | (a[i] ^ b[i]);
    }
    if diff == 0 { return 1; }
    return 0;
}

#[overflow_checked]
#[requires(0 <= off && off + 1 < len && len <= 512)]
fn read_u16_be(packet: [u8; 512], off: i32, len: i32) -> i32 {
    let hi: i32 = packet[off] as i32;
    let lo: i32 = packet[off + 1] as i32;
    return hi * 256 + lo;
}

$ make test-hmac-oracle

hmac_sha256
  reference: Python hmac/hashlib
  vectors: RFC 4231, FIPS 180-4, 600 generated cases
  status: tested_by_oracle
  proof level: regression evidence, not proof

#[requires(0 <= msg_len && msg_len <= 256)]
#[ensures(result <= 5)]
fn sha256_padded_blocks(msg_len: i32) -> i32 {
    return (msg_len + 9 + 63) / 64;
}

status: proved_by_smt
solver: z3
trust: solver_trusted
replay: none

assumed    explicit assumption, not proof
trusted    outside the proof model, named in audit
partial    one direction or point proved, not the full claim
stale      source changed after the proof was linked
vacuous    contract holds only because the premise is impossible
missing    proof eligible, but no proof is linked yet
unproven   obligation generated, not discharged
violation  runtime safety failure detected
invalid    malformed or ill scoped contract expression

4. Evidence Model

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

5. 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;
}

$ 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

6. Current Status

7. HMAC Work

HMAC-SHA256 is the deepest proof artifact. The extracted Concrete source is linked to Lean checked refinements against an independent SHA-256/HMAC specification, with drift gates tying the proof claim to the exact source body.

1. Source contracts and proof links stay in source.
2. Loop and bitvector obligations use reusable ProofKit machinery.
3. Oracle tests remain regression evidence, not proof.
4. Backend and machine-level behavior remain named trust boundaries.

8. 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.