diff --git a/cardano/lib/ibc/core/ics-023-vector-commitments/ics23/ops.ak b/cardano/lib/ibc/core/ics-023-vector-commitments/ics23/ops.ak index e0b41d10..95ba941b 100644 --- a/cardano/lib/ibc/core/ics-023-vector-commitments/ics23/ops.ak +++ b/cardano/lib/ibc/core/ics-023-vector-commitments/ics23/ops.ak @@ -5,9 +5,7 @@ use ibc/core/ics_023_vector_commitments/ics23/constants.{hash_op_no_hash} use ibc/core/ics_023_vector_commitments/ics23/proofs.{ HashOp, InnerOp, LeafOp, LengthOp, ProofSpec, } -use ibc/utils/bytes.{ - encode_varint, has_prefix, new_reader, read_varint, reader_len, -} +use ibc/utils/bytes.{encode_varint, has_prefix} /// apply_leaf_op() will calculate the leaf hash given the key and value being proven pub fn apply_leaf_op(op: LeafOp, key: ByteArray, value: ByteArray) -> ByteArray { @@ -73,26 +71,21 @@ fn validate_spec(spec: ProofSpec) -> Bool { /// validate_iavl_ops_leaf_op() validates the IAVL Ops with op type is LeafOp fn validate_iavl_ops_leaf_op(op: LeafOp, b: Int) -> Bool { - let r = new_reader(proofs.get_prefix_leaf_op(op)) - let iterator = - [0, 1, 2] - let (values, updated_r) = - list.reduce( - iterator, - ([], r), - fn(accum, _i) { - let (u_r, var_int) = read_varint(accum.2nd) - let next_accum_value = list.concat(accum.1st, [var_int]) - expect var_int >= 0 - (next_accum_value, u_r) - }, - ) - expect Some(values_first_ele) = list.at(values, 0) + let r = proofs.get_prefix_leaf_op(op) + + let (values_first_ele, updated_pos) = bytes.read_varint(r, 0) + expect values_first_ele >= 0 + let (value2, updated_pos) = bytes.read_varint(r, updated_pos) + expect value2 >= 0 + let (value3, updated_pos) = bytes.read_varint(r, updated_pos) + expect value3 >= 0 + expect values_first_ele >= b - let r2 = reader_len(updated_r) + + let r2 = bytearray.length(r) - updated_pos + if b == 0 { - expect r2 == 0 - True + r2 == 0 } else { // The corresponding code in the Golang version: // if !(r2^(0xff&0x01) == 0 || r2 == (0xde+int('v'))/10) { @@ -101,34 +94,27 @@ fn validate_iavl_ops_leaf_op(op: LeafOp, b: Int) -> Bool { // if op.GetHash()^1 != 0 { // return fmt.Errorf("invalid op") // } - expect !(r2 == 1 || r2 == 34) - expect op.hash == 1 - True + ( r2 == 1 || r2 == 34 ) && op.hash == 1 } } /// validate_iavl_ops_inner_op() validates the IAVL Ops with op type is InnerOp fn validate_iavl_ops_inner_op(op: InnerOp, b: Int) -> Bool { - let r = new_reader(proofs.get_prefix_inner_op(op)) - let iterator = - [0, 1, 2] - let (values, updated_r) = - list.reduce( - iterator, - ([], r), - fn(accum, _i) { - let (u_r, var_int) = read_varint(accum.2nd) - let next_accum_value = list.concat(accum.1st, [var_int]) - expect var_int >= 0 - (next_accum_value, u_r) - }, - ) - expect Some(values_first_ele) = list.at(values, 0) + let r = proofs.get_prefix_inner_op(op) + + let (values_first_ele, updated_pos) = bytes.read_varint(r, 0) + expect values_first_ele >= 0 + let (value2, updated_pos) = bytes.read_varint(r, updated_pos) + expect value2 >= 0 + let (value3, updated_pos) = bytes.read_varint(r, updated_pos) + expect value3 >= 0 + expect values_first_ele >= b - let r2 = reader_len(updated_r) + + let r2 = bytearray.length(r) - updated_pos + if b == 0 { - expect r2 == 0 - True + r2 == 0 } else { // The corresponding code in the Golang version: // if !(r2^(0xff&0x01) == 0 || r2 == (0xde+int('v'))/10) { @@ -137,9 +123,7 @@ fn validate_iavl_ops_inner_op(op: InnerOp, b: Int) -> Bool { // if op.GetHash()^1 != 0 { // return fmt.Errorf("invalid op") // } - expect !(r2 == 1 || r2 == 34) - expect op.hash == 1 - True + ( r2 == 1 || r2 == 34 ) && op.hash == 1 } } diff --git a/cardano/lib/ibc/utils/bytes.ak b/cardano/lib/ibc/utils/bytes.ak index 7fcbd29d..2ae316b0 100644 --- a/cardano/lib/ibc/utils/bytes.ak +++ b/cardano/lib/ibc/utils/bytes.ak @@ -1,90 +1,40 @@ use aiken/builtin.{ add_integer as add, divide_integer as div, if_then_else as ite, - index_bytearray, } use aiken/bytearray.{compare, length, push, slice} -use aiken/list -use ibc/utils/bits.{band, bnot_for_int64, bor, len64, shl, shr} +use ibc/utils/bits.{len64} use ibc/utils/int.{Int64} -pub const max_varint_len64: Int = 10 +fn inner_read_uvarint(bz: ByteArray, index: Int) -> (Int, Int) { + let cur_bz = builtin.index_bytearray(bz, index) -pub type Reader { - s: ByteArray, - // current reading index - i: Int, - // index of previous rune; or < 0 - prev_rune: Int, -} + let last_7_bits = cur_bz % 128 -pub fn reader_len(r: Reader) -> Int { - if r.i >= length(r.s) { - 0 - } else { - length(r.s) - r.i - } -} + let has_more_bytes = cur_bz >= 128 -pub fn new_reader(b: ByteArray) -> Reader { - Reader { s: b, i: 0, prev_rune: -1 } -} - -pub fn read_byte(r: Reader) -> (Reader, Int) { - if r.i < length(r.s) { - let updated_r = Reader { s: r.s, i: r.i + 1, prev_rune: -1 } - let b = index_bytearray(r.s, r.i) - (updated_r, b) + if !has_more_bytes { + (last_7_bits, index + 1) } else { - // EOF - (new_reader("EOF"), 0) + let res = inner_read_uvarint(bz, index + 1) + (last_7_bits + 128 * res.1st, res.2nd) } } /// read_uvarint() reads an encoded unsigned integer from r and returns it as a uint64. -pub fn read_uvarint(r: Reader) -> (Reader, Int) { - let iterator = list.range(0, max_varint_len64 - 1) - let (x, _s, updated_r) = - list.reduce( - iterator, - (0, 0, r), - fn(accum, i) { - if accum.3rd == new_reader(#[]) { - (accum.1st, 0, new_reader(#[])) - } else { - let (temp_updated_r, b) = read_byte(accum.3rd) - expect temp_updated_r != new_reader("EOF") - // check if b < 0x80 - if b < 128 { - expect !(i == max_varint_len64 - 1 && b > 1) - ( - // x | uint64(b)< (Int, Int) { + let res = inner_read_uvarint(bz, pos) - (updated_r, x) + (res.1st, res.2nd) } /// read_varint() reads an encoded signed integer from r and returns it as an int64. -pub fn read_varint(r: Reader) -> (Reader, Int) { - let (updated_r, ux) = read_uvarint(r) - let x = shr(ux, 1) - if band(ux, 1) != 0 { - (updated_r, bnot_for_int64(x)) +pub fn read_varint(r: ByteArray, pos: Int) -> (Int, Int) { + let (ux, updated_pos) = read_uvarint(r, pos) + let x = bits.shr(ux, 1) + if bits.band(ux, 1) != 0 { + (bits.bnot_for_int64(x), updated_pos) } else { - (updated_r, x) + (x, updated_pos) } } @@ -109,55 +59,14 @@ pub fn sov(x: Int64) -> Int { } //--------------------------------------Test-------------------------------------- - -test test_read_byte() { - let test_bytes = #[72, 101] - let reader_of_test_bytes = new_reader(test_bytes) - let updated_1st_reader = Reader { s: test_bytes, i: 1, prev_rune: -1 } - expect read_byte(reader_of_test_bytes) == (updated_1st_reader, 72) - let updated_2nd_reader = Reader { s: test_bytes, i: 2, prev_rune: -1 } - read_byte(updated_1st_reader) == (updated_2nd_reader, 101) -} - -test test_read_byte_when_eof() { - let test_bytes = #[72, 101] - let current_reader = Reader { s: test_bytes, i: 2, prev_rune: -1 } - read_byte(current_reader) == (new_reader("EOF"), 0) -} - test test_read_uvarint() { let test_bytes = #[129, 131, 188, 188, 181, 44, 132] - let reader_of_test_bytes = new_reader(test_bytes) - let expected_of_test_bytes = Reader { s: #[], i: 0, prev_rune: -1 } - read_uvarint(reader_of_test_bytes) == (expected_of_test_bytes, 1526182379905) -} - -test test_read_uvarint_fail_because_eof() fail { - let test_bytes = #[129, 131, 188, 188, 181, 144, 132, 159] - let reader_of_test_bytes = new_reader(test_bytes) - let expected_of_test_bytes = Reader { s: #[], i: 0, prev_rune: -1 } - read_uvarint(reader_of_test_bytes) == ( - expected_of_test_bytes, - 17469604851810689, - ) -} - -test test_read_uvarint_fail_because_overflow() fail { - // length of test_bytes >= max_varint_len64 and it's byte at index max_varint_len64 - 1 in (1, 0x80) - let test_bytes = #[129, 131, 188, 188, 181, 144, 132, 129, 242, 111] - let reader_of_test_bytes = new_reader(test_bytes) - let expected_of_test_bytes = Reader { s: #[], i: 0, prev_rune: -1 } - read_uvarint(reader_of_test_bytes) == ( - expected_of_test_bytes, - 8215146826572956033, - ) + read_uvarint(test_bytes, 0) == (1526182379905, 6) } test test_read_varint() { let test_bytes = #[129, 131, 188, 188, 181, 44, 132] - let reader_of_test_bytes = new_reader(test_bytes) - let expected_of_test_bytes = Reader { s: #[], i: 0, prev_rune: -1 } - read_varint(reader_of_test_bytes) == (expected_of_test_bytes, -763091189953) + read_varint(test_bytes, 0) == (-763091189953, 6) } test test_has_prefix() {