Skip to content

Commit

Permalink
Merge branch 'next' into plafer-1584-event-handlers
Browse files Browse the repository at this point in the history
  • Loading branch information
plafer committed Feb 3, 2025
2 parents 4b27efd + 80cd4ce commit 745293e
Show file tree
Hide file tree
Showing 14 changed files with 319 additions and 119 deletions.
1 change: 1 addition & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -29,6 +29,7 @@
- Optimized the computation of the DEEP queries in the recursive verifier (#1594).
- Added validity checks for the inputs to the recursive verifier (#1596).
- Allow multiple memory reads in the same clock cycle (#1626)
- Improved Falcon signiture verification (#1623).

## 0.11.0 (2024-11-04)

Expand Down
2 changes: 1 addition & 1 deletion assembly/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -44,7 +44,7 @@ let program = assembler.assemble_program(&Path::new("./example.masm")).unwrap();
As noted above, the default assembler is instantiated with nothing in it but
the source code you provide. If you want to support more complex programs, you
will want to factor code into libraries and modules, and then link all of them
together at once. This can be acheived using a set of builder methods of the
together at once. This can be achieved using a set of builder methods of the
`Assembler` struct, e.g. `with_kernel_from_module`, `with_library`, etc.

We'll look at a few of these in more detail below. See the module documentation
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 @@ -29,6 +30,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 @@ -52,6 +54,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 @@ -55,6 +55,7 @@ extern {
"push_mtnode" => Token::PushMtnode,
"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 @@ -675,6 +676,7 @@ SystemEvent: Instruction = {
"adv" "." "push_mtnode" => Instruction::SysEvent(SystemEventNode::PushMtNode),
"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 @@ -152,6 +152,7 @@ pub enum Token<'input> {
PushSmtset,
PushSmtget,
PushU64Div,
PushFalconDiv,
And,
Assert,
Assertz,
Expand Down Expand Up @@ -336,6 +337,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 @@ -528,6 +530,7 @@ impl<'input> Token<'input> {
| Token::PushSmtset
| Token::PushSmtget
| Token::PushU64Div
| Token::PushFalconDiv
| Token::And
| Token::Assert
| Token::Assertz
Expand Down Expand Up @@ -672,6 +675,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
21 changes: 21 additions & 0 deletions core/src/sys_events.rs
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,8 @@ mod constants {
pub const EVENT_HDWORD_TO_MAP: u32 = 2391452729;
pub const EVENT_HDWORD_TO_MAP_WITH_DOMAIN: u32 = 2822590340;
pub const EVENT_HPERM_TO_MAP: u32 = 3297060969;
// TODO(plafer): Move this to stdlib
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 @@ -117,6 +119,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 @@ -293,6 +311,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 @@ -317,6 +336,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 @@ -348,6 +368,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
2 changes: 1 addition & 1 deletion docs/src/user_docs/assembly/code_organization.md
Original file line number Diff line number Diff line change
Expand Up @@ -181,7 +181,7 @@ Miden assembly supports constant declarations. These constants are scoped to the

Constants must be declared right after module imports and before any procedures or program bodies. A constant's name must start with an upper-case letter and can contain any combination of numbers, upper-case ASCII letters, and underscores (`_`). The number of characters in a constant name cannot exceed 100.

A constant's value must be in a decimal or hexidecimal form and be in the range between $0$ and $2^{64} - 2^{32}$ (both inclusive). Value can be defined by an arithmetic expression using `+`, `-`, `*`, `/`, `//`, `(`, `)` operators and references to the previously defined constants if it uses only decimal numbers. Here `/` is a field division and `//` is an integer division. Note that the arithmetic expression cannot contain spaces.
A constant's value must be in a decimal or hexadecimal form and be in the range between $0$ and $2^{64} - 2^{32}$ (both inclusive). Value can be defined by an arithmetic expression using `+`, `-`, `*`, `/`, `//`, `(`, `)` operators and references to the previously defined constants if it uses only decimal numbers. Here `/` is a field division and `//` is an integer division. Note that the arithmetic expression cannot contain spaces.

```
use.std::math::u64
Expand Down
2 changes: 1 addition & 1 deletion processor/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -52,7 +52,7 @@ The processor is organized into several components:
* The range-checker, which is responsible for checking whether values can fit into 16 bits.
* The chiplets module, which contains specialized chiplets responsible for handling complex computations (e.g., hashing) as well as random access memory.

These components are connected via two busses:
These components are connected via two buses:
* The range-checker bus, which links stack and chiplets modules with the range-checker.
* The chiplet bus, which links stack and the decoder with the chiplets module.

Expand Down
42 changes: 42 additions & 0 deletions processor/src/operations/sys_ops/sys_event_handlers.rs
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,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_system_event(
&self,
Expand All @@ -38,6 +41,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 @@ -338,6 +342,44 @@ 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, remainder) = (dividend / M, dividend % 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 745293e

Please sign in to comment.