Formal Properties of the AVM
This module establishes key formal properties of the AVM instruction set and interpreter.
{-# OPTIONS --exact-split --without-K --guardedness #-} open import Foundation.BasicTypes using (ℕ) module AVM.FormalProperties -- Base types (Val : Set) (ObjectId : Set) (freshObjectId : ℕ → ObjectId) (MachineId : Set) (ControllerId : Set) (ControllerVersion : Set) (TxId : Set) (freshTxId : ℕ → TxId) where open import Foundation.BasicTypes hiding (ℕ) open import Foundation.InteractionTrees -- Import Objects module to get ObjectType open import AVM.Objects Val ObjectId freshObjectId MachineId ControllerId ControllerVersion TxId freshTxId using (Object) -- Import Instruction and Interpreter with Object open import AVM.Instruction Val ObjectId freshObjectId MachineId ControllerId ControllerVersion TxId freshTxId Object open import AVM.Interpreter Val ObjectId freshObjectId MachineId ControllerId ControllerVersion TxId freshTxId Object (λ obj → Object.behavior obj)
Verification Primitives
-- Helper predicates data Is-just {A : Set} : Maybe A → Set where is-just : ∀ {x} → Is-just (just x) postulate -- Existential uniqueness ∃! : ∀ {A : Set} → (A → Set) → Set -- Transaction states committed : State → Set aborted : State → Set
Functional Consistency
The interpreter is functionally consistent: the same state and instruction always produce the same result when using only base instructions (no nondeterminism):
-- Note: _==_ is already defined in Foundation.BasicTypes postulate -- For the interpreter to be functionally consistent, we need deterministic helper functions _≤v_ : ControllerVersion → ControllerVersion → Bool getFreshIdCounter : State → ℕ allObjectIds : State → List ObjectId interpretValue : Val → Object isReachableController : ControllerId → Bool isReachableMachine : MachineId → Bool sucVersion : ControllerVersion → ControllerVersion toVal : ∀ {A : Set} → A → Val -- Open the interpreter module (using _==_ from BasicTypes) open Interpreter _==_ _≤v_ getFreshIdCounter allObjectIds interpretValue isReachableController isReachableMachine sucVersion -- Functional consistency: Same state and instruction produce same result -- (for base instructions; nondeterministic instructions like `choose` are excluded) postulate determinism : ∀ {s A} (instr : Instr₀ s A) (st : State) → ∃! λ result → executeInstr₀ instr st ≡ result
Transaction Atomicity
Transactions provide all-or-nothing semantics:
-- A transaction either commits all its operations or aborts with no effect data TransactionOutcome : Set where Committed : State → TransactionOutcome Aborted : TransactionOutcome -- Atomicity property: A transaction's effects are atomic postulate atomicity : ∀ {A} (prog : ITree (Instr₀ Safe) A) (st : State) → ∀ (txid : TxId) → -- If we begin a transaction State.tx st ≡ just txid → -- Then after execution, either all effects are committed or none are ∃! λ outcome → ∃ λ st' → (outcome ≡ Committed st' × committed st') + (outcome ≡ Aborted × aborted st)
Safety Properties
Safe instructions cannot violate system invariants:
-- Safe instructions preserve store consistency postulate storeConsistency : ∀ {A} (instr : Instr₀ Safe A) (st : State) → ∀ (result : AVMResult A) → executeInstr₀ instr st ≡ result → -- If execution succeeds ∀ (succ : Success A) → result ≡ success succ → -- Then metadata exists for every object ∀ (oid : ObjectId) → Is-just (Store.objects (State.store (Success.state succ)) oid) → Is-just (Store.metadata (State.store (Success.state succ)) oid) -- Safe instructions cannot create duplicate objects postulate uniqueObjectCreation : ∀ (val : Val) (st : State) → ∀ (succ : Success ObjectId) → executeObj (createObj val) st ≡ success succ → -- The object didn't exist before Store.objects (State.store st) (Success.value succ) ≡ nothing
Event Properties
Events accurately reflect state changes:
-- Every state change produces a corresponding event postulate eventCompleteness : ∀ {s A} (instr : Instr₀ s A) (st : State) → ∀ (succ : Success A) → executeInstr₀ instr st ≡ success succ → -- If state changed, there must be events st ≢ Success.state succ → Success.trace succ ≢ [] -- Helper operators for event ordering postulate index-of : ∀ {A : Set} → A → List A → ℕ _<_ : ℕ → ℕ → Set -- Events are ordered by timestamp postulate eventOrdering : ∀ {s A} (instr : Instr₀ s A) (st : State) → ∀ (succ : Success A) → executeInstr₀ instr st ≡ success succ → -- Events are temporally ordered ∀ (e₁ e₂ : LogEntry) → e₁ ∈ Success.trace succ → e₂ ∈ Success.trace succ → index-of e₁ (Success.trace succ) < index-of e₂ (Success.trace succ) → LogEntry.timestamp e₁ ≤ LogEntry.timestamp e₂
Progress and Preservation
Well-formed programs make progress and preserve types:
-- Helper for program stepping postulate interpretProgramStep : ∀ {A} → ITree (Instr₀ Safe) A → State → Maybe (ITree (Instr₀ Safe) A × State × Trace) -- Progress: Well-formed programs can always take a step postulate progress : ∀ {A} (prog : ITree (Instr₀ Safe) A) (st : State) → -- If the program is not finished ¬ (∃ λ a → observe prog ≡ retF a) → -- Then it can take a step ∃ λ prog' → ∃ λ st' → ∃ λ entries → interpretProgramStep prog st ≡ just (prog' , st' , entries) -- Type preservation: Execution preserves well-typedness -- (This is trivially true in Agda due to its type system) postulate preservation : ∀ {B : Set} (instr : Instr₀ Safe B) (st : State) → ∀ (succ : Success B) → executeInstr₀ instr st ≡ success succ → -- The result has the expected type ⊤