Reverse the index of ReflexiveTransitiveClosureᵢ (#403)

* Reverse the index of `ReflexiveTransitiveClosureᵢ` * Fix `Computational` proof
IntersectMBO · Apr 29, 2024 · 44080e2 · 44080e2
1 parent ed315b0
commit 44080e2
Show file tree

Hide file tree

Showing 3 changed files with 43 additions and 27 deletions.
diff --git a/src/Interface/ComputationalRelation.agda b/src/Interface/ComputationalRelation.agda
@@ -192,22 +192,29 @@ module _ {BSTS : C → S → ⊤ → S → Set} ⦃ _ : Computational BSTS Err
     ... | success (s₂ , _) | p = p
 
   module _ {STS : C × ℕ → S → Sig → S → Set} ⦃ Computational-STS : Computational STS Err₂ ⦄ where instance
-    Computational-ReflexiveTransitiveClosureᵢᵇ : Computational (ReflexiveTransitiveClosureᵢᵇ BSTS STS) (Err₁ ⊎ Err₂)
-    Computational-ReflexiveTransitiveClosureᵢᵇ .computeProof c s [] = bimap inj₁ (map₂′ BS-base) (computeProof c s tt)
-    Computational-ReflexiveTransitiveClosureᵢᵇ .computeProof c s (sig ∷ sigs) with computeProof (c , length sigs) s sig
-    ... | success (s₁ , h) with computeProof c s₁ sigs
-    ...   | success (s₂ , hs) = success (s₂ , BS-ind h hs)
-    ...   | failure a = failure a
-    Computational-ReflexiveTransitiveClosureᵢᵇ .computeProof c s (sig ∷ sigs) | failure a = failure (inj₂ a)
-    Computational-ReflexiveTransitiveClosureᵢᵇ .completeness c s [] s' (BS-base p)
-      with computeProof {STS = BSTS} c s tt | completeness _ _ _ _ p
+    Computational-ReflexiveTransitiveClosureᵢᵇ' : Computational (_⊢_⇀⟦_⟧ᵢ*'_ BSTS STS) (Err₁ ⊎ Err₂)
+    Computational-ReflexiveTransitiveClosureᵢᵇ' .computeProof c s [] =
+      bimap inj₁ (map₂′ BS-base) (computeProof (proj₁ c) s tt)
+    Computational-ReflexiveTransitiveClosureᵢᵇ' .computeProof c s (sig ∷ sigs) with computeProof c s sig
+    ... | success (s₁ , h) with computeProof (proj₁ c , suc (proj₂ c)) s₁ sigs
+    ... | success (s₂ , hs) = success (s₂ , BS-ind h hs)
+    ... | failure a = failure a
+    Computational-ReflexiveTransitiveClosureᵢᵇ' .computeProof c s (sig ∷ sigs) | failure a = failure (inj₂ a)
+    Computational-ReflexiveTransitiveClosureᵢᵇ' .completeness c s [] s' (BS-base p)
+      with computeProof {STS = BSTS} (proj₁ c) s tt | completeness _ _ _ _ p
     ... | success x | refl = refl
-    Computational-ReflexiveTransitiveClosureᵢᵇ .completeness c s (sig ∷ sigs) s' (BS-ind h hs)
-      with computeProof {STS = STS} (c , length sigs) s sig | completeness _ _ _ _ h
+    Computational-ReflexiveTransitiveClosureᵢᵇ' .completeness c s (sig ∷ sigs) s' (BS-ind h hs)
+      with computeProof {STS = STS} c s sig | completeness _ _ _ _ h
     ... | success (s₁ , _) | refl
-      with computeProof ⦃ Computational-ReflexiveTransitiveClosureᵢᵇ ⦄ c s₁ sigs | completeness _ _ _ _ hs
+      with computeProof (proj₁ c , suc (proj₂ c)) s₁ sigs | completeness _ _ _ _ hs
     ...   | success (s₂ , _) | p = p
 
