Module 0x1::comparator

Provides a framework for comparing two elements

• Struct Result
• Constants
• Function is_equal
• Function is_smaller_than
• Function is_greater_than
• Function compare
• Function compare_u8_vector
• Specification
  • Struct Result
  • Function is_equal
  • Function is_smaller_than
  • Function is_greater_than
  • Function compare
  • Function compare_u8_vector

use 0x1::bcs;

Struct Result

struct Result has drop

Constants

const EQUAL: u8 = 0;

const GREATER: u8 = 2;

const SMALLER: u8 = 1;

Function is_equal

public fun is_equal(self: &comparator::Result): bool

public fun is_equal(self: &Result): bool {
    self.inner == EQUAL
}

Function is_smaller_than

public fun is_smaller_than(self: &comparator::Result): bool

public fun is_smaller_than(self: &Result): bool {
    self.inner == SMALLER
}

Function is_greater_than

public fun is_greater_than(self: &comparator::Result): bool

public fun is_greater_than(self: &Result): bool {
    self.inner == GREATER
}

Function compare

public fun compare<T>(left: &T, right: &T): comparator::Result

public fun compare<T>(left: &T, right: &T): Result {
    let left_bytes = bcs::to_bytes(left);
    let right_bytes = bcs::to_bytes(right);

    compare_u8_vector(left_bytes, right_bytes)
}

Function compare_u8_vector

public fun compare_u8_vector(left: vector<u8>, right: vector<u8>): comparator::Result

public fun compare_u8_vector(left: vector<u8>, right: vector<u8>): Result {
    let left_length = left.length();
    let right_length = right.length();

    let idx = 0;

    while (idx < left_length && idx < right_length) {
        let left_byte = left[idx];
        let right_byte = right[idx];

        if (left_byte < right_byte) {
            return Result { inner: SMALLER }
        } else if (left_byte > right_byte) {
            return Result { inner: GREATER }
        };
        idx += 1;
    };

    if (left_length < right_length) {
        Result { inner: SMALLER }
    } else if (left_length > right_length) {
        Result { inner: GREATER }
    } else {
        Result { inner: EQUAL }
    }
}

Specification

Struct Result

struct Result has drop

inner: u8

invariant inner == EQUAL || inner == SMALLER || inner == GREATER;

Function is_equal

public fun is_equal(self: &comparator::Result): bool

aborts_if false;
let res = self;
ensures result == (res.inner == EQUAL);

Function is_smaller_than

public fun is_smaller_than(self: &comparator::Result): bool

aborts_if false;
let res = self;
ensures result == (res.inner == SMALLER);

Function is_greater_than

public fun is_greater_than(self: &comparator::Result): bool

aborts_if false;
let res = self;
ensures result == (res.inner == GREATER);

Function compare

public fun compare<T>(left: &T, right: &T): comparator::Result

aborts_if false;
let left_bytes = bcs::to_bytes(left);
let right_bytes = bcs::to_bytes(right);
ensures result == spec_compare_u8_vector(left_bytes, right_bytes);

fun spec_compare_u8_vector(left: vector<u8>, right: vector<u8>): Result;

Function compare_u8_vector

public fun compare_u8_vector(left: vector<u8>, right: vector<u8>): comparator::Result

pragma unroll = 5;
pragma opaque;
aborts_if false;
let left_length = len(left);
let right_length = len(right);
ensures (result.inner == EQUAL) ==> (
    (left_length == right_length) &&
        (forall i: u64 where i < left_length: left[i] == right[i])
);
ensures (result.inner == SMALLER) ==> (
    (exists i: u64 where i < left_length:
        (i < right_length) &&
            (left[i] < right[i]) &&
            (forall j: u64 where j < i: left[j] == right[j])
    ) ||
        (left_length < right_length)
);
ensures (result.inner == GREATER) ==> (
    (exists i: u64 where i < left_length:
        (i < right_length) &&
            (left[i] > right[i]) &&
            (forall j: u64 where j < i: left[j] == right[j])
    ) ||
        (left_length > right_length)
);
ensures [abstract] result == spec_compare_u8_vector(left, right);