Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

refactoring the ics23 spec #975

Open
wants to merge 27 commits into
base: main
Choose a base branch
from
Open
Changes from 1 commit
Commits
Show all changes
27 commits
Select commit Hold shift + click to select a range
9a079cd
refactor the ICS23 spec
konnov Jun 20, 2023
52419f0
ignore empty leaf keys
konnov Jun 20, 2023
aa20aba
lowcase definitions and remove isTree
konnov Jun 20, 2023
446f4d3
clean up the specs
konnov Jun 20, 2023
bbf3f44
fix the test
konnov Jun 20, 2023
c13f256
symbolic hashing
konnov Jun 20, 2023
33bc57d
fix the comments
konnov Jun 21, 2023
8534b5e
rename words to hashes
konnov Jun 21, 2023
89f1559
refactoring the spec
konnov Jun 21, 2023
99c6fe7
refactored hashes, ics23, and ics23 tests
konnov Jun 22, 2023
c690426
uncomment one test
konnov Jun 22, 2023
db92c4c
fix all the tests in ics23test
konnov Jun 23, 2023
b2334dd
clean unneeded files and update the readme
konnov Jun 23, 2023
b81495c
Apply suggestions from code review
konnov Jun 23, 2023
60a2df4
apply comments and fix the spec
konnov Jun 23, 2023
4bcb8eb
fix lessThan
konnov Jun 23, 2023
de4cc26
fix the type error in termConcat
konnov Jul 6, 2023
2335cf9
fixing tests
konnov Jul 6, 2023
3813404
fix all but one test
konnov Jul 6, 2023
8ff175a
Merge branch 'main' into igor/ics23-fix
konnov Sep 4, 2023
2baba60
Merge remote-tracking branch 'origin/main' into igor/ics23-fix
bugarela Sep 10, 2024
ac11ff5
Fix command on README
bugarela Sep 10, 2024
c9f8ca0
Use a sum type to represent term nodes
bugarela Sep 10, 2024
2eea315
Merge remote-tracking branch 'origin/main' into igor/ics23-fix
bugarela Dec 11, 2024
f2f5e2d
Refactor and generalize to any spec
bugarela Dec 20, 2024
1115a51
Fix proof generation
bugarela Dec 20, 2024
5734cb4
Add stronger invariant
bugarela Dec 20, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
refactoring the spec
  • Loading branch information
