Changed ADHash to natural

scripts/bump-executable-spec.sh

@@ -18,7 +18,7 @@ chmod 755 -R $EXEC_SPEC_REPO_DIR
 pushd $EXEC_SPEC_REPO_DIR
 
 echo "Removing old files.."
-FILES_TO_RM=$(git ls-tree -r main --name-only | grep -vE "flake.lock|flake.nix|CHANGELOG.md|.gitignore")
+FILES_TO_RM=$(git ls-tree -r master --name-only | grep -vE "flake.lock|flake.nix|CHANGELOG.md|.gitignore")
 for f in $FILES_TO_RM; do
   rm -rf $f
 done
@@ -44,7 +44,10 @@ if [ $LEDGER_REPO_DIR ]; then
   pushd $LEDGER_REPO_DIR
   sed -i "s/tag: .*/tag: $EXEC_SPEC_COMMIT/" cabal.project
   sed -i "s/--sha256: .*/--sha256: sha256-0000000000000000000000000000000000000000000=/" cabal.project
+  sed -i "s/[^-]subdir/ --subdir/" cabal.project
+  sed -i 's/location: .*$/location: https:\/\/github.com\/Soupstraw\/exec-spec-temporary\.git/' cabal.project
+  #COMMIT_SHA=$(nix run nix-prefetch-git -- https://github.com/Soupstraw/exec-spec-temporary --rev $EXEC_SPEC_COMMIT | jq .hash)
+  #sed -i "s/--sha256 .*$/--sha256 $COMMIT_SHA/"
   popd
-  echo "Updated cabal.project in cardano-ledger. Replace sha256 with the hash given by 'nix develop'"
 fi
 echo "Done!"

src/Ledger/Certs.lagda

@@ -314,7 +314,8 @@ data _⊢_⇀⦇_,DELEG⦈_ where
   DELEG-delegate : let open PParams pp in
     ∙ (c ∉ dom rwds → d ≡ keyDeposit)
     ∙ (c ∈ dom rwds → d ≡ 0)
-    ∙ mv ∈ mapˢ (just ∘ credVoter DRep) delegatees ∪ ❴ nothing ❵
+    ∙ mv ∈ mapˢ (just ∘ credVoter DRep) delegatees ∪
+        fromList ( nothing ∷ just abstainRep ∷ just noConfidenceRep ∷ [] )
     ∙ mkh ∈ mapˢ just (dom pools) ∪ ❴ nothing ❵
       ────────────────────────────────
       ⟦ pp , pools , delegatees ⟧ᵈᵉ ⊢
@@ -429,7 +430,7 @@ data _⊢_⇀⦇_,CERTBASE⦈_ where
     refresh          = mapPartial getDRepVote (fromList vs)
     refreshedDReps   = mapValueRestricted (const (e + drepActivity)) dReps refresh
     wdrlCreds        = mapˢ stake (dom wdrls)
-    validVoteDelegs  = voteDelegs ∣^ mapˢ (credVoter DRep) (dom dReps)
+    validVoteDelegs  = voteDelegs ∣^ (mapˢ (credVoter DRep) (dom dReps) ∪ fromList (noConfidenceRep ∷ abstainRep ∷ []))
     in
     ∙ filter isKeyHash wdrlCreds ⊆ dom voteDelegs
     ∙ mapˢ (map₁ stake) (wdrls ˢ) ⊆ rewards ˢ

src/Ledger/Certs/Properties.agda

@@ -26,7 +26,8 @@ instance
   Computational-DELEG .computeProof ⟦ pp , pools , delegatees ⟧ᵈᵉ ⟦ _ , _ , rwds ⟧ᵈ = λ where
     (delegate c mv mc d) → case ¿ (c ∉ dom rwds → d ≡ pp .PParams.keyDeposit)
                                 × (c ∈ dom rwds → d ≡ 0)
-                                × mv ∈ mapˢ (just ∘ credVoter DRep) delegatees ∪ ❴ nothing ❵
+                                × mv ∈ mapˢ (just ∘ credVoter DRep) delegatees ∪
+                                    fromList ( nothing ∷ just abstainRep ∷ just noConfidenceRep ∷ [] )
                                 × mc ∈ mapˢ just (dom pools) ∪ ❴ nothing ❵
                                 ¿ of λ where
       (yes p) → success (-, DELEG-delegate p)
