formal-ledger-specification commit c64e42ba729d74e4bc16022cc7c051e99c…

…8a03e2
input-output-hk · May 7, 2024 · a9b7218 · a9b7218
1 parent d30dfe7
commit a9b7218
Show file tree

Hide file tree

Showing 6 changed files with 182 additions and 124 deletions.
diff --git a/MAlonzo/Code/Interface/ComputationalRelation.hs b/MAlonzo/Code/Interface/ComputationalRelation.hs
diff --git a/MAlonzo/Code/Ledger/Deleg/Properties.hs b/MAlonzo/Code/Ledger/Deleg/Properties.hs
@@ -2527,6 +2527,12 @@ d_Computational'45'CERTS_1604 ::
   MAlonzo.Code.Interface.ComputationalRelation.T_Computational_232
 d_Computational'45'CERTS_1604 v0
   = coe
-      MAlonzo.Code.Interface.ComputationalRelation.du_Computational'45'ReflexiveTransitiveClosure'7495'_734
+      MAlonzo.Code.Interface.ComputationalRelation.du_Computational'45'ReflexiveTransitiveClosure'7495'_762
       (coe d_Computational'45'CERTBASE_1474 (coe v0))
       (coe d_Computational'45'CERT_1090 (coe v0))
+      (coe
+         MAlonzo.Code.Interface.ComputationalRelation.C_InjectError'46'constructor_77373
+         (coe (\ v1 -> v1)))
+      (coe
+         MAlonzo.Code.Interface.ComputationalRelation.C_InjectError'46'constructor_77373
+         (coe (\ v1 -> v1)))
diff --git a/MAlonzo/Code/Ledger/Foreign/HSLedger.hs b/MAlonzo/Code/Ledger/Foreign/HSLedger.hs
@@ -32,7 +32,6 @@ import qualified MAlonzo.Code.Algebra.Morphism.Structures
 import qualified MAlonzo.Code.Algebra.PairOp
 import qualified MAlonzo.Code.Axiom.Set
 import qualified MAlonzo.Code.Axiom.Set.Map
-import qualified MAlonzo.Code.Class.Bifunctor
 import qualified MAlonzo.Code.Class.DecEq.Core
 import qualified MAlonzo.Code.Class.DecEq.Instances
 import qualified MAlonzo.Code.Class.Decidable.Core
@@ -47879,12 +47878,7 @@ d_gov'45'step_3038 v0 v1 v2
       (let v3
              = coe
                  MAlonzo.Code.Foreign.Convertible.C_Convertible'46'constructor_21
-                 (coe
-                    (\ v3 ->
-                       case coe v3 of
-                         MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 v4 -> coe v4
-                         _ -> MAlonzo.RTE.mazUnreachableError))
-                 (coe MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42) in
+                 (coe (\ v3 -> v3)) (coe (\ v3 -> v3)) in
        coe
          (let v4
                 = let v4
@@ -58513,26 +58507,29 @@ d_gov'45'step_3038 v0 v1 v2
                           _ -> MAlonzo.RTE.mazUnreachableError))))
             v2))
 -- Ledger.Foreign.HSLedger.certs-step
+certsStep ::
+  MAlonzo.Code.Ledger.Foreign.LedgerTypes.T_CertEnv_478 ->
+  MAlonzo.Code.Ledger.Foreign.LedgerTypes.T_CertState_530 ->
+  MAlonzo.Code.Agda.Builtin.List.T_List_10
+    () MAlonzo.Code.Ledger.Foreign.LedgerTypes.T_TxCert_122 ->
+  MAlonzo.Code.Ledger.Foreign.LedgerTypes.T_ComputationResult_12
+    MAlonzo.Code.Agda.Builtin.String.T_String_6
+    MAlonzo.Code.Ledger.Foreign.LedgerTypes.T_CertState_530
+certsStep = coe d_certs'45'step_3040
 d_certs'45'step_3040 ::
   MAlonzo.Code.Ledger.Foreign.LedgerTypes.T_CertEnv_478 ->
   MAlonzo.Code.Ledger.Foreign.LedgerTypes.T_CertState_530 ->
   [MAlonzo.Code.Ledger.Foreign.LedgerTypes.T_TxCert_122] ->
   MAlonzo.Code.Ledger.Foreign.LedgerTypes.T_ComputationResult_12
-    MAlonzo.Code.Data.Sum.Base.T__'8846'__30
+    MAlonzo.Code.Agda.Builtin.String.T_String_6
     MAlonzo.Code.Ledger.Foreign.LedgerTypes.T_CertState_530
 d_certs'45'step_3040 v0 v1 v2
   = coe
       MAlonzo.Code.Foreign.Convertible.d_to_18
       (let v3
              = coe
-                 MAlonzo.Code.Foreign.Convertible.du_Bifunctor'8658'Convertible_62
-                 (coe MAlonzo.Code.Class.Bifunctor.du_Bifunctor'45''8846'_158)
-                 (coe
-                    MAlonzo.Code.Foreign.Convertible.C_Convertible'46'constructor_21
-                    (coe (\ v3 -> v3)) (coe (\ v3 -> v3)))
-                 (coe
-                    MAlonzo.Code.Foreign.Convertible.C_Convertible'46'constructor_21
-                    (coe (\ v3 -> v3)) (coe (\ v3 -> v3))) in
+                 MAlonzo.Code.Foreign.Convertible.C_Convertible'46'constructor_21
+                 (coe (\ v3 -> v3)) (coe (\ v3 -> v3)) in
        coe
          (let v4
                 = coe

diff --git a/MAlonzo/Code/Ledger/Gov/Properties.hs b/MAlonzo/Code/Ledger/Gov/Properties.hs
@@ -2252,10 +2252,16 @@ d_Computational'45'GOV_1460 ::
   MAlonzo.Code.Interface.ComputationalRelation.T_Computational_232
 d_Computational'45'GOV_1460 v0
   = coe
-      MAlonzo.Code.Interface.ComputationalRelation.du_Computational'45'ReflexiveTransitiveClosure'7522''7495'_1054
+      MAlonzo.Code.Interface.ComputationalRelation.du_Computational'45'ReflexiveTransitiveClosure'7522''7495'_1088
       (coe
-         MAlonzo.Code.Interface.ComputationalRelation.du_Computational'45'Id_704)
+         MAlonzo.Code.Interface.ComputationalRelation.du_Computational'45'Id_726)
       (coe d_Computational'45'GOV''_1134 (coe v0))
+      (coe
+         MAlonzo.Code.Interface.ComputationalRelation.C_InjectError'46'constructor_77373
+         (coe (\ v1 -> MAlonzo.RTE.mazUnreachableError)))
+      (coe
+         MAlonzo.Code.Interface.ComputationalRelation.C_InjectError'46'constructor_77373
+         (coe (\ v1 -> v1)))
 -- Ledger.Gov.Properties.allEnactable-singleton
 d_allEnactable'45'singleton_1468 ::
   MAlonzo.Code.Ledger.Transaction.T_TransactionStructure_20 ->

diff --git a/MAlonzo/Code/Tactic/Constrs.hs b/MAlonzo/Code/Tactic/Constrs.hs
diff --git a/MAlonzo/Code/Tactic/ReduceDec.hs b/MAlonzo/Code/Tactic/ReduceDec.hs