celtolean: compare float fields at CEL's double precision

A proto `float` is Lean Float32, but CEL converts it to a double before any
numeric operation. Elaborating the literal at Float32 instead was not merely
imprecise: `this == 1.1` on a `float` field is satisfiable in Float32 (by the
Float32 nearest 1.1) and unsatisfiable in CEL, so the kernel could prove a
proposition whose CEL evaluation is false.

A typed `float` value now widens to Float wherever it meets a literal, another
numeric field or arithmetic. Float32 → Float is exact, so widening only removes
the rounding. `float`/`double` comparisons unify for the same reason. The
Float32 literal-magnitude check stays as a backstop for any unwidened path,
but is no longer the guarantee — `this < 1e40` is now emitted exactly rather
than rejected.

Standard `float.*` rules stay narrow deliberately: their bounds come from the
descriptor and are already exactly Float32 values, so the comparison cannot
round either way.

Author: petersonbill64

README.md

@@ -282,10 +282,11 @@ proposition whose CEL evaluation would have errored:
   under `Cel.mulOk x.toInt64 100` — so the guard is exactly CEL's condition
   and an intermediate outside the 32-bit range is not an overflow, matching
   CEL. Division and modulo widen too (fixing `int32Min / -1`, which wraps in
-  `Int32` but not in CEL). Without that typing (values bound by a
-  comprehension variable, elements reached through indexing) the guard falls
-  back to the operand's own Lean type, so `Int32`/`UInt32` operands demand the
-  32-bit range — conservatively stricter than CEL, sound but not exact.
+  `Int32` but not in CEL). Comprehension binders and indexed elements are typed
+  too (see below), so this reaches inside `all`/`exists` bodies; only values
+  with no proto type at all (free identifiers) fall back to the operand's own
+  Lean type, where `Int32`/`UInt32` operands demand the 32-bit range —
+  conservatively stricter than CEL, sound but not exact.
   `Nat` size arithmetic guards truncating subtraction. Constant arithmetic
   folds and range-checks at generation time (an always-erroring rule is
   rejected); concatenation and timestamp/duration arithmetic are total and
@@ -298,15 +299,18 @@ proposition whose CEL evaluation would have errored:
   scalar field rule, `this`-rooted select paths in message rules (including
   map-selection leaves and enum ints, which CEL compares as `int32`), and
   custom CEL on `repeated.items`/`map.keys`/`map.values` elements; it also
-  rejects negative literals against unsigned fields and `double` literals
-  outside `Float32`'s finite range on a `float` field. Literals meeting a
+  rejects negative literals against unsigned fields. Literals meeting a
   *widened* arithmetic result are checked at 64-bit width instead, so
   `this * 10000 <= 5000000000` on an `int32` field is accepted — the product
   is `Int64`. The same typing makes mixed-width comparisons elaborate
   (`this.small < this.big` across `int32`/`int64` widens the narrower side).
