Symbol Usage Index

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

`nothing`

Defined in: nothing Total references: 156

Other (156)

... | nothing | nothing = nothing in AVM.Interpreter:228
nothing : Maybe A in Background.BasicTypes:294
is-defined φ xs = Object.behavior φ xs ≢ nothing in Background.Objects:141
trigger (Tx (beginTx nothing)) >>= λ txId → in Background.StatelessObjects:128
... | nothing = false in examples.RunnerUtilities:54
trigger (tx-begin nothing) >>= λ setupTx → in examples.Battleship.Game:45
extractShip _ = nothing in examples.Battleship.PlayerBoard:61
showMaybeVal nothing = "nothing" in examples.Battleship.Runner:85
are all represented as functions mapping all object identifiers tonothing. in examples.Common.StateInit:35
createPing = trigger (obj-create "ping" nothing) in examples.PingPong.Main:98
... and 1 more unique reference(s)

`just`

Defined in: just Total references: 149

Other (149)

... | just obj | just meta = just (obj , meta) in AVM.Interpreter:229
just : A → Maybe A in Background.BasicTypes:295
... | just o = o in Background.Objects:155
handleDeposit txId (just r₂) = in Background.StatelessObjects:147
... | just _ = true in examples.RunnerUtilities:53
extractShip (VShip x y len) = just (x , y , len) in examples.Battleship.PlayerBoard:60
showMaybeVal (just v) = "just " ++ˢ showValAgda v in examples.Battleship.Runner:86
extractMsg (PP.VPingPongMsg msg) = just msg in examples.PingPong.Runner:87

`[]`

Defined in: Agda@[] Total references: 145

Other (145)

then just \[\] in AVM.Interpreter:320
\[\] : List A in Background.BasicTypes:463
ε = \[\] in Background.Objects:102
withdraw n = VList (VString "withdraw" ∷ VInt n ∷ \[\]) in Background.StatelessObjects:99
initialState = mkState 0 \[\] in examples.RunnerUtilities:69
checkHit \[\] x y = false in examples.Battleship.PlayerBoard:65
showTrace \[\] = "(no events)" in examples.Common.Display:87
; txLog = \[\] in examples.Common.StateInit:63
(λ result → ret (VList (VString "complete" ∷ result ∷ \[\]))) in examples.PingPong.Main:115
showValAgda (PP.VList \[\]) = "\[\]" in examples.PingPong.Runner:26

`List`

Defined in: List Total references: 129

Type Signatures (34)

VList : List Val → Val in Background.StatelessObjects:32
objects : List ((String × String) × ObjMeta) in examples.RunnerUtilities:66
checkHit : List Val → ℕ → ℕ → Bool in examples.Battleship.PlayerBoard:64
allObjectIds : State → List PB.ObjectId in examples.Battleship.Runner:59
VList : List Val → Val in examples.PingPong.Main:47
(allObjectIds : {State : Set} → State → List ObjectId) in examples.Common.InterpreterSetup:27

Other (95)

concretely inAVM.InstructionasAVMProgram (List Val)and passed through in AVM.Context:84
-- In concrete instantiations, this is AVMProgram (List Val) in AVM.Instruction:208
-- In concrete instantiations, this is AVMProgram (List Val) in AVM.Interpreter:152
## Lists in Background.BasicTypes:462
InputSequence = List Input in Background.Objects:65
showValAgda (PP.VList \[\]) = "\[\]" in examples.PingPong.Runner:98

`_∷_`

Defined in: _∷_ Total references: 114

Other (114)

record st { txLog = (State.txLog st) ++ ((oid , inp) ∷ \[\]) } in AVM.Interpreter:371
_∷_ : A → List A → List A in Background.BasicTypes:464
xs · x = xs ++ (x ∷ \[\]) in Background.Objects:109
withdraw n = VList (VString "withdraw" ∷ VInt n ∷ \[\]) in Background.StatelessObjects:99
lookupObj oid ((k , v) ∷ xs) with eqOID oid k in examples.RunnerUtilities:87
checkHit (v ∷ vs) x y = in examples.Battleship.PlayerBoard:66
(λ result → ret (VList (VString "complete" ∷ result ∷ \[\]))) in examples.PingPong.Main:115
showValAgda (PP.VList (x ∷ xs)) = showValAgda x ++ˢ " :: " ++ˢ showValAgda (PP.VList xs) in examples.PingPong.Runner:27

`if_then_else_`

Defined in: if_then_else_ Total references: 106

Type Signatures (5)

if_then_else_ : {A : Set} → Bool → A → A → A in Background.BasicTypes:195
If-then-else syntax for boolean conditionals: in Background.BasicTypes:196

Other (101)

specification of state transformation functions for each instruction type. in AVM.Interpreter:265
then in AVM.Interpreter:266
else in AVM.Interpreter:268
throughout different entries in this website. in Background.BasicTypes:196
- Object identifiers as pairs of node IDs and strings in Background.StatelessObjects:140
if success then in Background.StatelessObjects:140
else in Background.StatelessObjects:142
-- Check if coordinate is in a ship (vertical ship only for simplicity) in examples.Battleship.PlayerBoard:52
if shipX ==ℕ targetX then in examples.Battleship.PlayerBoard:52
else false in examples.Battleship.PlayerBoard:55
... and 2 more unique reference(s)

`ℕ`

Defined in: ℕ Total references: 105

Type Signatures (81)

Hash = ℕ -- Simplified: in practice would be a cryptographic hash in AVM.Context:226
constraintVars : List (ℕ × List Val) in AVM.Instruction:304
data ℕ : Set where in Background.BasicTypes:343
VInt : ℕ → Val in Background.StatelessObjects:27
showNat : ℕ → String in examples.RunnerUtilities:34
attack : PB.ObjectId → ℕ → ℕ → AVMProgram (Maybe PB.Val) in examples.Battleship.Game:69
freshObjectId : ℕ → PB.ObjectId in examples.Battleship.Runner:32
showNat : ℕ → String in examples.Common.Display:35
eqNat : ℕ → ℕ → Bool in examples.Common.Equality:32
counter : ℕ in examples.PingPong.Main:38
... and 2 more unique reference(s)

Other (24)

open import Background.BasicTypes using (ℕ) in AVM.Interpreter:119
open import Background.BasicTypes using (ℕ) in Background.Objects:18
ObjectId = ℕ in examples.Battleship.PlayerBoard:20

`_,_`

Defined in: _,_ Total references: 102

Other (102)

semantic definitions while designating certain aspects, such as detailed in AVM.Interpreter:229
_,_ : A → B → A × B in Background.BasicTypes:21
The product type represents pairs of values, fundamental for modeling object in Background.BasicTypes:33
This module formalises the core object model from the AVM green paper, including in Background.Objects:381
freshObjectId n = ("default-node" , nat-to-string n) in Background.StatelessObjects:54
This module provides common utilities for running AVM examples, including IO primitives, state manag... in examples.RunnerUtilities:46
Creates a game with two player boards, each with pre-placed ships. in examples.Battleship.Game:55
VShip : ℕ → ℕ → ℕ → Val -- Ship placement (x, y, length) in examples.Battleship.PlayerBoard:60
allObjectIds st = State.observed st ++ map (λ { (oid , _ , _) → oid }) (State.creates st) in examples.Battleship.Runner:60
showOid (_ , id) = id in examples.PingPong.Runner:20

`State`

Defined in: State Total references: 89

Other (89)

- **State Representation:** The complete interpreter knowledge state, including in AVM.Context:252
#### Object and State Management in AVM.Interpreter:188
open import examples.RunnerUtilities hiding (initialState) in examples.Battleship.Runner:59
# Common State Initialization in examples.Common.StateInit:58
open import examples.RunnerUtilities hiding (initialState) in examples.PingPong.Runner:127
(allObjectIds : {State : Set} → State → List ObjectId) in examples.Common.InterpreterSetup:54

`Bool`

Defined in: Bool Total references: 86

Type Signatures (56)

traceMode : Bool -- Debug tracing flag in AVM.Context:278
destroyObj : ObjectId → ObjInstruction Safe Bool -- May fail if object doesn't exist in AVM.Instruction:170
(eqObjectId : ObjectId → ObjectId → Bool) in AVM.Interpreter:183
VBool : Bool → Val in Background.StatelessObjects:28
eqOID : {NodeId : Set} → (NodeId × String) → (NodeId × String) → Bool in examples.RunnerUtilities:51
coordinateHitsShip : ℕ → ℕ → ℕ → ℕ → ℕ → Bool in examples.Battleship.PlayerBoard:50
eqObjectId : PB.ObjectId → PB.ObjectId → Bool in examples.Battleship.Runner:38
eqString : String → String → Bool in examples.Common.Equality:21
eqObjectId : PP.ObjectId → PP.ObjectId → Bool in examples.PingPong.Runner:53
(eqObjectId : ObjectId → ObjectId → Bool) in examples.Common.InterpreterSetup:24

Other (30)

## Boolean Type in Background.BasicTypes:133

`Maybe`

Defined in: Maybe Total references: 86

Type Signatures (57)

creatingController : Maybe ControllerId -- Who created (immutable, may be nothing at birth) in AVM.Context:110
createObj : String → Maybe ControllerId → ObjInstruction Safe ObjectId in AVM.Instruction:169
behavior : InputSequence → Maybe (List Output) in Background.Objects:122
handleDeposit : TxId → Maybe Val → AVMProgram Val in Background.StatelessObjects:145
lookupObj : {ObjMeta : Set} → (String × String) → List ((String × String) × ObjMeta) → Maybe ObjMeta in examples.RunnerUtilities:85
attack : PB.ObjectId → ℕ → ℕ → AVMProgram (Maybe PB.Val) in examples.Battleship.Game:69
extractShip : Val → Maybe (ℕ × ℕ × ℕ) in examples.Battleship.PlayerBoard:59
showMaybeVal : Maybe PB.Val → String in examples.Battleship.Runner:84

Other (29)

open import Background.BasicTypes using (ℕ; List; Maybe) in AVM.Interpreter:152
Option types or Maybe types handle partial operations and potential failures, in Background.BasicTypes:293
caseMaybe (node1 ≟-string node2) in examples.PingPong.Runner:86

`_>>=_`

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

Type Signatures (8)

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

Other (71)

behaviour state inp >>= in Background.Objects:819
trigger (Tx (beginTx nothing)) >>= λ txId → in Background.StatelessObjects:128
open import Background.InteractionTrees hiding (_>>=_) in examples.RunnerUtilities:9
trigger (tx-begin nothing) >>= λ setupTx → in examples.Battleship.Game:45
trigger (Introspect input) >>= λ inp → in examples.Battleship.PlayerBoard:84
open import Background.InteractionTrees as IT hiding (_>>=_) in examples.Battleship.Runner:11
IT._>>=_ (trigger (obj-create "PlayerBoard" nothing)) λ board → in examples.Battleship.Runner:97
createPing >>= λ pingId → in examples.PingPong.Main:105
open import Background.InteractionTrees as IT hiding (_>>=_) in examples.PingPong.Runner:10
IT._>>=_ (trigger (Introspect input)) λ inp → in examples.PingPong.Runner:100

`true`

Defined in: true Total references: 69

Other (69)

... | true = st in AVM.Interpreter:502
true : Bool in Background.BasicTypes:134
ok? (VString "ok") = true in Background.StatelessObjects:105
... | just _ = true in examples.RunnerUtilities:53
then true in examples.Battleship.PlayerBoard:70
eqString s1 s2 = caseMaybe (s1 ≟-string s2) (λ _ → true) false in examples.Common.Equality:22
(λ _ → caseMaybe (id1 ≟-string id2) (λ _ → true) false) in examples.PingPong.Runner:56

`false`

Defined in: false Total references: 61

Other (61)

-- - Accuracy: Best-effort (may have false positives during transient partitions) in AVM.Interpreter:503
false : Bool in Background.BasicTypes:135
ok? (VString _) = false -- Any other string in Background.StatelessObjects:106
... | nothing = false in examples.RunnerUtilities:54
else false in examples.Battleship.PlayerBoard:55
eqString s1 s2 = caseMaybe (s1 ≟-string s2) (λ _ → true) false in examples.Common.Equality:22
; traceMode = false in examples.Common.StateInit:74
(λ _ → caseMaybe (id1 ≟-string id2) (λ _ → true) false) in examples.PingPong.Runner:56

`trigger`

Defined in: trigger Total references: 56

Type Signatures (2)

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

Other (54)

trigger (Tx (beginTx nothing)) >>= λ txId → in Background.StatelessObjects:128
trigger (tx-begin nothing) >>= λ setupTx → in examples.Battleship.Game:45
trigger (Introspect input) >>= λ inp → in examples.Battleship.PlayerBoard:84
IT._>>=_ (trigger (obj-create "PlayerBoard" nothing)) λ board → in examples.Battleship.Runner:97
createPing = trigger (obj-create "ping" nothing) in examples.PingPong.Main:98
IT._>>=_ (trigger (Introspect input)) λ inp → in examples.PingPong.Runner:100

`ret`

Defined in: ret Total references: 54

Type Signatures (12)

ret : R -> ITree₁ E R in Background.InteractionTrees:146
- Attack (VCoord): checks if the coordinate hits any ship, returns hit/miss in examples.Battleship.PlayerBoard:92
instantiated concretely in the Runner module: in examples.PingPong.Main:115

Other (42)

as extra projections. For example, retrieving the current output for a sequential in Background.Objects:796
This module provides concrete examples demonstrating the AVM instruction set defined in Background.StatelessObjects:135
ret (board1 , board2) in examples.Battleship.Game:55
the \[AVM.Interpreter\](../../AVM/Interpreter.lagda.md). in examples.PingPong.Runner:106

`success`

Defined in: success Total references: 53

Other (53)

