Skip to content

Commit

Permalink
Permutations in global state transitions
Browse files Browse the repository at this point in the history
* Parties
* Messages
  • Loading branch information
yveshauser committed Feb 19, 2024
1 parent 68ed2fa commit 40c94bc
Showing 1 changed file with 19 additions and 15 deletions.
34 changes: 19 additions & 15 deletions src/Peras/SmallStep.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,8 @@ open import Data.Bool using (Bool; true; false)
open import Data.List as List using (List; all; foldr; _∷_; []; _++_; filterᵇ; map; cartesianProduct)
open import Data.List.Membership.Propositional using (_∈_)
open import Data.List.Relation.Unary.All using (All)
open import Data.List.Relation.Binary.Permutation.Propositional using (_↭_; ↭-sym)
open import Data.List.Relation.Binary.Permutation.Propositional.Properties
open import Data.Maybe using (just; nothing)
open import Data.Nat using (suc; pred; _≤_; _≤ᵇ_)
open import Data.Product using (Σ; _,_; ∃; Σ-syntax; ∃-syntax; _×_; proj₁; proj₂)
Expand Down Expand Up @@ -188,12 +190,6 @@ module _ {block₀ : Block⋆} where
N₀ : Stateᵍ
N₀ = ⟪ 0 , Ready , empty , [] , [] ⟫ -- FIXME: initial parties as parameter

permParties : List PartyId → List PartyId
permParties = id -- FIXME: permute

permMessages : List Message → List Message
permMessages = id -- FIXME: permute

updateStateˡ : PartyId → Stateˡ → Stateᵍ → Stateᵍ
updateStateˡ p sₗ N = record N { stateMap = M.insert p sₗ (stateMap N) }

Expand Down Expand Up @@ -329,13 +325,21 @@ module _ {block₀ : Block⋆} where
}

NextRound : ∀ {s sm ms ps}
→ ⟪ s , Baked , sm , ms , ps ⟫ ↝ ⟪ suc s , Ready , sm , ms , ps ⟫

PermParties : ∀ {s p sm ms ps}
→ ⟪ s , p , sm , ms , ps ⟫ ↝ ⟪ s , p , sm , ms , permParties ps ⟫

PermMsgs : ∀ {s p sm ms ps}
→ ⟪ s , p , sm , ms , ps ⟫ ↝ ⟪ s , p , sm , permMessages ms , ps ⟫
--------------------------------
→ ⟪ s , Baked , sm , ms , ps ⟫ ↝
⟪ suc s , Ready , sm , ms , ps ⟫

PermParties : ∀ {s p sm ms ps ps′}
→ ps ↭ ps′
--------------------------
→ ⟪ s , p , sm , ms , ps ⟫ ↝
⟪ s , p , sm , ms , ps′ ⟫

PermMsgs : ∀ {s p sm ms ms′ ps}
→ ms ↭ ms′
--------------------------
→ ⟪ s , p , sm , ms , ps ⟫ ↝
⟪ s , p , sm , ms′ , ps ⟫
```

## Reflexive, transitive closure (which is big-step in the paper)
Expand Down Expand Up @@ -441,8 +445,8 @@ module _ {block₀ : Block⋆} where
m′ = []↷-collision-free m x₅
in ∷-collision-free m′
↝-collision-free NextRound (collision-free x x₁ x₂ x₃) = collision-free x x₁ x₂ x₃
↝-collision-free PermParties (collision-free x x₁ x₂ x₃) = collision-free x x₁ x₂ x₃
↝-collision-free PermMsgs (collision-free x x₁ x₂ x₃) = collision-free x x₁ x₂ x₃
↝-collision-free (PermParties _) (collision-free x x₁ x₂ x₃) = collision-free x x₁ x₂ x₃
↝-collision-free (PermMsgs p) (collision-free x x₁ x₂ x₃) = collision-free (∈-resp-↭ (↭-sym p) x) (∈-resp-↭ (↭-sym p) x₁) x₂ x₃

-- When the current state is collision free, previous states were so too

Expand Down

0 comments on commit 40c94bc

Please sign in to comment.