Problem / current limitation
SEP-0004 specifies cost expressions with +, *, ^const, log, max, min, and projection-style measures such as len(xs). The implementation exposes a richer internal sporec_typeck::cost::CostExpr, but the parser AST only accepts literals, variables, and O(n)/linear notation, so user-written cost clauses cannot express the SEP grammar.
Evidence
spore-evolution/seps/SEP-0004-cost-analysis.md:19 and :31 require +, *, ^const, log, max, and min.spore-evolution/seps/SEP-0004-cost-analysis.md:116-121 shows cost <= len(list) * log(len(list)) * 5 + len(list).crates/sporec-parser/src/ast.rs:198-206 limits parser-level CostExpr to Literal, Var, and Linear.crates/sporec-typeck/src/cost.rs:12-29 already defines the target internal expression variants.crates/sporec-typeck/src/cost.rs:598-605 drops parser cost clauses into the limited internal subset.
Target behavior
Users can write the SEP-0004 cost grammar in signatures, including arithmetic composition, log, max, min, exponent-by-constant, and simple projections such as len(xs) / xs.len where supported by syntax. The type checker preserves those expressions in cost vectors and diagnostics.
Acceptance tests
- Parser tests accept cost clauses for
n + 1, n * log(n), max(len(xs), 1), min(a, b), and n^2/the selected exponent syntax.
- Type-checker tests verify the parsed expression is preserved in
CostResult::Declared and CostVector.
- CLI JSON/check output prints the declared symbolic cost without degrading it to a placeholder.
- Negative parser tests reject division, subtraction, conditionals, and non-constant exponents in cost expressions.
Release priority
P1 / language correctness before broader cost-contract adoption
Problem / current limitation
SEP-0004 specifies cost expressions with
+,*,^const,log,max,min, and projection-style measures such aslen(xs). The implementation exposes a richer internalsporec_typeck::cost::CostExpr, but the parser AST only accepts literals, variables, andO(n)/linear notation, so user-written cost clauses cannot express the SEP grammar.Evidence
spore-evolution/seps/SEP-0004-cost-analysis.md:19and:31require+,*,^const,log,max, andmin.spore-evolution/seps/SEP-0004-cost-analysis.md:116-121showscost <= len(list) * log(len(list)) * 5 + len(list).crates/sporec-parser/src/ast.rs:198-206limits parser-levelCostExprtoLiteral,Var, andLinear.crates/sporec-typeck/src/cost.rs:12-29already defines the target internal expression variants.crates/sporec-typeck/src/cost.rs:598-605drops parser cost clauses into the limited internal subset.Target behavior
Users can write the SEP-0004 cost grammar in signatures, including arithmetic composition,
log,max,min, exponent-by-constant, and simple projections such aslen(xs)/xs.lenwhere supported by syntax. The type checker preserves those expressions in cost vectors and diagnostics.Acceptance tests
n + 1,n * log(n),max(len(xs), 1),min(a, b), andn^2/the selected exponent syntax.CostResult::DeclaredandCostVector.Release priority
P1 / language correctness before broader cost-contract adoption