konnov authored and thpani committed Jul 26, 2023
commit 89f15591b93351c4e30e01378ae569b1673b020c
37 changes: 30 additions & 7 deletions examples/cosmos/ics23/hashes.qnt
Original file line number Diff line number Diff line change
@@ -31,9 +31,12 @@
/// [ 1 ] -> { t: "r", b: [ 5, 6 ] })
///
/// Igor Konnov, Informal Systems, 2022-2023
module words {
module hashes {
/// A sequence of bytes is simply a list of integers
type BYTES_T = List[int]

/// compare two lists of integers (e.g., bytes) lexicographically
pure def lessThan(w1: List[int], w2: List[int]): bool = {
pure def lessThan(w1: BYTES_T, w2: BYTES_T): bool = {
pure val len1 = length(w1)
pure val len2 = length(w2)
or {
@@ -53,16 +56,25 @@ module words {
// node type: either "h" (for hash), or "r" (for raw sequence)
t: str,
// the bytes when t = "r", and [] when t = "h"
b: List[int]
b: BYTES_T
}

/// A word is a map from a path to the term node.
/// The first root's child is [ 0 ], the second root's child is [ 1 ],
/// the first child of [ 0 ] is [ 0, 0], etc.
type TERM_T = List[int] -> TERM_NODE_T
type TERM_T = BYTES_T -> TERM_NODE_T

/// Compute term length in bytes,
/// assuming that a hash occupies 32 bytes (as SHA256 does)
pure def termLen(term: TERM_T): int = {
// the root's children
pure val top =
keys(term).filter(p => length(p) == 1).map(p => term.get(p))
top.fold(0, (s, t) => if (t.t == "h") s + 32 else s + length(t.b))
}

// Construct the term that encodes a raw sequence of bytes
konnov marked this conversation as resolved.
Show resolved Hide resolved
pure def raw(bytes: List[int]): TERM_T = {
pure def raw(bytes: BYTES_T): TERM_T = {
Map([ 0 ] -> { t: "r", b: bytes })
}

@@ -72,7 +84,7 @@ module words {
}

// Hash a term
konnov marked this conversation as resolved.
Show resolved Hide resolved
pure def hash(term: TERM_T): TERM_T = {
pure def termHash(term: TERM_T): TERM_T = {
// add "h" on top, which has the key [ 0 ], and attach term to it
pure val paths = Set([ 0 ]).union(keys(term).map(p => [ 0 ].concat(p)))
paths.mapBy(p =>
@@ -86,7 +98,7 @@ module words {

/// Concatenate two terms. Special attention is paid to the case when the
/// both terms are raw sequences, which requires them to be merged.
pure def plus(left: TERM_T, right: TERM_T): TERM_T = {
pure def termConcat(left: TERM_T, right: TERM_T): TERM_T = {
pure val l = left.get([0])
pure val r = right.get([0])
if (size(keys(left)) == 1 and size(keys(right)) == 1 and l.t == "r" and r.t == "r") {
@@ -111,4 +123,15 @@ module words {
)
}
}

// Slice the sequence represented by a term.
// We only slice raw sequences.
konnov marked this conversation as resolved.
Show resolved Hide resolved
pure def termSlice(term: TERM_T, start: int, end: int): TERM_T = {
pure val first = term.get([ 0 ])
if (size(keys(term)) == 1 and first.t == "r") {
raw(first.b.slice(start, end))
} else {
term
}
}
}
92 changes: 46 additions & 46 deletions examples/cosmos/ics23/ics23.qnt
Original file line number Diff line number Diff line change
@@ -18,49 +18,47 @@
//
// https://github.com/confio/ics23/blob/master/go/proof.go
module ics23 {
import words.* from "./words"
import hashes.* from "./hashes"

// ICS23 proof checking for IavlSpec.
// In contrast to the ICS32 implementation, we specialize it to binary trees:
// In contrast to the ICS23 implementation, we specialize it to binary trees:
// https://github.com/confio/ics23/tree/master/go

// type aliases for readability
type KEY_T = WORD_T
type VALUE_T = WORD_T
type CommitmentRoot_T = WORD_T
type CommitmentProof_T = WORD_T
type KEY_T = TERM_T
type VALUE_T = TERM_T
type CommitmentRoot_T = TERM_T
type CommitmentProof_T = TERM_T

// ICS23 IavlSpec has:
// MinPrefixLength = 4
// MaxPrefixLength = 12
// ChildSize = 33
//
// To ease spec testing, we set:
val MinPrefixLen = 1
val MaxPrefixLen = 2
pure val MinPrefixLen = 1
pure val MaxPrefixLen = 2
// It is crucial to make sure that ChildSize > MaxPrefixLen
val ChildSize = 3 // with length byte
pure val ChildSize = 33 // 32 bytes in SHA256 + 1 byte for length
// Empty child is a predefined sequence that fills an absent child.
val EmptyChild = [ 0, 0, 0 ]

/// We need a hash that returns ChildSize elements,
/// with 32 being in the head.
/// For simulation, we are just summing up the word elements modulo 8.
/// For verification, we should use an injective function as a perfect hash.
def hash(word) = [ 32, 0, word.foldl(0, (i, j) => i + j) % 8 ]
// TODO: EmptyChild is set to nil in IavlSpec. We have 33 bytes.
pure val EmptyChild = raw([
32, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
])

type LEAF_T = {
// The implementation additionally stores hashing and length functions:
// hash, prehashKey, prehashValue, len. Since we fix the spec to IAVL,
// we do not have to carry them around.
prefix: WORD_T
prefix: TERM_T
}

type INNER_T = {
// The implementation additionally stores the hashing function.
// Since we fix the spec to IAVL, we do not have to carry it around.
prefix: WORD_T,
suffix: WORD_T
prefix: TERM_T,
suffix: TERM_T
}

/// a proof of existence of (key, value)
@@ -74,20 +72,21 @@ module ics23 {
}

/// calculate a hash from an exists proof
def existsCalculate(p):
(ExistsProof_T) => CommitmentProof_T = {
def existsCalculate(p: ExistsProof_T): CommitmentProof_T = {
// This is how the leaf hash is computed.
// Notice that the key is not hashed.
val leafHash =
hash(p.leaf.prefix
.append(length(p.key))
.concat(p.key)
.append(length(p.value))
.concat(hash(p.value)))
termHash(p.leaf.prefix
// TODO: use encodeVarintProto
konnov marked this conversation as resolved.
Show resolved Hide resolved
.termConcat(raw([termLen(p.key)]))
.termConcat(p.key)
.termConcat(raw([32]))
.termConcat(termHash(p.value)))

// the inner node nodeHashes are concatenated and hashed upwards
p.path.foldl(leafHash,
(child, inner) => hash(inner.prefix.concat(child).concat(inner.suffix)))
(child, inner) =>
termHash(inner.prefix.termConcat(child).termConcat(inner.suffix)))
}

/// verify that a proof matches a root
@@ -101,8 +100,8 @@ module ics23 {
/// proof is an ExistenceProof for the given key and value AND
/// calculating the root for the ExistenceProof matches
/// the provided CommitmentRoot
def verifyMembership(root, proof, key, value):
(CommitmentRoot_T, ExistsProof_T, KEY_T, VALUE_T) => bool = {
def verifyMembership(root: CommitmentRoot_T,
proof: ExistsProof_T, key: KEY_T, value: VALUE_T): bool = {
// TODO: specify Decompress
// TODO: specify the case of CommitmentProof_Batch
// TODO: CheckAgainstSpec ensures that the proof can be verified
@@ -111,20 +110,21 @@ module ics23 {
}

/// checks if an op has the expected padding
def hasPadding(inner, minPrefixLen, maxPrefixLen, suffixLen) = and {
length(inner.prefix) >= minPrefixLen,
length(inner.prefix) <= maxPrefixLen,
def hasPadding(inner: INNER_T,
minPrefixLen: int, maxPrefixLen: int, suffixLen: int): bool = and {
termLen(inner.prefix) >= minPrefixLen,
termLen(inner.prefix) <= maxPrefixLen,
// When inner turns left, suffixLen == ChildSize,
// that is, we store the hash of the right child in the suffix.
// When inner turns right, suffixLen == 0,
// that is, we store the hash of the left child in the prefix.
length(inner.suffix) == suffixLen
termLen(inner.suffix) == suffixLen
}

/// This will look at the proof and determine which order it is...
/// So we can see if it is branch 0, 1, 2 etc... to determine neighbors
/// https://github.com/confio/ics23/blob/a4daeb4c24ce1be827829c0841446abc690c4f11/go/proof.go#L400-L411
def orderFromPadding(inner) = {
def orderFromPadding(inner: INNER_T): (int, bool) = {
// Specialize orderFromPadding to IavlSpec:
// ChildOrder = { 0, 1 }
// branch = 0: minp, maxp, suffix = MinPrefixLen, MaxPrefixLen, ChildSize
@@ -146,21 +146,21 @@ module ics23 {
/// leftBranchesAreEmpty returns true if the padding bytes correspond to all
/// empty siblings on the left side of a branch, ie. it's a valid placeholder
/// on a leftmost path
def leftBranchesAreEmpty(inner) = and {
def leftBranchesAreEmpty(inner: INNER_T): bool = and {
// the case of leftBranches == 0 returns false
val order = orderFromPadding(inner)
order._2 and order._1 != 0,
// the remaining case is leftBranches == 1, see orderFromPadding
// actualPrefix = len(inner.prefix) - 33
length(inner.prefix) >= ChildSize,
termLen(inner.prefix) >= ChildSize,
// getPosition(0) returns 0
val fromIndex = length(inner.prefix) - ChildSize
inner.prefix.slice(fromIndex, fromIndex + ChildSize) == EmptyChild
val fromIndex = termLen(inner.prefix) - ChildSize
termSlice(inner.prefix, fromIndex, fromIndex + ChildSize) == EmptyChild
}

/// IsLeftMost returns true if this is the left-most path in the tree,
/// excluding placeholder (empty child) nodes
def isLeftMost(path) = {
def isLeftMost(path: List[INNER_T]): bool = {
// Calls getPadding(0) => idx = 0, prefix = 0.
// We specialize the constants to IavlSpec.
path.indices().forall(i =>
@@ -177,19 +177,19 @@ module ics23 {
/// rightBranchesAreEmpty returns true if the padding bytes correspond
/// to all empty siblings on the right side of a branch,
/// i.e. it's a valid placeholder on a rightmost path
def rightBranchesAreEmpty(inner) = and {
def rightBranchesAreEmpty(inner: INNER_T): bool = and {
// the case of rightBranches == 0 returns false
val order = orderFromPadding(inner)
order._2 and order._1 != 1,
// the remaining case is rightBranches == 1, see orderFromPadding
length(inner.suffix) == ChildSize,
termLen(inner.suffix) == ChildSize,
// getPosition(0) returns 0, hence, from == 0
inner.suffix == EmptyChild
}

/// IsRightMost returns true if this is the left-most path in the tree,
/// excluding placeholder (empty child) nodes
def isRightMost(path) = {
def isRightMost(path: List[INNER_T]): bool = {
// Specialize to IavlSpec
// Calls getPadding(1) => minPrefix, maxPrefix,
// suffix = ChildSize + MinPrefixLen, ChildSize + MaxPrefixLen, 0
@@ -206,7 +206,7 @@ module ics23 {

/// isLeftStep assumes left and right have common parents
/// checks if left is exactly one slot to the left of right
def isLeftStep(left, right) = {
def isLeftStep(left: INNER_T, right: INNER_T): bool = {
// 'left' turns left, and 'right' turns right
val lorder = orderFromPadding(left)
val rorder = orderFromPadding(right)
@@ -225,7 +225,7 @@ module ics23 {
/// Validate that LPath[len-1] is the left neighbor of RPath[len-1].
/// For step in LPath[0..len-1], validate step is right-most node.
/// For step in RPath[0..len-1], validate step is left-most node.
def isLeftNeighbor(lpath, rpath) = {
def isLeftNeighbor(lpath: List[INNER_T], rpath: List[INNER_T]): bool = {
// count common tail (from end, near root)
// cut the left and right paths
lpath.indices().exists(li =>
@@ -264,8 +264,8 @@ module ics23 {
/// both left and right sub-proofs are valid existence proofs (see above) or nil
/// left and right proofs are neighbors (or left/right most if one is nil)
/// provided key is between the keys of the two proofs
def verifyNonMembership(root, np, key):
(CommitmentRoot_T, NonExistsProof_T, KEY_T) => bool = and {
def verifyNonMembership(root: CommitmentRoot_T,
np: NonExistsProof_T, key: KEY_T): bool = and {
// getNonExistProofForKey
isNil(np.left.key) or lessThan(np.left.key, key),
isNil(np.right.key) or lessThan(key, np.right.key),