proofs/lib/lemmas/spec/clock.bend

bend-collections-laws-containers@1.0.0.0 · 29 lines · 0 definitions

1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/types/model.bend as T
3
4# Abstract outcomes of requesting the caller's clock. Sample has already passed
5# the signed-64-bit millisecond validation. The other constructors distinguish
6# provider exceptions from rejected samples. A host conversion proof must map
7# real provider outcomes to these cases; it is not assumed here.
8type ClockEvent is Data:
9  Sample{milliseconds: T.Int64}
10  InvalidSample{reason: String}
11  ProviderException{reason: String}
12
13type Error is Data:
14  Exhausted{}
15  Invalid{reason: String}
16  Thrown{reason: String}
17
18type Reply is Data:
19  Accepted{milliseconds: T.Int64, remaining: List<&2, ClockEvent>}
20  Rejected{error: Error, remaining: List<&2, ClockEvent>}
21
22# Each evaluation denotes exactly one request, including a failed request.
23# Merely retaining a clock stream does not request or validate its next event.
24def request(events: List<&2, ClockEvent>) -> Reply:
25  match events:
26    case Nil{}: Rejected{Exhausted{}, Nil{}}
27    case Con{Sample{now}, tail}: Accepted{now, tail}
28    case Con{InvalidSample{reason}, tail}: Rejected{Invalid{reason}, tail}
29    case Con{ProviderException{reason}, tail}: Rejected{Thrown{reason}, tail}