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

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

2 imports

import Base
import ../types/model.bend as T

Types

type ClockEvent source · line 8 · raw

Data

Abstract outcomes of requesting the caller's clock. Sample has already passed the signed-64-bit millisecond validation. The other constructors distinguish provider exceptions from rejected samples. A host conversion proof must map real provider outcomes to these cases; it is not assumed here.

Sample

@milliseconds:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> ClockEvent

InvalidSample
```
@reason:String -> ClockEvent
```
ProviderException
```
@reason:String -> ClockEvent
```

type Error source · line 13 · raw

Data

Exhausted
```
Error
```
Invalid
```
@reason:String -> Error
```
Thrown
```
@reason:String -> Error
```

type Reply source · line 18 · raw

Data

Accepted

@milliseconds:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Int64 -> @remaining:List<&2, ClockEvent> -> Reply

Rejected

@error:Error -> @remaining:List<&2, ClockEvent> -> Reply

Definitions

def request source · line 24 · raw

@events:List<&2, ClockEvent> -> Reply

Each evaluation denotes exactly one request, including a failed request. Merely retaining a clock stream does not request or validate its next event.