harden message claims and retry handling

.github/workflows/ci.yml

@@ -49,13 +49,10 @@ jobs:
           mkdir -p ~/.local/share/tlaplus
           curl -sL -o ~/.local/share/tlaplus/tla2tools.jar \
             https://github.com/tlaplus/tlaplus/releases/latest/download/tla2tools.jar
-      # This audit pass proves bugs exist in CURRENT code and proves correct
-      # fix designs for them - the fixes are NOT yet applied to the Rust code
-      # (see node/README.md's "Known gap" sections). These configs model the
-      # verified fix designs (or a baseline that was never buggy) and must
-      # always pass. See root README.md's "Formal verification (TLA+)"
-      # section for what each spec covers.
-      - name: Run baseline + proposed-fix specs (must pass)
+      # These configs model the implemented fixes (or a baseline that was
+      # never buggy) and must always pass. The separate configs below retain
+      # the pre-fix counterexamples as historical regression documentation.
+      - name: Run baseline + fixed specs (must pass)
         working-directory: node/tla
         run: |
           set -e
@@ -152,7 +149,7 @@ jobs:
         run: sudo apt update && sudo apt install protobuf-compiler
       - run: |
           source ~/.zkm-toolchain/env
-          cargo clippy --all-targets -- -D warnings
+          cargo clippy --all-targets --features rpc-debug-endpoints -- -D warnings
   test:
     name: Cargo Test
     needs: tla-plus
@@ -173,4 +170,4 @@ jobs:
         run: |
           set -e
           source ~/.zkm-toolchain/env
-          cargo test -r --all --all-targets
+          cargo test -r --all --all-targets --features rpc-debug-endpoints

.gitignore

