def GaudisCrypt.hoareStmt (A : ProgramState → Prop) (p : Stmt) (B : ProgramState → Prop) : Prop

Equations

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

def GaudisCrypt.hoareProc {sig : ProcedureSignature} (A : sig.ParamType → VariableAssignment → Prop) (p : Procedure sig) (B : sig.ret → VariableAssignment → Prop) : Prop

Equations

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

theorem GaudisCrypt.SubProbability.ofEvent_eq_zero_of_subset {α : Type u_1} {μ : SubProbability α} {E F : Set α} (hEF : E ⊆ F) (h : μ.ofEvent F = 0) : μ.ofEvent E = 0

A sub-event of a null event is null. ofEvent is toNNReal of the measure and the measure is finite (total mass ≤ 1), so the ℝ≥0 and the ℝ≥0∞ values vanish together and monotonicity of the measure carries over.

theorem GaudisCrypt.SubProbability.expected_eq_zero_of_support {α : Type u_1} {μ : SubProbability α} {f : α → ENNReal} (h : ∀ a ∈ μ.support, f a = 0) : μ.expected f = 0

An expectation is 0 when the function vanishes on the support: the measure is discrete, so the points outside the support carry no mass.

theorem GaudisCrypt.hoareStmt_mono {A : ProgramState → Prop} {p : Stmt} {B₁ B₂ : ProgramState → Prop} (hB : ∀ (σ : ProgramState), B₁ σ → B₂ σ) (h : hoareStmt A p B₁) : hoareStmt A p B₂

hoareStmt is monotone in its postcondition: a weaker B is a weaker triple, because the null event ¬ B only shrinks.

theorem GaudisCrypt.hoareProc_mono {sig : ProcedureSignature} {A : sig.ParamType → VariableAssignment → Prop} {p : Procedure sig} {B₁ B₂ : sig.ret → VariableAssignment → Prop} (hB : ∀ (r : sig.ret) (σ : VariableAssignment), B₁ r σ → B₂ r σ) (h : hoareProc A p B₁) : hoareProc A p B₂

hoareProc is monotone in its postcondition, for the same reason as hoareStmt_mono.

theorem GaudisCrypt.hoareStmt_iff_wp {A : ProgramState → Prop} {p : Stmt} {B : ProgramState → Prop} : hoareStmt A p B ↔ ∀ (σ : ProgramState), A σ → (programDenotation p).wp ({r : Unit × ProgramState | ¬B r.2}.indicator fun (x : Unit × ProgramState) => 1) σ = 0

A hoareStmt triple is a wp statement: wp against the indicator of the failure event is that event's mass (expectation_indicator), so the triple is exactly that wp being 0.

theorem GaudisCrypt.hoareProc_iff_wp {sig : ProcedureSignature} {A : sig.ParamType → VariableAssignment → Prop} {p : Procedure sig} {B : sig.ret → VariableAssignment → Prop} : hoareProc A p B ↔ ∀ (args : sig.ParamType) (σ : VariableAssignment), A args σ → (procedureDenotation p args).wp ({r : sig.ret × VariableAssignment | ¬B r.1 r.2}.indicator fun (x : sig.ret × VariableAssignment) => 1) σ = 0

The same for hoareProc.

theorem GaudisCrypt.hoareStmt_of_wp {A : ProgramState → Prop} {p : Stmt} {B : ProgramState → Prop} (h : ∀ (σ : ProgramState), A σ → (programDenotation p).wp ({r : Unit × ProgramState | ¬B r.2}.indicator fun (x : Unit × ProgramState) => 1) σ = 0) : hoareStmt A p B

A hoareStmt triple from a wp computation — the direction of hoareStmt_iff_wp that proofs actually use.

theorem GaudisCrypt.hoareProc_of_wp {sig : ProcedureSignature} {A : sig.ParamType → VariableAssignment → Prop} {p : Procedure sig} {B : sig.ret → VariableAssignment → Prop} (h : ∀ (args : sig.ParamType) (σ : VariableAssignment), A args σ → (procedureDenotation p args).wp ({r : sig.ret × VariableAssignment | ¬B r.1 r.2}.indicator fun (x : sig.ret × VariableAssignment) => 1) σ = 0) : hoareProc A p B

