SNAP: Computational

This module proves that the SNAP transition rule is computational.

{-# OPTIONS --safe #-}

open import Ledger.Dijkstra.Specification.Transaction
open import Ledger.Dijkstra.Specification.Abstract

module Ledger.Dijkstra.Specification.Rewards.Properties.Computational
  (txs : _) (open TransactionStructure txs)
  (abs : AbstractFunctions txs) (open AbstractFunctions abs)
  where

open import Ledger.Prelude
open import Ledger.Dijkstra.Specification.Ledger txs abs
open import Ledger.Dijkstra.Specification.Rewards txs abs

open Computational ⦃...⦄

module _ {ss : Snapshots} where

  module _ {lstate : LedgerState} where

    SNAP-total : ∃[ ss' ] lstate ⊢ ss ⇀⦇ tt ,SNAP⦈ ss'
    SNAP-total = -, SNAP

    SNAP-complete : ∀ ss' → lstate ⊢ ss ⇀⦇ tt ,SNAP⦈ ss' → proj₁ SNAP-total ≡ ss'
    SNAP-complete ss' SNAP = refl

  SNAP-deterministic-≡ : ∀ {ls ls' ss' ss''}
                     → ls ≡ ls'
                     → ls ⊢ ss ⇀⦇ tt ,SNAP⦈ ss'
                     → ls' ⊢ ss ⇀⦇ tt ,SNAP⦈ ss'' → ss' ≡ ss''
  SNAP-deterministic-≡ refl SNAP SNAP = refl

instance
  Computational-SNAP : Computational _⊢_⇀⦇_,SNAP⦈_ ⊥
  Computational-SNAP .computeProof _ ss lstate = success SNAP-total
  Computational-SNAP .completeness _ ss lstate ss' h = cong success (SNAP-complete ss' h)