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