Type System

This document describes Lof’s type system research and design, focusing on how dependent information flow types enable fine-grained security policies for ZK circuits.

Overview

Lof combines three type system features to provide compile-time security guarantees for zero-knowledge circuits:

Strong Static Typing: Every value has a precise type known at compile time
Information Flow Tracking: Track public/private data flow through computations
Dependent Types: Types that depend on values to express invariants

This combination allows Lof to prevent privacy leaks, ensure correctness, and verify security properties before proof generation.

The Problem: Privacy in ZK Circuits

Zero-knowledge circuits have a fundamental security requirement: private witnesses must never leak to public outputs.

Traditional type systems are insufficient because:

They don’t distinguish public vs private data
Information flow isn’t tracked through computations
No way to express “this computation preserves privacy”

Example Vulnerability

proof Vulnerable {
    witness secret: Field;
    output leaked: Field;

    leaked === secret  // BUG: private data exposed publicly!
}

A naive type system sees both as Field and allows this. Lof’s information flow types catch this at compile time.

Information Flow Types

Visibility Levels

Lof tracks visibility as part of the type:

Public    // Data visible to everyone
Private   // Witness data (secrets)

These form a security lattice:

Public ⊑ Private

Meaning: public data can flow into private contexts, but not vice versa.

Tagged Types

Types are tagged with visibility:

Field@Public     // Public field element
Field@Private    // Private field element
Bool@Public      // Public boolean

Flow Rules

Information flow follows these rules:

Rule 1: Computation propagates privacy

witness x: Field@Private
input y: Field@Public

let z = x + y  // Type: Field@Private (private taints the result)

Rule 2: Cannot assign private to public

witness secret: Field@Private
output result: Field@Public

result === secret  // TYPE ERROR: cannot flow Private to Public

Rule 3: Same-level operations allowed

input a: Field@Public
input b: Field@Public

output sum: Field@Public
sum === a + b  // OK: Public + Public = Public

Dependent Types

Types can depend on values to express invariants and policies.

type PositiveField = refined { Field, x > 0 }

witness amount: PositiveField  // Statically guaranteed > 0

Dependent Security Policies

Combine visibility with refinements:

type SecureRange(level: Visibility, min: Nat, max: Nat) =
    refined { Field@level, x >= min && x < max }

// Private age between 0-150
witness age: SecureRange(Private, 0, 150)

// Public proof that age is in valid range (without revealing exact value)
output ageValid: SecureRange(Public, 18, 200)

Value-Dependent Visibility

Types can express how visibility changes based on values:

// Declassification: convert private to public with proof
type Declassified(x: Field@Private, proof: Proof) =
    { y: Field@Public | verifies(proof, x, y) }

Declassification

Converting private data to public requires explicit proof obligations.

Controlled Declassification

// Explicit declassification function
let declassify<T> (x: T@Private) (proof: SafetyProof): T@Public =
    // Compiler ensures proof demonstrates safety
    ...

Range Proof Example

proof AgeVerification {
    witness age: Field@Private;
    output valid: Bool@Public;

    // Prove age >= 18 without revealing exact age
    let isAdult: Bool@Private = age >= 18;

    // Declassify only the boolean result
    valid === declassify(isAdult)(rangeProof)
}

Hash Commitment Pattern

proof CommitmentVerify {
    witness secret: Field@Private;
    input commitment: Field@Public;
    output verified: Bool@Public;

    // Hash stays private
    let hash: Field@Private = poseidon(secret);

    // But we can prove equality
    assert hash === commitment  // TYPE ERROR: mismatched visibility!
}

Wait - this reveals a challenge. How do we compare private and public values?

Cross-Level Constraints

We need special constraint operators that work across visibility levels:

// Constraint equality works across levels (generates R1CS)
witness w: Field@Private
input x: Field@Public

assert w === x  // OK: creates constraint, doesn't leak w

The key insight: constraint generation doesn’t leak information, it just enforces relationships.

Dependent Information Flow Types

Combining dependent types with information flow:

Security-Indexed Types

// Type indexed by security level
type Secure<α: Visibility>(T: Type) = T@α

// Function preserving security level
let add<α> (x: Secure<α>(Field)) (y: Secure<α>(Field)): Secure<α>(Field) =
    x + y

Context-Dependent Types

// Type changes based on computation context
type Computed<α, β>(x: T@α, y: T@β): T@(α ⊔ β)  // ⊔ is lattice join (max)

witness w: Field@Private
input i: Field@Public

let result = compute(w, i)  // Type: Field@Private (Private ⊔ Public = Private)

Proof-Indexed Declassification

type SafelyDeclassified(x: Field@Private, policy: Policy) =
    { y: Field@Public |
        ∃ proof. verify(proof, policy, x, y)
    }

// Example policy: "only reveal range, not exact value"
let rangePolicy = RangePolicy(18, 150)

witness age: Field@Private
let ageProof: SafelyDeclassified(age, rangePolicy) = ...

Type Checking Algorithm

Flow Sensitivity

Track visibility through control flow:

match condition with
| true => {
    witness secret: Field@Private;
    // secret is Private here
}
| false => {
    input public: Field@Public;
    // public is Public here
}

Constraint Context

Special context for constraint generation:

