Skip to content

Make all STSs in the Agda spec executable #1270

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 4 commits into from
Oct 7, 2024
Merged

Make all STSs in the Agda spec executable #1270

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
9d68aa5
Synchronize local copy of the Ledger stuff to include latest changes
javierdiaz72 Sep 27, 2024
c048548
Make all STSs in the Agda spec executable
javierdiaz72 Sep 27, 2024
90934a8
Use `genErrors` whenever possible
javierdiaz72 Sep 30, 2024
44131c1
Synchronize local copy of `PParams` with the ledger spec
javierdiaz72 Oct 3, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Use genErrors whenever possible
  • Loading branch information
@javierdiaz72
javierdiaz72 committed Oct 7, 2024
commit 90934a8720b30990db97517a200ba4f174815e0c
5 changes: 3 additions & 2 deletions docs/agda-spec/src/Spec/ChainHead/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,7 @@ module Spec.ChainHead.Properties
(rs : _) (open RationalExtStructure rs)
where

open import Tactic.GenError
open import Ledger.Prelude
open import Ledger.PParams crypto es ss using (PParams; ProtVer)
open import Spec.TickForecast crypto es ss li
Expand Down Expand Up @@ -75,7 +76,7 @@ instance

computeProof : ComputationResult String (∃[ s′ ] nes ⊢ s ⇀⦇ bh ,CHAINHEAD⦈ s′)
computeProof = case ¿ prtlSeqChecks ¿² lab bh of λ where
(no _) → failure "Failed in CHAINHEAD"
(no ¬psc) → failure (genErrors ¬psc)
(yes psc) → do
(forecast , tickfStep) ← computeTICKF _ nes slot
let
Expand All @@ -84,7 +85,7 @@ instance
pp = getPParams forecast; open PParams
pd = getPoolDistr forecast
case chainChecks? MaxMajorPV (pp .maxHeaderSize , pp .maxBlockSize , pp .pv) bh of λ where
(no _) → failure "Failed in CHAINHEAD"
(no ¬cc) → failure (genErrors ¬cc)
(yes cc) → do
(⟦ η₀′ , _ ⟧ᵗˢ , ticknStep) ← computeTICKN ticknΓ ticknSt ne
(_ , prtclStep) ← computePRTCL ⟦ pd , η₀′ ⟧ᵖᵉ prtclSt bh
Expand Down
3 changes: 2 additions & 1 deletion docs/agda-spec/src/Spec/Protocol/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,7 @@ module Spec.Protocol.Properties

open import Data.Rational as ℚ using (1ℚ)
open import Ledger.Prelude
open import Tactic.GenError
open import Spec.Protocol crypto nonces es ss bs af rs
open import Spec.BaseTypes crypto using (OCertCounters)
open import Spec.UpdateNonce crypto nonces es
Expand Down Expand Up @@ -88,7 +89,7 @@ instance
(_ , updnStep) ← computeUPDN updnΓ updnSt slot
(_ , ocertStep) ← computeOCERT ocertΓ cs bh
success (-, Evolve-Prtcl (updnStep , ocertStep , prf))
(no _) → failure "Failed in PRTCL"
(no ¬prf) → failure (genErrors ¬prf)

completeness : ∀ s′ → Γ ⊢ s ⇀⦇ bh ,PRTCL⦈ s′ → (proj₁ <$> computeProof) ≡ success s′
completeness _ (Evolve-Prtcl (updnStep , ocertStep , p))
Expand Down