(success or failure) with associated state transformations in AVM.Context:757
in success (mkSuccess value st' (entry ∷ \[\])) in AVM.Interpreter:434
displaying either error messages or success values with their associated in examples.Common.Display:112

`AVMProgram`

Defined in: AVMProgram Total references: 51

Type Signatures (36)

kudosTransfer : ObjectId → ObjectId → ℕ → AVMProgram Val in Background.StatelessObjects:126
setupGame : AVMProgram GameState in examples.Battleship.Game:43
boardBehavior : AVMProgram (List Val) in examples.Battleship.PlayerBoard:82
getBehavior : PB.ObjectBehaviour → AVMProgram (List PB.Val) in examples.Battleship.Runner:62
createPing : AVMProgram ObjectId in examples.PingPong.Main:97
(getBehavior : ObjectBehaviour → AVMProgram (List Val)) in examples.Common.InterpreterSetup:48

Other (15)

-- In concrete instantiations, this is AVMProgram (List Val) in AVM.Instruction:748
| interpretAVMProgram | \[Interpret programs using full Instruction set\](#complete-avm-program-interp... in AVM.Interpreter:195
-- Import AVMProgram from Instruction module for implementation in Background.Objects:771
-- ObjectBehaviour is concretely defined as AVMProgram (List Val) in examples.PingPong.Runner:98

`failure`

Defined in: failure Total references: 51

Other (51)

- **Error Type Taxonomy:** A hierarchical classification of potential failure in AVM.Context:758
- **Reachability predicates**: Platform-provided failure detection for in AVM.Interpreter:570
showResult showA (failure err) = "Error: " ++ˢ showError err in examples.Common.Display:111

`_×_`

Defined in: _×_ Total references: 50

Type Signatures (23)

data _×_ (A B : Set) : Set where in Background.BasicTypes:20
step : Input → Maybe (Output × Object) in Background.Objects:372
freshId : String → ℕ → (String × String) in examples.RunnerUtilities:45
extractShip : Val → Maybe (ℕ × ℕ × ℕ) in examples.Battleship.PlayerBoard:59

Other (27)

RuntimeObject = ObjectBehaviour × ObjectMeta in AVM.Context:159
ReflectInstruction Unsafe (List (ObjectId × ObjectMeta)) in AVM.Instruction:232
(LogEntry × A) → in AVM.Interpreter:427
ObjectId = NodeId × String in Background.StatelessObjects:44
GameState = PB.ObjectId × PB.ObjectId in examples.Battleship.Game:35
ObjectId = NodeId × String in examples.PingPong.Main:28

`mkSuccess`

Defined in: mkSuccess Total references: 43

Other (43)

constructor mkSuccess in AVM.Context:739
in success (mkSuccess value st' (entry ∷ \[\])) in AVM.Interpreter:434

`_++_`

Defined in: _++_ Total references: 41

Type Signatures (12)

_++_ : {A : Set} → List A → List A → List A in Background.BasicTypes:481

Other (29)

record st { txLog = (State.txLog st) ++ ((oid , inp) ∷ \[\]) } in AVM.Interpreter:371
xs · x = xs ++ (x ∷ \[\]) in Background.Objects:109
step-counter history msg with φ-counter (history ++ (msg ∷ \[\])) in Background.StatelessObjects:342
showValAgda (PB.VCoord x y) = "(VCoord " ++ˢ showNat x ++ˢ " " ++ˢ showNat y ++ˢ ")" in examples.Battleship.Runner:60
showValAgda (PP.VInt n) = "(VInt " ++ˢ showNat n ++ˢ ")" in examples.PingPong.Runner:128

`_≡_`

Defined in: _≡_ Total references: 39

Type Signatures (26)

data _≡_ {A : Set} (x : A) : A → Set where in Background.BasicTypes:206

Other (13)

Object.behavior φ xs ≡ just o₁ → in Background.Objects:180

`refl`

Defined in: refl Total references: 38

Other (38)

refl : x ≡ x in Background.BasicTypes:207
... | nothing = ⊥-elim (defined refl) in Background.Objects:156

`AVMResult`

Defined in: AVMResult Total references: 37

Type Signatures (37)

AVMResult : Set → Set in AVM.Context:775
(interpretAVMProgram : ∀ {A} → AVMProgram A → State → AVMResult A) in AVM.Interpreter:211
interpretAVMProgramRec : ∀ {A} → AVMProgram A → State → AVMResult A in examples.Battleship.Runner:68
showResult : ∀ {A} → (A → String) → AVMResult A → String in examples.Common.Display:110
interpretAVMProgramRec : ∀ {A} → AVMProgram A → State → AVMResult A in examples.PingPong.Runner:146
interpretAVMProgramRec : ∀ {A} → AVMProgram A → State → AVMResult A in examples.Common.InterpreterSetup:54

`ITree`

Defined in: ITree Total references: 34

Other (34)

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

`Safe`

Defined in: Safe Total references: 34

Other (34)

### Safety Datatype in AVM.Instruction:152
machine, subject to reachability constraints. **Safety Invariant**: in AVM.Interpreter:1380

`suc`

Defined in: suc Total references: 33

Other (33)

semantic definitions while designating certain aspects, such as detailed in AVM.Interpreter:348
open import Agda.Primitive using (Level; lsuc) in Background.BasicTypes:345
trigger (Tx(commitTx txId)) >>= λ success → in Background.StatelessObjects:325
indent (suc n) = " " ++ˢ indent n in examples.RunnerUtilities:39
PP.VPingPongMsg (PP.mkMsg msgType (suc (PP.PingPongMsg.counter msg)) myId (PP.PingPongMsg.maxCount m... in examples.PingPong.Runner:95

`caseMaybe`

Defined in: caseMaybe Total references: 32

Type Signatures (3)

caseMaybe : {A B : Set} → Maybe A → (A → B) → B → B in Background.BasicTypes:330

Other (29)

let stUpdate = caseMaybe (State.tx st) (λ _ → inTxUpdate st) (noTxUpdate st) in AVM.Interpreter:432
caseMaybe (extractShip v) in examples.Battleship.PlayerBoard:67
caseMaybe mOut (λ out → " -> " ++ˢ showVal out) "" ++ˢ ")" in examples.Common.Display:51
eqString s1 s2 = caseMaybe (s1 ≟-string s2) (λ _ → true) false in examples.Common.Equality:22
caseMaybe mResult in examples.PingPong.Main:114
caseMaybe (node1 ≟-string node2) in examples.PingPong.Runner:55

`SequentialObject`

Defined in: SequentialObject Total references: 29

Other (29)

SequentialObject, _Observational Equivalence_, and _Behavioural State_. in Background.Objects:248

`zero`

Defined in: zero Total references: 27

Other (27)

zero : ℕ in Background.BasicTypes:344
... | zero = zero -- Cannot go below zero in Background.StatelessObjects:327
indent zero = "" in examples.RunnerUtilities:38

`mkObj`

Defined in: mkObj Total references: 26

Other (26)

constructor mkObjType in Background.Objects:249

`pure-layer-error`

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

Other (26)

pure-layer-error : PureLayerError → AVMError in AVM.Context:506

`Val`

Defined in: Val Total references: 26

Type Signatures (26)

data Val : Set where in examples.PingPong.Main:44
showValAgda : PP.Val → String in examples.PingPong.Runner:23

`_·_`

Defined in: _·_ Total references: 23

Type Signatures (23)

_·_ : InputSequence → Input → InputSequence in Background.Objects:108

`InputSequence`

Defined in: InputSequence Total references: 23

Type Signatures (22)

InputSequence : Set in Background.Objects:64

Other (1)

using (Object; Input; Output; InputSequence; mkObjType) in Background.StatelessObjects:81

`ObjectMeta`

Defined in: ObjectMeta Total references: 23

Other (23)

record ObjectMeta : Set where in AVM.Context:101
reflect : ObjectId → ReflectInstruction Unsafe (Maybe ObjectMeta) in AVM.Instruction:228
updateMeta : ObjectId → ObjectMeta → State → State in AVM.Interpreter:259

`tx-layer-error`

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

Other (23)

tx-layer-error : TxLayerError → PureLayerError in AVM.Context:495

`incrementEventCounter`

Defined in: incrementEventCounter Total references: 22

Type Signatures (22)

incrementEventCounter : State → State in AVM.Interpreter:346

`makeLogEntry`

Defined in: makeLogEntry Total references: 22

Other (22)

| makeLogEntry | \[Construct log entry with event data\](#metadata-initialization-and-observability-lo... in AVM.Interpreter:341

`VarId`

Defined in: VarId Total references: 22

Other (22)

record VarId : Set where in AVM.Instruction:518

`_≈φ[_]_`

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

Type Signatures (10)

_≈φ\[_\]_ : InputSequence → Object → InputSequence → Set in Background.Objects:191

Other (9)

\[^AbelAdelsbergerSetzer-JFP-2017]. in Background.Objects:192

`EventSig`

Defined in: EventSig Total references: 19

Type Signatures (19)

EventSig : Set₁ in Background.InteractionTrees:26

`EventType`

Defined in: EventType Total references: 19

Type Signatures (3)

makeLogEntry : EventType → State → LogEntry in AVM.Interpreter:341
showEventType : EventType → String in examples.Common.Display:46

Other (16)

### EventType in AVM.Context:676

`Safety`

Defined in: Safety Total references: 19

Type Signatures (1)

machine, subject to reachability constraints. **Safety Invariant**: in AVM.Interpreter:1375

Other (18)

### Safety Datatype in AVM.Instruction:151

`⊤`

Defined in: ⊤ Total references: 19

Other (19)

setState : List Val → IntrospectInstruction Safe ⊤ in AVM.Instruction:209
record ⊤ : Set where in Background.BasicTypes:104
send : String → MessageEvent ⊤ in Background.InteractionTrees:43
putStrLn : String → PrimIO ⊤ in examples.RunnerUtilities:17
ObjectBehaviour = ⊤ in examples.Battleship.PlayerBoard:36
runExample : String → ∀ {A} → (A → String) → AVMProgram A → PrimIO ⊤ in examples.Battleship.Runner:107
ObjectBehaviour = ⊤ in examples.PingPong.Main:81
runExample : String → AVMProgram PP.Val → PrimIO ⊤ in examples.PingPong.Runner:188

`ISA`

Defined in: ISA Total references: 18

Type Signatures (1)

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

Other (17)

The AVM instruction set architecture (ISA) defines the primitive operations in AVM.Instruction:135

`Obj`

Defined in: Obj Total references: 18

Other (18)

| **Object layer** | | in AVM.Instruction:675
| executeObj | \[Interpret object lifecycle instructions\](#object-lifecycle-operations) ... in AVM.Interpreter:1352
module Background.StatelessObjects where in Background.StatelessObjects:129
showOid : PP.ObjectId → String in examples.PingPong.Runner:105

`base-error`

Defined in: base-error Total references: 17

Other (17)

base-error : BaseError → TxLayerError in AVM.Context:485

`call`

Defined in: call Total references: 16

Other (16)

|call| \[Send message to object, receive output synchronously\](#call) | in AVM.Instruction:173
instruction set. This allows objects to call other objects, introspect their in AVM.Interpreter:844
trigger (Obj(call fromAcc (withdraw amount))) >>= λ mr₁ → in Background.StatelessObjects:129
(IT._>>=_ (trigger (Obj (call (PP.PingPongMsg.partnerId msg) (mkNextMsg responseType msg myId)))) λ ... in examples.PingPong.Runner:105

`Object`

Defined in: Object Total references: 16

Other (16)

the definitions of _Sequential Object_ as in in Background.Objects:119
module Background.StatelessObjects where in Background.StatelessObjects:81

`ObjectId`

Defined in: ObjectId Total references: 16

Type Signatures (16)

ObjectId : Set in examples.PingPong.Main:27
showOid : PP.ObjectId → String in examples.PingPong.Runner:19

`showEventType`

Defined in: showEventType Total references: 16

Type Signatures (16)

showEventType : EventType → String in examples.Common.Display:46

`_≈_`

Defined in: _≈_ Total references: 15

Type Signatures (15)

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

`∃-syntax`

Defined in: ∃-syntax Total references: 15

Type Signatures (11)

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

Other (4)

\[^AbelAdelsbergerSetzer-JFP-2017]. in Background.Objects:480

`_≡⟨_⟩_`

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

Other (14)

infixr 2 _≡⟨⟩_ _≡⟨_⟩_ in Background.BasicTypes:260
≡⟨ sym (just-injective eq1) ⟩ in Background.Objects:473

`Constraint`

Defined in: Constraint Total references: 14

Other (14)

|reifyConstraints| \[Capture constraint store as data (unsafe)\](#reifyconstraints-unsafe) | in AVM.Instruction:536

`Instruction`

Defined in: Instruction Total references: 14

Other (14)

| Instruction Set | Description | in AVM.Instruction:674
| interpretAVMProgram | \[Interpret programs using full Instruction set\](#complete-avm-program-interp... in AVM.Interpreter:1349

`mkSuccessNoTrace`

Defined in: mkSuccessNoTrace Total references: 14

Type Signatures (14)

mkSuccessNoTrace : ∀ {A} → A → State → AVMResult A in AVM.Interpreter:463

`obj-call`

Defined in: obj-call Total references: 14

Other (14)

pattern obj-call oid inp = Obj (call oid inp) in AVM.Instruction:700
trigger (obj-call board1 (PB.VShip 0 0 3)) >>= λ _ → in examples.Battleship.Game:49
IT._>>=_ (trigger (obj-call board (PB.VShip 0 0 3))) λ _ → in examples.Battleship.Runner:98
in trigger (obj-call pingId initialMsg) >>= λ mResult → in examples.PingPong.Main:113
in IT._>>=_ (trigger (obj-call pongId msg)) λ mResult → in examples.PingPong.Runner:171

`_≈ᵒ_`

Defined in: _≈ᵒ_ Total references: 13

Type Signatures (13)

_≈ᵒ_ : SequentialObject → SequentialObject → Set in Background.Objects:311

`IntrospectInstruction`

Defined in: IntrospectInstruction Total references: 13

Type Signatures (1)

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

Other (12)

#### IntrospectInstruction Datatype in AVM.Instruction:204

`_==ℕ_`

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

Type Signatures (7)

_==ℕ_ : ℕ → ℕ → Bool in Background.BasicTypes:444

Other (5)

if shipX ==ℕ targetX then in examples.Battleship.PlayerBoard:52
eqObjectId = _==ℕ_ in examples.Battleship.Runner:39
eqNat = _==ℕ_ in examples.Common.Equality:33
eqTxId = _==ℕ_ in examples.PingPong.Runner:61

`ControllerId`

Defined in: ControllerId Total references: 12

Type Signatures (3)

ControllerId : Set in examples.PingPong.Main:55

Other (9)

open import AVM.Interpreter PP.Val PP.ObjectId freshObjectId PP.MachineId PP.ControllerId PP.TxId fr... in examples.PingPong.Runner:45

`ok?`

Defined in: ok? Total references: 12

Type Signatures (12)

ok? : Val → Bool in Background.StatelessObjects:104

`VShip`

Defined in: VShip Total references: 12

Other (12)

trigger (obj-call board1 (PB.VShip 0 0 3)) >>= λ _ → in examples.Battleship.Game:49
VShip : ℕ → ℕ → ℕ → Val -- Ship placement (x, y, length) in examples.Battleship.PlayerBoard:24
showValAgda (PB.VShip x y len) = "(VShip " ++ˢ showNat x ++ˢ " " ++ˢ showNat y ++ˢ " len=" ++ˢ showN... in examples.Battleship.Runner:28

`AccountMsg`

Defined in: AccountMsg Total references: 11

Type Signatures (11)

data AccountMsg : Set where in Background.StatelessObjects:441

`executeIntrospect`

Defined in: executeIntrospect Total references: 11

Other (11)

| executeIntrospect | \[Interpret introspection instructions\](#execution-context-introspection-op... in AVM.Interpreter:875

`Key`

Defined in: Key Total references: 11

Other (11)

### Key-Value Store Object (Stateless) in Background.StatelessObjects:356

`KVMsg`

Defined in: KVMsg Total references: 11

Type Signatures (11)

data KVMsg : Set where in Background.StatelessObjects:359

`ObjInstruction`

Defined in: ObjInstruction Total references: 11

Type Signatures (1)

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

Other (10)

capabilities. While individual instruction families (e.g., ObjInstruction, in AVM.Instruction:167

`showValAgda`

Defined in: showValAgda Total references: 11

Type Signatures (11)

showValAgda : PP.Val → String in examples.PingPong.Runner:23

`VString`

Defined in: VString Total references: 11

Other (11)

VString : String → Val in examples.PingPong.Main:46
showValAgda (PP.VString s) = "\"" ++ˢ s ++ˢ "\"" in examples.PingPong.Runner:25

`obj-create`

Defined in: obj-create Total references: 10

Other (10)

pattern obj-create behaviorName mcid = Obj (createObj behaviorName mcid) in AVM.Instruction:698
trigger (obj-create "PlayerBoard" nothing) >>= λ board1 → in examples.Battleship.Game:46
IT._>>=_ (trigger (obj-create "PlayerBoard" nothing)) λ board → in examples.Battleship.Runner:97
createPing = trigger (obj-create "ping" nothing) in examples.PingPong.Main:98
IT._>>=_ (trigger (obj-create "pong" nothing)) λ pongId → in examples.PingPong.Runner:169

`ReflectInstruction`

Defined in: ReflectInstruction Total references: 10

Type Signatures (1)

executeReflect : ∀ {s A} → ReflectInstruction s A → State → AVMResult A in AVM.Interpreter:937

Other (9)

#### ReflectInstruction Datatype in AVM.Instruction:227

`ReifyInstruction`

Defined in: ReifyInstruction Total references: 10

Type Signatures (1)

executeReify : ∀ {s A} → ReifyInstruction s A → State → AVMResult A in AVM.Interpreter:982

Other (9)

#### ReifyInstruction Datatype in AVM.Instruction:310

`replay-account`

Defined in: replay-account Total references: 10

Type Signatures (10)

replay-account : List AccountMsg → ℕ in Background.StatelessObjects:459

`TxId`

Defined in: TxId Total references: 10

Type Signatures (10)

TxId : Set in examples.PingPong.Main:61
freshTxId : ℕ → PP.TxId in examples.PingPong.Runner:39

`_<?_`

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

Type Signatures (6)

_<?_ : ℕ → ℕ → Bool in Background.BasicTypes:414

Other (3)

if 0 <? n then in Background.StatelessObjects:272
targetY <? (shipY +ℕ shipLen) in examples.Battleship.PlayerBoard:54
(if PP.PingPongMsg.counter msg <? PP.PingPongMsg.maxCount msg then in examples.PingPong.Runner:104

`_→*[_]_`

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

Other (9)

data _→*\[_\]_ in Background.Objects:604
\[^AbelAdelsbergerSetzer-JFP-2017]. in Background.Objects:607

`_≈ˢ_`

Defined in: _≈ˢ_ Total references: 9

Type Signatures (9)

_≈ˢ_ : SequentialObject → SequentialObject → Set in Background.Objects:369

`AVMError`

Defined in: AVMError Total references: 9

Type Signatures (1)

showError : AVMError → String in examples.Common.Display:98

Other (8)

### AVMError in AVM.Context:505

`ControllerError`

Defined in: ControllerError Total references: 9

Type Signatures (9)

data ControllerError : Set where in AVM.Context:421

`err-object-not-found`

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

Other (9)

pattern err-object-not-found oid = in AVM.Context:521
... | just _ | nothing | nothing | _ = failure (err-object-not-found oid) in AVM.Interpreter:830

`executeObj`

Defined in: executeObj Total references: 9

Other (9)

| executeObj | \[Interpret object lifecycle instructions\](#object-lifecycle-operations) ... in AVM.Interpreter:813

`GameState`

Defined in: GameState Total references: 9

Type Signatures (9)

GameState : Set in examples.Battleship.Game:34
showGameState : Game.GameState → String in examples.Battleship.Runner:88

`Instr₂`

Defined in: Instr₂ Total references: 9

Other (9)

### Instr₂ instruction set, adds pure function computation in AVM.Instruction:407
| executeInstr₂ | \[Execute with pure computation support\](#extended-instruction-set-interpreter... in AVM.Interpreter:1330

`Instr₃`

Defined in: Instr₃ Total references: 9

Other (9)

### Instr₃ instruction set, adds distributed operations in AVM.Instruction:490

`interpretAux`

Defined in: interpretAux Total references: 9

Type Signatures (9)

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

`is-defined`

Defined in: is-defined Total references: 9

Type Signatures (9)

is-defined : Object → InputSequence → Set in Background.Objects:140

`ITreeF`

Defined in: ITreeF Total references: 9

Other (9)

##ITreeFStructure Functor in Background.InteractionTrees:99

`MachineId`

Defined in: MachineId Total references: 9

Type Signatures (3)

MachineId : Set in examples.PingPong.Main:58

Other (6)

open import AVM.Interpreter PP.Val PP.ObjectId freshObjectId PP.MachineId PP.ControllerId PP.TxId fr... in examples.PingPong.Runner:45

`TxInstruction`

Defined in: TxInstruction Total references: 9

Type Signatures (1)

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

Other (8)

TxInstruction) are defined independently, the numbered instruction sets in AVM.Instruction:360

`VCoord`

Defined in: VCoord Total references: 9

Other (9)

trigger (obj-call board (PB.VCoord x y)) >>= λ result → in examples.Battleship.Game:72
VCoord : ℕ → ℕ → Val -- Attack coordinate in examples.Battleship.PlayerBoard:23
showValAgda (PB.VCoord x y) = "(VCoord " ++ˢ showNat x ++ˢ " " ++ˢ showNat y ++ˢ ")" in examples.Battleship.Runner:27

`_+ℕ_`

Defined in: _+ℕ_ Total references: 8

Type Signatures (6)

_+ℕ_ : ℕ → ℕ → ℕ in Background.BasicTypes:355

Other (2)

x +ℕ prev-bal in Background.StatelessObjects:463
targetY <? (shipY +ℕ shipLen) in examples.Battleship.PlayerBoard:54

`_≤?_`

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

Type Signatures (6)

_≤?_ : ℕ → ℕ → Bool in Background.BasicTypes:407

Other (2)

if 0 ≤? n then in Background.StatelessObjects:220
if shipY ≤? targetY then in examples.Battleship.PlayerBoard:53

`_≥_`

Defined in: _≥_ Total references: 8

Type Signatures (8)

_≥_ : ℕ → ℕ → Set in Background.BasicTypes:387

`closeWithBalance`

Defined in: closeWithBalance Total references: 8

Type Signatures (8)

closeWithBalance : Val → AVMProgram Val in Background.StatelessObjects:270

`controller-error`

Defined in: controller-error Total references: 8

Other (8)

controller-error : ControllerError → AVMError in AVM.Context:508

`ControllerInstruction`

Defined in: ControllerInstruction Total references: 8

Type Signatures (1)

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

Other (7)

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

`counter-type`

Defined in: counter-type Total references: 8

Type Signatures (8)

counter-type : Object in Background.Objects:454

`CounterMsg`

Defined in: CounterMsg Total references: 8

Type Signatures (8)

data CounterMsg : Set where in Background.StatelessObjects:315

`executeController`

Defined in: executeController Total references: 8

Other (8)

| executeController | \[Interpret controller authority instructions\](#logical-authority-and-owner... in AVM.Interpreter:1222

`executeReflect`

Defined in: executeReflect Total references: 8

Other (8)

| executeReflect | \[Interpret reflection instructions\](#reflection-operations) ... in AVM.Interpreter:937

`executeReify`

Defined in: executeReify Total references: 8

Other (8)

| executeReify | \[Interpret reification instructions\](#reification-operations) ... in AVM.Interpreter:982

`filter`

Defined in: filter Total references: 8

Type Signatures (7)

filter : {A : Set} → (A → Bool) → List A → List A in Background.BasicTypes:545
filter-map : {A B : Set} → (A → Maybe B) → List A → List B in Background.StatelessObjects:392

Other (1)

filterMap (λ { (oid' , inp) → if eqObjectId oid oid' then just inp else nothing }) in AVM.Interpreter:391

`filterMap`

Defined in: filterMap Total references: 8

Type Signatures (5)

filterMap : {A B : Set} → (A → Maybe B) → List A → List B in Background.BasicTypes:623

Other (3)

filterMap (λ { (oid' , inp) → if eqObjectId oid oid' then just inp else nothing }) in AVM.Interpreter:360

`helper`

Defined in: helper Total references: 8

Type Signatures (8)

We define helper functions for creating messages and validating responses: in Background.StatelessObjects:202

`Instr₁`

Defined in: Instr₁ Total references: 8

Other (8)

(Instr₀, Instr₁, etc.) compose these families in a cumulative layered in AVM.Instruction:372
| executeInstr₁ | \[Execute with transaction support\](#transactional-instruction-set-interpreter... in AVM.Interpreter:1313

`lookupObjectWithMeta`

Defined in: lookupObjectWithMeta Total references: 8

Other (8)

| lookupObjectWithMeta | \[Retrieve object with metadata\](#object-and-metadata-retrieval-operations) ... in AVM.Interpreter:224

`lookupPendingCreate`

Defined in: lookupPendingCreate Total references: 8

Other (8)

| lookupPendingCreate | \[Query pending object creations\](#object-and-metadata-retrieval-operations)... in AVM.Interpreter:239

`MachineInstruction`

Defined in: MachineInstruction Total references: 8

Type Signatures (1)

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

Other (7)

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

`ObjError`

Defined in: ObjError Total references: 8

Type Signatures (8)

data ObjError : Set where in AVM.Context:329

`PureInstruction`

Defined in: PureInstruction Total references: 8

Type Signatures (1)

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

Other (7)

### PureInstruction datatype in AVM.Instruction:389

`TxError`

Defined in: TxError Total references: 8

Type Signatures (8)

data TxError : Set where in AVM.Context:394

`VPingPongMsg`

Defined in: VPingPongMsg Total references: 8

Other (8)

VPingPongMsg : PingPongMsg → Val in examples.PingPong.Main:48
showValAgda (PP.VPingPongMsg record { msgType = PP.Ping ; counter = c }) = in examples.PingPong.Runner:28

`⊥-elim`

Defined in: ⊥-elim Total references: 8

Type Signatures (2)

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

Other (6)

... | nothing = ⊥-elim (defined refl) in Background.Objects:156

`_→[_]_`

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

Other (7)

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

`_∧_`

Defined in: _∧_ Total references: 7

Type Signatures (7)

_∧_ : Bool → Bool → Bool in Background.BasicTypes:150

`_∨_`

Defined in: _∨_ Total references: 7

Type Signatures (7)

_∨_ : Bool → Bool → Bool in Background.BasicTypes:158

`_≟ℕ_`

Defined in: _≟ℕ_ Total references: 7

Type Signatures (7)

_≟ℕ_ : (m n : ℕ) → Dec (m ≡ n) in Background.BasicTypes:428

`AccountOutput`

Defined in: AccountOutput Total references: 7

Type Signatures (7)

data AccountOutput : Set where in Background.StatelessObjects:473

`any`

Defined in: any Total references: 7

Type Signatures (7)

requirements that any AVM implementation must satisfy: in AVM.Interpreter:492
Check if any element satisfies a predicate: in Background.BasicTypes:595

`BaseError`

Defined in: BaseError Total references: 7

Other (7)

### BaseError (Instr₀) in AVM.Context:472

`executeTx`

Defined in: executeTx Total references: 7

Other (7)

| executeTx | \[Interpret transaction control instructions\](#transactional-semantics-oper... in AVM.Interpreter:1026

`Instr₀`

Defined in: Instr₀ Total references: 7

Other (7)

(Instr₀, Instr₁, etc.) compose these families in a cumulative layered in AVM.Instruction:343
| executeInstr₀ | \[Execute basic instruction set (object + introspect)\](#basic-instruction-set-... in AVM.Interpreter:1299

`Interpreter`

Defined in: Interpreter Total references: 7

Other (7)

### Program-Level Interpreters in AVM.Interpreter:180
## AVM Interpreter Configuration in examples.Battleship.Runner:71
the \[AVM.Interpreter\](../../AVM/Interpreter.lagda.md). in examples.PingPong.Runner:149
# Common Interpreter Setup in examples.Common.InterpreterSetup:57

`Introspect`

Defined in: Introspect Total references: 7

Other (7)

| **Introspection layer** | | in AVM.Instruction:676
| executeIntrospect | \[Interpret introspection instructions\](#execution-context-introspection-op... in AVM.Interpreter:1353
trigger (Introspect input) >>= λ inp → in examples.Battleship.PlayerBoard:84
IT._>>=_ (trigger (Introspect input)) λ inp → in examples.PingPong.Runner:100

`invalidMsg`

Defined in: invalidMsg Total references: 7

Type Signatures (7)

invalidMsg : Val in Background.StatelessObjects:204

`length`

Defined in: length Total references: 7

Type Signatures (4)

length : {A : Set} → List A → ℕ in Background.BasicTypes:475

Other (3)

counter-type = mkObjType (λ inputs → just ((VInt (length inputs)) ∷ \[\])) in Background.Objects:455

`map`

Defined in: map Total references: 7

Type Signatures (5)

map-maybe : {A B : Set} → (A → B) → Maybe A → Maybe B in Background.BasicTypes:509
-- We use a named reference approach: String names map to concrete AVMProgram values in examples.PingPong.Runner:128

Other (2)

map-maybe (λ { (oid' , obj , meta) → obj , meta }) in AVM.Interpreter:1003
allObjectIds st = State.observed st ++ map (λ { (oid , _ , _) → oid }) (State.creates st) in examples.Battleship.Runner:60

`MessageType`

Defined in: MessageType Total references: 7

Type Signatures (4)

data MessageType : Set where in examples.PingPong.Main:30

Other (3)

open PP using (MessageType; Ping; Pong) in examples.PingPong.Runner:79

`obj-error`

Defined in: obj-error Total references: 7

Other (7)

obj-error : ObjError → BaseError in AVM.Context:473

`ObjectBehaviourImpl`

Defined in: ObjectBehaviourImpl Total references: 7

Type Signatures (7)

data ObjectBehaviourImpl : Set where in examples.PingPong.Runner:66

`Ping`

Defined in: Ping Total references: 7

Other (7)

module examples.PingPong.Main where in examples.PingPong.Main:31
showValAgda (PP.VPingPongMsg record { msgType = PP.Ping ; counter = c }) = in examples.PingPong.Runner:28
This module provides the execution harness for the Ping-Pong example using in examples.PingPong.Runner:79

`ReflectError`

Defined in: ReflectError Total references: 7

Type Signatures (7)

data ReflectError : Set where in AVM.Context:357

`replay-counter`

Defined in: replay-counter Total references: 7

Type Signatures (7)

replay-counter : List CounterMsg → ℕ in Background.StatelessObjects:323

`Result`

Defined in: Result Total references: 7

Type Signatures (7)

- **Result Type Algebra:** Algebraic types for communicating execution outcomes in AVM.Context:756

`RuntimeObjectWithId`

Defined in: RuntimeObjectWithId Total references: 7

Type Signatures (6)

RuntimeObjectWithId : Set in AVM.Context:165
inCreates : ObjectId → List RuntimeObjectWithId → Bool in AVM.Interpreter:510

Other (1)

ReflectInstruction Unsafe (List RuntimeObjectWithId) in AVM.Instruction:236

`sym`

Defined in: sym Total references: 7

Type Signatures (2)

sym : {A : Set} {x y : A} → x ≡ y → y ≡ x in Background.BasicTypes:218

Other (5)

φ-equivalence is symmetric. in Background.Objects:212

`tauF`

Defined in: tauF Total references: 7

Other (7)

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

`Tx`

Defined in: Tx Total references: 7

Other (7)

|reifyTxState| \[Capture transaction state as data (unsafe)\](#reifytxstate-unsafe) | in AVM.Instruction:679
| executeTx | \[Interpret transaction control instructions\](#transactional-semantics-oper... in AVM.Interpreter:1356
TxId : Set in Background.StatelessObjects:128
freshTxId : ℕ → PP.TxId in examples.PingPong.Runner:178

`tx-error`

Defined in: tx-error Total references: 7

Other (7)

tx-error : TxError → TxLayerError in AVM.Context:486

`Unsafe`

Defined in: Unsafe Total references: 7

Other (7)

The specification defines two distinct safety levels: Safe and Unsafe. in AVM.Instruction:153

`_,Σ_`

Defined in: _,Σ_ Total references: 6

Other (6)

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

`_||_`

Defined in: _||_ Total references: 6

Type Signatures (6)

_||_ : Bool → Bool → Bool in Background.BasicTypes:173

`_∸_`

Defined in: _∸_ Total references: 6

Type Signatures (6)

_∸_ : ℕ → ℕ → ℕ in Background.BasicTypes:374

`abortWithMsg`

Defined in: abortWithMsg Total references: 6

Type Signatures (6)

abortWithMsg : TxId → String → AVMProgram Val in Background.StatelessObjects:132

`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 Background.BasicTypes:87

Other (2)

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

`checkHit`

Defined in: checkHit Total references: 6

Type Signatures (6)

checkHit : List Val → ℕ → ℕ → Bool in examples.Battleship.PlayerBoard:64

`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 Background.BasicTypes:232

Other (2)

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

`ensureObserved`

Defined in: ensureObserved Total references: 6

Other (6)

| ensureObserved | \[Add object to transaction read set\](#read-set-tracking-and-validation) |... in AVM.Interpreter:499

`executeInstr₀`

Defined in: executeInstr₀ Total references: 6

Other (6)

| executeInstr₀ | \[Execute basic instruction set (object + introspect)\](#basic-instruction-set-... in AVM.Interpreter:1299

`executeMachine`

Defined in: executeMachine Total references: 6

Other (6)

| executeMachine | \[Interpret machine distribution instructions\](#physical-distribution-opera... in AVM.Interpreter:1161

`executePure`

Defined in: executePure Total references: 6

Other (6)

| executePure | \[Interpret pure function instructions\](#pure-computation-operations) ... in AVM.Interpreter:1106

`FDInstruction`

Defined in: FDInstruction Total references: 6

Other (6)

#### FDInstruction datatype in AVM.Instruction:582

`getBehavior`

Defined in: getBehavior Total references: 6

Type Signatures (6)

getBehavior : ObjectBehaviourImpl → AVMProgram (List PP.Val) in examples.PingPong.Runner:132

`getState`

Defined in: getState Total references: 6

Other (6)

|getState| \[Return current object's internal state\](#getstate) | in AVM.Instruction:208
ThegetStateinstruction retrieves the internal state of the current object. in AVM.Interpreter:898
hiding (Input; Output; Message; InputSequence; getState; setState) in Background.Objects:758
hiding (Input; Output; Message; getState; setState) in Background.StatelessObjects:90
trigger (Introspect getState) >>= λ currentState → in examples.Battleship.PlayerBoard:85

`interpret`

Defined in: interpret Total references: 6

Other (6)

The interpreter defines how instructions modify the virtual machine state and in AVM.Interpreter:1394

`isReachableController`

Defined in: isReachableController Total references: 6

Type Signatures (2)

isReachableController : {A : Set} → A → Bool in examples.Common.Equality:55

Other (4)

module interp = Interpreter eqObjectId eqTxId eqControllerId allObjectIds interpretBehaviorName getB... in examples.Battleship.Runner:71
module interp = Interpreter eqObjectId eqTxId eqControllerId allObjectIds interpretBehaviorName getB... in examples.PingPong.Runner:149

`isReachableMachine`

Defined in: isReachableMachine Total references: 6

Type Signatures (2)

isReachableMachine : {A : Set} → A → Bool in examples.Common.Equality:58

Other (4)

module interp = Interpreter eqObjectId eqTxId eqControllerId allObjectIds interpretBehaviorName getB... in examples.Battleship.Runner:71
module interp = Interpreter eqObjectId eqTxId eqControllerId allObjectIds interpretBehaviorName getB... in examples.PingPong.Runner:149

`ITree₁`

Defined in: ITree₁ Total references: 6

Other (6)

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

`KVEvent`

Defined in: KVEvent Total references: 6

Type Signatures (6)

data KVEvent : Set where in Background.StatelessObjects:368

`KVStore`

Defined in: KVStore Total references: 6

Type Signatures (6)

KVStore : Set in Background.StatelessObjects:373

`LogEntry`

Defined in: LogEntry Total references: 6

Other (6)

### LogEntry in AVM.Context:709
| makeLogEntry | \[Construct log entry with event data\](#metadata-initialization-and-observability-lo... in AVM.Interpreter:341
showLogEntry : LogEntry → String in examples.Common.Display:72

`not`

Defined in: not Total references: 6

Type Signatures (3)

Alternative notation for Σ interpreted as existential quantification: in Background.BasicTypes:144

Other (3)

Here we assume AVM programs can use language features not specified by the instruction set. in AVM.Interpreter:391
trigger (Tx (beginTx nothing)) >>= λ txId → in Background.StatelessObjects:392

`playerAttack`

Defined in: playerAttack Total references: 6

Type Signatures (6)

playerAttack : Player → GameState → ℕ → ℕ → AVMProgram (Maybe PB.Val) in examples.Battleship.Game:77

`reflect-error`

Defined in: reflect-error Total references: 6

Other (6)

reflect-error : ReflectError → BaseError in AVM.Context:475

`ReifyError`

Defined in: ReifyError Total references: 6

Type Signatures (6)

data ReifyError : Set where in AVM.Context:376

`retF`

Defined in: retF Total references: 6

Other (6)

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

`setState`

Defined in: setState Total references: 6

Other (6)

|setState| \[Update current object's internal state\](#setstate) | in AVM.Instruction:209
are now managed explicitly via thesetStateinstruction rather than through in AVM.Interpreter:908
hiding (Input; Output; Message; InputSequence; getState; setState) in Background.Objects:758
hiding (Input; Output; Message; getState; setState) in Background.StatelessObjects:90
trigger (Introspect (setState newState)) >>= λ _ → in examples.Battleship.PlayerBoard:91

`updateMeta`

Defined in: updateMeta Total references: 6

Other (6)

| updateMeta | \[Replace metadata for specific object\](#state-transformation-operations) ... in AVM.Interpreter:259

`visF`

Defined in: visF Total references: 6

Other (6)

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

`VList`

Defined in: VList Total references: 6

Other (6)

VList : List Val → Val in examples.PingPong.Main:47
showValAgda (PP.VList \[\]) = "\[\]" in examples.PingPong.Runner:26

`ε`

Defined in: ε Total references: 6

Type Signatures (6)

ε : InputSequence in Background.Objects:101

`Σ`

Defined in: Σ Total references: 6

Other (6)

Dependent pair type (Σ type): in Background.BasicTypes:44
Σ InputSequence (λ hist' → hist' ≈φ\[ φ \] hist) in Background.Objects:236

`φ-account-aux`

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

Type Signatures (6)

φ-account-aux : List AccountMsg → Maybe AccountMsg → Maybe AccountOutput in Background.StatelessObjects:478

`φ-kv-aux`

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

Type Signatures (6)

φ-kv-aux : List KVMsg → Maybe KVMsg → Maybe Val in Background.StatelessObjects:409

`++-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 Background.BasicTypes:493

Other (1)

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

`_*ℕ_`

Defined in: _*ℕ_ Total references: 5

Type Signatures (5)

_*ℕ_ : ℕ → ℕ → ℕ in Background.BasicTypes:361

`_+_`

Defined in: _+_ Total references: 5

Type Signatures (5)

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

`_∈_`

Defined in: _∈_ Total references: 5

Type Signatures (2)

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

Other (3)

syntax ∃-syntax A (λ x → B) = ∃\[ x ∈ A \] B in Background.BasicTypes:645

`_∎`

Defined in: _∎ Total references: 5

Other (5)

infix 3 _∎ in Background.BasicTypes:261
∎ in Background.Objects:477

`all`

Defined in: all Total references: 5

Type Signatures (4)

Decidability type for propositions that can be algorithmically decided: in Background.BasicTypes:587

Other (1)

| executeInstruction | \[Execute full instruction set (all layers)\](#complete-instruction-set-interpr... in AVM.Interpreter:528

`applyCreates`

Defined in: applyCreates Total references: 5

Other (5)

| applyCreates | \[Commit pending object creations\](#transaction-commitment-operations) |... in AVM.Interpreter:609

`applyDestroys`

Defined in: applyDestroys Total references: 5

Other (5)

| applyDestroys | \[Commit pending deletions\](#transaction-commitment-operations) |... in AVM.Interpreter:659

`applyStates`

Defined in: applyStates Total references: 5

Type Signatures (5)

4. applyStates: Apply pending state updates in AVM.Interpreter:685

`applyTransfers`

Defined in: applyTransfers Total references: 5

Other (5)

| applyTransfers | \[Commit pending ownership changes\](#transaction-commitment-operations) |... in AVM.Interpreter:677

`applyWrites`

Defined in: applyWrites Total references: 5

Other (5)

| applyWrites | \[Commit pending input updates\](#transaction-commitment-operations) |... in AVM.Interpreter:628

`attack`

Defined in: attack Total references: 5

Other (5)

Players attack each other's boards directly. in examples.Battleship.Game:69

`begin_`

Defined in: begin_ Total references: 5

Other (5)

infix 1 begin_ in Background.BasicTypes:259
begin in Background.Objects:471

`beginTx`

Defined in: beginTx Total references: 5

Other (5)

|beginTx| \[Start new atomic transaction context\](#begintx) | in AVM.Instruction:361
executeTx (beginTx mController) st with caseMaybe mController (λ cid → isReachableController cid) tr... in AVM.Interpreter:1027
trigger (Tx (beginTx nothing)) >>= λ txId → in Background.StatelessObjects:128
IT._>>=_ (trigger (Tx (beginTx nothing))) λ txid → in examples.PingPong.Runner:178

`bind-step`

Defined in: bind-step Total references: 5

Other (5)

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

`can-process`

Defined in: can-process Total references: 5

Type Signatures (5)

can-process : SequentialObject → Input → Set in Background.Objects:297

`commitTx`

Defined in: commitTx Total references: 5

Other (5)

|commitTx| \[Commit transaction changes to store\](#committx) | in AVM.Instruction:362
executeTx (commitTx txid) st in AVM.Interpreter:1050
trigger (Tx(commitTx txId)) >>= λ success → in Background.StatelessObjects:139
IT._>>=_ (trigger (Tx (commitTx txid))) λ _ → in examples.PingPong.Runner:181

`destroyObj`

Defined in: destroyObj Total references: 5

Other (5)

|destroyObj| \[Mark object for destruction\](#destroyobj) | in AVM.Instruction:170
destroyObjInTx : ObjectId → ObjectMeta → State → AVMResult Bool in AVM.Interpreter:823
trigger (Obj(destroyObj accountToClose)) >>= λ _ → in Background.StatelessObjects:277

`elem`

Defined in: elem Total references: 5

Type Signatures (5)

Operations on the two-element type: in Background.BasicTypes:555

`err-controller-unreachable`

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

Other (5)

pattern err-controller-unreachable cid = in AVM.Context:633
in failure (err-controller-unreachable cid) in AVM.Interpreter:1042

`err-cross-controller-tx`

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

Other (5)

pattern err-cross-controller-tx oid cid = in AVM.Context:639
in failure (err-cross-controller-tx oid cid) in AVM.Interpreter:582

`err-object-has-no-controller`

Defined in: err-object-has-no-controller Total references: 5

Other (5)

pattern err-object-has-no-controller oid = in AVM.Context:651
(failure (err-object-has-no-controller oid)))) in AVM.Interpreter:570

`find`

Defined in: find Total references: 5

Type Signatures (4)

find : {A : Set} → (A → Bool) → List A → Maybe A in Background.BasicTypes:603

Other (1)

(find (λ { (oid' , _ , _) → eqObjectId oid oid' }) (State.creates st)) in AVM.Interpreter:242

`foldr`

Defined in: foldr Total references: 5

Type Signatures (4)

foldr : {A B : Set} → (A → B → B) → B → List A → B in Background.BasicTypes:517

Other (1)

showTrace trace = foldr (λ entry acc → showLogEntry entry ++ˢ "\n" ++ˢ acc) "" trace in examples.Common.Display:88

`GenericInterpreter`

Defined in: GenericInterpreter Total references: 5

Other (5)

module GenericInterpreter in AVM.Interpreter:1374

`getController`

Defined in: getController Total references: 5

Other (5)

|getController| \[Query object's controller\](#getcontroller) | in AVM.Instruction:469
executeController (getController oid) st with lookupPendingCreate oid st in AVM.Interpreter:1232

`handleCall`

Defined in: handleCall Total references: 5

Other (5)

| handleCall | \[Execute object behavior and manage state\](#object-invocation-semantics) ... in AVM.Interpreter:700

`handleCall-aux`

Defined in: handleCall-aux Total references: 5

Other (5)

in handleCall-aux (interpretAVMProgram (getBehavior obj) objectContext) (State.tx st) in AVM.Interpreter:709

`Handler`

Defined in: Handler Total references: 5

Type Signatures (5)

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

`head`

Defined in: head Total references: 5

Type Signatures (3)

head-empty : {A : Set} → A in Background.BasicTypes:537

Other (2)

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

`input`

Defined in: input Total references: 5

Other (5)

|input| \[Return current input message\](#input) | in AVM.Instruction:206
| addPendingWrite | \[Append input to transaction log\](#transaction-log-query-operations) ... in AVM.Interpreter:883
trigger (Introspect input) >>= λ inp → in examples.Battleship.PlayerBoard:84
IT._>>=_ (trigger (Introspect input)) λ inp → in examples.PingPong.Runner:100

`interp-step`

Defined in: interp-step Total references: 5

Other (5)

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

`lookup`

Defined in: lookup Total references: 5

Type Signatures (4)

lookup : {A B : Set} → (A → A → Bool) → A → List (A × B) → Maybe B in Background.BasicTypes:613

Other (1)

| lookupObjectWithMeta | \[Retrieve object with metadata\](#object-and-metadata-retrieval-operations) ... in AVM.Interpreter:250

`MachineError`

Defined in: MachineError Total references: 5

Type Signatures (5)

data MachineError : Set where in AVM.Context:409

`MessageEvent`

Defined in: MessageEvent Total references: 5

Type Signatures (5)

data MessageEvent : EventSig where in Background.InteractionTrees:42

`msg-to-event`

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

Type Signatures (5)

msg-to-event : KVMsg → Maybe KVEvent in Background.StatelessObjects:404

`namedBehaviour`

Defined in: namedBehaviour Total references: 5

Other (5)

namedBehaviour : String → ObjectBehaviourImpl in examples.PingPong.Runner:67

`no`

Defined in: no Total references: 5

Other (5)

Alternative notation for Σ interpreted as existential quantification: in Background.BasicTypes:251

`null`

Defined in: null Total references: 5

Type Signatures (3)

null : {A : Set} → List A → Bool in Background.BasicTypes:525

Other (2)

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

`ObjectDestroyed`

Defined in: ObjectDestroyed Total references: 5

Other (5)

ObjectDestroyed : ObjectId → EventType in AVM.Context:679
entry = makeLogEntry (ObjectDestroyed oid) stObs in AVM.Interpreter:796
showEventType (ObjectDestroyed oid) = "ObjectDestroyed(" ++ˢ showOid oid ++ˢ ")" in examples.Common.Display:48

`ObjectTransferred`

Defined in: ObjectTransferred Total references: 5

Other (5)

ObjectTransferred : ObjectId → ControllerId → ControllerId → EventType in AVM.Context:691
entry = makeLogEntry (ObjectTransferred oid sourceCid targetCid) stObs in AVM.Interpreter:774
showEventType (ObjectTransferred oid fromCtrl toCtrl) = "ObjectTransferred(" ++ˢ showOid oid ++ˢ ", ... in examples.Common.Display:56

`PingPongMsg`

Defined in: PingPongMsg Total references: 5

Other (5)

record PingPongMsg : Set where in examples.PingPong.Main:34
extractMsg : PP.Val → Maybe PP.PingPongMsg in examples.PingPong.Runner:86

`Player`

Defined in: Player Total references: 5

Other (5)

open import examples.Battleship.PlayerBoard as PB in examples.Battleship.Game:29

`Pred`

Defined in: Pred Total references: 5

Other (5)

## Predicates and Set Relations in Background.BasicTypes:684

`process-input`

Defined in: process-input Total references: 5

Other (5)

process-input in Background.Objects:282

`processTransfers`

Defined in: processTransfers Total references: 5

Other (5)

processTransfers transfers in Background.StatelessObjects:244

`PureError`

Defined in: PureError Total references: 5

Type Signatures (5)

data PureError : Set where in AVM.Context:437

`PureLayerError`

Defined in: PureLayerError Total references: 5

Other (5)

### PureLayerError (Instr₂) in AVM.Context:494

`reify-error`

Defined in: reify-error Total references: 5

Other (5)

reify-error : ReifyError → BaseError in AVM.Context:476

`replay-kv`

Defined in: replay-kv Total references: 5

Type Signatures (5)

replay-kv : List KVEvent → KVStore in Background.StatelessObjects:395

`resolveAndCheckOwnership`

Defined in: resolveAndCheckOwnership Total references: 5

Type Signatures (5)

resolveAndCheckOwnership : ObjectId → ObjectMeta → State → AVMResult (State × Bool) in AVM.Interpreter:574

`resolveTxController`

Defined in: resolveTxController Total references: 5

Other (5)

-- Old checkOwnership removed - use checkOwnershipPure and resolveTxController instead in AVM.Interpreter:559

`setupGame`

Defined in: setupGame Total references: 5

Type Signatures (5)

setupGame : AVMProgram GameState in examples.Battleship.Game:43

`showGameState`

Defined in: showGameState Total references: 5

Type Signatures (5)

showGameState : Game.GameState → String in examples.Battleship.Runner:88

`showMaybeVal`

Defined in: showMaybeVal Total references: 5

Type Signatures (5)

showMaybeVal : Maybe PB.Val → String in examples.Battleship.Runner:84

`showResult`

Defined in: showResult Total references: 5

Type Signatures (3)

showResult : ∀ {A} → (A → String) → AVMResult A → String in examples.Common.Display:110

Other (2)

putStrLn (showResult showA result) in examples.Battleship.Runner:112
putStrLn (showResult showValAgda result) in examples.PingPong.Runner:193

`Trace`

Defined in: Trace Total references: 5

Other (5)

### Trace in AVM.Context:720
-- Traceless success construction produces a success result with an empty in AVM.Interpreter:1380
## Trace Display in examples.Common.Display:86

`trans`

Defined in: trans Total references: 5

Type Signatures (3)

trans : {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z in Background.BasicTypes:225

Other (2)

transaction processing units. Objects may be deterministic or nondeterministic in Background.Objects:225

`tt`

Defined in: tt Total references: 5

Other (5)

queried prior to consulting the global store, ensuring visibility of uncommitted in AVM.Interpreter:912
constructor tt in Background.BasicTypes:105
# Battleship Runner in examples.Battleship.Runner:57

`TxLayerError`

Defined in: TxLayerError Total references: 5

Other (5)

### TxLayerError (Instr₁) in AVM.Context:484

`vis`

Defined in: vis Total references: 5

Type Signatures (5)

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

`WellFormedObjectType`

Defined in: WellFormedObjectType Total references: 5

Other (5)

record WellFormedObjectType (φ : Object) : Set where in Background.Objects:162

`⊥`

Defined in: ⊥ Total references: 5

Type Signatures (5)

data ⊥ : Set where in Background.BasicTypes:113

`++-right-id`

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

Type Signatures (4)

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

`_≢_`

Defined in: _≢_ Total references: 4

Type Signatures (3)

_≢_ : {A : Set} → A → A → Set in Background.BasicTypes:240

Other (1)

is-defined φ xs = Object.behavior φ xs ≢ nothing in Background.Objects:141

`abortTx`

Defined in: abortTx Total references: 4

Other (4)

|abortTx| \[Abort transaction, discard changes\](#aborttx) | in AVM.Instruction:363
executeTx (abortTx txid) st = in AVM.Interpreter:1084
trigger (Tx(abortTx txId)) >>= λ _ → in Background.StatelessObjects:134

`addPendingTransfer`

Defined in: addPendingTransfer Total references: 4

Other (4)

| addPendingTransfer | \[Schedule ownership change\](#transactional-overlay-management) ... in AVM.Interpreter:407

`allObjectIds`

Defined in: allObjectIds Total references: 4

Type Signatures (4)

allObjectIds : State → List PP.ObjectId in examples.PingPong.Runner:127

`apply-kv-event`

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

Type Signatures (4)

apply-kv-event : KVStore → KVEvent → KVStore in Background.StatelessObjects:391

`concat`

Defined in: concat Total references: 4

Type Signatures (4)

List concatenation is associative: in Background.BasicTypes:563

`concatMap`

Defined in: concatMap Total references: 4

Type Signatures (4)

concatMap : {A B : Set} → (A → List B) → List A → List B in Background.BasicTypes:579

`createObj`

Defined in: createObj Total references: 4

Other (4)

|createObj| \[Create new object by referencing behavior name\](#createobj) | in AVM.Instruction:169
-- createObj instruction, eliminating duplication between immediate creation in AVM.Interpreter:814
trigger (Obj(createObj "counter" nothing)) >>= λ counterId → in Background.StatelessObjects:173

`createWithMeta`

Defined in: createWithMeta Total references: 4

Other (4)

| createWithMeta | \[Install object and metadata in store\](#state-transformation-operations) ... in AVM.Interpreter:304

`Dec`

Defined in: Dec Total references: 4

Other (4)

## Equality and Decidability in Background.BasicTypes:249

`deposit`

Defined in: deposit Total references: 4

Type Signatures (4)

deposit : ℕ → Message in Background.StatelessObjects:101

`destroyObjNoTx`

Defined in: destroyObjNoTx Total references: 4

Type Signatures (4)

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

`Domain`

Defined in: Domain Total references: 4

Other (4)

### Finite Domain Constraint Programming Layer in AVM.Instruction:527

`eqBool`

Defined in: eqBool Total references: 4

Type Signatures (4)

eqBool : Bool → Bool → Bool in examples.Common.Equality:41

`eqControllerId`

Defined in: eqControllerId Total references: 4

Type Signatures (4)

eqControllerId : PP.ControllerId → PP.ControllerId → Bool in examples.PingPong.Runner:75

`eqObjectId`

Defined in: eqObjectId Total references: 4

Type Signatures (4)

eqObjectId : PP.ObjectId → PP.ObjectId → Bool in examples.PingPong.Runner:53

`eqString`

Defined in: eqString Total references: 4

Type Signatures (2)

eqString : String → String → Bool in examples.Common.Equality:21

Other (2)

eqControllerId = eqString in examples.Battleship.Runner:51
eqControllerId = eqString in examples.PingPong.Runner:76

`eqTxId`

Defined in: eqTxId Total references: 4

Type Signatures (4)

eqTxId : PP.TxId → PP.TxId → Bool in examples.PingPong.Runner:60

`err-metadata-corruption`

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

Other (4)

pattern err-metadata-corruption oid = in AVM.Context:536
... | just _ | nothing | just _ | nothing = failure (err-metadata-corruption oid) in AVM.Interpreter:829

`extractMsg`

Defined in: extractMsg Total references: 4

Type Signatures (4)

extractMsg : PP.Val → Maybe PP.PingPongMsg in examples.PingPong.Runner:86

`extractShip`

Defined in: extractShip Total references: 4

Type Signatures (4)

extractShip : Val → Maybe (ℕ × ℕ × ℕ) in examples.Battleship.PlayerBoard:59

`freshObjectId`

Defined in: freshObjectId Total references: 4

Type Signatures (4)

freshObjectId : ℕ → PP.ObjectId in examples.PingPong.Runner:36

`freshTxId`

Defined in: freshTxId Total references: 4

Type Signatures (4)

freshTxId : ℕ → PP.TxId in examples.PingPong.Runner:39

`genericPingPongBehavior`

Defined in: genericPingPongBehavior Total references: 4

Type Signatures (4)

genericPingPongBehavior : MessageType → String → AVMProgram (List PP.Val) in examples.PingPong.Runner:98

`handleBalance`

Defined in: handleBalance Total references: 4

Other (4)

handleBalance mBalance in Background.StatelessObjects:268

`handleDeposit`

Defined in: handleDeposit Total references: 4

Type Signatures (4)

handleDeposit : TxId → Maybe Val → AVMProgram Val in Background.StatelessObjects:145

`handleInput`

Defined in: handleInput Total references: 4

Other (4)

handleInput inp currentState in examples.Battleship.PlayerBoard:86

`handleResult`

Defined in: handleResult Total references: 4

Other (4)

handleResult mv₃ in Background.StatelessObjects:185

`handleUpdateResult`

Defined in: handleUpdateResult Total references: 4

Type Signatures (4)

handleUpdateResult : Maybe Val → AVMProgram Val in Background.StatelessObjects:210

`handleWithdraw`

Defined in: handleWithdraw Total references: 4

Other (4)

handleWithdraw txId mr₁ in Background.StatelessObjects:130

`hasDuplicates`

Defined in: hasDuplicates Total references: 4

Type Signatures (4)

hasDuplicates : {A : Set} → List A → Bool in Background.BasicTypes:571

`indent`

Defined in: indent Total references: 4

Type Signatures (4)

indent : ℕ → String in examples.RunnerUtilities:37

`interpretAVMProgramRec`

Defined in: interpretAVMProgramRec Total references: 4

Type Signatures (4)

interpretAVMProgramRec : ∀ {A} → AVMProgram A → State → AVMResult A in examples.Common.InterpreterSetup:54

`interpretBehaviorName`

Defined in: interpretBehaviorName Total references: 4

Type Signatures (4)

interpretBehaviorName : String → ObjectBehaviourImpl in examples.PingPong.Runner:121

`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 Background.BasicTypes:307

Other (2)

≡⟨ sym (just-injective eq1) ⟩ in Background.Objects:473

`just≢nothing`

Defined in: just≢nothing Total references: 4

Type Signatures (2)

just≢nothing : ∀ {A} {x : A} → just x ≡ nothing → ⊥ in Background.BasicTypes:302

Other (2)

... | just _ | _ = just≢nothing eq-xs in Background.Objects:488

`lookupObj`

Defined in: lookupObj Total references: 4

Type Signatures (4)

lookupObj : {ObjMeta : Set} → (String × String) → List ((String × String) × ObjMeta) → Maybe ObjMeta in examples.RunnerUtilities:85

`machine-error`

Defined in: machine-error Total references: 4

Other (4)

machine-error : MachineError → AVMError in AVM.Context:507

`map-maybe`

Defined in: map-maybe Total references: 4

Type Signatures (3)

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

Other (1)

map-maybe (λ { (oid' , obj , meta) → obj , meta }) in AVM.Interpreter:241

`mkControllerId`

Defined in: mkControllerId Total references: 4

Type Signatures (4)

mkControllerId : String → PP.ControllerId in examples.PingPong.Runner:137

`mkInitialState`

Defined in: mkInitialState Total references: 4

Type Signatures (2)

mkInitialState : MachineId → ObjectId → Val → State in examples.Common.StateInit:58

Other (2)

initialState = mkInitialState "node1" 0 (PB.VCoord 0 0) in examples.Battleship.Runner:82
initialState = mkInitialState "node1" ("root", "orchestrator") (VString "") in examples.PingPong.Runner:161

`mkMsg`

Defined in: mkMsg Total references: 4

Other (4)

constructor mkMsg in examples.PingPong.Main:35
PP.VPingPongMsg (PP.mkMsg msgType (suc (PP.PingPongMsg.counter msg)) myId (PP.PingPongMsg.maxCount m... in examples.PingPong.Runner:95

`mkObjType`

Defined in: mkObjType Total references: 4

Other (4)

constructor mkObjType in Background.Objects:120
using (Object; Input; Output; InputSequence; mkObjType) in Background.StatelessObjects:81

`NondetInstruction`

Defined in: NondetInstruction Total references: 4

Type Signatures (4)

data NondetInstruction : Safety → ISA where in AVM.Instruction:623

`ObjectCalled`

Defined in: ObjectCalled Total references: 4

Other (4)

ObjectCalled : ObjectId → Input → Maybe Output → EventType in AVM.Context:682
entry = makeLogEntry (ObjectCalled oid inp output) stWithPending in AVM.Interpreter:725
showEventType (ObjectCalled oid inp mOut) = in examples.Common.Display:49

`ObjectFrozen`

Defined in: ObjectFrozen Total references: 4

Other (4)

ObjectFrozen : ObjectId → ControllerId → EventType in AVM.Context:692
entry = makeLogEntry (ObjectFrozen oid freezeCid) st in AVM.Interpreter:1280
showEventType (ObjectFrozen oid ctrl) = "ObjectFrozen(" ++ˢ showOid oid ++ˢ ", " ++ˢ showCid ctrl ++... in examples.Common.Display:57

`opponentBoard`

Defined in: opponentBoard Total references: 4

Type Signatures (4)

opponentBoard : Player → GameState → PB.ObjectId in examples.Battleship.Game:58

`Player1`

Defined in: Player1 Total references: 4

Other (4)

Player1 : Player in examples.Battleship.Game:30

`player1Attack`

Defined in: player1Attack Total references: 4

Other (4)

player1Attack = attack in examples.Battleship.Game:81

`Player2`

Defined in: Player2 Total references: 4

Other (4)

Player2 : Player in examples.Battleship.Game:31

`Pong`

Defined in: Pong Total references: 4

Other (4)

module examples.PingPong.Main where in examples.PingPong.Main:32
showValAgda (PP.VPingPongMsg record { msgType = PP.Pong ; counter = c }) = in examples.PingPong.Runner:30
This module provides the execution harness for the Ping-Pong example using in examples.PingPong.Runner:79

`pure-error`

Defined in: pure-error Total references: 4

Other (4)

pure-error : PureError → PureLayerError in AVM.Context:496

`PureFunctions`

Defined in: PureFunctions Total references: 4

Type Signatures (4)

PureFunctions : Set in AVM.Context:237
noPureFunctions : PureFunctions in examples.Common.StateInit:45

`run-object-itree`

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

Other (4)

run-object-itree in Background.Objects:807

`runExample`

Defined in: runExample Total references: 4

Type Signatures (4)

runExample : String → AVMProgram PP.Val → PrimIO ⊤ in examples.PingPong.Runner:188

`RuntimeObject`

Defined in: RuntimeObject Total references: 4

Type Signatures (4)

RuntimeObject : Set in AVM.Context:158
lookupObjectWithMeta : ObjectId → State → Maybe RuntimeObject in AVM.Interpreter:224

`self`

Defined in: self Total references: 4

Other (4)

|self| \[Return current object's ID\](#self) | in AVM.Instruction:205
-- Program interpreter: Recursive self-reference to avoid circular dependencies in AVM.Interpreter:876
IT._>>=_ (trigger (Introspect self)) λ myId → in examples.PingPong.Runner:101

`showNat`

Defined in: showNat Total references: 4

Type Signatures (3)

showNat : ℕ → String in examples.Common.Display:35

Other (1)

showValAgda (PP.VInt n) = "(VInt " ++ˢ showNat n ++ˢ ")" in examples.PingPong.Runner:72

`showTrace`

Defined in: showTrace Total references: 4

Type Signatures (4)

showTrace : Trace → String in examples.Common.Display:86

`tau`

Defined in: tau Total references: 4

Other (4)

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

`tx-begin`

Defined in: tx-begin Total references: 4

Other (4)

pattern tx-begin mcid = Tx (beginTx mcid) in AVM.Instruction:722
trigger (tx-begin nothing) >>= λ setupTx → in examples.Battleship.Game:45

`updateState`

Defined in: updateState Total references: 4

Type Signatures (4)

updateState : ObjectId → List Val → State → State in AVM.Interpreter:284

`VBool`

Defined in: VBool Total references: 4

Other (4)

VBool : Bool → Val in Background.StatelessObjects:28

`VNil`

Defined in: VNil Total references: 4

Other (4)

VNil : Val in Background.StatelessObjects:31

`VPair`

Defined in: VPair Total references: 4

Other (4)

VPair : Val → Val → Val in Background.StatelessObjects:30

`withdraw`

Defined in: withdraw Total references: 4

Type Signatures (4)

withdraw : ℕ → Message in Background.StatelessObjects:98

`yes`

Defined in: yes Total references: 4

Other (4)

yes : A → Dec A in Background.BasicTypes:250

`¬`

Defined in: ¬ Total references: 4

Type Signatures (4)

¬ : Set → Set in Background.BasicTypes:126

`·-++-assoc`

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

Other (4)

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

`φ-account`

Defined in: φ-account Total references: 4

Type Signatures (4)

φ-account-aux : List AccountMsg → Maybe AccountMsg → Maybe AccountOutput in Background.StatelessObjects:487

`φ-kv`

Defined in: φ-kv Total references: 4

Type Signatures (4)

φ-kv-aux : List KVMsg → Maybe KVMsg → Maybe Val in Background.StatelessObjects:418

`_<$>_`

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

Type Signatures (3)

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

`_>>=ᴹ_`

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

Type Signatures (3)

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

`_↔_`

Defined in: _↔_ Total references: 3

Other (3)

record _↔_ (A B : Set) : Set where in Background.BasicTypes:713

`_∈Pred_`

Defined in: _∈Pred_ Total references: 3

Type Signatures (3)

_∈Pred_ : {ℓ : Level} {A : Set ℓ} → A → Pred A → Set ℓ in Background.BasicTypes:691

`_∘_`

Defined in: _∘_ Total references: 3

Type Signatures (2)

_∘_ : {A B C : Set} → (B → C) → (A → B) → A → C in Background.BasicTypes:733

Other (1)

f <$> t = t >>= (ret ∘ f) in Background.InteractionTrees:201

`_≡⟨⟩_`

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

Other (3)

infixr 2 _≡⟨⟩_ _≡⟨_⟩_ in Background.BasicTypes:260

`_≤_`

Defined in: _≤_ Total references: 3

Type Signatures (3)

_≤_ : ℕ → ℕ → Set in Background.BasicTypes:395

`_⊆_`

Defined in: _⊆_ Total references: 3

Type Signatures (3)

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

`addPendingCreate`

Defined in: addPendingCreate Total references: 3

Other (3)

| addPendingCreate | \[Stage object creation for commit\](#transactional-overlay-management) ... in AVM.Interpreter:380

`addPendingDestroy`

Defined in: addPendingDestroy Total references: 3

Other (3)

| addPendingDestroy | \[Mark object for deletion\](#transactional-overlay-management) ... in AVM.Interpreter:398

`addPendingWrite`

Defined in: addPendingWrite Total references: 3

Other (3)

| addPendingWrite | \[Append input to transaction log\](#transaction-log-query-operations) ... in AVM.Interpreter:369

`applyDestroy`

Defined in: applyDestroy Total references: 3

Other (3)

| applyDestroys | \[Commit pending deletions\](#transaction-commitment-operations) |... in AVM.Interpreter:638

`applyTransfer`

Defined in: applyTransfer Total references: 3

Other (3)

| applyTransfers | \[Commit pending ownership changes\](#transaction-commitment-operations) |... in AVM.Interpreter:667

`applyWrite`

Defined in: applyWrite Total references: 3

Other (3)

| applyWrites | \[Commit pending input updates\](#transaction-commitment-operations) |... in AVM.Interpreter:620

`balanceMsg`

Defined in: balanceMsg Total references: 3

Other (3)

balanceMsg : AccountMsg in Background.StatelessObjects:444

`boardBehavior`

Defined in: boardBehavior Total references: 3

Type Signatures (2)

boardBehavior : AVMProgram (List Val) in examples.Battleship.PlayerBoard:82

Other (1)

getBehavior _ = PB.boardBehavior in examples.Battleship.Runner:63

`callObjInTx`

Defined in: callObjInTx Total references: 3

Type Signatures (3)

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

`callPure`

Defined in: callPure Total references: 3

Other (3)

|callPure| \[Invoke registered pure function\](#callpure) | in AVM.Instruction:391
executePure (callPure name args) st in AVM.Interpreter:1107

`checkObject`

Defined in: checkObject Total references: 3

Other (3)

validateObserved st = all checkObject (State.observed st) in AVM.Interpreter:528

`checkOwnershipPure`

Defined in: checkOwnershipPure Total references: 3

Other (3)

-- Old checkOwnership removed - use checkOwnershipPure and resolveTxController instead in AVM.Interpreter:550

`commitWithResult`

Defined in: commitWithResult Total references: 3

Type Signatures (3)

commitWithResult : TxId → AVMProgram Val in Background.StatelessObjects:137

`containsObserved`

Defined in: containsObserved Total references: 3

Type Signatures (3)

containsObserved : ObjectId → List ObjectId → Bool in AVM.Interpreter:491

`coordinateHitsShip`

Defined in: coordinateHitsShip Total references: 3

Type Signatures (3)

coordinateHitsShip : ℕ → ℕ → ℕ → ℕ → ℕ → Bool in examples.Battleship.PlayerBoard:50

`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 Background.Objects:480

`counter-wf`

Defined in: counter-wf Total references: 3

Type Signatures (3)

counter-wf : WellFormedObjectType counter-type in Background.Objects:463

`create-object`

Defined in: create-object Total references: 3

Other (3)

create-object in Background.Objects:645

`createCounter`

Defined in: createCounter Total references: 3

Type Signatures (3)

createCounter : Val → AVMProgram ObjectId in Background.StatelessObjects:171

`createPing`

Defined in: createPing Total references: 3

Type Signatures (3)

createPing : AVMProgram ObjectId in examples.PingPong.Main:97

`createPong`

Defined in: createPong Total references: 3

Type Signatures (3)

createPong : AVMProgram ObjectId in examples.PingPong.Main:100

`del`

Defined in: del Total references: 3

Other (3)

Now we instantiate the object model and instruction set with our concrete types. in Background.StatelessObjects:361

`del-event`

Defined in: del-event Total references: 3

Other (3)

del-event : Key → KVEvent in Background.StatelessObjects:370

`depositMsg`

Defined in: depositMsg Total references: 3

Other (3)

depositMsg : ℕ → AccountMsg in Background.StatelessObjects:442

`destroyObjInTx`

Defined in: destroyObjInTx Total references: 3

Type Signatures (3)

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

`emptyStore`

Defined in: emptyStore Total references: 3

Type Signatures (3)

emptyStore : Store in examples.Common.StateInit:34

`eqOID`

Defined in: eqOID Total references: 3

Type Signatures (3)

eqOID : {NodeId : Set} → (NodeId × String) → (NodeId × String) → Bool in examples.RunnerUtilities:51

`equiv-after-input`

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

Other (3)

,Σ (refl , refl , equiv-after-input)) in Background.Objects:725

`err-machine-unreachable`

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

Other (3)

pattern err-machine-unreachable mid = in AVM.Context:620
else failure (err-machine-unreachable mid) in AVM.Interpreter:1182

`err-tx-conflict`

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

Other (3)

pattern err-tx-conflict tid = in AVM.Context:585
... | false = failure (err-tx-conflict txid) in AVM.Interpreter:1055

`executeInstruction`

Defined in: executeInstruction Total references: 3

Other (3)

| executeInstruction | \[Execute full instruction set (all layers)\](#complete-instruction-set-interpr... in AVM.Interpreter:1349

`executeInstr₁`

Defined in: executeInstr₁ Total references: 3

Other (3)

| executeInstr₁ | \[Execute with transaction support\](#transactional-instruction-set-interpreter... in AVM.Interpreter:1313

`executeInstr₂`

Defined in: executeInstr₂ Total references: 3

Other (3)

| executeInstr₂ | \[Execute with pure computation support\](#extended-instruction-set-interpreter... in AVM.Interpreter:1330

`ExecutionMoved`

Defined in: ExecutionMoved Total references: 3

Other (3)

ExecutionMoved : MachineId → MachineId → EventType in AVM.Context:687
entry = makeLogEntry (ExecutionMoved mid (State.machineId st)) st in AVM.Interpreter:1180
showEventType (ExecutionMoved from to) = "ExecutionMoved(" ++ˢ showMid from ++ˢ " -> " ++ˢ showMid t... in examples.Common.Display:54

`FDError`

Defined in: FDError Total references: 3

Other (3)

### FDError in AVM.Context:448

`fetch`

Defined in: fetch Total references: 3

Other (3)

|fetch| \[Bring object replica to local machine\](#fetch) | in AVM.Instruction:449
executeMachine (fetch oid) st with lookupObjectWithMeta oid st in AVM.Interpreter:1199

`freeze`

Defined in: freeze Total references: 3

Other (3)

|freeze| \[Synchronize object replicas for strong consistency\](#freeze) | in AVM.Instruction:477
executeController (freeze oid) st with caseMaybe (State.txController st) (λ cid → just cid) nothing in AVM.Interpreter:1272

`FunctionUpdated`

Defined in: FunctionUpdated Total references: 3

Other (3)

FunctionUpdated : String → EventType in AVM.Context:695
entry = makeLogEntry (FunctionUpdated name) st in AVM.Interpreter:1148
showEventType (FunctionUpdated name) = "FunctionUpdated(" ++ˢ name ++ˢ ")" in examples.Common.Display:58

`gameWithRollback`

Defined in: gameWithRollback Total references: 3

Type Signatures (2)

gameWithRollback : AVMProgram GameState in examples.Battleship.Game:114

Other (1)

runExample "Game with Transaction Rollback" showGameState Game.gameWithRollback in examples.Battleship.Runner:123

`get`

Defined in: get Total references: 3

Other (3)

hiding (Input; Output; Message; getState; setState) in Background.StatelessObjects:362

`getCurrentController`

Defined in: getCurrentController Total references: 3

Other (3)

|getCurrentController| \[Return current controller ID\](#getcurrentcontroller) | in AVM.Instruction:468
executeController getCurrentController st = in AVM.Interpreter:1223

`getCurrentMachine`

Defined in: getCurrentMachine Total references: 3

Other (3)

|getCurrentMachine| \[Return current physical machine ID\](#getcurrentmachine) | in AVM.Instruction:207
ThegetCurrentMachineinstruction retrieves the physical machine identifier in AVM.Interpreter:891

`getMachine`

Defined in: getMachine Total references: 3

Other (3)

|getMachine| \[Query physical machine location of object\](#getmachine) | in AVM.Instruction:440
executeMachine (getMachine oid) st with lookupPendingCreate oid st in AVM.Interpreter:1162

`Hash`

Defined in: Hash Total references: 3

Type Signatures (3)

Hash : Set in AVM.Context:225

`inCreates`

Defined in: inCreates Total references: 3

Type Signatures (3)

inCreates : ObjectId → List RuntimeObjectWithId → Bool in AVM.Interpreter:510

`initialState`

Defined in: initialState Total references: 3

Other (3)

open import examples.RunnerUtilities hiding (initialState) in examples.PingPong.Runner:160

`initMeta`

Defined in: initMeta Total references: 3

Other (3)

| initMeta | \[Create initial metadata for new object\](#metadata-initialization-and-obser... in AVM.Interpreter:332

`IntrospectError`

Defined in: IntrospectError Total references: 3

Type Signatures (3)

data IntrospectError : Set where in AVM.Context:345

`kudosTransfer`

Defined in: kudosTransfer Total references: 3

Type Signatures (3)

kudosTransfer : ObjectId → ObjectId → ℕ → AVMProgram Val in Background.StatelessObjects:126

`lookupPendingTransfer`

Defined in: lookupPendingTransfer Total references: 3

Other (3)

| lookupPendingTransfer | \[Query pending ownership transfers\](#object-and-metadata-retrieval-operati... in AVM.Interpreter:249

`lookupState`

Defined in: lookupState Total references: 3

Type Signatures (3)

lookupState : ObjectId → State → Maybe (List Val) in AVM.Interpreter:277

`matchDeep`

Defined in: matchDeep Total references: 3

Other (3)

let results = filterMap matchDeep (allObjectIds st) in AVM.Interpreter:962

`matchMeta`

Defined in: matchMeta Total references: 3

Other (3)

let results = filterMap matchMeta (allObjectIds st) in AVM.Interpreter:948

`MessageReceived`

Defined in: MessageReceived Total references: 3

Other (3)

MessageReceived : ObjectId → Input → EventType in AVM.Context:683
entry = makeLogEntry (MessageReceived (State.self st) currentInput) st in AVM.Interpreter:864
showEventType (MessageReceived oid inp) = "MessageReceived(" ++ˢ showOid oid ++ˢ ", " ++ˢ showVal in... in examples.Common.Display:52

`MetaStore`

Defined in: MetaStore Total references: 3

Other (3)

### MetaStore in AVM.Context:134

`mkFunctionEntry`

Defined in: mkFunctionEntry Total references: 3

Other (3)

constructor mkFunctionEntry in AVM.Context:230
entry = mkFunctionEntry f 0 hash in AVM.Interpreter:1125

`mkNextMsg`

Defined in: mkNextMsg Total references: 3

Type Signatures (3)

mkNextMsg : MessageType → PP.PingPongMsg → PP.ObjectId → PP.Val in examples.PingPong.Runner:93

`moveObject`

Defined in: moveObject Total references: 3

Other (3)

|moveObject| \[Move object data to another machine\](#moveobject) | in AVM.Instruction:446
executeMachine (moveObject oid targetMid) st with lookupObjectWithMeta oid st in AVM.Interpreter:1189

`NodeId`

Defined in: NodeId Total references: 3

Type Signatures (3)

NodeId : Set in examples.PingPong.Main:24

`NondetConstraint`

Defined in: NondetConstraint Total references: 3

Other (3)

Nondeterministic constraints (NondetConstraint) differ from finite domain in AVM.Instruction:619

`NondetError`

Defined in: NondetError Total references: 3

Other (3)

### NondetError in AVM.Context:457

`noPureFunctions`

Defined in: noPureFunctions Total references: 3

Type Signatures (3)

noPureFunctions : PureFunctions in examples.Common.StateInit:45

`ObjectBehaviour`

Defined in: ObjectBehaviour Total references: 3

Other (3)

We define ObjectBehaviour as the type for object behaviours, which will be in examples.PingPong.Main:80

`ObjectCreated`

Defined in: ObjectCreated Total references: 3

Other (3)

ObjectCreated : ObjectId → String → EventType in AVM.Context:678
entry = makeLogEntry (ObjectCreated oid behaviorName) st in AVM.Interpreter:445
showEventType (ObjectCreated oid behaviorName) = "ObjectCreated(" ++ˢ showOid oid ++ˢ ", \"" ++ˢ beh... in examples.Common.Display:47

`ObjectFetched`

Defined in: ObjectFetched Total references: 3

Other (3)

ObjectFetched : ObjectId → MachineId → EventType in AVM.Context:688
entry = makeLogEntry (ObjectFetched oid localMid) st in AVM.Interpreter:1208
showEventType (ObjectFetched oid mid) = "ObjectFetched(" ++ˢ showOid oid ++ˢ ", " ++ˢ showMid mid ++... in examples.Common.Display:55

`ObjectMoved`

Defined in: ObjectMoved Total references: 3

Other (3)

ObjectMoved : ObjectId → MachineId → MachineId → EventType in AVM.Context:686
entry = makeLogEntry (ObjectMoved oid (ObjectMeta.machine meta) targetMid) st in AVM.Interpreter:1195
showEventType (ObjectMoved oid from to) = "ObjectMoved(" ++ˢ showOid oid ++ˢ ", " ++ˢ showMid from +... in examples.Common.Display:53

`ObjectStore`

Defined in: ObjectStore Total references: 3

Other (3)

### ObjectStore in AVM.Context:127

`ok`

Defined in: ok Total references: 3

Other (3)

ok? : Val → Bool in Background.StatelessObjects:474

`pingBehaviorImpl`

Defined in: pingBehaviorImpl Total references: 3

Type Signatures (3)

pingBehaviorImpl : AVMProgram (List PP.Val) in examples.PingPong.Runner:112

`player2Attack`

Defined in: player2Attack Total references: 3

Other (3)

player2Attack = attack in examples.Battleship.Game:82

`playFullGame`

Defined in: playFullGame Total references: 3

Type Signatures (2)

playFullGame : AVMProgram GameState in examples.Battleship.Game:90

Other (1)

runExample "Full Game with Two Players" showGameState Game.playFullGame in examples.Battleship.Runner:121

`playGameWithPlayerType`

Defined in: playGameWithPlayerType Total references: 3

Type Signatures (2)

playGameWithPlayerType : AVMProgram GameState in examples.Battleship.Game:134

Other (1)

runExample "Game with Player Types" showGameState Game.playGameWithPlayerType in examples.Battleship.Runner:122

`pongBehaviorImpl`

Defined in: pongBehaviorImpl Total references: 3

Type Signatures (3)

pongBehaviorImpl : AVMProgram (List PP.Val) in examples.PingPong.Runner:116

`prefix-def`

Defined in: prefix-def Total references: 3

Other (3)

prefix-def in Background.Objects:466

`put`

Defined in: put Total references: 3

Other (3)

using (Object; Input; Output; InputSequence; mkObjType) in Background.StatelessObjects:360

`put-event`

Defined in: put-event Total references: 3

Other (3)

put-event : Key → Val → KVEvent in Background.StatelessObjects:369

`reflect`

Defined in: reflect Total references: 3

Other (3)

|reflect| \[Retrieve object metadata (unsafe)\](#reflect-unsafe) | in AVM.Instruction:228
| executeReflect | \[Interpret reflection instructions\](#reflection-operations) ... in AVM.Interpreter:938

`registerPure`

Defined in: registerPure Total references: 3

Other (3)

|registerPure| \[Register new pure function (unsafe)\](#registerpure-unsafe) | in AVM.Instruction:394
executePure (registerPure name f) st in AVM.Interpreter:1119

`reifyConstraints`

Defined in: reifyConstraints Total references: 3

Other (3)

|reifyConstraints| \[Capture constraint store as data (unsafe)\](#reifyconstraints-unsafe) | in AVM.Instruction:318
ThereifyConstraintsinstruction captures the constraint solver's internal in AVM.Interpreter:1014

`reifyContext`

Defined in: reifyContext Total references: 3

Other (3)

|reifyContext| \[Capture current execution context as data\](#reifycontext) | in AVM.Instruction:312
ThereifyContextinstruction captures the current execution frame as a in AVM.Interpreter:983

`reifyTxState`

Defined in: reifyTxState Total references: 3

Other (3)

|reifyTxState| \[Capture transaction state as data (unsafe)\](#reifytxstate-unsafe) | in AVM.Instruction:315
ThereifyTxStateinstruction captures the current transaction's pending state in AVM.Interpreter:997

`removePendingCreate`

Defined in: removePendingCreate Total references: 3

Other (3)

| removePendingCreate | \[Cancel staged object creation\](#transactional-overlay-management) ... in AVM.Interpreter:389

`scryDeep`

Defined in: scryDeep Total references: 3

Other (3)

|scryDeep| \[Query objects by internals and metadata (unsafe)\](#scrydeep-unsafe) | in AVM.Instruction:234
executeReflect (scryDeep pred) st = in AVM.Interpreter:961

`scryMeta`

Defined in: scryMeta Total references: 3

Other (3)

|scryMeta| \[Query objects by metadata predicate (unsafe)\](#scrymeta-unsafe) | in AVM.Instruction:230
executeReflect (scryMeta pred) st = in AVM.Interpreter:947

`sender`

Defined in: sender Total references: 3

Other (3)

|sender| \[Return calling object's ID\](#sender) | in AVM.Instruction:210
; sender = just (State.self st) in AVM.Interpreter:924

`showError`

Defined in: showError Total references: 3

Type Signatures (3)

showError : AVMError → String in examples.Common.Display:98

`showLogEntry`

Defined in: showLogEntry Total references: 3

Type Signatures (3)

showLogEntry : LogEntry → String in examples.Common.Display:72

`showOid`

Defined in: showOid Total references: 3

Type Signatures (3)

showOid : PP.ObjectId → String in examples.PingPong.Runner:19

`startPingPong`

Defined in: startPingPong Total references: 3

Type Signatures (3)

startPingPong : ℕ → AVMProgram Val in examples.PingPong.Main:103

`StateStore`

Defined in: StateStore Total references: 3

Other (3)

StateStore, not in metadata. in AVM.Context:145

`Store`

Defined in: Store Total references: 3

Other (3)

StateStore, not in metadata. in AVM.Context:172
## Store Initialization in examples.Common.StateInit:34

`Success`

Defined in: Success Total references: 3

Other (3)

### Success Record in AVM.Context:738

`teleport`

Defined in: teleport Total references: 3

Other (3)

|teleport| \[Move execution context to another machine\](#teleport) | in AVM.Instruction:443
Execution teleportation performs computational migration to a different physical in AVM.Interpreter:1175

`test`

Defined in: test Total references: 3

Type Signatures (3)

testSimple : AVMProgram PP.Val in examples.PingPong.Runner:176

`testHit`

Defined in: testHit Total references: 3

Type Signatures (3)

testHit : AVMProgram (Maybe PB.Val) in examples.Battleship.Runner:95

`testMiss`

Defined in: testMiss Total references: 3

Type Signatures (3)

testMiss : AVMProgram (Maybe PB.Val) in examples.Battleship.Runner:101

`testSimple`

Defined in: testSimple Total references: 3

Type Signatures (3)

testSimple : AVMProgram PP.Val in examples.PingPong.Runner:167

`TransactionAborted`

Defined in: TransactionAborted Total references: 3

Other (3)

TransactionAborted : TxId → EventType in AVM.Context:700
entry = makeLogEntry (TransactionAborted txid) st in AVM.Interpreter:1095
showEventType (TransactionAborted txid) = "TransactionAborted(" ++ˢ showTxId txid ++ˢ ")" in examples.Common.Display:61

`TransactionCommitted`

Defined in: TransactionCommitted Total references: 3

Other (3)

TransactionCommitted : TxId → EventType in AVM.Context:699
entry = makeLogEntry (TransactionCommitted txid) st in AVM.Interpreter:1075
showEventType (TransactionCommitted txid) = "TransactionCommitted(" ++ˢ showTxId txid ++ˢ ")" in examples.Common.Display:60

`TransactionStarted`

Defined in: TransactionStarted Total references: 3

Other (3)

TransactionStarted : TxId → EventType in AVM.Context:698
entry = makeLogEntry (TransactionStarted txid) st in AVM.Interpreter:1037
showEventType (TransactionStarted txid) = "TransactionStarted(" ++ˢ showTxId txid ++ˢ ")" in examples.Common.Display:59

`transferObject`

Defined in: transferObject Total references: 3

Other (3)

|transferObject| \[Transfer object ownership to another controller\](#transferobject) | in AVM.Instruction:472
executeController (transferObject oid targetCid) st in AVM.Interpreter:1252

`transferObjInTx`

Defined in: transferObjInTx Total references: 3

Type Signatures (3)

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

`transferObjNoTx`

Defined in: transferObjNoTx Total references: 3

Type Signatures (3)

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

`tx-commit`

Defined in: tx-commit Total references: 3

Other (3)

pattern tx-commit tid = Tx (commitTx tid) in AVM.Instruction:723
trigger (tx-commit setupTx) >>= λ _ → in examples.Battleship.Game:54

`TxWrite`

Defined in: TxWrite Total references: 3

Other (3)

### TxWrite in AVM.Context:207

`updateHelper`

Defined in: updateHelper Total references: 3

Other (3)

helper (VInt n) = updateHelper n in Background.StatelessObjects:208

`updatePure`

Defined in: updatePure Total references: 3

Other (3)

|updatePure| \[Update existing pure function definition\](#updatepure) | in AVM.Instruction:397
executePure (updatePure name fn) st in AVM.Interpreter:1137

`validateObserved`

Defined in: validateObserved Total references: 3

Other (3)

| validateObserved | \[Verify all observed objects exist\](#read-set-tracking-and-validation) |... in AVM.Interpreter:527

`withCreateTxBranch`

Defined in: withCreateTxBranch Total references: 3

Type Signatures (3)

withCreateTxBranch : String → Maybe ControllerId → State → AVMResult ObjectId in AVM.Interpreter:439

`withdrawMsg`

Defined in: withdrawMsg Total references: 3

Other (3)

withdrawMsg : ℕ → AccountMsg in Background.StatelessObjects:443

`withTxBranch`

Defined in: withTxBranch Total references: 3

Type Signatures (3)

withTxBranch : ∀ {A} → in AVM.Interpreter:425

`φ-counter`

Defined in: φ-counter Total references: 3

Type Signatures (3)

φ-counter : List CounterMsg → Maybe ℕ in Background.StatelessObjects:334

`≈φ-refl`

Defined in: ≈φ-refl Total references: 3

Type Signatures (3)

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

`≈φ-sym`

Defined in: ≈φ-sym Total references: 3

Type Signatures (3)

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

`≈φ-trans`

Defined in: ≈φ-trans Total references: 3

Type Signatures (3)

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

`_>>_`

Defined in: _>>_ Total references: 2

Type Signatures (1)

_>>_ : {A B : Set} → PrimIO A → PrimIO B → PrimIO B in examples.RunnerUtilities:27

Other (1)

open import Background.InteractionTrees hiding (_>>=_) in examples.RunnerUtilities:28

`balance-val`

Defined in: balance-val Total references: 2

Other (2)

balance-val : ℕ → AccountOutput in Background.StatelessObjects:476

`BaseResult`

Defined in: BaseResult Total references: 2

Type Signatures (2)

BaseResult : Set → Set in AVM.Context:766

`behavioural-state-equiv`

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

Other (2)

behavioural-state-equiv in Background.Objects:424

`BehaviouralState`

Defined in: BehaviouralState Total references: 2

Type Signatures (2)

BehaviouralState : Object → InputSequence → Set in Background.Objects:234

`closeAccount`

Defined in: closeAccount Total references: 2

Type Signatures (2)

closeAccount : ObjectId → ObjectId → AVMProgram Val in Background.StatelessObjects:264

`Controller`

Defined in: Controller Total references: 2

Other (2)

| **Controller layer** | | in AVM.Instruction:682
| executeController | \[Interpret controller authority instructions\](#logical-authority-and-owner... in AVM.Interpreter:1359

`counter-object`

Defined in: counter-object Total references: 2

Type Signatures (2)

counter-object : SequentialObject in Background.Objects:671

`counterExample`

Defined in: counterExample Total references: 2

Type Signatures (2)

counterExample : AVMProgram Val in Background.StatelessObjects:179

`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 Background.StatelessObjects:317

`echo-type`

Defined in: echo-type Total references: 2

Type Signatures (2)

echo-type : Object in Background.Objects:497

`eqNat`

Defined in: eqNat Total references: 2

Type Signatures (2)

eqNat : ℕ → ℕ → Bool in examples.Common.Equality:32

`equiv-preserved`

Defined in: equiv-preserved Total references: 2

Other (2)

equiv-preserved in Background.Objects:701

`err-fd-not-implemented`

Defined in: err-fd-not-implemented Total references: 2

Other (2)

pattern err-fd-not-implemented msg = in AVM.Context:658
... | FD instr = failure (err-fd-not-implemented "FD instructions not yet implemented") in AVM.Interpreter:1360

`err-function-not-found`

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

Other (2)

pattern err-function-not-found name = in AVM.Context:607
... | nothing = failure (err-function-not-found name) in AVM.Interpreter:1139

`err-function-registered`

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

Other (2)

pattern err-function-registered name = in AVM.Context:610
... | just _ = failure (err-function-registered name) in AVM.Interpreter:1121

`err-invalid-during-tx`

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

Other (2)

pattern err-invalid-during-tx msg = in AVM.Context:600
... | just _ = failure (err-invalid-during-tx "teleport") in AVM.Interpreter:1176

`err-no-active-tx`

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

Other (2)

pattern err-no-active-tx = in AVM.Context:597
... | nothing = failure err-no-active-tx in AVM.Interpreter:1052

`err-nondet-not-implemented`

Defined in: err-nondet-not-implemented Total references: 2

Other (2)

pattern err-nondet-not-implemented msg = in AVM.Context:661
... | Nondet instr = failure (err-nondet-not-implemented "Nondeterminism instructions not yet imple... in AVM.Interpreter:1361

`ErrConstraintStoreUnavailable`

Defined in: ErrConstraintStoreUnavailable Total references: 2

Other (2)

ErrConstraintStoreUnavailable : ReifyError in AVM.Context:385

`ErrContextUnavailable`

Defined in: ErrContextUnavailable Total references: 2

Other (2)

ErrContextUnavailable : String → IntrospectError in AVM.Context:347

`ErrControllerUnreachable`

Defined in: ErrControllerUnreachable Total references: 2

Other (2)

ErrControllerUnreachable : ControllerId → ControllerError in AVM.Context:422

`ErrCrossControllerTx`

Defined in: ErrCrossControllerTx Total references: 2

Other (2)

ErrCrossControllerTx : ObjectId → ControllerId → ControllerError in AVM.Context:424

`ErrFreezeFailed`

Defined in: ErrFreezeFailed Total references: 2

Other (2)

ErrFreezeFailed : ObjectId → ControllerError in AVM.Context:427

`ErrFunctionAlreadyRegistered`

Defined in: ErrFunctionAlreadyRegistered Total references: 2

Other (2)

ErrFunctionAlreadyRegistered : String → PureError in AVM.Context:439

`ErrFunctionNotFound`

Defined in: ErrFunctionNotFound Total references: 2

Other (2)

ErrFunctionNotFound : String → PureError in AVM.Context:438

`ErrInvalidDuringTx`

Defined in: ErrInvalidDuringTx Total references: 2

Other (2)

ErrInvalidDuringTx : String → TxError in AVM.Context:400

`ErrInvalidInput`

Defined in: ErrInvalidInput Total references: 2

Other (2)

ErrInvalidInput : ObjectId → Input → ObjError in AVM.Context:333

`ErrInvalidMachineTransfer`

Defined in: ErrInvalidMachineTransfer Total references: 2

Other (2)

ErrInvalidMachineTransfer : ObjectId → MachineId → MachineError in AVM.Context:411

`ErrMachineUnreachable`

Defined in: ErrMachineUnreachable Total references: 2

Other (2)

ErrMachineUnreachable : MachineId → MachineError in AVM.Context:410

`ErrMetadataCorruption`

Defined in: ErrMetadataCorruption Total references: 2

Other (2)

ErrMetadataCorruption : ObjectId → ObjError in AVM.Context:335

`ErrMetadataInconsistent`

Defined in: ErrMetadataInconsistent Total references: 2

Other (2)

ErrMetadataInconsistent : ObjectId → String → ReflectError in AVM.Context:360

`ErrMetadataNotFound`

Defined in: ErrMetadataNotFound Total references: 2

Other (2)

ErrMetadataNotFound : ObjectId → ReflectError in AVM.Context:359

`ErrNoActiveTx`

Defined in: ErrNoActiveTx Total references: 2

Other (2)

ErrNoActiveTx : TxError in AVM.Context:399

`ErrNoTransactionToReify`

Defined in: ErrNoTransactionToReify Total references: 2

Other (2)

ErrNoTransactionToReify : ReifyError in AVM.Context:381

`ErrObjectAlreadyDestroyed`

Defined in: ErrObjectAlreadyDestroyed Total references: 2

Other (2)

ErrObjectAlreadyDestroyed : ObjectId → ObjError in AVM.Context:331

`ErrObjectAlreadyExists`

Defined in: ErrObjectAlreadyExists Total references: 2

Other (2)

ErrObjectAlreadyExists : ObjectId → ObjError in AVM.Context:332

`ErrObjectHasNoController`

Defined in: ErrObjectHasNoController Total references: 2

Other (2)

ErrObjectHasNoController : ObjectId → ControllerError in AVM.Context:428

`ErrObjectNotAvailable`

Defined in: ErrObjectNotAvailable Total references: 2

Other (2)

ErrObjectNotAvailable : ObjectId → ControllerError in AVM.Context:425

`ErrObjectNotConsistent`

Defined in: ErrObjectNotConsistent Total references: 2

Other (2)

ErrObjectNotConsistent : ObjectId → ControllerError in AVM.Context:426

`ErrObjectNotFound`

Defined in: ErrObjectNotFound Total references: 2

Other (2)

ErrObjectNotFound : ObjectId → ObjError in AVM.Context:330

`ErrObjectRejectedCall`

Defined in: ErrObjectRejectedCall Total references: 2

Other (2)

ErrObjectRejectedCall : ObjectId → Input → ObjError in AVM.Context:334

`ErrorOccurred`

Defined in: ErrorOccurred Total references: 2

Other (2)

ErrorOccurred : AVMError → EventType in AVM.Context:703
showEventType (ErrorOccurred err) = "ErrorOccurred(...)" in examples.Common.Display:62

`ErrReflectionDenied`

Defined in: ErrReflectionDenied Total references: 2

Other (2)

ErrReflectionDenied : ObjectId → ReflectError in AVM.Context:367

`ErrReifyContextFailed`

Defined in: ErrReifyContextFailed Total references: 2

Other (2)

ErrReifyContextFailed : String → ReifyError in AVM.Context:378

`ErrScryPredicateFailed`

Defined in: ErrScryPredicateFailed Total references: 2

Other (2)

ErrScryPredicateFailed : String → ReflectError in AVM.Context:364

`ErrStoreCorruption`

Defined in: ErrStoreCorruption Total references: 2

Other (2)

ErrStoreCorruption : String → ReflectError in AVM.Context:363

`ErrTeleportDuringTx`

Defined in: ErrTeleportDuringTx Total references: 2

Other (2)

ErrTeleportDuringTx : MachineError in AVM.Context:412

`ErrTxAlreadyAborted`

Defined in: ErrTxAlreadyAborted Total references: 2

Other (2)

ErrTxAlreadyAborted : TxId → TxError in AVM.Context:398

`ErrTxAlreadyCommitted`

Defined in: ErrTxAlreadyCommitted Total references: 2

Other (2)

ErrTxAlreadyCommitted : TxId → TxError in AVM.Context:397

`ErrTxConflict`

Defined in: ErrTxConflict Total references: 2

Other (2)

ErrTxConflict : TxId → TxError in AVM.Context:395

`ErrTxNotFound`

Defined in: ErrTxNotFound Total references: 2

Other (2)

ErrTxNotFound : TxId → TxError in AVM.Context:396

`ErrTxStateAccessDenied`

Defined in: ErrTxStateAccessDenied Total references: 2

Other (2)

ErrTxStateAccessDenied : ReifyError in AVM.Context:382

`ErrUnauthorizedTransfer`

Defined in: ErrUnauthorizedTransfer Total references: 2

Other (2)

ErrUnauthorizedTransfer : ObjectId → ControllerId → ControllerError in AVM.Context:423

`ErrVersionConflict`

Defined in: ErrVersionConflict Total references: 2

Other (2)

ErrVersionConflict : String → ℕ → ℕ → PureError -- name, expected version, actual version in AVM.Context:440

`execute-step`

Defined in: execute-step Total references: 2

Other (2)

execute-step in Background.Objects:779

`FD`

Defined in: FD Total references: 2

Other (2)

| **FD constraint layer** | | in AVM.Instruction:683
state. Currently returns an empty constraint store as FD instructions are not in AVM.Interpreter:1360

`fd-error`

Defined in: fd-error Total references: 2

Other (2)

fd-error : FDError → AVMError in AVM.Context:509

`FinSet`

Defined in: FinSet Total references: 2

Type Signatures (2)

FinSet : Set → Set in Background.BasicTypes:637

`freshId`

Defined in: freshId Total references: 2

Type Signatures (2)

freshId : String → ℕ → (String × String) in examples.RunnerUtilities:45

`fst`

Defined in: fst Total references: 2

Type Signatures (2)

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

`FunctionEntry`

Defined in: FunctionEntry Total references: 2

Other (2)

record FunctionEntry : Set where in AVM.Context:229

`Impl`

Defined in: Impl Total references: 2

Type Signatures (2)

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

`inc`

Defined in: inc Total references: 2

Other (2)

-- Define Message as alias for Val (since Instruction's Message is hidden) in Background.StatelessObjects:316

`inDestroys`

Defined in: inDestroys Total references: 2

Type Signatures (2)

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

`initial-output`

Defined in: initial-output Total references: 2

Type Signatures (2)

initial-output : Output in Background.Objects:658

`inl`

Defined in: inl Total references: 2

Other (2)

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

`Input`

Defined in: Input Total references: 2

Type Signatures (2)

Input : Set in examples.PingPong.Main:66

`inr`

Defined in: inr Total references: 2

Other (2)

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

`Interface`

Defined in: Interface Total references: 2

Type Signatures (2)

Interface : Set₁ in Background.InteractionTrees:34

`introspect-error`

Defined in: introspect-error Total references: 2

Other (2)

introspect-error : IntrospectError → BaseError in AVM.Context:474

`ITree-Monad`

Defined in: ITree-Monad Total references: 2

Type Signatures (2)

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

`Machine`

Defined in: Machine Total references: 2

Other (2)

|getCurrentMachine| \[Return current physical machine ID\](#getcurrentmachine) | in AVM.Instruction:681
| executeMachine | \[Interpret machine distribution instructions\](#physical-distribution-opera... in AVM.Interpreter:1358

`main`

Defined in: main Total references: 2

Other (2)

-- A more complete implementation would maintain a global registry in examples.PingPong.Runner:196

`Message`

Defined in: Message Total references: 2

Type Signatures (2)

data MessageType : Set where in examples.PingPong.Main:72

`mkLogEntry`

Defined in: mkLogEntry Total references: 2

Other (2)

constructor mkLogEntry in AVM.Context:710
mkLogEntry (State.eventCounter st) eventType (State.txController st) in AVM.Interpreter:343

`mkMeta`

Defined in: mkMeta Total references: 2

Other (2)

constructor mkMeta in AVM.Context:102
initMeta oid mid mcid = mkMeta oid mid mcid mcid in AVM.Interpreter:333

`mkReifiedConstraints`

Defined in: mkReifiedConstraints Total references: 2

Other (2)

constructor mkReifiedConstraints in AVM.Instruction:301
let constraints = mkReifiedConstraints \[\] 0 in AVM.Interpreter:1015

`mkReifiedContext`

Defined in: mkReifiedContext Total references: 2

Other (2)

constructor mkReifiedContext in AVM.Instruction:275
let ctx = mkReifiedContext in AVM.Interpreter:984

`mkReifiedTxState`

Defined in: mkReifiedTxState Total references: 2

Other (2)

constructor mkReifiedTxState in AVM.Instruction:288
let txState = mkReifiedTxState in AVM.Interpreter:1000

`mkState`

Defined in: mkState Total references: 2

Other (2)

constructor mkState in examples.RunnerUtilities:63

`mkStore`

Defined in: mkStore Total references: 2

Other (2)

constructor mkStore in AVM.Context:173
emptyStore = mkStore (λ _ → nothing) (λ _ → nothing) (λ _ → nothing) in examples.Common.StateInit:35

`mkSuccessWithEvent`

Defined in: mkSuccessWithEvent Total references: 2

Type Signatures (2)

mkSuccessWithEvent : ∀ {A} → A → State → EventType → AVMResult A in AVM.Interpreter:477

`mkSuccessWithLog`

Defined in: mkSuccessWithLog Total references: 2

Type Signatures (2)

mkSuccessWithLog : ∀ {A} → A → State → LogEntry → AVMResult A in AVM.Interpreter:469

`Nondet`

Defined in: Nondet Total references: 2

Other (2)

| **Nondeterminism layer** | | in AVM.Instruction:684
... | Nondet instr = failure (err-nondet-not-implemented "Nondeterminism instructions not yet imple... in AVM.Interpreter:1361

`nondet-error`

Defined in: nondet-error Total references: 2

Other (2)

nondet-error : NondetError → AVMError in AVM.Context:510

`objecttype-to-behaviour`

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

Type Signatures (2)

objecttype-to-behaviour : Object → ObjectBehaviour InputSequence in Background.Objects:794

`Output`

Defined in: Output Total references: 2

Type Signatures (2)

Output : Set in examples.PingPong.Main:69

`output`

Defined in: output Total references: 2

Other (2)

-- inputs and outputs have different structures. in Background.Objects:267

`output-of`

Defined in: output-of Total references: 2

Other (2)

output-of in Background.Objects:147

`pendingInputsFor`

Defined in: pendingInputsFor Total references: 2

Other (2)

| pendingInputsFor | \[Collect pending inputs for object\](#transaction-log-query-operations) ... in AVM.Interpreter:358

`pingPongExample`

Defined in: pingPongExample Total references: 2

Type Signatures (2)

pingPongExample : AVMProgram Val in examples.PingPong.Main:118

`process-preserves-wf`

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

Other (2)

process-preserves-wf in Background.Objects:684

`Pure`

Defined in: Pure Total references: 2

Other (2)

| **Pure function layer** | | in AVM.Instruction:680
| executePure | \[Interpret pure function instructions\](#pure-computation-operations) ... in AVM.Interpreter:1357

`PureResult`

Defined in: PureResult Total references: 2

Type Signatures (2)

PureResult : Set → Set in AVM.Context:772

`RawMonad`

Defined in: RawMonad Total references: 2

Other (2)

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

`reachable-from`

Defined in: reachable-from Total references: 2

Type Signatures (2)

reachable-from : SequentialObject → InputSequence → Set in Background.Objects:635

`Reflect`

Defined in: Reflect Total references: 2

Other (2)

| **Reflection layer** | | in AVM.Instruction:677
| executeReflect | \[Interpret reflection instructions\](#reflection-operations) ... in AVM.Interpreter:1354

`ReifiedConstraints`

Defined in: ReifiedConstraints Total references: 2

Other (2)

record ReifiedConstraints : Set where in AVM.Instruction:300

`ReifiedContext`

Defined in: ReifiedContext Total references: 2

Other (2)

record ReifiedContext : Set where in AVM.Instruction:274

`ReifiedTxState`

Defined in: ReifiedTxState Total references: 2

Other (2)

record ReifiedTxState : Set where in AVM.Instruction:287

`Reify`

Defined in: Reify Total references: 2

Other (2)

#### ReifyInstruction Datatype in AVM.Instruction:678
| executeReify | \[Interpret reification instructions\](#reification-operations) ... in AVM.Interpreter:1355

`RunnerState`

Defined in: RunnerState Total references: 2

Other (2)

record RunnerState (ObjMeta : Set) : Set where in examples.RunnerUtilities:62

`showOID`

Defined in: showOID Total references: 2

Type Signatures (2)

showOID : {NodeId : Set} → (NodeId × String) → String in examples.RunnerUtilities:48

`snd`

Defined in: snd Total references: 2

Type Signatures (2)

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

`step-account`

Defined in: step-account Total references: 2

Type Signatures (2)

step-account : List AccountMsg → AccountMsg → Maybe (AccountOutput × List AccountMsg) in Background.StatelessObjects:495

`step-counter`

Defined in: step-counter Total references: 2

Type Signatures (2)

step-counter : List CounterMsg → CounterMsg → Maybe (ℕ × List CounterMsg) in Background.StatelessObjects:341

`step-kv`

Defined in: step-kv Total references: 2

Type Signatures (2)

step-kv : List KVMsg → KVMsg → Maybe (Val × List KVMsg) in Background.StatelessObjects:426

`transferBatch`

Defined in: transferBatch Total references: 2

Type Signatures (2)

transferBatch : List (ObjectId × ObjectId × ℕ) → AVMProgram Val in Background.StatelessObjects:242

`transition`

Defined in: transition Total references: 2

Other (2)

model object behaviour and state transitions. The object model is also close to in Background.Objects:588

`transition-preserves-type`

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

Other (2)

transition-preserves-type in Background.Objects:622

`tx-abort`

Defined in: tx-abort Total references: 2

Other (2)

pattern tx-abort tid = Tx (abortTx tid) in AVM.Instruction:724
trigger (tx-abort badTurn) >>= λ _ → in examples.Battleship.Game:121

`TxResult`

Defined in: TxResult Total references: 2

Type Signatures (2)

TxResult : Set → Set in AVM.Context:769

`updateBalance`

Defined in: updateBalance Total references: 2

Type Signatures (2)

updateBalance : ObjectId → Val → AVMProgram Val in Background.StatelessObjects:201

`VInt`

Defined in: VInt Total references: 2

Other (2)

VInt : ℕ → Val in examples.PingPong.Main:45
showValAgda (PP.VInt n) = "(VInt " ++ˢ showNat n ++ˢ ")" in examples.PingPong.Runner:24

`wfObjType`

Defined in: wfObjType Total references: 2

Other (2)

constructor wfObjType in Background.Objects:163

`∃`

Defined in: ∃ Total references: 2

Type Signatures (2)

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

`≈ˢ-refl`

Defined in: ≈ˢ-refl Total references: 2

Type Signatures (2)

≈ˢ-refl : (obj : SequentialObject) → obj ≈ˢ obj in Background.Objects:380

`≈ˢ-sym`

Defined in: ≈ˢ-sym Total references: 2

Type Signatures (2)

≈ˢ-sym : (obj₁ obj₂ : SequentialObject) → in Background.Objects:389

`≈ˢ-trans`

Defined in: ≈ˢ-trans Total references: 2

Other (2)

≈ˢ-trans in Background.Objects:403

`≈ᵒ-refl`

Defined in: ≈ᵒ-refl Total references: 2

Type Signatures (2)

≈ᵒ-refl : (obj : SequentialObject) → obj ≈ᵒ obj in Background.Objects:334

`≈ᵒ-sym`

Defined in: ≈ᵒ-sym Total references: 2

Type Signatures (2)

≈ᵒ-sym : (obj₁ obj₂ : SequentialObject) in Background.Objects:343

`≈ᵒ-trans`

Defined in: ≈ᵒ-trans Total references: 2

Other (2)

≈ᵒ-trans in Background.Objects:355

`_`

Defined in: _ Total references: 1

Other (1)

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

`AllDiff`

Defined in: AllDiff Total references: 1

Other (1)

AllDiff : List VarId → Constraint in AVM.Instruction:557

`Assert`

Defined in: Assert Total references: 1

Other (1)

|require| \[Assert constraint for transaction\](#nondeterminism-instructions) | in AVM.Instruction:621

`call-pure`

Defined in: call-pure Total references: 1

Other (1)

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

`choose`

Defined in: choose Total references: 1

Other (1)

|choose| \[Select value from preference distribution\](#nondeterminism-instructions) | in AVM.Instruction:626

`create`

Defined in: create Total references: 1

Other (1)

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

`destroy`

Defined in: destroy Total references: 1

Other (1)

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

`do-reify-constraints`

Defined in: do-reify-constraints Total references: 1

Other (1)

pattern do-reify-constraints = Reify reifyConstraints in AVM.Instruction:719

`do-reify-context`

Defined in: do-reify-context Total references: 1

Other (1)

pattern do-reify-context = Reify reifyContext in AVM.Instruction:717

`do-reify-tx-state`

Defined in: do-reify-tx-state Total references: 1

Other (1)

pattern do-reify-tx-state = Reify reifyTxState in AVM.Instruction:718

`do-teleport`

Defined in: do-teleport Total references: 1

Other (1)

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

`Env`

Defined in: Env Total references: 1

Other (1)

record Env (ObjectId : Set) : Set where in examples.RunnerUtilities:75

`Eq`

Defined in: Eq Total references: 1

Other (1)

-- Equality: var₁ = var₂ in AVM.Instruction:538

`err-constraint-store-unavailable`

Defined in: err-constraint-store-unavailable Total references: 1

Other (1)

pattern err-constraint-store-unavailable = in AVM.Context:578

`err-context-unavailable`

Defined in: err-context-unavailable Total references: 1

Other (1)

pattern err-context-unavailable msg = in AVM.Context:543

`err-freeze-failed`

Defined in: err-freeze-failed Total references: 1

Other (1)

pattern err-freeze-failed oid = in AVM.Context:648

`err-invalid-input`

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

Other (1)

pattern err-invalid-input oid inp = in AVM.Context:530

`err-invalid-machine-transfer`

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

Other (1)

pattern err-invalid-machine-transfer oid mid = in AVM.Context:623

`err-metadata-inconsistent`

Defined in: err-metadata-inconsistent Total references: 1

Other (1)

pattern err-metadata-inconsistent oid msg = in AVM.Context:553

`err-metadata-not-found`

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

Other (1)

pattern err-metadata-not-found oid = in AVM.Context:550

`err-no-transaction-to-reify`

Defined in: err-no-transaction-to-reify Total references: 1

Other (1)

pattern err-no-transaction-to-reify = in AVM.Context:572

`err-object-destroyed`

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

Other (1)

pattern err-object-destroyed oid = in AVM.Context:524

`err-object-exists`

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

Other (1)

pattern err-object-exists oid = in AVM.Context:527

`err-object-not-available`

Defined in: err-object-not-available Total references: 1

Other (1)

pattern err-object-not-available oid = in AVM.Context:642

`err-object-not-consistent`

Defined in: err-object-not-consistent Total references: 1

Other (1)

pattern err-object-not-consistent oid = in AVM.Context:645

`err-object-rejected`

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

Other (1)

pattern err-object-rejected oid inp = in AVM.Context:533

`err-reflection-denied`

Defined in: err-reflection-denied Total references: 1

Other (1)

pattern err-reflection-denied oid = in AVM.Context:562

`err-reify-context-failed`

Defined in: err-reify-context-failed Total references: 1

Other (1)

pattern err-reify-context-failed msg = in AVM.Context:569

`err-scry-predicate-failed`

Defined in: err-scry-predicate-failed Total references: 1

Other (1)

pattern err-scry-predicate-failed msg = in AVM.Context:559

`err-store-corruption`

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

Other (1)

pattern err-store-corruption msg = in AVM.Context:556

`err-teleport-during-tx`

Defined in: err-teleport-during-tx Total references: 1

Other (1)

pattern err-teleport-during-tx = in AVM.Context:626

`err-tx-aborted`

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

Other (1)

pattern err-tx-aborted tid = in AVM.Context:594

`err-tx-committed`

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

Other (1)

pattern err-tx-committed tid = in AVM.Context:591

`err-tx-not-found`

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

Other (1)

pattern err-tx-not-found tid = in AVM.Context:588

`err-tx-state-access-denied`

Defined in: err-tx-state-access-denied Total references: 1

Other (1)

pattern err-tx-state-access-denied = in AVM.Context:575

`err-unauthorized-transfer`

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

Other (1)

pattern err-unauthorized-transfer oid cid = in AVM.Context:636

`err-version-conflict`

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

Other (1)

pattern err-version-conflict name expected actual = in AVM.Context:613

`ErrNotImplemented`

Defined in: ErrNotImplemented Total references: 1

Other (1)

ErrNotImplemented : String → FDError in AVM.Context:458

`error-insufficient`

Defined in: error-insufficient Total references: 1

Other (1)

error-insufficient : AccountOutput in Background.StatelessObjects:475

`fetch-object`

Defined in: fetch-object Total references: 1

Other (1)

pattern fetch-object oid = Machine (fetch oid) in AVM.Instruction:735

`first-definition`

Defined in: first-definition Total references: 1

Other (1)

module first-definition where in Background.InteractionTrees:64

`freeze-object`

Defined in: freeze-object Total references: 1

Other (1)

pattern freeze-object oid = Controller (freeze oid) in AVM.Instruction:741

`Geq`

Defined in: Geq Total references: 1

Other (1)

Geq : VarId → VarId → Constraint in AVM.Instruction:551

`get-controller`

Defined in: get-controller Total references: 1

Other (1)

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

`get-current-controller`

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

Other (1)

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

`get-current-machine`

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

Other (1)

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

`get-input`

Defined in: get-input Total references: 1

Other (1)

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

`get-machine`

Defined in: get-machine Total references: 1

Other (1)

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

`get-self`

Defined in: get-self Total references: 1

Other (1)

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

`get-sender`

Defined in: get-sender Total references: 1

Other (1)

pattern get-sender = Introspect sender in AVM.Instruction:709

`get-state`

Defined in: get-state Total references: 1

Other (1)

pattern get-state = Introspect getState in AVM.Instruction:707

`Gt`

Defined in: Gt Total references: 1

Other (1)

Gt : VarId → VarId → Constraint in AVM.Instruction:554

`here`

Defined in: here Total references: 1

Other (1)

module Background.BasicTypes where in Background.BasicTypes:645

`interp`

Defined in: interp Total references: 1

Other (1)

the AVM interpreter with proper termination handling. The module is in examples.Common.InterpreterSetup:57

`InterpreterImport`

Defined in: InterpreterImport Total references: 1

Other (1)

module InterpreterImport where in examples.PingPong.Runner:44

`key`

Defined in: key Total references: 1

Other (1)

key : String → Key in Background.StatelessObjects:357

`label`

Defined in: label Total references: 1

Other (1)

|label| \[Select value from variable's domain (search step)\](#label) | in AVM.Instruction:596

`Leq`

Defined in: Leq Total references: 1

Other (1)

Leq : VarId → VarId → Constraint in AVM.Instruction:545

`Lt`

Defined in: Lt Total references: 1

Other (1)

Lt : VarId → VarId → Constraint in AVM.Instruction:548

`mkEnv`

Defined in: mkEnv Total references: 1

Other (1)

constructor mkEnv in examples.RunnerUtilities:76

`mkVarId`

Defined in: mkVarId Total references: 1

Other (1)

constructor mkVarId in AVM.Instruction:519

`mk↔`

Defined in: mk↔ Total references: 1

Other (1)

constructor mk↔ in Background.BasicTypes:714

`move-object`

Defined in: move-object Total references: 1

Other (1)

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

`narrow`

Defined in: narrow Total references: 1

Other (1)

|narrow| \[Narrow variable domain by intersection\](#narrow) | in AVM.Instruction:588

`Neq`

Defined in: Neq Total references: 1

Other (1)

Neq : VarId → VarId → Constraint in AVM.Instruction:541

`newVar`

Defined in: newVar Total references: 1

Other (1)

|newVar| \[Create fresh constraint variable with finite domain\](#newvar) | in AVM.Instruction:584

`obj-destroy`

Defined in: obj-destroy Total references: 1

Other (1)

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

`obj-receive`

Defined in: obj-receive Total references: 1

Other (1)

pattern obj-receive = Obj receive in AVM.Instruction:701

`obj-reflect`

Defined in: obj-reflect Total references: 1

Other (1)

pattern obj-reflect oid = Reflect (reflect oid) in AVM.Instruction:712

`obj-scry-deep`

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

Other (1)

pattern obj-scry-deep pred = Reflect (scryDeep pred) in AVM.Instruction:714

`obj-scry-meta`

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

Other (1)

pattern obj-scry-meta pred = Reflect (scryMeta pred) in AVM.Instruction:713

`post`

Defined in: post Total references: 1

Other (1)

|post| \[Post relational constraint to constraint store\](#post) | in AVM.Instruction:592

`pure-update-pure`

Defined in: pure-update-pure Total references: 1

Other (1)

pattern pure-update-pure name fn = Pure (updatePure name fn) in AVM.Instruction:729

`receive`

Defined in: receive Total references: 1

Other (1)

receive : MessageEvent String in Background.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:728

`require`

Defined in: require Total references: 1

Other (1)

|require| \[Assert constraint for transaction\](#nondeterminism-instructions) | in AVM.Instruction:630

`ret-eq`

Defined in: ret-eq Total references: 1

Other (1)

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

`RunnerInterpreter`

Defined in: RunnerInterpreter Total references: 1

Other (1)

module RunnerInterpreter in examples.Common.InterpreterSetup:47

`send`

Defined in: send Total references: 1

Other (1)

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

`set-state`

Defined in: set-state Total references: 1

Other (1)

pattern set-state newState = Introspect (setState newState) in AVM.Instruction:708

`step-trans`

Defined in: step-trans Total references: 1

Other (1)

step-trans in Background.Objects:609

`tau-left`

Defined in: tau-left Total references: 1

Other (1)

tau-left : {t₁ t₂ : ITree E R} → t₁ ≈ t₂ → tau t₁ ≈ t₂ in Background.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 Background.InteractionTrees:306

`there`

Defined in: there Total references: 1

Other (1)

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

`transfer-object`

Defined in: transfer-object Total references: 1

Other (1)

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

`ValEq`

Defined in: ValEq Total references: 1

Other (1)

ValEq : VarId → Val → Constraint in AVM.Instruction:561

`ValGeq`

Defined in: ValGeq Total references: 1

Other (1)

ValGeq : VarId → Val → Constraint in AVM.Instruction:570

`ValGt`

Defined in: ValGt Total references: 1

Other (1)

ValGt : VarId → Val → Constraint in AVM.Instruction:573

`ValLeq`

Defined in: ValLeq Total references: 1

Other (1)

ValLeq : VarId → Val → Constraint in AVM.Instruction:564

`ValLt`

Defined in: ValLt Total references: 1

Other (1)

ValLt : VarId → Val → Constraint in AVM.Instruction:567

`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 Background.InteractionTrees:308

`ε-trans`

Defined in: ε-trans Total references: 1

Other (1)

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

References to other modules

This page references the following modules:

AVM.Context
- Symbols: ObjError, IntrospectError, ReflectError, ReifyError, TxError, MachineError, ControllerError, PureError, FDError, NondetError, BaseError, TxLayerError, PureLayerError, AVMError, EventType, Result, ObjectMeta, Store, FunctionEntry, State, LogEntry, Success, mkMeta, mkStore, mkFunctionEntry, ErrObjectNotFound, ErrObjectAlreadyDestroyed, ErrObjectAlreadyExists, ErrInvalidInput, ErrObjectRejectedCall, ErrMetadataCorruption, ErrContextUnavailable, ErrMetadataNotFound, ErrMetadataInconsistent, ErrStoreCorruption, ErrScryPredicateFailed, ErrReflectionDenied, ErrReifyContextFailed, ErrNoTransactionToReify, ErrTxStateAccessDenied, ErrConstraintStoreUnavailable, ErrTxConflict, ErrTxNotFound, ErrTxAlreadyCommitted, ErrTxAlreadyAborted, ErrNoActiveTx, ErrInvalidDuringTx, ErrMachineUnreachable, ErrInvalidMachineTransfer, ErrTeleportDuringTx, ErrControllerUnreachable, ErrUnauthorizedTransfer, ErrCrossControllerTx, ErrObjectNotAvailable, ErrObjectNotConsistent, ErrFreezeFailed, ErrObjectHasNoController, ErrFunctionNotFound, ErrFunctionAlreadyRegistered, ErrVersionConflict, ErrNotImplemented, obj-error, introspect-error, reflect-error, reify-error, base-error, tx-error, tx-layer-error, pure-error, pure-layer-error, machine-error, controller-error, fd-error, nondet-error, err-object-not-found, err-object-destroyed, err-object-exists, err-invalid-input, err-object-rejected, err-metadata-corruption, err-context-unavailable, err-metadata-not-found, err-metadata-inconsistent, err-store-corruption, err-scry-predicate-failed, err-reflection-denied, err-reify-context-failed, err-no-transaction-to-reify, err-tx-state-access-denied, err-constraint-store-unavailable, 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-version-conflict, err-machine-unreachable, err-invalid-machine-transfer, err-teleport-during-tx, err-controller-unreachable, err-unauthorized-transfer, err-cross-controller-tx, err-object-not-available, err-object-not-consistent, err-freeze-failed, err-object-has-no-controller, err-fd-not-implemented, err-nondet-not-implemented, ObjectCreated, ObjectDestroyed, ObjectCalled, MessageReceived, ObjectMoved, ExecutionMoved, ObjectFetched, ObjectTransferred, ObjectFrozen, FunctionUpdated, TransactionStarted, TransactionCommitted, TransactionAborted, ErrorOccurred, mkLogEntry, mkSuccess, success, failure, ObjectStore, MetaStore, StateStore, RuntimeObject, RuntimeObjectWithId, TxWrite, Hash, PureFunctions, Trace, BaseResult, TxResult, PureResult, AVMResult
AVM.Instruction
- Symbols: Safety, ObjInstruction, IntrospectInstruction, ReflectInstruction, ReifyInstruction, Instr₀, TxInstruction, Instr₁, PureInstruction, Instr₂, MachineInstruction, ControllerInstruction, Instr₃, Constraint, FDInstruction, NondetConstraint, NondetInstruction, Instruction, ReifiedContext, ReifiedTxState, ReifiedConstraints, VarId, Safe, Unsafe, createObj, destroyObj, call, self, input, getCurrentMachine, getState, setState, sender, reflect, scryMeta, scryDeep, mkReifiedContext, mkReifiedTxState, mkReifiedConstraints, reifyContext, reifyTxState, reifyConstraints, Obj, Introspect, Reflect, Reify, beginTx, commitTx, abortTx, Tx, callPure, registerPure, updatePure, Pure, getMachine, teleport, moveObject, fetch, getCurrentController, getController, transferObject, freeze, Machine, Controller, mkVarId, Eq, Neq, Leq, Lt, Geq, Gt, AllDiff, ValEq, ValLeq, ValLt, ValGeq, ValGt, newVar, narrow, post, label, Assert, choose, require, FD, Nondet, obj-create, obj-destroy, obj-call, obj-receive, get-self, get-input, get-current-machine, get-state, set-state, get-sender, obj-reflect, obj-scry-meta, obj-scry-deep, do-reify-context, do-reify-tx-state, do-reify-constraints, tx-begin, tx-commit, tx-abort, call-pure, register-pure, pure-update-pure, get-machine, do-teleport, move-object, fetch-object, get-current-controller, get-controller, transfer-object, freeze-object, ISA, Domain, AVMProgram
AVM.Interpreter
- Symbols: lookupObjectWithMeta, lookupPendingCreate, lookupPendingTransfer, updateMeta, lookupState, updateState, createWithMeta, initMeta, makeLogEntry, incrementEventCounter, pendingInputsFor, addPendingWrite, addPendingCreate, removePendingCreate, addPendingDestroy, addPendingTransfer, withTxBranch, withCreateTxBranch, mkSuccessNoTrace, mkSuccessWithLog, mkSuccessWithEvent, containsObserved, ensureObserved, inCreates, inDestroys, validateObserved, checkObject, checkOwnershipPure, resolveTxController, resolveAndCheckOwnership, applyCreates, applyWrite, applyWrites, applyDestroy, applyDestroys, applyTransfer, applyTransfers, applyStates, handleCall, handleCall-aux, callObjInTx, transferObjInTx, transferObjNoTx, destroyObjInTx, destroyObjNoTx, executeObj, executeIntrospect, executeReflect, matchMeta, matchDeep, executeReify, executeTx, executePure, executeMachine, executeController, executeInstr₀, executeInstr₁, executeInstr₂, executeInstruction, interpretAux, interpret, Interpreter, GenericInterpreter
Background.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, caseMaybe, length, ++-assoc, ++-right-id, map, foldr, null, head, filter, elem, concat, hasDuplicates, concatMap, all, any, find, lookup, filterMap, FinSet, Pred, case_of_, ∧, ∨, ||, if_then_else_, ≢, begin_, ≡⟨⟩, ≡⟨⟩_, _∎, >>=ᴹ, +ℕ, *ℕ, ∸, ≥, ≤, ≤?, <?, ≟ℕ, ==ℕ, ++, ∈Pred, ⊆, ∘, lsuc
Background.InteractionTrees
- Symbols: receive, Set₁, MessageEvent, ITreeF, ≈, ITree₁, ITree, send, 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-step, >>=, <$>, _, first-definition
Background.Objects
- Symbols: InputSequence, →[]_, →*[]_, Object, WellFormedObjectType, SequentialObject, mkObjType, wfObjType, mkObj, transition, ε-trans, step-trans, ε, 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, execute-step, objecttype-to-behaviour, run-object-itree, ·, ≈φ[]_, ≈ᵒ, ≈ˢ
Background.StatelessObjects
- Symbols: CounterMsg, Key, KVMsg, KVEvent, AccountMsg, AccountOutput, VBool, VPair, VNil, 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
examples.Battleship.Game
- Symbols: Player, Player1, Player2, GameState, setupGame, opponentBoard, attack, playerAttack, player1Attack, player2Attack, playFullGame, gameWithRollback, playGameWithPlayerType
examples.Battleship.PlayerBoard
- Symbols: VCoord, VShip, coordinateHitsShip, extractShip, checkHit, boardBehavior, handleInput
examples.Battleship.Runner
- Symbols: showMaybeVal, showGameState, testHit, testMiss
examples.Common.Display
- Symbols: showNat, showEventType, showLogEntry, showTrace, showError, showResult
examples.Common.Equality
- Symbols: eqString, eqNat, eqBool, isReachableController, isReachableMachine
examples.Common.InterpreterSetup
- Symbols: Set, interp, interpretAVMProgramRec, RunnerInterpreter
examples.Common.StateInit
- Symbols: emptyStore, noPureFunctions, mkInitialState
examples.PingPong.Main
- Symbols: Message, Input, Output, ObjectBehaviour, Val, VInt, VString, VList, NodeId, ObjectId, MachineId, ControllerId, TxId, MessageType, PingPongMsg, Ping, Pong, mkMsg, VPingPongMsg, createPing, createPong, startPingPong, pingPongExample
examples.PingPong.Runner
- Symbols: freshObjectId, freshTxId, initialState, showOid, showValAgda, eqObjectId, eqTxId, eqControllerId, mkControllerId, interpretBehaviorName, allObjectIds, getBehavior, runExample, main, ObjectBehaviourImpl, namedBehaviour, extractMsg, mkNextMsg, genericPingPongBehavior, pingBehaviorImpl, pongBehaviorImpl, testSimple, test, InterpreterImport
examples.RunnerUtilities
- Symbols: >>, RunnerState, Env, mkState, mkEnv, indent, freshId, showOID, eqOID, lookupObj

Symbol disambiguation log

The following references had multiple matches and were disambiguated:

_<: chose Background.BasicTypes._<?_ from ['Background.BasicTypes.<?', 'Background.InteractionTrees.<$>']
_≤: chose Background.BasicTypes._≤_ from ['Background.BasicTypes.≤', 'Background.BasicTypes.≤?']
_<: chose Background.BasicTypes._<?_ from ['Background.BasicTypes.<?', 'Background.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. ↩