Agda Functions Index

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

Operators

AVM › Objects

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

AVM › SmallExample

• _≤v_

Foundation › BasicTypes

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

Foundation › Hyperproperties

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

Foundation › InteractionTrees

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

Regular Functions

AVM › Examples

• KVStore
• abortWithMsg
• apply-kv-event
• closeAccount
• closeWithBalance
• commitWithResult
• counterExample
• createCounter
• deposit
• handleBalance
• handleDeposit
• handleResult
• handleUpdateResult
• handleWithdraw
• helper
• invalidMsg
• kudosTransfer
• msg-to-event
• ok?
• processTransfers
• replay-account
• replay-counter
• replay-kv
• step-account
• step-counter
• step-kv
• transferBatch
• updateBalance
• updateHelper
• withdraw
• φ-account
• φ-account-aux
• φ-counter
• φ-kv
• φ-kv-aux

AVM › Instruction

• AVMProgram
• AVMProgram₀
• AVMProgram₁
• AVMProgram₂
• AVMProgram₄
• ISA

AVM › Interpreter

• addPendingCreate
• addPendingDestroy
• addPendingTransfer
• addPendingWrite
• applyCreates
• applyDestroy
• applyDestroys
• applyTransfer
• applyTransfers
• applyWrite
• applyWrites
• callObjInTx
• checkAll
• checkOwnership
• collect
• collectMatches
• containsObserved
• createWithMeta
• destroyObjInTx
• destroyObjNoTx
• ensureObserved
• executeController
• executeInstruction
• executeInstr₀
• executeInstr₁
• executeInstr₂
• executeIntrospect
• executeMachine
• executeObj
• executePure
• executeTx
• go
• handleCall
• inCreates
• inDestroys
• initMeta
• interpret
• interpretAux
• lookupObjectWithMeta
• lookupPendingCreate
• lookupPendingTransfer
• makeLogEntry
• pendingInputsFor
• remove
• removePendingCreate
• transferObjInTx
• transferObjNoTx
• updateMeta
• validateObserved

AVM › Objects

• BehaviouralState
• InputSequence
• ObjectBehaviour
• 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

AVM › Runtime

• AVMResult
• BaseResult
• Input
• Message
• MetaStore
• ObjectStore
• Output
• PureFunctions
• PureResult
• Trace
• TxResult
• TxWrite

AVM › SmallExample

• ControllerId
• ControllerVersion
• MachineId
• TxId
• Val
• allObjectIds
• emptyFuns
• eqNat
• exCtrl
• exMachine
• exOid
• freshObjectId
• freshTxId
• getFreshIdCounter
• initState
• initStore
• interpretValue
• invalidTeleportProg
• invalidTeleportResult
• isReachableController
• isReachableMachine
• meta0
• simpleObj
• stagedResult
• stagedTransferProg
• sucVersion
• targetCtrl

AVM › Transactions

• withTransaction

Foundation › BasicTypes

• Agda@++-assoc
• Agda@++-right-id
• FinSet
• Pred
• all
• concat
• concatMap
• cong
• elem
• filter
• foldr
• fst
• hasDuplicates
• head
• just-injective
• just≢nothing
• length
• map
• map-maybe
• not
• null
• 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

RM › Types › Action

• LogicVKOuterHash

RM › Types › Compliance

• ComplianceProof
• MerklePath
• createComplianceUnit

RM › Types › ConsumedCreated

• isConsumed
• isCreated

RM › Types › Delta

• DeltaProof
• compose
• empty
• fromComplianceWitnesses

RM › Types › Identities

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

RM › Types › Logic

• isConsumedArgs

RM › Types › Nonce

• defaultNonce

RM › Types › Nullifier

• toNonce

RM › Types › NullifierKey

• checkNullifierKey
• commitment

RM › Types › Program

• StorageKey
• genObjectId

RM › Types › Resource

• isEphemeral
• isPersistent
• nullifier

RM › Types › Transaction

• generateDeltaProof

---

References to other modules

This page references the following modules:

• AVM.Examples
  • Symbols: CounterMsg, Key, KVMsg, KVEvent, AccountMsg, AccountOutput, VInt, VBool, VString, VPair, VNil, VList, inc, dec, key, put, del, get, put-event, del-event, depositMsg, withdrawMsg, balanceMsg, ok, error-insufficient, balance-val, withdraw, deposit, ok?, kudosTransfer, abortWithMsg, commitWithResult, handleDeposit, handleWithdraw, createCounter, counterExample, handleResult, updateBalance, invalidMsg, helper, handleUpdateResult, updateHelper, transferBatch, processTransfers, closeAccount, closeWithBalance, handleBalance, replay-counter, φ-counter, step-counter, KVStore, apply-kv-event, replay-kv, msg-to-event, φ-kv-aux, φ-kv, step-kv, replay-account, φ-account-aux, φ-account, step-account
• AVM.Instruction
  • Symbols: Safety, ObjInstruction, IntrospectInstruction, Instr₀, TxInstruction, Instr₁, PureInstruction, Instr₂, MachineInstruction, ControllerInstruction, Instruction, NondetInstruction, LinearConstraint, ConstraintInstruction, Instr₄, WeightedVal, ConstraintId, Safe, Unsafe, createObj, destroyObj, call, self, input, getCurrentMachine, reflect, scryMeta, scryDeep, Obj, Introspect, beginTx, commitTx, abortTx, Tx, callPure, registerPure, Pure, getMachine, teleport, moveObject, getCurrentController, getController, transferObject, getCurrentVersion, switchVersion, Machine, Controller, obj-create, obj-destroy, obj-call, get-self, get-input, get-current-machine, obj-scry-meta, obj-scry-deep, obj-reflect, tx-begin, tx-commit, tx-abort, call-pure, register-pure, get-machine, do-teleport, move-object, get-current-controller, get-controller, transfer-object, get-current-version, switch-version, choose, require, mkCid, UseOnce, newConstraint, satisfy, Nondet, Constr, ISA, AVMProgram₀, AVMProgram₁, AVMProgram₂, AVMProgram, AVMProgram₄
