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.0", "soil": "0.1" },
  "spec": {
    "provenance": "human",
    "hashes": {
      "formal": "sha256:4f523045c3a5c366ee4d455053150edda848a78e66028785b13f9a7dedfda790",
      "test": null,
      "prose": "sha256:ab30ca95085f61fa4f5af771b61e0a36cd316e93356b50ba6e54fcbceaf69730"
    },
    "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.0", "soil": "0.1" },
  "spec": {
    "provenance": "human",
    "hashes": {
      "formal": "sha256:36af0f58e2bd320599cdcced097bf362d82842a7000b7fcf878ca04005cdd5f8",
      "test": null,
      "prose": "sha256:1334d065c2a08b423f5a99a2c417fda1915967977e42b7c79c16e0fb2ec8e282"
    },
    "prose_state": "fresh",
    "blocks": [
      { "block": "soil-type", "author": "human" },
      { "block": "invariant", "author": "human" }
    ],
    "pinned": false,
    "escape_hatches": []
  },
  "checks": {
    "types": "ok",
    "invariants": {
      "non-empty": "runtime"
    }
  },
  "tests": [],
  "cycle_hash": null,
  "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 : I64, 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.0", "soil": "0.1" },
  "spec": {
    "provenance": "human",
    "hashes": {
      "formal": "sha256:bf4c9b19e1ca0e7050768a3cf2b707acb7c3b30bbce5eebd34a0fe57955e584d",
      "test": "sha256:f234b5385d86dc133a6e40652bf95789ce50a98e832822865f26733500c2edc2",
      "prose": "sha256:5ba26adaea0a1d2f2e5a5042570f2c83f167041d289cc5cae6dbd8ad228149bd"
    },
    "prose_state": "fresh",
    "blocks": [
      { "block": "soil-sig", "author": "human" },
      { "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:c3f99d99d11fa4352ff1f9f252f5933ae28cd4f278ac0a5b6ce971c411407391",
    "provenance": "human-verified",
    "provider": null,
    "model": null,
    "private_helpers": [
      { "name": "_parse_cell", "hash": "sha256:fbbc9e37d86ec7298fd1ac46213aa6fc7cb19c208963fcad8381c110f1eb1a24" }
    ],
    "calls": [],
    "decisions": {
      "scope_hash": "sha256:af5570f5a1810b7af78caf4bc70a660f0df51e42baf91d4de5b2328de0e83dfc",
      "applied": []
    }
  },
  "checks": {
    "types": "ok",
    "termination": "unverified",
    "refinements": {},
    "holes": 0
  },
  "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 finite floats. For an even
number of elements, returns the mean of the two middle elements. The
bounds below need the all-finite domain: the mean of middles `-Inf`
and `+Inf` is `NaN`, which sorts *after* `+Inf` in Soil's total order
on `F64` (design §3.7) and so escapes `result <= max(xs)`.

```soil-sig
median : (xs : List F64) -> F64
```

```requires
non-empty: len(xs) > 0
all-finite: all_finite xs
```

```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
```

Sorting first never changes the answer, and under the total order this
holds for *every* non-empty list — even `NaN`-bearing ones, since both
sides reduce to the same middles of the same sorted list.

```property sort-invariant
forall xs : List F64
len(xs) > 0 implies median (sort xs) == median xs
```

median.soil

median : (xs : {v : List F64 | len v > 0 and all_finite v}) -> {r : F64 | min xs <= r and r <= max xs}
median xs =
  let ordered = sort xs in
  let n = len ordered in
  let mid = n / 2 in
  if n % 2 == 1
  then nth ordered mid
  else
    let a = nth ordered (mid - 1) in
    let b = nth ordered mid in
    let s = a + b in
    if s - s == 0.0
    then s / 2.0
    else a / 2.0 + b / 2.0

median.lock

{
  "lock_format": 1,
  "name": "median",
  "kind": "function",
  "versions": { "trellis": "0.1.0", "soil": "0.1" },
  "spec": {
    "provenance": "human",
    "hashes": {
      "formal": "sha256:8efa23f9ee5e01193b92be29c015233544916d41e0957938a721d5ee9d706a43",
      "test": "sha256:63929b6a73266fabd7ec20a7c54389b5a463e91780d40facdd3bc7b84f836800",
      "prose": "sha256:51f17924a3f698e3d6c289ee0fb8946d8cad30d5ee8ecc603c34fe736d3a75d3"
    },
    "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 sort-invariant", "author": "human" }
    ],
    "pinned": true,
    "escape_hatches": []
  },
  "lowering": {
    "soil_hash": "sha256:2ab06f664670b3982b5a1dbbb2213cabc4d4f61aa1174f685aa2f6fe5fd901a7",
    "provenance": "human-verified",
    "provider": null,
    "model": null,
    "private_helpers": [],
    "calls": [
      { "name": "len", "hash": "sha256:1d0db7042147887e451444fd609243b27aabb1fd18bfe3fb678823dc2f1e1d8e" },
      { "name": "nth", "hash": "sha256:d32fd45ca339a7f7cc735e362a3e2621dbd451c2f732fc06f0de82e63e4a9c7c" },
      { "name": "sort", "hash": "sha256:ecb7c98a9c4fbcc3a802c3c224067136fc92df2c39bb7501277ee82c759a8188" }
    ],
    "decisions": {
      "scope_hash": "sha256:af5570f5a1810b7af78caf4bc70a660f0df51e42baf91d4de5b2328de0e83dfc",
      "applied": []
    }
  },
  "checks": {
    "types": "ok",
    "termination": "verified",
    "refinements": {
      "all-finite": "runtime",
      "lower bound": "runtime",
      "non-empty": "runtime",
      "upper bound": "runtime"
    },
    "holes": 0
  },
  "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": "sort-invariant", "tier": "property", "mode": "sandboxed", "origin": "spec", "result": "pass" },
    { "name": "derived:ensures:lower bound", "tier": "property", "mode": "sandboxed", "origin": "derived", "result": "pass" },
    { "name": "derived:ensures:upper bound", "tier": "property", "mode": "sandboxed", "origin": "derived", "result": "pass" },
    { "name": "derived:differential:ref/stats.py::median", "tier": "differential", "mode": "sandboxed", "origin": "derived", "result": "pass" }
  ],
  "oracles": [
    { "kind": "reference", "path": "ref/stats.py::median", "hash": "sha256:4c6a37d371476edb8bb5beb89290908c19a7f8a8c10adf5d4fa8bffd32617242" }
  ],
  "accepted": true
}