Skip to content

Commit

Permalink
feat: improve Falcon signature verification
Browse files Browse the repository at this point in the history
  • Loading branch information
Al-Kindi-0 committed Jan 14, 2025
1 parent 8420dcd commit ba8239d
Show file tree
Hide file tree
Showing 7 changed files with 252 additions and 84 deletions.
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
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: [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.
///
/// # 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

0 comments on commit ba8239d

Please sign in to comment.