Denotation of SMT terms for the Strata DSL

This module interprets the shallowly embedded SMT term language into Lean types. The interpretation is partial because not every SMT feature is currently supported. The core entry point is denoteTerm, which builds a TermDenoteResult describing both the type of a term and a semantic interpreter for it. The surrounding infrastructure tracks the well-formedness of term and uninterpreted-function contexts so that evaluation is safe.

The denotation uses propositional extensionality (propext) and Classical.propDecidable (excluded middle) to make if-then-else over Prop-valued conditions definable. Downstream correctness proofs (see FactoryCorrect.lean) inherit these dependencies.

theorem List.getElem_of_findIdx?_eq_some {α : Type u_1} {xs : List α} {mkTypeFunType : α → Bool} {i : Nat} (h : findIdx? mkTypeFunType xs = some i) : mkTypeFunType xs[i] = true

def mkTypeFunType (n : Nat) : Type 1

Equations

• mkTypeFunType n = Nat.repeat (fun (x : Type 1) => Type → x) n Type

def applyTypeArg {n : Nat} (tf : mkTypeFunType (n + 1)) (α : Type) : mkTypeFunType n

Equations

• applyTypeArg tf α = tf α

def applyTypeArgs {n : Nat} (tf : mkTypeFunType n) (αs : List Type) (h : αs.length = n) : Type

Equations

• applyTypeArgs tf_2 [] h_2 = tf_2
• applyTypeArgs tf_2 (α :: αs_2) h_2 = applyTypeArgs (applyTypeArg tf_2 α) αs_2 ⋯

def mkNonemptyPred {n : Nat} (us : mkTypeFunType n) : Prop

Equations

• mkNonemptyPred us_2 = Nonempty us_2
• mkNonemptyPred us_2 = ∀ (α : Type), mkNonemptyPred (applyTypeArg us_2 α)

@[reducible]

def applyNonemptyPred {n : Nat} {fα : mkTypeFunType n} (hfα : mkNonemptyPred fα) (αs : List Type) (h : αs.length = n) : Nonempty (applyTypeArgs fα αs h)

Equations

• ⋯ = ⋯

structure USDenote : Type 1

• us : Core.SMT.Sort
• usΓ : mkTypeFunType self.us.arity
• nonempty : mkNonemptyPred self.usΓ

@[reducible, inline]

abbrev USContext : Type

Equations

• USContext = List Core.SMT.Sort

@[reducible, inline]

abbrev USEnvironment : Type 1

Equations

• USEnvironment = List USDenote

structure USEnvironment.WF (uss : USContext) (Γ : USEnvironment) : Prop

• h : List.length uss = List.length Γ
• ha (i : Nat) (hi : i < List.length uss) : uss[i] = Γ[i].us

@[reducible, inline]

abbrev ISContext : Type

Context for type synonyms. Maps a sort name to its type, which is assumed to not contain other type synonyms. Denotation fails if this is violated

Equations

• ISContext = Map String Strata.SMT.TermType

structure SortContext : Type

• uss : USContext
• iss : ISContext

@[reducible, inline]

abbrev SortEnvironment : Type 1

Equations

• SortEnvironment = USEnvironment

@[reducible, inline]

abbrev SortEnvironment.WF (sctx : SortContext) (Γ : SortEnvironment) : Prop

Equations

• SortEnvironment.WF sctx Γ = USEnvironment.WF sctx.uss Γ

structure SortDenoteInput (sctx : SortContext) : Type 1

• sΓ : SortEnvironment
• hsΓ : SortEnvironment.WF sctx self.sΓ

@[reducible, inline]

abbrev SortDenoteResult (sctx : SortContext) : Type 1

Equations

• SortDenoteResult sctx = (SortDenoteInput sctx → Type)

def substituteIS (iss : ISContext) (ty : Strata.SMT.TermType) : Strata.SMT.TermType

Equations

• substituteIS iss (Strata.SMT.TermType.prim pty) = Strata.SMT.TermType.prim pty
• substituteIS iss ty_2.option = (substituteIS iss ty_2).option
• substituteIS iss (Strata.SMT.TermType.constr id args) = match Map.find? iss id with | some ty' => ty' | none => Strata.SMT.TermType.constr id (substituteISs iss args)

