PoV.lagda.md

source_branch	source_path
master	src/Ledger/Conway/Specification/Certs/Properties/PoV.lagda.md

Theorem: The CERTS rule preserves value {#thm:CERTS-PoV}

Informally.

Let l{.AgdaBound} be a list of DCerts{.AgdaDatatype}, and let s₁{.AgdaBound}, sₙ{.AgdaBound} be CertStates{.AgdaRecord} such that s₁{.AgdaBound} ⇀⦇{.AgdaDatatype} l{.AgdaBound} ,CERTS⦈{.AgdaDatatype} sₙ{.AgdaBound}. Then, the value of s₁{.AgdaBound} is equal to the value of sₙ{.AgdaBound} plus the value of the withdrawals in Γ{.AgdaBound}.

Formally.

    CERTS-pov : {Γ : CertEnv} {s₁ sₙ  : CertState}
      → ∀[ a ∈ dom (WithdrawalsOf Γ) ] NetworkIdOf a ≡ NetworkId
      → Γ ⊢ s₁ ⇀⦇ l ,CERTS⦈ sₙ
      → getCoin s₁ ≡ getCoin sₙ + getCoin (WithdrawalsOf Γ)

Proof.

    CERTS-pov {Γ = Γ} validNetId (run (pre-cert , certs)) =
      trans  (PRE-CERT-pov validNetId pre-cert)
             (cong (_+ getCoin (WithdrawalsOf Γ)) (sts-pov certs))