Agda Functions Index

This page lists all functions and operators defined in the Agda modules.

Operators

AVM › Objects

• _·_
• _≈ˢ_
• _≈φ[_]_
• _≈ᵒ_

Foundation › BasicTypes

• _*ℕ_
• _++_
• _+ℕ_
• _<?_?_
• _>>=ᴹ_
• _>>_
• _∈Pred_
• _∎
• _∘_
• _∧_
• _∨_
• _≟ℕ_
• _≡⟨_⟩_
• _≡⟨⟩_
• _≢_
• _≤_?_
• _≤_
• _≥_
• _⊆_
• begin_
• case_of_
• if_then_else_

Foundation › Hyperproperties

• Agda@[_]
• _≤ᴼ_
• _⊨_
• _⊨α_
• _⊨ᴴ_

Foundation › InteractionTrees

• _<?_$>_
• _>>=_

Regular Functions

AVM › Bytecode

• decode
• decodeCommit
• decodeScry
• encode

AVM › Instruction

• AVMProgram
• Filter
• ISA
• Input
• Message
• Output
• Store
• SystemProgram
• Trace
• TxId
• TxLog
• closeAccount
• closeWithBalance
• counterExample
• createCounter
• deposit
• helper
• invalidMsg
• kudosTransfer
• ok??
• processTransfers
• transferBatch
• updateBalance
• withdraw

AVM › Objects

• BehaviouralState
• InputSequence
• ObjectBehaviour
• ObjectType
• behavioural-state-equiv
• can-process
• counter-always-defined
• counter-object
• counter-type
• counter-wf
• create-object
• echo-type
• equiv-after-input
• equiv-preserved
• execute-step
• initial-output
• is-defined
• objecttype-to-behaviour
• output
• output-of
• prefix-def
• process-input
• process-preserves-wf
• reachable-from
• run-object-itree
• transition-preserves-type
• ·-++-assoc
• ε
• ≈ˢ-refl
• ≈ˢ-sym
• ≈ˢ-trans
• ≈φ-refl
• ≈φ-sym
• ≈φ-trans
• ≈ᵒ-refl
• ≈ᵒ-sym
• ≈ᵒ-trans

Foundation › BasicTypes

• Agda@++-assoc
• Agda@++-right-id
• FinSet
• Pred
• cong
• foldr
• fst
• just-injective
• just≢nothing
• length
• map
• map-maybe
• not
• snd
• sym
• trans
• ¬
• ∃
• ∃-syntax
• ⊥-elim

Foundation › Hyperproperties

• HyperProp
• Hypersafety
• Obs
• SysAsProp
• TraceFin
• TraceInf
• TraceProp
• kSafety
• size
• α⋆

Foundation › InteractionTrees

• EventSig
• Handler
• ITree-Monad
• Impl
• Interface
• bind-step
• interp
• interp-step
• ret
• tau
• trigger
• vis

Goose › Anoma › Action

• LogicVKOuterHash

Goose › Anoma › Compliance

• ComplianceProof
• MerklePath
• createComplianceUnit

Goose › Anoma › ConsumedCreated

• isConsumed
• isCreated

Goose › Anoma › Delta

• DeltaProof
• compose
• empty
• fromComplianceWitnesses

Goose › Anoma › Identities

• Ciphertext
• Commitment
• EngineId
• EngineName
• ExternalId
• ExternalIdentity
• Identity
• InternalId
• NodeId
• ObjectId
• Plaintext
• Signable
• isLocalEngineID
• isRemoteEngineID

Goose › Anoma › Logic

• isConsumedArgs

Goose › Anoma › Nonce

• defaultNonce

Goose › Anoma › Nullifier

• toNonce

Goose › Anoma › NullifierKey

• checkNullifierKey
• commitment

Goose › Anoma › Program

• StorageKey
• genObjectId

Goose › Anoma › Resource

• isEphemeral
• isPersistent
• nullifier

Goose › Anoma › Transaction

• generateDeltaProof

---

References to other modules

This page references the following modules:

• AVM.Bytecode
  • Symbols: Opcode, Bytecode, DecodeResult, OP_BEGIN_TX, OP_COMMIT_TX, OP_ABORT_TX, OP_CREATE_OBJ, OP_DESTROY_OBJ, OP_CALL, OP_SCRY, OP_REFLECT, OP_SELF, OP_INPUT, BC, SafeOp, UnsafeOp, TypeError, encode, decode, decodeCommit, decodeScry
• AVM.Instruction
  • Symbols: Val, Safety, Instr₀, Object, Ctx, State, AVMEvent, VInt, VBool, VString, VPair, VNil, VList, ctx, st, ev, Safe, Unsafe, beginTx, commitTx, abortTx, createObj, destroyObj, call, self, input, scry, reflect, Message, Input, Output, Store, TxLog, TxId, Trace, ISA, Filter, AVMProgram, SystemProgram, withdraw, deposit, ok?, kudosTransfer, createCounter, counterExample, updateBalance, invalidMsg, helper, transferBatch, processTransfers, closeAccount, closeWithBalance
