Tutorial

This tutorial walks through writing an IRIS program, verifying it, evolving alternatives, deploying it, and running it as a self-improving service.

Step 1: Write a Specification

Create a file programs/my_service/spec.iris that defines what we want: a function that computes the sum of integers from 0 to n-1.

-- Sum a list of integers.
-- test: 0 -> 0
-- test: 1 -> 0
-- test: 2 -> 1
-- test: 3 -> 3
-- test: 4 -> 6
-- test: 5 -> 10
-- test: 10 -> 45
let sum_to n : Int -> Int [cost: Linear(n)] = fold 0 (+) n

The -- test: <inputs> -> <output> comments define the specification. Each line provides input(s) and the expected output, separated by ->. Multiple inputs are comma-separated.

Step 2: Write the Program

Create programs/my_service/service.iris:

-- A service that computes various reductions over integer ranges.

-- Sum of integers from 0 to n-1
let sum_to n : Int -> Int [cost: Linear(n)]
  requires n >= 0
  ensures result >= 0
  = fold 0 (+) n

-- Product of integers from 1 to n (factorial)
let product_to n : Int -> Int [cost: Linear(n)]
  requires n >= 0
  = fold 1 (\acc i -> acc * (i + 1)) n

-- Maximum of integers from 0 to n-1
let max_of n : Int -> Int [cost: Linear(n)]
  requires n >= 1
  = fold 0 (\acc i -> if i > acc then i else acc) n

-- Entry point: dispatch based on operation code
-- op=0: sum, op=1: product, op=2: max
let main op n : Int -> Int -> Int [cost: Linear(n)] =
  match op with
  | 0 -> sum_to n
  | 1 -> product_to n
  | 2 -> max_of n
  | _ -> 0

Step 3: Verify

Run the type checker to verify correctness:

iris check programs/my_service/service.iris

Expected output:

[OK] sum_to: 5/5 obligations satisfied (score: 1.00)
[OK] product_to: 4/4 obligations satisfied (score: 1.00)
[OK] max_of: 4/4 obligations satisfied (score: 1.00)
[OK] main: 6/6 obligations satisfied (score: 1.00)
All 4 definitions verified.

Step 4: Test

Run the service via main, which dispatches on the first argument (0=sum, 1=product, 2=max):

iris run programs/my_service/service.iris 0 10    # main 0 10 -> sum_to 10 = 45
iris run programs/my_service/service.iris 1 5     # main 1 5  -> product_to 5 = 120
iris run programs/my_service/service.iris 2 10    # main 2 10 -> max_of 10 = 9

Or call the individual functions directly:

iris run programs/my_service/sum_to.iris 10       # 45
iris run programs/my_service/product_to.iris 5    # 120
iris run programs/my_service/max_of.iris 10       # 9

Step 5: Evolve an Alternative

Create a specification file with test cases:

-- test: 0 -> 0
-- test: 1 -> 0
-- test: 2 -> 1
-- test: 3 -> 3
-- test: 4 -> 6
-- test: 5 -> 10
-- test: 10 -> 45
-- test: 100 -> 4950

Save as programs/my_service/evolve_spec.iris and run:

iris solve programs/my_service/evolve_spec.iris

The evolutionary engine will:

1. Analyze the test cases to detect the problem pattern (sum detection)
2. Generate seed skeletons matching the detected pattern
3. Launch enumeration in a background thread for small programs (<=8 nodes)
4. Run NSGA-II with a population of 64 individuals
5. Score each individual on three objectives: correctness, performance, verifiability
6. Report the best solution found

Example output:

Evolving solution from 8 test cases...
Evolution complete: 12 generations in 0.34s
Best fitness: correctness=1.0000, performance=0.9800, verifiability=0.9000
Best program: 3 nodes, 2 edges

Step 6: Deploy

As Deployable Rust Source

iris deploy programs/my_service/service.iris -o my_service.rs
rustc --edition 2021 -O my_service.rs -o my_service

This generates a self-contained Rust file with the bootstrap evaluator embedded.

As a Shared Library

The deploy_shared_lib API generates a .so that exports:

