Documentation

Cedar.Thm.SymCC.Term.PE

Basic properties of partial evaluation of terms #

This file proves basic lemmas about the Factory functions on terms when applied to literal (concrete) inputs. #

PE for Factory.not #

source
@[simp]
theorem Cedar.Thm.pe_not_true :
SymCC.Factory.not (SymCC.Term.prim (SymCC.TermPrim.bool true)) = SymCC.Term.prim (SymCC.TermPrim.bool false)
source
@[simp]
theorem Cedar.Thm.pe_not_false :
SymCC.Factory.not (SymCC.Term.prim (SymCC.TermPrim.bool false)) = SymCC.Term.prim (SymCC.TermPrim.bool true)
source
theorem Cedar.Thm.pe_not_lit {b : Bool} :
SymCC.Factory.not (SymCC.Term.prim (SymCC.TermPrim.bool b)) = SymCC.Term.prim (SymCC.TermPrim.bool !b)
source
theorem Cedar.Thm.pe_not_wfl {εs : SymCC.SymEntities} {t : SymCC.Term} :
SymCC.Term.WellFormedLiteral εs t → t.typeOf = SymCC.TermType.bool → (SymCC.Factory.not t).isLiteral = true

PE for Factory.and #

source
theorem Cedar.Thm.pe_and_wfl {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} :
SymCC.Term.WellFormedLiteral εs t₁ → t₁.typeOf = SymCC.TermType.bool → SymCC.Term.WellFormedLiteral εs t₂ → t₂.typeOf = SymCC.TermType.bool → (SymCC.Factory.and t₁ t₂).isLiteral = true
source
@[simp]
theorem Cedar.Thm.pe_and_false_left {t : SymCC.Term} :
SymCC.Factory.and (SymCC.Term.prim (SymCC.TermPrim.bool false)) t = SymCC.Term.prim (SymCC.TermPrim.bool false)
source
@[simp]
theorem Cedar.Thm.pe_and_false_right {t : SymCC.Term} :
SymCC.Factory.and t (SymCC.Term.prim (SymCC.TermPrim.bool false)) = SymCC.Term.prim (SymCC.TermPrim.bool false)
source
@[simp]
theorem Cedar.Thm.pe_and_true_left {t : SymCC.Term} :
SymCC.Factory.and (SymCC.Term.prim (SymCC.TermPrim.bool true)) t = t
source
@[simp]
theorem Cedar.Thm.pe_and_true_right {t : SymCC.Term} :
SymCC.Factory.and t (SymCC.Term.prim (SymCC.TermPrim.bool true)) = t
source
@[simp]
theorem Cedar.Thm.pe_and_true_iff_true {t₁ t₂ : SymCC.Term} :
SymCC.Factory.and t₁ t₂ = SymCC.Term.prim (SymCC.TermPrim.bool true) ↔ t₁ = SymCC.Term.prim (SymCC.TermPrim.bool true) ∧ t₂ = SymCC.Term.prim (SymCC.TermPrim.bool true)

PE for Factory.or #

source
theorem Cedar.Thm.pe_or_wfl {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} :
SymCC.Term.WellFormedLiteral εs t₁ → t₁.typeOf = SymCC.TermType.bool → SymCC.Term.WellFormedLiteral εs t₂ → t₂.typeOf = SymCC.TermType.bool → (SymCC.Factory.or t₁ t₂).isLiteral = true
source
@[simp]
theorem Cedar.Thm.pe_or_true_left {t : SymCC.Term} :
SymCC.Factory.or (SymCC.Term.prim (SymCC.TermPrim.bool true)) t = SymCC.Term.prim (SymCC.TermPrim.bool true)
source
@[simp]
theorem Cedar.Thm.pe_or_true_right {t : SymCC.Term} :
SymCC.Factory.or t (SymCC.Term.prim (SymCC.TermPrim.bool true)) = SymCC.Term.prim (SymCC.TermPrim.bool true)
source
@[simp]
theorem Cedar.Thm.pe_or_false_left {t : SymCC.Term} :
SymCC.Factory.or (SymCC.Term.prim (SymCC.TermPrim.bool false)) t = t
source
@[simp]
theorem Cedar.Thm.pe_or_false_right {t : SymCC.Term} :
SymCC.Factory.or t (SymCC.Term.prim (SymCC.TermPrim.bool false)) = t

PE for Factory.implies #

source
@[simp]
theorem Cedar.Thm.pe_implies_false_left {t : SymCC.Term} :
SymCC.Factory.implies (SymCC.Term.prim (SymCC.TermPrim.bool false)) t = SymCC.Term.prim (SymCC.TermPrim.bool true)
source
@[simp]
theorem Cedar.Thm.pe_implies_true_left {t : SymCC.Term} :
SymCC.Factory.implies (SymCC.Term.prim (SymCC.TermPrim.bool true)) t = t

PE for Factory.ite #

source
@[simp]
theorem Cedar.Thm.pe_ite_true {t₁ t₂ : SymCC.Term} :
SymCC.Factory.ite (SymCC.Term.prim (SymCC.TermPrim.bool true)) t₁ t₂ = t₁
source
@[simp]
theorem Cedar.Thm.pe_ite_false {t₁ t₂ : SymCC.Term} :
SymCC.Factory.ite (SymCC.Term.prim (SymCC.TermPrim.bool false)) t₁ t₂ = t₂
source
theorem Cedar.Thm.pe_ite_wfl {εs : SymCC.SymEntities} {t₁ t₂ t₃ : SymCC.Term} :
SymCC.Term.WellFormedLiteral εs t₁ → SymCC.Term.WellFormedLiteral εs t₂ → SymCC.Term.WellFormedLiteral εs t₃ → t₁.typeOf = SymCC.TermType.bool → (SymCC.Factory.ite t₁ t₂ t₃).isLiteral = true

PE for Factory.eq #

