Keyboard shortcuts

Press or to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Module 0x1::base16

Function hex_char_to_u8

public(friend) fun hex_char_to_u8(c: u8): u8
Implementation
public(friend) fun hex_char_to_u8(c: u8): u8 {
    if (c >= 48 && c <= 57) {  // '0' to '9'
        c - 48
    } else if (c >= 65 && c <= 70) { // 'A' to 'F'
        c - 55
    } else if (c >= 97 && c <= 102) { // 'a' to 'f'
        c - 87
    } else {
        abort 1
    }
}

Function base16_utf8_to_vec_u8

public(friend) fun base16_utf8_to_vec_u8(str: vector<u8>): vector<u8>
Implementation
public(friend) fun base16_utf8_to_vec_u8(str: vector<u8>): vector<u8> {
    let result = vector::empty<u8>();
    let i = 0;
    while (i < str.length()) {
        let c1 = str.borrow(i);
        let c2 = str.borrow(i + 1);
        let byte = hex_char_to_u8(*c1) << 4 | hex_char_to_u8(*c2);
        result.push_back(byte);
        i += 2;
    };
    result
}

Specification

Function base16_utf8_to_vec_u8

public(friend) fun base16_utf8_to_vec_u8(str: vector<u8>): vector<u8>
pragma opaque;
ensures [abstract] result == spec_base16_utf8_to_vec_u8(str);

fun spec_base16_utf8_to_vec_u8(str: vector<u8>): vector<u8>;