Memory/Remember Tactics

This file provides tactics and rules for remembering values read from memory locations during relational proofs. This is useful when the same location is read multiple times and you want to avoid re-reading it.

Main definitions

Rules

• r_get_remember_lhs - One-sided get on LHS that adds rem_lhs to precondition
• r_get_remember_rhs - One-sided get on RHS that adds rem_rhs to precondition
• r_get_remind_lhs - One-sided get on LHS that uses existing rem_lhs from precondition
• r_get_remind_rhs - One-sided get on RHS that uses existing rem_rhs from precondition
• r_forget_lhs - Weaken precondition by dropping rem_lhs
• r_forget_rhs - Weaken precondition by dropping rem_rhs

Tactics

• ssprove_forget - Discard most recent remembered value from precondition
• ssprove_forget_all - Discard all remembered values from precondition
• ssprove_remember_lhs - Apply r_get_remember_lhs rule
• ssprove_remember_rhs - Apply r_get_remember_rhs rule
• ssprove_remind_lhs - Apply r_get_remind_lhs rule
• ssprove_remind_rhs - Apply r_get_remind_rhs rule

Usage

When reading from a location, you can "remember" the value for later use. This adds a rem_lhs l v or rem_rhs l v conjunct to the precondition. Later, remind rules let you use the remembered value instead of reading again.

-- When we have a goal with `x <- get l` on the left
-- Apply r_get_remember_lhs to add rem_lhs l x to precondition
ssprove_remember_lhs

-- Later, when we read from the same location again
-- Apply r_get_remind_lhs to use the remembered value
ssprove_remind_lhs

References

• SSProve: theories/Crypt/package/pkg_rhl.v (r_get_remember_lhs, etc.)
• SSProve: theories/Crypt/package/pkg_user_util.v (ssprove_forget)

Remember Rules

theorem CatCrypt.Relational.r_get_remember_lhs {α β : Type} {Φ : RPre} {Ψ : RPost α β} (l : Core.Location) {c₂ : Core.SPComp β} {f : l.ty → Core.SPComp α} (h : ∀ (v : l.ty), rHoare (Φ ⋊ Invariant.rem_lhs l v) (f v) c₂ Ψ) : rHoare Φ (Core.SPComp.get l >>= f) c₂ Ψ

One-sided get on the left that remembers the value.

After reading a value v from location l on the left side, the precondition is extended with rem_lhs l v, remembering that the left heap has value v at location l.

This is useful when the same location is read multiple times and you want to use r_get_remind_lhs for subsequent reads.

theorem CatCrypt.Relational.r_get_remember_rhs {α β : Type} {Φ : RPre} {Ψ : RPost α β} (l : Core.Location) {c₁ : Core.SPComp α} {f : l.ty → Core.SPComp β} (h : ∀ (v : l.ty), rHoare (Φ ⋊ Invariant.rem_rhs l v) c₁ (f v) Ψ) : rHoare Φ c₁ (Core.SPComp.get l >>= f) Ψ

One-sided get on the right that remembers the value.

After reading a value v from location l on the right side, the precondition is extended with rem_rhs l v, remembering that the right heap has value v at location l.

Remind Rules

theorem CatCrypt.Relational.r_get_remind_lhs {α β : Type} {l : Core.Location} {v : l.ty} {Φ : RPre} {Ψ : RPost α β} {f : l.ty → Core.SPComp α} {c₂ : Core.SPComp β} [hr : Invariant.ProvenBy (Invariant.rem_lhs l v) Φ] (h : rHoare Φ (f v) c₂ Ψ) : rHoare Φ (Core.SPComp.get l >>= f) c₂ Ψ

One-sided get on the left that uses a remembered value.

If the precondition contains rem_lhs l v, then reading from location l on the left side can be replaced by using the known value v directly.

The [ProvenBy (rem_lhs l v) Φ] constraint ensures that the precondition contains the remembered value. This is automatically inferred using the ProvenBy instances.

theorem CatCrypt.Relational.r_get_remind_rhs {α β : Type} {l : Core.Location} {v : l.ty} {Φ : RPre} {Ψ : RPost α β} {c₁ : Core.SPComp α} {f : l.ty → Core.SPComp β} [hr : Invariant.ProvenBy (Invariant.rem_rhs l v) Φ] (h : rHoare Φ c₁ (f v) Ψ) : rHoare Φ c₁ (Core.SPComp.get l >>= f) Ψ

One-sided get on the right that uses a remembered value.

If the precondition contains rem_rhs l v, then reading from location l on the right side can be replaced by using the known value v directly.

