Skip to content

fuzz: Int→Bool predicate generation; silence point-free appendTR false-alarm#32

Merged
emeryberger merged 1 commit into
mainfrom
int-bool-predicates
Jul 7, 2026
Merged

fuzz: Int→Bool predicate generation; silence point-free appendTR false-alarm#32
emeryberger merged 1 commit into
mainfrom
int-bool-predicates

Conversation

@emeryberger

Copy link
Copy Markdown
Owner

Two follow-ups from the campaign wrap-up.

Int → Bool predicate generation

Generalizes the Char → Bool predicate machinery to any α → Bool predicate, adding Int → Bool. A predicate value is a finite subset of a fixed element universe (chars from the alphabet, or a small signed-Int range) — "is this element in the subset?" — which has identical semantics in a Lean and a Python lambda and is serializable. The tag now records the element type ({"__pred__": [...], "ety": "Char"|"Int"}) so the Lean literal and Python materialize rebuild the right membership test.

Unlocks Cedar's setAll/setAny/setFilter (harvest 535 → 538); all three differentially agree with the oracle. Regression case (18) added.

Silence point-free appendTR self-coverage false-alarm

Point-free List.append/appendTR/binop are now handled before the fallthrough.* self-coverage tag (marking const.* instead), so the report no longer falsely flags List.appendTR as a possibly-broken core handler. The emitted code is unchanged and correct ((lambda a, b: a + b)); this only fixes the reporting.

Verification

  • RegressionFixes (44 cases), Comprehensions, TailCalls green; lake build + lake build Corpus green.
  • Local corpus sweep clean (0 bugs), no fallthrough warning.
  • Char→Bool predicates still work (rust-lean-models contains_char_filter/find_char_filter verified).

…e-alarm

- Generalize the `Char → Bool` predicate machinery to any `α → Bool` predicate,
  adding `Int → Bool`: a predicate value is a finite subset of a fixed element
  universe (chars from the alphabet, or a small signed-Int range), tagged with
  the element type (`{"__pred__": [...], "ety": "Char"|"Int"}`) so the Lean
  literal and Python `materialize` rebuild the right membership test. Unlocks
  Cedar's `setAll`/`setAny`/`setFilter` (harvest 535 → 538); all 3 differentially
  agree. Regression case (18).
- Handle point-free `List.append`/`appendTR`/binop BEFORE the `fallthrough.*`
  self-coverage tag (marking `const.*` instead), so the report no longer falsely
  flags `List.appendTR` as a broken core handler. Code output unchanged/correct.

RegressionFixes (44 cases), Comprehensions, TailCalls green; local corpus sweep
clean (0 bugs), no fallthrough warning.
@emeryberger emeryberger merged commit eb3b80b into main Jul 7, 2026
1 check passed
@emeryberger emeryberger deleted the int-bool-predicates branch July 7, 2026 19:43
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant