Computational
Computational-SUBUTXO : Computational _⊢_⇀⦇_,SUBUTXO⦈_ String
Computational-UTXOS : Computational _⊢_⇀⦇_,UTXOS⦈_ String
Computational-UTXO : Computational _⊢_⇀⦇_,UTXO⦈_ String
<!--
Computational-UTXOies.Computational.html#4951" class="Function"> =="Function"> MkComputational212" class="InductiveConstructor"> computeProof2" class="InductiveConstructor"> completeness where opentra.Specification.Utxo.Properties.Computational.html#10102" class="Function"> Computational id="10817" class="Symbol"> Computational-UTXOSBound"> renamingtin.Sigma.html#235" class="InductiveConstructor Operator"> (eConstructor Operator"> computeProof.Computational.html#10822" class="Bound"> toound"> computeProof-UTXOSid="10826" href="Ledger.Dijkstra.Specification.Utxo.Properties.Computational.html#10826" class="Bound"> ;l.html#10102" class="Function"> completeness" href="Ledger.Dijkstra.Specification.Utxo.Properties.Computational.html#10818" class="Bound"> toon.Utxo.Properties.Computational.html#10818" class="Bound"> completeness-UTXOS="Bound">)="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator"> genErr-premation.html#10518" class="InductiveConstructor"> :Constructor"> (985" class="Symbol">Γ×lmid="10989" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator"> :a.html#235" class="InductiveConstructor Operator"> UTxOEnvSpecification.Utxo.Properties.Computational.html#10991" class="Bound"> × Bool )(ary.Decidable.Core.html#2099" class="InductiveConstructor">s₀cation.Utxo.Properties.Computational.html#11009" class="Bound"> :al.html#11009" class="Bound"> UTxOStategda.Builtin.Equality.html#207" class="InductiveConstructor">)(ss="InductiveConstructor">txTop :utationalRelation.html#10518" class="InductiveConstructor"> TopLevelTx>).Unit.html#212" class="InductiveConstructor"> →. ¬.html#10518" class="InductiveConstructor"> (ructor">UTXO-Premises" class="InductiveConstructor"> Γ×lmr Operator"> s₀lass="Bound"> txTopf="Relation.Nullary.Decidable.Core.html#2136" class="InductiveConstructor">)e.html#2136" class="InductiveConstructor"> →ructor"> Stringes.Computational.html#11064" class="Bound"> genErr-premation.html#10560" class="InductiveConstructor"> Γ×lm.Properties.Computational.html#11114" class="Bound"> s₀ id="11134" class="Symbol"> txTops="Function"> ¬p47" href="Function.Base.html#4061" class="Function Operator"> = class="Function Operator"> casetionalEquality.Core.html#2080" class="Function"> dec-de-morganSymbol"> ¬p oflRelation.html#12265" class="Function"> λion"> wheres="Symbol"> ( inj₁="Ledger.Dijkstra.Specification.Utxo.Properties.Computational.html#4951" class="Function"> _)o.Properties.Computational.html#4951" class="Function"> →51" class="Function"> "¬ (SpendInputsOf txTop ≢ ∅)"Γ ( inj₂rator"> b) → case dec-de-morgan b of λ where (inj₁ _) → "¬ (inInterval (SlotOf Γ) (ValidIntervalOf txTop))" (inj₂ b) → case dec-de-morgan b of λ where (inj₁ _) → "¬ (minfee (PParamsOf Γ) txTop (UTxOOf s₀) ≤ TxFeesOf txTop)" (inj₂ b) → case dec-de-morgan b of λ where (inj₁ _) → "¬ (consumedBatch (DepositsChangeOf Γ) txTop (UTxOOf Γ) ≡ producedBatch (DepositsChangeOf Γ) txTop)" (inj₂ b) → case dec-de-morgan b of λ where (inj₁ _) → "¬ (legacyMode ≡ true → consumed (DepositsChangeOf Γ) txTop (UTxOOf Γ) ≡ produced (DepositsChangeOf Γ) txTop)" (inj₂ b) → case dec-de-morgan b of λ where (inj₁ _) → "¬ (SizeOf txTop ≤ maxTxSize (PParamsOf Γ))" (inj₂ b) → case dec-de-morgan b of λ where (inj₁ _) → "¬ (refScriptsSize txTop (UTxOOf Γ) ≤ (PParamsOf Γ) .maxRefScriptSizePerTx)" (inj₂ b) → case dec-de-morgan b of λ where (inj₁ _) → "¬ (allSpendInputs txTop ⊆ dom (UTxOOf Γ))" (inj₂ b) → case dec-de-morgan b of λ where (inj₁ _) → "¬ (allReferenceInputs txTop ⊆ dom (UTxOOf Γ))" (inj₂ b) → case dec-de-morgan b of λ where (inj₁ _) → "¬ (NoOverlappingSpendInputs txTop)" (inj₂ b) → case dec-de-morgan b of λ where (inj₁ _) → "¬ ((RedeemersOf txTop ˢ ≢ ∅) → collateralCheck (PParamsOf Γ) txTop (UTxOOf Γ))" (inj₂ b) → case dec-de-morgan b of λ where (inj₁ _) → "¬ (allMintedCoin txTop ≡ 0)" (inj₂ b) → case dec-de-morgan b of λ where (inj₁ _) → "¬ (∀[ (_ , o) ∈ ∣ TxOutsOf txTop ∣ ] ( (inject ((160 + utxoEntrySize o) * coinsPerUTxOByte (PParamsOf Γ)) ≤ᵗ txOutToValue o) × (serializedSize (txOutToValue o) ≤ maxValSize (PParamsOf Γ)) ))" (inj₂ b) → case dec-de-morgan b of λ where (inj₁ _) → "¬ (∀[ (a , _) ∈ range (TxOutsOf txTop) ] ( ((Sum.All (const ⊤) (λ a → AttrSizeOf a ≤ 64)) a) × (netId a ≡ NetworkId) ))" (inj₂ b) → case dec-de-morgan b of λ where (inj₁ _) → "¬ (∀[ a ∈ dom (WithdrawalsOf txTop)] NetworkIdOf a ≡ NetworkId)" (inj₂ b) → case dec-de-morgan b of λ where (inj₁ _) → "¬ (MaybeNetworkIdOf txTop ~ just NetworkId)" (inj₂ b) → "¬ (CurrentTreasuryOf txTop ~ just (TreasuryOf Γ))" -------------------------------------------------------------------------- -- computeProof for UTXO -------------------------------------------------------------------------- computeProof : (Γ×lm : UTxOEnv × Bool) (s : UTxOState) (txTop : TopLevelTx) → ComputationResult String (∃[ s' ] Γ×lm ⊢ s ⇀⦇ txTop ,UTXO⦈ s') computeProof (Γ , lm) s txTop with IsValidFlagOf txTop in isValid | computeProof-UTXOS Γ tt txTop | ¿ UTXO-Premises (Γ , lm) s txTop ¿ ... | true | success (tt , utxosProof) | yes prem = success ( $\begin{pmatrix} \,\htmlId{8620}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Transaction.html#5511}{\htmlId{8621}{\htmlClass{Field}{\text{UTxOOf}}}}\, \,\htmlId{8628}{\htmlClass{Bound}{\text{s}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{8630}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Dijkstra.Specification.Transaction.html#10727}{\htmlId{8632}{\htmlClass{Field}{\text{SpendInputsOf}}}}\, \,\htmlId{8646}{\htmlClass{Bound}{\text{txTop}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{8652}{\htmlClass{Function Operator}{\text{ᶜ}}}}\,\,\htmlId{8653}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{8655}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7809}{\htmlId{8658}{\htmlClass{Function}{\text{outs}}}}\, \,\htmlId{8663}{\htmlClass{Bound}{\text{txTop}}}\, \\ \,\href{Ledger.Prelude.Base.html#765}{\htmlId{8742}{\htmlClass{Field}{\text{FeesOf}}}}\, \,\htmlId{8749}{\htmlClass{Bound}{\text{s}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{8751}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Dijkstra.Specification.Transaction.html#9788}{\htmlId{8753}{\htmlClass{Field}{\text{TxFeesOf}}}}\, \,\htmlId{8762}{\htmlClass{Bound}{\text{txTop}}}\, \\ \,\href{Ledger.Prelude.Base.html#650}{\htmlId{8841}{\htmlClass{Field}{\text{DonationsOf}}}}\, \,\htmlId{8853}{\htmlClass{Bound}{\text{s}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{8855}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Prelude.Base.html#650}{\htmlId{8857}{\htmlClass{Field}{\text{DonationsOf}}}}\, \,\htmlId{8869}{\htmlClass{Bound}{\text{txTop}}}\, \end{pmatrix}$ , UTXO-valid (isValid , utxosProof , prem ) ) ... | false | success (tt , utxosProof) | yes prem = success ( $\begin{pmatrix} \,\htmlId{9205}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Transaction.html#5511}{\htmlId{9206}{\htmlClass{Field}{\text{UTxOOf}}}}\, \,\htmlId{9213}{\htmlClass{Bound}{\text{s}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{9215}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Dijkstra.Specification.Transaction.html#9623}{\htmlId{9217}{\htmlClass{Field}{\text{CollateralInputsOf}}}}\, \,\htmlId{9236}{\htmlClass{Bound}{\text{txTop}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{9242}{\htmlClass{Function Operator}{\text{ᶜ}}}}\,\,\htmlId{9243}{\htmlClass{Symbol}{\text{)}}}\, \\ \,\href{Ledger.Prelude.Base.html#765}{\htmlId{9318}{\htmlClass{Field}{\text{FeesOf}}}}\, \,\htmlId{9325}{\htmlClass{Bound}{\text{s}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{9327}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7946}{\htmlId{9329}{\htmlClass{Function}{\text{cbalance}}}}\, \,\htmlId{9338}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Transaction.html#5511}{\htmlId{9339}{\htmlClass{Field}{\text{UTxOOf}}}}\, \,\htmlId{9346}{\htmlClass{Bound}{\text{s}}}\, \,\href{Axiom.Set.Map.html#13536}{\htmlId{9348}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Dijkstra.Specification.Transaction.html#9623}{\htmlId{9350}{\htmlClass{Field}{\text{CollateralInputsOf}}}}\, \,\htmlId{9369}{\htmlClass{Bound}{\text{txTop}}}\,\,\htmlId{9374}{\htmlClass{Symbol}{\text{)}}}\, \\ \,\href{Ledger.Prelude.Base.html#650}{\htmlId{9449}{\htmlClass{Field}{\text{DonationsOf}}}}\, \,\htmlId{9461}{\htmlClass{Bound}{\text{s}}}\, \end{pmatrix}$ , UTXO-invalid (isValid , utxosProof , prem) ) ... | _ | _ | no ¬prem = failure (genErr-prem (Γ , lm) s txTop ¬prem) ... | _ | failure es | _ = failure es -------------------------------------------------------------------------- -- completeness for UTXO -------------------------------------------------------------------------- completeness : (Γ×lm : UTxOEnv × Bool) (s : UTxOState) (txTop : TopLevelTx) → ∀ s' → Γ×lm ⊢ s ⇀⦇ txTop ,UTXO⦈ s' → (map proj₁ $ computeProof Γ×lm s txTop) ≡ success s' completeness (Γ , lm) s txTop s' (UTXO-valid (refl , h-utxos , h-prem)) with computeProof-UTXOS Γ tt txTop in eqU | ¿ UTXO-Premises (Γ , lm) s txTop ¿ ... | success (tt , utxosProof) | yes prem = refl ... | success (tt , utxosProof) | no ¬prem = ⊥-elim (¬prem h-prem) ... | failure es | _ = ⊥-elim $ case trans (sym (map-failure {f = proj₁} eqU)) (completeness-UTXOS Γ tt txTop tt h-utxos) of λ () completeness (Γ , lm) s txTop s' (UTXO-invalid (refl , h-utxos , h-prem)) with computeProof-UTXOS Γ tt txTop in eqU | ¿ UTXO-Premises (Γ , lm) s txTop ¿ ... | success (tt , utxosProof) | yes prem = refl ... | success (tt , utxosProof) | no ¬prem = ⊥-elim (¬prem h-prem) ... | failure es | _ = ⊥-elim $ case trans (sym (map-failure {f = proj₁} eqU)) (completeness-UTXOS Γ tt txTop tt h-utxos) of λ ()