Skip to content

Latest commit

 

History

189 Commits

Folders and files

NameName
Last commit message
Last commit date
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Orange

Orange: cryptography you can check.

Orange is a language and toolchain for cryptography you can check. You write the mathematical specification, connect it to a fast implementation, say exactly which properties you claim, and ship the native code together with the evidence for each claim.

Orange is made for cryptographers, cryptologists, and cryptanalysts: people who read mathematics for a living. Its aim is to be exact and beautiful at once, so that Orange source reads like the definition in a standard or a paper, while every step from that definition to machine code stays precise enough to check.

Important

Orange is pre-alpha and built by one person. Today the compiler checks and evaluates a small typed fragment of the language. It does not yet generate native code or check proofs, and nothing in this repository has been independently reviewed or formally verified.

Why Orange exists

A serious cryptographic library carries several meanings at once: the mathematics it is meant to compute, the code that runs on real machines, the security properties it claims, and the evidence behind those claims. Today those meanings live in different tools: a notation for the specification, C or Rust or assembly for speed, a proof assistant for correctness, a separate analyzer for constant-time behavior, and test vectors and build logs around the outside. Each tool can be excellent. The trouble is at the crossings, where a proof about one definition gets attached to a different binary, or a source-level guarantee quietly fails to survive the compiler.

Orange aims to make those crossings part of the product:

  • One language, several semantic worlds. Mathematical specifications, executable implementations, leakage-aware machine code, security games, and proofs live in one module system, each with semantics suited to its job.
  • Claims, not labels. Instead of a single "verified" badge, every artifact carries narrowly worded claims (conformance, functional refinement, memory safety, leakage, compiler preservation, ABI agreement, and more), each with its own subject, assumptions, evidence, and outcome.
  • Evidence you can replay. Proofs, certificates, and build records are machine-readable and content-addressed, so a release can be rechecked offline.
  • A small, published trusted base per claim. Each claim names exactly which components it trusts, instead of inheriting one project-wide trust list.
  • Real native output. The end goal is production native code with a stable C ABI, deterministic builds, and signed release provenance.

These are design directions, not current features. The Orange Book explains them in depth.

A first look

This is Orange 2026 source that the current compiler accepts: three of the SHA-256 functions of FIPS 180-4, written the way the standard writes them.

edition 2026;
module sha256 {
  spec choose(x: Word[32], y: Word[32], z: Word[32]) -> Word[32] {
    (x & y) ^ (~x & z)
  }
  spec majority(x: Word[32], y: Word[32], z: Word[32]) -> Word[32] {
    (x & y) ^ (x & z) ^ (y & z)
  }
  spec big_sigma0(x: Word[32]) -> Word[32] {
    (x >>> 2) ^ (x >>> 13) ^ (x >>> 22)
  }

  // Values from round 0 of the FIPS 180-4 "abc" example.
  spec sigma0_of_h0() -> Word[32] { big_sigma0(0x6a09_e667) }
  spec majority_of_h() -> Word[32] { majority(0x6a09_e667, 0xbb67_ae85, 0x3c6e_f372) }
}

Word[32] is the ring of integers modulo 2^32, so +, -, and * on words are the ring operations: wrapping is the meaning, never an accident. >>> and <<< rotate, >> and << shift, and every amount is a literal checked against the width. Int is the type of mathematical integers, with no overflow. A literal must fit its type exactly, so 256 is an error as a Word[8], not a silent zero. Saved as sha256.or, the module checks and evaluates:

$ orangec eval sha256.or
sha256::sigma0_of_h0: Word[32] = 0xce20b47e
sha256::majority_of_h: Word[32] = 0x3a6fe667

The full SHA-256 fixture carries these functions through round 0 and reproduces NIST's published value of a, 0x5d6aebcd; the ChaCha20 fixture reproduces the quarter-round test vector of RFC 8439.

Orange's whole precedence table fits in one line: prefix operators first, then * before + and -. Operators from different families never share a level without parentheses, so every expression reads exactly as it groups. For a file mix.or whose function body is a + b ^ b <<< 7:

$ orangec check mix.or
error[ORC0108]: `^` follows `+` without grouping parentheses
 --> mix.or:4:11
  |
4 |     a + b ^ b <<< 7
  |           ^ ungrouped operator
  = note: operators from different groups have no relative precedence in Orange; parenthesize the part that applies first

Named steps and explicit conversions