• AVM.Objects
  • Symbols: mkObj, →[]_, →*[]_, WellFormedObjectType, SequentialObject, wfObjType, transition, ε-trans, step-trans, InputSequence, ε, ObjectType, is-defined, output-of, ≈φ-refl, ≈φ-sym, ≈φ-trans, BehaviouralState, output, process-input, can-process, ≈ᵒ-refl, ≈ᵒ-sym, ≈ᵒ-trans, ≈ˢ-refl, ≈ˢ-sym, ≈ˢ-trans, behavioural-state-equiv, counter-type, counter-wf, counter-always-defined, prefix-def, echo-type, transition-preserves-type, reachable-from, create-object, initial-output, counter-object, process-preserves-wf, equiv-preserved, equiv-after-input, ·-++-assoc, ObjectBehaviour, execute-step, objecttype-to-behaviour, run-object-itree, ·, ≈φ[]_, ≈ᵒ, ≈ˢ
• Foundation.BasicTypes
  • Symbols: ×, +, ⊥, Bool, ≡, Dec, Maybe, ℕ, List, ∈, Σ, ⊤, ↔, RawMonad, ,, ,Σ, inl, inr, tt, true, false, refl, yes, no, nothing, just, zero, suc, [], ∷, here, there, mk↔, fst, snd, ∃, ∃-syntax, ⊥-elim, ¬, not, sym, trans, cong, just≢nothing, just-injective, map-maybe, length, ++-assoc, ++-right-id, map, foldr, FinSet, Pred, case_of_, ∧, ∨, if_then_else_, ≢, begin_, ≡⟨⟩, ≡⟨⟩_, _∎, >>=ᴹ, +ℕ, *ℕ, ≥, ≤, ≤?, <?, ≟ℕ, ++, ∈Pred, ⊆, ∘, >>
• Foundation.Hyperproperties
  • Symbols: lsuc, ⊑, Stream, System, Sys×, []-⊑, ∷-⊑, size, TraceFin, TraceInf, TraceProp, HyperProp, SysAsProp, Obs, Hypersafety, kSafety, α⋆, ⊨, ⊨ᴴ, [_], ≤ᴼ, ⊨α
• Foundation.InteractionTrees
  • Symbols: Set₁, MessageEvent, ITreeF, ≈, ITree₁, ITree, send, receive, create, destroy, retF, tauF, visF, ret-eq, tau-left, tau-right, vis-eq, EventSig, Interface, ret, tau, vis, trigger, bind-step, ITree-Monad, Handler, Impl, interp, interp-step, >>=, <$>, first-definition, _
• Goose.Anoma.Action
  • Symbols: Tag, DeletionCriterion, LogicVerifierInput, Action, DeleteImmediately, StoreForever, LogicVKOuterHash
• Goose.Anoma.Compliance
  • Symbols: ComplianceWitness, ComplianceInstance, ComplianceUnit, MerklePath, ComplianceProof, createComplianceUnit
• Goose.Anoma.ConsumedCreated
  • Symbols: Created, Consumed, ConsumedCreated, isCreated, isConsumed
• Goose.Anoma.Delta
  • Symbols: DeltaWitness, DeltaProof, fromComplianceWitnesses, compose, empty
• Goose.Anoma.Identities
  • Symbols: NodeId, ObjectId, IDParams, Backend, Capabilities, Ed25519, Secp256k1, BLS, localMemory, localConnection, remoteConnection, commit, commitAndDecrypt, Ciphertext, Plaintext, Signable, ExternalId, InternalId, Identity, Commitment, EngineName, ExternalIdentity, EngineId, isLocalEngineID, isRemoteEngineID
• Goose.Anoma.Logic
  • Symbols: LogicArgs, Logic, isConsumedArgs
• Goose.Anoma.Nonce
  • Symbols: Nonce, defaultNonce
• Goose.Anoma.Nullifier
  • Symbols: Nullifier, privateMk, toNonce
• Goose.Anoma.NullifierKey
  • Symbols: NullifierKey, NullifierKeyCommitment, NullifierKeyMatchesCommitment, universal, secret, ofSecret, checkNullifierKey, commitment
• Goose.Anoma.Program
  • Symbols: decrypt, StorageValue, ResourceQuery, ProgramError, Program, str, int, bool, bytes, queryByObjectId, networkError, engineError, decryptionError, commitmentError, identityError, storageError, typeError, userError, skip, raise, tryCatch, withRandomGen, queryResource, submitTransaction, requestCommitment, generateIdentity, connectIdentity, deleteIdentity, getValue, setValue, deleteValue, StorageKey, genObjectId
• Goose.Anoma.Resource
  • Symbols: LogicRef, Resource, CanNullifyResource, isEphemeral, isPersistent, nullifier
• Goose.Anoma.Transaction
  • Symbols: Set, Transaction, generateDeltaProof

---

Symbol disambiguation log

The following references had multiple matches and were disambiguated:

• _<: chose Foundation.BasicTypes._<?_ from ['Foundation.BasicTypes.<?', 'Foundation.InteractionTrees.<$>']
• _≤: chose Foundation.BasicTypes._≤_ from ['Foundation.BasicTypes.≤', 'Foundation.BasicTypes.≤?', 'Foundation.Hyperproperties.≤ᴼ']
• _<: chose Foundation.BasicTypes._<?_ from ['Foundation.BasicTypes.<?', 'Foundation.InteractionTrees.<$>']

?>