Theorems that Value.symbolizer? produces well-formed, well-typed literals.

@[irreducible]

theorem Cedar.Thm.value_symbolize?_well_typed {Γ : Validation.TypeEnv} {v : Spec.Value} {ty : Validation.CedarType} {t : SymCC.Term} (hwf_ty : Validation.CedarType.WellFormed Γ ty) (hwt_v : InstanceOfType Γ v ty) (hsym : v.symbolize? ty = some t) : t.typeOf = SymCC.TermType.ofType ty

The results of symbolize? has the correct type.

theorem Cedar.Thm.value_symbolize?_not_none {v : Spec.Value} {ty : Validation.CedarType} {t : SymCC.Term} {ty' : SymCC.TermType} (hsome : v.symbolize? ty = some t) : t ≠ SymCC.Term.none ty'

The results of symbolize? is not Term.none.

theorem Cedar.Thm.value_symbolize?_not_some {v : Spec.Value} {ty : Validation.CedarType} {t t' : SymCC.Term} (hsome : v.symbolize? ty = some t) : t ≠ t'.some

The results of symbolize? is not Term.some.

@[irreducible]

theorem Cedar.Thm.value_symbolize?_wf {Γ : Validation.TypeEnv} {env : Spec.Env} {v : Spec.Value} {ty : Validation.CedarType} {t : SymCC.Term} (hinst : InstanceOfWellFormedEnvironment env.request env.entities Γ) (hwf_ty : Validation.CedarType.WellFormed Γ ty) (hwf_v : Spec.Value.WellFormed env.entities v) (hwt_v : InstanceOfType Γ v ty) (hsym : v.symbolize? ty = some t) : SymCC.Term.WellFormed (SymCC.SymEnv.ofEnv Γ).entities t

The results of symbolize? is well-formed.

@[irreducible]

theorem Cedar.Thm.value?_symbolize?_id {Γ : Validation.TypeEnv} {entities : Spec.Entities} {v : Spec.Value} {ty : Validation.CedarType} (hwf_Γ : Γ.WellFormed) (hwf_ty : Validation.CedarType.WellFormed Γ ty) (hwf_v : Spec.Value.WellFormed entities v) (hwt_v : InstanceOfType Γ v ty) : ∃ (t : SymCC.Term), v.symbolize? ty = some t ∧ t.value? = some v

symbolize? is the right inverse of value?, on sufficiently well-formed inputs

@[irreducible]

theorem Cedar.Thm.value_symbolize?_is_lit {v : Spec.Value} {ty : Validation.CedarType} {t : SymCC.Term} (hsym : v.symbolize? ty = some t) : t.isLiteral = true