Forget Rules

theorem CatCrypt.Relational.r_forget_lhs {α : Type u_5} {β : Type u_6} {Φ : RPre} {Ψ : RPost α β} {c₁ : Core.SPComp α} {c₂ : Core.SPComp β} {l : Core.Location} {v : l.ty} (h : rHoare Φ c₁ c₂ Ψ) : rHoare (Φ ⋊ Invariant.rem_lhs l v) c₁ c₂ Ψ

Weaken precondition by dropping rem_lhs.

This rule drops a remembered value once it is irrelevant to the goal. It projects out the rem_lhs conjunct from the precondition.

theorem CatCrypt.Relational.r_forget_rhs {α : Type u_5} {β : Type u_6} {Φ : RPre} {Ψ : RPost α β} {c₁ : Core.SPComp α} {c₂ : Core.SPComp β} {l : Core.Location} {v : l.ty} (h : rHoare Φ c₁ c₂ Ψ) : rHoare (Φ ⋊ Invariant.rem_rhs l v) c₁ c₂ Ψ

Weaken precondition by dropping rem_rhs.

This rule drops a remembered value once it is irrelevant to the goal.

Synchronized Remember Rules

theorem CatCrypt.Relational.r_get_vs_get_remember_lhs {α β : Type} {Φ : RPre} {Ψ : RPost α β} (l : Core.Location) {f₁ : l.ty → Core.SPComp α} {f₂ : l.ty → Core.SPComp β} [ht : Invariant.ProvenBy (Invariant.syncsAt l) Φ] (h : ∀ (v : l.ty), rHoare (Φ ⋊ Invariant.rem_lhs l v) (f₁ v) (f₂ v) Ψ) : rHoare Φ (Core.SPComp.get l >>= f₁) (Core.SPComp.get l >>= f₂) Ψ

Synchronized get that remembers on the left.

When both sides read from synchronized locations (same value on both sides), and we want to remember the value on the left side.

theorem CatCrypt.Relational.r_get_vs_get_remember_rhs {α β : Type} {Φ : RPre} {Ψ : RPost α β} (l : Core.Location) {f₁ : l.ty → Core.SPComp α} {f₂ : l.ty → Core.SPComp β} [ht : Invariant.ProvenBy (Invariant.syncsAt l) Φ] (h : ∀ (v : l.ty), rHoare (Φ ⋊ Invariant.rem_rhs l v) (f₁ v) (f₂ v) Ψ) : rHoare Φ (Core.SPComp.get l >>= f₁) (Core.SPComp.get l >>= f₂) Ψ

Synchronized get that remembers on the right.

When both sides read from synchronized locations, and we want to remember the value on the right side.

Remembers Syncs

theorem CatCrypt.Relational.Remembers_syncs {s : Invariant.Side} {l : Core.Location} {v : l.ty} {Φ : RPre} [Invariant.ProvenBy (Invariant.rem_inv s l v) Φ] [Invariant.ProvenBy (Invariant.syncsAt l) Φ] (h₁ h₂ : Core.Heap) : Φ h₁ h₂ → Invariant.rem_inv s.other l v h₁ h₂

If we remember a value on one side and locations are synced, we can derive the remembered value on the other side.

Forget Tactics

def CatCrypt.Tactics.tacticSsprove_forget : Lean.ParserDescr

ssprove_forget discards the most recent remembered value from the precondition.

This tactic looks for a precondition of the form (Φ ⋊ rem_lhs l v) or (Φ ⋊ rem_rhs l v) and applies the corresponding forget rule to drop the remembered value.

Example:

-- Goal: rHoare (Φ ⋊ rem_lhs l v) c₁ c₂ Ψ
ssprove_forget
-- New goal: rHoare Φ c₁ c₂ Ψ

Equations

• CatCrypt.Tactics.tacticSsprove_forget = Lean.ParserDescr.node `CatCrypt.Tactics.tacticSsprove_forget 1024 (Lean.ParserDescr.nonReservedSymbol "ssprove_forget" false)

def CatCrypt.Tactics.tacticSsprove_forget_all : Lean.ParserDescr

ssprove_forget_all discards all remembered values from the precondition.

This repeatedly applies ssprove_forget until no more remembered values remain.

Example:

-- Goal: rHoare (Φ ⋊ rem_lhs l₁ v₁ ⋊ rem_rhs l₂ v₂ ⋊ rem_lhs l₃ v₃) c₁ c₂ Ψ
ssprove_forget_all
-- New goal: rHoare Φ c₁ c₂ Ψ

Equations

• CatCrypt.Tactics.tacticSsprove_forget_all = Lean.ParserDescr.node `CatCrypt.Tactics.tacticSsprove_forget_all 1024 (Lean.ParserDescr.nonReservedSymbol "ssprove_forget_all" false)

