Statistics

─── Uninterpreted refinement-language symbols ───────────────────────── These live in the refinement language so Z3 can reason about them as abstract symbols. Runtime providers below tie concrete values back to them via refined return types. Fraction of xs strictly below threshold t.
Imports
open Array;
Table of Contents

Functions

widenBelow

Monotonicity below: t1 <= t2 ⇒ fracBelow xs t1 <= fracBelow xs t2.
def widenBelow (1 xs : Array Float | Array.size xs > 0) (t1 : Float) (t2 : Float | t2 ≥ t1) : {r : Array Float | Array.size r > 0 && fracBelow r t2 ≥ fracBelow xs t1}

widenAbove

Monotonicity above: t1 <= t2 ⇒ fracAbove xs t1 >= fracAbove xs t2.
def widenAbove (1 xs : Array Float | Array.size xs > 0) (t1 : Float) (t2 : Float | t2 ≤ t1) : {r : Array Float | Array.size r > 0 && fracAbove r t2 ≥ fracAbove xs t1}

belowComplement

Complement at a non-atomic point: fracBelow + fracAbove = 1.
def belowComplement (1 xs : Array Float | Array.size xs > 0) (t : Float) : {r : Array Float | Array.size r > 0 && fracBelow r t = 1.0 - fracAbove xs t}

betweenFromBelow

Between bound: fracBetween lo hi >= fracBelow hi - fracBelow lo (slack covers atoms).
def betweenFromBelow (1 xs : Array Float | Array.size xs > 0) (lo : Float) (hi : Float | hi ≥ lo) : {r : Array Float | Array.size r > 0 && fracBetween r lo hi ≥ fracBelow xs hi - fracBelow xs lo}

mean

Returns the mean (average) of a non-empty list of numbers.
def mean (1 xs : Array Float | Array.size xs > 0) : {m : Float | m = sampleMean xs}

median

Returns the median (middle value) of a non-empty list of numbers.
def median (1 xs : Array Float | Array.size xs > 0) : Float

std

Returns the sample standard deviation of a non-empty list of numbers.
def std (1 xs : Array Float | Array.size xs > 0) : {s : Float | s = sampleStd xs}

var

Returns the sample variance of a non-empty list of numbers.
def var (1 xs : Array Float | Array.size xs > 0) : {v : Float | v = sampleVar xs}

min

Returns the minimum value in a non-empty list of numbers.
def min (1 xs : Array Float | Array.size xs > 0) : {m : Float | m = sampleMin xs}

max

Returns the maximum value in a non-empty list of numbers.
def max (1 xs : Array Float | Array.size xs > 0) : {m : Float | m = sampleMax xs}

sum

Returns the sum of a non-empty list of numbers.
def sum (1 xs : Array Float | Array.size xs > 0) : Float

quantile

Returns the quantile of a non-empty list of numbers.
def quantile (1 xs : Array Float | Array.size xs > 0) (q : Float) : Float

prod

Returns the product of a non-empty list of numbers.
def prod (1 xs : Array Float | Array.size xs > 0) : Float

cumsum

Returns the cumulative sum of a non-empty list of numbers.
def cumsum (1 xs : Array Float | Array.size xs > 0) : Array Float

cumprod

Returns the cumulative product of a non-empty list of numbers.
def cumprod (1 xs : Array Float | Array.size xs > 0) : Array Float

quartiles

Returns the 1st (Q1), 2nd (median), and 3rd (Q3) quartiles of a non-empty list of numbers.
def quartiles (1 xs : Array Float | Array.size xs > 0) : Array Float

unique

Returns the unique values in a non-empty list.
def unique (1 xs : Array Float | Array.size xs > 0) : Array Float

argmax

Returns the index of the maximum value in a non-empty list of numbers.
def argmax (1 xs : Array Float | Array.size xs > 0) : Float

argmin

Returns the index of the minimum value in a non-empty list of numbers.
def argmin (1 xs : Array Float | Array.size xs > 0) : Float

percentile

Returns the percentile of a non-empty list of numbers.
def percentile (1 xs : Array Float | Array.size xs > 0) (p : Float) : Float

corrcoef

Returns the correlation coefficient of two non-empty lists of equal length.
def corrcoef (1 xs : Array Float | Array.size xs > 0) (1 ys : Array Float | Array.size ys = Array.size xs) : Float

cov

Returns the covariance of two non-empty lists of equal length.
def cov (1 xs : Array Float | Array.size xs > 0) (1 ys : Array Float | Array.size ys = Array.size xs) : Float

proportionBelow

Proportion of values strictly below a threshold.
def proportionBelow (1 xs : Array Float | Array.size xs > 0) (t : Float) : {f : Float | f = fracBelow xs t && (0.0 ≤ f && f ≤ 1.0)}

proportionAbove

Proportion of values strictly above a threshold.
def proportionAbove (1 xs : Array Float | Array.size xs > 0) (t : Float) : {f : Float | f = fracAbove xs t && (0.0 ≤ f && f ≤ 1.0)}

proportionBetween

Proportion of values strictly inside the open interval (lo, hi).
def proportionBetween (1 xs : Array Float | Array.size xs > 0) (lo : Float) (hi : Float | hi ≥ lo) : {f : Float | f = fracBetween xs lo hi && (0.0 ≤ f && f ≤ 1.0)}

Uninterpreted

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

fracBelow

uninterpreted
Fraction of xs strictly below threshold t.
def fracBelow : (xs : Array Float) → (t : Float) → Float

fracAbove

uninterpreted
Fraction of xs strictly above threshold t.
def fracAbove : (xs : Array Float) → (t : Float) → Float

fracBetween

uninterpreted
Fraction of xs in the open interval (lo, hi).
def fracBetween : (xs : Array Float) → (lo : Float) → (hi : Float) → Float

sampleMean

uninterpreted
Sample summary statistics as abstract symbols.
def sampleMean : (xs : Array Float) → Float

sampleVar

uninterpreted
def sampleVar : (xs : Array Float) → Float

sampleStd

uninterpreted
def sampleStd : (xs : Array Float) → Float

sampleMin

uninterpreted
def sampleMin : (xs : Array Float) → Float

sampleMax

uninterpreted
def sampleMax : (xs : Array Float) → Float