Implement applicative recursion fact registry

.github/workflows/applicative_recursion_formatting_and_testing.yml

@@ -0,0 +1,26 @@
+name: Applicative Recursion - Formatting & Testing
+
+on:
+  push:
+  pull_request:
+
+jobs:
+  applicative-recursion-formatting-and-testing:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v3
+
+      - name: Setup Scarb
+        uses: software-mansion/setup-scarb@v1
+
+      - name: Setup Snfoundry
+        uses: foundry-rs/setup-snfoundry@v4
+
+      - name: Format code
+        run: scarb fmt -c
+        working-directory: ./applicative_recursion
+
+      - name: Run tests
+        run: scarb test
+        working-directory: ./applicative_recursion

.github/workflows/tests.yml → .github/workflows/formatting_and_testing.yml

@@ -1,4 +1,4 @@
-name: Continuous Integration - tests
+name: Formatting & Testing
 
 on:
   push:
@@ -13,9 +13,12 @@ jobs:
 
       - name: Setup Scarb
         uses: software-mansion/setup-scarb@v1
+
+      - name: Setup Snfoundry
+        uses: foundry-rs/setup-snfoundry@v4
 
       - name: Format code
-        run: scarb fmt --check
+        run: scarb fmt -w src -c
 
       - name: Run tests
         run: scarb test

.github/workflows/proof_verification_tests.yml

@@ -1,35 +1,35 @@
-name: Continuous Integration - proof verification tests
+name: Proof Verification Tests
 
 on:
-    push:
-        branches:
-            - main
-    pull_request:
-        branches:
-            - main
+  push:
+    branches:
+      - main
+  pull_request:
+    branches:
+      - main
 
 jobs:
-    verify-example-proofs:
-        runs-on: ubuntu-latest
-        strategy:
-            matrix:
-                memory_verification: ['cairo0', 'cairo1']
-                layout: ['recursive', 'recursive_with_poseidon', 'small', 'dex', 'starknet', 'starknet_with_keccak']
-                hash_function: ['keccak']
-                hasher_bit_length: ['160_lsb']
-                stone_version: ['stone5']
-        steps:
-            - name: Checkout repository
-              uses: actions/checkout@v3
+  proof-verification-tests:
+    runs-on: ubuntu-latest
+    strategy:
+      matrix:
+        memory_verification: ['cairo0', 'cairo1']
+        layout: ['recursive', 'recursive_with_poseidon', 'small', 'dex', 'starknet', 'starknet_with_keccak']
+        hash_function: ['keccak']
+        hasher_bit_length: ['160_lsb']
+        stone_version: ['stone5']
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v3
 
-            - name: Setup Scarb
-              uses: software-mansion/setup-scarb@v1
+      - name: Setup Scarb
+        uses: software-mansion/setup-scarb@v1
 
-            - name: Setup Rust toolchain
-              uses: actions-rust-lang/setup-rust-toolchain@v1
+      - name: Setup Rust toolchain
+        uses: actions-rust-lang/setup-rust-toolchain@v1
 
-            - name: Build project
-              run: scarb build --no-default-features --features monolith,${{ matrix.layout }},${{ matrix.hash_function }}
+      - name: Build project
+        run: scarb build --no-default-features --features monolith,${{ matrix.layout }},${{ matrix.hash_function }}
 
-            - name: Run verification
-              run: cargo run --release --bin runner -- --program target/dev/integrity.sierra.json --memory-verification ${{ matrix.memory_verification == 'cairo0' && 'strict' || 'cairo1' }} --stone-version ${{ matrix.stone_version }} --hasher-bit-length ${{ matrix.hasher_bit_length }} < examples/proofs/${{ matrix.layout }}/${{ matrix.memory_verification }}_${{ matrix.stone_version }}_${{ matrix.hash_function }}_${{ matrix.hasher_bit_length }}_example_proof.json
+      - name: Run verification
+        run: cargo run --release --bin runner -- --program target/dev/integrity.sierra.json --memory-verification ${{ matrix.memory_verification == 'cairo0' && 'strict' || 'cairo1' }} --stone-version ${{ matrix.stone_version }} --hasher-bit-length ${{ matrix.hasher_bit_length }} < examples/proofs/${{ matrix.layout }}/${{ matrix.memory_verification }}_${{ matrix.stone_version }}_${{ matrix.hash_function }}_${{ matrix.hasher_bit_length }}_example_proof.json