def substituteISs (iss : ISContext) (tys : List Strata.SMT.TermType) : List Strata.SMT.TermType

Equations

• substituteISs iss [] = []
• substituteISs iss (ty :: tys_2) = substituteIS iss ty :: substituteISs iss tys_2

def substituteTermVarIS (isctx : ISContext) (v : Strata.SMT.TermVar) : Strata.SMT.TermVar

Equations

• substituteTermVarIS isctx v = { id := v.id, ty := substituteIS isctx v.ty }

def substituteUFIS (isctx : ISContext) (uf : Strata.SMT.UF) : Strata.SMT.UF

Equations

• substituteUFIS isctx uf = { id := uf.id, args := List.map (substituteTermVarIS isctx) uf.args, out := substituteIS isctx uf.out }

def substituteTermIS (isctx : ISContext) (t : Strata.SMT.Term) : Strata.SMT.Term

Equations

• One or more equations did not get rendered due to their size.
• substituteTermIS isctx (Strata.SMT.Term.prim v) = Strata.SMT.Term.prim v
• substituteTermIS isctx (Strata.SMT.Term.var v) = Strata.SMT.Term.var (substituteTermVarIS isctx v)
• substituteTermIS isctx (Strata.SMT.Term.none ty) = Strata.SMT.Term.none (substituteIS isctx ty)
• substituteTermIS isctx t_2.some = (substituteTermIS isctx t_2).some
• substituteTermIS isctx (Strata.SMT.Term.app op as ty) = Strata.SMT.Term.app op (substituteTermISs isctx as) (substituteIS isctx ty)
• substituteTermIS isctx (Strata.SMT.Term.quant q vs t_2 b) = Strata.SMT.Term.quant q (List.map (substituteTermVarIS isctx) vs) (substituteTermIS isctx t_2) (substituteTermIS isctx b)

def substituteTermISs (isctx : ISContext) (ts : List Strata.SMT.Term) : List Strata.SMT.Term

Equations

• substituteTermISs isctx [] = []
• substituteTermISs isctx (t :: ts_2) = substituteTermIS isctx t :: substituteTermISs isctx ts_2

def substituteIFIS (isctx : ISContext) (iF : Core.SMT.IF) : Core.SMT.IF

Equations

• substituteIFIS isctx iF = { uf := substituteUFIS isctx iF.uf, body := substituteTermIS isctx iF.body }

def denotePrimSort (sctx : SortContext) (pty : Strata.SMT.TermPrimType) : Option (SortDenoteResult sctx)

Interpret primitive SMT types as Lean types, when supported.

Equations

• denotePrimSort sctx Strata.SMT.TermPrimType.bool = pure fun (x : SortDenoteInput sctx) => Prop
• denotePrimSort sctx Strata.SMT.TermPrimType.int = pure fun (x : SortDenoteInput sctx) => Int
• denotePrimSort sctx (Strata.SMT.TermPrimType.bitvec n) = pure fun (x : SortDenoteInput sctx) => BitVec n
• denotePrimSort sctx Strata.SMT.TermPrimType.real = none
• denotePrimSort sctx Strata.SMT.TermPrimType.string = pure fun (x : SortDenoteInput sctx) => String
• denotePrimSort sctx Strata.SMT.TermPrimType.regex = none
• denotePrimSort sctx Strata.SMT.TermPrimType.trigger = none

def denoteSortAux (sctx : SortContext) (ty : Strata.SMT.TermType) : Option (SortDenoteResult sctx)

Interpret an SMT TermType as a Lean Type, when supported.

Returns none when we lack an interpretation (e.g. for reals).

Note: similar to denoteSort, but does not attempt to look up type synonyms.

Equations

• One or more equations did not get rendered due to their size.
• denoteSortAux sctx (Strata.SMT.TermType.prim pty) = denotePrimSort sctx pty
• denoteSortAux sctx ty_2.option = do let ty ← denoteSortAux sctx ty_2 pure fun (sΓ : SortDenoteInput sctx) => Option (ty sΓ)

def denoteSortsAux (sctx : SortContext) (tys : List Strata.SMT.TermType) : Option (List (SortDenoteResult sctx))

