RATIFY: Computational

This module proves that the RATIFY and RATIFIES transition rules are computational.

{-# OPTIONS --safe #-}
open import Ledger.Dijkstra.Specification.Transaction
module Ledger.Dijkstra.Specification.Ratify.Properties.Computational
  (txs : _) (open TransactionStructure txs) where

open import Ledger.Prelude
open import Ledger.Dijkstra.Specification.Gov govStructure
open import Ledger.Dijkstra.Specification.Enact govStructure
open import Ledger.Dijkstra.Specification.Enact.Properties.Computational govStructure
open import Ledger.Dijkstra.Specification.Ratify govStructure
open Computational ⦃...⦄ hiding (computeProof; completeness)

-- NOTE: The Dijkstra RATIFY transition system has the same three constructors as
--       Conway (RATIFY-Accept, RATIFY-Reject, RATIFY-Continue) with identical
--       premises.  This is a direct port of the Conway instance to Dijkstra module
--       paths.

private
  module Implementation
    Γ (s : RatifyState) (sig : GovActionID × _)
    (let gid , st = sig)
    where
    open RatifyState s
    open RatifyEnv Γ; open GovActionState st

    es'  = compute $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ratify.Properties.Computational.html#1244}{\htmlId{1360}{\htmlClass{Bound}{\text{gid}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ratify.html#3523}{\htmlId{1366}{\htmlClass{Function}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ratify.html#3399}{\htmlId{1377}{\htmlClass{Function}{\text{currentEpoch}}}}\, \end{pmatrix}$ es action
    acc? = accepted? Γ es st
    exp? = expired? currentEpoch st
    del? = delayed? (action .gaType) prevAction es delay

    opaque
      acceptConds? : ∀ a → Dec (acceptConds Γ s a)
      acceptConds? _ = Dec-× ⦃ ⁇ accepted? _ _ _ ⦄
        ⦃ Dec-× ⦃ Dec-→ ⦃ ⁇ delayed? _ _ _ _ ⦄ ⦄ ⦃ ⁇ Computational⇒Dec' ⦄ ⦄ .dec

    RATIFY-total : ∃[ s' ] Γ ⊢ s ⇀⦇ sig ,RATIFY⦈ s'
    RATIFY-total
      with acceptConds? sig | exp?
    ... | yes p@(_ , _ , (_ , q)) | _ = -, RATIFY-Accept (p , q)
    ... | no ¬p | no ¬a = -, RATIFY-Continue (¬p , ¬a)
    ... | no ¬p | yes a = -, RATIFY-Reject (¬p , a)

    computeProof = success {Err = ⊥} RATIFY-total

    RATIFY-completeness : ∀ s' → Γ ⊢ s ⇀⦇ sig ,RATIFY⦈ s' → RATIFY-total .proj₁ ≡ s'
    RATIFY-completeness stʳ (RATIFY-Accept (p , a)) with acceptConds? sig
    ... | no ¬h = ⊥-elim (¬h p)
    ... | yes (_ , _ , _ , h) = cong (λ stᵉ → $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ratify.Properties.Computational.html#2279}{\htmlId{2287}{\htmlClass{Bound}{\text{stᵉ}}}}\, \\ \,\htmlId{2293}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{2297}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$) $
          computational⇒rightUnique Computational-ENACT h a
    RATIFY-completeness s' (RATIFY-Reject (¬p , a))
      rewrite dec-no (acceptConds? _) ¬p | dec-yes exp? a .proj₂ = refl
    RATIFY-completeness s' (RATIFY-Continue (¬p , ¬a))
      rewrite dec-no (acceptConds? _) ¬p | dec-no exp? ¬a = refl

    completeness = cong (success {Err = ⊥}) ∘₂ RATIFY-completeness

instance

  Computational-RATIFY : Computational _⊢_⇀⦇_,RATIFY⦈_ ⊥
  Computational-RATIFY = record {Implementation}

Computational-RATIFIES : Computational _⊢_⇀⦇_,RATIFIES⦈_ ⊥
Computational-RATIFIES = it

RATIFIES-total : ∀ {Γ s sig} → ∃[ s' ] Γ ⊢ s ⇀⦇ sig ,RATIFIES⦈ s'
RATIFIES-total = ReflexiveTransitiveClosure-total (Implementation.RATIFY-total _ _ _)

RATIFIES-complete : ∀ {Γ s sig s'} →
  Γ ⊢ s ⇀⦇ sig ,RATIFIES⦈ s' → RATIFIES-total {Γ} {s} {sig} .proj₁ ≡ s'
RATIFIES-complete = computational⇒rightUnique Computational-RATIFIES (RATIFIES-total .proj₂)

opaque
  RATIFIES-total' : ∀ {Γ s sig} → ∃[ s' ] Γ ⊢ s ⇀⦇ sig ,RATIFIES⦈ s'
  RATIFIES-total' = RATIFIES-total

  RATIFIES-complete' : ∀ {Γ s sig s'} →
    Γ ⊢ s ⇀⦇ sig ,RATIFIES⦈ s' → RATIFIES-total' {Γ} {s} {sig} .proj₁ ≡ s'
  RATIFIES-complete' = RATIFIES-complete

  RATIFIES-deterministic : ∀ {Γ s sig s' s''}
    → Γ ⊢ s ⇀⦇ sig ,RATIFIES⦈ s'
    → Γ ⊢ s ⇀⦇ sig ,RATIFIES⦈ s''
    → s' ≡ s''
  RATIFIES-deterministic p₁ p₂ = trans (sym (RATIFIES-complete' p₁)) (RATIFIES-complete' p₂)

  RATIFIES-deterministic-≡ : ∀ {Γ Γ' s s' sig sig' s'' s'''}
    → Γ ≡ Γ' → s ≡ s' → sig ≡ sig'
    → Γ  ⊢ s  ⇀⦇ sig  ,RATIFIES⦈ s''
    → Γ' ⊢ s' ⇀⦇ sig' ,RATIFIES⦈ s'''
    → s'' ≡ s'''
  RATIFIES-deterministic-≡ refl refl refl = RATIFIES-deterministic