+    Computational-ReflexiveTransitiveClosureᵢᵇ : Computational (ReflexiveTransitiveClosureᵢᵇ BSTS STS) (Err₁ ⊎ Err₂)
+    Computational-ReflexiveTransitiveClosureᵢᵇ .computeProof c =
+      Computational-ReflexiveTransitiveClosureᵢᵇ' .computeProof (c , 0)
+    Computational-ReflexiveTransitiveClosureᵢᵇ .completeness c =
+      Computational-ReflexiveTransitiveClosureᵢᵇ' .completeness (c , 0)
+
 Computational-ReflexiveTransitiveClosure : {STS : C → S → Sig → S → Set} → ⦃ Computational STS Err ⦄
   → Computational (ReflexiveTransitiveClosure STS) (⊥ ⊎ Err)
 Computational-ReflexiveTransitiveClosure = it

diff --git a/src/Interface/STS.agda b/src/Interface/STS.agda
@@ -35,6 +35,7 @@ private
            s s' s'' : S
            sig : Sig
            sigs : List Sig
+           n : ℕ
 
 -- small-step to big-step transformer
 
@@ -50,21 +51,24 @@ module _ (_⊢_⇀⟦_⟧ᵇ_ : C → S → ⊤ → S → Set) (_⊢_⇀⟦_⟧_
         Γ ⊢ s  ⇀⟦ sig  ⟧  s'
       → Γ ⊢ s' ⇀⟦ sigs ⟧* s''
         ───────────────────────────────────────
-        Γ ⊢ s ⇀⟦ sig ∷ sigs ⟧* s''
+        Γ ⊢ s  ⇀⟦ sig ∷ sigs ⟧* s''
 
 module _ (_⊢_⇀⟦_⟧ᵇ_ : C → S → ⊤ → S → Set) (_⊢_⇀⟦_⟧_ : C × ℕ → S → Sig → S → Set) where
-  data _⊢_⇀⟦_⟧ᵢ*_ : C → S → List Sig → S → Set where
+  data _⊢_⇀⟦_⟧ᵢ*'_ : C × ℕ → S → List Sig → S → Set where
 
     BS-base :
       Γ ⊢ s ⇀⟦ _ ⟧ᵇ s'
       ───────────────────────────────────────
-      Γ ⊢ s ⇀⟦ [] ⟧ᵢ* s'
+      (Γ , n) ⊢ s ⇀⟦ [] ⟧ᵢ*' s'
 
     BS-ind :
-        (Γ , length sigs) ⊢ s  ⇀⟦ sig  ⟧  s'
-      → Γ                ⊢ s' ⇀⟦ sigs ⟧ᵢ* s''
+        (Γ , n)     ⊢ s  ⇀⟦ sig  ⟧  s'
+      → (Γ , suc n) ⊢ s' ⇀⟦ sigs ⟧ᵢ*' s''
         ───────────────────────────────────────
-        Γ ⊢ s ⇀⟦ sig ∷ sigs ⟧ᵢ* s''
+        (Γ , n)     ⊢ s  ⇀⟦ sig ∷ sigs ⟧ᵢ*' s''
+
+  _⊢_⇀⟦_⟧ᵢ*_ : C → S → List Sig → S → Set
+  _⊢_⇀⟦_⟧ᵢ*_ Γ = _⊢_⇀⟦_⟧ᵢ*'_ (Γ , 0)
 
 data IdSTS {C S} : C → S → ⊤ → S → Set where
   Id-nop : IdSTS Γ s _ s
@@ -73,9 +77,11 @@ data IdSTS {C S} : C → S → ⊤ → S → Set where
 ReflexiveTransitiveClosure : (C → S → Sig → S → Set) → C → S → List Sig → S → Set
 ReflexiveTransitiveClosure = _⊢_⇀⟦_⟧*_ IdSTS
 
+STS-total : (C → S → Sig → S → Set) → Set
+STS-total _⊢_⇀⟦_⟧_ = ∀ {Γ s sig} → ∃[ s' ] Γ ⊢ s ⇀⟦ sig ⟧ s'
+
 ReflexiveTransitiveClosure-total : {_⊢_⇀⟦_⟧_ : C → S → Sig → S → Set}
-            → (∀ {Γ s sig} → ∃[ s' ] Γ ⊢ s ⇀⟦ sig ⟧ s')
-            → (∀ {Γ s sig} → ∃[ s' ] ReflexiveTransitiveClosure _⊢_⇀⟦_⟧_ Γ s sig s')
+  → STS-total _⊢_⇀⟦_⟧_ → STS-total (ReflexiveTransitiveClosure _⊢_⇀⟦_⟧_)
 ReflexiveTransitiveClosure-total SS-total {Γ} {s} {[]} = s , BS-base Id-nop
 ReflexiveTransitiveClosure-total SS-total {Γ} {s} {x ∷ sig} =
   case SS-total of λ where
@@ -85,12 +91,15 @@ ReflexiveTransitiveClosureᵢ : (C × ℕ → S → Sig → S → Set) → C →
 ReflexiveTransitiveClosureᵢ = _⊢_⇀⟦_⟧ᵢ*_ IdSTS
 
 ReflexiveTransitiveClosureᵢ-total : {_⊢_⇀⟦_⟧_ : C × ℕ → S → Sig → S → Set}
-             → (∀ {Γ s sig} → ∃[ s' ] Γ ⊢ s ⇀⟦ sig ⟧ s')
-             → (∀ {Γ s sig} → ∃[ s' ] ReflexiveTransitiveClosureᵢ _⊢_⇀⟦_⟧_ Γ s sig s')
-ReflexiveTransitiveClosureᵢ-total SS-total {s = s} {[]} = s , BS-base Id-nop
-ReflexiveTransitiveClosureᵢ-total SS-total {s = s} {x ∷ sig} =
-  case SS-total of λ where
-    (s' , Ps') → map₂′ (BS-ind Ps') $ ReflexiveTransitiveClosureᵢ-total SS-total
+  → STS-total _⊢_⇀⟦_⟧_ → STS-total (ReflexiveTransitiveClosureᵢ _⊢_⇀⟦_⟧_)
+ReflexiveTransitiveClosureᵢ-total SS-total = helper SS-total
+  where
+    helper : {_⊢_⇀⟦_⟧_ : C × ℕ → S → Sig → S → Set}
+      → STS-total _⊢_⇀⟦_⟧_ → STS-total (_⊢_⇀⟦_⟧ᵢ*'_ IdSTS _⊢_⇀⟦_⟧_)
+    helper SS-total {s = s} {[]} = s , BS-base Id-nop
+    helper SS-total {s = s} {x ∷ sig} =
+      case SS-total of λ where
+        (s' , Ps') → map₂′ (BS-ind Ps') $ helper SS-total
 
 -- with a given base case
 ReflexiveTransitiveClosureᵢᵇ = _⊢_⇀⟦_⟧ᵢ*_

diff --git a/src/Ledger/Ledger/Properties.agda b/src/Ledger/Ledger/Properties.agda
@@ -64,7 +64,7 @@ instance
       ... | success (utxoSt' , _) | refl
         with computeCerts certΓ certSt txcerts | complete _ _ _ _ certStep
       ... | success (certSt' , _) | refl
-        with computeGov govΓ govSt (txgov txb) | complete _ _ _ _ govStep
+        with computeGov govΓ govSt (txgov txb) | complete govΓ _ _ _ govStep
       ... | success (govSt' , _) | refl = refl
       completeness ⟦ utxoSt' , govSt' , certState' ⟧ˡ (LEDGER-I⋯ i utxoStep)
         with isValid ≟ true