• AVM.Interpreter
  • Symbols: lookupObjectWithMeta, lookupPendingCreate, go, lookupPendingTransfer, updateMeta, createWithMeta, initMeta, makeLogEntry, pendingInputsFor, collect, addPendingWrite, addPendingCreate, removePendingCreate, remove, addPendingDestroy, addPendingTransfer, containsObserved, ensureObserved, inCreates, inDestroys, validateObserved, checkAll, checkOwnership, applyCreates, applyWrite, applyWrites, applyDestroy, applyDestroys, applyTransfer, applyTransfers, handleCall, callObjInTx, transferObjInTx, transferObjNoTx, destroyObjInTx, destroyObjNoTx, executeObj, executeIntrospect, collectMatches, executeTx, executePure, executeMachine, executeController, executeInstr₀, executeInstr₁, executeInstr₂, executeInstruction, interpretAux, interpret, Interpreter, GenericInterpreter
• AVM.Objects
  • Symbols: →[]_, →*[]_, Object, WellFormedObjectType, SequentialObject, mkObjType, wfObjType, mkObj, transition, ε-trans, step-trans, InputSequence, ε, 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, ·, ≈φ[]_, ≈ᵒ, ≈ˢ
• AVM.Runtime
  • Symbols: Message, Input, Output, ObjError, IntrospectError, TxError, DistribError, PureError, BaseError, TxLayerError, PureLayerError, AVMError, EventType, Result, ObjectMeta, Store, State, LogEntry, Success, mkMeta, mkStore, ErrObjectNotFound, ErrObjectAlreadyDestroyed, ErrObjectAlreadyExists, ErrInvalidInput, ErrObjectRejectedCall, ErrMetadataCorruption, ErrStoreCorruption, ErrTxConflict, ErrTxNotFound, ErrTxAlreadyCommitted, ErrTxAlreadyAborted, ErrNoActiveTx, ErrInvalidDuringTx, ErrControllerUnreachable, ErrUnauthorizedTransfer, ErrVersionMismatch, ErrCrossControllerTx, ErrMachineUnreachable, ErrInvalidMachineTransfer, ErrFunctionNotFound, ErrFunctionAlreadyRegistered, obj-error, introspect-error, base-error, tx-error, tx-layer-error, pure-error, pure-layer-error, distrib-error, err-object-not-found, err-object-destroyed, err-object-exists, err-invalid-input, err-object-rejected, err-metadata-corruption, err-store-corruption, err-tx-conflict, err-tx-not-found, err-tx-committed, err-tx-aborted, err-no-active-tx, err-invalid-during-tx, err-function-not-found, err-function-registered, err-controller-unreachable, err-unauthorized-transfer, err-version-mismatch, err-cross-controller-tx, err-machine-unreachable, err-invalid-machine-transfer, ObjectCreated, ObjectDestroyed, ObjectCalled, ObjectMoved, ExecutionMoved, ObjectTransferred, ControllerSwitched, TransactionStarted, TransactionCommitted, TransactionAborted, ErrorOccurred, mkLogEntry, mkSuccess, success, failure, ObjectStore, MetaStore, TxWrite, PureFunctions, Trace, BaseResult, TxResult, PureResult, AVMResult
• AVM.SmallExample
  • Symbols: Val, freshObjectId, MachineId, ControllerId, ControllerVersion, TxId, freshTxId, simpleObj, eqNat, getFreshIdCounter, allObjectIds, interpretValue, isReachableController, isReachableMachine, sucVersion, exOid, exMachine, exCtrl, meta0, initStore, emptyFuns, initState, targetCtrl, stagedTransferProg, stagedResult, invalidTeleportProg, invalidTeleportResult, ≤v, Run
• AVM.Transactions
  • Symbols: withTransaction
• 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, null, head, filter, FinSet, Pred, elem, concat, hasDuplicates, concatMap, all, 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
• RM.Types.Action
  • Symbols: Tag, DeletionCriterion, LogicVerifierInput, Action, DeleteImmediately, StoreForever, LogicVKOuterHash
• RM.Types.Compliance
  • Symbols: ComplianceWitness, ComplianceInstance, ComplianceUnit, MerklePath, ComplianceProof, createComplianceUnit
• RM.Types.ConsumedCreated
  • Symbols: Created, Consumed, ConsumedCreated, isCreated, isConsumed
• RM.Types.Delta
  • Symbols: DeltaWitness, DeltaProof, fromComplianceWitnesses, compose, empty
• RM.Types.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
• RM.Types.Logic
  • Symbols: LogicArgs, Logic, isConsumedArgs
• RM.Types.Nonce
  • Symbols: Nonce, defaultNonce
• RM.Types.Nullifier
  • Symbols: Nullifier, privateMk, toNonce
• RM.Types.NullifierKey
  • Symbols: NullifierKey, NullifierKeyCommitment, NullifierKeyMatchesCommitment, universal, secret, ofSecret, checkNullifierKey, commitment
• RM.Types.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
• RM.Types.Resource
  • Symbols: LogicRef, Resource, CanNullifyResource, isEphemeral, isPersistent, nullifier
• RM.Types.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.≤', 'AVM.SmallExample.≤v', 'Foundation.BasicTypes.≤?']
• _<: chose Foundation.BasicTypes._<?_ from ['Foundation.BasicTypes.<?', 'Foundation.InteractionTrees.<$>']

?>