Symbol Usage Index

This page shows where each symbol is used throughout the codebase.

`[]`

Defined in: Agda@[] Total references: 135

Other (135)

withdraw n = VList (VString "withdraw" ∷ VInt n ∷ \[\]) in AVM.Examples:102
go \[\] = nothing in AVM.Interpreter:95
ε = \[\] in AVM.Objects:99
simpleObj = mkObjType (λ _ → just (\[\])) in AVM.SmallExample:53
\[\] : List A in Foundation.BasicTypes:422
using (Pred; _⊆_; _↔_; ⊥; ¬; Σ; ℕ; _≤_; List; \[\]; _∷_; _≡_; refl; _×_; suc; zero; ∃; ∃-syntax; FinSe... in Foundation.Hyperproperties:16

`just`

Defined in: just Total references: 127

Other (127)

handleDeposit txId (just r₂) = in AVM.Examples:150
... | just obj | just meta = just (obj , meta) in AVM.Interpreter:82
... | just o = o in AVM.Objects:152
simpleObj = mkObjType (λ _ → just (\[\])) in AVM.SmallExample:53
just : A → Maybe A in Foundation.BasicTypes:276
isLocalEngineID (Maybe.just _ , _) = false in RM.Types.Identities:70

`List`

Defined in: List Total references: 112

Type Signatures (39)

VList : List Val → Val in AVM.Examples:32
history : List Input -- Accumulated inputs in AVM.Runtime:73
allObjectIds : State → List ObjectId in AVM.SmallExample:66
complianceUnits : List ComplianceUnit in RM.Types.Action:59
fromComplianceWitnesses : List ComplianceWitness → DeltaWitness in RM.Types.Delta:35
consumed : List Resource in RM.Types.Logic:21
actions : List Action in RM.Types.Transaction:19

Other (73)

IntrospectInstruction Unsafe (List (ObjectId × ObjectMeta)) in AVM.Instruction:229
open import Foundation.BasicTypes using (ℕ; List; Maybe) in AVM.Interpreter:12
InputSequence = List Input in AVM.Objects:62
## Lists in Foundation.BasicTypes:421
using (Pred; _⊆_; _↔_; ⊥; ¬; Σ; ℕ; _≤_; List; \[\]; _∷_; _≡_; refl; _×_; suc; zero; ∃; ∃-syntax; FinSe... in Foundation.Hyperproperties:16
MerklePath = List ℕ in RM.Types.Compliance:18

`nothing`

Defined in: nothing Total references: 112

Other (112)

handleDeposit txId nothing = abortWithMsg txId "deposit-call-failed" in AVM.Examples:149
... | just obj | nothing = nothing in AVM.Interpreter:83
is-defined φ xs = Object.behavior φ xs ≢ nothing in AVM.Objects:138
emptyFuns _ = nothing in AVM.SmallExample:106
nothing : Maybe A in Foundation.BasicTypes:275
isLocalEngineID (Maybe.nothing , _) = true in RM.Types.Identities:69

`_∷_`

Defined in: _∷_ Total references: 108

Other (108)

withdraw n = VList (VString "withdraw" ∷ VInt n ∷ \[\]) in AVM.Examples:102
go ((oid' , obj , meta) ∷ rest) with oid == oid' in AVM.Interpreter:96
xs · x = xs ++ (x ∷ \[\]) in AVM.Objects:106
_∷_ : A → List A → List A in Foundation.BasicTypes:423
using (Pred; _⊆_; _↔_; ⊥; ¬; Σ; ℕ; _≤_; List; \[\]; _∷_; _≡_; refl; _×_; suc; zero; ∃; ∃-syntax; FinSe... in Foundation.Hyperproperties:16

`ℕ`

Defined in: ℕ Total references: 90

Type Signatures (67)

VInt : ℕ → Val in AVM.Examples:27
(freshObjectId : ℕ → ObjectId) in AVM.Instruction:26
(freshObjectId : ℕ → ObjectId) in AVM.Runtime:20
(freshObjectId : ℕ → ObjectId) in AVM.Transactions:17
data ℕ : Set where in Foundation.BasicTypes:316
value : ℕ in RM.Types.Nonce:17
secret : ℕ → NullifierKey in RM.Types.NullifierKey:17
int : ℕ → StorageValue in RM.Types.Program:23
quantity : ℕ in RM.Types.Resource:39

Other (23)

open import Foundation.BasicTypes using (ℕ; List; Maybe) in AVM.Interpreter:12
open import Foundation.BasicTypes using (ℕ) in AVM.Objects:18
Val = ℕ in AVM.SmallExample:18
using (Pred; _⊆_; _↔_; ⊥; ¬; Σ; ℕ; _≤_; List; \[\]; _∷_; _≡_; refl; _×_; suc; zero; ∃; ∃-syntax; FinSe... in Foundation.Hyperproperties:16
MerklePath = List ℕ in RM.Types.Compliance:18
ObjectId = ℕ in RM.Types.Identities:17

`if_then_else_`

Defined in: if_then_else_ Total references: 85

Type Signatures (5)

if_then_else_ : {A : Set} → Bool → A → A → A in Foundation.BasicTypes:177
If-then-else syntax for boolean conditionals: in Foundation.BasicTypes:178

Other (80)

- Object identifiers as pairs of node IDs and strings in AVM.Examples:143
if success then in AVM.Examples:143
else in AVM.Examples:145
This module defines the operational semantics of the AVM by specifying how each in AVM.Interpreter:123
metadata = λ oid' → if oid == oid' then just meta in AVM.Interpreter:123
else Store.metadata (State.store st) oid' in AVM.Interpreter:124
if ok then ret res else in AVM.Transactions:41
throughout different entries in this website. in Foundation.BasicTypes:178

`Bool`

Defined in: Bool Total references: 72

Type Signatures (46)

VBool : Bool → Val in AVM.Examples:28
destroyObj : ObjectId → ObjInstruction Safe Bool -- May fail if object doesn't exist in AVM.Instruction:195
(_==_ : ∀ {A : Set} → A → A → Bool) in AVM.Interpreter:56
traceMode : Bool -- Debug tracing flag in AVM.Runtime:192
eqNat : ∀ {A : Set} → A → A → Bool in AVM.SmallExample:57
isCreated : ConsumedCreated → Bool in RM.Types.ConsumedCreated:23
isLocalEngineID : EngineId → Bool in RM.Types.Identities:68
isConsumedArgs : LogicArgs → Bool in RM.Types.Logic:34
bool : Bool → StorageValue in RM.Types.Program:24
ephemeral : Bool in RM.Types.Resource:41

Other (26)

## Boolean Type in Foundation.BasicTypes:137

`true`

Defined in: true Total references: 67

Other (67)

ok? (VString "ok") = true in AVM.Examples:108
... | true = just (obj , meta) in AVM.Interpreter:97
eqNat {A} x y = true in AVM.SmallExample:58
true : Bool in Foundation.BasicTypes:138
isCreated Created = true in RM.Types.ConsumedCreated:24
isLocalEngineID (Maybe.nothing , _) = true in RM.Types.Identities:69

`_,_`

Defined in: _,_ Total references: 66

Other (66)

freshObjectId n = ("default-node" , nat-to-string n) in AVM.Examples:54
is parameterized by an abstract object model, making it independent of any in AVM.Interpreter:82
This module formalises the core object model from the AVM green paper, including in AVM.Objects:378
_,_ : A → B → A × B in Foundation.BasicTypes:21
The product type represents pairs of values, fundamental for modeling object in Foundation.BasicTypes:33
isLocalEngineID (Maybe.nothing , _) = true in RM.Types.Identities:69
Anoma program representation reifying the local domain, solver and controller. in RM.Types.Program:75

`_×_`

Defined in: _×_ Total references: 66

Type Signatures (39)

lookupObjectWithMeta : ObjectId → State → Maybe (Object × ObjectMeta) in AVM.Interpreter:80
step : Input → Maybe (Output × Object) in AVM.Objects:369
data _×_ (A B : Set) : Set where in Foundation.BasicTypes:20
logicVerifierInputs : List (Tag × LogicVerifierInput) in RM.Types.Action:60
withRandomGen : (ℕ → Program × ℕ) → Program in RM.Types.Program:56

Other (27)

ObjectId = NodeId × String in AVM.Examples:44
IntrospectInstruction Unsafe (List (ObjectId × ObjectMeta)) in AVM.Instruction:229
TxWrite = ObjectId × Input in AVM.Runtime:138
using (Pred; _⊆_; _↔_; ⊥; ¬; Σ; ℕ; _≤_; List; \[\]; _∷_; _≡_; refl; _×_; suc; zero; ∃; ∃-syntax; FinSe... in Foundation.Hyperproperties:16
Identity = ExternalId × InternalId in RM.Types.Identities:39

`State`

Defined in: State Total references: 63

Other (63)

-- State helpers in AVM.Interpreter:60
Transactions provide atomicity. State modifications within a transaction remain in AVM.Runtime:165
getFreshIdCounter : State → ℕ in AVM.SmallExample:63

`Maybe`

Defined in: Maybe Total references: 61

Type Signatures (30)

handleDeposit : TxId → Maybe Val → AVMProgram₁ Val in AVM.Examples:148
call : ObjectId → Input → ObjInstruction Safe (Maybe Output) in AVM.Instruction:198
behavior : InputSequence → Maybe (List Output) in AVM.Objects:119
stagedTransferProg : AVMProgram (Maybe ControllerId) in AVM.SmallExample:131

Other (31)

open import Foundation.BasicTypes using (ℕ; List; Maybe) in AVM.Interpreter:12
ObjectStore = ObjectId → Maybe Object in AVM.Runtime:97
Option types or Maybe types handle partial operations and potential failures, crucial for in Foundation.BasicTypes:274
EngineId = Maybe NodeId × EngineName in RM.Types.Identities:62
→ (Maybe EngineId → Maybe EngineId → EngineId → Program) → Program in RM.Types.Program:62

`false`

Defined in: false Total references: 59

Other (59)

ok? (VString _) = false -- Any other string in AVM.Examples:109
... | false = go rest in AVM.Interpreter:98
; traceMode = false in AVM.SmallExample:123
false : Bool in Foundation.BasicTypes:139
isCreated Consumed = false in RM.Types.ConsumedCreated:25
isLocalEngineID (Maybe.just _ , _) = false in RM.Types.Identities:70

`_≡_`

Defined in: _≡_ Total references: 43

Type Signatures (28)

data _≡_ {A : Set} (x : A) : A → Set where in Foundation.BasicTypes:187
secret : {n m : ℕ} → n ≡ m → NullifierKeyMatchesCommitment (secret n) (ofSecret m) in RM.Types.NullifierKey:37

Other (15)

Object.behavior φ xs ≡ just o₁ → in AVM.Objects:177
using (Pred; _⊆_; _↔_; ⊥; ¬; Σ; ℕ; _≤_; List; \[\]; _∷_; _≡_; refl; _×_; suc; zero; ∃; ∃-syntax; FinSe... in Foundation.Hyperproperties:16

`_++_`

Defined in: _++_ Total references: 40

Type Signatures (12)

_++_ : {A : Set} → List A → List A → List A in Foundation.BasicTypes:440

Other (28)

step-counter history msg with φ-counter (history ++ (msg ∷ \[\])) in AVM.Examples:343
record st { txLog = (State.txLog st) ++ ((oid , inp) ∷ \[\]) } in AVM.Interpreter:182
xs · x = xs ++ (x ∷ \[\]) in AVM.Objects:106

`refl`

Defined in: refl Total references: 39

Other (39)

... | nothing = ⊥-elim (defined refl) in AVM.Objects:153
refl : x ≡ x in Foundation.BasicTypes:188
using (Pred; _⊆_; _↔_; ⊥; ¬; Σ; ℕ; _≤_; List; \[\]; _∷_; _≡_; refl; _×_; suc; zero; ∃; ∃-syntax; FinSe... in Foundation.Hyperproperties:16

`success`

Defined in: success Total references: 39

Other (39)

in success (mkSuccess output st' (entry ∷ \[\])) in AVM.Interpreter:382
Instruction execution produces either success or failure. The Result type in AVM.Runtime:516

`ITree`

Defined in: ITree Total references: 38

Other (38)

AVMProgram₀ = ITree (Instr₀ Safe) in AVM.Instruction:278
interpretAux : ∀ {A} → ITree (Instr Safe) A → State → Trace → AVMResult A in AVM.Interpreter:815
occurrence ofITree₁ E Rwithin the tau constructor's type argument. in Foundation.InteractionTrees:115

`mkSuccess`

Defined in: mkSuccess Total references: 38

Other (38)

in success (mkSuccess output st' (entry ∷ \[\])) in AVM.Interpreter:382
constructor mkSuccess in AVM.Runtime:498

`ret`

Defined in: ret Total references: 38

Type Signatures (7)

ret : R -> ITree₁ E R in Foundation.InteractionTrees:146

Other (31)

This module provides concrete examples demonstrating the AVM instruction set defined in AVM.Examples:138
as extra projections. For example, retrieving the current output for a sequential in AVM.Objects:770
transaction boundaries and states a correspondence lemma with the interpreter. in AVM.Transactions:41

`_>>=_`

Defined in: _>>=_ Total references: 36

Type Signatures (8)

_>>=_ : ITree E R → (R → ITree E S) → ITree E S in Foundation.InteractionTrees:186

Other (28)

trigger (Tx beginTx) >>= λ txId → in AVM.Examples:131
behaviour state inp >>= in AVM.Objects:793
trigger (Tx beginTx) >>= λ txid → in AVM.SmallExample:133
trigger {E = Instr₁ Safe} (Tx beginTx) >>= λ txid → in AVM.Transactions:38

`VString`

Defined in: VString Total references: 36

Other (36)

VString : String → Val in AVM.Examples:29

`ObjectMeta`

Defined in: ObjectMeta Total references: 33

Other (33)

object metadata (ObjectMeta), and execution state (State). All runtime in AVM.Instruction:224
lookupObjectWithMeta : ObjectId → State → Maybe (Object × ObjectMeta) in AVM.Interpreter:80
record ObjectMeta : Set where in AVM.Runtime:69
meta0 : ObjectMeta in AVM.SmallExample:97

`Safe`

Defined in: Safe Total references: 33

Other (33)

### Safety datatype in AVM.Instruction:178
**Safety constraint**: teleportation is invalid during active transactions. in AVM.Interpreter:815
trigger {E = Instr₁ Safe} (Tx beginTx) >>= λ txid → in AVM.Transactions:38

`Program`

Defined in: Program Total references: 31

Other (31)

module RM.Types.Program where in RM.Types.Program:52

`suc`

Defined in: suc Total references: 31

Other (31)

trigger (Tx(commitTx txId)) >>= λ success → in AVM.Examples:326
-- A trivial object type that always succeeds and returns no outputs in AVM.SmallExample:79
open import Agda.Primitive using (Level; lsuc) in Foundation.BasicTypes:318
open import Agda.Primitive using (Level; lsuc) in Foundation.Hyperproperties:16

`SequentialObject`

Defined in: SequentialObject Total references: 29

Other (29)

SequentialObject, _Observational Equivalence_, and _Behavioural State_. in AVM.Objects:245

`failure`

Defined in: failure Total references: 28

Other (28)

... | nothing = failure (err-invalid-input oid inp) in AVM.Interpreter:376
Instruction execution produces either success or failure. The Result type in AVM.Runtime:517

`trigger`

Defined in: trigger Total references: 27

Type Signatures (2)

trigger : {E : EventSig} {A : Set} → E A → ITree E A in Foundation.InteractionTrees:167

Other (25)

trigger (Tx beginTx) >>= λ txId → in AVM.Examples:131
trigger (Tx beginTx) >>= λ txid → in AVM.SmallExample:133
trigger {E = Instr₁ Safe} (Tx beginTx) >>= λ txid → in AVM.Transactions:38

`zero`

Defined in: zero Total references: 27

Other (27)

... | zero = zero -- Cannot go below zero in AVM.Examples:328
zero : ℕ in Foundation.BasicTypes:317
using (Pred; _⊆_; _↔_; ⊥; ¬; Σ; ℕ; _≤_; List; \[\]; _∷_; _≡_; refl; _×_; suc; zero; ∃; ∃-syntax; FinSe... in Foundation.Hyperproperties:16

`mkObj`

Defined in: mkObj Total references: 26

Other (26)

constructor mkObjType in AVM.Objects:246

`Object`

Defined in: Object Total references: 24

Other (24)

- Object identifiers as pairs of node IDs and strings in AVM.Examples:84
the definitions of _Sequential Object_ as in in AVM.Objects:116
This small example demonstrates howtransferObjectis staged inside a in AVM.SmallExample:43
(ObjectId : Set) in AVM.Transactions:27

`_·_`

Defined in: _·_ Total references: 23

Type Signatures (23)

_·_ : InputSequence → Input → InputSequence in AVM.Objects:105

`AVMResult`

Defined in: AVMResult Total references: 23

Type Signatures (23)

handleCall : ObjectId → Input → State → Object → ObjectMeta → AVMResult (Maybe Val) in AVM.Interpreter:374
AVMResult : Set → Set in AVM.Runtime:534
stagedResult : AVMResult (Maybe ControllerId) in AVM.SmallExample:138

`InputSequence`

Defined in: InputSequence Total references: 23

Type Signatures (22)

InputSequence : Set in AVM.Objects:61

Other (1)

using (Object; Input; Output; InputSequence; mkObjType) in AVM.Examples:84

`AVMProgram₁`

Defined in: AVMProgram₁ Total references: 21

Type Signatures (19)

kudosTransfer : ObjectId → ObjectId → ℕ → AVMProgram₁ Val in AVM.Examples:129
AVMProgram₁ : Set → Set in AVM.Instruction:309

Other (2)

-- Uses AVMProgram₁ which includes Base + Transactions in AVM.Transactions:36

`Input`

Defined in: Input Total references: 21

Type Signatures (8)

(Val : Set) -- Values (data) - used for both Input and Output in AVM.Interpreter:166

Other (13)

using (Object; Input; Output; InputSequence; mkObjType) in AVM.Examples:93
The module is parameterized by Val which serves as both Input and Output types in AVM.Instruction:198
-- Input/Output types for object communication in AVM.Objects:732
type O. The current implementation uses the same type (Val) for both Input and Output in AVM.Runtime:52

`_≈φ[_]_`

Defined in: _≈φ[_]_ Total references: 19

Type Signatures (10)

_≈φ\[_\]_ : InputSequence → Object → InputSequence → Set in AVM.Objects:188

Other (9)

\[^AbelAdelsbergerSetzer-JFP-2017]. in AVM.Objects:189

`EventSig`

Defined in: EventSig Total references: 19

Type Signatures (19)

EventSig : Set₁ in Foundation.InteractionTrees:26

`makeLogEntry`

Defined in: makeLogEntry Total references: 18

Type Signatures (18)

makeLogEntry : EventType → State → LogEntry in AVM.Interpreter:157

`Safety`

Defined in: Safety Total references: 17

Type Signatures (1)

**Safety constraint**: teleportation is invalid during active transactions. in AVM.Interpreter:810

Other (16)

### Safety datatype in AVM.Instruction:177

`ISA`

Defined in: ISA Total references: 16

Type Signatures (1)

(Instr : Safety → ISA) in AVM.Interpreter:810

Other (15)

## Baseline Instruction Set Architecture (ISA) in AVM.Instruction:166

`pure-layer-error`

Defined in: pure-layer-error Total references: 16

Other (16)

pure-layer-error : PureLayerError → AVMError in AVM.Runtime:335

`TraceProp`

Defined in: TraceProp Total references: 16

Type Signatures (16)

TraceProp : {ℓ : Level} → Set ℓ → Set (lsuc ℓ) in Foundation.Hyperproperties:82

`∃-syntax`

Defined in: ∃-syntax Total references: 16

Type Signatures (11)

counter-always-defined : ∀ xs → ∃\[ o ∈ List Output \] (Object.behavior counter-type xs ≡ just o) in AVM.Objects:477
∃-syntax : {ℓ : Level} (A : Set ℓ) → (A → Set ℓ) → Set ℓ in Foundation.BasicTypes:61

Other (5)

\[^AbelAdelsbergerSetzer-JFP-2017]. in AVM.Objects:477
using (Pred; _⊆_; _↔_; ⊥; ¬; Σ; ℕ; _≤_; List; \[\]; _∷_; _≡_; refl; _×_; suc; zero; ∃; ∃-syntax; FinSe... in Foundation.Hyperproperties:16

`_≈_`

Defined in: _≈_ Total references: 15

Type Signatures (15)

data _≈_ {E : EventSig} {R : Set} in Foundation.InteractionTrees:301

`_≡⟨_⟩_`

Defined in: _≡⟨_⟩_ Total references: 14

Other (14)

≡⟨ sym (just-injective eq1) ⟩ in AVM.Objects:470
infixr 2 _≡⟨⟩_ _≡⟨_⟩_ in Foundation.BasicTypes:241

`call`

Defined in: call Total references: 14

Other (14)

trigger (Obj(call fromAcc (withdraw amount))) >>= λ mr₁ → in AVM.Examples:132
safe programs cannot call unsafe operations at compile time. in AVM.Instruction:198
Handling a call invokes the object behavior with accumulated inputs and produces output. in AVM.Interpreter:490

`EventType`

Defined in: EventType Total references: 14

Type Signatures (1)

makeLogEntry : EventType → State → LogEntry in AVM.Interpreter:157

Other (13)

### EventType in AVM.Runtime:440

`tx-layer-error`

Defined in: tx-layer-error Total references: 14

Other (14)

tx-layer-error : TxLayerError → PureLayerError in AVM.Runtime:325

`_≈ᵒ_`

Defined in: _≈ᵒ_ Total references: 13

Type Signatures (13)

_≈ᵒ_ : SequentialObject → SequentialObject → Set in AVM.Objects:308

`EngineId`

Defined in: EngineId Total references: 13

Type Signatures (13)

EngineId : Set in RM.Types.Identities:61
decrypt : EngineId → Ciphertext → (Plaintext → Program) → Program in RM.Types.Program:59

`IntrospectInstruction`

Defined in: IntrospectInstruction Total references: 13

Type Signatures (1)

executeIntrospect : ∀ {s A} → IntrospectInstruction s A → State → AVMResult A in AVM.Interpreter:504

Other (12)

#### IntrospectInstruction datatype in AVM.Instruction:216

`Resource`

Defined in: Resource Total references: 13

Other (13)

Compliance structures for zero-knowledge proofs in the Anoma Resource Machine. in RM.Types.Compliance:26
Resource logic structures for the Anoma Resource Machine. in RM.Types.Logic:19
open import RM.Types.Resource in RM.Types.Program:57
Representation of Anoma Resource data. in RM.Types.Resource:33

`ok?`

Defined in: ok? Total references: 12

Type Signatures (12)

ok? : Val → Bool in AVM.Examples:107

`AccountMsg`

Defined in: AccountMsg Total references: 11

Type Signatures (11)

data AccountMsg : Set where in AVM.Examples:442

`executeIntrospect`

Defined in: executeIntrospect Total references: 11

Type Signatures (11)

executeIntrospect : ∀ {s A} → IntrospectInstruction s A → State → AVMResult A in AVM.Interpreter:504

`Key`

Defined in: Key Total references: 11

Other (11)

### Key-Value Store Object (Stateless) in AVM.Examples:357

`KVMsg`

Defined in: KVMsg Total references: 11

Type Signatures (11)

data KVMsg : Set where in AVM.Examples:360

`ProgramError`

Defined in: ProgramError Total references: 11

Type Signatures (11)

data ProgramError : Set where in RM.Types.Program:38

`System`

Defined in: System Total references: 11

Other (11)

## Traces and Systems in Foundation.Hyperproperties:66

`⊤`

Defined in: ⊤ Total references: 11

Other (11)

abortTx : TxId → TxInstruction Safe ⊤ in AVM.Instruction:290
(trigger {E = Instr₁ Safe} {A = ⊤} (Tx (abortTx txid)) >>= λ _ → ret res) in AVM.Transactions:42
record ⊤ : Set where in Foundation.BasicTypes:104
send : String → MessageEvent ⊤ in Foundation.InteractionTrees:43

`ControllerId`

Defined in: ControllerId Total references: 10

Type Signatures (10)

ControllerId : Set in AVM.SmallExample:26

`Instruction`

Defined in: Instruction Total references: 10

Other (10)

module AVM.Instruction in AVM.Instruction:415
-- Import Runtime and Instruction modules (which use Object as parameter) in AVM.Interpreter:790

`Instr₁`

Defined in: Instr₁ Total references: 10

Other (10)

### Instr₁ instruction set, adds transactional support in AVM.Instruction:300
#### Transactional Instruction Set (Instr₁) in AVM.Interpreter:763
trigger {E = Instr₁ Safe} (Tx beginTx) >>= λ txid → in AVM.Transactions:38

`Instr₄`

Defined in: Instr₄ Total references: 10

Type Signatures (10)

### Instr₄ instruction set: intent-aware ISA in AVM.Instruction:841

`length`

Defined in: length Total references: 10

Type Signatures (4)

length : {A : Set} → List A → ℕ in Foundation.BasicTypes:434

Other (6)

counter-type = mkObjType (λ inputs → just ((VInt (length inputs)) ∷ \[\])) in AVM.Objects:452
using (Pred; _⊆_; _↔_; ⊥; ¬; Σ; ℕ; _≤_; List; \[\]; _∷_; _≡_; refl; _×_; suc; zero; ∃; ∃-syntax; FinSe... in Foundation.Hyperproperties:16
"DeltaProof for a transaction with " ++ˢ nat-to-string (length actions) ++ˢ " actions and signing ke... in RM.Types.Transaction:32

`ObjInstruction`

Defined in: ObjInstruction Total references: 10

Type Signatures (1)

executeObj : ∀ {s A} → ObjInstruction s A → State → AVMResult A in AVM.Interpreter:450

Other (9)

#### ObjInstruction datatype in AVM.Instruction:192

`Pred`

Defined in: Pred Total references: 10

Other (10)

## Predicates and Set Relations in Foundation.BasicTypes:560
using (Pred; _⊆_; _↔_; ⊥; ¬; Σ; ℕ; _≤_; List; \[\]; _∷_; _≡_; refl; _×_; suc; zero; ∃; ∃-syntax; FinSe... in Foundation.Hyperproperties:16

`replay-account`

Defined in: replay-account Total references: 10

Type Signatures (10)

replay-account : List AccountMsg → ℕ in AVM.Examples:460

`¬`

Defined in: ¬ Total references: 10

Type Signatures (4)

¬ : Set → Set in Foundation.BasicTypes:126

Other (6)

using (Pred; _⊆_; _↔_; ⊥; ¬; Σ; ℕ; _≤_; List; \[\]; _∷_; _≡_; refl; _×_; suc; zero; ∃; ∃-syntax; FinSe... in Foundation.Hyperproperties:16

`_→*[_]_`

Defined in: _→*[_]_ Total references: 9

Other (9)

data _→*\[_\]_ in AVM.Objects:578
\[^AbelAdelsbergerSetzer-JFP-2017]. in AVM.Objects:581

`_≈ˢ_`

Defined in: _≈ˢ_ Total references: 9

Type Signatures (9)

_≈ˢ_ : SequentialObject → SequentialObject → Set in AVM.Objects:366

`_⊆_`

Defined in: _⊆_ Total references: 9

Type Signatures (3)

_⊆_ : {ℓ : Level} {A : Set ℓ} → Pred {ℓ} A → Pred {ℓ} A → Set (lsuc ℓ) in Foundation.BasicTypes:576

Other (6)

using (Pred; _⊆_; _↔_; ⊥; ¬; Σ; ℕ; _≤_; List; \[\]; _∷_; _≡_; refl; _×_; suc; zero; ∃; ∃-syntax; FinSe... in Foundation.Hyperproperties:16

`ControllerInstruction`

Defined in: ControllerInstruction Total references: 9

Type Signatures (1)

executeController : ∀ {s A} → ControllerInstruction s A → State → AVMResult A in AVM.Interpreter:691

Other (8)

#### ControllerInstruction datatype in AVM.Instruction:390

`ControllerVersion`

Defined in: ControllerVersion Total references: 9

Type Signatures (9)

ControllerVersion : Set in AVM.SmallExample:29

`interpretAux`

Defined in: interpretAux Total references: 9

Type Signatures (9)

interpretAux : ∀ {A} → ITree (Instr Safe) A → State → Trace → AVMResult A in AVM.Interpreter:815

`is-defined`

Defined in: is-defined Total references: 9

Type Signatures (9)

is-defined : Object → InputSequence → Set in AVM.Objects:137

`ITreeF`

Defined in: ITreeF Total references: 9

Other (9)

##ITreeFStructure Functor in Foundation.InteractionTrees:99

`no`

Defined in: no Total references: 9

Other (9)

Alternative notation for Σ interpreted as existential quantification: in Foundation.BasicTypes:232
checkNullifierKey universal (ofSecret _) = no (λ ()) in RM.Types.NullifierKey:46

`NullifierKey`

Defined in: NullifierKey Total references: 9

Other (9)

open import RM.Types.NullifierKey in RM.Types.Compliance:28
module RM.Types.NullifierKey where in RM.Types.NullifierKey:15
open import RM.Types.NullifierKey in RM.Types.Resource:65

`TraceInf`

Defined in: TraceInf Total references: 9

Type Signatures (9)

TraceInf : {ℓ : Level} → Set ℓ → Set ℓ in Foundation.Hyperproperties:56

`TxInstruction`

Defined in: TxInstruction Total references: 9

Type Signatures (1)

executeTx : ∀ {s A} → TxInstruction s A → State → AVMResult A in AVM.Interpreter:560

Other (8)

### TxInstruction datatype in AVM.Instruction:287

`∃`

Defined in: ∃ Total references: 9

Type Signatures (2)

∃ : {ℓ : Level} {A : Set ℓ} → (A → Set ℓ) → Set ℓ in Foundation.BasicTypes:58

Other (7)

using (Pred; _⊆_; _↔_; ⊥; ¬; Σ; ℕ; _≤_; List; \[\]; _∷_; _≡_; refl; _×_; suc; zero; ∃; ∃-syntax; FinSe... in Foundation.Hyperproperties:16

`_≟ℕ_`

Defined in: _≟ℕ_ Total references: 8

Type Signatures (7)

_≟ℕ_ : (m n : ℕ) → Dec (m ≡ n) in Foundation.BasicTypes:401

Other (1)

checkNullifierKey (secret n) (ofSecret m) with n ≟ℕ m in RM.Types.NullifierKey:48

`_≥_`

Defined in: _≥_ Total references: 8

Type Signatures (8)

_≥_ : ℕ → ℕ → Set in Foundation.BasicTypes:360

`base-error`

Defined in: base-error Total references: 8

Other (8)

base-error : BaseError → TxLayerError in AVM.Runtime:315

`closeWithBalance`

Defined in: closeWithBalance Total references: 8

Type Signatures (8)

closeWithBalance : Val → AVMProgram₁ Val in AVM.Examples:271

`counter-type`

Defined in: counter-type Total references: 8

Type Signatures (8)

counter-type : Object in AVM.Objects:451

`CounterMsg`

Defined in: CounterMsg Total references: 8

Type Signatures (8)

data CounterMsg : Set where in AVM.Examples:316

`DeltaWitness`

Defined in: DeltaWitness Total references: 8

Other (8)

record DeltaWitness : Set where in RM.Types.Delta:23
generateDeltaProof : DeltaWitness → List Action → DeltaProof in RM.Types.Transaction:30

`DistribError`

Defined in: DistribError Total references: 8

Type Signatures (8)

data DistribError : Set where in AVM.Runtime:272

`err-object-not-found`

Defined in: err-object-not-found Total references: 8

Other (8)

... | just _ | nothing | nothing | _ = failure (err-object-not-found oid) in AVM.Interpreter:478
pattern err-object-not-found oid = in AVM.Runtime:347

`executeObj`

Defined in: executeObj Total references: 8

Type Signatures (8)

executeObj : ∀ {s A} → ObjInstruction s A → State → AVMResult A in AVM.Interpreter:450

`helper`

Defined in: helper Total references: 8

Type Signatures (8)

We define helper functions for creating messages and validating responses: in AVM.Examples:203

`Instr₂`

Defined in: Instr₂ Total references: 8

Other (8)

### Instr₂ instruction set, adds pure function computation in AVM.Instruction:336
#### Extended Instruction Set (Instr₂) in AVM.Interpreter:776

`ObjError`

Defined in: ObjError Total references: 8

Type Signatures (8)

data ObjError : Set where in AVM.Runtime:233

`TxError`

Defined in: TxError Total references: 8

Type Signatures (8)

data TxError : Set where in AVM.Runtime:257

`VInt`

Defined in: VInt Total references: 8

Other (8)

VInt : ℕ → Val in AVM.Examples:27

`VList`

Defined in: VList Total references: 8

Other (8)

VList : List Val → Val in AVM.Examples:32

`⊥-elim`

Defined in: ⊥-elim Total references: 8

Type Signatures (2)

⊥-elim : {A : Set} → ⊥ → A in Foundation.BasicTypes:119

Other (6)

... | nothing = ⊥-elim (defined refl) in AVM.Objects:153

`_+ℕ_`

Defined in: _+ℕ_ Total references: 7

Type Signatures (6)

_+ℕ_ : ℕ → ℕ → ℕ in Foundation.BasicTypes:328

Other (1)

x +ℕ prev-bal in AVM.Examples:464

`_<?_`

Defined in: _<?_?_ Total references: 7

Type Signatures (6)

_<?_ : ℕ → ℕ → Bool in Foundation.BasicTypes:387

Other (1)

if 0 <? n then in AVM.Examples:273

`_==ℕ_`

Defined in: _==ℕ_ Total references: 7

Type Signatures (7)

_==ℕ_ : ℕ → ℕ → Bool in Foundation.BasicTypes:632

`_→[_]_`

Defined in: _→[_]_ Total references: 7

Other (7)

data _→\[_\]_ in AVM.Objects:555
The transition relationprevObj →[ input ] nextObjholds when the object's in AVM.Objects:569
\[^AbelAdelsbergerSetzer-JFP-2017]. in AVM.Objects:569

`_∈_`

Defined in: _∈_ Total references: 7

Type Signatures (2)

data _∈_ {A : Set} (x : A) : List A → Set where in Foundation.BasicTypes:525

Other (5)

syntax ∃-syntax A (λ x → B) = ∃\[ x ∈ A \] B in Foundation.BasicTypes:526
using (Pred; _⊆_; _↔_; ⊥; ¬; Σ; ℕ; _≤_; List; \[\]; _∷_; _≡_; refl; _×_; suc; zero; ∃; ∃-syntax; FinSe... in Foundation.Hyperproperties:16

`_∧_`

Defined in: _∧_ Total references: 7

Type Signatures (7)

_∧_ : Bool → Bool → Bool in Foundation.BasicTypes:154

`_∨_`

Defined in: _∨_ Total references: 7

Type Signatures (7)

_∨_ : Bool → Bool → Bool in Foundation.BasicTypes:162

`_≤?_`

Defined in: _≤_?_ Total references: 7

Type Signatures (6)

_≤?_ : ℕ → ℕ → Bool in Foundation.BasicTypes:380

Other (1)

if 0 ≤? n then in AVM.Examples:221

`AccountOutput`

Defined in: AccountOutput Total references: 7

Type Signatures (7)

data AccountOutput : Set where in AVM.Examples:474

`Backend`

Defined in: Backend Total references: 7

Type Signatures (3)

generateIdentity : Backend → IDParams → Capabilities in RM.Types.Program:61

Other (4)

## Backend Connection Types in RM.Types.Identities:88

`beginTx`

Defined in: beginTx Total references: 7

Other (7)

trigger (Tx beginTx) >>= λ txId → in AVM.Examples:131
beginTx : TxInstruction Safe TxId in AVM.Instruction:288
executeTx beginTx st = in AVM.Interpreter:561
trigger (Tx beginTx) >>= λ txid → in AVM.SmallExample:133
trigger {E = Instr₁ Safe} (Tx beginTx) >>= λ txid → in AVM.Transactions:38

`checkOwnership`

Defined in: checkOwnership Total references: 7

Type Signatures (7)

checkOwnership : ObjectId → ObjectMeta → State → Bool in AVM.Interpreter:288

`ConsumedCreated`

Defined in: ConsumedCreated Total references: 7

Other (7)

open import RM.Types.ConsumedCreated in RM.Types.Action:43
This module defines the ConsumedCreated type representing whether a resource is consumed or created.... in RM.Types.ConsumedCreated:15
open import RM.Types.ConsumedCreated in RM.Types.Logic:20

`distrib-error`

Defined in: distrib-error Total references: 7

Other (7)

distrib-error : DistribError → AVMError in AVM.Runtime:336

`executeController`

Defined in: executeController Total references: 7

Type Signatures (7)

executeController : ∀ {s A} → ControllerInstruction s A → State → AVMResult A in AVM.Interpreter:691

`executeTx`

Defined in: executeTx Total references: 7

Type Signatures (7)

executeTx : ∀ {s A} → TxInstruction s A → State → AVMResult A in AVM.Interpreter:560

`filter`

Defined in: filter Total references: 7

Type Signatures (7)

filter-map : {A B : Set} → (A → Maybe B) → List A → List B in AVM.Examples:393
filter : {A : Set} → (A → Bool) → List A → List A in Foundation.BasicTypes:504

`foldr`

Defined in: foldr Total references: 7

Type Signatures (4)

foldr : {A B : Set} → (A → B → B) → B → List A → B in Foundation.BasicTypes:476

Other (3)

let results = foldr collectMatches \[\] (allObjectIds st) in AVM.Interpreter:524
{ signingKey = foldr _++ˢ_ "" (map (λ w → w .rcv) witnesses) } in RM.Types.Delta:37

`invalidMsg`

Defined in: invalidMsg Total references: 7

Type Signatures (7)

invalidMsg : Val in AVM.Examples:205

`lookupPendingCreate`

Defined in: lookupPendingCreate Total references: 7

Type Signatures (7)

lookupPendingCreate : ObjectId → State → Maybe (Object × ObjectMeta) in AVM.Interpreter:91

`MachineId`

Defined in: MachineId Total references: 7

Type Signatures (7)

MachineId : Set in AVM.SmallExample:23

`MachineInstruction`

Defined in: MachineInstruction Total references: 7

Type Signatures (1)

executeMachine : ∀ {s A} → MachineInstruction s A → State → AVMResult A in AVM.Interpreter:648

Other (6)

#### MachineInstruction datatype in AVM.Instruction:367

`not`

Defined in: not Total references: 7

Type Signatures (3)

Alternative notation for Σ interpreted as existential quantification: in Foundation.BasicTypes:148

Other (4)

handleDeposit txId nothing = abortWithMsg txId "deposit-call-failed" in AVM.Examples:393
isLocalEngineID (Maybe.nothing , _) = true in RM.Types.Identities:73
isPersistent r = not (isEphemeral r) in RM.Types.Resource:57

`NullifierKeyCommitment`

Defined in: NullifierKeyCommitment Total references: 7

Type Signatures (7)

data NullifierKeyCommitment : Set where in RM.Types.NullifierKey:25
nullifierKeyCommitment : NullifierKeyCommitment in RM.Types.Resource:43

`obj-error`

Defined in: obj-error Total references: 7

Other (7)

obj-error : ObjError → BaseError in AVM.Runtime:305

`Output`

Defined in: Output Total references: 7

Type Signatures (1)

(Val : Set) -- Values (data) - used for both Input and Output in AVM.Interpreter:404

Other (6)

using (Object; Input; Output; InputSequence; mkObjType) in AVM.Examples:93
The module is parameterized by Val which serves as both Input and Output types in AVM.Instruction:198
-- Input/Output types for object communication in AVM.Objects:732
type O. The current implementation uses the same type (Val) for both Input and Output in AVM.Runtime:55

`PureInstruction`

Defined in: PureInstruction Total references: 7

Type Signatures (1)

executePure : ∀ {s A} → PureInstruction s A → State → AVMResult A in AVM.Interpreter:624

Other (6)

### PureInstruction datatype in AVM.Instruction:321

`replay-counter`

Defined in: replay-counter Total references: 7

Type Signatures (7)

replay-counter : List CounterMsg → ℕ in AVM.Examples:324

`Result`

Defined in: Result Total references: 7

Other (7)

## Result Types in AVM.Runtime:515

`StorageValue`

Defined in: StorageValue Total references: 7

Type Signatures (7)

data StorageValue : Set where in RM.Types.Program:21

`sym`

Defined in: sym Total references: 7

Type Signatures (2)

sym : {A : Set} {x y : A} → x ≡ y → y ≡ x in Foundation.BasicTypes:199

Other (5)

φ-equivalence is symmetric. in AVM.Objects:209

`tauF`

Defined in: tauF Total references: 7

Other (7)

... | tauF prog' = interpretAux prog' st trace in AVM.Interpreter:819
tauF : X → ITreeF E R X in Foundation.InteractionTrees:101

`tx-error`

Defined in: tx-error Total references: 7

Other (7)

tx-error : TxError → TxLayerError in AVM.Runtime:316

`updateMeta`

Defined in: updateMeta Total references: 7

Type Signatures (7)

updateMeta : ObjectId → ObjectMeta → State → State in AVM.Interpreter:119

`yes`

Defined in: yes Total references: 7

Other (7)

yes : A → Dec A in Foundation.BasicTypes:231
checkNullifierKey universal universal = yes universal in RM.Types.NullifierKey:45

`Σ`

Defined in: Σ Total references: 7

Other (7)

Σ InputSequence (λ hist' → hist' ≈φ\[ φ \] hist) in AVM.Objects:233
Dependent pair type (Σ type): in Foundation.BasicTypes:44
using (Pred; _⊆_; _↔_; ⊥; ¬; Σ; ℕ; _≤_; List; \[\]; _∷_; _≡_; refl; _×_; suc; zero; ∃; ∃-syntax; FinSe... in Foundation.Hyperproperties:16

`_,Σ_`

Defined in: _,Σ_ Total references: 6

Other (6)

counter-always-defined xs = ((VInt (length xs)) ∷ \[\]) ,Σ refl in AVM.Objects:478
constructor _,Σ_ in Foundation.BasicTypes:45

`_∸_`

Defined in: _∸_ Total references: 6

Type Signatures (6)

_∸_ : ℕ → ℕ → ℕ in Foundation.BasicTypes:347

`_≤ᴼ_`

Defined in: _≤ᴼ_ Total references: 6

Type Signatures (6)

_≤ᴼ_ : {ℓ : Level} {Σᵀ : Set ℓ} → Obs Σᵀ → TraceProp Σᵀ → Set (lsuc ℓ) in Foundation.Hyperproperties:169

`abortWithMsg`

Defined in: abortWithMsg Total references: 6

Type Signatures (6)

abortWithMsg : TxId → String → AVMProgram₁ Val in AVM.Examples:135

`Capabilities`

Defined in: Capabilities Total references: 6

Type Signatures (2)

generateIdentity : Backend → IDParams → Capabilities in RM.Types.Program:61

Other (4)

## Identity Capabilities in RM.Types.Identities:97

`case_of_`

Defined in: case_of_ Total references: 6

Type Signatures (4)

case_of_ : {A B C : Set} → A + B → (A → C) → (B → C) → C in Foundation.BasicTypes:87

Other (2)

The product type represents pairs of values, fundamental for modeling object in Foundation.BasicTypes:88

`checkAll`

Defined in: checkAll Total references: 6

Other (6)

validateObserved st = checkAll (State.observed st) in AVM.Interpreter:272

`collect`

Defined in: collect Total references: 6

Other (6)

pendingInputsFor oid st = collect (State.txLog st) in AVM.Interpreter:167

`cong`

Defined in: cong Total references: 6

Type Signatures (4)

cong : {A B : Set} {x y : A} (f : A → B) → x ≡ y → f x ≡ f y in Foundation.BasicTypes:213

Other (2)

≡⟨ cong (Object.behavior φ₁) (·-++-assoc hist₁ inp future) ⟩ in AVM.Objects:708

`ensureObserved`

Defined in: ensureObserved Total references: 6

Type Signatures (6)

ensureObserved : ObjectId → ObjectMeta → State → State in AVM.Interpreter:241

`err-cross-controller-tx`

Defined in: err-cross-controller-tx Total references: 6

Other (6)

... | false = failure (err-cross-controller-tx oid (ObjectMeta.currentController meta)) in AVM.Interpreter:406
pattern err-cross-controller-tx oid cid = in AVM.Runtime:418

`exOid`

Defined in: exOid Total references: 6

Type Signatures (6)

exOid : ObjectId in AVM.SmallExample:88

`HyperProp`

Defined in: HyperProp Total references: 6

Type Signatures (6)

HyperProp : {ℓ : Level} → Set ℓ → Set (lsuc (lsuc ℓ)) in Foundation.Hyperproperties:106

`Instr₀`

Defined in: Instr₀ Total references: 6

Other (6)

### Instr₀ instruction set, the minimal instruction set in AVM.Instruction:264
#### Basic Instruction Set (Instr₀) in AVM.Interpreter:753

`interpret`

Defined in: interpret Total references: 6

Other (6)

instruction transforms the VM state and generates log entries. The interpreter in AVM.Interpreter:829

`ITree₁`

Defined in: ITree₁ Total references: 6

Other (6)

occurrence ofITree₁ E Rwithin the tau constructor's type argument. in Foundation.InteractionTrees:67

`KVEvent`

Defined in: KVEvent Total references: 6

Type Signatures (6)

data KVEvent : Set where in AVM.Examples:369

`KVStore`

Defined in: KVStore Total references: 6

Type Signatures (6)

KVStore : Set in AVM.Examples:374

`lookupObjectWithMeta`

Defined in: lookupObjectWithMeta Total references: 6

Type Signatures (6)

lookupObjectWithMeta : ObjectId → State → Maybe (Object × ObjectMeta) in AVM.Interpreter:80

`Message`

Defined in: Message Total references: 6

Other (6)

-- Define Message as alias for Val (since Instruction's Message is hidden) in AVM.Examples:93
hiding (Input; Output; Message) in AVM.Objects:732
## Message Types in AVM.Runtime:49

`mkObjType`

Defined in: mkObjType Total references: 6

Other (6)

using (Object; Input; Output; InputSequence; mkObjType) in AVM.Examples:84
constructor mkObjType in AVM.Objects:117
using (Object; mkObjType) in AVM.SmallExample:43

`retF`

Defined in: retF Total references: 6

Other (6)

... | retF x = success (mkSuccess x st trace) in AVM.Interpreter:818
retF : R → ITreeF E R X in Foundation.InteractionTrees:100

`TxId`

Defined in: TxId Total references: 6

Type Signatures (6)

TxId : Set in AVM.SmallExample:32

`Val`

Defined in: Val Total references: 6

Other (6)

-- Values and identifiers are naturals for simplicity in AVM.SmallExample:17

`visF`

Defined in: visF Total references: 6

Other (6)

... | visF B instr k in AVM.Interpreter:820
visF : (A : Set) → E A → (A → X) → ITreeF E R X in Foundation.InteractionTrees:102

`ε`

Defined in: ε Total references: 6

Type Signatures (6)

ε : InputSequence in AVM.Objects:98

`φ-account-aux`

Defined in: φ-account-aux Total references: 6

Type Signatures (6)

φ-account-aux : List AccountMsg → Maybe AccountMsg → Maybe AccountOutput in AVM.Examples:479

`φ-kv-aux`

Defined in: φ-kv-aux Total references: 6

Type Signatures (6)

φ-kv-aux : List KVMsg → Maybe KVMsg → Maybe Val in AVM.Examples:410

`⊥`

Defined in: ⊥ Total references: 6

Type Signatures (5)

data ⊥ : Set where in Foundation.BasicTypes:113

Other (1)

using (Pred; _⊆_; _↔_; ⊥; ¬; Σ; ℕ; _≤_; List; \[\]; _∷_; _≡_; refl; _×_; suc; zero; ∃; ∃-syntax; FinSe... in Foundation.Hyperproperties:16

`++-assoc`

Defined in: Agda@++-assoc Total references: 5

Type Signatures (4)

++-assoc : ∀ {A} (xs ys zs : List A) → ((xs ++ ys) ++ zs) ≡ (xs ++ (ys ++ zs)) in Foundation.BasicTypes:452

Other (1)

≡⟨ cong (Object.behavior φ₁) (·-++-assoc hist₁ inp future) ⟩ in AVM.Objects:717

`[_]`

Defined in: Agda@[_] Total references: 5

Type Signatures (1)

\[_\] : {ℓ : Level} {Σᵀ : Set ℓ} → TraceProp Σᵀ → HyperProp Σᵀ in Foundation.Hyperproperties:136

Other (4)

using (Pred; _⊆_; _↔_; ⊥; ¬; Σ; ℕ; _≤_; List; \[\]; _∷_; _≡_; refl; _×_; suc; zero; ∃; ∃-syntax; FinSe... in Foundation.Hyperproperties:137

`_*ℕ_`

Defined in: _*ℕ_ Total references: 5

Type Signatures (5)

_*ℕ_ : ℕ → ℕ → ℕ in Foundation.BasicTypes:334

`_+_`

Defined in: _+_ Total references: 5

Type Signatures (5)

data _+_ (A B : Set) : Set where in Foundation.BasicTypes:75

`_||_`

Defined in: _||_ Total references: 5

Type Signatures (5)

_||_ : Bool → Bool → Bool in Foundation.BasicTypes:657

`_↔_`

Defined in: _↔_ Total references: 5

Other (5)

record _↔_ (A B : Set) : Set where in Foundation.BasicTypes:589
using (Pred; _⊆_; _↔_; ⊥; ¬; Σ; ℕ; _≤_; List; \[\]; _∷_; _≡_; refl; _×_; suc; zero; ∃; ∃-syntax; FinSe... in Foundation.Hyperproperties:16

`_∎`

Defined in: _∎ Total references: 5

Other (5)

∎ in AVM.Objects:474
infix 3 _∎ in Foundation.BasicTypes:242

`_≤_`

Defined in: _≤_ Total references: 5

Type Signatures (3)

_≤_ : ℕ → ℕ → Set in Foundation.BasicTypes:368

Other (2)

using (Pred; _⊆_; _↔_; ⊥; ¬; Σ; ℕ; _≤_; List; \[\]; _∷_; _≡_; refl; _×_; suc; zero; ∃; ∃-syntax; FinSe... in Foundation.Hyperproperties:16

`_⊑_`

Defined in: _⊑_ Total references: 5

Type Signatures (1)

data _⊑_ {ℓ : Level} {Σᵀ : Set ℓ} : TraceFin Σᵀ → TraceInf Σᵀ → Set ℓ where in Foundation.Hyperproperties:148

Other (4)

The prefix relationl ⊑ texpresses that finite tracelis a prefix of in Foundation.Hyperproperties:149

`abortTx`

Defined in: abortTx Total references: 5

Other (5)

trigger (Tx(abortTx txId)) >>= λ _ → in AVM.Examples:137
abortTx : TxId → TxInstruction Safe ⊤ in AVM.Instruction:290
executeTx (abortTx txid) st = in AVM.Interpreter:606
(trigger {E = Instr₁ Safe} {A = ⊤} (Tx (abortTx txid)) >>= λ _ → ret res) in AVM.Transactions:42

`applyCreates`

Defined in: applyCreates Total references: 5

Type Signatures (5)

applyCreates : List (ObjectId × Object × ObjectMeta) → State → State in AVM.Interpreter:297

`applyDestroys`

Defined in: applyDestroys Total references: 5

Type Signatures (5)

applyDestroys : List ObjectId → State → State in AVM.Interpreter:347

`applyTransfers`

Defined in: applyTransfers Total references: 5

Type Signatures (5)

applyTransfers : List (ObjectId × ControllerId) → State → State in AVM.Interpreter:364

`applyWrites`

Defined in: applyWrites Total references: 5

Type Signatures (5)

applyWrites : List (ObjectId × Input) → State → State in AVM.Interpreter:323

`AVMError`

Defined in: AVMError Total references: 5

Type Signatures (5)

data AVMError : Set where in AVM.Runtime:334

`AVMProgram₀`

Defined in: AVMProgram₀ Total references: 5

Type Signatures (2)

AVMProgram₀ : Set → Set in AVM.Instruction:277

Other (3)

-- Import AVMProgram₀ from Instruction module for implementation in AVM.Objects:745

`BaseError`

Defined in: BaseError Total references: 5

Type Signatures (5)

data BaseError : Set where in AVM.Runtime:304

`begin_`

Defined in: begin_ Total references: 5

Other (5)

begin in AVM.Objects:468
infix 1 begin_ in Foundation.BasicTypes:240

`bind-step`

Defined in: bind-step Total references: 5

Other (5)

observe (t >>= k) = bind-step (observe t) k in Foundation.InteractionTrees:187

`can-process`

Defined in: can-process Total references: 5

Type Signatures (5)

can-process : SequentialObject → Input → Set in AVM.Objects:294

`checkNullifierKey`

Defined in: checkNullifierKey Total references: 5

Type Signatures (5)

checkNullifierKey : (key : NullifierKey) → (nfc : NullifierKeyCommitment) in RM.Types.NullifierKey:43

`Commitment`

Defined in: Commitment Total references: 5

Type Signatures (3)

Created : Commitment → Tag in RM.Types.Action:19
requestCommitment : EngineId → Signable → (Commitment → Program) → Program in RM.Types.Program:60
nullifierKeyCommitment : NullifierKeyCommitment in RM.Types.Resource:87

Other (2)

## Commitments in RM.Types.Identities:45

`commitTx`

Defined in: commitTx Total references: 5

Other (5)

trigger (Tx(commitTx txId)) >>= λ success → in AVM.Examples:142
commitTx : TxId → TxInstruction Safe Bool -- May fail if conflicts in AVM.Instruction:289
executeTx (commitTx txid) st in AVM.Interpreter:576
trigger {E = Instr₁ Safe} (Tx (commitTx txid)) >>= λ ok → in AVM.Transactions:40

`containsObserved`

Defined in: containsObserved Total references: 5

Type Signatures (5)

containsObserved : ObjectId → List (ObjectId × ControllerVersion) → Bool in AVM.Interpreter:230

`Dec`

Defined in: Dec Total references: 5

Other (5)

## Equality and Decidability in Foundation.BasicTypes:230
## Decidable Nullifier Key Check in RM.Types.NullifierKey:44

`destroyObj`

Defined in: destroyObj Total references: 5

Other (5)

trigger (Obj(destroyObj accountToClose)) >>= λ _ → in AVM.Examples:278
destroyObj : ObjectId → ObjInstruction Safe Bool -- May fail if object doesn't exist in AVM.Instruction:195
destroyObjInTx : ObjectId → ObjectMeta → State → AVMResult Bool in AVM.Interpreter:471

`elem`

Defined in: elem Total references: 5

Other (5)

Boolean type or the two-element type is a fundamental type in type theory. It is used to represent t... in Foundation.BasicTypes:668

`exCtrl`

Defined in: exCtrl Total references: 5

Type Signatures (5)

exCtrl : ControllerId in AVM.SmallExample:94

`executeMachine`

Defined in: executeMachine Total references: 5

Type Signatures (5)

executeMachine : ∀ {s A} → MachineInstruction s A → State → AVMResult A in AVM.Interpreter:648

`executePure`

Defined in: executePure Total references: 5

Type Signatures (5)

executePure : ∀ {s A} → PureInstruction s A → State → AVMResult A in AVM.Interpreter:624

`FinSet`

Defined in: FinSet Total references: 5

Type Signatures (2)

FinSet : Set → Set in Foundation.BasicTypes:518

Other (3)

using (Pred; _⊆_; _↔_; ⊥; ¬; Σ; ℕ; _≤_; List; \[\]; _∷_; _≡_; refl; _×_; suc; zero; ∃; ∃-syntax; FinSe... in Foundation.Hyperproperties:16

`freshObjectId`

Defined in: freshObjectId Total references: 5

Type Signatures (5)

freshObjectId : ℕ → ObjectId in AVM.SmallExample:35

`freshTxId`

Defined in: freshTxId Total references: 5

Type Signatures (5)

freshTxId : ℕ → TxId in AVM.SmallExample:38

`GenericInterpreter`

Defined in: GenericInterpreter Total references: 5

Other (5)

module GenericInterpreter in AVM.Interpreter:809

`go`

Defined in: go Total references: 5

Other (5)

lookupPendingCreate oid st = go (State.creates st) in AVM.Interpreter:105

`handleCall`

Defined in: handleCall Total references: 5

Type Signatures (5)

handleCall : ObjectId → Input → State → Object → ObjectMeta → AVMResult (Maybe Val) in AVM.Interpreter:374

`Handler`

Defined in: Handler Total references: 5

Type Signatures (5)

Handler : EventSig → EventSig → Set₁ in Foundation.InteractionTrees:240

`head`

Defined in: head Total references: 5

Type Signatures (3)

head-empty : {A : Set} → A in Foundation.BasicTypes:496

Other (2)

let output = (if null outputs then nothing else just (head outputs)) in AVM.Interpreter:379

`IDParams`

Defined in: IDParams Total references: 5

Type Signatures (5)

data IDParams : Set where in RM.Types.Identities:79
generateIdentity : Backend → IDParams → Capabilities in RM.Types.Program:61

`inCreates`

Defined in: inCreates Total references: 5

Type Signatures (5)

inCreates : ObjectId → List (ObjectId × Object × ObjectMeta) → Bool in AVM.Interpreter:251

`interp-step`

Defined in: interp-step Total references: 5

Other (5)

observe (interp h t) = interp-step h (observe t) in Foundation.InteractionTrees:261

`map`

Defined in: map Total references: 5

Type Signatures (4)

map-maybe : {A B : Set} → (A → B) → Maybe A → Maybe B in Foundation.BasicTypes:468

Other (1)

{ signingKey = foldr _++ˢ_ "" (map (λ w → w .rcv) witnesses) } in RM.Types.Delta:37

`MessageEvent`

Defined in: MessageEvent Total references: 5

Type Signatures (5)

data MessageEvent : EventSig where in Foundation.InteractionTrees:42

`mkMeta`

Defined in: mkMeta Total references: 5

Other (5)

initMeta oid mid cid ver = mkMeta oid \[\] mid cid cid ver ver in AVM.Interpreter:151
constructor mkMeta in AVM.Runtime:70
meta0 = mkMeta exOid \[\] exMachine exCtrl exCtrl 0 0 in AVM.SmallExample:98

`msg-to-event`

Defined in: msg-to-event Total references: 5

Type Signatures (5)

msg-to-event : KVMsg → Maybe KVEvent in AVM.Examples:405

`Nonce`

Defined in: Nonce Total references: 5

Other (5)

This module defines the Nonce type for ensuring uniqueness of resource commitments. in RM.Types.Nonce:15
open import RM.Types.Nonce in RM.Types.Nullifier:23
open import RM.Types.Nonce in RM.Types.Resource:42

`null`

Defined in: null Total references: 5

Type Signatures (3)

null : {A : Set} → List A → Bool in Foundation.BasicTypes:484

Other (2)

let output = (if null outputs then nothing else just (head outputs)) in AVM.Interpreter:379

`NullifierKeyMatchesCommitment`

Defined in: NullifierKeyMatchesCommitment Total references: 5

Type Signatures (5)

data NullifierKeyMatchesCommitment : NullifierKey → NullifierKeyCommitment → Set where in RM.Types.NullifierKey:35
proof : NullifierKeyMatchesCommitment key (res .nullifierKeyCommitment) in RM.Types.Resource:67

`ObjectBehaviour`

Defined in: ObjectBehaviour Total references: 5

Type Signatures (5)

ObjectBehaviour : Set → Set in AVM.Objects:744

`Obs`

Defined in: Obs Total references: 5

Other (5)

## Prefixes and Observations in Foundation.Hyperproperties:159

`ofSecret`

Defined in: ofSecret Total references: 5

Other (5)

ofSecret : ℕ → NullifierKeyCommitment in RM.Types.NullifierKey:27

`process-input`

Defined in: process-input Total references: 5

Other (5)

process-input in AVM.Objects:279

`processTransfers`

Defined in: processTransfers Total references: 5

Other (5)

processTransfers transfers in AVM.Examples:245

`PureLayerError`

Defined in: PureLayerError Total references: 5

Type Signatures (5)

data PureLayerError : Set where in AVM.Runtime:324

`remove`

Defined in: remove Total references: 5

Type Signatures (5)

removePendingCreate : ObjectId → State → State in AVM.Interpreter:200

`replay-kv`

Defined in: replay-kv Total references: 5

Type Signatures (5)

replay-kv : List KVEvent → KVStore in AVM.Examples:396

`StorageKey`

Defined in: StorageKey Total references: 5

Type Signatures (5)

StorageKey : Set in RM.Types.Program:18

`Stream`

Defined in: Stream Total references: 5

Other (5)

record Stream {ℓ : Level} (A : Set ℓ) : Set ℓ where in Foundation.Hyperproperties:36

`trans`

Defined in: trans Total references: 5

Type Signatures (3)

trans : {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z in Foundation.BasicTypes:206

Other (2)

transaction processing units. Objects may be deterministic or nondeterministic in AVM.Objects:222

`TxLayerError`

Defined in: TxLayerError Total references: 5

Type Signatures (5)

data TxLayerError : Set where in AVM.Runtime:314

`Unsafe`

Defined in: Unsafe Total references: 5

Other (5)

Two safety levels are defined: Safe and Unsafe. Instructions below are in AVM.Instruction:179

`vis`

Defined in: vis Total references: 5

Type Signatures (5)

vis : {A : Set} in Foundation.InteractionTrees:160

`WellFormedObjectType`

Defined in: WellFormedObjectType Total references: 5

Other (5)

record WellFormedObjectType (φ : Object) : Set where in AVM.Objects:159

`++-right-id`

Defined in: Agda@++-right-id Total references: 4

Type Signatures (4)

++-right-id : ∀ {A} (xs : List A) → (xs ++ \[\]) ≡ xs in Foundation.BasicTypes:460

`_∈Pred_`

Defined in: _∈Pred_ Total references: 4

Type Signatures (3)

_∈Pred_ : {ℓ : Level} {A : Set ℓ} → A → Pred A → Set ℓ in Foundation.BasicTypes:567

Other (1)

renaming (_∈Pred_ to _∈ₚ_) in Foundation.Hyperproperties:17

`_∘_`

Defined in: _∘_ Total references: 4

Type Signatures (2)

_∘_ : {A B C : Set} → (B → C) → (A → B) → A → C in Foundation.BasicTypes:609

Other (2)

f <$> t = t >>= (ret ∘ f) in Foundation.InteractionTrees:201
isRemoteEngineID = not ∘ isLocalEngineID in RM.Types.Identities:73

`_≢_`

Defined in: _≢_ Total references: 4

Type Signatures (3)

_≢_ : {A : Set} → A → A → Set in Foundation.BasicTypes:221

Other (1)

is-defined φ xs = Object.behavior φ xs ≢ nothing in AVM.Objects:138

`Action`

Defined in: Action Total references: 4

Other (4)

Action structures for the Anoma Resource Machine. in RM.Types.Action:57
open import RM.Types.Action in RM.Types.Transaction:19

`addPendingTransfer`

Defined in: addPendingTransfer Total references: 4

Type Signatures (4)

addPendingTransfer : ObjectId → ControllerId → State → State in AVM.Interpreter:220

`all`

Defined in: all Total references: 4

Type Signatures (4)

Decidability type for propositions that can be algorithmically decided: in Foundation.BasicTypes:700

`apply-kv-event`

Defined in: apply-kv-event Total references: 4

Type Signatures (4)

apply-kv-event : KVStore → KVEvent → KVStore in AVM.Examples:392

`AVMProgram`

Defined in: AVMProgram Total references: 4

Other (4)

Programs have the type AVMProgram, whose semantics we define using in AVM.Instruction:471
active transaction. It uses theinterpretAVMProgramrunner from the in AVM.SmallExample:131

`ComplianceUnit`

Defined in: ComplianceUnit Total references: 4

Other (4)

complianceUnits : List ComplianceUnit in RM.Types.Action:59
record ComplianceUnit : Set where in RM.Types.Compliance:56

`ComplianceWitness`

Defined in: ComplianceWitness Total references: 4

Other (4)

record ComplianceWitness : Set where in RM.Types.Compliance:24
fromComplianceWitnesses : List ComplianceWitness → DeltaWitness in RM.Types.Delta:35

`concat`

Defined in: concat Total references: 4

Type Signatures (4)

List concatenation is associative: in Foundation.BasicTypes:676

`concatMap`

Defined in: concatMap Total references: 4

Type Signatures (4)

concatMap : {A B : Set} → (A → List B) → List A → List B in Foundation.BasicTypes:692

`ConstraintInstruction`

Defined in: ConstraintInstruction Total references: 4

Other (4)

### ConstraintInstruction datatype in AVM.Instruction:828

`createObj`

Defined in: createObj Total references: 4

Other (4)

trigger (Obj(createObj (VList (VString "counter" ∷ initialValue ∷ \[\])))) >>= λ counterId → in AVM.Examples:176
createObj would break parametricity by exposing implementation details in AVM.Instruction:194
executeObj (createObj val) st with State.tx st in AVM.Interpreter:451

`createWithMeta`

Defined in: createWithMeta Total references: 4

Type Signatures (4)

createWithMeta : Object → ObjectMeta → State → State in AVM.Interpreter:132

`DeltaProof`

Defined in: DeltaProof Total references: 4

Type Signatures (4)

DeltaProof : Set in RM.Types.Delta:16
deltaProof : DeltaProof in RM.Types.Transaction:20

`deposit`

Defined in: deposit Total references: 4

Type Signatures (4)

deposit : ℕ → Message in AVM.Examples:104

`destroyObjNoTx`

Defined in: destroyObjNoTx Total references: 4

Type Signatures (4)

destroyObjNoTx : ObjectId → ObjectMeta → State → AVMResult Bool in AVM.Interpreter:436

`EngineName`

Defined in: EngineName Total references: 4

Type Signatures (4)

EngineName : Set in RM.Types.Identities:55

`err-metadata-corruption`

Defined in: err-metadata-corruption Total references: 4

Other (4)

... | just _ | nothing | just _ | nothing = failure (err-metadata-corruption oid) in AVM.Interpreter:477
pattern err-metadata-corruption oid = in AVM.Runtime:362

`executeInstr₀`

Defined in: executeInstr₀ Total references: 4

Type Signatures (4)

executeInstr₀ : ∀ {s A} → Instr₀ s A → State → AVMResult A in AVM.Interpreter:753

`exMachine`

Defined in: exMachine Total references: 4

Type Signatures (4)

exMachine : MachineId in AVM.SmallExample:91

`ExternalId`

Defined in: ExternalId Total references: 4

Type Signatures (4)

ExternalId : Set in RM.Types.Identities:32

`getController`

Defined in: getController Total references: 4

Other (4)

getController : ObjectId → ControllerInstruction Safe (Maybe ControllerId) in AVM.Instruction:393
executeController (getController oid) st with lookupPendingCreate oid st in AVM.Interpreter:699
-- Program 1: Stage a transfer inside a transaction and observe getController in AVM.SmallExample:136

`handleBalance`

Defined in: handleBalance Total references: 4

Other (4)

handleBalance mBalance in AVM.Examples:269

`handleDeposit`

Defined in: handleDeposit Total references: 4

Type Signatures (4)

handleDeposit : TxId → Maybe Val → AVMProgram₁ Val in AVM.Examples:148

`handleResult`

Defined in: handleResult Total references: 4

Other (4)

handleResult mv₃ in AVM.Examples:187

`handleUpdateResult`

Defined in: handleUpdateResult Total references: 4

Type Signatures (4)

handleUpdateResult : Maybe Val → AVMProgram₁ Val in AVM.Examples:211

`handleWithdraw`

Defined in: handleWithdraw Total references: 4

Other (4)

handleWithdraw txId mr₁ in AVM.Examples:133

`hasDuplicates`

Defined in: hasDuplicates Total references: 4

Type Signatures (4)

hasDuplicates : {A : Set} → List A → Bool in Foundation.BasicTypes:684

`inDestroys`

Defined in: inDestroys Total references: 4

Type Signatures (4)

inDestroys : ObjectId → List ObjectId → Bool in AVM.Interpreter:261

`initMeta`

Defined in: initMeta Total references: 4

Type Signatures (4)

initMeta : ObjectId → MachineId → ControllerId → ControllerVersion → ObjectMeta in AVM.Interpreter:150

`initState`

Defined in: initState Total references: 4

Type Signatures (4)

initState : State in AVM.SmallExample:108

`interp`

Defined in: interp Total references: 4

Type Signatures (4)

interp : {E F : EventSig} {R : Set} → in Foundation.InteractionTrees:256

`isConsumed`

Defined in: isConsumed Total references: 4

Type Signatures (4)

isConsumed : ConsumedCreated → Bool in RM.Types.ConsumedCreated:29
isConsumedArgs : LogicArgs → Bool in RM.Types.Logic:35

`isLocalEngineID`

Defined in: isLocalEngineID Total references: 4

Type Signatures (4)

isLocalEngineID : EngineId → Bool in RM.Types.Identities:68

`just-injective`

Defined in: just-injective Total references: 4

Type Signatures (2)

just-injective : ∀ {A} {x y : A} → just x ≡ just y → x ≡ y in Foundation.BasicTypes:288

Other (2)

≡⟨ sym (just-injective eq1) ⟩ in AVM.Objects:470

`just≢nothing`

Defined in: just≢nothing Total references: 4

Type Signatures (2)

just≢nothing : ∀ {A} {x : A} → just x ≡ nothing → ⊥ in Foundation.BasicTypes:283

Other (2)

... | just _ | _ = just≢nothing eq-xs in AVM.Objects:485

`kSafety`

Defined in: kSafety Total references: 4

Type Signatures (4)

kSafety : {ℓ : Level} {Σᵀ : Set ℓ} → (k : ℕ) → HyperProp Σᵀ → Set (lsuc (lsuc ℓ)) in Foundation.Hyperproperties:196

`LogicArgs`

Defined in: LogicArgs Total references: 4

Other (4)

record LogicArgs : Set where in RM.Types.Logic:17

`LogicRef`

Defined in: LogicRef Total references: 4

Other (4)

reference : LogicRef in RM.Types.Logic:43
record LogicRef : Set where in RM.Types.Resource:21

`NondetInstruction`

Defined in: NondetInstruction Total references: 4

Other (4)

### NondetInstruction datatype in AVM.Instruction:798

`Nullifier`

Defined in: Nullifier Total references: 4

Other (4)

A public value derived from a secret NullifierKey and a resource. in RM.Types.Nullifier:16
open import RM.Types.Nullifier in RM.Types.Resource:77

`ObjectDestroyed`

Defined in: ObjectDestroyed Total references: 4

Other (4)

entry = makeLogEntry (ObjectDestroyed oid) st in AVM.Interpreter:433
ObjectDestroyed : ObjectId → EventType in AVM.Runtime:443

`ObjectId`

Defined in: ObjectId Total references: 4

Type Signatures (4)

ObjectId : Set in RM.Types.Identities:16
queryByObjectId : ObjectId → ResourceQuery in RM.Types.Program:32

`ObjectTransferred`

Defined in: ObjectTransferred Total references: 4

Other (4)

entry = makeLogEntry (ObjectTransferred oid (State.controllerId st) targetCid) st in AVM.Interpreter:415
ObjectTransferred : ObjectId → ControllerId → ControllerId → EventType in AVM.Runtime:453

`PureError`

Defined in: PureError Total references: 4

Type Signatures (4)

data PureError : Set where in AVM.Runtime:289

`PureFunctions`

Defined in: PureFunctions Total references: 4

Type Signatures (4)

PureFunctions : Set in AVM.Runtime:148
emptyFuns : PureFunctions in AVM.SmallExample:105

`run-object-itree`

Defined in: run-object-itree Total references: 4

Other (4)

run-object-itree in AVM.Objects:781

`simpleObj`

Defined in: simpleObj Total references: 4

Type Signatures (4)

simpleObj : Object in AVM.SmallExample:52

`Tag`

Defined in: Tag Total references: 4

Other (4)

## Tag in RM.Types.Action:18

`targetCtrl`

Defined in: targetCtrl Total references: 4

Type Signatures (4)

targetCtrl : ControllerId in AVM.SmallExample:128

`tau`

Defined in: tau Total references: 4

Other (4)

occurrence ofITree₁ E Rwithin the tau constructor's type argument. in Foundation.InteractionTrees:153

`teleport`

Defined in: teleport Total references: 4

Other (4)

teleport : MachineId → MachineInstruction Safe Bool in AVM.Instruction:372
**Safety constraint**: teleportation is invalid during active transactions. in AVM.Interpreter:660
transaction (overlay) and how the interpreter forbidsteleportduring an in AVM.SmallExample:146

`Trace`

Defined in: Trace Total references: 4

Type Signatures (1)

interpretAux : ∀ {A} → ITree (Instr Safe) A → State → Trace → AVMResult A in AVM.Interpreter:815

Other (3)

### Trace in AVM.Runtime:479

`TraceFin`

Defined in: TraceFin Total references: 4

Type Signatures (4)

TraceFin : {ℓ : Level} → Set ℓ → Set ℓ in Foundation.Hyperproperties:53

`transferObject`

Defined in: transferObject Total references: 4

Other (4)

transferObject : ObjectId → ControllerId → ControllerInstruction Safe Bool in AVM.Instruction:396
executeController (transferObject oid targetCid) st in AVM.Interpreter:712
This small example demonstrates howtransferObjectis staged inside a in AVM.SmallExample:134

`VBool`

Defined in: VBool Total references: 4

Other (4)

VBool : Bool → Val in AVM.Examples:28

`VNil`

Defined in: VNil Total references: 4

Other (4)

VNil : Val in AVM.Examples:31

`VPair`

Defined in: VPair Total references: 4

Other (4)

VPair : Val → Val → Val in AVM.Examples:30

`withdraw`

Defined in: withdraw Total references: 4

Type Signatures (4)

withdraw : ℕ → Message in AVM.Examples:101

`·-++-assoc`

Defined in: ·-++-assoc Total references: 4

Other (4)

≡⟨ cong (Object.behavior φ₁) (·-++-assoc hist₁ inp future) ⟩ in AVM.Objects:708

`φ-account`

Defined in: φ-account Total references: 4

Type Signatures (4)

φ-account-aux : List AccountMsg → Maybe AccountMsg → Maybe AccountOutput in AVM.Examples:488

`φ-kv`

Defined in: φ-kv Total references: 4

Type Signatures (4)

φ-kv-aux : List KVMsg → Maybe KVMsg → Maybe Val in AVM.Examples:419

`_<$>_`

Defined in: _<?_$>_ Total references: 3

Type Signatures (3)

_<$>_ : (R → S) → ITree E R → ITree E S in Foundation.InteractionTrees:200

`_>>=ᴹ_`

Defined in: _>>=ᴹ_ Total references: 3

Type Signatures (3)

_>>=ᴹ_ : {A B : Set} → Maybe A → (A → Maybe B) → Maybe B in Foundation.BasicTypes:295

`_≡⟨⟩_`

Defined in: _≡⟨⟩_ Total references: 3

Other (3)

infixr 2 _≡⟨⟩_ _≡⟨_⟩_ in Foundation.BasicTypes:241

`_≤v_`

Defined in: _≤v_ Total references: 3

Type Signatures (3)

_≤v_ : ControllerVersion → ControllerVersion → Bool in AVM.SmallExample:60

`addPendingCreate`

Defined in: addPendingCreate Total references: 3

Type Signatures (3)

addPendingCreate : ObjectId → Object → ObjectMeta → State → State in AVM.Interpreter:190

`addPendingDestroy`

Defined in: addPendingDestroy Total references: 3

Type Signatures (3)

addPendingDestroy : ObjectId → State → State in AVM.Interpreter:212

`addPendingWrite`

Defined in: addPendingWrite Total references: 3

Type Signatures (3)

addPendingWrite : ObjectId → Input → State → State in AVM.Interpreter:180

`allObjectIds`

Defined in: allObjectIds Total references: 3

Type Signatures (3)

allObjectIds : State → List ObjectId in AVM.SmallExample:66

`applyDestroy`

Defined in: applyDestroy Total references: 3

Type Signatures (3)

applyDestroy : ObjectId → State → State in AVM.Interpreter:332

`applyTransfer`

Defined in: applyTransfer Total references: 3

Type Signatures (3)

applyTransfer : (ObjectId × ControllerId) → State → State in AVM.Interpreter:355

`applyWrite`

Defined in: applyWrite Total references: 3

Type Signatures (3)

applyWrite : ObjectId → Input → State → State in AVM.Interpreter:306

`balanceMsg`

Defined in: balanceMsg Total references: 3

Other (3)

balanceMsg : AccountMsg in AVM.Examples:445

`callObjInTx`

Defined in: callObjInTx Total references: 3

Type Signatures (3)

callObjInTx : ObjectId → Input → State → Object → ObjectMeta → AVMResult (Maybe Output) in AVM.Interpreter:404

`callPure`

Defined in: callPure Total references: 3

Other (3)

callPure : String → List Val → PureInstruction Safe (Maybe Val) in AVM.Instruction:323
executePure (callPure name args) st in AVM.Interpreter:625

`CanNullifyResource`

Defined in: CanNullifyResource Total references: 3

Other (3)

record CanNullifyResource (key : NullifierKey) (res : Resource) : Set where in RM.Types.Resource:65

`Ciphertext`

Defined in: Ciphertext Total references: 3

Type Signatures (3)

Ciphertext : Set in RM.Types.Identities:19
decrypt : EngineId → Ciphertext → (Plaintext → Program) → Program in RM.Types.Program:59

`collectMatches`

Defined in: collectMatches Total references: 3

Other (3)

let results = foldr collectMatches \[\] (allObjectIds st) in AVM.Interpreter:537

`commitment`

Defined in: commitment Total references: 3

Other (3)

Computes the commitment of a NullifierKey. in RM.Types.NullifierKey:58

`commitWithResult`

Defined in: commitWithResult Total references: 3

Type Signatures (3)

commitWithResult : TxId → AVMProgram₁ Val in AVM.Examples:140

`ComplianceInstance`

Defined in: ComplianceInstance Total references: 3

Other (3)

record ComplianceInstance : Set where in RM.Types.Compliance:41

`ComplianceProof`

Defined in: ComplianceProof Total references: 3

Type Signatures (3)

ComplianceProof : Set in RM.Types.Compliance:49

`ConstraintId`

Defined in: ConstraintId Total references: 3

Other (3)

### ConstraintId datatype in AVM.Instruction:810

`Consumed`

Defined in: Consumed Total references: 3

Other (3)

This module defines the ConsumedCreated type representing whether a resource is consumed or created.... in RM.Types.ConsumedCreated:17

`counter-always-defined`

Defined in: counter-always-defined Total references: 3

Type Signatures (3)

counter-always-defined : ∀ xs → ∃\[ o ∈ List Output \] (Object.behavior counter-type xs ≡ just o) in AVM.Objects:477

`counter-wf`

Defined in: counter-wf Total references: 3

Type Signatures (3)

counter-wf : WellFormedObjectType counter-type in AVM.Objects:460

`create-object`

Defined in: create-object Total references: 3

Other (3)

create-object in AVM.Objects:619

`createCounter`

Defined in: createCounter Total references: 3

Type Signatures (3)

createCounter : Val → AVMProgram₁ ObjectId in AVM.Examples:174

`Created`

Defined in: Created Total references: 3

Other (3)

This module defines the ConsumedCreated type representing whether a resource is consumed or created.... in RM.Types.ConsumedCreated:16

`defaultNonce`

Defined in: defaultNonce Total references: 3

Type Signatures (2)

defaultNonce : Nonce in RM.Types.Nonce:27

Other (1)

toNonce privateMk = defaultNonce in RM.Types.Nullifier:24

`del`

Defined in: del Total references: 3

Other (3)

Now we instantiate the object model and instruction set with our concrete types. in AVM.Examples:362

`del-event`

Defined in: del-event Total references: 3

Other (3)

del-event : Key → KVEvent in AVM.Examples:371

`DeletionCriterion`

Defined in: DeletionCriterion Total references: 3

Type Signatures (3)

data DeletionCriterion : Set where in RM.Types.Action:33

`depositMsg`

Defined in: depositMsg Total references: 3

Other (3)

depositMsg : ℕ → AccountMsg in AVM.Examples:443

`destroyObjInTx`

Defined in: destroyObjInTx Total references: 3

Type Signatures (3)

destroyObjInTx : ObjectId → ObjectMeta → State → AVMResult Bool in AVM.Interpreter:427

`emptyFuns`

Defined in: emptyFuns Total references: 3

Type Signatures (3)

emptyFuns : PureFunctions in AVM.SmallExample:105

`eqNat`

Defined in: eqNat Total references: 3

Type Signatures (3)

eqNat : ∀ {A : Set} → A → A → Bool in AVM.SmallExample:57

`equiv-after-input`

Defined in: equiv-after-input Total references: 3

Other (3)

,Σ (refl , refl , equiv-after-input)) in AVM.Objects:699

`err-controller-unreachable`

Defined in: err-controller-unreachable Total references: 3

Other (3)

... | just _ | false | _ | _ = failure (err-controller-unreachable targetCid) in AVM.Interpreter:714
pattern err-controller-unreachable cid = in AVM.Runtime:409

`err-invalid-during-tx`

Defined in: err-invalid-during-tx Total references: 3

Other (3)

... | just _ = failure (err-invalid-during-tx "teleport") in AVM.Interpreter:661
pattern err-invalid-during-tx msg = in AVM.Runtime:391

`err-machine-unreachable`

Defined in: err-machine-unreachable Total references: 3

Other (3)

else failure (err-machine-unreachable mid) in AVM.Interpreter:667
pattern err-machine-unreachable mid = in AVM.Runtime:422

`err-tx-conflict`

Defined in: err-tx-conflict Total references: 3

Other (3)

... | false = failure (err-tx-conflict txid) in AVM.Interpreter:581
pattern err-tx-conflict tid = in AVM.Runtime:376

`executeInstruction`

Defined in: executeInstruction Total references: 3

Type Signatures (3)

executeInstruction : ∀ {s A} → Instruction s A → State → AVMResult A in AVM.Interpreter:790

`executeInstr₁`

Defined in: executeInstr₁ Total references: 3

Type Signatures (3)

executeInstr₁ : ∀ {s A} → Instr₁ s A → State → AVMResult A in AVM.Interpreter:763

`executeInstr₂`

Defined in: executeInstr₂ Total references: 3

Type Signatures (3)

executeInstr₂ : ∀ {s A} → Instr₂ s A → State → AVMResult A in AVM.Interpreter:776

`ExternalIdentity`

Defined in: ExternalIdentity Total references: 3

Type Signatures (3)

ExternalIdentity : Set in RM.Types.Identities:58

`get`

Defined in: get Total references: 3

Other (3)

trigger (Obj(call ctr (VString "get"))) >>= λ mv₃ → in AVM.Examples:363

`getCurrentController`

Defined in: getCurrentController Total references: 3

Other (3)

getCurrentController : ControllerInstruction Safe ControllerId in AVM.Instruction:392
executeController getCurrentController st = in AVM.Interpreter:692

`getCurrentMachine`

Defined in: getCurrentMachine Total references: 3

Other (3)

getCurrentMachine : IntrospectInstruction Safe MachineId in AVM.Instruction:221
The getCurrentMachine instruction returns the physical machine identifier from the execution context... in AVM.Interpreter:517

`getCurrentVersion`

Defined in: getCurrentVersion Total references: 3

Other (3)

getCurrentVersion : ControllerInstruction Safe ControllerVersion in AVM.Instruction:399
executeController getCurrentVersion st = in AVM.Interpreter:729

`getFreshIdCounter`

Defined in: getFreshIdCounter Total references: 3

Type Signatures (3)

getFreshIdCounter : State → ℕ in AVM.SmallExample:63

`getMachine`

Defined in: getMachine Total references: 3

Other (3)

getMachine : ObjectId → MachineInstruction Safe (Maybe MachineId) in AVM.Instruction:369
executeMachine (getMachine oid) st with lookupPendingCreate oid st in AVM.Interpreter:649

`Hypersafety`

Defined in: Hypersafety Total references: 3

Other (3)

## Hypersafety and Hyperliveness in Foundation.Hyperproperties:182

`initStore`

Defined in: initStore Total references: 3

Type Signatures (3)

initStore : Store in AVM.SmallExample:100

`input`

Defined in: input Total references: 3

Other (3)

mapping input sequences to output sequences (see the \[Objects\](./Objects.lagda.md) in AVM.Instruction:220
Pending inputs accumulate all inputs directed to an object within the current transaction. in AVM.Interpreter:511

`InternalId`

Defined in: InternalId Total references: 3

Type Signatures (3)

InternalId : Set in RM.Types.Identities:35

`interpretValue`

Defined in: interpretValue Total references: 3

Type Signatures (3)

interpretValue : Val → Object in AVM.SmallExample:69

`IntrospectError`

Defined in: IntrospectError Total references: 3

Type Signatures (3)

data IntrospectError : Set where in AVM.Runtime:247

`invalidTeleportProg`

Defined in: invalidTeleportProg Total references: 3

Type Signatures (3)

invalidTeleportProg : AVMProgram Bool in AVM.SmallExample:143

`isCreated`

Defined in: isCreated Total references: 3

Type Signatures (3)

isCreated : ConsumedCreated → Bool in RM.Types.ConsumedCreated:23

`isEphemeral`

Defined in: isEphemeral Total references: 3

Type Signatures (3)

isEphemeral : Resource → Bool in RM.Types.Resource:53

`isReachableController`

Defined in: isReachableController Total references: 3

Type Signatures (3)

isReachableController : ControllerId → Bool in AVM.SmallExample:72

`isReachableMachine`

Defined in: isReachableMachine Total references: 3

Type Signatures (3)

isReachableMachine : MachineId → Bool in AVM.SmallExample:75

`kudosTransfer`

Defined in: kudosTransfer Total references: 3

Type Signatures (3)

kudosTransfer : ObjectId → ObjectId → ℕ → AVMProgram₁ Val in AVM.Examples:129

`LinearConstraint`

Defined in: LinearConstraint Total references: 3

Other (3)

### LinearConstraint datatype in AVM.Instruction:821

`LogEntry`

Defined in: LogEntry Total references: 3

Other (3)

makeLogEntry : EventType → State → LogEntry in AVM.Interpreter:157
### LogEntry in AVM.Runtime:468

`LogicVerifierInput`

Defined in: LogicVerifierInput Total references: 3

Other (3)

record LogicVerifierInput : Set where in RM.Types.Action:41

`LogicVKOuterHash`

Defined in: LogicVKOuterHash Total references: 3

Type Signatures (3)

LogicVKOuterHash : Set in RM.Types.Action:26

`lookupPendingTransfer`

Defined in: lookupPendingTransfer Total references: 3

Type Signatures (3)

lookupPendingTransfer : ObjectId → State → Maybe ControllerId in AVM.Interpreter:104

`map-maybe`

Defined in: map-maybe Total references: 3

Type Signatures (3)

map-maybe : {A B : Set} → (A → B) → Maybe A → Maybe B in Foundation.BasicTypes:303

`MerklePath`

Defined in: MerklePath Total references: 3

Type Signatures (3)

MerklePath : Set in RM.Types.Compliance:17

`meta0`

Defined in: meta0 Total references: 3

Type Signatures (3)

meta0 : ObjectMeta in AVM.SmallExample:97

`MetaStore`

Defined in: MetaStore Total references: 3

Other (3)

### MetaStore in AVM.Runtime:103

`moveObject`

Defined in: moveObject Total references: 3

Other (3)

moveObject : ObjectId → MachineId → MachineInstruction Safe Bool in AVM.Instruction:375
executeMachine (moveObject oid targetMid) st with lookupObjectWithMeta oid st in AVM.Interpreter:673

`NodeId`

Defined in: NodeId Total references: 3

Type Signatures (3)

NodeId : Set in RM.Types.Identities:52

`ObjectCalled`

Defined in: ObjectCalled Total references: 3

Other (3)

entry = makeLogEntry (ObjectCalled oid inp output) st in AVM.Interpreter:380
ObjectCalled : ObjectId → Input → Maybe Output → EventType in AVM.Runtime:446

`ObjectCreated`

Defined in: ObjectCreated Total references: 3

Other (3)

let entry = makeLogEntry (ObjectCreated oid val) st in in AVM.Interpreter:456
ObjectCreated : ObjectId → Val → EventType in AVM.Runtime:442

`ObjectStore`

Defined in: ObjectStore Total references: 3

Other (3)

### ObjectStore in AVM.Runtime:96

`ok`

Defined in: ok Total references: 3

Other (3)

ok? : Val → Bool in AVM.Examples:475

`pendingInputsFor`

Defined in: pendingInputsFor Total references: 3

Type Signatures (3)

pendingInputsFor : ObjectId → State → List Input in AVM.Interpreter:166

`Plaintext`

Defined in: Plaintext Total references: 3

Type Signatures (3)

Plaintext : Set in RM.Types.Identities:22
decrypt : EngineId → Ciphertext → (Plaintext → Program) → Program in RM.Types.Program:59

`prefix-def`

Defined in: prefix-def Total references: 3

Other (3)

prefix-def in AVM.Objects:463

`PrivateKey`

Defined in: PrivateKey Total references: 3

Type Signatures (2)

data PrivateKey : Set where in RM.Types.Crypto:20

Other (1)

InternalId = PrivateKey in RM.Types.Identities:36

`privateMk`

Defined in: privateMk Total references: 3

Other (3)

privateMk : Nullifier in RM.Types.Nullifier:17
nullifier _ = privateMk in RM.Types.Resource:78

`PublicKey`

Defined in: PublicKey Total references: 3

Type Signatures (2)

data PublicKey : Set where in RM.Types.Crypto:15

Other (1)

ExternalId = PublicKey in RM.Types.Identities:33

`pure-error`

Defined in: pure-error Total references: 3

Other (3)

pure-error : PureError → PureLayerError in AVM.Runtime:326

`put`

Defined in: put Total references: 3

Other (3)

using (Object; Input; Output; InputSequence; mkObjType) in AVM.Examples:361

`put-event`

Defined in: put-event Total references: 3

Other (3)

put-event : Key → Val → KVEvent in AVM.Examples:370

`reflect`

Defined in: reflect Total references: 3

Other (3)

- Introspection layer: Context queries and reflection in AVM.Instruction:224
executeIntrospect (reflect oid) st = in AVM.Interpreter:551

`registerPure`

Defined in: registerPure Total references: 3

Other (3)

registerPure : String → (List Val → Maybe Val) → PureInstruction Unsafe Bool in AVM.Instruction:326
executePure (registerPure name f) st = in AVM.Interpreter:634

`removePendingCreate`

Defined in: removePendingCreate Total references: 3

Type Signatures (3)

removePendingCreate : ObjectId → State → State in AVM.Interpreter:198

`ResourceQuery`

Defined in: ResourceQuery Total references: 3

Type Signatures (3)

data ResourceQuery : Set where in RM.Types.Program:31

`scryDeep`

Defined in: scryDeep Total references: 3

Other (3)

scryDeep in AVM.Instruction:231
executeIntrospect (scryDeep pred) st = in AVM.Interpreter:536

`scryMeta`

Defined in: scryMeta Total references: 3

Other (3)

scryMeta in AVM.Instruction:227
executeIntrospect (scryMeta pred) st = in AVM.Interpreter:523

`secret`

Defined in: secret Total references: 3

Other (3)

A secret value used to assign ownership to a resource. in RM.Types.NullifierKey:37

`self`

Defined in: self Total references: 3

Other (3)

self : IntrospectInstruction Safe ObjectId in AVM.Instruction:219
The self instruction returns the current object identifier from the execution context. in AVM.Interpreter:505

`Signable`

Defined in: Signable Total references: 3

Type Signatures (3)

Signable : Set in RM.Types.Identities:25
requestCommitment : EngineId → Signable → (Commitment → Program) → Program in RM.Types.Program:60

`Signature`

Defined in: Signature Total references: 3

Other (3)

## Cryptographic Signature in RM.Types.Crypto:27
Commitment = Signature in RM.Types.Identities:46

`size`

Defined in: size Total references: 3

Type Signatures (3)

size : {A : Set} → FinSet A → ℕ in Foundation.Hyperproperties:25

`stagedTransferProg`

Defined in: stagedTransferProg Total references: 3

Type Signatures (3)

stagedTransferProg : AVMProgram (Maybe ControllerId) in AVM.SmallExample:131

`Store`

Defined in: Store Total references: 3

Other (3)

## Store: Persistent Object Database in AVM.Runtime:110
initStore : Store in AVM.SmallExample:100

`Success`

Defined in: Success Total references: 3

Other (3)

### Success Record in AVM.Runtime:497

`sucVersion`

Defined in: sucVersion Total references: 3

Type Signatures (3)

sucVersion : ControllerVersion → ControllerVersion in AVM.SmallExample:78

`switchVersion`

Defined in: switchVersion Total references: 3

Other (3)

switchVersion : ControllerVersion → ControllerInstruction Safe Bool in AVM.Instruction:400
executeController (switchVersion ver) st with State.tx st in AVM.Interpreter:736

`SysAsProp`

Defined in: SysAsProp Total references: 3

Type Signatures (3)

SysAsProp : {ℓ : Level} {Σᵀ : Set ℓ} → System Σᵀ → TraceProp Σᵀ in Foundation.Hyperproperties:116

`Transaction`

Defined in: Transaction Total references: 3

Other (3)

open import RM.Types.Transaction in RM.Types.Program:58
Transaction structures for the Anoma Resource Machine. in RM.Types.Transaction:17

`transferObjInTx`

Defined in: transferObjInTx Total references: 3

Type Signatures (3)

transferObjInTx : ObjectId → ControllerId → ObjectMeta → State → AVMResult Bool in AVM.Interpreter:409

`transferObjNoTx`

Defined in: transferObjNoTx Total references: 3

Type Signatures (3)

transferObjNoTx : ObjectId → ControllerId → ObjectMeta → State → AVMResult Bool in AVM.Interpreter:418

`TxWrite`

Defined in: TxWrite Total references: 3

Other (3)

### TxWrite in AVM.Runtime:137

`updateHelper`

Defined in: updateHelper Total references: 3

Other (3)

helper (VInt n) = updateHelper n in AVM.Examples:209

`validateObserved`

Defined in: validateObserved Total references: 3

Type Signatures (3)

validateObserved : State → Bool in AVM.Interpreter:271

`withdrawMsg`

Defined in: withdrawMsg Total references: 3

Other (3)

withdrawMsg : ℕ → AccountMsg in AVM.Examples:444

`α⋆`

Defined in: α⋆ Total references: 3

Type Signatures (3)

α⋆ : {ℓ : Level} {Σᵀ : Set ℓ} → TraceProp Σᵀ → TraceProp Σᵀ in Foundation.Hyperproperties:277

`φ-counter`

Defined in: φ-counter Total references: 3

Type Signatures (3)

φ-counter : List CounterMsg → Maybe ℕ in AVM.Examples:335

`≈φ-refl`

Defined in: ≈φ-refl Total references: 3

Type Signatures (3)

≈φ-refl : ∀ (φ : Object) (hist : InputSequence) → hist ≈φ\[ φ \] hist in AVM.Objects:198

`≈φ-sym`

Defined in: ≈φ-sym Total references: 3

Type Signatures (3)

≈φ-sym : ∀ {φ} {hist₁ hist₂ : InputSequence} → in AVM.Objects:207

`≈φ-trans`

Defined in: ≈φ-trans Total references: 3

Type Signatures (3)

≈φ-trans : ∀ {φ} {hist₁ hist₂ hist₃ : InputSequence} → in AVM.Objects:217

`_>>_`

Defined in: _>>_ Total references: 2

Type Signatures (2)

_>>_ : {A B : Set} → M A → M B → M B in Foundation.BasicTypes:623
_>>=ᴹ_ : {A B : Set} → Maybe A → (A → Maybe B) → Maybe B in Foundation.BasicTypes:624

`_⊨_`

Defined in: _⊨_ Total references: 2

Type Signatures (2)

_⊨_ : {ℓ : Level} {Σᵀ : Set ℓ} in Foundation.Hyperproperties:92

`_⊨α_`

Defined in: _⊨α_ Total references: 2

Type Signatures (2)

_⊨α_ : {ℓ : Level} {Σᵀ : Set ℓ} → System Σᵀ → TraceProp Σᵀ → Set (lsuc ℓ) in Foundation.Hyperproperties:284

`_⊨ᴴ_`

Defined in: _⊨ᴴ_ Total references: 2

Type Signatures (2)

_⊨ᴴ_ : {ℓ : Level} {Σᵀ : Set ℓ} → System Σᵀ → HyperProp Σᵀ → Set (lsuc (lsuc ℓ)) in Foundation.Hyperproperties:126

`AVMProgram₂`

Defined in: AVMProgram₂ Total references: 2

Type Signatures (2)

AVMProgram₂ : Set → Set in AVM.Instruction:344

`AVMProgram₄`

Defined in: AVMProgram₄ Total references: 2

Type Signatures (2)

AVMProgram₄ : Set → Set in AVM.Instruction:853

`balance-val`

Defined in: balance-val Total references: 2

Other (2)

balance-val : ℕ → AccountOutput in AVM.Examples:477

`BaseResult`

Defined in: BaseResult Total references: 2

Type Signatures (2)

BaseResult : Set → Set in AVM.Runtime:525

`behavioural-state-equiv`

Defined in: behavioural-state-equiv Total references: 2

Other (2)

behavioural-state-equiv in AVM.Objects:421

`BehaviouralState`

Defined in: BehaviouralState Total references: 2

Type Signatures (2)

BehaviouralState : Object → InputSequence → Set in AVM.Objects:231

`closeAccount`

Defined in: closeAccount Total references: 2

Type Signatures (2)

closeAccount : ObjectId → ObjectId → AVMProgram₁ Val in AVM.Examples:265

`compose`

Defined in: compose Total references: 2

Type Signatures (2)

compose : DeltaWitness → DeltaWitness → DeltaWitness in RM.Types.Delta:43

`ControllerSwitched`

Defined in: ControllerSwitched Total references: 2

Other (2)

entry = makeLogEntry (ControllerSwitched (State.controllerId st) ver) st in AVM.Interpreter:741
ControllerSwitched : ControllerId → ControllerVersion → EventType in AVM.Runtime:454

`counter-object`

Defined in: counter-object Total references: 2

Type Signatures (2)

counter-object : SequentialObject in AVM.Objects:645

`counterExample`

Defined in: counterExample Total references: 2

Type Signatures (2)

counterExample : AVMProgram₁ Val in AVM.Examples:181

`createComplianceUnit`

Defined in: createComplianceUnit Total references: 2

Type Signatures (2)

createComplianceUnit : ComplianceWitness → ComplianceUnit in RM.Types.Compliance:69

`dec`

Defined in: dec Total references: 2

Other (2)

The counter maintains a count by processing increment and decrement messages. The state (current cou... in AVM.Examples:318

`Digest`

Defined in: Digest Total references: 2

Other (2)

## Message Digest in RM.Types.Crypto:36

`echo-type`

Defined in: echo-type Total references: 2

Type Signatures (2)

echo-type : Object in AVM.Objects:494

`empty`

Defined in: empty Total references: 2

Type Signatures (2)

empty : DeltaWitness in RM.Types.Delta:50

`equiv-preserved`

Defined in: equiv-preserved Total references: 2

Other (2)

equiv-preserved in AVM.Objects:675

`err-invalid-input`

Defined in: err-invalid-input Total references: 2

Other (2)

... | nothing = failure (err-invalid-input oid inp) in AVM.Interpreter:376
pattern err-invalid-input oid inp = in AVM.Runtime:356

`err-no-active-tx`

Defined in: err-no-active-tx Total references: 2

Other (2)

... | nothing = failure err-no-active-tx in AVM.Interpreter:578
pattern err-no-active-tx = in AVM.Runtime:388

`ErrControllerUnreachable`

Defined in: ErrControllerUnreachable Total references: 2

Other (2)

ErrControllerUnreachable : ControllerId → DistribError in AVM.Runtime:274

`ErrCrossControllerTx`

Defined in: ErrCrossControllerTx Total references: 2

Other (2)

ErrCrossControllerTx : ObjectId → ControllerId → DistribError in AVM.Runtime:277

`ErrFunctionAlreadyRegistered`

Defined in: ErrFunctionAlreadyRegistered Total references: 2

Other (2)

ErrFunctionAlreadyRegistered : String → PureError in AVM.Runtime:291

`ErrFunctionNotFound`

Defined in: ErrFunctionNotFound Total references: 2

Other (2)

ErrFunctionNotFound : String → PureError in AVM.Runtime:290

`ErrInvalidDuringTx`

Defined in: ErrInvalidDuringTx Total references: 2

Other (2)

ErrInvalidDuringTx : String → TxError in AVM.Runtime:263

`ErrInvalidInput`

Defined in: ErrInvalidInput Total references: 2

Other (2)

ErrInvalidInput : ObjectId → Input → ObjError in AVM.Runtime:237

`ErrInvalidMachineTransfer`

Defined in: ErrInvalidMachineTransfer Total references: 2

Other (2)

ErrInvalidMachineTransfer : ObjectId → MachineId → DistribError in AVM.Runtime:281

`ErrMachineUnreachable`

Defined in: ErrMachineUnreachable Total references: 2

Other (2)

ErrMachineUnreachable : MachineId → DistribError in AVM.Runtime:280

`ErrMetadataCorruption`

Defined in: ErrMetadataCorruption Total references: 2

Other (2)

ErrMetadataCorruption : ObjectId → ObjError in AVM.Runtime:239

`ErrNoActiveTx`

Defined in: ErrNoActiveTx Total references: 2

Other (2)

ErrNoActiveTx : TxError in AVM.Runtime:262

`ErrObjectAlreadyDestroyed`

Defined in: ErrObjectAlreadyDestroyed Total references: 2

Other (2)

ErrObjectAlreadyDestroyed : ObjectId → ObjError in AVM.Runtime:235

`ErrObjectAlreadyExists`

Defined in: ErrObjectAlreadyExists Total references: 2

Other (2)

ErrObjectAlreadyExists : ObjectId → ObjError in AVM.Runtime:236

`ErrObjectNotFound`

Defined in: ErrObjectNotFound Total references: 2

Other (2)

ErrObjectNotFound : ObjectId → ObjError in AVM.Runtime:234

`ErrObjectRejectedCall`

Defined in: ErrObjectRejectedCall Total references: 2

Other (2)

ErrObjectRejectedCall : ObjectId → Input → ObjError in AVM.Runtime:238

`ErrStoreCorruption`

Defined in: ErrStoreCorruption Total references: 2

Other (2)

ErrStoreCorruption : String → IntrospectError in AVM.Runtime:248

`ErrTxAlreadyAborted`

Defined in: ErrTxAlreadyAborted Total references: 2

Other (2)

ErrTxAlreadyAborted : TxId → TxError in AVM.Runtime:261

`ErrTxAlreadyCommitted`

Defined in: ErrTxAlreadyCommitted Total references: 2

Other (2)

ErrTxAlreadyCommitted : TxId → TxError in AVM.Runtime:260

`ErrTxConflict`

Defined in: ErrTxConflict Total references: 2

Other (2)

ErrTxConflict : TxId → TxError in AVM.Runtime:258

`ErrTxNotFound`

Defined in: ErrTxNotFound Total references: 2

Other (2)

ErrTxNotFound : TxId → TxError in AVM.Runtime:259

`ErrUnauthorizedTransfer`

Defined in: ErrUnauthorizedTransfer Total references: 2

Other (2)

ErrUnauthorizedTransfer : ObjectId → ControllerId → DistribError in AVM.Runtime:275

`ErrVersionMismatch`

Defined in: ErrVersionMismatch Total references: 2

Other (2)

ErrVersionMismatch : ControllerVersion → ControllerVersion → DistribError in AVM.Runtime:276

`execute-step`

Defined in: execute-step Total references: 2

Other (2)

execute-step in AVM.Objects:753

`ExecutionMoved`

Defined in: ExecutionMoved Total references: 2

Other (2)

entry = makeLogEntry (ExecutionMoved mid (State.machineId st)) st in AVM.Interpreter:665
ExecutionMoved : MachineId → MachineId → EventType in AVM.Runtime:450

`fromComplianceWitnesses`

Defined in: fromComplianceWitnesses Total references: 2

Type Signatures (2)

fromComplianceWitnesses : List ComplianceWitness → DeltaWitness in RM.Types.Delta:35

`fst`

Defined in: fst Total references: 2

Type Signatures (2)

fst : {A B : Set} → A × B → A in Foundation.BasicTypes:32

`generateDeltaProof`

Defined in: generateDeltaProof Total references: 2

Type Signatures (2)

generateDeltaProof : DeltaWitness → List Action → DeltaProof in RM.Types.Transaction:30

`genObjectId`

Defined in: genObjectId Total references: 2

Type Signatures (2)

genObjectId : (ObjectId → Program) → Program in RM.Types.Program:74

`Identity`

Defined in: Identity Total references: 2

Type Signatures (2)

Identity : Set in RM.Types.Identities:38

`Impl`

Defined in: Impl Total references: 2

Type Signatures (2)

Impl : EventSig → EventSig → Set₁ in Foundation.InteractionTrees:247

`inc`

Defined in: inc Total references: 2

Other (2)

-- Define Message as alias for Val (since Instruction's Message is hidden) in AVM.Examples:317

`initial-output`

Defined in: initial-output Total references: 2

Type Signatures (2)

initial-output : Output in AVM.Objects:632

`inl`

Defined in: inl Total references: 2

Other (2)

inl : A → A + B in Foundation.BasicTypes:76

`inr`

Defined in: inr Total references: 2

Other (2)

inr : B → A + B in Foundation.BasicTypes:77

`Interface`

Defined in: Interface Total references: 2

Type Signatures (2)

Interface : Set₁ in Foundation.InteractionTrees:34

`Interpreter`

Defined in: Interpreter Total references: 2

Other (2)

# AVM Interpreter in AVM.Interpreter:54
-- Import Instruction and Interpreter with Object in AVM.SmallExample:82

`introspect-error`

Defined in: introspect-error Total references: 2

Other (2)

introspect-error : IntrospectError → BaseError in AVM.Runtime:306

`invalidTeleportResult`

Defined in: invalidTeleportResult Total references: 2

Type Signatures (2)

invalidTeleportResult : AVMResult Bool in AVM.SmallExample:148

`isConsumedArgs`

Defined in: isConsumedArgs Total references: 2

Type Signatures (2)

isConsumedArgs : LogicArgs → Bool in RM.Types.Logic:34

`isPersistent`

Defined in: isPersistent Total references: 2

Type Signatures (2)

isPersistent : Resource → Bool in RM.Types.Resource:56

`isRemoteEngineID`

Defined in: isRemoteEngineID Total references: 2

Type Signatures (2)

isRemoteEngineID : EngineId → Bool in RM.Types.Identities:72

`ITree-Monad`

Defined in: ITree-Monad Total references: 2

Type Signatures (2)

ITree-Monad : {E : EventSig} → RawMonad (ITree E) in Foundation.InteractionTrees:214

`Logic`

Defined in: Logic Total references: 2

Other (2)

module RM.Types.Logic where in RM.Types.Logic:41

`mkLogEntry`

Defined in: mkLogEntry Total references: 2

Other (2)

makeLogEntry eventType st = mkLogEntry (getFreshIdCounter st) eventType (State.controllerId st) in AVM.Interpreter:158
constructor mkLogEntry in AVM.Runtime:469

`mkStore`

Defined in: mkStore Total references: 2

Other (2)

constructor mkStore in AVM.Runtime:111
initStore = mkStore in AVM.SmallExample:101

`nullifier`

Defined in: nullifier Total references: 2

Type Signatures (2)

nullifierKeyCommitment : NullifierKeyCommitment in RM.Types.Resource:77

`ObjectMoved`

Defined in: ObjectMoved Total references: 2

Other (2)

entry = makeLogEntry (ObjectMoved oid (ObjectMeta.machine meta) targetMid) st in AVM.Interpreter:679
ObjectMoved : ObjectId → MachineId → MachineId → EventType in AVM.Runtime:449

`objecttype-to-behaviour`

Defined in: objecttype-to-behaviour Total references: 2

Type Signatures (2)

objecttype-to-behaviour : Object → ObjectBehaviour InputSequence in AVM.Objects:768

`output`

Defined in: output Total references: 2

Other (2)

-- inputs and outputs have different structures. in AVM.Objects:264

`output-of`

Defined in: output-of Total references: 2

Other (2)

output-of in AVM.Objects:144

`process-preserves-wf`

Defined in: process-preserves-wf Total references: 2

Other (2)

process-preserves-wf in AVM.Objects:658

`PureResult`

Defined in: PureResult Total references: 2

Type Signatures (2)

PureResult : Set → Set in AVM.Runtime:531

`RawMonad`

Defined in: RawMonad Total references: 2

Other (2)

record RawMonad (M : Set → Set) : Set₁ where in Foundation.BasicTypes:618
Agda supports do-notation for monads. We instantiate theRawMonadrecord (defined in BasicTypes) f... in Foundation.InteractionTrees:214

`reachable-from`

Defined in: reachable-from Total references: 2

Type Signatures (2)

reachable-from : SequentialObject → InputSequence → Set in AVM.Objects:609

`Run`

Defined in: Run Total references: 2

Other (2)

module Run = Interpreter eqNat _≤v_ getFreshIdCounter allObjectIds interpretValue isReachableControl... in AVM.SmallExample:82

`snd`

Defined in: snd Total references: 2

Type Signatures (2)

snd : {A B : Set} → A × B → B in Foundation.BasicTypes:37

`stagedResult`

Defined in: stagedResult Total references: 2

Type Signatures (2)

stagedResult : AVMResult (Maybe ControllerId) in AVM.SmallExample:138

`step-account`

Defined in: step-account Total references: 2

Type Signatures (2)

step-account : List AccountMsg → AccountMsg → Maybe (AccountOutput × List AccountMsg) in AVM.Examples:496

`step-counter`

Defined in: step-counter Total references: 2

Type Signatures (2)

step-counter : List CounterMsg → CounterMsg → Maybe (ℕ × List CounterMsg) in AVM.Examples:342

`step-kv`

Defined in: step-kv Total references: 2

Type Signatures (2)

step-kv : List KVMsg → KVMsg → Maybe (Val × List KVMsg) in AVM.Examples:427

`toNonce`

Defined in: toNonce Total references: 2

Type Signatures (2)

toNonce : Nullifier → Nonce in RM.Types.Nullifier:23

`TransactionAborted`

Defined in: TransactionAborted Total references: 2

Other (2)

entry = makeLogEntry (TransactionAborted txid) st in AVM.Interpreter:615
TransactionAborted : TxId → EventType in AVM.Runtime:459

`TransactionCommitted`

Defined in: TransactionCommitted Total references: 2

Other (2)

entry = makeLogEntry (TransactionCommitted txid) st in AVM.Interpreter:599
TransactionCommitted : TxId → EventType in AVM.Runtime:458

`TransactionStarted`

Defined in: TransactionStarted Total references: 2

Other (2)

entry = makeLogEntry (TransactionStarted txid) st in AVM.Interpreter:569
TransactionStarted : TxId → EventType in AVM.Runtime:457

`transferBatch`

Defined in: transferBatch Total references: 2

Type Signatures (2)

transferBatch : List (ObjectId × ObjectId × ℕ) → AVMProgram₁ Val in AVM.Examples:243

`transition`

Defined in: transition Total references: 2

Other (2)

model object behaviour and state transitions. The object model is also close to in AVM.Objects:562

`transition-preserves-type`

Defined in: transition-preserves-type Total references: 2

Other (2)

transition-preserves-type in AVM.Objects:596

`tt`

Defined in: tt Total references: 2

Other (2)

Pending creates are staged object creations committed at transaction end. in AVM.Interpreter:616
constructor tt in Foundation.BasicTypes:105

`TxResult`

Defined in: TxResult Total references: 2

Type Signatures (2)

TxResult : Set → Set in AVM.Runtime:528

`universal`

Defined in: universal Total references: 2

Other (2)

universal : NullifierKey in RM.Types.NullifierKey:36

`updateBalance`

Defined in: updateBalance Total references: 2

Type Signatures (2)

updateBalance : ObjectId → Val → AVMProgram₁ Val in AVM.Examples:202

`wfObjType`

Defined in: wfObjType Total references: 2

Other (2)

constructor wfObjType in AVM.Objects:160

`withRandomGen`

Defined in: withRandomGen Total references: 2

Other (2)

withRandomGen : (ℕ → Program × ℕ) → Program in RM.Types.Program:56

`withTransaction`

Defined in: withTransaction Total references: 2

Type Signatures (2)

withTransaction : ∀ {A : Set} → AVMProgram₁ A → AVMProgram₁ A in AVM.Transactions:36

`≈ˢ-refl`

Defined in: ≈ˢ-refl Total references: 2

Type Signatures (2)

≈ˢ-refl : (obj : SequentialObject) → obj ≈ˢ obj in AVM.Objects:377

`≈ˢ-sym`

Defined in: ≈ˢ-sym Total references: 2

Type Signatures (2)

≈ˢ-sym : (obj₁ obj₂ : SequentialObject) → in AVM.Objects:386

`≈ˢ-trans`

Defined in: ≈ˢ-trans Total references: 2

Other (2)

≈ˢ-trans in AVM.Objects:400

`≈ᵒ-refl`

Defined in: ≈ᵒ-refl Total references: 2

Type Signatures (2)

≈ᵒ-refl : (obj : SequentialObject) → obj ≈ᵒ obj in AVM.Objects:331

`≈ᵒ-sym`

Defined in: ≈ᵒ-sym Total references: 2

Type Signatures (2)

≈ᵒ-sym : (obj₁ obj₂ : SequentialObject) in AVM.Objects:340

`≈ᵒ-trans`

Defined in: ≈ᵒ-trans Total references: 2

Other (2)

≈ᵒ-trans in AVM.Objects:352

`[]-⊑`

Defined in: Agda@[]-⊑ Total references: 1

Other (1)

\[\]-⊑ : ∀ {t} → \[\] ⊑ t in Foundation.Hyperproperties:149

`_`

Defined in: _ Total references: 1

Other (1)

_interact_ with an _external environment_.For a more comprehensive library, in Foundation.InteractionTrees:178

`_∷_-⊑`

Defined in: _∷_-⊑ Total references: 1

Other (1)

_∷_-⊑ : ∀ {x xs t} → head t ≡ x → xs ⊑ tail t → (x ∷ xs) ⊑ t in Foundation.Hyperproperties:150

`Blake3Digest`

Defined in: Blake3Digest Total references: 1

Other (1)

Blake3Digest : String → Digest in RM.Types.Crypto:37

`BLS`

Defined in: BLS Total references: 1

Other (1)

BLS : IDParams in RM.Types.Identities:82

`bool`

Defined in: bool Total references: 1

Other (1)

bool : Bool → StorageValue in RM.Types.Program:24

`bytes`

Defined in: bytes Total references: 1

Other (1)

bytes : String → StorageValue in RM.Types.Program:25

`call-pure`

Defined in: call-pure Total references: 1

Other (1)

pattern call-pure name args = Pure (callPure name args) in AVM.Instruction:450

`choose`

Defined in: choose Total references: 1

Other (1)

thechooseinstruction. Alternative models could use different concurrency semantics, in AVM.Instruction:800

`commit`

Defined in: commit Total references: 1

Other (1)

commit : Capabilities in RM.Types.Identities:98

`commitAndDecrypt`

Defined in: commitAndDecrypt Total references: 1

Other (1)

commitAndDecrypt : Capabilities in RM.Types.Identities:100

`commitmentError`

Defined in: commitmentError Total references: 1

Other (1)

commitmentError : String → ProgramError in RM.Types.Program:42

`connectIdentity`

Defined in: connectIdentity Total references: 1

Other (1)

connectIdentity : EngineId → Backend → Capabilities in RM.Types.Program:63

`Constr`

Defined in: Constr Total references: 1

Other (1)

**Constraint**: This instruction is invalid during active transactions. The in AVM.Instruction:849

`Controller`

Defined in: Controller Total references: 1

Other (1)

-- Controller/distribution types in AVM.Instruction:847

`create`

Defined in: create Total references: 1

Other (1)

create : ObjectId → MessageEvent ⊤ in Foundation.InteractionTrees:45

`curve25519PrivKey`

Defined in: curve25519PrivKey Total references: 1

Other (1)

curve25519PrivKey : String → PrivateKey in RM.Types.Crypto:21

`curve25519PubKey`

Defined in: curve25519PubKey Total references: 1

Other (1)

curve25519PubKey : String → PublicKey in RM.Types.Crypto:16

`decrypt`

Defined in: decrypt Total references: 1

Other (1)

decryptionError : String → ProgramError in RM.Types.Program:59

`decryptionError`

Defined in: decryptionError Total references: 1

Other (1)

decryptionError : String → ProgramError in RM.Types.Program:41

`deleteIdentity`

Defined in: deleteIdentity Total references: 1

Other (1)

deleteIdentity : EngineId → Backend → Program → Program in RM.Types.Program:65

`DeleteImmediately`

Defined in: DeleteImmediately Total references: 1

Other (1)

DeleteImmediately : DeletionCriterion in RM.Types.Action:34

`deleteValue`

Defined in: deleteValue Total references: 1

Other (1)

deleteValue : StorageKey → Program → Program in RM.Types.Program:68

`destroy`

Defined in: destroy Total references: 1

Other (1)

destroy : ObjectId → MessageEvent ⊤ in Foundation.InteractionTrees:46

`do-teleport`

Defined in: do-teleport Total references: 1

Other (1)

pattern do-teleport mid = Machine (teleport mid) in AVM.Instruction:455

`Ed25519`

Defined in: Ed25519 Total references: 1

Other (1)

Ed25519 : IDParams in RM.Types.Identities:80

`ed25519Signature`

Defined in: ed25519Signature Total references: 1

Other (1)

ed25519Signature : String → Signature in RM.Types.Crypto:28

`engineError`

Defined in: engineError Total references: 1

Other (1)

engineError : String → ProgramError in RM.Types.Program:40

`err-function-not-found`

Defined in: err-function-not-found Total references: 1

Other (1)

pattern err-function-not-found name = in AVM.Runtime:398

`err-function-registered`

Defined in: err-function-registered Total references: 1

Other (1)

pattern err-function-registered name = in AVM.Runtime:401

`err-invalid-machine-transfer`

Defined in: err-invalid-machine-transfer Total references: 1

Other (1)

pattern err-invalid-machine-transfer oid mid = in AVM.Runtime:425

`err-object-destroyed`

Defined in: err-object-destroyed Total references: 1

Other (1)

pattern err-object-destroyed oid = in AVM.Runtime:350

`err-object-exists`

Defined in: err-object-exists Total references: 1

Other (1)

pattern err-object-exists oid = in AVM.Runtime:353

`err-object-rejected`

Defined in: err-object-rejected Total references: 1

Other (1)

pattern err-object-rejected oid inp = in AVM.Runtime:359

`err-store-corruption`

Defined in: err-store-corruption Total references: 1

Other (1)

pattern err-store-corruption msg = in AVM.Runtime:369

`err-tx-aborted`

Defined in: err-tx-aborted Total references: 1

Other (1)

pattern err-tx-aborted tid = in AVM.Runtime:385

`err-tx-committed`

Defined in: err-tx-committed Total references: 1

Other (1)

pattern err-tx-committed tid = in AVM.Runtime:382

`err-tx-not-found`

Defined in: err-tx-not-found Total references: 1

Other (1)

pattern err-tx-not-found tid = in AVM.Runtime:379

`err-unauthorized-transfer`

Defined in: err-unauthorized-transfer Total references: 1

Other (1)

pattern err-unauthorized-transfer oid cid = in AVM.Runtime:412

`err-version-mismatch`

Defined in: err-version-mismatch Total references: 1

Other (1)

pattern err-version-mismatch v1 v2 = in AVM.Runtime:415

`error-insufficient`

Defined in: error-insufficient Total references: 1

Other (1)

error-insufficient : AccountOutput in AVM.Examples:476

`ErrorOccurred`

Defined in: ErrorOccurred Total references: 1

Other (1)

ErrorOccurred : AVMError → EventType in AVM.Runtime:462

`first-definition`

Defined in: first-definition Total references: 1

Other (1)

module first-definition where in Foundation.InteractionTrees:64

`generateIdentity`

Defined in: generateIdentity Total references: 1

Other (1)

generateIdentity : Backend → IDParams → Capabilities in RM.Types.Program:61

`get-controller`

Defined in: get-controller Total references: 1

Other (1)

pattern get-controller oid = Controller (getController oid) in AVM.Instruction:460

`get-current-controller`

Defined in: get-current-controller Total references: 1

Other (1)

pattern get-current-controller = Controller getCurrentController in AVM.Instruction:459

`get-current-machine`

Defined in: get-current-machine Total references: 1

Other (1)

pattern get-current-machine = Introspect getCurrentMachine in AVM.Instruction:439

`get-current-version`

Defined in: get-current-version Total references: 1

Other (1)

pattern get-current-version = Controller getCurrentVersion in AVM.Instruction:462

`get-input`

Defined in: get-input Total references: 1

Other (1)

pattern get-input = Introspect input in AVM.Instruction:438

`get-machine`

Defined in: get-machine Total references: 1

Other (1)

pattern get-machine oid = Machine (getMachine oid) in AVM.Instruction:454

`get-self`

Defined in: get-self Total references: 1

Other (1)

pattern get-self = Introspect self in AVM.Instruction:437

`getValue`

Defined in: getValue Total references: 1

Other (1)

getValue : StorageKey → (Maybe StorageValue → Program) → Program in RM.Types.Program:66

`here`

Defined in: here Total references: 1

Other (1)

module Foundation.BasicTypes where in Foundation.BasicTypes:526

`identityError`

Defined in: identityError Total references: 1

Other (1)

identityError : String → ProgramError in RM.Types.Program:43

`int`

Defined in: int Total references: 1

Other (1)

int : ℕ → StorageValue in RM.Types.Program:23

`Introspect`

Defined in: Introspect Total references: 1

Other (1)

- Introspection layer: Context queries and reflection in AVM.Instruction:843

`key`

Defined in: key Total references: 1

Other (1)

key : String → Key in AVM.Examples:358

`localConnection`

Defined in: localConnection Total references: 1

Other (1)

localConnection : String → Backend in RM.Types.Identities:90

`localMemory`

Defined in: localMemory Total references: 1

Other (1)

localMemory : Backend in RM.Types.Identities:89

`Machine`

Defined in: Machine Total references: 1

Other (1)

instruction set of the Anoma Virtual Machine which will implicitly define in AVM.Instruction:846

`mkCid`

Defined in: mkCid Total references: 1

Other (1)

constructor mkCid in AVM.Instruction:811

`mk↔`

Defined in: mk↔ Total references: 1

Other (1)

constructor mk↔ in Foundation.BasicTypes:590

`move-object`

Defined in: move-object Total references: 1

Other (1)

pattern move-object oid mid = Machine (moveObject oid mid) in AVM.Instruction:456

`networkError`

Defined in: networkError Total references: 1

Other (1)

networkError : String → ProgramError in RM.Types.Program:39

`newConstraint`

Defined in: newConstraint Total references: 1

Other (1)

newConstraint : LinearConstraint → ConstraintInstruction Safe ConstraintId in AVM.Instruction:830

`Nondet`

Defined in: Nondet Total references: 1

Other (1)

- Nondeterminism layer: Choice and constraint instructions for intent matching in AVM.Instruction:848

`Obj`

Defined in: Obj Total references: 1

Other (1)

(ObjectId : Set) in AVM.Instruction:842

`obj-call`

Defined in: obj-call Total references: 1

Other (1)

pattern obj-call oid inp = Obj (call oid inp) in AVM.Instruction:434

`obj-create`

Defined in: obj-create Total references: 1

Other (1)

pattern obj-create val = Obj (createObj val) in AVM.Instruction:432

`obj-destroy`

Defined in: obj-destroy Total references: 1

Other (1)

pattern obj-destroy oid = Obj (destroyObj oid) in AVM.Instruction:433

`obj-reflect`

Defined in: obj-reflect Total references: 1

Other (1)

pattern obj-reflect oid = Introspect (reflect oid) in AVM.Instruction:442

`obj-scry-deep`

Defined in: obj-scry-deep Total references: 1

Other (1)

pattern obj-scry-deep pred = Introspect (scryDeep pred) in AVM.Instruction:441

`obj-scry-meta`

Defined in: obj-scry-meta Total references: 1

Other (1)

pattern obj-scry-meta pred = Introspect (scryMeta pred) in AVM.Instruction:440

`Pure`

Defined in: Pure Total references: 1

Other (1)

(TxWrite), controller identity, pure function registry (PureFunctions), in AVM.Instruction:845

`queryByObjectId`

Defined in: queryByObjectId Total references: 1

Other (1)

queryByObjectId : ObjectId → ResourceQuery in RM.Types.Program:32

`queryResource`

Defined in: queryResource Total references: 1

Other (1)

queryResource : ResourceQuery → (Resource → Program) → Program in RM.Types.Program:57

`raise`

Defined in: raise Total references: 1

Other (1)

raise : ProgramError → Program in RM.Types.Program:54

`receive`

Defined in: receive Total references: 1

Other (1)

receive : MessageEvent String in Foundation.InteractionTrees:44

`register-pure`

Defined in: register-pure Total references: 1

Other (1)

pattern register-pure name fn = Pure (registerPure name fn) in AVM.Instruction:451

`remoteConnection`

Defined in: remoteConnection Total references: 1

Other (1)

remoteConnection : ExternalIdentity → Backend in RM.Types.Identities:91

`requestCommitment`

Defined in: requestCommitment Total references: 1

Other (1)

requestCommitment : EngineId → Signable → (Commitment → Program) → Program in RM.Types.Program:60

`require`

Defined in: require Total references: 1

Other (1)

**Authority requirements**:transferObjectrequires proper authorization. in AVM.Instruction:803

`ret-eq`

Defined in: ret-eq Total references: 1

Other (1)

ret-eq : (r : R) → ret r ≈ ret r in Foundation.InteractionTrees:303

`satisfy`

Defined in: satisfy Total references: 1

Other (1)

The instruction set operates uniformly over any object model satisfying the in AVM.Instruction:833

`Secp256k1`

Defined in: Secp256k1 Total references: 1

Other (1)

Secp256k1 : IDParams in RM.Types.Identities:81

`send`

Defined in: send Total references: 1

Other (1)

send : String → MessageEvent ⊤ in Foundation.InteractionTrees:43

`setValue`

Defined in: setValue Total references: 1

Other (1)

setValue : StorageKey → StorageValue → Program → Program in RM.Types.Program:67

`skip`

Defined in: skip Total references: 1

Other (1)

skip : Program in RM.Types.Program:53

`step-trans`

Defined in: step-trans Total references: 1

Other (1)

step-trans in AVM.Objects:583

`storageError`

Defined in: storageError Total references: 1

Other (1)

storageError : String → ProgramError in RM.Types.Program:44

`StoreForever`

Defined in: StoreForever Total references: 1

Other (1)

StoreForever : DeletionCriterion in RM.Types.Action:35

`str`

Defined in: str Total references: 1

Other (1)

str : String → StorageValue in RM.Types.Program:22

`submitTransaction`

Defined in: submitTransaction Total references: 1

Other (1)

submitTransaction : Transaction → Program → Program in RM.Types.Program:58

`switch-version`

Defined in: switch-version Total references: 1

Other (1)

pattern switch-version ver = Controller (switchVersion ver) in AVM.Instruction:463

`Sys×`

Defined in: Sys× Total references: 1

Other (1)

record Sys× {ℓ : Level} {Σᵀ : Set ℓ} (S₁ S₂ : System Σᵀ) : Set (lsuc ℓ) where in Foundation.Hyperproperties:225

`tau-left`

Defined in: tau-left Total references: 1

Other (1)

tau-left : {t₁ t₂ : ITree E R} → t₁ ≈ t₂ → tau t₁ ≈ t₂ in Foundation.InteractionTrees:305

`tau-right`

Defined in: tau-right Total references: 1

Other (1)

tau-right : {t₁ t₂ : ITree E R} → t₁ ≈ t₂ → t₁ ≈ tau t₂ in Foundation.InteractionTrees:306

`there`

Defined in: there Total references: 1

Other (1)

there : {y : A} {xs : List A} → x ∈ xs → x ∈ (y ∷ xs) in Foundation.BasicTypes:527

`transfer-object`

Defined in: transfer-object Total references: 1

Other (1)

pattern transfer-object oid cid = Controller (transferObject oid cid) in AVM.Instruction:461

`tryCatch`

Defined in: tryCatch Total references: 1

Other (1)

tryCatch : Program → (ProgramError → Program) → Program → Program in RM.Types.Program:55

`Tx`

Defined in: Tx Total references: 1

Other (1)

(TxId : Set) in AVM.Instruction:844

`tx-abort`

Defined in: tx-abort Total references: 1

Other (1)

pattern tx-abort tid = Tx (abortTx tid) in AVM.Instruction:447

`tx-begin`

Defined in: tx-begin Total references: 1

Other (1)

pattern tx-begin = Tx beginTx in AVM.Instruction:445

`tx-commit`

Defined in: tx-commit Total references: 1

Other (1)

pattern tx-commit tid = Tx (commitTx tid) in AVM.Instruction:446

`typeError`

Defined in: typeError Total references: 1

Other (1)

typeError : String → ProgramError in RM.Types.Program:45

`UseOnce`

Defined in: UseOnce Total references: 1

Other (1)

UseOnce : ObjectId → Input → LinearConstraint in AVM.Instruction:822

`userError`

Defined in: userError Total references: 1

Other (1)

userError : ProgramError in RM.Types.Program:46

`vis-eq`

Defined in: vis-eq Total references: 1

Other (1)

vis-eq : {A : Set} {e : E A} {k₁ k₂ : A → ITree E R} → in Foundation.InteractionTrees:308

`WeightedVal`

Defined in: WeightedVal Total references: 1

Other (1)

### WeightedVal datatype in AVM.Instruction:790

`ε-trans`

Defined in: ε-trans Total references: 1

Other (1)

ε-trans : ∀ {obj} → obj →*\[ ε \] obj in AVM.Objects:581

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.Crypto
- Symbols: PublicKey, PrivateKey, Signature, Digest, curve25519PubKey, curve25519PrivKey, ed25519Signature, Blake3Digest
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.<$>']

?>

Andreas Abel, Stephan Adelsberger, and Anton Setzer. Interactive programming in agda – objects and graphical user interfaces. Journal of Functional Programming, 27:e8, 2017. doi:10.1017/S0956796816000319. ↩