Adding closure resolution - Part 1

[sagjoshi]

Add closure expression resolution to transform Raw.ClosureExpr into
Ast.ClosureExpr with fully resolved types and expressions.

New Methods in ExprResolver.dfy

• ResolveClosureExpr: Main entry point for closure resolution

  • Resolves result type
  • Resolves each closure binding via ResolveClosureBindingWithWF
  • Resolves each closure property via ResolveClosurePropertyWithWF
  • Creates resolved Ast.ClosureExpr

• ResolveClosureBindingWithWF: Resolves a single closure binding

  • Validates parameter names are legal
  • Resolves parameter types
  • Creates scope with binding parameters (can shadow outer scope)
  • Resolves RHS expression in extended scope
  • Proves raw binding well-formedness

• ResolveClosurePropertyWithWF: Resolves a single closure property

  • Builds property scope: outer + result var + binding names + binding params
  • Resolves triggers and body in extended scope
  • Proves raw property well-formedness with detailed invariants

API Changes

• Added ers.Valid() precondition to:

  • ResolveExpr
  • ResolveMaybeExpr
  • ResolveExprList
  • ResolvePatterns

  This is required to prove b3.IsType() for resolved types using the
  equivalence: b3.IsType(t) <==> t in BuiltInTypes || t in typeMap

Design Fix in RawAst.dfy

• Updated Raw.ClosureProperty.WellFormed signature to include resultVar

• Extended property scope to include:

  • Result variable (e.g., %s)
  • Binding names (e.g., %body)
  • Binding parameters (e.g., x in %body(x: int) := e)

  Previously only included outer scope + binding params, which was
  insufficient for properties that reference result var or binding names.