Skip to main content

WEIGHT_CHECK

Constant WEIGHT_CHECK 

Source
pub const WEIGHT_CHECK: &str = "CHECK (weight >= 0.0 AND weight < 9e999 AND typeof(weight) = \'real\')";
Expand description

Table-level CHECK on links.weight (§4.7, T2.1, D-083).

Three clauses. Only the first is the one the item asked for; the other two were found by probing what the first still admits.

weight >= 0.0 is the item as written: shortest-path analytics are unsound over negative weights, so Dijkstra and A* refuse the graph at load time (D-039). Until now that refusal was the only place the property was enforced, which made it §4.7’s one genuinely open gap — a database this crate wrote by itself could hold a row this crate would not read back.

typeof(weight) = 'real' closes a hole the item does not mention and which probing found. REAL in SQLite is an affinity, not a type: values that can be converted are, and values that cannot are stored as they came. 'abc' cannot become a number, so it is stored as TEXT — and in SQLite’s type ordering every text value sorts above every numeric one, so 'abc' >= 0.0 is true and the first clause passes it through.

That is not a wrong answer on the read side. It is a panic: reading a text weight as f64 reaches unreachable!("invalid value type") inside libsql 0.9.30, in whatever unrelated query first touches the row. Measured, not reasoned about — see examples/weight_check_probe.rs.

The clause costs one typeof per insert and refuses nothing legitimate: 3, '5' and 1.0 all arrive as REAL through affinity conversion and pass. It is taken now rather than in a later rung because SQLite has no ADD CONSTRAINT — every clause added later costs another full rebuild of the largest table in the schema.

weight < 9e999 refuses +∞, and the reason is not the one anybody predicted. The plan expected the CHECK to admit infinity and argued the loader guard would catch it; the guard tests < 0.0 and is_nan(), so it does not. The next guess — mine — was that this is harmless, since IEEE infinity propagates through addition and stays totally ordered, leaving Dijkstra terminating with “that edge is unusable”: an odd answer, not a wrong one.

Both were wrong, and a test found it. An infinite weight makes the transaction log unreplayable. The log trigger serialises the row to JSON, and JSON has no representation for infinity, so the payload round-trips into ReplayCorrupt { reason: "number out of range" } — every later reconstruct() fails, including the one close() performs. The ledger is the source of truth under Doctrine III, so a value that cannot survive the log is not an eccentric weight, it is a corrupt one.

9e999 is the idiom because SQLite has no isinf: the literal overflows to +∞ on parse, and inf < inf is false. Finite values, including 1e308, pass.

The loader guard still stays, for the reason the constraint cannot cover: links_current carries no CHECK, and neither do cold files created before this rung.