@@ -38,7 +39,8 @@ instance
   Computational-DELEG .completeness ⟦ pp , pools , delegatees ⟧ᵈᵉ ⟦ _ , _ , rwds ⟧ᵈ (delegate c mv mc d)
     s' (DELEG-delegate p) rewrite dec-yes (¿ (c ∉ dom rwds → d ≡ pp .PParams.keyDeposit)
                                            × (c ∈ dom rwds → d ≡ 0)
-                                           × mv ∈ mapˢ (just ∘ credVoter DRep) delegatees ∪ ❴ nothing ❵
+                                           × mv ∈ mapˢ (just ∘ credVoter DRep) delegatees ∪
+                                               fromList ( nothing ∷ just abstainRep ∷ just noConfidenceRep ∷ [] )
                                            × mc ∈ mapˢ just (dom pools) ∪ ❴ nothing ❵
                                            ¿) p .proj₂ = refl
   Computational-DELEG .completeness ⟦ _ , _ , _ ⟧ᵈᵉ ⟦ _ , _ , rwds ⟧ᵈ (dereg c d) _ (DELEG-dereg p)

src/Ledger/Conway/Conformance/Certs.agda

@@ -104,7 +104,13 @@ data _⊢_⇀⦇_,DELEG⦈_ where
   DELEG-delegate : let open PParams pp in
     ∙ (c ∉ dom rwds → d ≡ keyDeposit)
     ∙ (c ∈ dom rwds → d ≡ 0)
-    ∙ mv ∈ mapˢ (just ∘ credVoter DRep) delegatees ∪ ❴ nothing ❵
+    ∙ mv ∈ mapˢ (just ∘ credVoter DRep) delegatees ∪
+        fromList
+          ( nothing
+          ∷ just abstainRep
+          ∷ just noConfidenceRep
+          ∷ []
+          )
     ∙ mkh ∈ mapˢ just (dom pools) ∪ ❴ nothing ❵
       ────────────────────────────────
       ⟦ pp , pools , delegatees ⟧ᵈᵉ ⊢
@@ -170,7 +176,7 @@ data _⊢_⇀⦇_,CERTBASE⦈_ : CertEnv → CertState → ⊤ → CertState →
         refresh         = mapPartial getDRepVote (fromList vs)
         refreshedDReps  = mapValueRestricted (const (e + drepActivity)) dReps refresh
         wdrlCreds       = mapˢ stake (dom wdrls)
-        validVoteDelegs  = voteDelegs ∣^ mapˢ (credVoter DRep) (dom dReps)
+        validVoteDelegs  = voteDelegs ∣^ (mapˢ (credVoter DRep) (dom dReps) ∪ fromList (noConfidenceRep ∷ abstainRep ∷ []))
     in
     ∙ filterˢ isKeyHash wdrlCreds ⊆ dom voteDelegs
     ∙ mapˢ (map₁ stake) (wdrls ˢ) ⊆ rewards ˢ

src/Ledger/Conway/Conformance/Certs/Properties.agda

@@ -22,7 +22,8 @@ instance
   Computational-DELEG .computeProof ⟦ pp , pools , delegatees ⟧ᵈᵉ ⟦ _ , _ , rwds , dep ⟧ᵈ = λ where
     (delegate c mv mc d) → case ¿ (c ∉ dom rwds → d ≡ pp .PParams.keyDeposit)
                                 × (c ∈ dom rwds → d ≡ 0)
-                                × mv ∈ mapˢ (just ∘ credVoter DRep) delegatees ∪ ❴ nothing ❵
+                                × mv ∈ mapˢ (just ∘ credVoter DRep) delegatees ∪
+                                    fromList ( nothing ∷ just abstainRep ∷ just noConfidenceRep ∷ [] )
                                 × mc ∈ mapˢ just (dom pools) ∪ ❴ nothing ❵ ¿ of λ where
       (yes p) → success (-, DELEG-delegate p )
       (no ¬p) → failure (genErrors ¬p)
@@ -34,7 +35,8 @@ instance
   Computational-DELEG .completeness ⟦ pp , pools , delegatees ⟧ᵈᵉ ⟦ _ , _ , rwds , dep ⟧ᵈ (delegate c mv mc d)
     s' (DELEG-delegate p) rewrite dec-yes (¿ (c ∉ dom rwds → d ≡ pp .PParams.keyDeposit)
                                            × (c ∈ dom rwds → d ≡ 0)