source
theorem Cedar.Thm.pe_eq_simplify_same {t : SymCC.Term} :
SymCC.Factory.eq.simplify t t = SymCC.Term.prim (SymCC.TermPrim.bool true)
source
@[simp]
theorem Cedar.Thm.pe_eq_same {t : SymCC.Term} :
SymCC.Factory.eq t t = SymCC.Term.prim (SymCC.TermPrim.bool true)
source
@[simp]
theorem Cedar.Thm.pe_eq_some_none {t : SymCC.Term} {ty : SymCC.TermType} :
SymCC.Factory.eq t.some (SymCC.Term.none ty) = SymCC.Term.prim (SymCC.TermPrim.bool false)
source
@[simp]
theorem Cedar.Thm.pe_eq_none_some {t : SymCC.Term} {ty : SymCC.TermType} :
SymCC.Factory.eq (SymCC.Term.none ty) t.some = SymCC.Term.prim (SymCC.TermPrim.bool false)
source
theorem Cedar.Thm.pe_eq_some_some {t₁ t₂ : SymCC.Term} :
SymCC.Factory.eq t₁.some t₂.some = SymCC.Factory.eq.simplify t₁ t₂
source
@[simp]
theorem Cedar.Thm.pe_eq_simplify_lit {t₁ t₂ : SymCC.Term} :
t₁.isLiteral = true → t₂.isLiteral = true → (SymCC.Factory.eq.simplify t₁ t₂).isLiteral = true ∧ SymCC.Factory.eq.simplify t₁ t₂ = SymCC.Term.prim (SymCC.TermPrim.bool (t₁ == t₂))
source
theorem Cedar.Thm.pe_eq_lit {t₁ t₂ : SymCC.Term} :
t₁.isLiteral = true → t₂.isLiteral = true → (SymCC.Factory.eq t₁ t₂).isLiteral = true ∧ SymCC.Factory.eq t₁ t₂ = SymCC.Term.prim (SymCC.TermPrim.bool (t₁ == t₂))
source
theorem Cedar.Thm.pe_eq_prim {p₁ p₂ : SymCC.TermPrim} :
SymCC.Factory.eq (SymCC.Term.prim p₁) (SymCC.Term.prim p₂) = SymCC.Term.prim (SymCC.TermPrim.bool (p₁ == p₂))

PE for Factory.option.get and Factory.option.get' #