Remember Tactics

def CatCrypt.Tactics.tacticSsprove_remember_lhs : Lean.ParserDescr

ssprove_remember_lhs applies the r_get_remember_lhs rule.

This is used when you have a get l on the left side and want to remember the value for later use. The precondition is extended with rem_lhs l v.

Example:

-- Goal: rHoare Φ (SPComp.get l >>= f) c₂ Ψ
ssprove_remember_lhs
-- New goal: ∀ v, rHoare (Φ ⋊ rem_lhs l v) (f v) c₂ Ψ

Equations

• CatCrypt.Tactics.tacticSsprove_remember_lhs = Lean.ParserDescr.node `CatCrypt.Tactics.tacticSsprove_remember_lhs 1024 (Lean.ParserDescr.nonReservedSymbol "ssprove_remember_lhs" false)

def CatCrypt.Tactics.tacticSsprove_remember_rhs : Lean.ParserDescr

ssprove_remember_rhs applies the r_get_remember_rhs rule.

This is used when you have a get l on the right side and want to remember the value for later use.

Example:

-- Goal: rHoare Φ c₁ (SPComp.get l >>= f) Ψ
ssprove_remember_rhs
-- New goal: ∀ v, rHoare (Φ ⋊ rem_rhs l v) c₁ (f v) Ψ

Equations

• CatCrypt.Tactics.tacticSsprove_remember_rhs = Lean.ParserDescr.node `CatCrypt.Tactics.tacticSsprove_remember_rhs 1024 (Lean.ParserDescr.nonReservedSymbol "ssprove_remember_rhs" false)

Remind Tactics

def CatCrypt.Tactics.tacticSsprove_remind_lhs : Lean.ParserDescr

ssprove_remind_lhs applies the r_get_remind_lhs rule.

This is used when you have a get l on the left side and the precondition already contains rem_lhs l v. The get is replaced by using the known value.

Example:

-- Goal: rHoare (Φ ⋊ rem_lhs l v) (SPComp.get l >>= f) c₂ Ψ
ssprove_remind_lhs
-- New goal: rHoare (Φ ⋊ rem_lhs l v) (f v) c₂ Ψ

Equations

• CatCrypt.Tactics.tacticSsprove_remind_lhs = Lean.ParserDescr.node `CatCrypt.Tactics.tacticSsprove_remind_lhs 1024 (Lean.ParserDescr.nonReservedSymbol "ssprove_remind_lhs" false)

def CatCrypt.Tactics.tacticSsprove_remind_rhs : Lean.ParserDescr

ssprove_remind_rhs applies the r_get_remind_rhs rule.

This is used when you have a get l on the right side and the precondition already contains rem_rhs l v.

Example:

-- Goal: rHoare (Φ ⋊ rem_rhs l v) c₁ (SPComp.get l >>= f) Ψ
ssprove_remind_rhs
-- New goal: rHoare (Φ ⋊ rem_rhs l v) c₁ (f v) Ψ

Equations

• CatCrypt.Tactics.tacticSsprove_remind_rhs = Lean.ParserDescr.node `CatCrypt.Tactics.tacticSsprove_remind_rhs 1024 (Lean.ParserDescr.nonReservedSymbol "ssprove_remind_rhs" false)

Combined Remember/Remind Tactics

def CatCrypt.Tactics.tacticSsprove_get_lhs : Lean.ParserDescr

ssprove_get_lhs handles a get on the left side by either remembering or reminding.

If the precondition already contains rem_lhs l v, it uses the remembered value. Otherwise, it remembers the new value.

Equations

• CatCrypt.Tactics.tacticSsprove_get_lhs = Lean.ParserDescr.node `CatCrypt.Tactics.tacticSsprove_get_lhs 1024 (Lean.ParserDescr.nonReservedSymbol "ssprove_get_lhs" false)

def CatCrypt.Tactics.tacticSsprove_get_rhs : Lean.ParserDescr

ssprove_get_rhs handles a get on the right side by either remembering or reminding.

If the precondition already contains rem_rhs l v, it uses the remembered value. Otherwise, it remembers the new value.

Equations

• CatCrypt.Tactics.tacticSsprove_get_rhs = Lean.ParserDescr.node `CatCrypt.Tactics.tacticSsprove_get_rhs 1024 (Lean.ParserDescr.nonReservedSymbol "ssprove_get_rhs" false)