-  Values with no resolvable proto type — comprehension binders
-  (`this.all(v, v > 3000000000)`), indexed elements, free identifiers — are
-  *not* checked and can still wrap.
+- **Container elements are typed**: a path may descend into a container, so
+  the value a comprehension binds (`this.all(v, …)` — a repeated field's
+  elements, a map's keys) and the value indexing yields (`this.items[0]` — an
+  element, a map's value) carry the same descriptor typing a named field does.
+  Paths compose through binders, so `this.all(o, o.lots.all(n, n > 3e9))` is
+  range-checked at the innermost element's type. This closes the last
+  silent-wrap corner: only free identifiers now go untyped.
 - **Indexing**: CEL errors on an out-of-range index or missing map key, so
   `l[i]` / `m['k']` translate to `(l[i]?).get h` under a pending
   `(l[i]?).isSome` guard rather than a panicking `l[i]!`. Guards discharge at
@@ -320,20 +324,30 @@ proposition whose CEL evaluation would have errored:
 - **Enums work as ints**: the plugin resolves every `this` path against the
   descriptors, so enum-typed values (field rules, message-rule leaves,
   repeated/map element rules) render through the generated enum's `.toInt32`
-  view, matching CEL's enum-as-int semantics. Standard enum rules keep their
-  constructor-test form. (Enum values reached through *indexing* — an
-  enum-valued `m['k']` compared to an int — still fail at Lean elaboration.)
+  view, matching CEL's enum-as-int semantics — including enum values a
+  comprehension binds or indexing reaches (`this.tier_history[0] >= 1`), under
+  the index guard. Standard enum rules keep their constructor-test form.
 - **Map selection sugar works**: `this.labels.priority` becomes guarded key
   indexing (missing key ⇒ false, CEL's error), and `has(this.labels.priority)`
   becomes key presence — at any path depth.
 - Warnings (stderr / JSON) flag translations with caveats: `has()` presence
   semantics beyond `Option` fields, evaluation-time-dependent `now`,
   placeholder timestamp/duration types, free identifiers kept verbatim,
   non-literal regex patterns.
-- `string(e)` uses `toString`, whose formatting may diverge from CEL's for
-  floats. `float` fields compare at `Float32` precision where CEL compares at
-  double precision, so a `double` literal that is not exactly representable in
-  `Float32` rounds (its *magnitude* is range-checked, its precision is not).
+- **`float` fields are compared at double precision**, as CEL does. A proto
+  `float` is Lean `Float32`, but CEL converts it to a double before any numeric
+  operation, so a typed `float` value is emitted as `x.toFloat` wherever it
+  meets a literal, another numeric field, or arithmetic (`this <= 1.1` on a
+  `float` field becomes `x.toFloat ≤ 1.1`). Widening Float32 → Float is exact,
+  so this only removes a rounding: without it the literal would elaborate at
+  `Float32` and `this == 1.1` would be *satisfiable* in Lean (by the `Float32`
+  nearest 1.1) while being unsatisfiable in CEL — the kernel proving a
+  proposition whose CEL evaluation is false. Standard `float.*` rules are left
+  narrow deliberately: their bounds come from the descriptor and are already
+  exactly `Float32` values, so the comparison cannot round either way. A
+  `float`/`double` field comparison now elaborates too (the `float` side
+  widens). What remains: `string(e)` uses `toString`, whose formatting may
+  diverge from CEL's for floats.
 
 ## Codegen semantics and limitations
 
@@ -542,17 +556,15 @@ non-generated, option-only proto dependencies such as
    now-dependent rules (`timestamp.lt_now`/`within`), which need a
    validation-time story for `Cel.now`.
 3. Residual conservative spots (sound, but stricter than CEL or late-failing).
-   Descriptor-aware numerics closed the literal-wrapping hole and made
-   arithmetic guards CEL-exact wherever a rule's `this`-rooted path resolves
-   to a proto field; what is left is where no such path exists:
-   - values bound by a comprehension variable (`this.all(v, v * 2 > 0)`) or
-     reached through indexing (`this.items[0].qty`) carry no descriptor type,
-     so their literals are unchecked and their 32-bit guards stay
-     conservative — and enum values reached through indexing still lack the
-     `.toInt32` view;
+   Descriptor-aware numerics — now reaching comprehension binders and indexed
+   elements — closed the literal-wrapping hole and made arithmetic guards
+   CEL-exact wherever a rule's value resolves to a proto type. What is left:
+   - free identifiers carry no descriptor type, so their literals are
+     unchecked and their 32-bit guards stay conservative;
    - error absorption under negation (`!(err && false)`) translates to
      failure;
-   - `float` fields compare at `Float32` precision, CEL at double precision.
+   - index proofs inside `exists_one`/`map`/`filter` bodies and negated
+     quantifier bodies have no sound discharge point and are rejected.
 4. No formal relation between `Protovalidate.Cel.Regex` and RE2 beyond the
    per-pattern differential batteries (see
    [regex assurance](#regex-assurance-what-the-guards-do-and-do-not-say)), nor

Test/cel_corpus.tsv

@@ -115,6 +115,8 @@ dom_uint32_wide	UInt32	dom=uint32	this * 2u < 8589934592u
 dom_uint64_add	UInt64	dom=uint64	this + 1u > 0u
 dom_int64_arith	Int64	dom=int64	this * 2 + 1 <= 100
 dom_float_range	Float32	dom=float	this >= -3.4e38 && this <= 3.4e38
+dom_float_precision	Float32	dom=float	this <= 1.1 && this > -1.1
+dom_float_beyond_f32	Float32	dom=float	this < 1e40
 dom_double_range	Float	dom=double	this * 2.0 <= 1e300
 dom_enum_int	CelTest.Tier	dom=enum	this >= 1 && this != 3
 dom_enum_arith	CelTest.Tier	dom=enum	this + 1 == 2

celtolean/domain.go

@@ -143,17 +143,21 @@ func (d *numDom) outOfRange(lit string) error {
 		"type, where it would wrap", lit, d.proto, d.lean, d.minInt(), d.maxInt())
 }
 
-// widen lifts a 32-bit proto integer to the width CEL actually computes at, so
+// widen lifts a 32-bit proto scalar to the width CEL actually computes at, so
 // arithmetic on it (and its overflow guard) is CEL-exact instead of
-// conservatively 32-bit. Values already at CEL width, floats and untyped
-// fragments pass through.
+// conservatively 32-bit, and so a `float` field is compared at the double
+// precision CEL uses. Values already at CEL width and untyped fragments pass
+// through.
 func (t *translator) widen(p piece) piece {
 	d := p.dom
-	if d == nil || d.float || d.bits != 32 {
+	if d == nil || d.bits != 32 {
 		return p
 	}
 	conv, to := ".toInt64", domI64
-	if d.unsigned {
+	switch {
+	case d.float:
+		conv, to = ".toFloat", domF64
+	case d.unsigned:
 		conv, to = ".toUInt64", domU64
 	}
 	return piece{
@@ -166,20 +170,33 @@ func (t *translator) widen(p piece) piece {
 	}
 }
 
-// unifyWidth makes two comparable proto integers elaborate at a common Lean
-// type by widening the narrower one (CEL compares int32 and int64 fields
-// directly; Lean's fixed-width types would not unify). Mixed signedness is a
-// Lean type error either way and is left alone.
+// widenFloat lifts a `float` value to `Float` before it meets anything
+// numeric. Unlike the integer widening, which unifyWidth applies only when two
+// typed operands must meet, this is unconditional: CEL evaluates every numeric
+// operation on a `float` field at double precision, and a double literal is
+// generally *not* representable in Float32. `this == 1.1` on a `float` field
+// is satisfiable in Float32 (by the Float32 nearest 1.1) and unsatisfiable in
+// CEL — so without widening the kernel could prove a proposition whose CEL
+// evaluation is false. Float32 → Float is exact, so widening only removes the
+// rounding, never introduces one.
+func (t *translator) widenFloat(p piece) piece {
+	if p.dom != domF32 {
+		return p
+	}
+	return t.widen(p)
+}
+
+// unifyWidth makes two comparable proto scalars elaborate at a common Lean
+// type by widening the narrower one (CEL compares int32 and int64, or float
+// and double, fields directly; Lean's fixed-width types would not unify).
+// Mixed signedness is a Lean type error either way and is left alone.
 func (t *translator) unifyWidth(l, r piece) (piece, piece) {
 	if l.dom == nil || r.dom == nil || l.dom == r.dom {
 		return l, r
 	}
 	if l.dom.float != r.dom.float || l.dom.unsigned != r.dom.unsigned {
 		return l, r
 	}
-	if l.dom.float {
-		return l, r
-	}
 	if l.dom.bits < r.dom.bits {
 		return t.widen(l), r
 	}
@@ -207,6 +224,11 @@ func arithDom(l, r piece) *numDom {
 // checkLiterals rejects numeric literals that fall outside the domain of the
 // typed operand they meet. Both directions are checked (`this < 3e9` and
 // `3e9 < this`), as are list/map literals on the right of `in`.
+//
+// The Float32 branch of accepts is a backstop: every site that lets a literal
+// meet a `float` value widens it to `Float` first (widenFloat), so the value's
+// domain is `double` by the time the check runs. It fires only if some path
+// forgot to widen — better a generation error than a silently rounded literal.
 func (t *translator) checkLiterals(l, r piece) error {
 	for _, pair := range [2][2]piece{{l, r}, {r, l}} {
 		v, lit := pair[0], pair[1]

celtolean/translate.go

@@ -816,8 +816,10 @@ func (t *translator) binaryArgs(op binOp, args []ast.Expr) (piece, error) {
 		return piece{}, err
 	}
 	// Descriptor-aware checks: a literal outside the typed operand's domain
-	// would silently wrap at elaboration, and two proto integers of different
-	// widths only unify once the narrower one is lifted to CEL's width.
+	// would silently wrap at elaboration, two proto integers of different
+	// widths only unify once the narrower one is lifted to CEL's width, and a
+	// `float` field is compared at the double precision CEL uses.
+	l, r = t.widenFloat(l), t.widenFloat(r)
 	if err := t.checkLiterals(l, r); err != nil {
 		return piece{}, err
 	}
@@ -975,6 +977,7 @@ func (t *translator) equality(fn string, args []ast.Expr) (piece, error) {
 	if rerr != nil {
 		return piece{}, rerr
 	}
+	l, r = t.widenFloat(l), t.widenFloat(r)
 	if err := t.checkLiterals(l, r); err != nil {
 		return piece{}, err
 	}

celtolean/translate_test.go

@@ -378,11 +378,19 @@ func TestNumericDomainWidening(t *testing.T) {
 		// No arithmetic: no widening, so the emitted proposition stays the one
 		// a Lean author would write over the field's own type.
 		{"int32_plain_compare", map[string]PathAttr{"": PathInt32}, `this > 3`, `x > 3`},
-		// Floats stay at the field's own type: CEL double arithmetic cannot
-		// error, so there is no guard to tighten (the ArithOk instance is
-		// trivially true) and widening would only obscure the proposition.
-		{"float_no_widen", map[string]PathAttr{"": PathFloat}, `this * 2.0 < 5.0`,
-			`(if h : Cel.mulOk x 2.0 then x * 2.0 < 5.0 else False)`},
+		// `float` fields widen to Float: CEL evaluates every numeric operation
+		// on them at double precision, and a double literal generally has no
+		// exact Float32 counterpart.
+		{"float_widen_arith", map[string]PathAttr{"": PathFloat}, `this * 2.0 < 5.0`,
+			`(if h : Cel.mulOk x.toFloat 2.0 then x.toFloat * 2.0 < 5.0 else False)`},
+		{"float_widen_compare", map[string]PathAttr{"": PathFloat}, `this <= 1.1`,
+			`x.toFloat ≤ 1.1`},
+		// The literal is beyond Float32's finite range but an ordinary double:
+		// widened, the comparison is exactly CEL's.
+		{"float_widen_magnitude", map[string]PathAttr{"": PathFloat}, `this < 1e40`,
+			`x.toFloat < 1e40`},
+		// double fields are already at CEL's width.
+		{"double_plain", map[string]PathAttr{"": PathDouble}, `this <= 1.1`, `x ≤ 1.1`},
 	}
 	for _, tt := range tests {
 		t.Run(tt.name, func(t *testing.T) {
@@ -396,13 +404,21 @@ func TestNumericDomainWidening(t *testing.T) {
 		})
 	}
 
-	// Comparing proto integers of different widths: CEL compares them
+	// Comparing proto scalars of different widths: CEL compares them
 	// directly, so the narrower one is lifted to the wider Lean type.
-	fields := map[string]ThisField{"small": {Text: "small"}, "big": {Text: "big"}, "n": {Text: "n"}}
-	attrs := map[string]PathAttr{"small": PathInt32, "big": PathInt64, "n": PathUInt32}
+	fields := map[string]ThisField{
+		"small": {Text: "small"}, "big": {Text: "big"}, "n": {Text: "n"},
+		"f": {Text: "f"}, "d": {Text: "d"},
+	}
+	attrs := map[string]PathAttr{
+		"small": PathInt32, "big": PathInt64, "n": PathUInt32,
+		"f": PathFloat, "d": PathDouble,
+	}
 	mixed := []struct{ cel, want string }{
 		{`this.small < this.big`, `small.toInt64 < big`},
 		{`this.big == this.small`, `big = small.toInt64`},
+		{`this.f < this.d`, `f.toFloat < d`},
+		{`this.d == this.f`, `d = f.toFloat`},
 		{`this.small + 1 > this.big`,
 			`(if h : Cel.addOk small.toInt64 1 then small.toInt64 + 1 > big else False)`},
 		{`this.n * 2u > 100u`,
@@ -447,8 +463,6 @@ func TestNumericDomainRejects(t *testing.T) {
 			"outside the domain of the int64 value"},
 		{"in_list", map[string]PathAttr{"": PathInt32}, nil, `this in [1, 2, 5000000000]`,
 			"outside the domain of the int32 value"},
-		{"float_overflow", map[string]PathAttr{"": PathFloat}, nil, `this < 1e40`,
-			"outside the finite range of the `float` field's Lean type Float32"},
 		{"message_rule_leaf", map[string]PathAttr{"stock": PathInt32}, fields,
 			`this.stock < 3000000000`, "outside the domain of the int32 value"},
 		{"message_rule_uint", map[string]PathAttr{"batch": PathUInt32}, fields,

examples/shipping/InventoryValidTest.lean

@@ -93,6 +93,14 @@ def main : IO Unit := do
     "product.first_tier" "indexed enum element below bound"
   expectId (Valid.Product.validate { goodProduct with tier_history := #[] }) "" "empty array: index guard unforced"
 
+  -- A `float` field is compared at CEL's double precision. The Float32
+  -- nearest 1.1 is 1.10000002384…, which is *greater* than the double 1.1, so
+  -- CEL rejects it — and so must the refinement. Comparing in Float32 (where
+  -- the literal would round to that same value) would have accepted it.
+  expectId (Valid.Product.validate { goodProduct with weight_kg := 1.0 }) "" "float under cap"
+  expectId (Valid.Product.validate { goodProduct with weight_kg := 1.1 }) "weight.cap" "float double-precision cap"
+  expectId (Valid.Product.validate { goodProduct with weight_kg := -1.0 }) "float.gte" "float gte"
+
   -- encode → decodeValid roundtrip
   let base := v.toBase
   match base.encode with

examples/shipping/inventory.proto

@@ -64,6 +64,15 @@ message Product {
     id: "lots.capacity", message: "each lot must stay under the reserved cap",
     expression: "this.all(n, n * 10000 <= 5000000000)"
   }];
+  float weight_kg = 18 [(buf.validate.field).float.gte = 0.0,
+                        (buf.validate.field).cel = {
+    // A `float` field compared against a *double* literal: CEL converts the
+    // field to double, so the emitted proposition does too. Elaborating 1.1
+    // at Float32 instead would round it up to 1.10000002384…, and a stored
+    // 1.1f would then pass a rule CEL rejects.
+    id: "weight.cap", message: "weight must not exceed the cap",
+    expression: "this <= 1.1"
+  }];
   repeated Tier tier_history = 17 [(buf.validate.field).cel = {
     // Enum elements compare as ints, through the generated .toInt32 view.
     id: "tiers.known", message: "every recorded tier must be a known tier",