-                                           × mv ∈ mapˢ (just ∘ credVoter DRep) delegatees ∪ ❴ nothing ❵
+                                           × mv ∈ mapˢ (just ∘ credVoter DRep) delegatees ∪
+                                               fromList ( nothing ∷ just abstainRep ∷ just noConfidenceRep ∷ [] )
                                            × mc ∈ mapˢ just (dom pools) ∪ ❴ nothing ❵ ¿) p .proj₂ = refl
   Computational-DELEG .completeness ⟦ _ , _ , _ ⟧ᵈᵉ ⟦ _ , _ , rwds , dep ⟧ᵈ (dereg c d) _ (DELEG-dereg p)
     rewrite dec-yes (¿ (c , 0) ∈ rwds × (CredentialDeposit c , d) ∈ dep ¿) p .proj₂ = refl

src/Ledger/Conway/Foreign/HSLedger/Core.agda

@@ -34,11 +34,11 @@ instance
   Hashable-⊤ = λ where .hash tt → 0
 
 module Implementation where
-  Network          = ⊤
+  Network          = ℕ
   SlotsPerEpochᶜ   = 100
   StabilityWindowᶜ = 10
   Quorum           = 1
-  NetworkId        = tt
+  NetworkId        = 0 -- Testnet
 
   SKey = ℕ
   VKey = ℕ
@@ -49,10 +49,10 @@ module Implementation where
   sign       = _+_
   ScriptHash = ℕ
 
-  Data         = ⊤
+  Data         = ℕ
   Dataʰ        = mkHashableSet Data
   toData : ∀ {A : Type} → A → Data
-  toData _ = tt
+  toData _ = 0
 
   PlutusScript = ⊤
   ExUnits      = ℕ × ℕ
@@ -96,7 +96,7 @@ module Implementation where
 
   TxId            = ℕ
   Ix              = ℕ
-  AuxiliaryData   = ⊤
+  AuxiliaryData   = ℕ
   DocHash         = ℕ
   tokenAlgebra    = coinTokenAlgebra
 

src/Ledger/hs-src/test/UtxowSpec.hs

@@ -64,7 +64,7 @@ initEnv :: UTxOEnv
 initEnv = MkUTxOEnv {ueSlot = 0, uePparams = initParams, ueTreasury = 0}
 
 baseAddr :: Integer -> Addr
-baseAddr n = Left BaseAddr{baseNet = (), basePay = KeyHashObj n, baseStake = KeyHashObj n}
+baseAddr n = Left BaseAddr{baseNet = 0, basePay = KeyHashObj n, baseStake = KeyHashObj n}
 
 a0 :: Addr
 a0 = baseAddr 0
@@ -106,7 +106,7 @@ bodyFromSimple pp stxb = let s = 5 in MkTxBody
   , txdonation    = 0
   , txup          = Nothing
   , txADhash      = Nothing
-  , txNetworkId   = Just ()
+  , txNetworkId   = Just 0
   , curTreasury   = Nothing
   , collateral    = MkHSSet []
   , reqSigHash    = MkHSSet []

src/ScriptVerification/LedgerImplementation.agda

@@ -30,11 +30,11 @@ instance
   Hashable-⊤ = λ where .hash tt → 0
 
 module Implementation where
-  Network          = ⊤
+  Network          = ℕ
   SlotsPerEpochᶜ   = 100
   StabilityWindowᶜ = 10
   Quorum           = 1
-  NetworkId        = tt
+  NetworkId        = 0
 
   SKey = ℕ
   VKey = ℕ
@@ -92,7 +92,7 @@ module Implementation where
 
   TxId            = ℕ
   Ix              = ℕ
-  AuxiliaryData   = ⊤
+  AuxiliaryData   = ℕ
   DocHash         = ℕ
   tokenAlgebra    = coinTokenAlgebra
 

src/ScriptVerification/Lib.agda

@@ -81,7 +81,7 @@ createUTxO : (index : ℕ)
            → Maybe (D ⊎ DataHash)
            → TxIn × TxOut
 createUTxO index wallet value d = (index , index)
-                                , (inj₁ (record { net = tt ; pay = KeyHashObj wallet ; stake = KeyHashObj wallet })
+                                , (inj₁ (record { net = 0 ; pay = KeyHashObj wallet ; stake = KeyHashObj wallet })
                                   , value , d , nothing)
 
 createInitUtxoState : (wallets : ℕ)