Basic properties of well-formed interpretations

This file proves basic lemmas about well-formedness predicate on interpretations.

theorem Cedar.Thm.wf_interpretation_implies_wfl_var {εs : SymCC.SymEntities} {I : SymCC.Interpretation} {v : SymCC.TermVar} : I.WellFormed εs → SymCC.TermVar.WellFormed εs v → SymCC.Term.WellFormedLiteral εs (I.vars v)

theorem Cedar.Thm.wf_interpretation_implies_wf_var {εs : SymCC.SymEntities} {I : SymCC.Interpretation} {v : SymCC.TermVar} : I.WellFormed εs → SymCC.TermVar.WellFormed εs v → SymCC.Term.WellFormed εs (I.vars v)

theorem Cedar.Thm.wf_interpretation_implies_typeOf_var {εs : SymCC.SymEntities} {I : SymCC.Interpretation} {v : SymCC.TermVar} : I.WellFormed εs → SymCC.TermVar.WellFormed εs v → (I.vars v).typeOf = v.ty

theorem Cedar.Thm.wf_interpretation_implies_wf_udf {εs : SymCC.SymEntities} {I : SymCC.Interpretation} {f : SymCC.UUF} : I.WellFormed εs → SymCC.UUF.WellFormed εs f → SymCC.UDF.WellFormed εs (I.funs f) ∧ (I.funs f).arg = f.arg ∧ (I.funs f).out = f.out

theorem Cedar.Thm.wf_interpretation_implies_wfp_option_get {εs : SymCC.SymEntities} {I : SymCC.Interpretation} {t : SymCC.Term} {ty : SymCC.TermType} : I.WellFormed εs → SymCC.TermType.WellFormed εs ty → t = SymCC.Term.app SymCC.Op.option.get [SymCC.Term.none ty] ty → SymCC.Term.WellFormedLiteral εs (I.partials t) ∧ (I.partials t).typeOf = ty

theorem Cedar.Thm.wf_interpretation_implies_wfp_ext_ipaddr_addrV4 {εs : SymCC.SymEntities} {I : SymCC.Interpretation} {t : SymCC.Term} (v6 : Spec.Ext.IPAddr.IPv6Addr) (p6 : Spec.Ext.IPAddr.IPv6Prefix) : I.WellFormed εs → t = SymCC.Term.app (SymCC.Op.ext SymCC.ExtOp.ipaddr.addrV4) [SymCC.Term.prim (SymCC.TermPrim.ext (Spec.Ext.ipaddr (Spec.Ext.IPAddr.IPNet.V6 { addr := v6, pre := p6 })))] (SymCC.TermType.bitvec 32) → SymCC.Term.WellFormedLiteral εs (I.partials t) ∧ (I.partials t).typeOf = SymCC.TermType.bitvec 32

theorem Cedar.Thm.wf_interpretation_implies_wfp_ext_ipaddr_prefixV4 {εs : SymCC.SymEntities} {I : SymCC.Interpretation} {t : SymCC.Term} (v6 : Spec.Ext.IPAddr.IPv6Addr) (p6 : Spec.Ext.IPAddr.IPv6Prefix) : I.WellFormed εs → t = SymCC.Term.app (SymCC.Op.ext SymCC.ExtOp.ipaddr.prefixV4) [SymCC.Term.prim (SymCC.TermPrim.ext (Spec.Ext.ipaddr (Spec.Ext.IPAddr.IPNet.V6 { addr := v6, pre := p6 })))] (SymCC.TermType.bitvec 5).option → SymCC.Term.WellFormedLiteral εs (I.partials t) ∧ (I.partials t).typeOf = (SymCC.TermType.bitvec 5).option

theorem Cedar.Thm.wf_interpretation_implies_wfp_ext_ipaddr_addrV6 {εs : SymCC.SymEntities} {I : SymCC.Interpretation} {t : SymCC.Term} (v4 : Spec.Ext.IPAddr.IPv4Addr) (p4 : Spec.Ext.IPAddr.IPv4Prefix) : I.WellFormed εs → t = SymCC.Term.app (SymCC.Op.ext SymCC.ExtOp.ipaddr.addrV6) [SymCC.Term.prim (SymCC.TermPrim.ext (Spec.Ext.ipaddr (Spec.Ext.IPAddr.IPNet.V4 { addr := v4, pre := p4 })))] (SymCC.TermType.bitvec 128) → SymCC.Term.WellFormedLiteral εs (I.partials t) ∧ (I.partials t).typeOf = SymCC.TermType.bitvec 128

theorem Cedar.Thm.wf_interpretation_implies_wfp_ext_ipaddr_prefixV6 {εs : SymCC.SymEntities} {I : SymCC.Interpretation} {t : SymCC.Term} (v4 : Spec.Ext.IPAddr.IPv4Addr) (p4 : Spec.Ext.IPAddr.IPv4Prefix) : I.WellFormed εs → t = SymCC.Term.app (SymCC.Op.ext SymCC.ExtOp.ipaddr.prefixV6) [SymCC.Term.prim (SymCC.TermPrim.ext (Spec.Ext.ipaddr (Spec.Ext.IPAddr.IPNet.V4 { addr := v4, pre := p4 })))] (SymCC.TermType.bitvec 7).option → SymCC.Term.WellFormedLiteral εs (I.partials t) ∧ (I.partials t).typeOf = (SymCC.TermType.bitvec 7).option