Skip to content
Aptos Docs

comparator - [testnet]

Provides a framework for comparing two elements

use 0x1::bcs;

Constants

const EQUAL: u8 = 0;
const GREATER: u8 = 2;
const SMALLER: u8 = 1;

Structs

Result

struct Result has drop
Fields
inner: u8

Functions

is_equal

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

is_smaller_than

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

is_greater_than

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

compare

public fun compare<T>(left: &T, right: &T): comparator::Result
Implementation 
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)
}

compare_u8_vector

public fun compare_u8_vector(left: vector<u8>, right: vector<u8>): comparator::Result
Implementation 
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

Result

struct Result has drop
inner: u8 
invariant inner == EQUAL || inner == SMALLER || inner == GREATER;

is_equal

public fun is_equal(self: &comparator::Result): bool
aborts_if false;
let res = self;
ensures result == (res.inner == EQUAL);

is_smaller_than

public fun is_smaller_than(self: &comparator::Result): bool
aborts_if false;
let res = self;
ensures result == (res.inner == SMALLER);

is_greater_than

public fun is_greater_than(self: &comparator::Result): bool
aborts_if false;
let res = self;
ensures result == (res.inner == GREATER);

compare

public fun compare<T>(left: &T, right: &T): comparator::Result
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;

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);