A standard names its intermediate values, and so can Orange. A body may begin with let bindings, each with a stated type, and a value changes type only through a written as. The ChaCha20 quarter round of RFC 8439 then reads the way the RFC prints it, and bytes become a word in the order the standard names:

edition 2026;
module chacha20 {
  spec quarter_a(a: Word[32], b: Word[32], c: Word[32], d: Word[32]) -> Word[32] {
    let a1: Word[32] = a + b;
    let d1: Word[32] = (d ^ a1) <<< 16;
    let c1: Word[32] = c + d1;
    let b1: Word[32] = (b ^ c1) <<< 12;
    a1 + b1
  }
  spec load_le32(b0: Word[8], b1: Word[8], b2: Word[8], b3: Word[8]) -> Word[32] {
    (b0 as Word[32]) | ((b1 as Word[32]) << 8) | ((b2 as Word[32]) << 16)
      | ((b3 as Word[32]) << 24)
  }

  // RFC 8439: the quarter-round test vector of section 2.1.1 and the first
  // key word of section 2.3.2.
  spec a() -> Word[32] { quarter_a(0x11111111, 0x01020304, 0x9b8d6f43, 0x01234567) }
  spec key_word0() -> Word[32] { load_le32(0x00, 0x01, 0x02, 0x03) }
}
$ orangec eval chacha20.or
chacha20::a: Word[32] = 0xea2a92f4
chacha20::key_word0: Word[32] = 0x03020100

A binding never shadows another name, and as converts exactly one operand. x + y as Word[32] is an error, because for bytes x and y the two readings, (x + y) as Word[32] and (x as Word[32]) + (y as Word[32]), are different values. This slice, S3c, is implemented and tested; its specification is in review as OEP-0006.

A whole state as one value

A cipher works on a state, and in Orange a state is one value. Word[32]^8 is eight 32-bit words, an element of (Z/2^32 Z)^8. An array literal lists every element, and s[4] reads one at a literal index that the compiler checks against the length. One SHA-256 round of FIPS 180-4 section 6.2.2 is then one function from state to state:

spec round(s: Word[32]^8, k: Word[32], w: Word[32]) -> Word[32]^8 {
  let t1: Word[32] = s[7] + big_sigma1(s[4]) + choose(s[4], s[5], s[6]) + k + w;
  let t2: Word[32] = big_sigma0(s[0]) + majority(s[0], s[1], s[2]);
  [t1 + t2, s[0], s[1], s[2], s[3] + t1, s[4], s[5], s[6]]
}

Applied to the initial hash value and the first word of the padded "abc" block, the SHA-256 fixture gives exactly the working variables NIST publishes for round 0:

sha256::after_round0: Word[32]^8 = [0x5d6aebcd, 0x6a09e667, 0xbb67ae85, 0x3c6ef372, 0xfa2a4622, 0x510e527f, 0x9b05688c, 0x1f83d9ab]

The ChaCha20 fixture holds the whole block function of RFC 8439, ten double rounds over a Word[32]^16 state, and reproduces the serialized block of section 2.3.2 word for word. Arrays have no operators of their own, so every operator still acts on one ring element, and every index is a literal, so every position a specification reads is visible and in range. This slice, S3d, is implemented and tested; its specification is in review as OEP-0007.

Loops the way standards write them

FIPS 180-4 prepares the SHA-256 message schedule "for t = 16 to 63", and Orange writes exactly that. A loop runs over a range given by two literals, carries one accumulator of a stated type, and has that accumulator's value after its last step: a fold, with its count in plain sight. w with [t] = v is the array w with element t replaced, and [0; 64] is sixty-four zeros.

spec schedule(m: Word[32]^16) -> Word[32]^64 {
  let head: Word[32]^64 = for t in 0..16 with w: Word[32]^64 = [0; 64] { w with [t] = m[t] };
  for t in 16..64 with w: Word[32]^64 = head {
    w with [t] = small_sigma1(w[t - 2]) + w[t - 7] + small_sigma0(w[t - 15]) + w[t - 16]
  }
}

spec compress(h: Word[32]^8, m: Word[32]^16) -> Word[32]^8 {
  let w: Word[32]^64 = schedule(m);
  let k: Word[32]^64 = round_constants();
  let v: Word[32]^8 = for t in 0..64 with v: Word[32]^8 = h { round(v, k[t], w[t]) };
  for i in 0..8 with out: Word[32]^8 = v { out with [i] = out[i] + h[i] }
}