.tool-versions

@@ -1,2 +1,2 @@
-scarb 2.8.4
-starknet-foundry 0.32.0
+scarb 2.11.4
+starknet-foundry 0.41.0

Scarb.toml

@@ -9,10 +9,10 @@ license = "Apache-2.0"
 keywords = ["STARK proof", "verifier", "cairo_verifier"]
 
 [dependencies]
-starknet = "2.8.4"
+starknet = "2.11.4"
 
 [dev-dependencies]
-cairo_test = "2.8.4"
+snforge_std = "0.41.0"
 
 [[target.starknet-contract]]
 casm = true
@@ -22,6 +22,9 @@ casm = true
 sierra = true
 casm = false
 
+[scripts]
+test = "snforge test"
+
 [features]
 
 _verifier_logic = []

applicative_recursion/.gitignore

@@ -0,0 +1 @@
+target

applicative_recursion/Scarb.toml

@@ -0,0 +1,26 @@
+[package]
+name = "applicative_recursion"
+version = "1.0.0"
+edition = "2024_07"
+
+# See more keys and their definitions at https://docs.swmansion.com/scarb/docs/reference/manifest.html
+
+openzeppelin_merkle_tree = "2.0.0-alpha.0"
+
+[dependencies]
+starknet = "2.9.4"
+openzeppelin = { git = "https://github.com/OpenZeppelin/cairo-contracts.git", tag = "v2.0.0-alpha.0" }
+integrity = { path = "../" }
+
+[dev-dependencies]
+cairo_test = "2.11.4"
+snforge_std = "0.41.0"
+
+[scripts]
+test = "snforge test"
+
+[tool.scarb]
+allow-prebuilt-plugins = ["snforge_std"]
+
+[[target.starknet-contract]]
+build-external-contracts = ["integrity::contracts::mocked_fact_registry::MockedFactRegistry"]

applicative_recursion/deploy.toml

@@ -0,0 +1,15 @@
+[[call]]
+call_type = "deploy"
+class_hash = "0x0553da7f80b8672f3b6aebc8b23eba313c036a2aa2809839270ee59b8cb16f6a"
+inputs = [
+    "0x2697ab2f3631993e735ca0e5a8b526b42210f87a3ab0d84276e05ea469f942a", # bootloader program hash
+    "0x675d09dc6a5a1a2317bee3abcc05074881553e0b88c05c646f384b924aa6445", # aggregator program hash
+    "0x4ce7851f00b6c3289674841fd7a1b96b6fd41ed1edc248faccd672c26371b8c", # integrity address
+    "0x7265637572736976655f776974685f706f736569646f6e", # layout
+    "0x6b656363616b5f3136305f6c7362", # hasher
+    "0x73746f6e6536", # stone version
+    "0x72656c61786564", # memory verification
+    "0x60" # security bits
+]
+id = "deploy"
+unique = false

applicative_recursion/snfoundry.toml

@@ -0,0 +1,4 @@
+[sncast.default]
+accounts-file = "~/.starknet_accounts/starknet_open_zeppelin_accounts.json"
+account = "my-sepolia-account"
+url = "https://free-rpc.nethermind.io/sepolia-juno/v0_8"

applicative_recursion/src/fact_registry.cairo

