Lean → code

lungo

Generate Rust, C, Go, Python, Swift and TypeScript from ordinary Lake projects. Lean checks and compiles the program; lungo runs it on one runtime behind an idiomatic API in each language.

Download lungo

All downloads Configuration Errors All documentation For coding agents

Sides times k, area times k²

Lean · lean/Shapes.lean

structure Rect where
  width : Nat
  height : Nat

def area (r : Rect) : Nat := r.width * r.height

@[lungo_claim "lungo.law" subject area scale]
theorem area_scale (k : Nat) (r : Rect) :
    area (scale k r) = k * k * area r := by
  simp only [area, scale]
  rw [Nat.mul_mul_mul_comm]

cargo build # build.rs: lungo_build::compile_lean("lean")

Rust · tests/rect.rs

let r = Rect { width: Nat::from(3u64), height: Nat::from(4u64) };
assert_eq!(area(r), Nat::from(12u64));

A ranking proved sorted

Lean · lean/Sorting.lean

structure Entry where
  name : String
  score : Nat

def rank (es : List Entry) : List Entry := es.mergeSort ranksBefore

@[lungo_claim "lungo.satisfies" subject rank spec RanksByScore]
theorem rank_satisfies : Satisfies rank RanksByScore :=
  fun es _ => ⟨List.pairwise_mergeSort ranksBefore_trans ranksBefore_total es,
    List.mergeSort_perm es _⟩

lungo generate --go_out=gen/go

Go · sort_test.go

ranked, err := sorting.Rank([]sorting.Entry{
    {Name: "ada", Score: big.NewInt(3)},
    {Name: "bo", Score: big.NewInt(9)},
})  // bo, then ada: the highest score first

Access checks tested against a proof

Lean · lean/Access.lean

@[lungo_spec "lungo.relation"]
def Permits (policy : List Rule) (r : Request) : Prop :=
  (∃ rule ∈ policy, rule.covers r = true ∧ rule.effect = .allow) ∧
    ∀ rule ∈ policy, rule.covers r = true → rule.effect ≠ .deny

@[lungo_role "lungo.oracle"]
def evaluate (policy : List Rule) (r : Request) : Bool := ⋯
@[lungo_claim "lungo.decides" subject evaluate spec Permits]
theorem evaluate_decides (policy : List Rule) (r : Request) :
    evaluate policy r = true ↔ Permits policy r := by ⋯

lungo generate --python_out=gen/py

Python · test_access.py

import access as A
for role, action in itertools.product(ROLES, ACTIONS):
    # the hand-written evaluator agrees with the proved oracle
    assert permits(policy, role, action) == \
        A.evaluate(policy, A.Request(role, action))

A ledger that can't be overdrawn

Lean · lean/Ledger.lean

inductive Event where
  | deposit (amount : Nat)
  | withdraw (amount : Nat)

def replay (events : List Event) : Option Nat := account.run events

@[lungo_claim "lungo.law" subject replay spec Solvent]
theorem replay_solvent (events : List Event) (accepted : (replay events).isSome) :
    Solvent.allowed events :=
  account_refines events accepted

lungo generate --swift_out=gen/swift

Swift · LedgerTests.swift

import Ledger
try replay([.deposit(amount: 100), .withdraw(amount: 30)])  // 70
try replay([.withdraw(amount: 1), .deposit(amount: 100)])   // nil: an overdraft is refused
assurance.claim("Ledger.replay_solvent")?.status  // "proved"

Numbers to bytes and back, proved

Lean · lean/Varint.lean

def encode (n : Nat) : List UInt8 :=
  if n < 128 then [n.toUInt8] else (n % 128 + 128).toUInt8 :: encode (n / 128)
termination_by n
decreasing_by omega

@[lungo_claim "lungo.roundtrip" subject encode decode]
theorem decode_encode (n : Nat) (rest : List UInt8) :
    decode (encode n ++ rest) = some (n, rest) := by
  ⋯

lungo generate --ts_out=gen/ts

TypeScript · codec.test.js

const varint = await load();
varint.encode(300n);         // [172, 2]
varint.decode([172, 2, 9]);  // [300n, [9]]
varint.decode([128, 129]);   // null: the bytes end inside a number

Time left never exceeds what was set

Lean · lean/Timing.lean

@[lungo_facility "timing.clock"]
structure Clock

@[lungo_assumption Clock]
def Ticks : Prop := 0 < ticksPerSecond ()

@[lungo_claim "lungo.law" subject secondsLeft toTicks]
theorem secondsLeft_deadline (h : Ticks) (seconds t t' : Nat) (later : t ≤ t') :
    secondsLeft (t + toTicks seconds) t = seconds ∧
      secondsLeft (t + toTicks seconds) t' ≤ seconds := by ⋯

lungo generate --c_out=gen/c

C · test.c

timing_implement_clock_now(now, NULL, NULL);       /* the host's clock */
uint64_t deadline = call(timing_deadline_in, 5);   /* 5 s from now */
now_ticks += 2500;                                 /* 2.5 s pass */
call(timing_remaining, deadline);                  /* 2: never more than 5 */

One line in build.rs

compile_lean("lean") builds the Lake project’s default targets and generates a Rust module named after the package.

Checked by Lean

Lean elaborates and kernel-checks the project; a false proof or invalid Lean fails the build.

No Lean runtime

Compiled code runs on a Rust port of Lean’s runtime, built into Rust crates or prebuilt for every other language.

Idiomatic APIs

Lean structures become Rust structs, Go structs, Python dataclasses, Swift structs, TypeScript objects; Nat an unbounded integer; IO an error.

Every language, one runtime

lungo generate writes Go, Python, Swift, TypeScript and C packages that run on the prebuilt runtime, verified by SHA-256.