Equations

• denoteSortsAux sctx [] = pure []
• denoteSortsAux sctx (a :: as) = do let a ← denoteSortAux sctx a let as ← denoteSortsAux sctx as pure (a :: as)

def denoteSort (sctx : SortContext) (ty : Strata.SMT.TermType) : Option (SortDenoteResult sctx)

Interpret an SMT TermType as a Lean Type, when supported.

Returns none when we lack an interpretation (e.g. for reals).

Equations

• One or more equations did not get rendered due to their size.
• denoteSort sctx (Strata.SMT.TermType.prim pty) = denotePrimSort sctx pty
• denoteSort sctx ty_2.option = do let ty ← denoteSort sctx ty_2 pure fun (sΓ : SortDenoteInput sctx) => Option (ty sΓ)

def denoteSorts (sctx : SortContext) (tys : List Strata.SMT.TermType) : Option (List (SortDenoteResult sctx))

Equations

• denoteSorts sctx [] = pure []
• denoteSorts sctx (a :: as) = do let a ← denoteSort sctx a let as ← denoteSorts sctx as pure (a :: as)

def denoteFunSort (sctx : SortContext) (as : List Strata.SMT.TermVar) (out : Strata.SMT.TermType) : Option (SortDenoteResult sctx)

Interpret a function type described by SMT term variables and a return type.

The result is an arrow type a₁ → … → out when every argument and the result type can be interpreted.

Equations

• denoteFunSort sctx [] out = denoteSort sctx out
• denoteFunSort sctx (a :: as_2) out = do let a ← denoteSort sctx a.ty let as ← denoteFunSort sctx as_2 out pure fun (sΓ : SortDenoteInput sctx) => a sΓ → as sΓ

theorem denoteSortOption_isSome {sctx : SortContext} {ty : Strata.SMT.TermType} (h : (denoteSort sctx ty.option).isSome = true) : (denoteSort sctx ty).isSome = true

theorem isSome_denoteSortOption {sctx : SortContext} {ty : Strata.SMT.TermType} (h : (denoteSort sctx ty).isSome = true) : (denoteSort sctx ty.option).isSome = true

theorem denoteSortOption_Some {sctx : SortContext} {ty : Strata.SMT.TermType} {h : (denoteSort sctx ty.option).isSome = true} {sΓ : SortDenoteInput sctx} : (denoteSort sctx ty.option).get h sΓ = Option ((denoteSort sctx ty).get ⋯ sΓ)

theorem denoteFunSortCons_isSome {sctx : SortContext} {a : Strata.SMT.TermVar} {as : List Strata.SMT.TermVar} {out : Strata.SMT.TermType} (h : (denoteFunSort sctx (a :: as) out).isSome = true) : (denoteSort sctx a.ty).isSome = true ∧ (denoteFunSort sctx as out).isSome = true

theorem arrow_of_denoteFunSortCons_isSome {sctx : SortContext} {a : Strata.SMT.TermVar} {as : List Strata.SMT.TermVar} {out : Strata.SMT.TermType} {sΓ : SortDenoteInput sctx} (h : (denoteFunSort sctx (a :: as) out).isSome = true) : have has := ⋯; (denoteFunSort sctx (a :: as) out).get h sΓ = ((denoteSort sctx a.ty).get ⋯ sΓ → (denoteFunSort sctx as out).get ⋯ sΓ)

theorem denoteSortOut_isSome_of_denoteFunSort_isSome {sctx : SortContext} {as : List Strata.SMT.TermVar} {out : Strata.SMT.TermType} (h : (denoteFunSort sctx as out).isSome = true) : (denoteSort sctx out).isSome = true

structure TermVarDenote {sctx : SortContext} (sΓ : SortDenoteInput sctx) : Type

Runtime value paired with a term-variable declaration and a proof that the type can be interpreted.

• var : Strata.SMT.TermVar
• h : (denoteSort sctx self.var.ty).isSome = true
• varΓ : (denoteSort sctx self.var.ty).get ⋯ sΓ

@[reducible, inline]

abbrev TermVarContext : Type

Equations

• TermVarContext = List Strata.SMT.TermVar

