triangle_encoding.sc

# optimally encoding a set of two integers

N := 32
N/2 := N // 2
NUMVALS := N * (N + 1) // 2

fn trienc (x y)
    assert (x < N)
    assert (y < N)
    assert (x >= y)
    x y := if (y >= N/2)
        pass
            y - N/2
            x - N/2
    else
        pass (x + 1) y
    y * (N + 1) + x

fn tridec (i)
    assert (i < NUMVALS)
    y := i // (N + 1)
    x := i - y * (N + 1)
    if (y >= x)
        pass
            y + N/2
            x + N/2
    else
        pass (x - 1) y

# optimally encoding a set of two integers, assuming x != y we save one bit.

NUMVALS := N * (N - 1) // 2
fn triencne (x y)
    assert (x < N)
    assert (y < N)
    assert (x > y)
    x y := if (y >= N/2)
        pass
            y - N/2
            x - N/2
    else
        pass (x - 1) y
    y * (N - 1) + x

fn tridecne (i)
    assert (i < NUMVALS)
    y := i // (N - 1)
    x := i - y * (N - 1)
    if (y > x)
        pass
            y + N/2
            x + N/2
    else
        pass (x + 1) y