Move DataType into internal/datatype, aliased by the root, and what a proof knows of a value into internal/proven

builtins.go

@@ -9,6 +9,7 @@ import (
 	"strings"
 
 	"github.com/larvit/fejkdata/internal/drawstate"
+	"github.com/larvit/fejkdata/internal/proven"
 )
 
 // maxLen caps sample output lengths (hex, nanoid, base64, digits, upper, lower)
@@ -20,9 +21,6 @@ const (
 	maxDecimals = 1024
 )
 
-// shortestDecimals prints the fewest digits that read back as the same float64.
-const shortestDecimals = -1
-
 // builtins is the registry of {name(args)} functions. Derivations read the digits
 // emitted so far in the current expansion (place them after their payload);
 // samples read only the rng. A time-based id (uuid v7, ulid) draws its timestamp
@@ -35,8 +33,8 @@ var builtins = withTransforms(map[string]builtin{
 	"ulid":   {arity: 0, prep: sample(ulid)},
 	"nanoid": {arity: 1, checkArgs: posIntArg, prep: chars(nanoidAlphabet)},
 	"hex":    {arity: 1, checkArgs: posIntArg, prep: chars(hexDigits)},
-	"digits": {arity: 1, checkArgs: posIntArg, prep: chars("0123456789"), prints: DataTypeString, proveNumber: func(token string, prints DataType, a []string) proven {
+	"digits": {arity: 1, checkArgs: posIntArg, prep: chars("0123456789"), prints: DataTypeString, proveNumber: func(token string, prints DataType, a []string) proven.Value {
-		return printing(token, prints, bounded(0, math.Pow(10, float64(atoi(a[0])))-1, true))
+		return proven.Printing(token, prints, proven.Bounded(0, math.Pow(10, float64(atoi(a[0])))-1, true))
 	}},
 	"upper": {arity: 1, checkArgs: posIntArg, prep: chars("ABCDEFGHIJKLMNOPQRSTUVWXYZ")},
 	"lower": {arity: 1, checkArgs: posIntArg, prep: chars("abcdefghijklmnopqrstuvwxyz")},
@@ -49,16 +47,16 @@ var builtins = withTransforms(map[string]builtin{
 	"int": {arity: 2, checkArgs: intRangeArgs, prep: func(a []string) callFn {
 		lo, span := atoi(a[0]), atoi(a[1])-atoi(a[0])+1
 		return func(s *drawstate.State, _ string, _ []string) string { return strconv.Itoa(lo + s.IntN(span)) }
-	}, prints: DataTypeInteger, proveNumber: func(token string, prints DataType, a []string) proven {
+	}, prints: DataTypeInteger, proveNumber: func(token string, prints DataType, a []string) proven.Value {
-		return printing(token, prints, bounded(float64(atoi(a[0])), float64(atoi(a[1])), true))
+		return proven.Printing(token, prints, proven.Bounded(float64(atoi(a[0])), float64(atoi(a[1])), true))
 	}},
 	"float": {arity: 3, checkArgs: floatArgs, prep: func(a []string) callFn {
 		lo, hi, dp := atof(a[0]), atof(a[1]), atoi(a[2])
 		return func(s *drawstate.State, _ string, _ []string) string {
 			return formatFloat(lo+s.Float64()*(hi-lo), dp)
 		}
-	}, prints: DataTypeNumber, proveNumber: func(token string, _ DataType, a []string) proven {
+	}, prints: DataTypeNumber, proveNumber: func(token string, _ DataType, a []string) proven.Value {
-		return printedNumber(token, bounded(atof(a[0]), atof(a[1]), false), atoi(a[2]))
+		return proven.PrintedNumber(token, proven.Bounded(atof(a[0]), atof(a[1]), false), atoi(a[2]))
 	}},
 	"iban": {arity: 1, checkArgs: ibanArg, prep: func(a []string) callFn {
 		cc := a[0]
@@ -78,8 +76,8 @@ var builtins = withTransforms(map[string]builtin{
 		return func(s *drawstate.State, _ string, _ []string) string {
 			return strconv.FormatUint(s.Seq(key), 10)
 		}
-	}, prints: DataTypeInteger, proveNumber: func(token string, prints DataType, _ []string) proven {
+	}, prints: DataTypeInteger, proveNumber: func(token string, prints DataType, _ []string) proven.Value {
-		return printing(token, prints, bounded(1, math.MaxInt64, true))
+		return proven.Printing(token, prints, proven.Bounded(1, math.MaxInt64, true))
 	}},
 })
 

builtins_test.go

@@ -8,7 +8,6 @@ import (
 	"strings"
 	"testing"
 	"time"
-
 )
 
 func TestBuiltinIDGenerators(t *testing.T) {

calc.go

@@ -9,6 +9,7 @@ import (
 
 	"github.com/larvit/fejkdata/internal/drawstate"
 	"github.com/larvit/fejkdata/internal/grammar"
+	"github.com/larvit/fejkdata/internal/proven"
 )
 
 // evalCalc evaluates an expression over the operand values expand already read, so it
@@ -218,12 +219,12 @@ func parsedCalc(expr string) grammar.Calc {
 	return c
 }
 
-// calcDecimals is a calc's decimals count, or shortestDecimals where it names none.
+// calcDecimals is a calc's decimals count, or proven.ShortestDecimals where it names none.
 func calcDecimals(args []string) int {
 	if len(args) == 2 {
 		return atoi(args[1])
 	}
-	return shortestDecimals
+	return proven.ShortestDecimals
 }
 
 // calcOperands lists the operands a calc's args read, fields or names. checkCalc reports

datatype.go

@@ -3,32 +3,21 @@ package fejkdata
 import (
 	"errors"
 	"fmt"
+
+	"github.com/larvit/fejkdata/internal/datatype"
 )
 
 // DataType is what a record column holds, which decides how a record writes its value.
-type DataType int
+type DataType = datatype.DataType
 
 // The datatypes a column declares with "datatype"; a column without one is a string.
 const (
-	DataTypeString DataType = iota
+	DataTypeString  = datatype.String
-	DataTypeInteger
+	DataTypeInteger = datatype.Integer
-	DataTypeNumber
+	DataTypeNumber  = datatype.Number
-	DataTypeBoolean
+	DataTypeBoolean = datatype.Boolean
 )
 
-var (
-	dataTypeNames = [...]string{"string", "integer", "number", "boolean"}
-	dataTypeNouns = [...]string{"text", "an integer", "a number", "a boolean"}
-)
-
-// String is the datatype as data spells it.
-func (d DataType) String() string {
-	if d < 0 || int(d) >= len(dataTypeNames) {
-		return fmt.Sprintf("DataType(%d)", int(d))
-	}
-	return dataTypeNames[d]
-}
-
 // position is where a JSON value sits, which decides whether it may carry a datatype or
 // be null.
 type position int
@@ -174,7 +163,7 @@ func disagreement(a *template, da DataType, b *template, db DataType) error {
 		fix, other, want = b, a, da
 	}
 	held := fmt.Sprintf("its items hold %s and %s; a column holds one datatype", da, db)
-	fits := (&valueProof{}).proveColumnItem(fix).not[want] == ""
+	fits := (&valueProof{}).proveColumnItem(fix).Not[want] == ""
 	switch kindOf(fix) {
 	case kindDeclares:
 		return errors.New(held)
@@ -189,7 +178,7 @@ func disagreement(a *template, da DataType, b *template, db DataType) error {
 			panic(internalError("two text items hold one datatype, so they never disagree"))
 		case kindReads:
 			if !fits {
-				return fmt.Errorf(`item %q is not %s, the datatype item %q takes from the column it reads; to read that column as text, %s`, fix.format, dataTypeNouns[want], other.format, asText(other))
+				return fmt.Errorf(`item %q is not %s, the datatype item %q takes from the column it reads; to read that column as text, %s`, fix.format, datatype.Noun(want), other.format, asText(other))
 			}
 		}
 		if fix.fromString { // an object may carry a weight, which this spelling would drop

format.go

@@ -6,6 +6,7 @@ import (
 
 	"github.com/larvit/fejkdata/internal/drawstate"
 	"github.com/larvit/fejkdata/internal/grammar"
+	"github.com/larvit/fejkdata/internal/proven"
 )
 
 // builtin is a format-string function invoked as {name(args)}. It receives the
@@ -27,7 +28,7 @@ type builtin struct {
 	// proveNumber bounds the number a call's text reads as, token its body, and says which
 	// datatypes that text is not; set it where every render reads as a finite number, which
 	// makes the call a calc operand, and leave it nil otherwise.
-	proveNumber func(token string, prints DataType, args []string) proven
+	proveNumber func(token string, prints DataType, args []string) proven.Value
 	// prints is the datatype a call's text is, handed to proveNumber: DataTypeString where it
 	// reads as a number no column should type, as digits' leading zeros; unset where
 	// proveNumber is nil.

internal/datatype/datatype.go

@@ -0,0 +1,34 @@
+// Package datatype names what a record column holds.
+package datatype
+
+import "fmt"
+
+// DataType is what a record column holds, which decides how a record writes its value.
+type DataType int
+
+// The datatypes a column declares with "datatype"; a column without one is a string.
+const (
+	String DataType = iota
+	Integer
+	Number
+	Boolean
+)
+
+// Count is the number of datatypes, for an array indexed by one.
+const Count = len(names)
+
+var (
+	names = [...]string{"string", "integer", "number", "boolean"}
+	nouns = [...]string{"text", "an integer", "a number", "a boolean"}
+)
+
+// String is the datatype as data spells it.
+func (d DataType) String() string {
+	if d < 0 || int(d) >= len(names) {
+		return fmt.Sprintf("DataType(%d)", int(d))
+	}
+	return names[d]
+}
+
+// Noun is the datatype as an error names what a value is.
+func Noun(d DataType) string { return nouns[d] }

internal/proven/proven.go

@@ -0,0 +1,209 @@
+// Package proven holds what a proof knows of every render of a value, and the arithmetic
+// that bounds a calc from its operands.
+package proven
+
+import (
+	"fmt"
+	"math"
+	"regexp"
+	"strconv"
+	"strings"
+
+	"github.com/larvit/fejkdata/internal/datatype"
+	"github.com/larvit/fejkdata/internal/grammar"
+)
+
+// Value is what a proof knows of every render of a node: bounds on the number each
+// reads as, and per datatype why some render's text is not one ("" when none).
+type Value struct {
+	Lo, Hi     float64
+	NonZero    float64 // every value is at least this far from zero; 0 when one can be zero
+	Integral   bool
+	NotOperand string // why some render reads as no finite number, the way calc reads it
+	Not        [datatype.Count]string
+	Nullable   bool // some draw of a column is null
+}
+
+// ShortestDecimals prints the fewest digits that read back as the same float64.
+const ShortestDecimals = -1
+
+// limit is the largest magnitude a proof accepts as finite, far enough below
+// math.MaxFloat64 that rounding in the bounds cannot hide an overflow.
+const limit = 1e300
+
+// Or is what a proof knows of a render that is either v or w.
+func (v Value) Or(w Value) Value {
+	v.Lo, v.Hi, v.NonZero = min(v.Lo, w.Lo), max(v.Hi, w.Hi), min(v.NonZero, w.NonZero)
+	v.Integral, v.Nullable = v.Integral && w.Integral, v.Nullable || w.Nullable
+	if v.NotOperand == "" {
+		v.NotOperand = w.NotOperand
+	}
+	for d := range v.Not {
+		if v.Not[d] == "" {
+			v.Not[d] = w.Not[d]
+		}
+	}
+	return v
+}
+
+// Calc bounds a calc expression from its operands, or says why it cannot.
+func Calc(expr grammar.CalcNode, operand func(name string) Value) (Value, string) {
+	v, doubt := bound(expr, operand)
+	if doubt == "" && !(magnitude(v) <= limit) {
+		doubt = grammar.CalcText(expr) + " is not proven within 1e300"
+	}
+	return v, doubt
+}
+
+func bound(n grammar.CalcNode, operand func(name string) Value) (Value, string) {
+	switch n := n.(type) {
+	case grammar.CalcNum:
+		v := float64(n)
+		return Bounded(v, v, v == math.Trunc(v)), ""
+	case grammar.CalcVar:
+		v := operand(n.Name)
+		if v.NotOperand != "" {
+			return Value{}, fmt.Sprintf("operand %q: %s", n.Name, v.NotOperand)
+		}
+		return Value{Lo: v.Lo, Hi: v.Hi, NonZero: v.NonZero, Integral: v.Integral}, ""
+	case grammar.CalcNeg:
+		v, doubt := bound(n.X, operand)
+		v.Lo, v.Hi = -v.Hi, -v.Lo
+		return v, doubt
+	case grammar.CalcBin:
+		l, doubt := bound(n.L, operand)
+		if doubt != "" {
+			return l, doubt
+		}
+		r, doubt := bound(n.R, operand)
+		if doubt != "" {
+			return r, doubt
+		}
+		return combine(n, l, r)
+	}
+	panic(fmt.Sprintf("fejkdata: internal error: calc node %T has no bound", n))
+}
+
+// combine bounds one operation from the bounds of its sides.
+func combine(n grammar.CalcBin, l, r Value) (Value, string) {
+	var v Value
+	integral := l.Integral && r.Integral
+	switch n.Operator {
+	case '+':
+		v = Bounded(l.Lo+r.Lo, l.Hi+r.Hi, integral)
+	case '-':
+		v = Bounded(l.Lo-r.Hi, l.Hi-r.Lo, integral)
+	case '*':
+		v = Bounded(min(l.Lo*r.Lo, l.Lo*r.Hi, l.Hi*r.Lo, l.Hi*r.Hi), max(l.Lo*r.Lo, l.Lo*r.Hi, l.Hi*r.Lo, l.Hi*r.Hi), integral)
+		v.NonZero = max(v.NonZero, l.NonZero*r.NonZero)
+	default:
+		if r.NonZero == 0 {
+			return v, fmt.Sprintf("divides by %s, which is not proven nonzero", grammar.CalcText(n.R))
+		}
+		m := magnitude(l) / r.NonZero
+		v = Value{Lo: -m, Hi: m, NonZero: l.NonZero / magnitude(r)}
+	}
+	if !(magnitude(v) <= limit) {
+		return v, grammar.CalcText(n) + " is not proven within 1e300"
+	}
+	return v, ""
+}
+
+// Bounded is a number in [lo, hi], its distance from zero read off the bounds.
+func Bounded(lo, hi float64, integral bool) Value {
+	v := Value{Lo: lo, Hi: hi, Integral: integral}
+	switch {
+	case lo > 0:
+		v.NonZero = lo
+	case hi < 0:
+		v.NonZero = -hi
+	}
+	return v
+}
+
+func magnitude(v Value) float64 { return math.Max(math.Abs(v.Lo), math.Abs(v.Hi)) }
+
+// PrintedNumber is what a token printing v to dp decimals holds.
+func PrintedNumber(token string, v Value, dp int) Value {
+	if dp == ShortestDecimals {
+		if v.Integral { // a whole value prints with no point
+			return printedInteger(token, v)
+		}
+		return Printing(token, datatype.Number, v)
+	}
+	half, _ := strconv.ParseFloat("5e-"+strconv.Itoa(dp+1), 64)
+	v = Value{Lo: v.Lo - half, Hi: v.Hi + half, NonZero: math.Max(0, v.NonZero-half), Integral: v.Integral || dp == 0}
+	if dp == 0 {
+		return printedInteger(token, v)
+	}
+	return Printing(token, datatype.Number, v)
+}
+
+func printedInteger(token string, v Value) Value {
+	v = Printing(token, datatype.Integer, v)
+	if !(magnitude(v) < math.MaxInt64) {
+		v.Not[datatype.Integer] = fmt.Sprintf("{%s} is not proven within int64", token)
+	}
+	return v
+}
+
+// Printing is v for a token whose every render is text of datatype prints, with a reason
+// against each datatype that text is not.
+func Printing(token string, prints datatype.DataType, v Value) Value {
+	for d := datatype.Integer; d <= datatype.Boolean; d++ {
+		if prints != d && !(prints == datatype.Integer && d == datatype.Number) {
+			v.Not[d] = fmt.Sprintf("{%s} prints %s, not %s", token, datatype.Noun(prints), datatype.Noun(d))
+		}
+	}
+	return v
+}
+
+// Unproven is a render no datatype and no calc can take, for why.
+func Unproven(why string) Value {
+	v := Value{NotOperand: why}
+	for d := datatype.Integer; d <= datatype.Boolean; d++ {
+		v.Not[d] = why
+	}
+	return v
+}
+
+var (
+	integerText = regexp.MustCompile(`^-?(0|[1-9][0-9]*)$`)
+	numberText  = regexp.MustCompile(`^-?(0|[1-9][0-9]*)(\.[0-9]+)?([eE][+-]?[0-9]+)?$`)
+)
+
+// Literal proves fixed text: the number calc reads it as, and each datatype it is.
+func Literal(text string) Value {
+	var v Value
+	if f, err := strconv.ParseFloat(strings.TrimSpace(text), 64); err != nil || math.IsNaN(f) || math.IsInf(f, 0) {
+		v.NotOperand = fmt.Sprintf("%q is not a number", text)
+	} else {
+		v = Bounded(f, f, f == math.Trunc(f))
+	}
+	if _, err := strconv.ParseInt(text, 10, 64); !integerText.MatchString(text) {
+		v.Not[datatype.Integer] = fmt.Sprintf("%q is not an integer", text)
+	} else if err != nil {
+		v.Not[datatype.Integer] = fmt.Sprintf("%q is past the int64 range", text)
+	}
+	if v.NotOperand != "" || !numberText.MatchString(text) {
+		v.Not[datatype.Number] = fmt.Sprintf("%q is not a number", text)
+	}
+	if text != "true" && text != "false" {
+		v.Not[datatype.Boolean] = fmt.Sprintf("%q is not a boolean", text)
+	}
+	return signedZero(text, v)
+}
+
+// signedZero refuses a zero written with a sign as a typed value, naming it unsigned.
+func signedZero(text string, v Value) Value {
+	mantissa, _, _ := strings.Cut(strings.ToLower(text), "e")
+	if !strings.HasPrefix(text, "-") || v.NotOperand != "" || strings.Trim(mantissa, "-0.") != "" {
+		return v
+	}
+	for _, d := range []datatype.DataType{datatype.Integer, datatype.Number} {
+		if v.Not[d] == "" {
+			v.Not[d] = fmt.Sprintf("%q is zero written with a sign; write %q", text, text[1:])
+		}
+	}
+	return v
+}

struct.go

@@ -11,6 +11,7 @@ import (
 
 	"github.com/larvit/fejkdata/internal/drawstate"
 	"github.com/larvit/fejkdata/internal/grammar"
+	"github.com/larvit/fejkdata/internal/proven"
 )
 
 // FakeStruct fills the struct v points to. Each exported field tagged `fake:"…"` is a
@@ -308,14 +309,14 @@ var columnKinds = map[reflect.Kind]columnKind{
 
 // holds reports whether a field of this kind holds every value v proves. An integer prints
 // whole, so its bounds round inward first.
-func (k columnKind) holds(v proven) bool {
+func (k columnKind) holds(v proven.Value) bool {
 	switch k.datatype {
 	case DataTypeString, DataTypeBoolean:
 		return true
 	case DataTypeInteger:
-		return math.Ceil(v.lo) >= k.lo && math.Floor(v.hi) <= k.hi
+		return math.Ceil(v.Lo) >= k.lo && math.Floor(v.Hi) <= k.hi
 	}
-	return v.lo >= k.lo && v.hi <= k.hi
+	return v.Lo >= k.lo && v.Hi <= k.hi
 }
 
 // fill draws the record into v's tagged fields, then each nested struct as a record of its own.

valueproof.go

@@ -2,31 +2,18 @@ package fejkdata
 
 import (
 	"fmt"
-	"math"
 	"reflect"
-	"regexp"
 	"slices"
-	"strconv"
 	"strings"
 
 	"github.com/larvit/fejkdata/internal/grammar"
+	"github.com/larvit/fejkdata/internal/proven"
 )
 
-// proven is what a proof knows of every render of a node: bounds on the number each
-// reads as, and per datatype why some render's text is not one ("" when none).
-type proven struct {
-	lo, hi     float64
-	nonZero    float64 // every value is at least this far from zero; 0 when one can be zero
-	integral   bool
-	notOperand string // why some render reads as no finite number, the way calc reads it
-	not        [len(dataTypeNames)]string
-	nullable   bool // some draw of a column is null
-}
-
 // valueProof proves what typed columns and their calc operands hold, each node once per scope.
 type valueProof struct {
-	memo       map[node]proven
+	memo       map[node]proven.Value
-	columnMemo map[node]proven
+	columnMemo map[node]proven.Value
 }
 
 // checkDatatype rejects a typed column item some render of which is not text of its datatype,
@@ -40,7 +27,7 @@ func (p *valueProof) checkDatatype(path string, n node) error {
 	if r := t.link.readsColumn; r != nil && columnDatatype(r.column) == t.datatype {
 		return fmt.Errorf(`%s: %s takes datatype %s from the column it reads; drop "datatype"`, path, t.format, t.datatype)
 	}
-	if reason := p.proveColumnItem(t).not[t.datatype]; reason != "" {
+	if reason := p.proveColumnItem(t).Not[t.datatype]; reason != "" {
 		return fmt.Errorf("%s: datatype %s: %s", path, t.datatype, reason)
 	}
 	return nil
@@ -58,7 +45,7 @@ func (p *valueProof) checkField(label string, ft reflect.Type, column node) erro
 	elem := ft
 	if ft.Kind() == reflect.Pointer {
 		elem = ft.Elem()
-	} else if p.proveColumn(column).nullable {
+	} else if p.proveColumn(column).Nullable {
 		return fmt.Errorf("%s: its tag can draw null, which %s cannot hold; make it *%s", label, ft, ft)
 	}
 	kind := columnKinds[elem.Kind()]
@@ -67,7 +54,7 @@ func (p *valueProof) checkField(label string, ft reflect.Type, column node) erro
 	}
 	for _, it := range items {
 		v := p.proveColumnItem(it)
-		if reason := v.not[kind.datatype]; reason != "" {
+		if reason := v.Not[kind.datatype]; reason != "" {
 			return fmt.Errorf("%s (%s): %s", label, ft, reason)
 		}
 		if !kind.holds(v) {
@@ -78,7 +65,7 @@ func (p *valueProof) checkField(label string, ft reflect.Type, column node) erro
 }
 
 // proveColumnItem proves a column item: what it renders, or, when it is a column it reads, that column.
-func (p *valueProof) proveColumnItem(t *template) proven {
+func (p *valueProof) proveColumnItem(t *template) proven.Value {
 	if t.link.readsColumn == nil {
 		return p.prove(t)
 	}
@@ -87,35 +74,35 @@ func (p *valueProof) proveColumnItem(t *template) proven {
 
 // proveColumn proves a column over what its items draw, a null item marking it null rather than
 // rendering "".
-func (p *valueProof) proveColumn(n node) proven {
+func (p *valueProof) proveColumn(n node) proven.Value {
 	if v, done := p.columnMemo[n]; done {
 		return v
 	}
 	if p.columnMemo == nil {
-		p.columnMemo = map[node]proven{}
+		p.columnMemo = map[node]proven.Value{}
 	}
 	items, nullable := columnItems(n)
-	var v proven
+	var v proven.Value
 	for i, it := range items {
 		if w := p.proveColumnItem(it); i == 0 {
 			v = w
 		} else {
-			v = v.or(w)
+			v = v.Or(w)
 		}
 	}
-	v.nullable = v.nullable || nullable
+	v.Nullable = v.Nullable || nullable
 	p.columnMemo[n] = v
 	return v
 }
 
-func (p *valueProof) prove(n node) proven {
+func (p *valueProof) prove(n node) proven.Value {
 	if v, done := p.memo[n]; done {
 		return v
 	}
 	if p.memo == nil {
-		p.memo = map[node]proven{}
+		p.memo = map[node]proven.Value{}
 	}
-	var v proven
+	var v proven.Value
 	switch n := n.(type) {
 	case *choice:
 		v = p.proveUnion(n.items)
@@ -126,9 +113,9 @@ func (p *valueProof) prove(n node) proven {
 	case *table:
 		v = p.prove(n.rowNode)
 	case *tableRow:
-		v = unproven(fmt.Sprintf("%q renders a row of %s, which is composed text", n.t.formatTemplate.format, n.t.segment))
+		v = proven.Unproven(fmt.Sprintf("%q renders a row of %s, which is composed text", n.t.formatTemplate.format, n.t.segment))
 	case *nullItem:
-		v = unproven(`it reads a null, which renders "" outside its own column`)
+		v = proven.Unproven(`it reads a null, which renders "" outside its own column`)
 	default:
 		panic(internalError("prove has no case for node %T", n))
 	}
@@ -137,59 +124,44 @@ func (p *valueProof) prove(n node) proven {
 }
 
 // proveCells proves a table column over every cell it may render.
-func (p *valueProof) proveCells(c *tableColumn) proven {
+func (p *valueProof) proveCells(c *tableColumn) proven.Value {
-	var v proven
+	var v proven.Value
 	for r := 0; r < c.t.rowCount(); r++ {
-		var w proven
+		var w proven.Value
 		if cell := c.t.cellTemplate(r, c.i); cell != nil {
 			w = p.prove(cell)
 		} else {
-			w = literalValue(c.t.cell(r, c.i))
+			w = proven.Literal(c.t.cell(r, c.i))
 		}
 		if r == 0 {
 			v = w
 		} else {
-			v = v.or(w)
+			v = v.Or(w)
 		}
 	}
 	return v
 }
 
-func (p *valueProof) proveUnion(nodes []node) proven {
+func (p *valueProof) proveUnion(nodes []node) proven.Value {
 	v := p.prove(nodes[0])
 	for _, n := range nodes[1:] {
-		v = v.or(p.prove(n))
+		v = v.Or(p.prove(n))
-	}
-	return v
-}
-
-// or is what a proof knows of a render that is either v or w.
-func (v proven) or(w proven) proven {
-	v.lo, v.hi, v.nonZero = min(v.lo, w.lo), max(v.hi, w.hi), min(v.nonZero, w.nonZero)
-	v.integral, v.nullable = v.integral && w.integral, v.nullable || w.nullable
-	if v.notOperand == "" {
-		v.notOperand = w.notOperand
-	}
-	for d := range v.not {
-		if v.not[d] == "" {
-			v.not[d] = w.not[d]
-		}
 	}
 	return v
 }
 
 // proveTemplate proves a template that renders one value: fixed text, or a format that is
 // one token alone.
-func (p *valueProof) proveTemplate(t *template) proven {
+func (p *valueProof) proveTemplate(t *template) proven.Value {
 	lit, fixed := t.fixedText()
 	switch {
 	case t.repeat != 1:
-		return unproven(fmt.Sprintf("%q carries a repeat, which composes text rather than one value", t.format))
+		return proven.Unproven(fmt.Sprintf("%q carries a repeat, which composes text rather than one value", t.format))
 	case fixed:
-		return literalValue(lit)
+		return proven.Literal(lit)
 	case len(t.compiled.ops) != 1:
-		v := unproven(notOneValue(t.format, typedCalls))
+		v := proven.Unproven(notOneValue(t.format, typedCalls))
-		v.notOperand = notOneValue(t.format, operandCalls)
+		v.NotOperand = notOneValue(t.format, operandCalls)
 		return v
 	}
 	o := t.compiled.ops[0]
@@ -206,131 +178,19 @@ func (p *valueProof) proveTemplate(t *template) proven {
 	case builtins[name].proveNumber != nil:
 		return builtins[name].proveNumber(body, builtins[name].prints, args)
 	case isTransform:
-		return unproven(fmt.Sprintf("{%s} rewrites text rather than printing a value; write the values it would print", body))
+		return proven.Unproven(fmt.Sprintf("{%s} rewrites text rather than printing a value; write the values it would print", body))
 	}
-	return printing(body, DataTypeString, proven{notOperand: fmt.Sprintf("{%s} prints text, not a number", body)})
+	return proven.Printing(body, DataTypeString, proven.Value{NotOperand: fmt.Sprintf("{%s} prints text, not a number", body)})
 }
 
-func (p *valueProof) proveCalc(o op) proven {
+func (p *valueProof) proveCalc(o op) proven.Value {
 	body, args := o.Body, o.Args
-	expr := parsedCalc(args[0]).Expr
 	nodes := operandNodes(o)
-	v, doubt := p.proveExpr(expr, func(name string) proven { return p.proveUnion(nodes(name)) })
+	v, doubt := proven.Calc(parsedCalc(args[0]).Expr, func(name string) proven.Value { return p.proveUnion(nodes(name)) })
-	if doubt == "" && !(magnitude(v) <= calcLimit) {
-		doubt = grammar.CalcText(expr) + " is not proven within 1e300"
-	}
 	if doubt != "" {
-		return unproven(fmt.Sprintf("{%s}: %s", body, doubt))
+		return proven.Unproven(fmt.Sprintf("{%s}: %s", body, doubt))
 	}
-	return printedNumber(body, v, calcDecimals(args))
+	return proven.PrintedNumber(body, v, calcDecimals(args))
-}
-
-// calcLimit is the largest magnitude a proof accepts as finite, far enough below
-// math.MaxFloat64 that rounding in the bounds cannot hide an overflow.
-const calcLimit = 1e300
-
-// proveExpr bounds a calc expression from its operands, or says why it cannot.
-func (p *valueProof) proveExpr(n grammar.CalcNode, operand func(name string) proven) (proven, string) {
-	switch n := n.(type) {
-	case grammar.CalcNum:
-		v := float64(n)
-		return bounded(v, v, v == math.Trunc(v)), ""
-	case grammar.CalcVar:
-		v := operand(n.Name)
-		if v.notOperand != "" {
-			return proven{}, fmt.Sprintf("operand %q: %s", n.Name, v.notOperand)
-		}
-		return proven{lo: v.lo, hi: v.hi, nonZero: v.nonZero, integral: v.integral}, ""
-	case grammar.CalcNeg:
-		v, doubt := p.proveExpr(n.X, operand)
-		v.lo, v.hi = -v.hi, -v.lo
-		return v, doubt
-	case grammar.CalcBin:
-		l, doubt := p.proveExpr(n.L, operand)
-		if doubt != "" {
-			return l, doubt
-		}
-		r, doubt := p.proveExpr(n.R, operand)
-		if doubt != "" {
-			return r, doubt
-		}
-		return combine(n, l, r)
-	}
-	panic(internalError("calc node %T has no bound", n))
-}
-
-// combine bounds one operation from the bounds of its sides.
-func combine(n grammar.CalcBin, l, r proven) (proven, string) {
-	var v proven
-	integral := l.integral && r.integral
-	switch n.Operator {
-	case '+':
-		v = bounded(l.lo+r.lo, l.hi+r.hi, integral)
-	case '-':
-		v = bounded(l.lo-r.hi, l.hi-r.lo, integral)
-	case '*':
-		v = bounded(min(l.lo*r.lo, l.lo*r.hi, l.hi*r.lo, l.hi*r.hi), max(l.lo*r.lo, l.lo*r.hi, l.hi*r.lo, l.hi*r.hi), integral)
-		v.nonZero = max(v.nonZero, l.nonZero*r.nonZero)
-	default:
-		if r.nonZero == 0 {
-			return v, fmt.Sprintf("divides by %s, which is not proven nonzero", grammar.CalcText(n.R))
-		}
-		m := magnitude(l) / r.nonZero
-		v = proven{lo: -m, hi: m, nonZero: l.nonZero / magnitude(r)}
-	}
-	if !(magnitude(v) <= calcLimit) {
-		return v, grammar.CalcText(n) + " is not proven within 1e300"
-	}
-	return v, ""
-}
-
-// bounded is a number in [lo, hi], its distance from zero read off the bounds.
-func bounded(lo, hi float64, integral bool) proven {
-	v := proven{lo: lo, hi: hi, integral: integral}
-	switch {
-	case lo > 0:
-		v.nonZero = lo
-	case hi < 0:
-		v.nonZero = -hi
-	}
-	return v
-}
-
-func magnitude(v proven) float64 { return math.Max(math.Abs(v.lo), math.Abs(v.hi)) }
-
-// printedNumber is what a token printing v to dp decimals holds.
-func printedNumber(token string, v proven, dp int) proven {
-	if dp == shortestDecimals {
-		if v.integral { // a whole value prints with no point
-			return printedInteger(token, v)
-		}
-		return printing(token, DataTypeNumber, v)
-	}
-	half, _ := strconv.ParseFloat("5e-"+strconv.Itoa(dp+1), 64)
-	v = proven{lo: v.lo - half, hi: v.hi + half, nonZero: math.Max(0, v.nonZero-half), integral: v.integral || dp == 0}
-	if dp == 0 {
-		return printedInteger(token, v)
-	}
-	return printing(token, DataTypeNumber, v)
-}
-
-func printedInteger(token string, v proven) proven {
-	v = printing(token, DataTypeInteger, v)
-	if !(magnitude(v) < math.MaxInt64) {
-		v.not[DataTypeInteger] = fmt.Sprintf("{%s} is not proven within int64", token)
-	}
-	return v
-}
-
-// printing is v for a token whose every render is text of datatype prints, with a reason
-// against each datatype that text is not.
-func printing(token string, prints DataType, v proven) proven {
-	for d := DataTypeInteger; d <= DataTypeBoolean; d++ {
-		if prints != d && !(prints == DataTypeInteger && d == DataTypeNumber) {
-			v.not[d] = fmt.Sprintf("{%s} prints %s, not %s", token, dataTypeNouns[prints], dataTypeNouns[d])
-		}
-	}
-	return v
 }
 
 var typedCalls, operandCalls = numberCalls(false), numberCalls(true)
@@ -351,53 +211,3 @@ func numberCalls(text bool) string {
 func notOneValue(format, calls string) string {
 	return fmt.Sprintf("%q is not one value; write one literal or one %s, or read one", format, calls)
 }
-
-// unproven is a render no datatype and no calc can take, for why.
-func unproven(why string) proven {
-	v := proven{notOperand: why}
-	for d := DataTypeInteger; d <= DataTypeBoolean; d++ {
-		v.not[d] = why
-	}
-	return v
-}
-
-var (
-	integerText = regexp.MustCompile(`^-?(0|[1-9][0-9]*)$`)
-	numberText  = regexp.MustCompile(`^-?(0|[1-9][0-9]*)(\.[0-9]+)?([eE][+-]?[0-9]+)?$`)
-)
-
-// literalValue proves fixed text: the number calc reads it as, and each datatype it is.
-func literalValue(text string) proven {
-	var v proven
-	if f, err := strconv.ParseFloat(strings.TrimSpace(text), 64); err != nil || math.IsNaN(f) || math.IsInf(f, 0) {
-		v.notOperand = fmt.Sprintf("%q is not a number", text)
-	} else {
-		v = bounded(f, f, f == math.Trunc(f))
-	}
-	if _, err := strconv.ParseInt(text, 10, 64); !integerText.MatchString(text) {
-		v.not[DataTypeInteger] = fmt.Sprintf("%q is not an integer", text)
-	} else if err != nil {
-		v.not[DataTypeInteger] = fmt.Sprintf("%q is past the int64 range", text)
-	}
-	if v.notOperand != "" || !numberText.MatchString(text) {
-		v.not[DataTypeNumber] = fmt.Sprintf("%q is not a number", text)
-	}
-	if text != "true" && text != "false" {
-		v.not[DataTypeBoolean] = fmt.Sprintf("%q is not a boolean", text)
-	}
-	return signedZero(text, v)
-}
-
-// signedZero refuses a zero written with a sign as a typed value, naming it unsigned.
-func signedZero(text string, v proven) proven {
-	mantissa, _, _ := strings.Cut(strings.ToLower(text), "e")
-	if !strings.HasPrefix(text, "-") || v.notOperand != "" || strings.Trim(mantissa, "-0.") != "" {
-		return v
-	}
-	for _, d := range []DataType{DataTypeInteger, DataTypeNumber} {
-		if v.not[d] == "" {
-			v.not[d] = fmt.Sprintf("%q is zero written with a sign; write %q", text, text[1:])
-		}
-	}
-	return v
-}