source
@[simp]
theorem Cedar.Thm.pe_option_get_some {t : SymCC.Term} :
SymCC.Factory.option.get t.some = t
source
@[simp]
theorem Cedar.Thm.pe_option_get'_some {I : SymCC.Interpretation} {t : SymCC.Term} :
SymCC.Factory.option.get' I t.some = t
source
theorem Cedar.Thm.pe_option_get'_wfl {εs : SymCC.SymEntities} {I : SymCC.Interpretation} {t : SymCC.Term} {ty : SymCC.TermType} :
I.WellFormed εs → SymCC.Term.WellFormedLiteral εs t → t.typeOf = ty.option → (SymCC.Factory.option.get' I t).isLiteral = true

PE for Factory.isNone and Factory.isSome #

source
@[simp]
theorem Cedar.Thm.pe_isNone_none {ty : SymCC.TermType} :
SymCC.Factory.isNone (SymCC.Term.none ty) = SymCC.Term.prim (SymCC.TermPrim.bool true)
source
@[simp]
theorem Cedar.Thm.pe_isNone_some {t : SymCC.Term} :
SymCC.Factory.isNone t.some = SymCC.Term.prim (SymCC.TermPrim.bool false)
source
@[simp]
theorem Cedar.Thm.pe_isSome_none {ty : SymCC.TermType} :
SymCC.Factory.isSome (SymCC.Term.none ty) = SymCC.Term.prim (SymCC.TermPrim.bool false)
source
@[simp]
theorem Cedar.Thm.pe_isSome_some {t : SymCC.Term} :
SymCC.Factory.isSome t.some = SymCC.Term.prim (SymCC.TermPrim.bool true)

PE for Factory.ifSome #

source
theorem Cedar.Thm.pe_ifSome_none {t : SymCC.Term} {gty tty : SymCC.TermType} :
t.typeOf = tty.option → SymCC.Factory.ifSome (SymCC.Term.none gty) t = SymCC.Term.none tty
source
theorem Cedar.Thm.pe_ifSome_some {g t : SymCC.Term} {tty : SymCC.TermType} :
t.typeOf = tty.option → SymCC.Factory.ifSome g.some t = t
source
theorem Cedar.Thm.pe_ifSome_get_eq_get' {εs : SymCC.SymEntities} (I : SymCC.Interpretation) {t : SymCC.Term} {ty ty' : SymCC.TermType} (f : SymCC.Term → SymCC.Term) :
SymCC.Term.WellFormedLiteral εs t → t.typeOf = ty.option → (f (SymCC.Factory.option.get t)).typeOf = ty'.option → (f (SymCC.Factory.option.get' I t)).typeOf = ty'.option → SymCC.Factory.ifSome t (f (SymCC.Factory.option.get t)) = SymCC.Factory.ifSome t (f (SymCC.Factory.option.get' I t))
source
theorem Cedar.Thm.pe_ifSome_get_eq_get'₂ {εs : SymCC.SymEntities} (I : SymCC.Interpretation) {t₁ t₂ : SymCC.Term} {ty₁ ty₂ ty₃ : SymCC.TermType} (f : SymCC.Term → SymCC.Term → SymCC.Term) (hwφ₁ : SymCC.Term.WellFormedLiteral εs t₁ ∧ t₁.typeOf = ty₁.option) (hwφ₂ : SymCC.Term.WellFormedLiteral εs t₂ ∧ t₂.typeOf = ty₂.option) (hty₁ : (f (SymCC.Factory.option.get t₁) (SymCC.Factory.option.get t₂)).typeOf = ty₃.option) (hty₂ : (f (SymCC.Factory.option.get' I t₁) (SymCC.Factory.option.get' I t₂)).typeOf = ty₃.option) :
SymCC.Factory.ifSome t₁ (SymCC.Factory.ifSome t₂ (f (SymCC.Factory.option.get t₁) (SymCC.Factory.option.get t₂))) = SymCC.Factory.ifSome t₁ (SymCC.Factory.ifSome t₂ (f (SymCC.Factory.option.get' I t₁) (SymCC.Factory.option.get' I t₂)))
source
theorem Cedar.Thm.pe_ifSome_ok_get_eq_get' {εs : SymCC.SymEntities} (I : SymCC.Interpretation) {t₁ t₂ t₃ : SymCC.Term} {ty₁ ty₂ : SymCC.TermType} (f : SymCC.Term → SymCC.Result SymCC.Term) (hwφ₁ : SymCC.Term.WellFormedLiteral εs t₁ ∧ t₁.typeOf = ty₁.option) (hty₂ : t₂.typeOf = ty₂.option) (hty₃ : t₃.typeOf = ty₂.option) (hok₂ : f (SymCC.Factory.option.get' I t₁) = Except.ok t₂) (hok₃ : f (SymCC.Factory.option.get t₁) = Except.ok t₃) :
SymCC.Factory.ifSome t₁ t₃ = SymCC.Factory.ifSome t₁ t₂
source
theorem Cedar.Thm.pe_ifSome_ok_get_eq_get'₂ {εs : SymCC.SymEntities} (I : SymCC.Interpretation) {t₁ t₂ t₃ t₄ : SymCC.Term} {ty₁ ty₂ ty₃ : SymCC.TermType} (f : SymCC.Term → SymCC.Term → SymCC.Result SymCC.Term) (hwφ₁ : SymCC.Term.WellFormedLiteral εs t₁ ∧ t₁.typeOf = ty₁.option) (hwφ₂ : SymCC.Term.WellFormedLiteral εs t₂ ∧ t₂.typeOf = ty₂.option) (hty₃ : t₃.typeOf = ty₃.option) (hty₄ : t₄.typeOf = ty₃.option) (hok₃ : f (SymCC.Factory.option.get' I t₁) (SymCC.Factory.option.get' I t₂) = Except.ok t₃) (hok₄ : f (SymCC.Factory.option.get t₁) (SymCC.Factory.option.get t₂) = Except.ok t₄) :
SymCC.Factory.ifSome t₁ (SymCC.Factory.ifSome t₂ t₄) = SymCC.Factory.ifSome t₁ (SymCC.Factory.ifSome t₂ t₃)

PE for Factory.anyNone and Factory.ifAllSome #

source
theorem Cedar.Thm.pe_wfls_of_type_option {εs : SymCC.SymEntities} {ts : List SymCC.Term} (hwφ : ∀ (t : SymCC.Term), t ∈ ts → SymCC.Term.WellFormedLiteral εs t ∧ ∃ (ty : SymCC.TermType), t.typeOf = ty.option) :
(∃ (ty : SymCC.TermType), SymCC.Term.none ty ∈ ts) ∨ ∃ (ts' : List SymCC.Term), ts = List.map SymCC.Term.some ts'
source
theorem Cedar.Thm.pe_anyTrue_true {f : SymCC.Term → SymCC.Term} {ts : List SymCC.Term} {t : SymCC.Term} :
t ∈ ts → f t = SymCC.Term.prim (SymCC.TermPrim.bool true) → SymCC.Factory.anyTrue f ts = SymCC.Term.prim (SymCC.TermPrim.bool true)
source
theorem Cedar.Thm.pe_anyTrue_false {f : SymCC.Term → SymCC.Term} {ts : List SymCC.Term} :
(∀ (t : SymCC.Term), t ∈ ts → f t = SymCC.Term.prim (SymCC.TermPrim.bool false)) → SymCC.Factory.anyTrue f ts = SymCC.Term.prim (SymCC.TermPrim.bool false)
source
theorem Cedar.Thm.pe_anyNone_true {ts : List SymCC.Term} {ty : SymCC.TermType} :
SymCC.Term.none ty ∈ ts → SymCC.Factory.anyNone ts = SymCC.Term.prim (SymCC.TermPrim.bool true)
source
theorem Cedar.Thm.pe_anyNone_false {ts : List SymCC.Term} :
SymCC.Factory.anyNone (List.map SymCC.Term.some ts) = SymCC.Term.prim (SymCC.TermPrim.bool false)
source
theorem Cedar.Thm.pe_ifAllSome_none {ts : List SymCC.Term} {t : SymCC.Term} {ty₁ ty₂ : SymCC.TermType} :
SymCC.Term.none ty₁ ∈ ts → t.typeOf = ty₂.option → SymCC.Factory.ifAllSome ts t = SymCC.Term.none ty₂
source
theorem Cedar.Thm.pe_ifAllSome_some {ts : List SymCC.Term} {t : SymCC.Term} {ty : SymCC.TermType} :
t.typeOf = ty.option → SymCC.Factory.ifAllSome (List.map SymCC.Term.some ts) t = t

PE for Factory.ifFalse and Factory.ifTrue #

source
@[simp]
theorem Cedar.Thm.pe_ifFalse_true {t : SymCC.Term} :
SymCC.Factory.ifFalse (SymCC.Term.prim (SymCC.TermPrim.bool true)) t = SymCC.Term.none t.typeOf
source
@[simp]
theorem Cedar.Thm.pe_ifFalse_false {t : SymCC.Term} :
SymCC.Factory.ifFalse (SymCC.Term.prim (SymCC.TermPrim.bool false)) t = t.some
source
@[simp]
theorem Cedar.Thm.pe_ifTrue_true {t : SymCC.Term} :
SymCC.Factory.ifTrue (SymCC.Term.prim (SymCC.TermPrim.bool true)) t = t.some
source
@[simp]
theorem Cedar.Thm.pe_ifTrue_false {t : SymCC.Term} :
SymCC.Factory.ifTrue (SymCC.Term.prim (SymCC.TermPrim.bool false)) t = SymCC.Term.none t.typeOf

PE for Factory.app #

source
theorem Cedar.Thm.pe_app_wfl {εs : SymCC.SymEntities} {f : SymCC.UDF} {t : SymCC.Term} :
SymCC.Term.WellFormedLiteral εs t → SymCC.UDF.WellFormed εs f → (SymCC.Factory.app (SymCC.UnaryFunction.udf f) t).isLiteral = true

PE for Factory bitvector operators #

source
theorem Cedar.Thm.pe_bvneg_wfl {εs : SymCC.SymEntities} {t : SymCC.Term} {n : Nat} :
SymCC.Term.WellFormedLiteral εs t → t.typeOf = SymCC.TermType.bitvec n → (SymCC.Factory.bvneg t).isLiteral = true
source
theorem Cedar.Thm.pe_bvnego_wfl {εs : SymCC.SymEntities} {t : SymCC.Term} {n : Nat} :
SymCC.Term.WellFormedLiteral εs t → t.typeOf = SymCC.TermType.bitvec n → (SymCC.Factory.bvnego t).isLiteral = true
source
theorem Cedar.Thm.pe_zero_extend_wfl {εs : SymCC.SymEntities} {t : SymCC.Term} {n m : Nat} :
SymCC.Term.WellFormedLiteral εs t → t.typeOf = SymCC.TermType.bitvec m → (SymCC.Factory.zero_extend n t).isLiteral = true
source
theorem Cedar.Thm.pe_bvadd_wfl {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} :
SymCC.Term.WellFormedLiteral εs t₁ → t₁.typeOf = SymCC.TermType.bitvec n → SymCC.Term.WellFormedLiteral εs t₂ → t₂.typeOf = SymCC.TermType.bitvec n → (SymCC.Factory.bvadd t₁ t₂).isLiteral = true
source
theorem Cedar.Thm.pe_bvsub_wfl {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} :
SymCC.Term.WellFormedLiteral εs t₁ → t₁.typeOf = SymCC.TermType.bitvec n → SymCC.Term.WellFormedLiteral εs t₂ → t₂.typeOf = SymCC.TermType.bitvec n → (SymCC.Factory.bvsub t₁ t₂).isLiteral = true
source
theorem Cedar.Thm.pe_bvmul_wfl {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} :
SymCC.Term.WellFormedLiteral εs t₁ → t₁.typeOf = SymCC.TermType.bitvec n → SymCC.Term.WellFormedLiteral εs t₂ → t₂.typeOf = SymCC.TermType.bitvec n → (SymCC.Factory.bvmul t₁ t₂).isLiteral = true
source
theorem Cedar.Thm.pe_bvsdiv_wfl {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} :
SymCC.Term.WellFormedLiteral εs t₁ → t₁.typeOf = SymCC.TermType.bitvec n → SymCC.Term.WellFormedLiteral εs t₂ → t₂.typeOf = SymCC.TermType.bitvec n → (SymCC.Factory.bvsdiv t₁ t₂).isLiteral = true
source
theorem Cedar.Thm.pe_bvudiv_wfl {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} :
SymCC.Term.WellFormedLiteral εs t₁ → t₁.typeOf = SymCC.TermType.bitvec n → SymCC.Term.WellFormedLiteral εs t₂ → t₂.typeOf = SymCC.TermType.bitvec n → (SymCC.Factory.bvudiv t₁ t₂).isLiteral = true
source
theorem Cedar.Thm.pe_bvsrem_wfl {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} :
SymCC.Term.WellFormedLiteral εs t₁ → t₁.typeOf = SymCC.TermType.bitvec n → SymCC.Term.WellFormedLiteral εs t₂ → t₂.typeOf = SymCC.TermType.bitvec n → (SymCC.Factory.bvsrem t₁ t₂).isLiteral = true
source
theorem Cedar.Thm.pe_bvsmod_wfl {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} :
SymCC.Term.WellFormedLiteral εs t₁ → t₁.typeOf = SymCC.TermType.bitvec n → SymCC.Term.WellFormedLiteral εs t₂ → t₂.typeOf = SymCC.TermType.bitvec n → (SymCC.Factory.bvsmod t₁ t₂).isLiteral = true
source
theorem Cedar.Thm.pe_bvurem_wfl {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} :
SymCC.Term.WellFormedLiteral εs t₁ → t₁.typeOf = SymCC.TermType.bitvec n → SymCC.Term.WellFormedLiteral εs t₂ → t₂.typeOf = SymCC.TermType.bitvec n → (SymCC.Factory.bvurem t₁ t₂).isLiteral = true
source
theorem Cedar.Thm.pe_bvshl_wfl {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} :
SymCC.Term.WellFormedLiteral εs t₁ → t₁.typeOf = SymCC.TermType.bitvec n → SymCC.Term.WellFormedLiteral εs t₂ → t₂.typeOf = SymCC.TermType.bitvec n → (SymCC.Factory.bvshl t₁ t₂).isLiteral = true
source
theorem Cedar.Thm.pe_bvlshr_wfl {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} :
SymCC.Term.WellFormedLiteral εs t₁ → t₁.typeOf = SymCC.TermType.bitvec n → SymCC.Term.WellFormedLiteral εs t₂ → t₂.typeOf = SymCC.TermType.bitvec n → (SymCC.Factory.bvlshr t₁ t₂).isLiteral = true
source
theorem Cedar.Thm.pe_bvslt_wfl {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} :
SymCC.Term.WellFormedLiteral εs t₁ → t₁.typeOf = SymCC.TermType.bitvec n → SymCC.Term.WellFormedLiteral εs t₂ → t₂.typeOf = SymCC.TermType.bitvec n → (SymCC.Factory.bvslt t₁ t₂).isLiteral = true
source
theorem Cedar.Thm.pe_bvsle_wfl {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} :
SymCC.Term.WellFormedLiteral εs t₁ → t₁.typeOf = SymCC.TermType.bitvec n → SymCC.Term.WellFormedLiteral εs t₂ → t₂.typeOf = SymCC.TermType.bitvec n → (SymCC.Factory.bvsle t₁ t₂).isLiteral = true
source
theorem Cedar.Thm.pe_bvult_wfl {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} :
SymCC.Term.WellFormedLiteral εs t₁ → t₁.typeOf = SymCC.TermType.bitvec n → SymCC.Term.WellFormedLiteral εs t₂ → t₂.typeOf = SymCC.TermType.bitvec n → (SymCC.Factory.bvult t₁ t₂).isLiteral = true
source
theorem Cedar.Thm.pe_bvule_wfl {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} :
SymCC.Term.WellFormedLiteral εs t₁ → t₁.typeOf = SymCC.TermType.bitvec n → SymCC.Term.WellFormedLiteral εs t₂ → t₂.typeOf = SymCC.TermType.bitvec n → (SymCC.Factory.bvule t₁ t₂).isLiteral = true
source
theorem Cedar.Thm.pe_bvsaddo_wfl {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} :
SymCC.Term.WellFormedLiteral εs t₁ → t₁.typeOf = SymCC.TermType.bitvec n → SymCC.Term.WellFormedLiteral εs t₂ → t₂.typeOf = SymCC.TermType.bitvec n → (SymCC.Factory.bvsaddo t₁ t₂).isLiteral = true
source
theorem Cedar.Thm.pe_bvssubo_wfl {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} :
SymCC.Term.WellFormedLiteral εs t₁ → t₁.typeOf = SymCC.TermType.bitvec n → SymCC.Term.WellFormedLiteral εs t₂ → t₂.typeOf = SymCC.TermType.bitvec n → (SymCC.Factory.bvssubo t₁ t₂).isLiteral = true
source
theorem Cedar.Thm.pe_bvsmulo_wfl {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} :
SymCC.Term.WellFormedLiteral εs t₁ → t₁.typeOf = SymCC.TermType.bitvec n → SymCC.Term.WellFormedLiteral εs t₂ → t₂.typeOf = SymCC.TermType.bitvec n → (SymCC.Factory.bvsmulo t₁ t₂).isLiteral = true
source
@[simp]
theorem Cedar.Thm.pe_bvadd {n : Nat} {bv₁ bv₂ : BitVec n} :
SymCC.Factory.bvadd (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₁)) (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₂)) = SymCC.Term.prim (SymCC.TermPrim.bitvec (bv₁.add bv₂))
source
@[simp]
theorem Cedar.Thm.pe_bvsub {n : Nat} {bv₁ bv₂ : BitVec n} :
SymCC.Factory.bvsub (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₁)) (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₂)) = SymCC.Term.prim (SymCC.TermPrim.bitvec (bv₁.sub bv₂))
source
@[simp]
theorem Cedar.Thm.pe_bvmul {n : Nat} {bv₁ bv₂ : BitVec n} :
SymCC.Factory.bvmul (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₁)) (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₂)) = SymCC.Term.prim (SymCC.TermPrim.bitvec (bv₁.mul bv₂))
source
@[simp]
theorem Cedar.Thm.pe_bvsdiv {n : Nat} {bv₁ bv₂ : BitVec n} :
SymCC.Factory.bvsdiv (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₁)) (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₂)) = SymCC.Term.prim (SymCC.TermPrim.bitvec (bv₁.smtSDiv bv₂))
source
@[simp]
theorem Cedar.Thm.pe_bvudiv {n : Nat} {bv₁ bv₂ : BitVec n} :
SymCC.Factory.bvudiv (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₁)) (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₂)) = SymCC.Term.prim (SymCC.TermPrim.bitvec (bv₁.smtUDiv bv₂))
source
@[simp]
theorem Cedar.Thm.pe_bvsrem {n : Nat} {bv₁ bv₂ : BitVec n} :
SymCC.Factory.bvsrem (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₁)) (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₂)) = SymCC.Term.prim (SymCC.TermPrim.bitvec (bv₁.srem bv₂))
source
@[simp]
theorem Cedar.Thm.pe_bvsmod {n : Nat} {bv₁ bv₂ : BitVec n} :
SymCC.Factory.bvsmod (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₁)) (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₂)) = SymCC.Term.prim (SymCC.TermPrim.bitvec (bv₁.smod bv₂))
source
@[simp]
theorem Cedar.Thm.pe_bvurem {n : Nat} {bv₁ bv₂ : BitVec n} :
SymCC.Factory.bvurem (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₁)) (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₂)) = SymCC.Term.prim (SymCC.TermPrim.bitvec (bv₁.umod bv₂))
source
@[simp]
theorem Cedar.Thm.pe_bvlshr {n : Nat} {bv₁ bv₂ : BitVec n} :
SymCC.Factory.bvlshr (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₁)) (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₂)) = SymCC.Term.prim (SymCC.TermPrim.bitvec (bv₁ >>> bv₂))
source
@[simp]
theorem Cedar.Thm.pe_bvshl {n : Nat} {bv₁ bv₂ : BitVec n} :
SymCC.Factory.bvshl (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₁)) (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₂)) = SymCC.Term.prim (SymCC.TermPrim.bitvec (bv₁ <<< bv₂))
source
@[simp]
theorem Cedar.Thm.pe_bvsaddo {n : Nat} {bv₁ bv₂ : BitVec n} :
SymCC.Factory.bvsaddo (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₁)) (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₂)) = SymCC.Term.prim (SymCC.TermPrim.bool (BitVec.overflows n (bv₁.toInt + bv₂.toInt)))
source
@[simp]
theorem Cedar.Thm.pe_bvssubo {n : Nat} {bv₁ bv₂ : BitVec n} :
SymCC.Factory.bvssubo (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₁)) (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₂)) = SymCC.Term.prim (SymCC.TermPrim.bool (BitVec.overflows n (bv₁.toInt - bv₂.toInt)))
source
@[simp]
theorem Cedar.Thm.pe_bvsmulo {n : Nat} {bv₁ bv₂ : BitVec n} :
SymCC.Factory.bvsmulo (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₁)) (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₂)) = SymCC.Term.prim (SymCC.TermPrim.bool (BitVec.overflows n (bv₁.toInt * bv₂.toInt)))
source
theorem Cedar.Thm.pe_zero_extend {k n : Nat} {bv : BitVec k} :
k ≤ n → SymCC.Factory.zero_extend (n - k) (SymCC.Term.prim (SymCC.TermPrim.bitvec bv)) = SymCC.Term.prim (SymCC.TermPrim.bitvec (BitVec.zeroExtend n bv))
source
@[simp]
theorem Cedar.Thm.pe_bvslt {n : Nat} {bv₁ bv₂ : BitVec n} :
SymCC.Factory.bvslt (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₁)) (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₂)) = SymCC.Term.prim (SymCC.TermPrim.bool (bv₁.slt bv₂))
source
@[simp]
theorem Cedar.Thm.pe_bvsle {n : Nat} {bv₁ bv₂ : BitVec n} :
SymCC.Factory.bvsle (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₁)) (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₂)) = SymCC.Term.prim (SymCC.TermPrim.bool (bv₁.sle bv₂))
source
@[simp]
theorem Cedar.Thm.pe_bvule {n : Nat} {bv₁ bv₂ : BitVec n} :
SymCC.Factory.bvule (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₁)) (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₂)) = SymCC.Term.prim (SymCC.TermPrim.bool (bv₁.ule bv₂))
source
theorem Cedar.Thm.pe_bvaddChecked_wfl {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} :
SymCC.Term.WellFormedLiteral εs t₁ → t₁.typeOf = SymCC.TermType.bitvec n → SymCC.Term.WellFormedLiteral εs t₂ → t₂.typeOf = SymCC.TermType.bitvec n → (SymCC.Factory.bvaddChecked t₁ t₂).isLiteral = true
source
theorem Cedar.Thm.pe_bvsubChecked_wfl {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} :
SymCC.Term.WellFormedLiteral εs t₁ → t₁.typeOf = SymCC.TermType.bitvec n → SymCC.Term.WellFormedLiteral εs t₂ → t₂.typeOf = SymCC.TermType.bitvec n → (SymCC.Factory.bvsubChecked t₁ t₂).isLiteral = true
source
theorem Cedar.Thm.pe_bvmulChecked_wfl {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {n : Nat} :
SymCC.Term.WellFormedLiteral εs t₁ → t₁.typeOf = SymCC.TermType.bitvec n → SymCC.Term.WellFormedLiteral εs t₂ → t₂.typeOf = SymCC.TermType.bitvec n → (SymCC.Factory.bvmulChecked t₁ t₂).isLiteral = true
source
theorem Cedar.Thm.pe_bvaddChecked_overflow {n : Nat} {bv₁ bv₂ : BitVec n} :
SymCC.Factory.bvsaddo (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₁)) (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₂)) = SymCC.Term.prim (SymCC.TermPrim.bool true) → SymCC.Factory.bvaddChecked (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₁)) (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₂)) = SymCC.Term.none (SymCC.TermType.prim (SymCC.TermPrimType.bitvec n))
source
theorem Cedar.Thm.pe_bvaddChecked_no_overflow {n : Nat} {bv₁ bv₂ : BitVec n} :
SymCC.Factory.bvsaddo (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₁)) (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₂)) = SymCC.Term.prim (SymCC.TermPrim.bool false) → SymCC.Factory.bvaddChecked (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₁)) (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₂)) = (SymCC.Term.prim (SymCC.TermPrim.bitvec (bv₁.add bv₂))).some
source
theorem Cedar.Thm.pe_bvsubChecked_overflow {n : Nat} {bv₁ bv₂ : BitVec n} :
SymCC.Factory.bvssubo (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₁)) (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₂)) = SymCC.Term.prim (SymCC.TermPrim.bool true) → SymCC.Factory.bvsubChecked (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₁)) (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₂)) = SymCC.Term.none (SymCC.TermType.prim (SymCC.TermPrimType.bitvec n))
source
theorem Cedar.Thm.pe_bvsubChecked_no_overflow {n : Nat} {bv₁ bv₂ : BitVec n} :
SymCC.Factory.bvssubo (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₁)) (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₂)) = SymCC.Term.prim (SymCC.TermPrim.bool false) → SymCC.Factory.bvsubChecked (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₁)) (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₂)) = (SymCC.Term.prim (SymCC.TermPrim.bitvec (bv₁.sub bv₂))).some
source
theorem Cedar.Thm.pe_bvmulChecked_overflow {n : Nat} {bv₁ bv₂ : BitVec n} :
SymCC.Factory.bvsmulo (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₁)) (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₂)) = SymCC.Term.prim (SymCC.TermPrim.bool true) → SymCC.Factory.bvmulChecked (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₁)) (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₂)) = SymCC.Term.none (SymCC.TermType.prim (SymCC.TermPrimType.bitvec n))
source
theorem Cedar.Thm.pe_bvmulChecked_no_overflow {n : Nat} {bv₁ bv₂ : BitVec n} :
SymCC.Factory.bvsmulo (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₁)) (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₂)) = SymCC.Term.prim (SymCC.TermPrim.bool false) → SymCC.Factory.bvmulChecked (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₁)) (SymCC.Term.prim (SymCC.TermPrim.bitvec bv₂)) = (SymCC.Term.prim (SymCC.TermPrim.bitvec (bv₁.mul bv₂))).some