@@ -0,0 +1,132 @@
+#[starknet::interface]
+pub trait IApplicativeRecursionFactRegistry<TContractState> {
+    fn decommit_leaf(ref self: TContractState, leaf: felt252, proof: Span<felt252>);
+    fn decommit_tree(ref self: TContractState, leaves: Span<felt252>);
+
+    fn is_valid(self: @TContractState, fact_hash: felt252) -> bool;
+}
+
+#[starknet::contract]
+pub mod ApplicativeRecursionFactRegistry {
+    use applicative_recursion::merkle_tree::{get_root_hash, hash_leaf, hash_leaves};
+    use integrity::{
+        Integrity, IntegrityWithConfig, SHARP_BOOTLOADER_PROGRAM_HASH, VerifierConfiguration,
+        calculate_bootloaded_fact_hash, get_verifier_config_hash,
+    };
+    use openzeppelin::merkle_tree::hashes::PoseidonCHasher;
+    use openzeppelin::merkle_tree::merkle_proof::process_proof;
+    use starknet::ContractAddress;
+    use starknet::storage::{
+        Map, StoragePathEntry, StoragePointerReadAccess, StoragePointerWriteAccess,
+    };
+    use super::IApplicativeRecursionFactRegistry;
+
+    #[storage]
+    struct Storage {
+        bootloader_program_hash: felt252,
+        aggregator_program_hash: felt252,
+        integrity_address: ContractAddress,
+        integrity_config_hash: felt252,
+        integrity_security_bits: u32,
+        fact_hashes: Map<felt252, bool>,
+    }
+
+    #[constructor]
+    fn constructor(
+        ref self: ContractState,
+        bootloader_program_hash: felt252,
+        aggregator_program_hash: felt252,
+        integrity_address: ContractAddress,
+        integrity_config: VerifierConfiguration,
+        integrity_security_bits: u32,
+    ) {
+        self.bootloader_program_hash.write(bootloader_program_hash);
+        self.aggregator_program_hash.write(aggregator_program_hash);
+        self.integrity_address.write(integrity_address);
+        self.integrity_config_hash.write(get_verifier_config_hash(integrity_config));
+        self.integrity_security_bits.write(integrity_security_bits);
+    }
+
+    #[event]
+    #[derive(Drop, starknet::Event)]
+    enum Event {
+        FactRegistered: FactRegistered,
+    }
+
+    #[derive(Drop, starknet::Event)]
+    struct FactRegistered {
+        #[key]
+        fact_hash: felt252,
+        #[key]
+        root_hash: felt252,
+        #[key]
+        integrity_fact_hash: felt252,
+    }
+
+    #[generate_trait]
+    impl ApplicativeRecursionFactRegistryInternal of IApplicativeRecursionFactRegistryInternal {
+        fn get_fact_hash(self: @ContractState, root_hash: felt252) -> felt252 {
+            let output = [self.aggregator_program_hash.read(), root_hash, 0x0].span();
+            let program_hash = self.bootloader_program_hash.read();
+
+            calculate_bootloaded_fact_hash(SHARP_BOOTLOADER_PROGRAM_HASH, program_hash, output)
+        }
+
+        fn is_fact_hash_valid(self: @ContractState, fact_hash: felt252) -> bool {
+            let integrity = Integrity::from_address(self.integrity_address.read());
+
+            let config_hash = self.integrity_config_hash.read();
+            let security_bits = self.integrity_security_bits.read();
+
+            integrity.with_hashed_config(config_hash, security_bits).is_fact_hash_valid(fact_hash)
+        }
+    }
+
+    #[abi(embed_v0)]
+    impl ApplicativeRecursionFactRegistryImpl of IApplicativeRecursionFactRegistry<ContractState> {
+        fn decommit_leaf(ref self: ContractState, leaf: felt252, proof: Span<felt252>) {
+            let hashed_leaf = hash_leaf(leaf);
+            let root_hash = process_proof::<PoseidonCHasher>(proof, hashed_leaf);
+
+            let fact_hash = self.get_fact_hash(root_hash);
+            let is_valid = self.is_fact_hash_valid(fact_hash);
+            assert(is_valid, 'Fact hash is not registered');
+
+            self.fact_hashes.entry(leaf).write(true);
+            self
+                .emit(
+                    Event::FactRegistered(
+                        FactRegistered {
+                            fact_hash: leaf, root_hash, integrity_fact_hash: fact_hash,
+                        },
+                    ),
+                );
+        }
+
+        fn decommit_tree(ref self: ContractState, leaves: Span<felt252>) {
+            let hashed_leaves = hash_leaves(leaves);
+            let root_hash = get_root_hash(hashed_leaves);
+
+            let fact_hash = self.get_fact_hash(root_hash);
+            let is_valid = self.is_fact_hash_valid(fact_hash);
+            assert(is_valid, 'Fact hash is not registered');
+
+            for leaf in leaves {
+                self.fact_hashes.entry(*leaf).write(true);
+
+                self
+                    .emit(
+                        Event::FactRegistered(
+                            FactRegistered {
+                                fact_hash: *leaf, root_hash, integrity_fact_hash: fact_hash,
+                            },
+                        ),
+                    );
+            }
+        }
+
+        fn is_valid(self: @ContractState, fact_hash: felt252) -> bool {
+            self.fact_hashes.entry(fact_hash).read()
+        }
+    }
+}

