Image

Imports
open Color;
Table of Contents

Types

Image

(type)
type Image

Constructors

For each type in this module: inductive types list their declared constructors; opaque types list any local function whose name starts with mk and which returns a value of that type.

Image (opaque · mk*)

mk

Creates a new image of given width, height, and color.
def mk (w: {p : Int | p > 0}) (h: {p : Int | p > 0}) (color: Color) : {i : Image | width i = w && height i = h}

Functions

get_width

Reads the width at runtime. The return type is refined to equal the `width` measure, so the value is provably the same width the type system reasons about (e.g. `get_width (mk w h c)` has type `{r:Int | r == w}`).
def get_width (im: Image) : {r : Int | r = width im}

get_height

Reads the height at runtime; refined to equal the `height` measure (see `get_width`).
def get_height (im: Image) : {r : Int | r = height im}

mk

Creates a new image of given width, height, and color.
def mk (w: {p : Int | p > 0}) (h: {p : Int | p > 0}) (color: Color) : {i : Image | width i = w && height i = h}

copy

Returns an independent copy (PIL Image.copy).
def copy (im: Image) : {c : Image | width c = width im && height c = height im}

crop

Crops a rectangular region [x, x+w) × [y, y+h) into a new image of size w×h.
def crop (im: Image) (x: {p : Int | p ≥ 0 && p ≤ width im}) (y: {p : Int | p ≥ 0 && p ≤ height im}) (w: {p : Int | p > 0 && x + p ≤ width im}) (h: {p : Int | p > 0 && y + p ≤ height im}) : {r : Image | width r = w && height r = h}

resize

Resamples to an exact width and height (PIL Image.resize with high-quality filter).
def resize (im: Image) (w: {p : Int | p > 0}) (h: {p : Int | p > 0}) : {r : Image | width r = w && height r = h}

fit_inside

Shrinks the image in-place on a copy so it fits inside max_w×max_h while preserving aspect ratio (PIL thumbnail).
def fit_inside (im: Image) (max_w: {p : Int | p > 0}) (max_h: {p : Int | p > 0}) : Image

rotate

Rotates counter-clockwise by angle degrees; output size matches input (expand=False, PIL default behavior).
def rotate (im: Image) (angle: Float) : {r : Image | width r = width im && height r = height im}

flip_horizontal

Horizontal mirror (PIL FLIP_LEFT_RIGHT).
def flip_horizontal (im: Image) : {r : Image | width r = width im && height r = height im}

flip_vertical

Vertical mirror (PIL FLIP_TOP_BOTTOM).
def flip_vertical (im: Image) : {r : Image | width r = width im && height r = height im}

get_pixel

Samples the RGB pixel at (x, y) as a Color (always RGB mode after open/mk).
def get_pixel (im: Image) (x: {p : Int | p ≥ 0 && p < width im}) (y: {p : Int | p ≥ 0 && p < height im}) : Color

put_pixel

Functional single-pixel draw: returns a new image with one pixel replaced (PIL putpixel on a copy).
def put_pixel (im: Image) (x: {p : Int | p ≥ 0 && p < width im}) (y: {p : Int | p ≥ 0 && p < height im}) (color: Color) : {r : Image | width r = width im && height r = height im}

paste

Pastes `src` onto `dest` with top-left at (x, y); both images stay RGB-aligned in the binding layer.
def paste (dest: Image) (src: Image) (x: {p : Int | p ≥ 0 && p + width src ≤ width dest}) (y: {p : Int | p ≥ 0 && p + height src ≤ height dest}) : {r : Image | width r = width dest && height r = height dest}

grayscale

Converts to grayscale luminance then back to RGB so Color-based pipelines keep one channel width.
def grayscale (im: Image) : {g : Image | width g = width im && height g = height im}

invert

Per-channel photographic invert (ImageOps.invert).
def invert (im: Image) : {r : Image | width r = width im && height r = height im}

blur

Gaussian blur; radius is the PIL GaussianBlur radius (in pixels, ≥ 0).
def blur (im: Image) (radius: Float) : {r : Image | width r = width im && height r = height im}

show

Displays the image.
def show (image: Image) : Unit

save

Saves the image to a file.
def save (image: Image) (path: String) : Unit

open

Opens an image from a file (normalized to RGB for predictable Color / pixel operations).
def open (path: String) : Image

diff

Computes the mean squared error (MSE) difference between two images.
def diff (img: Image) (img2: Image) : Float

fitness_bw_mse

def fitness_bw_mse (candidate: Image) (reference: Image) : Float

fitness_half_size_mse

def fitness_half_size_mse (candidate: Image) (reference: Image) : Float

fitness_row_mismatch

def fitness_row_mismatch (candidate: Image) (reference: Image) : Float

fitness_col_mismatch

def fitness_col_mismatch (candidate: Image) (reference: Image) : Float

fitness_pixel_mismatch

def fitness_pixel_mismatch (candidate: Image) (reference: Image) : Float

draw_rectangle

Draws a rectangle on the image.
def draw_rectangle (im: Image) (x: {p : Int | p ≥ 0 && p ≤ width im}) (y: {p : Int | p ≥ 0 && p ≤ height im}) (w: {p : Int | p > 0 && x + p ≤ width im}) (h: {p : Int | p > 0 && y + p ≤ height im}) (color: Color) : {rim : Image | width rim = width im && height rim = height im}

Uninterpreted

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

height

uninterpreted
The image's height in pixels, as an uninterpreted measure. It carries the size contracts of every operation (`mk`, `crop`, `resize`, ...) through the type system but has no runtime value; use `get_height` to read it at runtime.
def height : (im : Image) → Int

width

uninterpreted
The image's width in pixels, as an uninterpreted measure (see `height`). Use `get_width` to read it at runtime.
def width : (im : Image) → Int