int64_t iris_invoke(int64_t* inputs, size_t num_inputs, int64_t* output);

Step 7: Run the Self-Improving Daemon

The daemon improves IRIS’s own internal components – not your programs, but the runtime machinery that mutation, seed generation, and evolution depend on. It breeds IRIS replacements for Rust-implemented system functions.

iris daemon --max-cycles 100 --exec-mode interval:800 --improve-threshold 2.0

By default, the daemon registers 5 components for improvement:

The daemon cycle:

1. Profile each registered component’s latency over a sliding window
2. Identify the slowest component that exceeds its baseline threshold
3. Evolve a candidate IRIS replacement in a background thread
4. Gate the replacement: must be 100% correct and no more than 2x slower
5. Hot-swap the component if it passes (or discard it)
6. Audit every change with before/after metrics
7. Roll back automatically if regressions are detected
8. Converge when no component can be improved further

Daemon Options

Monitoring

The daemon logs its activity to stderr:

Starting IRIS threaded self-improving daemon...
  max_improve_threads=2, max_stagnant=5, max_slowdown=2.0x
  Will run 100 cycles.
Daemon stopped after 100 cycles (82.45s): 8 improvement cycles, 3 deployed,
  12 audit entries, 2 converged, fully_converged=false

Key metrics:

• improvement_cycles – how many times the daemon attempted improvement
• components_deployed – how many improved components were accepted
• audit_entries – total audit trail entries
• converged_components – components that reached a local optimum
• fully_converged – whether all components have converged

Step 8: Audit Trail

Every deployment action is recorded in the audit trail:

• Action type – Deploy, Rollback, Inspect
• Component name – which component was affected
• Before/after metrics – latency, correctness score
• Timestamp – when the action occurred

The daemon persists state to .iris-daemon/ in the current directory, enabling restart with preserved history.

Program Patterns

Self-Modifying Programs

IRIS programs can inspect and modify their own graph at runtime. Here, test_cases is a tuple of (input, expected_output) pairs that the program uses to score itself and its modifications:

-- test_cases: ((1, 1), (2, 4), (3, 9), ...)
-- Each pair is (input, expected_output).
let self_improve test_cases : Tuple -> Int =
  let program = self_graph () in           -- capture own graph
  let score = graph_eval program test_cases in
  let root = graph_get_root program in
  let modified = graph_set_prim_op program root 0x02 in  -- try mul
  let new_score = graph_eval modified test_cases in
  if new_score > score then new_score      -- keep if better
  else score

Running it:

iris run self_improve.iris '((1,1),(2,4),(3,9),(4,16))'

Capability-Restricted Modules

Control what effects your module can perform. This module can read any file and write under /tmp/, but cannot open network connections, spawn threads, or execute native code:

allow [FileRead, FileWrite "/tmp/*"]
deny [TcpConnect, ThreadSpawn, MmapExec]

-- Read a file and return its contents.
-- path: file path string, e.g., "/tmp/data.txt"
let process path : String -> Bytes =
  let h = file_open path "r" in
  let data = file_read_bytes h 4096 in
  let _ = file_close h in
  data

iris run process.iris "/tmp/data.txt"

Concurrent Programs

Spawn threads that each execute a program and collect their results:

-- Run two copies of a computation in parallel.
-- n: input value passed to both threads
let parallel_square n : Int -> Tuple =
  let half = n / 2 in
  let h1 = thread_spawn (self_graph ()) in  -- thread 1: runs this program
  let h2 = thread_spawn (self_graph ()) in  -- thread 2: runs this program
  let r1 = thread_join h1 in
  let r2 = thread_join h2 in
  (r1, r2)

iris run parallel_square.iris 42
# Output: (42, 42)  -- both threads compute the same result

FFI Integration

Call C functions from IRIS via ffi_call "library" "function" (args):

-- Call libc functions: getpid() and time(NULL)
let main : Tuple =
  let pid = ffi_call "libc" "getpid" () in    -- returns process ID
  let time = ffi_call "libc" "time" (0) in    -- returns Unix timestamp
  (pid, time)

iris run ffi_example.iris
# Output: (12345, 1711234567)