@[reducible, inline]

abbrev TermVarEnvironment {sctx : SortContext} (sΓ : SortDenoteInput sctx) : Type

Equations

• TermVarEnvironment sΓ = List (TermVarDenote sΓ)

def TermVarEnvironment.toContext {sctx✝ : SortContext} {sΓ : SortDenoteInput sctx✝} (tΓ : TermVarEnvironment sΓ) : TermVarContext

Forget semantic values, keeping only the declared term variables.

Equations

• tΓ.toContext = List.map (fun (x : TermVarDenote sΓ) => x.var) tΓ

structure TermVarEnvironment.WF {x✝ : SortContext} {sΓ : SortDenoteInput x✝} (vs : TermVarContext) (tΓ : TermVarEnvironment sΓ) : Prop

Well-formedness predicate ensuring that an interpreted term-variable environment matches its syntactic context.

• h : List.length vs = List.length tΓ
• ha (i : Nat) (hi : i < List.length vs) : vs[i] = tΓ[i].var

structure UFDenote {sctx : SortContext} (sΓ : SortDenoteInput sctx) : Type

Runtime function paired with the corresponding uninterpreted-function declaration and interpretation witness.

• uf : Strata.SMT.UF
• h : (denoteFunSort sctx self.uf.args self.uf.out).isSome = true
• ufΓ : (denoteFunSort sctx self.uf.args self.uf.out).get ⋯ sΓ

@[reducible, inline]

abbrev UFContext : Type

Equations

• UFContext = List Strata.SMT.UF

@[reducible, inline]

abbrev UFEnvironment {sctx : SortContext} (sΓ : SortDenoteInput sctx) : Type

Equations

• UFEnvironment sΓ = List (UFDenote sΓ)

def UFEnvironment.toContext {sctx✝ : SortContext} {sΓ : SortDenoteInput sctx✝} (Γ : UFEnvironment sΓ) : UFContext

Forget semantic values, keeping only UF declarations.

Equations

• Γ.toContext = List.map (fun (x : UFDenote sΓ) => x.uf) Γ

structure UFEnvironment.WF {x✝ : SortContext} {sΓ : SortDenoteInput x✝} (ufs : UFContext) (Γ : UFEnvironment sΓ) : Prop

Well-formedness predicate ensuring that an interpreted uninterpreted-function environment aligns with the syntactic declarations.

• h : List.length ufs = List.length Γ
• ha (i : Nat) (hi : i < List.length ufs) : ufs[i] = Γ[i].uf

structure TermContext : Type

Syntactic context tracking the declared term variables and uninterpreted functions that may appear in a term.

This is intentionally separate from TermEnvironment: an environment contains strictly more information (semantic values), but denotation judgments are formulated against syntax-level declarations and then related to environments via TermEnvironment.WF.

• vs : TermVarContext
• ufs : UFContext

structure TermEnvironment {sctx : SortContext} (sΓ : SortDenoteInput sctx) : Type

Semantic environment providing Lean values for the elements stored in a TermContext.

Although this could project back to a context (toContext), we keep an explicit TermContext parameter in denotation APIs so binder-extension and lookup steps can be stated over declarations first, with realizability tracked separately via WF.

• vs : TermVarEnvironment sΓ
• ufs : UFEnvironment sΓ

structure TermEnvironment.WF {x✝ : SortContext} {sΓ : SortDenoteInput x✝} (tctx : TermContext) (Γ : TermEnvironment sΓ) : Prop

Well-formedness predicate linking a semantic Environment with the corresponding syntactic Context.

• hv : TermVarEnvironment.WF tctx.vs Γ.vs
• huf : UFEnvironment.WF tctx.ufs Γ.ufs

structure Context : Type

• sctx : SortContext
• tctx : TermContext

structure TermDenoteInput (ctx : Context) : Type 1

Bundle pairing an environment with a proof that it realises a particular context. This is the argument given to semantic interpreters.

• sΓ : SortEnvironment
• hsΓ : SortEnvironment.WF ctx.sctx self.sΓ
• tΓ : TermEnvironment { sΓ := self.sΓ, hsΓ := ⋯ }
• htΓ : TermEnvironment.WF ctx.tctx self.tΓ

