Equality up to an invariant

eq_up_to_inv relates two shallow packages that agree on every operation up to a heap invariant, with the bridge simplify_eq_rel_intro from the relational judgment rHoare.

A security bound — a zero or bounded Advantage — is proved through the deep embedding: DeepNomAdvantage and NomPkgSecure in CatCrypt.Crypto.NomAdvantage, over DeepPackage.link.

References

• Larsen and Schürmann, Nominal State-Separating Proofs
• SSProve: theories/Crypt/package/pkg_rhl.v

Equality Up To Invariant

def CatCrypt.Invariant.eq_up_to_inv {L₀ L₁ : Package.Locations} {I E : Package.Interface} (inv : Relational.RPre) (P₀ P₁ : Package.RawPackage) : Package.ValidPackage L₀ I E P₀ → Package.ValidPackage L₁ I E P₁ → Prop

Two packages are equal up to an invariant if each procedure, when run from states satisfying the invariant, produces coupled outputs that also satisfy the invariant.

Equations

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

Bridge from the relational judgment

theorem CatCrypt.Invariant.simplify_eq_rel_intro {L₀ L₁ : Package.Locations} {I E : Package.Interface} (inv : Relational.RPre) (P₀ P₁ : Package.RawPackage) (hP₀ : Package.ValidPackage L₀ I E P₀) (hP₁ : Package.ValidPackage L₁ I E P₁) (h : ∀ (id : ℕ) (S T : Type), E.has id S T → ∀ (x : S), Relational.rHoare inv (P₀.resolve id x) (P₁.resolve id x) fun (v₀ : T) (h₀ : Core.Heap) (v₁ : T) (h₁ : Core.Heap) => v₀ = v₁ ∧ inv h₀ h₁) : eq_up_to_inv inv P₀ P₁ hP₀ hP₁

Package equality up to an invariant follows from a per-operation rHoare judgment relating the two resolutions.

The types line up as:

• RawPackage.resolve P id x : SPComp T = Heap → SDistr (T × Heap)
• rHoare expects SPComp α and SPComp β.