applicative_recursion/src/lib.cairo

@@ -0,0 +1,2 @@
+pub mod fact_registry;
+pub mod merkle_tree;

applicative_recursion/src/merkle_tree.cairo

@@ -0,0 +1,64 @@
+use core::hash::HashStateTrait;
+use core::poseidon::PoseidonTrait;
+use openzeppelin::merkle_tree::hashes::PoseidonCHasher;
+
+pub fn get_root_hash(leaves: Span<felt252>) -> felt252 {
+    let mut nodes = leaves;
+    let mut next_nodes = array![];
+    loop {
+        loop {
+            let x = nodes.pop_front();
+            if x.is_none() {
+                break;
+            }
+            let x = x.unwrap();
+
+            if let Some(y) = nodes.pop_front() {
+                let z = PoseidonCHasher::commutative_hash(*x, *y);
+                next_nodes.append(z);
+            } else {
+                next_nodes.append(*x);
+            };
+        }
+        nodes = next_nodes.span();
+        next_nodes = array![];
+
+        if nodes.len() == 1 {
+            break *nodes.pop_front().unwrap();
+        }
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::get_root_hash;
+
+    #[test]
+    fn test_root_hash() {
+        let leaf_1 = 1073156302979560792221579174510302617030152323580472146146609514826389505953;
+        let leaf_2 = 3480373627587233544730874138440391736870787221204167186361820851772543726392;
+        let leaf_3 = 3331964270381854350382580527122817180649953314104348840989537158202691620591;
+        let leaf_4 = 663603216509782636457470027552452500581997608842766641099217590049269815062;
+        let leaf_5 = 3561455703173699215459883981864709246532730017982956264444923577051119991603;
+
+        let expected_root = 0x1ffc48eb9b02993240241d49908bc3d3ad0e21b7a9ab2b2b6b2efa1c1fd93ef;
+
+        let leaves = [leaf_1, leaf_2, leaf_3, leaf_4, leaf_5];
+        let root = get_root_hash(leaves.span());
+
+        assert(root == expected_root, 'root hash mismatch');
+    }
+}
+
+pub fn hash_leaf(leaf: felt252) -> felt252 {
+    PoseidonTrait::new().update(leaf).finalize()
+}
+
+pub fn hash_leaves(leaves: Span<felt252>) -> Span<felt252> {
+    let mut result = array![];
+    for leaf in leaves {
+        let hash = hash_leaf(*leaf);
+        result.append(hash);
+    }
+    result.span()
+}