structure TermDenoteResult (ctx : Context) : Type 1

Result of attempting to interpret a term: carries its type, a proof that the type is supported, and a semantic interpreter.

• ty : Strata.SMT.TermType
• h : (denoteSort ctx.sctx self.ty).isSome = true
• res (tdi : TermDenoteInput ctx) : (denoteSort ctx.sctx self.ty).get ⋯ { sΓ := tdi.sΓ, hsΓ := ⋯ }

noncomputable def argTypesAlign {ctx : Context} (as : List (TermDenoteResult ctx)) (vs : List Strata.SMT.TermVar) : Bool

Check that denoted argument types match declared variable types.

If lengths differ, this returns false.

Equations

• argTypesAlign [] [] = true
• argTypesAlign (a :: as_2) (v :: vs_2) = (a.ty == v.ty && argTypesAlign as_2 vs_2)
• argTypesAlign as vs = false

theorem argTypesAlign_length_eq {ctx✝ : Context} {as : List (TermDenoteResult ctx✝)} {vs : List Strata.SMT.TermVar} (h : argTypesAlign as vs = true) : as.length = vs.length

theorem argTypesAlign_true {ctx : Context} {as : List (TermDenoteResult ctx)} {vs : List Strata.SMT.TermVar} (h : argTypesAlign as vs = true) (i : Nat) (hi : i < as.length) : as[i].ty = vs[i].ty

theorem argTypesAlign_arg_types {ctx : Context} {as : List (TermDenoteResult ctx)} {vs : List Strata.SMT.TermVar} (h : argTypesAlign as vs = true) (i : Nat) (hi : i < as.length) : as[i].ty = vs[i].ty

noncomputable def applyUFAux {ctx : Context} {args : List Strata.SMT.TermVar} {out : Strata.SMT.TermType} {h : (denoteFunSort ctx.sctx args out).isSome = true} (tdi : TermDenoteInput ctx) (uf : (denoteFunSort ctx.sctx args out).get h { sΓ := tdi.sΓ, hsΓ := ⋯ }) (as : List (TermDenoteResult ctx)) (hl : args.length = as.length) (has : ∀ (i : Nat) (hi : i < as.length), as[i].ty = args[i].ty) : (denoteSort ctx.sctx out).get ⋯ { sΓ := tdi.sΓ, hsΓ := ⋯ }

Apply the semantic interpretation of a UF symbol to denoted arguments.

Equations

• applyUFAux tdi uf_2 [] hl_2 has_2 = uf_2
• applyUFAux tdi uf_2 (a :: as_2) hl_2 has_2 = applyUFAux tdi ((⋯ ▸ uf_2) (⋯ ▸ a.res tdi)) as_2 ⋯ ⋯

noncomputable def applyUF {ctx : Context} {args : List Strata.SMT.TermVar} {out : Strata.SMT.TermType} {h : (denoteFunSort ctx.sctx args out).isSome = true} (tdi : TermDenoteInput ctx) (uf : (denoteFunSort ctx.sctx args out).get h { sΓ := tdi.sΓ, hsΓ := ⋯ }) (as : List (TermDenoteResult ctx)) (hAlign : argTypesAlign as args = true) : (denoteSort ctx.sctx out).get ⋯ { sΓ := tdi.sΓ, hsΓ := ⋯ }

Apply the semantic interpretation of a UF symbol to denoted arguments.

Equations

• applyUF tdi uf as hAlign = applyUFAux tdi uf as ⋯ ⋯

@[reducible, inline]

abbrev QuantVarBinder : Type 1

Shape of a one-variable quantifier binder combinator (∀ or ∃).

Equations

• One or more equations did not get rendered due to their size.

def bindForallVar : QuantVarBinder

Semantics helper for universal quantification.

Given a body interpretation over the context extended with one bound variable (n : ty), produce the interpretation in the original context by universally quantifying over all Lean values of the denoted sort ty. This also extends the term environment with the chosen value and carries the corresponding WF proof for the extended context.

Equations

• One or more equations did not get rendered due to their size.

def bindExistsVar : QuantVarBinder

Semantics helper for existential quantification.

