Use schema in TPE to reduce has/hasTag/in/==/is

[john-h-kastner-aws]

Extends the TPE model so that has, hasTag, in, ==, and is reduce to literals when type information in the schema (plus error-freedom) is enough to reach a concrete value.

Large diff because TPE.evaluate now needs a schema.

Key changes addings this functions with calls at appropriate sites.

/-- Does the schema prove that applying this operation to types `ty₁` and `ty₂` must produce `false`? -/
def mustBeFalse (env : TypeEnv) (op₂ : BinaryOp) (ty₁ ty₂ : CedarType) : Bool :=
  match op₂, ty₁, ty₂ with
  | .mem, .entity ety₁, .entity ety₂
  | .mem, .entity ety₁, .set (.entity ety₂) => !env.descendentOf ety₁ ety₂
  | .eq,  .entity ety₁, .entity ety₂        => ety₁ != ety₂
  | .hasTag, .entity ety, .string           => env.ets.tags? ety == some .none
  | _, _, _                                 => false

/-- Does the schema prove that a value of type `ty₁` cannot have attribute `a`? -/
def cannotHaveAttr (env : TypeEnv) (ty₁ : CedarType) (a : Attr) : Bool :=
  match ty₁ with
  | .record rty => (rty.find? a).isNone
  | .entity ety =>
    match env.ets.attrs? ety with
    | .some rty => (rty.find? a).isNone
    | .none     => false
  | _ => false

Issue #, if available:

Description of changes: