csvstats
A hand-written module exercising the formats: a module header, two types
(Row, ParseError), and three functions (parse_row, mean, median). Not every definition has every layer — median is the
only one carried through all three (.tr → .soil → .lock); _module,
row, and parse_row have .tr + .lock; parse_error and mean are
spec-only. The canonical files live in
examples/csvstats/;
these are included verbatim.
_module (module header: .tr + .lock)
_module.tr
---
name: csvstats
---
# csvstats
Reads rows of decimal numbers from CSV lines and computes summary
statistics. The parsing functions own input validation; the statistics
functions assume validated `Row` values and stay total.
```exports
parse_row
median
mean
type Row
type ParseError
```
_module.lock
{
"lock_format": 1,
"name": "csvstats",
"kind": "module",
"versions": { "trellis": "0.1", "soil": "0.1" },
"spec": {
"provenance": "human",
"hashes": {
"formal": "sha256:1c9be044",
"test": null,
"prose": "sha256:73a0d5f2"
},
"prose_state": "fresh",
"blocks": [
{ "block": "exports", "author": "human" }
],
"pinned": false,
"escape_hatches": []
},
"checks": {
"exports": "ok"
},
"accepted": false
}
row (type: .tr + .lock)
row.tr
---
name: Row
---
# Row
One parsed CSV row. Construction goes through `parse_row` or row literals;
every row has at least one cell.
```soil-type
type Row = { cells : List F64 }
```
```invariant
non-empty: len(self.cells) > 0
```
row.lock
{
"lock_format": 1,
"name": "Row",
"kind": "type",
"versions": { "trellis": "0.1", "soil": "0.1" },
"spec": {
"provenance": "human",
"hashes": {
"formal": "sha256:4d7e02c9",
"test": null,
"prose": "sha256:88b1f6a3"
},
"prose_state": "fresh",
"blocks": [
{ "block": "soil-type", "author": "human" },
{ "block": "invariant", "author": "human" }
],
"pinned": false,
"escape_hatches": []
},
"cycle_hash": null,
"checks": {
"types": "ok",
"invariants": "proven",
"demoted": []
},
"tests": [
{ "name": "invariant non-empty", "tier": "property", "mode": "sandboxed", "origin": "derived", "result": "pass" }
],
"accepted": true
}
parse_error (type: .tr only)
parse_error.tr
---
name: ParseError
---
# ParseError
Why a CSV line failed to parse. `BadCell` carries the zero-based index of
the offending cell and its raw text.
```soil-type
type ParseError =
| EmptyLine
| BadCell { index : U64, text : Utf8 }
```
parse_row (function: .tr + .lock)
parse_row.tr
---
name: parse_row
tags: [parser]
---
# parse_row
Parses one CSV line of decimal numbers into a `Row`. Cells are separated by
commas; surrounding whitespace in a cell is ignored. An empty line, or any
cell that is not a decimal number, is an error.
```soil-sig
parse_row : (line : Utf8) -> Result Row ParseError
```
```test happy-path
("1.0,2.5,3.0") => {"tag": "Ok", "value": {"cells": [1.0, 2.5, 3.0]}}
(" 4.0 , 5.0") => {"tag": "Ok", "value": {"cells": [4.0, 5.0]}}
```
```test errors
("") => {"tag": "Err", "value": {"tag": "EmptyLine"}}
("1.0,x,3.0") => {"tag": "Err", "value": {"tag": "BadCell", "value": {"index": 1, "text": "x"}}}
```
Scientific notation is a known gap, blocked on deciding the cell grammar:
```test scientific-notation xfail
("1e3") => {"tag": "Ok", "value": {"cells": [1000.0]}}
```
parse_row.lock
{
"lock_format": 1,
"name": "parse_row",
"kind": "function",
"versions": { "trellis": "0.1", "soil": "0.1" },
"spec": {
"provenance": "human",
"hashes": {
"formal": "sha256:b3e91c07",
"test": "sha256:6a2f88d1",
"prose": "sha256:12c4a9ee"
},
"prose_state": "fresh",
"blocks": [
{ "block": "soil-sig", "author": "agent" },
{ "block": "test happy-path", "author": "human" },
{ "block": "test errors", "author": "human" },
{ "block": "test scientific-notation", "author": "human" }
],
"pinned": false,
"escape_hatches": []
},
"lowering": {
"soil_hash": "sha256:f00d3c21",
"provenance": "agent",
"provider": "claude-code",
"model": "claude-opus-4-7",
"private_helpers": [
{ "name": "_parse_cell", "hash": "sha256:3fe210bb" }
],
"calls": [
{ "name": "utf8_split", "hash": "sha256:91d0aa47" },
{ "name": "utf8_trim", "hash": "sha256:207cbe55" }
]
},
"checks": {
"types": "ok",
"refinements": "none",
"demoted": []
},
"tests": [
{ "name": "happy-path#1", "tier": "expect", "mode": "sandboxed", "origin": "spec", "result": "pass" },
{ "name": "happy-path#2", "tier": "expect", "mode": "sandboxed", "origin": "spec", "result": "pass" },
{ "name": "errors#1", "tier": "expect", "mode": "sandboxed", "origin": "spec", "result": "pass" },
{ "name": "errors#2", "tier": "expect", "mode": "sandboxed", "origin": "spec", "result": "pass" },
{ "name": "scientific-notation#1", "tier": "expect", "mode": "sandboxed", "origin": "spec", "result": "xfail" }
],
"oracles": [],
"accepted": false
}
mean (function: .tr only)
mean.tr
---
name: mean
---
The arithmetic mean of a non-empty list of floats.
```test simple
([1.0, 2.0, 3.0]) => 2.0
```
median (function: .tr + .soil + .lock)
median.tr
---
name: median
---
# median
Returns the median of a non-empty list of floats. For an even number of
elements, returns the mean of the two middle elements.
```soil-sig
median : (xs : List F64) -> F64
```
```requires
non-empty: len(xs) > 0
```
```ensures
lower bound: min(xs) <= result
upper bound: result <= max(xs)
```
The reference implementation wraps `statistics.median` from the Python
standard library.
```reference
ref/stats.py::median
```
```test odd-length
([1.0, 3.0, 2.0]) => 2.0
```
```test even-length
([1.0, 2.0, 3.0, 4.0]) => 2.5
```
```test single
([42.0]) => 42.0
```
```property order-independent
forall xs : List F64 where len(xs) > 0
median(xs) == median(reverse(xs))
```
median.soil
median : (xs : {v : List F64 | len v > 0}) -> {r : F64 | min xs <= r and r <= max xs}
median xs =
let sorted = sort_by (fun x -> x) xs in
let n = len sorted in
let mid = n / 2 in
if n % 2 == 1
then nth sorted mid
else (nth sorted (mid - 1) + nth sorted mid) / 2.0
median.lock
{
"lock_format": 1,
"name": "median",
"kind": "function",
"versions": { "trellis": "0.1", "soil": "0.1" },
"spec": {
"provenance": "human",
"hashes": {
"formal": "sha256:9f2c41aa",
"test": "sha256:41aa73c0",
"prose": "sha256:c8172d99"
},
"prose_state": "fresh",
"blocks": [
{ "block": "soil-sig", "author": "human" },
{ "block": "requires", "author": "human" },
{ "block": "ensures", "author": "human" },
{ "block": "reference", "author": "human" },
{ "block": "test odd-length", "author": "human" },
{ "block": "test even-length", "author": "human" },
{ "block": "test single", "author": "human" },
{ "block": "property order-independent", "author": "human" }
],
"pinned": true,
"escape_hatches": []
},
"lowering": {
"soil_hash": "sha256:77b04e12",
"provenance": "agent",
"provider": "claude-code",
"model": "claude-opus-4-7",
"private_helpers": [],
"calls": [
{ "name": "sort_by", "hash": "sha256:aa90b1f3" },
{ "name": "len", "hash": "sha256:0d33c2e8" },
{ "name": "nth", "hash": "sha256:6b1e94d7" }
]
},
"checks": {
"types": "ok",
"refinements": "proven",
"demoted": []
},
"tests": [
{ "name": "odd-length#1", "tier": "expect", "mode": "sandboxed", "origin": "spec", "result": "pass" },
{ "name": "even-length#1", "tier": "expect", "mode": "sandboxed", "origin": "spec", "result": "pass" },
{ "name": "single#1", "tier": "expect", "mode": "sandboxed", "origin": "spec", "result": "pass" },
{ "name": "order-independent", "tier": "property", "mode": "sandboxed", "origin": "spec", "result": "pass" },
{ "name": "ensures lower bound", "tier": "property", "mode": "sandboxed", "origin": "derived", "result": "pass" },
{ "name": "ensures upper bound", "tier": "property", "mode": "sandboxed", "origin": "derived", "result": "pass" },
{ "name": "differential ref/stats.py::median", "tier": "differential", "mode": "sandboxed", "origin": "derived", "result": "pass" }
],
"oracles": [
{ "kind": "reference", "path": "ref/stats.py::median", "hash": "sha256:5e8f0b2a" }
],
"accepted": true
}