diff --git a/build/StarcoinFramework/BuildInfo.yaml b/build/StarcoinFramework/BuildInfo.yaml index 013c40fd..ae8f3019 100644 --- a/build/StarcoinFramework/BuildInfo.yaml +++ b/build/StarcoinFramework/BuildInfo.yaml @@ -261,7 +261,7 @@ compiled_package_info: ? address: "0x00000000000000000000000000000001" name: YieldFarmingV2 : StarcoinFramework - source_digest: F39F5364AE53D568F6DE697F20438F49769B5D07FDB6D7231ED2F8262053CE66 + source_digest: 3DB38FA53B8165D50EFE27CA96B9F5C6B7B338D7519835094216173A9B06D40B build_flags: dev_mode: false test_mode: false diff --git a/build/StarcoinFramework/bytecode_modules/BCS.mv b/build/StarcoinFramework/bytecode_modules/BCS.mv index ee2fa3e9..cdebc88d 100644 Binary files a/build/StarcoinFramework/bytecode_modules/BCS.mv and b/build/StarcoinFramework/bytecode_modules/BCS.mv differ diff --git a/build/StarcoinFramework/docs/BCS.md b/build/StarcoinFramework/docs/BCS.md index b9a138fc..2c40dac5 100644 --- a/build/StarcoinFramework/docs/BCS.md +++ b/build/StarcoinFramework/docs/BCS.md @@ -27,11 +27,26 @@ published on-chain. - [Function `deserialize_option_tag`](#0x1_BCS_deserialize_option_tag) - [Function `deserialize_len`](#0x1_BCS_deserialize_len) - [Function `deserialize_bool`](#0x1_BCS_deserialize_bool) -- [Function `deserialize_uleb128_as_u32`](#0x1_BCS_deserialize_uleb128_as_u32) - [Function `get_byte`](#0x1_BCS_get_byte) - [Function `get_n_bytes`](#0x1_BCS_get_n_bytes) - [Function `get_n_bytes_as_u128`](#0x1_BCS_get_n_bytes_as_u128) +- [Function `deserialize_uleb128_as_u32`](#0x1_BCS_deserialize_uleb128_as_u32) - [Function `serialize_u32_as_uleb128`](#0x1_BCS_serialize_u32_as_uleb128) +- [Function `skip_option_bytes_vector`](#0x1_BCS_skip_option_bytes_vector) +- [Function `skip_option_bytes`](#0x1_BCS_skip_option_bytes) +- [Function `skip_bytes_vector`](#0x1_BCS_skip_bytes_vector) +- [Function `skip_bytes`](#0x1_BCS_skip_bytes) +- [Function `skip_n_bytes`](#0x1_BCS_skip_n_bytes) +- [Function `skip_u64_vector`](#0x1_BCS_skip_u64_vector) +- [Function `skip_u128_vector`](#0x1_BCS_skip_u128_vector) +- [Function `skip_u256`](#0x1_BCS_skip_u256) +- [Function `skip_u128`](#0x1_BCS_skip_u128) +- [Function `skip_u64`](#0x1_BCS_skip_u64) +- [Function `skip_u32`](#0x1_BCS_skip_u32) +- [Function `skip_u16`](#0x1_BCS_skip_u16) +- [Function `skip_address`](#0x1_BCS_skip_address) +- [Function `skip_bool`](#0x1_BCS_skip_bool) +- [Function `can_skip`](#0x1_BCS_can_skip) - [Module Specification](#@Module_Specification_1) @@ -770,6 +785,132 @@ Return the address of key bytes + + + + +## Function `get_byte` + + + +
fun get_byte(input: &vector<u8>, offset: u64): u8
+
+ + + +
+Implementation + + +
fun get_byte(input: &vector<u8>, offset: u64): u8 {
+    assert!(((offset + 1) <= Vector::length(input)) && (offset < offset + 1), Errors::invalid_state(ERR_INPUT_NOT_LARGE_ENOUGH));
+    *Vector::borrow(input, offset)
+}
+
+ + + +
+ +
+Specification + + + +
pragma verify = false;
+
+ + + +
+ + + +## Function `get_n_bytes` + + + +
fun get_n_bytes(input: &vector<u8>, offset: u64, n: u64): vector<u8>
+
+ + + +
+Implementation + + +
fun get_n_bytes(input: &vector<u8>, offset: u64, n: u64): vector<u8> {
+    assert!(((offset + n) <= Vector::length(input)) && (offset < offset + n), Errors::invalid_state(ERR_INPUT_NOT_LARGE_ENOUGH));
+    let i = 0;
+    let content = Vector::empty<u8>();
+    while (i < n) {
+        let b = *Vector::borrow(input, offset + i);
+        Vector::push_back(&mut content, b);
+        i = i + 1;
+    };
+    content
+}
+
+ + + +
+ +
+Specification + + + +
pragma verify = false;
+
+ + + +
+ + + +## Function `get_n_bytes_as_u128` + + + +
fun get_n_bytes_as_u128(input: &vector<u8>, offset: u64, n: u64): u128
+
+ + + +
+Implementation + + +
fun get_n_bytes_as_u128(input: &vector<u8>, offset: u64, n: u64): u128 {
+    assert!(((offset + n) <= Vector::length(input)) && (offset < offset + n), Errors::invalid_state(ERR_INPUT_NOT_LARGE_ENOUGH));
+    let number: u128 = 0;
+    let i = 0;
+    while (i < n) {
+        let byte = *Vector::borrow(input, offset + i);
+        let s = (i as u8) * 8;
+        number = number + ((byte as u128) << s);
+        i = i + 1;
+    };
+    number
+}
+
+ + + +
+ +
+Specification + + + +
pragma verify = false;
+
+ + +
@@ -827,13 +968,13 @@ Return the address of key bytes - + -## Function `get_byte` +## Function `serialize_u32_as_uleb128` -
fun get_byte(input: &vector<u8>, offset: u64): u8
+
fun serialize_u32_as_uleb128(value: u64): vector<u8>
 
@@ -842,9 +983,14 @@ Return the address of key bytes Implementation -
fun get_byte(input: &vector<u8>, offset: u64): u8 {
-    assert!(((offset + 1) <= Vector::length(input)) && (offset < offset + 1), Errors::invalid_state(ERR_INPUT_NOT_LARGE_ENOUGH));
-    *Vector::borrow(input, offset)
+
fun serialize_u32_as_uleb128(value: u64): vector<u8> {
+    let output = Vector::empty<u8>();
+    while ((value >> 7) != 0) {
+        Vector::push_back(&mut output, (((value & 0x7f) | 0x80) as u8));
+        value = value >> 7;
+    };
+    Vector::push_back(&mut output, (value as u8));
+    output
 }
 
@@ -864,13 +1010,13 @@ Return the address of key bytes - + -## Function `get_n_bytes` +## Function `skip_option_bytes_vector` -
fun get_n_bytes(input: &vector<u8>, offset: u64, n: u64): vector<u8>
+
public fun skip_option_bytes_vector(input: &vector<u8>, offset: u64): u64
 
@@ -879,16 +1025,14 @@ Return the address of key bytes Implementation -
fun get_n_bytes(input: &vector<u8>, offset: u64, n: u64): vector<u8> {
-    assert!(((offset + n) <= Vector::length(input)) && (offset < offset + n), Errors::invalid_state(ERR_INPUT_NOT_LARGE_ENOUGH));
+
public fun skip_option_bytes_vector(input: &vector<u8>, offset: u64): u64 {
+    let (len, new_offset) = deserialize_len(input, offset);
     let i = 0;
-    let content = Vector::empty<u8>();
-    while (i < n) {
-        let b = *Vector::borrow(input, offset + i);
-        Vector::push_back(&mut content, b);
+    while (i < len) {
+        new_offset = skip_option_bytes(input, new_offset);
         i = i + 1;
     };
-    content
+    new_offset
 }
 
@@ -908,13 +1052,13 @@ Return the address of key bytes - + -## Function `get_n_bytes_as_u128` +## Function `skip_option_bytes` -
fun get_n_bytes_as_u128(input: &vector<u8>, offset: u64, n: u64): u128
+
public fun skip_option_bytes(input: &vector<u8>, offset: u64): u64
 
@@ -923,17 +1067,55 @@ Return the address of key bytes Implementation -
fun get_n_bytes_as_u128(input: &vector<u8>, offset: u64, n: u64): u128 {
-    assert!(((offset + n) <= Vector::length(input)) && (offset < offset + n), Errors::invalid_state(ERR_INPUT_NOT_LARGE_ENOUGH));
-    let number: u128 = 0;
+
public fun skip_option_bytes(input: &vector<u8>, offset: u64):  u64 {
+    let (tag, new_offset) = deserialize_option_tag(input, offset);
+    if (!tag) {
+        new_offset
+    } else {
+        skip_bytes(input, new_offset)
+    }
+}
+
+ + + + + +
+Specification + + + +
pragma verify = false;
+
+ + + +
+ + + +## Function `skip_bytes_vector` + + + +
public fun skip_bytes_vector(input: &vector<u8>, offset: u64): u64
+
+ + + +
+Implementation + + +
public fun skip_bytes_vector(input: &vector<u8>, offset: u64): u64 {
+    let (len, new_offset) = deserialize_len(input, offset);
     let i = 0;
-    while (i < n) {
-        let byte = *Vector::borrow(input, offset + i);
-        let s = (i as u8) * 8;
-        number = number + ((byte as u128) << s);
+    while (i < len) {
+        new_offset = skip_bytes(input, new_offset);
         i = i + 1;
     };
-    number
+    new_offset
 }
 
@@ -953,13 +1135,13 @@ Return the address of key bytes
- + -## Function `serialize_u32_as_uleb128` +## Function `skip_bytes` -
fun serialize_u32_as_uleb128(value: u64): vector<u8>
+
public fun skip_bytes(input: &vector<u8>, offset: u64): u64
 
@@ -968,14 +1150,416 @@ Return the address of key bytes Implementation -
fun serialize_u32_as_uleb128(value: u64): vector<u8> {
-    let output = Vector::empty<u8>();
-    while ((value >> 7) != 0) {
-        Vector::push_back(&mut output, (((value & 0x7f) | 0x80) as u8));
-        value = value >> 7;
-    };
-    Vector::push_back(&mut output, (value as u8));
-    output
+
public fun skip_bytes(input: &vector<u8>, offset: u64): u64 {
+    let (len, new_offset) = deserialize_len(input, offset);
+    new_offset + len
+}
+
+ + + + + +
+Specification + + + +
pragma verify = false;
+
+ + + +
+ + + +## Function `skip_n_bytes` + + + +
public fun skip_n_bytes(input: &vector<u8>, offset: u64, n: u64): u64
+
+ + + +
+Implementation + + +
public fun skip_n_bytes(input: &vector<u8>, offset: u64, n:u64): u64 {
+    can_skip(input, offset, n );
+    offset + n
+}
+
+ + + +
+ +
+Specification + + + +
pragma verify = false;
+
+ + + +
+ + + +## Function `skip_u64_vector` + + + +
public fun skip_u64_vector(input: &vector<u8>, offset: u64): u64
+
+ + + +
+Implementation + + +
public fun skip_u64_vector(input: &vector<u8>, offset: u64): u64 {
+    let (len, new_offset) = deserialize_len(input, offset);
+    can_skip(input, new_offset, len * 8);
+    new_offset + len * 8
+}
+
+ + + +
+ +
+Specification + + + +
pragma verify = false;
+
+ + + +
+ + + +## Function `skip_u128_vector` + + + +
public fun skip_u128_vector(input: &vector<u8>, offset: u64): u64
+
+ + + +
+Implementation + + +
public fun skip_u128_vector(input: &vector<u8>, offset: u64): u64 {
+    let (len, new_offset) = deserialize_len(input, offset);
+    can_skip(input, new_offset, len * 16);
+    new_offset + len * 16
+}
+
+ + + +
+ +
+Specification + + + +
pragma verify = false;
+
+ + + +
+ + + +## Function `skip_u256` + + + +
public fun skip_u256(input: &vector<u8>, offset: u64): u64
+
+ + + +
+Implementation + + +
public fun skip_u256(input: &vector<u8>, offset: u64): u64 {
+    can_skip(input, offset, 32 );
+    offset + 32
+}
+
+ + + +
+ +
+Specification + + + +
pragma verify = false;
+
+ + + +
+ + + +## Function `skip_u128` + + + +
public fun skip_u128(input: &vector<u8>, offset: u64): u64
+
+ + + +
+Implementation + + +
public fun skip_u128(input: &vector<u8>, offset: u64): u64 {
+    can_skip(input, offset, 16 );
+    offset + 16
+}
+
+ + + +
+ +
+Specification + + + +
pragma verify = false;
+
+ + + +
+ + + +## Function `skip_u64` + + + +
public fun skip_u64(input: &vector<u8>, offset: u64): u64
+
+ + + +
+Implementation + + +
public fun skip_u64(input: &vector<u8>, offset: u64): u64 {
+    can_skip(input, offset, 8 );
+    offset + 8
+}
+
+ + + +
+ +
+Specification + + + +
pragma verify = false;
+
+ + + +
+ + + +## Function `skip_u32` + + + +
public fun skip_u32(input: &vector<u8>, offset: u64): u64
+
+ + + +
+Implementation + + +
public fun skip_u32(input: &vector<u8>, offset: u64): u64 {
+    can_skip(input, offset, 4 );
+    offset + 4
+}
+
+ + + +
+ +
+Specification + + + +
pragma verify = false;
+
+ + + +
+ + + +## Function `skip_u16` + + + +
public fun skip_u16(input: &vector<u8>, offset: u64): u64
+
+ + + +
+Implementation + + +
public fun skip_u16(input: &vector<u8>, offset: u64): u64 {
+    can_skip(input, offset, 2 );
+    offset + 2
+}
+
+ + + +
+ +
+Specification + + + +
pragma verify = false;
+
+ + + +
+ + + +## Function `skip_address` + + + +
public fun skip_address(input: &vector<u8>, offset: u64): u64
+
+ + + +
+Implementation + + +
public fun skip_address(input: &vector<u8>, offset: u64): u64 {
+    skip_n_bytes(input, offset, 16)
+}
+
+ + + +
+ +
+Specification + + + +
pragma verify = false;
+
+ + + +
+ + + +## Function `skip_bool` + + + +
public fun skip_bool(input: &vector<u8>, offset: u64): u64
+
+ + + +
+Implementation + + +
public fun skip_bool(input: &vector<u8>, offset: u64):  u64{
+    can_skip(input, offset, 1);
+    offset + 1
+}
+
+ + + +
+ +
+Specification + + + +
pragma verify = false;
+
+ + + +
+ + + +## Function `can_skip` + + + +
fun can_skip(input: &vector<u8>, offset: u64, n: u64)
+
+ + + +
+Implementation + + +
fun can_skip(input: &vector<u8>, offset: u64, n: u64){
+    assert!(((offset + n) <= Vector::length(input)) && (offset < offset + n), Errors::invalid_state(ERR_INPUT_NOT_LARGE_ENOUGH));
 }
 
diff --git a/build/StarcoinFramework/source_maps/BCS.mvsm b/build/StarcoinFramework/source_maps/BCS.mvsm index d0a81bc0..08a694ec 100644 Binary files a/build/StarcoinFramework/source_maps/BCS.mvsm and b/build/StarcoinFramework/source_maps/BCS.mvsm differ diff --git a/sources/BCS.move b/sources/BCS.move index 3b44a3d6..139117d7 100644 --- a/sources/BCS.move +++ b/sources/BCS.move @@ -310,33 +310,6 @@ module BCS { assert!(!d, 1015); } - public fun deserialize_uleb128_as_u32(input: &vector, offset: u64): (u64, u64) { - let value: u64 = 0; - let shift = 0; - let new_offset = offset; - while (shift < 32) { - let x = get_byte(input, new_offset); - new_offset = new_offset + 1; - let digit: u8 = x & 0x7F; - value = value | (digit as u64) << shift; - if ((value < 0) || (value > INTEGER32_MAX_VALUE)) { - abort ERR_OVERFLOW_PARSING_ULEB128_ENCODED_UINT32 - }; - if (digit == x) { - if (shift > 0 && digit == 0) { - abort ERR_INVALID_ULEB128_NUMBER_UNEXPECTED_ZERO_DIGIT - }; - return (value, new_offset) - }; - shift = shift + 7 - }; - abort ERR_OVERFLOW_PARSING_ULEB128_ENCODED_UINT32 - } - - spec deserialize_uleb128_as_u32 { - pragma verify = false; - } - fun get_byte(input: &vector, offset: u64): u8 { assert!(((offset + 1) <= Vector::length(input)) && (offset < offset + 1), Errors::invalid_state(ERR_INPUT_NOT_LARGE_ENOUGH)); *Vector::borrow(input, offset) @@ -379,6 +352,33 @@ module BCS { pragma verify = false; } + public fun deserialize_uleb128_as_u32(input: &vector, offset: u64): (u64, u64) { + let value: u64 = 0; + let shift = 0; + let new_offset = offset; + while (shift < 32) { + let x = get_byte(input, new_offset); + new_offset = new_offset + 1; + let digit: u8 = x & 0x7F; + value = value | (digit as u64) << shift; + if ((value < 0) || (value > INTEGER32_MAX_VALUE)) { + abort ERR_OVERFLOW_PARSING_ULEB128_ENCODED_UINT32 + }; + if (digit == x) { + if (shift > 0 && digit == 0) { + abort ERR_INVALID_ULEB128_NUMBER_UNEXPECTED_ZERO_DIGIT + }; + return (value, new_offset) + }; + shift = shift + 7 + }; + abort ERR_OVERFLOW_PARSING_ULEB128_ENCODED_UINT32 + } + + spec deserialize_uleb128_as_u32 { + pragma verify = false; + } + #[test] public fun test_deserialize_uleb128_as_u32() { let i: u64 = 0x7F; @@ -427,5 +427,269 @@ module BCS { pragma verify = false; } + // skip Vector>> + public fun skip_option_bytes_vector(input: &vector, offset: u64): u64 { + let (len, new_offset) = deserialize_len(input, offset); + let i = 0; + while (i < len) { + new_offset = skip_option_bytes(input, new_offset); + i = i + 1; + }; + new_offset + } + + spec skip_option_bytes_vector { + pragma verify = false; + } + + #[test] + fun test_skip_option_bytes_vector(){ + let vec = Vector::empty>>(); + Vector::push_back(&mut vec, Option::some(x"01020304")); + Vector::push_back(&mut vec, Option::some(x"04030201")); + let vec = to_bytes(&vec); + //vec : [2, 1, 4, 1, 2, 3, 4, 1, 4, 4, 3, 2, 1] + assert!(skip_option_bytes_vector(&vec, 0) == 13,2000); + } + + // skip Option::Option> + public fun skip_option_bytes(input: &vector, offset: u64): u64 { + let (tag, new_offset) = deserialize_option_tag(input, offset); + if (!tag) { + new_offset + } else { + skip_bytes(input, new_offset) + } + } + + spec skip_option_bytes { + pragma verify = false; + } + + #[test] + fun test_skip_none_option_bytes(){ + let op = Option::none>(); + let op = to_bytes(&op); + let vec = to_bytes(&x"01020304"); + Vector::append(&mut op, vec); + // op : [0, 4, 1, 2, 3, 4] + assert!(skip_option_bytes(&op, 0) == 1,2007); + } + + #[test] + fun test_skip_some_option_bytes(){ + let op = Option::some(x"01020304"); + let op = to_bytes(&op); + let vec = to_bytes(&x"01020304"); + Vector::append(&mut op, vec); + // op : [1, 4, 1, 2, 3, 4, 4, 1, 2, 3, 4] + assert!(skip_option_bytes(&op, 0) == 6,2008); + } + + // skip vector> + public fun skip_bytes_vector(input: &vector, offset: u64): u64 { + let (len, new_offset) = deserialize_len(input, offset); + let i = 0; + while (i < len) { + new_offset = skip_bytes(input, new_offset); + i = i + 1; + }; + new_offset + } + + spec skip_bytes_vector { + pragma verify = false; + } + + // skip vector + public fun skip_bytes(input: &vector, offset: u64): u64 { + let (len, new_offset) = deserialize_len(input, offset); + new_offset + len + } + + spec skip_bytes { + pragma verify = false; + } + + #[test] + fun test_skip_bytes(){ + let vec = to_bytes(&x"01020304"); + let u_64 = to_bytes(&10); + Vector::append(&mut vec, u_64); + // vec : [4, 1, 2, 3, 4, 10, 0, 0, 0, 0, 0, 0, 0] + assert!(skip_bytes(&vec, 0) == 5,2001); + } + + // skip some bytes + public fun skip_n_bytes(input: &vector, offset: u64, n:u64): u64 { + can_skip(input, offset, n ); + offset + n + } + + spec skip_n_bytes { + pragma verify = false; + } + + #[test] + fun test_skip_n_bytes(){ + let vec = to_bytes(&x"01020304"); + let u_64 = to_bytes(&10); + Vector::append(&mut vec, u_64); + // vec : [4, 1, 2, 3, 4, 10, 0, 0, 0, 0, 0, 0, 0] + assert!(skip_n_bytes(&vec, 0, 1) == 1,2002); + } + + // skip vector + public fun skip_u64_vector(input: &vector, offset: u64): u64 { + let (len, new_offset) = deserialize_len(input, offset); + can_skip(input, new_offset, len * 8); + new_offset + len * 8 + } + + spec skip_u64_vector { + pragma verify = false; + } + + #[test] + fun test_skip_u64_vector(){ + let vec = Vector::empty(); + Vector::push_back(&mut vec, 11111); + Vector::push_back(&mut vec, 22222); + let u_64 = to_bytes(&10); + let vec = to_bytes(&vec); + Vector::append(&mut vec, u_64); + // vec : [2, 103, 43, 0, 0, 0, 0, 0, 0, 206, 86, 0, 0, 0, 0, 0, 0, 10, 0, 0, 0, 0, 0, 0, 0] + assert!(skip_u64_vector(&vec, 0) == 17,2004); + } + + // skip vector + public fun skip_u128_vector(input: &vector, offset: u64): u64 { + let (len, new_offset) = deserialize_len(input, offset); + can_skip(input, new_offset, len * 16); + new_offset + len * 16 + } + + spec skip_u128_vector { + pragma verify = false; + } + + #[test] + fun test_skip_u128_vector(){ + let vec = Vector::empty(); + Vector::push_back(&mut vec, 11111); + Vector::push_back(&mut vec, 22222); + let u_64 = to_bytes(&10); + let vec = to_bytes(&vec); + Vector::append(&mut vec, u_64); + // vec : [2, 103, 43, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 206, 86, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 10, 0, 0, 0, 0, 0, 0, 0] + assert!(skip_u128_vector(&vec, 0) == 33,2003); + } + + // skip u256 + public fun skip_u256(input: &vector, offset: u64): u64 { + can_skip(input, offset, 32 ); + offset + 32 + } + + spec skip_u256 { + pragma verify = false; + } + + // skip u128 + public fun skip_u128(input: &vector, offset: u64): u64 { + can_skip(input, offset, 16 ); + offset + 16 + } + + spec skip_u128 { + pragma verify = false; + } + + #[test] + fun test_skip_u128(){ + let u_128:u128 = 100; + let u_128 = to_bytes(&u_128); + let vec = to_bytes(&x"01020304"); + Vector::append(&mut u_128, vec); + // u_128 : [100, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 1, 2, 3, 4] + assert!(skip_u128(&u_128, 0) == 16,2005); + } + + // skip u64 + public fun skip_u64(input: &vector, offset: u64): u64 { + can_skip(input, offset, 8 ); + offset + 8 + } + + spec skip_u64 { + pragma verify = false; + } + + #[test] + fun test_skip_u64(){ + let u_64:u64 = 100; + let u_64 = to_bytes(&u_64); + let vec = to_bytes(&x"01020304"); + Vector::append(&mut u_64, vec); + // u_64 : [100, 0, 0, 0, 0, 0, 0, 0, 4, 1, 2, 3, 4] + assert!(skip_u64(&u_64, 0) == 8,2006); + } + + // skip u32 + public fun skip_u32(input: &vector, offset: u64): u64 { + can_skip(input, offset, 4 ); + offset + 4 + } + + spec skip_u32 { + pragma verify = false; + } + + // skip u16 + public fun skip_u16(input: &vector, offset: u64): u64 { + can_skip(input, offset, 2 ); + offset + 2 + } + + spec skip_u16 { + pragma verify = false; + } + + // skip address + public fun skip_address(input: &vector, offset: u64): u64 { + skip_n_bytes(input, offset, 16) + } + + spec skip_address { + pragma verify = false; + } + + #[test] + fun test_address(){ + let addr:address = @0x1; + let addr = to_bytes(&addr); + let vec = to_bytes(&x"01020304"); + Vector::append(&mut addr, vec); + // addr : [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 4, 1, 2, 3, 4] + assert!(skip_address(&addr, 0) == 16,2006); + } + + // skip bool + public fun skip_bool(input: &vector, offset: u64): u64{ + can_skip(input, offset, 1); + offset + 1 + } + + spec skip_bool { + pragma verify = false; + } + + fun can_skip(input: &vector, offset: u64, n: u64){ + assert!(((offset + n) <= Vector::length(input)) && (offset < offset + n), Errors::invalid_state(ERR_INPUT_NOT_LARGE_ENOUGH)); + } + + spec can_skip { + pragma verify = false; + } } }