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

Improve Falcon DSA verification procedure #1623

Open
wants to merge 5 commits into
base: next
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
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
1 change: 1 addition & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@
- Added `miden_core::mast::MastForest::advice_map` to load it into the advice provider before the `MastForest` execution (#1574).
- Optimized the computation of the DEEP queries in the recursive verifier (#1594).
- Added validity checks for the inputs to the recursive verifier (#1596).
- Improved Falcon signiture verification (#1623).

## 0.11.0 (2024-11-04)

Expand Down
3 changes: 3 additions & 0 deletions assembly/src/ast/instruction/advice.rs
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ use vm_core::sys_events::SystemEvent;
#[derive(Clone, PartialEq, Eq, Debug)]
pub enum SystemEventNode {
PushU64Div,
PushFalconDiv,
PushExt2intt,
PushSmtPeek,
PushMapVal,
Expand All @@ -30,6 +31,7 @@ impl From<&SystemEventNode> for SystemEvent {
use SystemEventNode::*;
match value {
PushU64Div => Self::U64Div,
PushFalconDiv => Self::FalconDiv,
PushExt2intt => Self::Ext2Intt,
PushSmtPeek => Self::SmtPeek,
PushMapVal => Self::MapValueToStack,
Expand All @@ -56,6 +58,7 @@ impl fmt::Display for SystemEventNode {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
match self {
Self::PushU64Div => write!(f, "push_u64div"),
Self::PushFalconDiv => write!(f, "push_falcon_div"),
Self::PushExt2intt => write!(f, "push_ext2intt"),
Self::PushSmtPeek => write!(f, "push_smtpeek"),
Self::PushMapVal => write!(f, "push_mapval"),
Expand Down
2 changes: 2 additions & 0 deletions assembly/src/parser/grammar.lalrpop
Original file line number Diff line number Diff line change
Expand Up @@ -56,6 +56,7 @@ extern {
"push_sig" => Token::PushSig,
"push_smtpeek" => Token::PushSmtpeek,
"push_u64div" => Token::PushU64Div,
"push_falcon_div" => Token::PushFalconDiv,
"and" => Token::And,
"assert" => Token::Assert,
"assertz" => Token::Assertz,
Expand Down Expand Up @@ -677,6 +678,7 @@ SystemEvent: Instruction = {
"adv" "." "push_sig" "." <kind:SignatureKind> => Instruction::SysEvent(SystemEventNode::PushSignature { kind }),
"adv" "." "push_smtpeek" => Instruction::SysEvent(SystemEventNode::PushSmtPeek),
"adv" "." "push_u64div" => Instruction::SysEvent(SystemEventNode::PushU64Div),
"adv" "." "push_falcon_div" => Instruction::SysEvent(SystemEventNode::PushFalconDiv),
}

#[inline]
Expand Down
4 changes: 4 additions & 0 deletions assembly/src/parser/token.rs
Original file line number Diff line number Diff line change
Expand Up @@ -153,6 +153,7 @@ pub enum Token<'input> {
PushSmtset,
PushSmtget,
PushU64Div,
PushFalconDiv,
And,
Assert,
Assertz,
Expand Down Expand Up @@ -338,6 +339,7 @@ impl fmt::Display for Token<'_> {
Token::PushSmtset => write!(f, "push_smtset"),
Token::PushSmtget => write!(f, "push_smtget"),
Token::PushU64Div => write!(f, "push_u64div"),
Token::PushFalconDiv => write!(f, "push_falcon_div"),
Token::And => write!(f, "and"),
Token::Assert => write!(f, "assert"),
Token::Assertz => write!(f, "assertz"),
Expand Down Expand Up @@ -531,6 +533,7 @@ impl<'input> Token<'input> {
| Token::PushSmtset
| Token::PushSmtget
| Token::PushU64Div
| Token::PushFalconDiv
| Token::And
| Token::Assert
| Token::Assertz
Expand Down Expand Up @@ -676,6 +679,7 @@ impl<'input> Token<'input> {
("push_smtset", Token::PushSmtset),
("push_smtget", Token::PushSmtget),
("push_u64div", Token::PushU64Div),
("push_falcon_div", Token::PushFalconDiv),
("and", Token::And),
("assert", Token::Assert),
("assertz", Token::Assertz),
Expand Down
2 changes: 1 addition & 1 deletion core/src/debuginfo/source_file.rs
Original file line number Diff line number Diff line change
Expand Up @@ -515,7 +515,7 @@ impl SourceContent {
///
/// Returns `None` if the given index is out of bounds
pub fn line_start(&self, line_index: LineIndex) -> Option<ByteIndex> {
self.line_starts.get(line_index.to_usize()).copied().map(ByteIndex::from)
self.line_starts.get(line_index.to_usize()).copied()
}

/// Returns the index of the last line in this file
Expand Down
2 changes: 2 additions & 0 deletions core/src/mast/serialization/tests.rs
Original file line number Diff line number Diff line change
Expand Up @@ -356,6 +356,8 @@ fn mast_forest_invalid_node_id() {

// Hydrate a forest larger than the first to get an overflow MastNodeId
let mut overflow_forest = MastForest::new();

#[allow(clippy::double_ended_iterator_last)]
let overflow = (0..=3)
.map(|_| overflow_forest.add_block(vec![Operation::U32div], None).unwrap())
.last()
Expand Down
20 changes: 20 additions & 0 deletions core/src/sys_events.rs
Original file line number Diff line number Diff line change
Expand Up @@ -28,6 +28,7 @@ mod constants {
pub const EVENT_HDWORD_TO_MAP_WITH_DOMAIN: u32 = 2822590340;
pub const EVENT_HPERM_TO_MAP: u32 = 3297060969;
pub const EVENT_FALCON_SIG_TO_STACK: u32 = 3419226139;
pub const EVENT_FALCON_DIV: u32 = 3419226155;
}

/// Defines a set of actions which can be initiated from the VM to inject new data into the advice
Expand Down Expand Up @@ -119,6 +120,22 @@ pub enum SystemEvent {
/// the remainder respectively.
U64Div,

/// Pushes the result of divison (both the quotient and the remainder) of a [u64] by the Falcon
/// prime (M = 12289) onto the advice stack.
///
/// Inputs:
/// Operand stack: [a1, a0, ...]
/// Advice stack: [...]
///
/// Outputs:
/// Operand stack: [a1, a0, ...]
/// Advice stack: [q0, q1, r, ...]
///
/// Where (a0, a1) are the 32-bit limbs of the dividend (with a0 representing the 32 least
/// significant bits and a1 representing the 32 most significant bits).
/// Similarly, (q0, q1) represent the quotient and r the remainder.
FalconDiv,

/// Given an element in a quadratic extension field on the top of the stack (i.e., a0, b1),
/// computes its multiplicative inverse and push the result onto the advice stack.
///
Expand Down Expand Up @@ -310,6 +327,7 @@ impl SystemEvent {
SystemEvent::MapValueToStack => EVENT_MAP_VALUE_TO_STACK,
SystemEvent::MapValueToStackN => EVENT_MAP_VALUE_TO_STACK_N,
SystemEvent::U64Div => EVENT_U64_DIV,
SystemEvent::FalconDiv => EVENT_FALCON_DIV,
SystemEvent::Ext2Inv => EVENT_EXT2_INV,
SystemEvent::Ext2Intt => EVENT_EXT2_INTT,
SystemEvent::SmtPeek => EVENT_SMT_PEEK,
Expand All @@ -335,6 +353,7 @@ impl SystemEvent {
EVENT_MAP_VALUE_TO_STACK => Some(SystemEvent::MapValueToStack),
EVENT_MAP_VALUE_TO_STACK_N => Some(SystemEvent::MapValueToStackN),
EVENT_U64_DIV => Some(SystemEvent::U64Div),
EVENT_FALCON_DIV => Some(SystemEvent::FalconDiv),
EVENT_EXT2_INV => Some(SystemEvent::Ext2Inv),
EVENT_EXT2_INTT => Some(SystemEvent::Ext2Intt),
EVENT_SMT_PEEK => Some(SystemEvent::SmtPeek),
Expand Down Expand Up @@ -367,6 +386,7 @@ impl fmt::Display for SystemEvent {
Self::MapValueToStack => write!(f, "map_value_to_stack"),
Self::MapValueToStackN => write!(f, "map_value_to_stack_with_len"),
Self::U64Div => write!(f, "div_u64"),
Self::FalconDiv => write!(f, "falcon_div"),
Self::Ext2Inv => write!(f, "ext2_inv"),
Self::Ext2Intt => write!(f, "ext2_intt"),
Self::SmtPeek => write!(f, "smt_peek"),
Expand Down
43 changes: 43 additions & 0 deletions processor/src/operations/sys_ops/sys_event_handlers.rs
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,9 @@ use crate::{
/// The offset of the domain value on the stack in the `hdword_to_map_with_domain` system event.
const HDWORD_TO_MAP_WITH_DOMAIN_DOMAIN_OFFSET: usize = 8;

/// Falcon signature prime.
const M: u64 = 12289;

impl Process {
pub(super) fn handle_sytem_event(
&self,
Expand All @@ -39,6 +42,7 @@ impl Process {
copy_map_value_to_adv_stack(advice_provider, process_state, true)
},
SystemEvent::U64Div => push_u64_div_result(advice_provider, process_state),
SystemEvent::FalconDiv => push_falcon_mod_result(advice_provider, process_state),
SystemEvent::Ext2Inv => push_ext2_inv_result(advice_provider, process_state),
SystemEvent::Ext2Intt => push_ext2_intt_result(advice_provider, process_state),
SystemEvent::SmtPeek => push_smtpeek_result(advice_provider, process_state),
Expand Down Expand Up @@ -342,6 +346,45 @@ pub fn push_u64_div_result(
Ok(())
}

/// Pushes the result of divison (both the quotient and the remainder) of a [u64] by the Falcon
/// prime (M = 12289) onto the advice stack.
///
/// Inputs:
/// Operand stack: [a1, a0, ...]
/// Advice stack: [...]
///
/// Outputs:
/// Operand stack: [a1, a0, ...]
/// Advice stack: [q1, q0, r, ...]
///
/// Where (a0, a1) are the 32-bit limbs of the dividend (with a0 representing the 32 least
/// significant bits and a1 representing the 32 most significant bits).
/// Similarly, (q0, q1) represent the quotient and r the remainder.
///
/// # Errors
/// Returns an error if the divisor is ZERO.
pub fn push_falcon_mod_result(
advice_provider: &mut impl AdviceProvider,
process: ProcessState,
) -> Result<(), ExecutionError> {
let dividend_hi = process.get_stack_item(0).as_int();
let dividend_lo = process.get_stack_item(1).as_int();
let dividend = (dividend_hi << 32) + dividend_lo;

let quotient = dividend / M;
let remainder = dividend - quotient * M;

let (q_hi, q_lo) = u64_to_u32_elements(quotient);
let (r_hi, r_lo) = u64_to_u32_elements(remainder);
assert_eq!(r_hi, ZERO);

advice_provider.push_stack(AdviceSource::Value(r_lo))?;
advice_provider.push_stack(AdviceSource::Value(q_lo))?;
advice_provider.push_stack(AdviceSource::Value(q_hi))?;

Ok(())
}

/// Given an element in a quadratic extension field on the top of the stack (i.e., a0, b1),
/// computes its multiplicative inverse and push the result onto the advice stack.
///
Expand Down
Loading
Loading