The same for hoareProc.

theorem GaudisCrypt.hoare_pre {A A' : ProgramState → Prop} {p : Stmt} {B : ProgramState → Prop} (h : hoareStmt A' p B) (hA : ∀ (σ : ProgramState), A σ → A' σ) : hoareStmt A p B

Strengthening the precondition. The triple comes first, so that apply hoare_pre leaves it with an open precondition ?A', to be filled by the wp steps, and the implication into it as the last goal.

theorem GaudisCrypt.hoare_post {A : ProgramState → Prop} {p : Stmt} {B B' : ProgramState → Prop} (h : hoareStmt A p B') (hB : ∀ (σ : ProgramState), B' σ → B σ) : hoareStmt A p B

Weakening the postcondition (hoareStmt_mono, with the triple first as in hoare_pre): apply hoare_post leaves the triple with an open postcondition ?B' and the implication out of it as the last goal.

theorem GaudisCrypt.hoare_skip_of_imp {A B : ProgramState → Prop} (h : ∀ (σ : ProgramState), A σ → B σ) : hoareStmt A StmtWithHoles.skip B

The rule for skip: the precondition implies the postcondition.

theorem GaudisCrypt.hoare_skip_wp (B : ProgramState → Prop) : hoareStmt B StmtWithHoles.skip B

The wp rule for skip: the postcondition itself.

theorem GaudisCrypt.SubProbability.expected_eq_zero_of_null {α : Type u_1} {μ : SubProbability α} {f : α → ENNReal} {S : Set α} (hS : μ.ofEvent S = 0) (h : ∀ a ∉ S, f a = 0) : μ.expected f = 0

An expectation is 0 when the function vanishes outside a null event.

theorem GaudisCrypt.hoare_seq {A B C : ProgramState → Prop} {p q : Stmt} (hq : hoareStmt B q C) (hp : hoareStmt A p B) : hoareStmt A (StmtWithHoles.seq p q) C

Sequencing: the postcondition of the first statement is the precondition of the second. The second statement's triple comes first, so that apply hoare_seq leaves it with the open intermediate condition ?B to be filled by the wp steps, and the first statement's after it.

theorem GaudisCrypt.hoare_sample_wp {α : Type} {e : Getter (SubProbability α) ProgramState} (x : Setter α ProgramState) (B : ProgramState → Prop) : hoareStmt (fun (σ : ProgramState) => ∀ a ∈ (e.get σ).support, B (x.set a σ)) (StmtWithHoles.sample x e) B

The wp rule for sampling: the postcondition must hold after writing any value in the support of the sampled distribution.

theorem GaudisCrypt.hoare_assign_wp {α : Type} (x : Setter α ProgramState) (e : Getter α ProgramState) (B : ProgramState → Prop) : hoareStmt (fun (σ : ProgramState) => B (x.set (e.get σ) σ)) (StmtWithHoles.assign x e) B

The wp rule for assignment: the postcondition, at the state with the value written.

theorem GaudisCrypt.hoareProc_as_hoareStmt {sig : ProcedureSignature} (resL : Lens sig.ret VariableAssignment) (argsL : Lens sig.ParamType VariableAssignment) (A : sig.ParamType → VariableAssignment → Prop) (p : Procedure sig) (B : sig.ret → VariableAssignment → Prop) : hoareProc A p B ↔ hoareStmt (fun (σ : ProgramState) => A (argsL.get σ.locals) σ.globals) (Stmt.call resL.intoLocal.toSetter p argsL.intoLocal.toGetter) fun (σ : ProgramState) => B (resL.get σ.locals) σ.globals

A procedure triple is the statement triple about the one-line body

res <- p(args);

where res and args are any two lenses into the caller's locals. The callee runs in its own frame, so the two need not be disjoint, and neither needs to avoid p's parameter names. args is read before res is written, and only res and the globals are read afterwards. hoareStmt quantifies over every initial state; the ← direction picks one whose args slot holds the given arguments. The tactic hoare_proc_to_stmt (Syntax/HoareSyntax.lean) picks the two for a given triple: one local variable per parameter, and one for the result.