Given a body interpretation over the context extended with one bound variable (n : ty), produce the interpretation in the original context by existentially quantifying over Lean values of the denoted sort ty. This also extends the term environment with the chosen witness and carries the corresponding WF proof for the extended context.

Equations

• One or more equations did not get rendered due to their size.

def buildQuant (bindVar : QuantVarBinder) (ctx : Context) (vs : List Strata.SMT.TermVar) (hTys : (denoteFunSort ctx.sctx vs (Strata.SMT.TermType.prim Strata.SMT.TermPrimType.bool)).isSome = true) (bodyFt : TermDenoteInput { sctx := ctx.sctx, tctx := { vs := vs.reverse ++ ctx.tctx.vs, ufs := ctx.tctx.ufs } } → Prop) (tdi : TermDenoteInput ctx) : Prop

Equations

• One or more equations did not get rendered due to their size.
• buildQuant bindVar ctx [] hTys_2 bodyFt_2 tdi = bodyFt_2 tdi

def buildExists (ctx : Context) (vs : List Strata.SMT.TermVar) (hTys : (denoteFunSort ctx.sctx vs (Strata.SMT.TermType.prim Strata.SMT.TermPrimType.bool)).isSome = true) (bodyFt : TermDenoteInput { sctx := ctx.sctx, tctx := { vs := vs.reverse ++ ctx.tctx.vs, ufs := ctx.tctx.ufs } } → Prop) (tdi : TermDenoteInput ctx) : Prop

Equations

• buildExists ctx vs hTys bodyFt tdi = buildQuant (fun {n : String} {ty : Strata.SMT.TermType} => bindExistsVar) ctx vs hTys bodyFt tdi

def buildForall (ctx : Context) (vs : List Strata.SMT.TermVar) (hTys : (denoteFunSort ctx.sctx vs (Strata.SMT.TermType.prim Strata.SMT.TermPrimType.bool)).isSome = true) (bodyFt : TermDenoteInput { sctx := ctx.sctx, tctx := { vs := vs.reverse ++ ctx.tctx.vs, ufs := ctx.tctx.ufs } } → Prop) (tdi : TermDenoteInput ctx) : Prop

Equations

• buildForall ctx vs hTys bodyFt tdi = buildQuant (fun {n : String} {ty : Strata.SMT.TermType} => bindForallVar) ctx vs hTys bodyFt tdi

noncomputable def denoteTerm (ctx : Context) (t : Strata.SMT.Term) : Option (TermDenoteResult ctx)

Attempt to interpret a single SMT term under ctx, returning its Lean type and semantics when successful.

noncomputable def denoteTerms (ctx : Context) (ts : List Strata.SMT.Term) : Option (List (TermDenoteResult ctx))

Interpret every term in a list, short-circuiting if any sub-term fails.

Equations

• denoteTerms ctx [] = pure []
• denoteTerms ctx (a :: as) = do let a ← denoteTerm ctx a let as ← denoteTerms ctx as pure (a :: as)

noncomputable def leftAssoc (ctx : Context) (ty : Strata.SMT.TermType) (h : (denoteSort ctx.sctx ty).isSome = true) (op : (sdi : SortDenoteInput ctx.sctx) → (denoteSort ctx.sctx ty).get h sdi → (denoteSort ctx.sctx ty).get h sdi → (denoteSort ctx.sctx ty).get h sdi) (ts : List (TermDenoteResult ctx)) : Option (TermDenoteResult ctx)

Equations

• One or more equations did not get rendered due to their size.
• leftAssoc ctx ty h op ts = none

noncomputable def leftAssoc.go (ctx : Context) (ty : Strata.SMT.TermType) (h : (denoteSort ctx.sctx ty).isSome = true) (op : (sdi : SortDenoteInput ctx.sctx) → (denoteSort ctx.sctx ty).get h sdi → (denoteSort ctx.sctx ty).get h sdi → (denoteSort ctx.sctx ty).get h sdi) (ft : (tdi : TermDenoteInput ctx) → (denoteSort ctx.sctx ty).get h { sΓ := tdi.sΓ, hsΓ := ⋯ }) (ts : List (TermDenoteResult ctx)) : Option (TermDenoteResult ctx)