@@ -38,6 +38,7 @@ proof-builder-rpc/*.ckpt
 node/tla/states/
 
 local_docs/
+local_scripts/
 scripts/testnet/
 scripts/devnet/
 *.DS_Store

Cargo.toml

@@ -10,6 +10,7 @@ members = [
     "crates/cbft-rpc",
     "crates/bitvm-gc",
     "crates/store",
+    "crates/node-macros",
     "crates/client",
     "crates/util",
     "crates/header-chain",

crates/bitvm-gc/src/timelocks.rs

@@ -155,6 +155,7 @@ pub fn validate_timelock_config(network: Network, config: &TimelockConfig) -> Re
         ("operator_commit", config.operator_commit),
         ("connector_f", config.connector_f),
     ] {
+        ensure_bip68_height_based_sequence(name, value)?;
         if value < budget.reaction_blocks {
             bail!(
                 "timelock_config.{name} must be at least {} reaction blocks, got {value}",
@@ -210,6 +211,17 @@ pub fn validate_timelock_config(network: Network, config: &TimelockConfig) -> Re
     Ok(())
 }
 
+const BIP68_BLOCKS_MASK: u32 = 0x0000_ffff;
+
+fn ensure_bip68_height_based_sequence(name: &str, value: u32) -> Result<()> {
+    if value & !BIP68_BLOCKS_MASK != 0 {
+        bail!(
+            "timelock_config.{name} must use a BIP68 height-based sequence value, got {value:#010x}"
+        );
+    }
+    Ok(())
+}
+
 fn ensure_gap_at_least(
     left_name: &str,
     left: u32,
@@ -291,4 +303,14 @@ mod tests {
             validate_timelock_config(network, &config).unwrap();
         }
     }
+
+    #[test]
+    fn rejects_non_height_based_bip68_sequences() {
+        assert!(ensure_bip68_height_based_sequence("test", BIP68_BLOCKS_MASK).is_ok());
+
+        for invalid in [1 << 16, 1 << 22, 1 << 31] {
+            let error = ensure_bip68_height_based_sequence("test", invalid).unwrap_err();
+            assert!(error.to_string().contains("BIP68 height-based sequence"));
+        }
+    }
 }

crates/node-macros/Cargo.toml

@@ -0,0 +1,12 @@
+[package]
+name = "node-macros"
+version.workspace = true
+edition.workspace = true
+
+[lib]
+proc-macro = true
+
+[dependencies]
+proc-macro2 = "1"
+quote = "1"
+syn = { version = "2", features = ["full"] }

crates/node-macros/src/lib.rs

@@ -0,0 +1,210 @@
+use proc_macro::TokenStream;
+use quote::quote;
+use syn::spanned::Spanned;
+use syn::{Attribute, Data, DeriveInput, Fields, Ident, Meta, Result, Variant, parse_macro_input};
+
+#[proc_macro_derive(MessageBusinessRef, attributes(business_ref))]
+pub fn derive_message_business_ref(input: TokenStream) -> TokenStream {
+    let input = parse_macro_input!(input as DeriveInput);
+    match expand_message_business_ref(input) {
+        Ok(tokens) => tokens.into(),
+        Err(error) => error.into_compile_error().into(),
+    }
+}
+
+fn expand_message_business_ref(input: DeriveInput) -> Result<proc_macro2::TokenStream> {
+    let enum_name = input.ident;
+    let Data::Enum(data) = input.data else {
+        return Err(syn::Error::new(
+            enum_name.span(),
+            "MessageBusinessRef can only be derived for enums",
+        ));
+    };
+
+    let match_arms = data.variants.iter().map(expand_variant).collect::<Result<Vec<_>>>()?;
+
+    Ok(quote! {
+        impl HasBusinessRef for #enum_name {
+            fn business_ref(&self) -> BusinessRef {
+                match self {
+                    #(#match_arms),*
+                }
+            }
+        }
+    })
+}
+
+fn expand_variant(variant: &Variant) -> Result<proc_macro2::TokenStream> {
+    let scope = business_ref_scope(variant)?;
+    let variant_name = &variant.ident;
+
+    match scope.as_str() {
+        "graph" => {
+            let binding = tuple_payload_binding(variant)?;
+            Ok(quote! {
+                Self::#variant_name(#binding) => BusinessRef::Graph {
+                    instance_id: #binding.instance_id,
+                    graph_id: #binding.graph_id,
+                }
+            })
+        }
+        "instance" => {
+            let binding = tuple_payload_binding(variant)?;
+            Ok(quote! {
+                Self::#variant_name(#binding) => BusinessRef::Instance {
+                    instance_id: #binding.instance_id,
+                }
+            })
+        }
+        "unscoped" => match &variant.fields {
+            Fields::Unit => Ok(quote! {
+                Self::#variant_name => BusinessRef::Unscoped
+            }),
+            Fields::Unnamed(_) => Ok(quote! {
+                Self::#variant_name(..) => BusinessRef::Unscoped
+            }),
+            Fields::Named(_) => Ok(quote! {
+                Self::#variant_name { .. } => BusinessRef::Unscoped
+            }),
+        },
+        _ => unreachable!("business_ref_scope validates accepted values"),
+    }
+}
+
+fn tuple_payload_binding(variant: &Variant) -> Result<Ident> {
+    match &variant.fields {
+        Fields::Unnamed(fields) if fields.unnamed.len() == 1 => {
+            Ok(Ident::new("message", variant.span()))
+        }
+        _ => Err(syn::Error::new(
+            variant.span(),
+            "graph and instance business references require exactly one payload field",
+        )),
+    }
+}
+
+fn business_ref_scope(variant: &Variant) -> Result<String> {
+    let mut matching = variant
+        .attrs
+        .iter()
+        .filter(|attribute: &&Attribute| attribute.path().is_ident("business_ref"));
+    let Some(attribute) = matching.next() else {
+        // Point at the offending variant rather than the derive site, so the
+        // compiler error names the variant that lacks an attribute.
+        return Err(syn::Error::new(
+            variant.ident.span(),
+            "each message variant must declare #[business_ref(graph)], #[business_ref(instance)], or #[business_ref(unscoped)]",
+        ));
+    };
+    if matching.next().is_some() {
+        return Err(syn::Error::new(attribute.span(), "duplicate business_ref attribute"));
+    }
+
+    let Meta::List(list) = &attribute.meta else {
+        return Err(syn::Error::new(
+            attribute.span(),
+            "business_ref must be written as #[business_ref(graph)], #[business_ref(instance)], or #[business_ref(unscoped)]",
+        ));
+    };
+    let scope: Ident = list.parse_args()?;
+    let scope = scope.to_string();
+    if matches!(scope.as_str(), "graph" | "instance" | "unscoped") {
+        Ok(scope)
+    } else {
+        Err(syn::Error::new(attribute.span(), "business_ref must be graph, instance, or unscoped"))
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use syn::parse_quote;
+
+    fn expand_error(input: DeriveInput) -> String {
+        expand_message_business_ref(input).unwrap_err().to_string()
+    }
+
+    #[test]
+    fn rejects_non_enum_input() {
+        let input = parse_quote! {
+            struct Message;
+        };
+
+        assert_eq!(expand_error(input), "MessageBusinessRef can only be derived for enums");
+    }
+
+    #[test]
+    fn requires_a_business_ref_scope_for_every_variant() {
+        let input = parse_quote! {
+            enum Message {
+                Missing(Payload),
+            }
+        };
+
+        assert_eq!(
+            expand_error(input),
+            "each message variant must declare #[business_ref(graph)], #[business_ref(instance)], or #[business_ref(unscoped)]"
+        );
+    }
+
+    #[test]
+    fn rejects_invalid_or_duplicate_scopes() {
+        let invalid = parse_quote! {
+            enum Message {
+                #[business_ref(other)]
+                Invalid(Payload),
+            }
+        };
+        assert_eq!(expand_error(invalid), "business_ref must be graph, instance, or unscoped");
+
+        let duplicate = parse_quote! {
+            enum Message {
+                #[business_ref(graph)]
+                #[business_ref(instance)]
+                Duplicate(Payload),
+            }
+        };
+        assert_eq!(expand_error(duplicate), "duplicate business_ref attribute");
+    }
+
+    #[test]
+    fn graph_and_instance_scopes_require_one_tuple_payload() {
+        let named = parse_quote! {
+            enum Message {
+                #[business_ref(graph)]
+                Graph { payload: Payload },
+            }
+        };
+        assert_eq!(
+            expand_error(named),
+            "graph and instance business references require exactly one payload field"
+        );
+
+        let multiple = parse_quote! {
+            enum Message {
+                #[business_ref(instance)]
+                Instance(Payload, Payload),
+            }
+        };
+        assert_eq!(
+            expand_error(multiple),
+            "graph and instance business references require exactly one payload field"
+        );
+    }
+
+    #[test]
+    fn accepts_all_unscoped_variant_shapes() {
+        let input = parse_quote! {
+            enum Message {
+                #[business_ref(unscoped)]
+                Unit,
+                #[business_ref(unscoped)]
+                Tuple(u8, u16),
+                #[business_ref(unscoped)]
+                Named { value: u8 },
+            }
+        };
+
+        assert!(expand_message_business_ref(input).is_ok());
+    }
+}

crates/node-macros/tests/message_business_ref.rs

@@ -0,0 +1,47 @@
+use node_macros::MessageBusinessRef;
+
+#[derive(Debug, Eq, PartialEq)]
+enum BusinessRef {
+    Instance { instance_id: u64 },
+    Graph { instance_id: u64, graph_id: u64 },
+    Unscoped,
+}
+
+trait HasBusinessRef {
+    fn business_ref(&self) -> BusinessRef;
+}
+
+struct Payload {
+    instance_id: u64,
+    graph_id: u64,
+}
+
+#[allow(dead_code)]
+#[derive(MessageBusinessRef)]
+enum Message {
+    #[business_ref(graph)]
+    Graph(Payload),
+    #[business_ref(instance)]
+    Instance(Payload),
+    #[business_ref(unscoped)]
+    Unit,
+    #[business_ref(unscoped)]
+    Tuple(u8, u16),
+    #[business_ref(unscoped)]
+    Named { value: u8 },
+}
+
+#[test]
+fn derives_the_expected_business_reference_for_every_scope() {
+    assert_eq!(
+        Message::Graph(Payload { instance_id: 7, graph_id: 11 }).business_ref(),
+        BusinessRef::Graph { instance_id: 7, graph_id: 11 }
+    );
+    assert_eq!(
+        Message::Instance(Payload { instance_id: 7, graph_id: 11 }).business_ref(),
+        BusinessRef::Instance { instance_id: 7 }
+    );
+    assert_eq!(Message::Unit.business_ref(), BusinessRef::Unscoped);
+    assert_eq!(Message::Tuple(1, 2).business_ref(), BusinessRef::Unscoped);
+    assert_eq!(Message::Named { value: 1 }.business_ref(), BusinessRef::Unscoped);
+}