Merge pull request #992 from 0xPolygonMiden/tohrnii-nested-modules

feat: add support for nested modules

CHANGELOG.md

@@ -4,6 +4,7 @@
 
 #### Assembly
 - Added ability to attach doc comments to re-exported procedures (#994).
+- Added support for nested modules (#992).
 
 #### VM Internals
 - Simplified range checker and removed 1 main and 1 auxiliary trace column (#949).

assembly/src/library/masl.rs

@@ -62,6 +62,8 @@ impl MaslLibrary {
     pub const LIBRARY_EXTENSION: &str = "masl";
     /// File extension for the Assembly Module.
     pub const MODULE_EXTENSION: &str = "masm";
+    /// Name of the root module.
+    pub const MOD: &str = "mod";
 
     // CONSTRUCTOR
     // --------------------------------------------------------------------------------------------
@@ -156,6 +158,14 @@ mod use_std {
             let module_path = LibraryPath::new(&namespace)
                 .map_err(|err| io::Error::new(io::ErrorKind::Other, format!("{err}")))?;
 
+            // mod.masm is not allowed in the root directory
+            if path.as_ref().join("mod.masm").exists() {
+                return Err(io::Error::new(
+                    io::ErrorKind::Other,
+                    "mod.masm is not allowed in the root directory",
+                ));
+            }
+
             let modules = read_from_dir_helper(
                 Default::default(),
                 path,
@@ -246,6 +256,17 @@ mod use_std {
                         io::Error::new(io::ErrorKind::Other, "invalid directory entry!")
                     })?;
 
+                    // check if a directory with the same name exists in the directory
+                    if path.with_file_name(name).is_dir() {
+                        return Err(io::Error::new(
+                            io::ErrorKind::Other,
+                            format!(
+                                "file and directory with the same name '{}' are not allowed",
+                                name
+                            ),
+                        ));
+                    }
+
                     // read & parse file
                     let contents = fs::read_to_string(&path)?;
                     let ast = ModuleAst::parse(&contents)?;
@@ -257,9 +278,14 @@ mod use_std {
                     }
 
                     // build module path and add it to the map of modules
-                    let module = module_path
-                        .append(name)
-                        .map_err(|err| io::Error::new(io::ErrorKind::Other, format!("{err}")))?;
+                    let module = if name == MaslLibrary::MOD {
+                        module_path.clone()
+                    } else {
+                        module_path
+                            .append(name)
+                            .map_err(|err| io::Error::new(io::ErrorKind::Other, format!("{err}")))?
+                    };
+
                     if state.insert(module, ast).is_some() {
                         unreachable!(
                             "the filesystem is inconsistent as it produced duplicated module paths"

assembly/src/library/path.rs

@@ -203,7 +203,7 @@ impl LibraryPath {
             .path
             .rsplit_once(Self::PATH_DELIM)
             .expect("failed to split path on module delimiter")
-            .1;
+            .0;
 
         Ok(Self {
             path: rem.to_string(),

stdlib/asm/crypto/stark/mod.masm

@@ -0,0 +1,26 @@
+use.std::crypto::stark::verifier
+
+#!   Verify a STARK proof attesting to the correct execution of a program in the Miden VM.
+#!   The following simplifying assumptions are currently made:
+#!   - The blowup is set to 8.
+#!   - The maximal allowed degree of the remainder polynomial is 7.
+#!   - Only the input and output stacks, assumed of fixed size equal to 16, are handled in regards
+#!   to public inputs.
+#!   - There are two trace segments, main and auxiliary. It is assumed that the main trace segment
+#!   is 73 columns wide while the auxiliary trace segment is 9 columns wide.
+#!   - The OOD evaluation frame is composed of two interleaved rows, current and next, each composed
+#!    of 73 elements representing the main trace portion and 9 elements for the auxiliary trace one.
+#!   - To boost soundness, the protocol is run on a quadratic extension field and this means that
+#!    the OOD evaluation frame is composed of elements in a quadratic extension field i.e. tuples.
+#!    Similarly, elements of the auxiliary trace are quadratic extension field elements.
+#!   - The following procedure makes use of global memory address beyond 3 * 2^30 and these are
+#!    defined in `constants.masm`.
+#!
+#! Input: [log(trace_length), num_queries, log(blowup), grinding]
+#! Output: []
+#! Cycles:
+#!  1- Remainder codeword size 32:
+#!   5000 + num_queries * (40 + num_fri_layers * 76 + 26 + 463) + 83 * num_fri_layers + 10 * log(trace_length) + 1633
+#!  2- Remainder codeword size 64:
+#!   5000 + num_queries * (40 + num_fri_layers * 76 + 26 + 463) + 83 * num_fri_layers + 10 * log(trace_length) + 3109
+export.verifier::verify

stdlib/build.rs

@@ -55,7 +55,7 @@ trait Renderer {
     fn render(stdlib: &ModuleMap, output_dir: &str);
 }
 
-// Writes Miden standard library modules documentation markdown files based on the available modules and comments.
+/// Writes Miden standard library modules documentation markdown files based on the available modules and comments.
 pub fn build_stdlib_docs(module_map: &ModuleMap, output_dir: &str) {
     // Remove functions folder to re-generate
     fs::remove_dir_all(output_dir).unwrap();

stdlib/docs/crypto/stark.md

@@ -0,0 +1,5 @@
+
+## std::crypto::stark
+| Procedure | Description |
+| ----------- | ------------- |
+| verify | Verify a STARK proof attesting to the correct execution of a program in the Miden VM.<br /><br />The following simplifying assumptions are currently made:<br /><br />- The blowup is set to 8.<br /><br />- The maximal allowed degree of the remainder polynomial is 7.<br /><br />- Only the input and output stacks, assumed of fixed size equal to 16, are handled in regards<br /><br />to public inputs.<br /><br />- There are two trace segments, main and auxiliary. It is assumed that the main trace segment<br /><br />is 73 columns wide while the auxiliary trace segment is 9 columns wide.<br /><br />- The OOD evaluation frame is composed of two interleaved rows, current and next, each composed<br /><br />of 73 elements representing the main trace portion and 9 elements for the auxiliary trace one.<br /><br />- To boost soundness, the protocol is run on a quadratic extension field and this means that<br /><br />the OOD evaluation frame is composed of elements in a quadratic extension field i.e. tuples.<br /><br />Similarly, elements of the auxiliary trace are quadratic extension field elements.<br /><br />- The following procedure makes use of global memory address beyond 3 * 2^30 and these are<br /><br />defined in `constants.masm`.<br /><br />Input: [log(trace_length), num_queries, log(blowup), grinding]<br /><br />Output: []<br /><br />Cycles:<br /><br />1- Remainder codeword size 32:<br /><br />5000 + num_queries * (40 + num_fri_layers * 76 + 26 + 463) + 83 * num_fri_layers + 10 * log(trace_length) + 1633<br /><br />2- Remainder codeword size 64:<br /><br />5000 + num_queries * (40 + num_fri_layers * 76 + 26 + 463) + 83 * num_fri_layers + 10 * log(trace_length) + 3109 |