Equations

• One or more equations did not get rendered due to their size.
• leftAssoc.go ctx ty h op ft [] = pure { ty := ty, h := h, res := ft }

noncomputable def rightAssoc (ctx : Context) (ty : Strata.SMT.TermType) (h : (denoteSort ctx.sctx ty).isSome = true) (op : (sdi : SortDenoteInput ctx.sctx) → (denoteSort ctx.sctx ty).get h sdi → (denoteSort ctx.sctx ty).get h sdi → (denoteSort ctx.sctx ty).get h sdi) (ts : List (TermDenoteResult ctx)) : Option (TermDenoteResult ctx)

Equations

• rightAssoc ctx ty h op ts = do let ft ← rightAssoc.go ctx ty h op ts pure { ty := ty, h := h, res := ft }

noncomputable def rightAssoc.go (ctx : Context) (ty : Strata.SMT.TermType) (h : (denoteSort ctx.sctx ty).isSome = true) (op : (sdi : SortDenoteInput ctx.sctx) → (denoteSort ctx.sctx ty).get h sdi → (denoteSort ctx.sctx ty).get h sdi → (denoteSort ctx.sctx ty).get h sdi) (ts : List (TermDenoteResult ctx)) : Option ((tdi : TermDenoteInput ctx) → (denoteSort ctx.sctx ty).get h { sΓ := tdi.sΓ, hsΓ := ⋯ })

Equations

• One or more equations did not get rendered due to their size.
• rightAssoc.go ctx ty h op [] = none
• rightAssoc.go ctx ty h op [head] = none

noncomputable def chainable (ctx : Context) (ty : Strata.SMT.TermType) (h : (denoteSort ctx.sctx ty).isSome = true) (op : (sdi : SortDenoteInput ctx.sctx) → (denoteSort ctx.sctx ty).get h sdi → (denoteSort ctx.sctx ty).get h sdi → Prop) (ts : List (TermDenoteResult ctx)) : Option (TermDenoteResult ctx)

Equations

• One or more equations did not get rendered due to their size.
• chainable ctx ty h op ts = none

noncomputable def chainable.go (ctx : Context) (ty : Strata.SMT.TermType) (h : (denoteSort ctx.sctx ty).isSome = true) (op : (sdi : SortDenoteInput ctx.sctx) → (denoteSort ctx.sctx ty).get h sdi → (denoteSort ctx.sctx ty).get h sdi → Prop) (ft : TermDenoteInput ctx → Prop) (ft₁ : (tdi : TermDenoteInput ctx) → (denoteSort ctx.sctx ty).get h { sΓ := tdi.sΓ, hsΓ := ⋯ }) (ts : List (TermDenoteResult ctx)) : Option (TermDenoteResult ctx)

Equations

• One or more equations did not get rendered due to their size.
• chainable.go ctx ty h op ft ft₁ [] = pure { ty := Strata.SMT.TermType.prim Strata.SMT.TermPrimType.bool, h := ⋯, res := ft }

noncomputable def denoteBoolTermAux (t : Strata.SMT.Term) : Option Prop

Interpret a ground boolean term in the empty context.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def denoteIntTermAux (t : Strata.SMT.Term) : Option Int

Interpret a ground integer term in the empty context.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def denoteBVTermAux (n : Nat) (t : Strata.SMT.Term) : Option (BitVec n)

Interpret a ground bitvector term in the empty context.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def denoteStringTermAux (t : Strata.SMT.Term) : Option String

