proofs/lib/lemmas/spec/effectful_aggregate.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/spec/effectful_aggregate.bend as Effectful_aggregate

7 imports

import Base
import ../types/model.bend as T
import ./clock.bend as Clock
import ./cache.bend as S
import ./numeric.bend as N
import ./operations.bend as O
import ./effectful_operations.bend as E

Types

type Prefix source · line 11 · raw

@-K:Data -> @-V:Data -> Data

Ordered abstract bindings, not implementation fuel or native Map traversal. Every successful removal is retained even when the next provider event fails.

Finished

@-K:Data -> @-V:Data -> @removed:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>> -> @retained:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>> -> @remaining:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/clock.ClockEvent> -> @requests:Nat -> Prefix<K, V>

Failed

@-K:Data -> @-V:Data -> @error:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/clock.Error -> @removed:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>> -> @retained:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>> -> @remaining:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/clock.ClockEvent> -> @requests:Nat -> Prefix<K, V>

Definitions

def prepend source · line 15 · raw

@-K:Data -> @-V:Data -> @entry:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V> -> @result:Prefix<K, V> -> Prefix<K, V>

def decide source · line 20 · raw

@-K:Data -> @-V:Data -> @entry:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V> -> @tail:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>> -> @events:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/clock.ClockEvent> -> @rest:Prefix<K, V> -> @expired:Bool -> Prefix<K, V>

def sentinel source · line 25 · raw

@-K:Data -> @-V:Data -> @entry:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V> -> @tail:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>> -> @events:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/clock.ClockEvent> -> @result:Prefix<K, V> -> @immortal:Bool -> Prefix<K, V>

def prefix source · line 30 · raw

@-K:Data -> @-V:Data -> @ordered:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>> -> @events:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/clock.ClockEvent> -> Prefix<K, V>

Templates

template apply_prefix source · line 42 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> @result:Prefix<K, V> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/effectful_operations.Outcome<K, V>

template purge_expired source · line 47 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @+s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> @events:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/clock.ClockEvent> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/effectful_operations.Outcome<K, V>