The SHA-256 fixture hashes "abc" to the digest FIPS 180-4 publishes, and the two-block NIST example too:

sha256::abc_digest: Word[32]^8 = [0xba7816bf, 0x8f01cfea, 0x414140de, 0x5dae2223, 0xb00361a3, 0x96177a9c, 0xb410ff61, 0xf20015ad]

An index such as w[t - 15] may use only literals and loop indices, and the compiler proves, before anything runs, that it stays in range for every t from 16 to 63; w[t - 17] is rejected with the range it would take, -1 through 46. An index that depends on data, the classic source of cache-timing leaks in table-driven code, cannot be written at all. The ChaCha20 fixture loads the key and nonce with loops, runs the ten double rounds as one loop, and encrypts the "sunscreen" plaintext of RFC 8439 section 2.4.2 to the RFC's ciphertext, byte for byte. This slice, S3e, is implemented and tested; its specification is in review as OEP-0008.

Prime fields and choices

RFC 7748 defines X25519 in the integers modulo 2^255 − 19: reduce after every product, read one bit of the scalar per rung of the Montgomery ladder, and swap two points when the bit is set. Orange writes each step the way the RFC does. % is Euclidean, so a % p is always the canonical residue from 0 through p − 1; a comparison gives a Bool; and if c { a } else { b } chooses one of two values of the same type and evaluates only the one it chooses.

spec rung(x1: Int, s: Int^4, set: Bool) -> Int^4 {
  if set { swap(ladder(x1, swap(s))) } else { ladder(x1, s) }
}

spec x25519(scalar: Word[8]^32, u: Word[8]^32) -> Word[8]^32 {
  let k: Word[8]^32 = clamp(scalar);
  let masks: Word[8]^8 = [1, 2, 4, 8, 16, 32, 64, 128];
  let x1: Int = decode_u(u);
  let s: Int^4 = for i in 0..255 with s: Int^4 = [1, 0, x1, 1] {
    rung(x1, s, (k[(254 - i) / 8] & masks[(254 - i) % 8]) != 0)
  };
  encode((s[0] * power(s[1], prime() - 2)) % prime())
}

The X25519 fixture computes the first test vector of RFC 7748 section 5.2, byte for byte:

x25519::test_vector: Word[8]^32 = [0xc3, 0xda, 0x55, 0x37, 0x9d, 0xe9, 0xc6, 0x90, 0x8e, 0x94, 0xea, 0x4d, 0xf2, 0x8d, 0x08, 0x4f, 0x32, 0xec, 0xcf, 0x03, 0x49, 0x1c, 0x71, 0xf7, 0x54, 0xb4, 0x07, 0x55, 0x77, 0xa2, 0x85, 0x52]

The index k[(254 - i) / 8] divides a loop index, and the compiler still proves it in range, 0 through 31, before anything runs. The Poly1305 fixture reproduces the tag of RFC 8439 section 2.5.2, and the AEAD fixture seals the section 2.8.2 "sunscreen" message with ChaCha20-Poly1305 to the RFC's ciphertext and tag. Division by zero is defined (x / 0 is 0 and x % 0 is x), so nothing fails at run time, and Bool is not a number: it converts to nothing and has only !, &&, ||, ==, and !=. A conditional is a choice between values, not a claim about how a machine branches; RFC 7748 asks for a constant-time swap, and Orange makes no timing claim until it generates code. This slice, S3f, is implemented and tested; its specification is in review as OEP-0009.

Daylight Horizon example

examples/daylight/ contains an owner-directed Orange port of Daylight Horizon v17's SHA-256, HKDF, ChaCha20 and Poly1305 computations. It includes a standalone framed-encryption vector, a host adapter that preserves Horizon's existing evidence-policy checks, and interoperability tests. This is executable reference code, not verified production cryptography.

What works today

Area Status
Source model, UTF-8 byte spans, stable diagnostic codes Working
Deterministic lexer (orangec lex) Working
Orange 2026 grammar: one edition, one module, spec and impl declarations Working
Typed spec functions: parameters, calls, Int, and Word[8] through Word[64] Working; specification in review (OEP-0005)
Operators: exact Int arithmetic, word ring arithmetic, and, or, xor, not, shifts, rotations Working; specification in review
Typed let bindings and explicit as conversions Working; specification in review (OEP-0006)
Fixed-length arrays T^n, array literals, and literal indices Working; specification in review (OEP-0007)
Bounded loops, indices proved in range, updates, and fill literals Working; specification in review (OEP-0008)
Bool, comparisons, Euclidean division, and conditionals Working; specification in review (OEP-0009)
Typed Reference Core and reference evaluator (orangec eval) Working
Data-dependent indices, mixed-type tuples, a type of integers modulo a prime Not yet
Typed impl bodies and refinement between spec and impl Not yet
Proof checking, claim reports, evidence bundles Proposed; decisions open (D-005, D-006, D-007); not built
Code generation, native targets, C ABI Proposed; strategy under investigation (D-010, D-011, D-013); not built
Cryptography corpus (hashes, AEADs, signatures, KEMs) Planned
Packages and releases Planned; no release exists