PE for Factory string, set, and record operators #

source
theorem Cedar.Thm.pe_string_like_wfl {εs : SymCC.SymEntities} {t : SymCC.Term} {p : Spec.Pattern} :
SymCC.Term.WellFormedLiteral εs t → t.typeOf = SymCC.TermType.string → (SymCC.Factory.string.like t p).isLiteral = true
source
@[simp]
theorem Cedar.Thm.pe_set_isEmpty {s : Data.Set SymCC.Term} {ty : SymCC.TermType} :
SymCC.Factory.set.isEmpty (SymCC.Term.set s ty) = SymCC.Term.prim (SymCC.TermPrim.bool s.isEmpty)
source
theorem Cedar.Thm.pe_set_member {t : SymCC.Term} {s : Data.Set SymCC.Term} {ty : SymCC.TermType} :
(SymCC.Term.set s ty).isLiteral = true → t.isLiteral = true → SymCC.Factory.set.member t (SymCC.Term.set s ty) = SymCC.Term.prim (SymCC.TermPrim.bool (s.contains t))
source
theorem Cedar.Thm.pe_set_member_wfl {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {ty : SymCC.TermType} :
SymCC.Term.WellFormedLiteral εs t₁ → SymCC.Term.WellFormedLiteral εs t₂ → t₂.typeOf = ty.set → (SymCC.Factory.set.member t₁ t₂).isLiteral = true
source
theorem Cedar.Thm.pe_set_subset {s₁ s₂ : Data.Set SymCC.Term} {ty : SymCC.TermType} :
(SymCC.Term.set s₁ ty).isLiteral = true → (SymCC.Term.set s₂ ty).isLiteral = true → SymCC.Factory.set.subset (SymCC.Term.set s₁ ty) (SymCC.Term.set s₂ ty) = SymCC.Term.prim (SymCC.TermPrim.bool (s₁.subset s₂))
source
theorem Cedar.Thm.pe_set_subset_wfl {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {ty : SymCC.TermType} :
SymCC.Term.WellFormedLiteral εs t₁ → t₁.typeOf = ty.set → SymCC.Term.WellFormedLiteral εs t₂ → t₂.typeOf = ty.set → (SymCC.Factory.set.subset t₁ t₂).isLiteral = true
source
theorem Cedar.Thm.pe_set_inter_wfl {εs : SymCC.SymEntities} {t₁ t₂ : SymCC.Term} {ty : SymCC.TermType} :
SymCC.Term.WellFormedLiteral εs t₁ → t₁.typeOf = ty.set → SymCC.Term.WellFormedLiteral εs t₂ → t₂.typeOf = ty.set → (SymCC.Factory.set.inter t₁ t₂).isLiteral = true
source
theorem Cedar.Thm.pe_set_inter {s₁ s₂ : Data.Set SymCC.Term} {ty : SymCC.TermType} :
(SymCC.Term.set s₁ ty).isLiteral = true → (SymCC.Term.set s₂ ty).isLiteral = true → SymCC.Factory.set.inter (SymCC.Term.set s₁ ty) (SymCC.Term.set s₂ ty) = SymCC.Term.set (s₁.intersect s₂) ty
source
theorem Cedar.Thm.pe_set_intersects {s₁ s₂ : Data.Set SymCC.Term} {ty : SymCC.TermType} :
(SymCC.Term.set s₁ ty).isLiteral = true → (SymCC.Term.set s₂ ty).isLiteral = true → SymCC.Factory.set.intersects (SymCC.Term.set s₁ ty) (SymCC.Term.set s₂ ty) = SymCC.Term.prim (SymCC.TermPrim.bool (s₁.intersects s₂))
source
theorem Cedar.Thm.pe_record_get_wfl {εs : SymCC.SymEntities} {a : Spec.Attr} {t : SymCC.Term} {ty : SymCC.TermType} {rty : Data.Map Spec.Attr SymCC.TermType} :
SymCC.Term.WellFormedLiteral εs t → t.typeOf = SymCC.TermType.record rty → rty.find? a = some ty → (SymCC.Factory.record.get t a).isLiteral = true
source
theorem Cedar.Thm.pe_record_get {rt : Data.Map Spec.Attr SymCC.Term} {a : Spec.Attr} {tₐ : SymCC.Term} :
rt.find? a = some tₐ → SymCC.Factory.record.get (SymCC.Term.record rt) a = tₐ

PE for Factory extension operators #

source
theorem Cedar.Thm.pe_ext_decimal_val_wfl {εs : SymCC.SymEntities} {t : SymCC.Term} :
SymCC.Term.WellFormedLiteral εs t → t.typeOf = SymCC.TermType.ext Validation.ExtType.decimal → (SymCC.Factory.ext.decimal.val t).isLiteral = true
source
theorem Cedar.Thm.pe_ext_ipaddr_isV4_wfl {εs : SymCC.SymEntities} {t : SymCC.Term} :
SymCC.Term.WellFormedLiteral εs t → t.typeOf = SymCC.TermType.ext Validation.ExtType.ipAddr → (SymCC.Factory.ext.ipaddr.isV4 t).isLiteral = true
source
theorem Cedar.Thm.pe_ext_ipaddr_addrV4'_wfl {εs : SymCC.SymEntities} {I : SymCC.Interpretation} {t : SymCC.Term} :
I.WellFormed εs → SymCC.Term.WellFormedLiteral εs t → t.typeOf = SymCC.TermType.ext Validation.ExtType.ipAddr → (SymCC.Factory.ext.ipaddr.addrV4' I t).isLiteral = true
source
theorem Cedar.Thm.pe_ext_ipaddr_prefixV4'_wfl {εs : SymCC.SymEntities} {I : SymCC.Interpretation} {t : SymCC.Term} :
I.WellFormed εs → SymCC.Term.WellFormedLiteral εs t → t.typeOf = SymCC.TermType.ext Validation.ExtType.ipAddr → (SymCC.Factory.ext.ipaddr.prefixV4' I t).isLiteral = true
source
theorem Cedar.Thm.pe_ext_ipaddr_addrV6'_wfl {εs : SymCC.SymEntities} {I : SymCC.Interpretation} {t : SymCC.Term} :
I.WellFormed εs → SymCC.Term.WellFormedLiteral εs t → t.typeOf = SymCC.TermType.ext Validation.ExtType.ipAddr → (SymCC.Factory.ext.ipaddr.addrV6' I t).isLiteral = true
source
theorem Cedar.Thm.pe_ext_ipaddr_prefixV6'_wfl {εs : SymCC.SymEntities} {I : SymCC.Interpretation} {t : SymCC.Term} :
I.WellFormed εs → SymCC.Term.WellFormedLiteral εs t → t.typeOf = SymCC.TermType.ext Validation.ExtType.ipAddr → (SymCC.Factory.ext.ipaddr.prefixV6' I t).isLiteral = true
source
theorem Cedar.Thm.pe_ext_datetime_val_wfl {εs : SymCC.SymEntities} {t : SymCC.Term} :
SymCC.Term.WellFormedLiteral εs t → t.typeOf = SymCC.TermType.ext Validation.ExtType.datetime → (SymCC.Factory.ext.datetime.val t).isLiteral = true
source
theorem Cedar.Thm.pe_ext_datetime_ofBitVec_wfl {εs : SymCC.SymEntities} {t : SymCC.Term} :
SymCC.Term.WellFormedLiteral εs t → t.typeOf = SymCC.TermType.prim (SymCC.TermPrimType.bitvec 64) → (SymCC.Factory.ext.datetime.ofBitVec t).isLiteral = true
source
theorem Cedar.Thm.pe_ext_duration_val_wfl {εs : SymCC.SymEntities} {t : SymCC.Term} :
SymCC.Term.WellFormedLiteral εs t → t.typeOf = SymCC.TermType.ext Validation.ExtType.duration → (SymCC.Factory.ext.duration.val t).isLiteral = true
source
theorem Cedar.Thm.pe_ext_duration_ofBitVec_wfl {εs : SymCC.SymEntities} {t : SymCC.Term} :
SymCC.Term.WellFormedLiteral εs t → t.typeOf = SymCC.TermType.prim (SymCC.TermPrimType.bitvec 64) → (SymCC.Factory.ext.duration.ofBitVec t).isLiteral = true
source
@[simp]
theorem Cedar.Thm.pe_ext_decimal_val {d : Spec.Ext.Decimal} :
SymCC.Factory.ext.decimal.val (SymCC.Term.prim (SymCC.TermPrim.ext (Spec.Ext.decimal d))) = SymCC.Term.prim (SymCC.TermPrim.bitvec (Int64.toBitVec d))
source
@[simp]
theorem Cedar.Thm.pe_ext_ipaddr_isV4_V4 {cidr : Spec.Ext.IPAddr.CIDR Spec.Ext.IPAddr.V4_WIDTH} :
SymCC.Factory.ext.ipaddr.isV4 (SymCC.Term.prim (SymCC.TermPrim.ext (Spec.Ext.ipaddr (Spec.Ext.IPAddr.IPNet.V4 cidr)))) = SymCC.Term.prim (SymCC.TermPrim.bool true)
source
@[simp]
theorem Cedar.Thm.pe_ext_ipaddr_isV4_V6 {cidr : Spec.Ext.IPAddr.CIDR Spec.Ext.IPAddr.V6_WIDTH} :
SymCC.Factory.ext.ipaddr.isV4 (SymCC.Term.prim (SymCC.TermPrim.ext (Spec.Ext.ipaddr (Spec.Ext.IPAddr.IPNet.V6 cidr)))) = SymCC.Term.prim (SymCC.TermPrim.bool false)
source
@[simp]
theorem Cedar.Thm.pe_ext_ipaddr_addrV4_V4 {cidr : Spec.Ext.IPAddr.CIDR Spec.Ext.IPAddr.V4_WIDTH} :
SymCC.Factory.ext.ipaddr.addrV4 (SymCC.Term.prim (SymCC.TermPrim.ext (Spec.Ext.ipaddr (Spec.Ext.IPAddr.IPNet.V4 cidr)))) = SymCC.Term.prim (SymCC.TermPrim.bitvec cidr.addr)
source
theorem Cedar.Thm.pe_ext_ipaddr_addrV4'_V4 {I : SymCC.Interpretation} {cidr : Spec.Ext.IPAddr.CIDR Spec.Ext.IPAddr.V4_WIDTH} :
SymCC.Factory.ext.ipaddr.addrV4' I (SymCC.Term.prim (SymCC.TermPrim.ext (Spec.Ext.ipaddr (Spec.Ext.IPAddr.IPNet.V4 cidr)))) = SymCC.Factory.ext.ipaddr.addrV4 (SymCC.Term.prim (SymCC.TermPrim.ext (Spec.Ext.ipaddr (Spec.Ext.IPAddr.IPNet.V4 cidr))))
source
def Cedar.Thm.cidrPrefixTerm {w : Nat} (cidr : Spec.Ext.IPAddr.CIDR w) :
SymCC.Term
Equations
Instances For
    source
    @[simp]
    theorem Cedar.Thm.pe_ext_ipaddr_prefixV4_V4 {cidr : Spec.Ext.IPAddr.CIDR Spec.Ext.IPAddr.V4_WIDTH} :
    SymCC.Factory.ext.ipaddr.prefixV4 (SymCC.Term.prim (SymCC.TermPrim.ext (Spec.Ext.ipaddr (Spec.Ext.IPAddr.IPNet.V4 cidr)))) = cidrPrefixTerm cidr
    source
    theorem Cedar.Thm.pe_ext_ipaddr_prefixV4'_V4 {I : SymCC.Interpretation} {cidr : Spec.Ext.IPAddr.CIDR Spec.Ext.IPAddr.V4_WIDTH} :
    SymCC.Factory.ext.ipaddr.prefixV4' I (SymCC.Term.prim (SymCC.TermPrim.ext (Spec.Ext.ipaddr (Spec.Ext.IPAddr.IPNet.V4 cidr)))) = SymCC.Factory.ext.ipaddr.prefixV4 (SymCC.Term.prim (SymCC.TermPrim.ext (Spec.Ext.ipaddr (Spec.Ext.IPAddr.IPNet.V4 cidr))))
    source
    @[simp]
    theorem Cedar.Thm.pe_ext_ipaddr_addrV6_V6 {cidr : Spec.Ext.IPAddr.CIDR Spec.Ext.IPAddr.V6_WIDTH} :
    SymCC.Factory.ext.ipaddr.addrV6 (SymCC.Term.prim (SymCC.TermPrim.ext (Spec.Ext.ipaddr (Spec.Ext.IPAddr.IPNet.V6 cidr)))) = SymCC.Term.prim (SymCC.TermPrim.bitvec cidr.addr)
    source
    theorem Cedar.Thm.pe_ext_ipaddr_addrV6'_V6 {I : SymCC.Interpretation} {cidr : Spec.Ext.IPAddr.CIDR Spec.Ext.IPAddr.V6_WIDTH} :
    SymCC.Factory.ext.ipaddr.addrV6' I (SymCC.Term.prim (SymCC.TermPrim.ext (Spec.Ext.ipaddr (Spec.Ext.IPAddr.IPNet.V6 cidr)))) = SymCC.Factory.ext.ipaddr.addrV6 (SymCC.Term.prim (SymCC.TermPrim.ext (Spec.Ext.ipaddr (Spec.Ext.IPAddr.IPNet.V6 cidr))))
    source
    @[simp]
    theorem Cedar.Thm.pe_ext_ipaddr_prefixV6_V6 {cidr : Spec.Ext.IPAddr.CIDR Spec.Ext.IPAddr.V6_WIDTH} :
    SymCC.Factory.ext.ipaddr.prefixV6 (SymCC.Term.prim (SymCC.TermPrim.ext (Spec.Ext.ipaddr (Spec.Ext.IPAddr.IPNet.V6 cidr)))) = cidrPrefixTerm cidr
    source
    theorem Cedar.Thm.pe_ext_ipaddr_prefixV6'_V6 {I : SymCC.Interpretation} {cidr : Spec.Ext.IPAddr.CIDR Spec.Ext.IPAddr.V6_WIDTH} :
    SymCC.Factory.ext.ipaddr.prefixV6' I (SymCC.Term.prim (SymCC.TermPrim.ext (Spec.Ext.ipaddr (Spec.Ext.IPAddr.IPNet.V6 cidr)))) = SymCC.Factory.ext.ipaddr.prefixV6 (SymCC.Term.prim (SymCC.TermPrim.ext (Spec.Ext.ipaddr (Spec.Ext.IPAddr.IPNet.V6 cidr))))
    source
    @[simp]
    theorem Cedar.Thm.pe_ext_datetime_val {d : Spec.Ext.Datetime} :
    SymCC.Factory.ext.datetime.val (SymCC.Term.prim (SymCC.TermPrim.ext (Spec.Ext.datetime d))) = SymCC.Term.prim (SymCC.TermPrim.bitvec d.val.toBitVec)
    source
    @[simp]
    theorem Cedar.Thm.pe_ext_datetime_ofBitVec {bv : BitVec 64} :
    SymCC.Factory.ext.datetime.ofBitVec (SymCC.Term.prim (SymCC.TermPrim.bitvec bv)) = SymCC.Term.prim (SymCC.TermPrim.ext (Spec.Ext.datetime { val := Int64.ofInt bv.toInt }))
    source
    @[simp]
    theorem Cedar.Thm.pe_ext_duration_val {d : Spec.Ext.Datetime.Duration} :
    SymCC.Factory.ext.duration.val (SymCC.Term.prim (SymCC.TermPrim.ext (Spec.Ext.duration d))) = SymCC.Term.prim (SymCC.TermPrim.bitvec d.val.toBitVec)
    source
    @[simp]
    theorem Cedar.Thm.pe_ext_duration_ofBitVec {bv : BitVec 64} :
    SymCC.Factory.ext.duration.ofBitVec (SymCC.Term.prim (SymCC.TermPrim.bitvec bv)) = SymCC.Term.prim (SymCC.TermPrim.ext (Spec.Ext.duration { val := Int64.ofInt bv.toInt }))