Interpret a ground string term in the empty context.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def bindUS (uss : List Core.SMT.Sort) (iss : ISContext) {us' : Core.SMT.Sort} (ft' : SortDenoteInput { uss := us' :: uss, iss := iss } → Prop) : Option (SortDenoteInput { uss := uss, iss := iss } → Prop)

Eliminate one uninterpreted sort binder by quantifying over all of its semantic realizations and extending the sort environment accordingly.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def bindUF {n : String} {args : List Strata.SMT.TermVar} {out : Strata.SMT.TermType} (ctx : Context) (ft' : have uf' := { id := n, args := args, out := out }; have ufs' := uf' :: ctx.tctx.ufs; have tctx' := { vs := ctx.tctx.vs, ufs := ufs' }; TermDenoteInput { sctx := ctx.sctx, tctx := tctx' } → Prop) : Option (TermDenoteInput ctx → Prop)

Extend the context with an uninterpreted function and push its realisation into the denotation.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def bindIFVar {vs : List Strata.SMT.TermVar} {out : Strata.SMT.TermType} {n : String} {ty : Strata.SMT.TermType} (ctx : Context) {hTys : (denoteFunSort ctx.sctx vs out).isSome = true} {hTyTys : (denoteFunSort ctx.sctx ({ id := n, ty := ty } :: vs) out).isSome = true} : have tctx := ctx.tctx; let v' := { id := n, ty := ty }; have vs' := v' :: ctx.tctx.vs; have tctx' := { vs := vs', ufs := ctx.tctx.ufs }; ((tdi : TermDenoteInput { sctx := ctx.sctx, tctx := tctx' }) → (denoteFunSort ctx.sctx vs out).get hTys { sΓ := tdi.sΓ, hsΓ := ⋯ }) → (tdi : TermDenoteInput { sctx := ctx.sctx, tctx := tctx }) → (denoteFunSort ctx.sctx (v' :: vs) out).get hTyTys { sΓ := tdi.sΓ, hsΓ := ⋯ }

Lambda-lift one IF-body argument binder into an arrow in the resulting function.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def buildIFBody {out : Strata.SMT.TermType} {vs : List Strata.SMT.TermVar} (ctx : Context) {hTys : (denoteFunSort ctx.sctx vs out).isSome = true} {hTy : (denoteSort ctx.sctx out).isSome = true} (bodyFt : (tdi : TermDenoteInput { sctx := ctx.sctx, tctx := { vs := vs.reverse ++ ctx.tctx.vs, ufs := ctx.tctx.ufs } }) → (denoteSort ctx.sctx out).get hTy { sΓ := tdi.sΓ, hsΓ := ⋯ }) (tdi : TermDenoteInput ctx) : (denoteFunSort ctx.sctx vs out).get hTys { sΓ := tdi.sΓ, hsΓ := ⋯ }

Turn a denoted IF body (under its argument binders) into a denoted function.

Equations

• One or more equations did not get rendered due to their size.
• buildIFBody ctx bodyFt_2 tdi = bodyFt_2 tdi

noncomputable def bindIF {n : String} {args : List Strata.SMT.TermVar} {out : Strata.SMT.TermType} (body : Strata.SMT.Term) (ctx : Context) (ft' : have uf' := { id := n, args := args, out := out }; have ufs' := uf' :: ctx.tctx.ufs; have tctx' := { vs := ctx.tctx.vs, ufs := ufs' }; TermDenoteInput { sctx := ctx.sctx, tctx := tctx' } → Prop) : Option (TermDenoteInput ctx → Prop)

Eliminate one interpreted-function declaration from the term context.

ft' expects a context where the function symbol (n : args -> out) is available in tctx.ufs. This combinator constructs the semantic function by denoting body, pushes that interpretation into the environment, and returns a proposition over the original (smaller) context.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def denoteBoolTermFromContext (uss : USContext) (iss : ISContext) (ufs : UFContext) (ifs : List Core.SMT.IF) (t : Strata.SMT.Term) : Option (PLift Prop)

Interpret a closed boolean term under SMT declarations.

denoteTerm is context-parametric: it interprets a term relative to explicit sort/term contexts and semantic environments. This function "closes" that interpretation by successively eliminating context binders (IF, UF, sort aliases, uninterpreted sorts) and then evaluating in the empty environment.

It is boolean-specific because SMT queries denote propositions.

Equations

• One or more equations did not get rendered due to their size.

def mkISContext (iss : Map String Strata.SMT.TermType) : ISContext

Equations

• mkISContext iss = mkISContext.go✝ ∅ iss

noncomputable def denoteQuery (ctx : Core.SMT.Context) (assums : List Strata.SMT.Term) (conc : Strata.SMT.Term) : Option Prop

Interpret an SMT query by universally quantifying assumptions and returning the semantic proposition.

Equations

• One or more equations did not get rendered due to their size.