Quick start

You need rustup. The repository pins Rust 1.96.1 in rust-toolchain.toml, so rustup selects it automatically. The compiler has no third-party dependencies.

git clone https://github.com/chasebryan/orange.git
cd orange

# Build and try the compiler
cargo run --manifest-path compiler/Cargo.toml -p orangec -- eval compiler/fixtures/s3f/valid-x25519.or
cargo run --manifest-path compiler/Cargo.toml -p orangec -- eval compiler/fixtures/s3b/valid-sha256-functions.or
cargo run --manifest-path compiler/Cargo.toml -p orangec -- check compiler/fixtures/hello.or
cargo run --manifest-path compiler/Cargo.toml -p orangec -- lex compiler/fixtures/hello.or

# Run the compiler test suite
cargo test --manifest-path compiler/Cargo.toml --workspace

# Run the local repository gate: policy checks and sandboxed compiler checks
scripts/ci/check-repository

The repository gate runs on Linux and needs a C compiler, Python 3, user namespaces, and Landlock ABI 3 or newer; the policy guide explains the sandbox. Markdown lint, workflow audits, and link checks run only in CI.

orangec reads a file path, or - for standard input:

Usage: orangec [OPTIONS] <check|eval|lex> <FILE>...

Commands:
  check    Perform lexical, syntactic, and semantic validation
  eval     Reference-evaluate one source after complete validation
  lex      Print the deterministic token stream

The compiler guide covers the grammar, diagnostics, and test corpora in detail.

Roadmap

Orange is built in dependency order. Each stage adds permanent components to the production compiler; there is no throwaway prototype.

Stage Delivers Status
S0 Repository foundation: governance, CI, policy checks Done
S1 Compiler foundation: source model, spans, diagnostics, lexer, CLI Done
S2 Editioned grammar and bounded parser Done
S3 Name resolution, types, expressions, typed Core, reference evaluator In progress: typed literals done; pure expressions, bindings, conversions, arrays, loops, and conditions in review
S4 Proof and claim boundary Research underway
S5 Compiler IRs and one output path Open
S6 Memory, leakage, ABI, and native targets Open
S7 Cryptography corpus Open
S8 Packages, developer tools, and preview releases Open
1.0 Stable release Open

Three of the ten gates are closed. That counts finished stages, not effort or time remaining. The roadmap has the details, and the decision register tracks every open design choice.

Read more

Repository layout

Path Contents
compiler/ The Rust workspace: the orange-compiler library and the orangec CLI
tabula/ A local workbench for writing Orange; a separate tool, not part of the language
docs/ The Orange Book, language specification, architecture, assurance, roadmap, and decisions
research/decisions/ Decision laboratories that compare design candidates
schemas/ and conformance/ Provisional evidence schemas and their test fixtures
policy/ and tools/ Repository policy and the Python checks that enforce it
assets/identity/ and assets/brand/ The Orange emblem, wordmark, README banner, and book covers, and the original brand assets

Project status

  • Solo, pre-alpha. One owner, Chase Bryan, designs, builds, and reviews Orange. Owner review is not independent review, and passing tests show only that the implemented slice behaves as tested.
  • No license yet. An outbound license has not been chosen (D-018), so no right to use, copy, or redistribute is granted. For the same reason, outside pull requests can't be merged yet; issues with facts, sources, and questions are welcome. See CONTRIBUTING.md.
  • Security reports stay private. Use the process in SECURITY.md, never a public issue.
  • Working name. "Orange" is a working name until naming and trademark questions are settled. Other software, including an earlier systems language, already uses the name.

About

Orange is a language for specifying, implementing, and verifying cryptography.

Resources

Code of conduct

Contributing

Security policy

Stars

0 stars

Watchers

0 watching

Forks

Releases

Packages

Used by

Contributors

Languages