Laurel: Add constrained type support

[fabiomadge]

Constrained Types for Laurel

Adds constrained types to Laurel via a Laurel-to-Laurel elimination pass that inserts verification checks at type boundaries.

Syntax

constrained nat = x: int where x >= 0 witness 0
constrained posnat = x: nat where x > 0 witness 1

How it works

The pass (ConstrainedTypeElim.lean) eliminates constrained types by:

1. requires for constrained-typed inputs — Core handles caller asserts and body assumes via call elimination
2. ensures for constrained-typed outputs — Core handles body checks and caller assumes
3. assert after local variable init and reassignment of constrained-typed variables
4. Witness as default for uninitialized constrained-typed variables
5. Witness validation via synthetic procedures that assert the witness satisfies all constraints
6. Quantifier constraint injection — forall(n: nat) => body becomes forall(n: int) => n >= 0 ==> body; exists uses &&
7. Type resolution — all constrained type references resolved to base types

The Core translator sees only base types and regular requires/ensures/assert — no translator changes needed beyond pipeline wiring.

Functions

Functions (isFunctional procedures) with constrained return types have isFunctional cleared since the Laurel translator does not yet support function postconditions. A TODO marks this for restoration once that support lands.

Changes

• ConstrainedTypeElim.lean — the elimination pass
• LaurelGrammar.st — constrained type syntax
• ConcreteToAbstractTreeTranslator.lean — parser for constrained keyword
• LaurelToCoreTranslator.lean — pipeline wiring (import + pass + resolve)
• T09_ConstrainedTypes.lean — 24 test procedures covering inputs, outputs, assignments, arguments, nested types, functions, witnesses, quantifiers, capture avoidance

Known limitations

• resolveBaseType, getAllConstraints, and substId are partial — cyclic constrained type definitions loop forever; capture avoidance prevents a termination proof for substId

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.