Downloader

Download session with typestate + progress ghost (LiquidJava ``Downloader``). States: created → start → downloading → (update)* → finish → completed ``progress`` is a ghost measure in ``[0, 100]``. Updates must strictly increase it; ``finish`` requires ``progress = 100``.
Table of Contents

Types

Downloader

(type) linear
linear type Downloader

Functions

new_downloader

Fresh session at 0% in the created state.
def new_downloader (_ : Unit) : {d : Downloader | created d = True && (downloading d = False && (completed d = False && progress d = 0))}

start

Begin downloading (created → downloading), progress stays 0.
def start (1 d : Downloader | created d = True && progress d = 0) : {out : Downloader | created out = False && (downloading out = True && (completed out = False && progress out = 0))}

update

Monotonic progress update while downloading. ``p`` must exceed current progress and be at most 100.
def update (1 d : Downloader | downloading d = True) (p : Int | p > progress d && p ≤ 100) : {out : Downloader | downloading out = True && (completed out = False && progress out = p)}

finish

Complete only at 100%.
def finish (1 d : Downloader | downloading d = True && progress d = 100) : {out : Downloader | downloading out = False && (completed out = True && progress out = 100)}

discard

Consume a completed session.
def discard (1 d : Downloader | completed d = True) : Unit

Uninterpreted

Functions declared as def f ... = uninterpreted: only their signature is known to the verifier; they have no body.

created

uninterpreted
def created : (d : Downloader) → Bool

downloading

uninterpreted
def downloading : (d : Downloader) → Bool

completed

uninterpreted
def completed : (d : Downloader) → Bool

progress

uninterpreted
def progress : (d : Downloader) → Int