def HeyVL.Verifies (C : HeyVL) : Prop

A HeyVL program C verifies if vp⟦C⟧ ⊤ = ⊤

Equations

• C.Verifies = (⟦@(vp⟦@C⟧ ⊤)⟧' = ⊤)

structure Conditions (E : Encoding) : Type

• original : spGCL
• O : Optimization
• post : HeyLo HeyLo.Ty.ENNReal
• pre : HeyLo HeyLo.Ty.ENNReal
• encoding : HeyLo HeyLo.Ty.ENNReal
• prop : self.original.vp self.O E self.post = self.encoding
• fv : Globals
• fv_prop : self.fv = self.original.fv ∪ self.post.fv ∪ self.pre.fv
• invs : List (HeyLo HeyLo.Ty.ENNReal)
• invs_prop : self.invs = self.original.invsList

def pgclEncoding.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.pgclEncoding : Category

Equations

• Lean.Parser.Category.pgclEncoding = { }

def pgclEncoding_ : Lean.ParserDescr

Equations

• pgclEncoding_ = Lean.ParserDescr.node `pgclEncoding_ 1022 (Lean.ParserDescr.const `ident)

def «termPgclEncoding[_]» : Lean.ParserDescr

Equations

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

def «termVc[_,_]{_}_{_}» : Lean.ParserDescr

Equations

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

theorem HeyVL.vp_sem_eq {φ ψ : HeyLo HeyLo.Ty.ENNReal} (S : HeyVL) (h : ⟦@φ⟧' = ⟦@ψ⟧') : ⟦@(vp⟦@S⟧ φ)⟧' = ⟦@(vp⟦@S⟧ ψ)⟧'

theorem Conditions.wlp_valid {E : Encoding} (C : Conditions E) (h₁ : ⟦@C.post⟧' ≤ 1) (hI : ∀ I ∈ C.original.invs, ⟦@I⟧' ≤ 1) (h : heyvl {assume(@C.pre) ; @(C.original.enc C.O Encoding.wlp (C.original.fv ∪ C.post.fv)).2 ; assert(@C.post)}.Verifies) : ⟦@C.pre⟧' ≤ wlp[C.O]⟦@C.original.pGCL⟧ ⟦@C.post⟧'

def Conditions.sound {E : Encoding} (C : Conditions E) : Prop

Equations

• C_2.sound = (wp[C_2.O]⟦@C_2.original.pGCL⟧ ⟦@C_2.post⟧' ≤ ⟦@C_2.pre⟧')
• C_2.sound = (⟦@C_2.pre⟧' ≤ wlp[C_2.O]⟦@C_2.original.pGCL⟧ ⟦@C_2.post⟧')

def Conditions.show_wp (C : Conditions Encoding.wp) (h : ⟦@C.encoding⟧' ≤ ⟦@C.pre⟧') : C.sound

Equations

• ⋯ = ⋯

def Conditions.show_wlp' (C : Conditions Encoding.wlp) (h : ⟦@C.pre⟧' ≤ ⟦@C.encoding⟧') (hpost : ⟦@C.post⟧' ≤ 1) (hI : ∀ I ∈ C.invs, ⟦@I⟧' ≤ 1) : C.sound

Equations

• ⋯ = ⋯

@[simp]

theorem Nat.log2_div_2 (n : ℕ) : (n / 2).log2 = n.log2 - 1

theorem Nat.log2_le_succ {n : ℕ} : n.log2 ≤ (n + 1).log2

theorem Nat.log2_mono {n m : ℕ} (h : n ≤ m) : n.log2 ≤ m.log2

@[simp]

theorem ENNReal.two_inv_mul_two : 2⁻¹ * 2 = 1

@[simp]

theorem ENNReal.two_mul_two_inv : 2 * 2⁻¹ = 1

@[simp]

theorem ENNReal.two_inv_mul_two_id (q : ENNReal) : 2⁻¹ * q * 2 = q