// In constraint context, cross-level operations allowed
assert (witness: Field@Private) === (input: Field@Public)  // OK

// In computation context, not allowed
let x = (witness: Field@Private) + (input: Field@Public)  // Type: Field@Private
output y: Field@Public
y === x  // ERROR: cannot assign Private to Public

Verify dependent type predicates:

type PositiveField = refined { Field, x > 0 }

let addPositive (a: PositiveField) (b: PositiveField): PositiveField =
    // Compiler proves: (a > 0 ∧ b > 0) ⟹ (a + b > 0)
    a + b

Advanced Features

Linear Information Flow

Prevent witness reuse to avoid side channels:

witness secret: Linear<Field@Private>

let hash1 = hash(secret)  // OK: first use
let hash2 = hash(secret)  // ERROR: secret already consumed

// This prevents timing attacks from multiple uses

Effect System Integration

Track constraint generation as effects:

effect Constrained(s: Signal)

assert x === y
// Effects: Constrained(x), Constrained(y)

// Proof must constrain all witnesses
proof P {
    witness w: Field@Private;
    // ERROR: witness w not constrained (no effect Constrained(w))
}

Information Erasure

Computations that provably erase information:

// One-way function: Private -> Public is safe
type OneWay(f: Field@Private -> Field@Public) = {
    f | ∀ y: Field@Public. |{ x | f(x) = y }| > 1
}

let hash: OneWay = poseidon  // OK: hash has collisions

Practical Applications

Anonymous Credentials

proof AnonCredential {
    witness age: Field@Private;
    witness credential: Field@Private;
    input credRoot: Field@Public;
    output valid: Bool@Public;

    // Prove credential membership without revealing it
    let proof = merkleProof(credential, credRoot);
    assert verifyMerkle(proof);  // Private credential, public root

    // Prove age requirement
    assert age >= 18;

    valid === true
}

Private Voting

proof Vote {
    witness vote: Field@Private;  // 0 or 1
    witness voterKey: Field@Private;
    input eligibleVoters: Field@Public;
    output voteCommitment: Field@Public;

    // Prove voter is eligible
    assert memberOf(voterKey, eligibleVoters);

    // Prove vote is valid
    assert vote * (vote - 1) === 0;  // vote ∈ {0, 1}

    // Commit to vote without revealing it
    voteCommitment === hash(vote, voterKey)
}

Confidential Transactions

proof ConfidentialTransfer {
    witness balance: Field@Private;
    witness amount: Field@Private;
    input commitment: Field@Public;
    output newCommitment: Field@Public;

    // Prove balance matches commitment
    assert hash(balance) === commitment;

    // Prove sufficient funds
    assert balance >= amount;

    // Create new commitment
    newCommitment === hash(balance - amount)
}

Research Directions

Open Questions

Type Inference: Can we infer visibility levels automatically, or must they be explicit?
Decidability: Is type checking decidable for the full dependent information flow system?
Granularity: Should we support more fine-grained levels than Public/Private?
Composition: How do types compose across proof boundaries and proof composition?
Optimization: Can type information guide constraint optimization?

Future Extensions

Multi-Level Security

// Lattice with multiple security levels
type Classified = Public | Internal | Secret | TopSecret

// Automatic level propagation
let combine (x: Field@Secret) (y: Field@Internal): Field@Secret = x + y

Probabilistic Privacy

// Differential privacy via types
type DP<ε>(T) = DifferentiallyPrivate<ε, T>

let noisySum (data: Array<Field@Private, N>): Field@DP<1.0> = ...

Proof Composition

// Compose proofs while tracking information flow
proof P1 { ... }
proof P2 { ... }

let composed = P1 ∘ P2  // Type system ensures safe composition

Formal Foundations

Type System Specification

Γ ⊢ e : T@α

Where:
- Γ is the typing context
- e is an expression
- T is the base type
- α is the visibility level

Flow Rules (Formal)

Γ ⊢ e₁ : T@α    Γ ⊢ e₂ : T@β
─────────────────────────────────  (T-OP)
Γ ⊢ e₁ ⊕ e₂ : T@(α ⊔ β)


Γ ⊢ e : T@Private    x : T@Public ∈ Γ
─────────────────────────────────────  (T-LEAK-ERROR)
Γ ⊬ x := e

Soundness Theorem

Theorem (Noninterference): If Γ ⊢ proof : Valid and all witnesses are typed @Private, then public outputs are independent of witness values (modulo constraints).

Proof sketch: By induction on typing derivations, show that information only flows upward in the security lattice.

Implementation Notes

Current Status in Lof

The current Lof implementation has:

Basic visibility tracking (input, witness, output)
Type checking for field operations
Pattern matching with type safety

Planned Enhancements

Full dependent information flow types
Automatic visibility inference
Refinement type checking
Linear witness tracking
Effect system for constraints

References

Myers, A.C. “JFlow: Practical Mostly-Static Information Flow Control” (1999)
Zdancewic, S. “Programming Languages for Information Security” (2002)
Xi, H. “Dependent Types in Practical Programming” (1998)
Norell, U. “Dependently Typed Programming in Agda” (2009)
Swamy, N. et al. “Secure Distributed Programming with Value-Dependent Types” (2011)