diff --git a/.github/workflows/verification.yml b/.github/workflows/verification.yml
index afecb1a422..f5e939f9c8 100644
--- a/.github/workflows/verification.yml
+++ b/.github/workflows/verification.yml
@@ -1,10 +1,6 @@
 name: Verification
 
-# Right now, we should only run this check on the vcalyx branch
-on:  
-  push:
-    branches:
-      - vcalyx
+on: [push]
 
 # Ensures that only the latest commit of a PR can execute the actions.
 # Useful for cancelling job when a sequence of commits are quickly added.
@@ -19,19 +15,15 @@ jobs:
     container: ghcr.io/cucapra/calyx:latest
     steps:
     - name: Checkout
-      uses: actions/checkout@v2
+      uses: actions/checkout@v3
     - name: Get bwrap for opam
       run: |
         apt-get update -y
         apt-get install -y bubblewrap
-    - name: Set up opam and OCaml 4.13.1
+    - name: Set up opam and OCaml
       uses: ocaml/setup-ocaml@v2
       with:
-          ocaml-compiler: 4.13.1
-    - name: Checkout commit that triggered run
-      run: |
-        git fetch --all
-        git checkout $GITHUB_SHA
+          ocaml-compiler: 4.14.1
     - name: Install dependencies
       run: |
         cd vcalyx
@@ -39,7 +31,19 @@ jobs:
         opam repo add coq-released https://coq.inria.fr/opam/released
         opam install . --deps-only 
         opam install coq yojson core core_unix ppx_deriving coq-stdpp coq-ceres
-    - name: Build with dune
+
+    - name: Build Rust
+      uses: actions-rs/cargo@v1
+      with:
+        command: build
+        args: --features serialize --all --manifest-path /home/calyx/interp/Cargo.toml
+
+    - name: Build Coq and OCaml
       run: |
         cd vcalyx
         opam exec -- dune build
+
+    - name: Coq Interpreter Runt Tests
+      run: |
+        cd vcalyx
+        runt --diff --only fail
diff --git a/.gitignore b/.gitignore
index ccf0b37dea..0ff8390dd3 100644
--- a/.gitignore
+++ b/.gitignore
@@ -44,5 +44,47 @@ tests/xilinx/cocotb/**/hdl
 sim_build/
 results.xml
 
+.vscode/settings.json
+
+# Dune build directory
+_build
+vcalyx.install
+# Github template for Coq .gitignores
+.*.aux
+.*.d
+*.a
+*.cma
+*.cmi
+*.cmo
+*.cmx
+*.cmxa
+*.cmxs
+*.glob
+*.ml.d
+*.ml4.d
+*.mli.d
+*.mllib.d
+*.mlpack.d
+*.native
+*.o
+*.v.d
+*.vio
+*.vo
+*.vok
+*.vos
+.coq-native/
+.csdp.cache
+.lia.cache
+.nia.cache
+.nlia.cache
+.nra.cache
+csdp.cache
+lia.cache
+nia.cache
+nlia.cache
+nra.cache
+
+# vim temporary files
+*.sw?
 
 !cider-dap/calyxDebug/package.json
diff --git a/Cargo.lock b/Cargo.lock
index 17bf05397b..ab079102f8 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -4,32 +4,33 @@ version = 3
 
 [[package]]
 name = "ahash"
-version = "0.7.6"
+version = "0.7.7"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "fcb51a0695d8f838b1ee009b3fbf66bda078cd64590202a864a8f3e8c4315c47"
+checksum = "5a824f2aa7e75a0c98c5a504fceb80649e9c35265d44525b5f94de4771a395cd"
 dependencies = [
  "getrandom",
  "once_cell",
- "version_check 0.9.4",
+ "version_check",
 ]
 
 [[package]]
 name = "ahash"
-version = "0.8.3"
+version = "0.8.7"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "2c99f64d1e06488f620f932677e24bc6e2897582980441ae90a671415bd7ec2f"
+checksum = "77c3a9648d43b9cd48db467b3f87fdd6e146bcc88ab0180006cef2179fe11d01"
 dependencies = [
  "cfg-if",
  "getrandom",
  "once_cell",
- "version_check 0.9.4",
+ "version_check",
+ "zerocopy",
 ]
 
 [[package]]
 name = "aho-corasick"
-version = "1.0.5"
+version = "1.1.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "0c378d78423fdad8089616f827526ee33c19f2fddbd5de1629152c9593ba4783"
+checksum = "b2969dcb958b36655471fc61f7e416fa76033bdd4bfed0678d8fee1e2d07a1f0"
 dependencies = [
  "memchr",
 ]
@@ -68,7 +69,7 @@ dependencies = [
  "argh_shared",
  "proc-macro2",
  "quote",
- "syn 2.0.29",
+ "syn 2.0.48",
 ]
 
 [[package]]
@@ -92,7 +93,7 @@ version = "0.2.14"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "d9b39be18770d11421cdb1b9947a45dd3f37e93092cbf377614828a319d5fee8"
 dependencies = [
- "hermit-abi 0.1.19",
+ "hermit-abi",
  "libc",
  "winapi",
 ]
@@ -111,9 +112,9 @@ checksum = "9e1b586273c5702936fe7b7d6896644d8be71e6314cfe09d3167c95f712589e8"
 
 [[package]]
 name = "base64"
-version = "0.21.3"
+version = "0.21.7"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "414dcefbc63d77c526a76b3afcf6fbb9b5e2791c19c3aa2297733208750c6e53"
+checksum = "9d297deb1925b89f2ccc13d7635fa0714f12c87adce1c75356b39ca9b7178567"
 
 [[package]]
 name = "bit-set"
@@ -138,9 +139,9 @@ checksum = "bef38d45163c2f1dde094a7dfd33ccf595c92905c8f8f4fdc18d06fb1037718a"
 
 [[package]]
 name = "bitflags"
-version = "2.4.0"
+version = "2.4.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b4682ae6287fcf752ecaabbfcc7b6f9b72aa33933dc23a554d853aea8eea8635"
+checksum = "327762f6e5a765692301e5bb513e0d9fef63be86bbc14528052b1cd3e6f03e07"
 
 [[package]]
 name = "bitvec"
@@ -165,15 +166,9 @@ dependencies = [
 
 [[package]]
 name = "bumpalo"
-version = "3.13.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "a3e2c3daef883ecc1b5d58c15adae93470a91d425f3532ba1695849656af3fc1"
-
-[[package]]
-name = "byteorder"
-version = "1.4.3"
+version = "3.14.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "14c189c53d098945499cdfa7ecc63567cf3886b3332b312a5b4585d8d3a6a610"
+checksum = "7f30e7476521f6f8af1a1c4c0b8cc94f0bee37d91763d0ca2665f299b6cd8aec"
 
 [[package]]
 name = "calyx"
@@ -208,9 +203,9 @@ dependencies = [
  "petgraph",
  "quick-xml",
  "serde",
+ "serde-lexpr",
  "serde_json",
- "serde_sexpr",
- "serde_with 3.3.0",
+ "serde_with 3.4.0",
  "smallvec",
  "string-interner",
  "vast",
@@ -230,7 +225,7 @@ dependencies = [
  "pest_consume",
  "pest_derive",
  "serde",
- "serde_with 3.3.0",
+ "serde_with 3.4.0",
  "smallvec",
  "strum",
  "strum_macros",
@@ -247,7 +242,7 @@ dependencies = [
  "log",
  "petgraph",
  "serde",
- "serde_with 3.3.0",
+ "serde_with 3.4.0",
  "smallvec",
  "string-interner",
 ]
@@ -323,15 +318,15 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd"
 
 [[package]]
 name = "chrono"
-version = "0.4.27"
+version = "0.4.31"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f56b4c72906975ca04becb8a30e102dfecddd0c06181e3e95ddc444be28881f8"
+checksum = "7f2c685bad3eb3d45a01354cedb7d5faa66194d1d58ba6e267a8de788f79db38"
 dependencies = [
  "android-tzdata",
  "iana-time-zone",
  "num-traits",
  "serde",
- "windows-targets",
+ "windows-targets 0.48.5",
 ]
 
 [[package]]
@@ -383,15 +378,15 @@ dependencies = [
 
 [[package]]
 name = "core-foundation-sys"
-version = "0.8.4"
+version = "0.8.6"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e496a50fda8aacccc86d7529e2c1e0892dbd0f898a6b5645b5561b89c3210efa"
+checksum = "06ea2b9bc92be3c2baa9334a323ebca2d6f074ff852cd1d7b11064035cd3868f"
 
 [[package]]
 name = "cpufeatures"
-version = "0.2.9"
+version = "0.2.12"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "a17b76ff3a4162b0b27f354a0c87015ddad39d35f9c0c36607a3bdd175dde1f1"
+checksum = "53fe5e26ff1b7aef8bca9c6080520cfb8d9333c7568e1829cef191a9723e5504"
 dependencies = [
  "libc",
 ]
@@ -434,46 +429,37 @@ dependencies = [
 
 [[package]]
 name = "crossbeam-channel"
-version = "0.5.8"
+version = "0.5.11"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "a33c2bf77f2df06183c3aa30d1e96c0695a313d4f9c453cc3762a6db39f99200"
+checksum = "176dc175b78f56c0f321911d9c8eb2b77a78a4860b9c19db83835fea1a46649b"
 dependencies = [
- "cfg-if",
  "crossbeam-utils",
 ]
 
 [[package]]
 name = "crossbeam-deque"
-version = "0.8.3"
+version = "0.8.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "ce6fd6f855243022dcecf8702fef0c297d4338e226845fe067f6341ad9fa0cef"
+checksum = "613f8cc01fe9cf1a3eb3d7f488fd2fa8388403e97039e2f73692932e291a770d"
 dependencies = [
- "cfg-if",
  "crossbeam-epoch",
  "crossbeam-utils",
 ]
 
 [[package]]
 name = "crossbeam-epoch"
-version = "0.9.15"
+version = "0.9.18"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "ae211234986c545741a7dc064309f67ee1e5ad243d0e48335adc0484d960bcc7"
+checksum = "5b82ac4a3c2ca9c3460964f020e1402edd5753411d7737aa39c3714ad1b5420e"
 dependencies = [
- "autocfg",
- "cfg-if",
  "crossbeam-utils",
- "memoffset",
- "scopeguard",
 ]
 
 [[package]]
 name = "crossbeam-utils"
-version = "0.8.16"
+version = "0.8.19"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "5a22b2d63d4d1dc0b7f1b6b2747dd0088008a9be28b6ddf0b1e7d335e3037294"
-dependencies = [
- "cfg-if",
-]
+checksum = "248e3bacc7dc6baa3b21e405ee045c3047101a49145e7e9eca583ab4c2ca5345"
 
 [[package]]
 name = "crypto-common"
@@ -487,9 +473,9 @@ dependencies = [
 
 [[package]]
 name = "csv"
-version = "1.2.2"
+version = "1.3.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "626ae34994d3d8d668f4269922248239db4ae42d538b14c398b74a52208e8086"
+checksum = "ac574ff4d437a7b5ad237ef331c17ccca63c46479e5b5453eb8e10bb99a759fe"
 dependencies = [
  "csv-core",
  "itoa",
@@ -499,9 +485,9 @@ dependencies = [
 
 [[package]]
 name = "csv-core"
-version = "0.1.10"
+version = "0.1.11"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "2b2466559f260f48ad25fe6317b3c8dac77b5bdb5763ac7d9d6103530663bc90"
+checksum = "5efa2b3d7902f4b634a20cae3c9c4e6209dc4779feb6863329607560143efa70"
 dependencies = [
  "memchr",
 ]
@@ -561,7 +547,7 @@ dependencies = [
  "proc-macro2",
  "quote",
  "strsim",
- "syn 2.0.29",
+ "syn 2.0.48",
 ]
 
 [[package]]
@@ -583,7 +569,7 @@ checksum = "836a9bbc7ad63342d6d6e7b815ccab164bc77a2d95d84bc3117a8c0d5c98e2d5"
 dependencies = [
  "darling_core 0.20.3",
  "quote",
- "syn 2.0.29",
+ "syn 2.0.48",
 ]
 
 [[package]]
@@ -603,10 +589,11 @@ dependencies = [
 
 [[package]]
 name = "deranged"
-version = "0.3.8"
+version = "0.3.11"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f2696e8a945f658fd14dc3b87242e6b80cd0f36ff04ea560fa39082368847946"
+checksum = "b42b6fa04a440b495c8b04d0e71b707c585f83cb9cb28cf8cd0d976c315e31b4"
 dependencies = [
+ "powerfmt",
  "serde",
 ]
 
@@ -672,23 +659,12 @@ checksum = "5443807d6dff69373d433ab9ef5378ad8df50ca6298caf15de6e52e24aaf54d5"
 
 [[package]]
 name = "errno"
-version = "0.3.3"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "136526188508e25c6fef639d7927dfb3e0e3084488bf202267829cf7fc23dbdd"
-dependencies = [
- "errno-dragonfly",
- "libc",
- "windows-sys",
-]
-
-[[package]]
-name = "errno-dragonfly"
-version = "0.1.2"
+version = "0.3.8"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "aa68f1b12764fab894d2755d2518754e71b4fd80ecfb822714a1206c2aab39bf"
+checksum = "a258e46cdc063eb8519c00b9fc845fc47bcfca4130e2f08e88665ceda8474245"
 dependencies = [
- "cc",
  "libc",
+ "windows-sys 0.52.0",
 ]
 
 [[package]]
@@ -703,9 +679,9 @@ dependencies = [
 
 [[package]]
 name = "fastrand"
-version = "2.0.0"
+version = "2.0.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "6999dc1837253364c2ebb0704ba97994bd874e8f195d665c50b7548f6ea92764"
+checksum = "25cbce373ec4653f1a01a31e8a5e5ec0c622dc27ff9c4e6606eefef5cbbed4a5"
 
 [[package]]
 name = "fd-lock"
@@ -715,7 +691,7 @@ checksum = "ef033ed5e9bad94e55838ca0ca906db0e043f517adda0c8b79c7a8c66c93c1b5"
 dependencies = [
  "cfg-if",
  "rustix",
- "windows-sys",
+ "windows-sys 0.48.0",
 ]
 
 [[package]]
@@ -755,14 +731,14 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "85649ca51fd72272d7821adaf274ad91c288277713d9c18820d8499a7ff69e9a"
 dependencies = [
  "typenum",
- "version_check 0.9.4",
+ "version_check",
 ]
 
 [[package]]
 name = "getrandom"
-version = "0.2.10"
+version = "0.2.12"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "be4136b2a15dd319360be1c07d9933517ccf0be8f16bf62a3bee4f0d618df427"
+checksum = "190092ea657667030ac6a35e305e62fc4dd69fd98ac98631e5d3a2b1575a12b5"
 dependencies = [
  "cfg-if",
  "libc",
@@ -781,7 +757,7 @@ version = "0.11.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "ab5ef0d4909ef3724cc8cce6ccc8572c5c817592e9285f5464f8e86f8bd3726e"
 dependencies = [
- "ahash 0.7.6",
+ "ahash 0.7.7",
 ]
 
 [[package]]
@@ -790,14 +766,14 @@ version = "0.12.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "8a9ee70c43aaf417c914396645a0fa852624801b24ebb7ae78fe8272889ac888"
 dependencies = [
- "ahash 0.7.6",
+ "ahash 0.7.7",
 ]
 
 [[package]]
 name = "hashbrown"
-version = "0.14.0"
+version = "0.14.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "2c6201b9ff9fd90a5a3bac2e56a830d0caa509576f0e503818ee82c181b3437a"
+checksum = "290f1a1d9242c78d09ce40a5e87e7554ee637af1351968159f4952f028f75604"
 
 [[package]]
 name = "heck"
@@ -814,12 +790,6 @@ dependencies = [
  "libc",
 ]
 
-[[package]]
-name = "hermit-abi"
-version = "0.3.2"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "443144c8cdadd93ebf52ddb4056d257f5b52c04d3c804e657d19eb73fc33668b"
-
 [[package]]
 name = "hex"
 version = "0.4.3"
@@ -828,16 +798,16 @@ checksum = "7f24254aa9a54b5c858eaee2f5bccdb46aaf0e486a595ed5fd8f86ba55232a70"
 
 [[package]]
 name = "iana-time-zone"
-version = "0.1.57"
+version = "0.1.59"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "2fad5b825842d2b38bd206f3e81d6957625fd7f0a361e345c30e01a0ae2dd613"
+checksum = "b6a67363e2aa4443928ce15e57ebae94fd8949958fd1223c4cfc0cd473ad7539"
 dependencies = [
  "android_system_properties",
  "core-foundation-sys",
  "iana-time-zone-haiku",
  "js-sys",
  "wasm-bindgen",
- "windows",
+ "windows-core",
 ]
 
 [[package]]
@@ -881,12 +851,12 @@ dependencies = [
 
 [[package]]
 name = "indexmap"
-version = "2.0.0"
+version = "2.1.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d5477fe2230a79769d8dc68e0eabf5437907c0457a5614a9e8dddb67f65eb65d"
+checksum = "d530e1a18b1cb4c484e6e34556a0d948706958449fca0cab753d649f2bce3d1f"
 dependencies = [
  "equivalent",
- "hashbrown 0.14.0",
+ "hashbrown 0.14.3",
  "serde",
 ]
 
@@ -894,7 +864,7 @@ dependencies = [
 name = "interp"
 version = "0.1.1"
 dependencies = [
- "ahash 0.8.3",
+ "ahash 0.8.7",
  "argh",
  "base64 0.13.1",
  "bitvec",
@@ -944,9 +914,9 @@ dependencies = [
 
 [[package]]
 name = "itoa"
-version = "1.0.9"
+version = "1.0.10"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "af150ab688ff2122fcef229be89cb50dd66af9e01a4ff320cc137eecc9bacc38"
+checksum = "b1a46d1a171d865aa5f83f92695765caa047a9b4cbae2cbf37dbd613a793fd4c"
 
 [[package]]
 name = "js-sys"
@@ -963,17 +933,49 @@ version = "1.4.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "e2abad23fbc42b3700f2f279844dc832adb2b2eb069b2df918f455c4e18cc646"
 
+[[package]]
+name = "lexpr"
+version = "0.2.7"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "6a84de6a9df442363b08f5dbf0cd5b92edc70097b89c4ce4bfea4679fe48bc67"
+dependencies = [
+ "itoa",
+ "lexpr-macros",
+ "ryu",
+]
+
+[[package]]
+name = "lexpr-macros"
+version = "0.2.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "36b5cb8bb985c81a8ac1a0f8b5c4865214f574ddd64397ef7a99c236e21f35bb"
+dependencies = [
+ "proc-macro2",
+ "quote",
+]
+
 [[package]]
 name = "libc"
-version = "0.2.147"
+version = "0.2.152"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b4668fb0ea861c1df094127ac5f1da3409a82116a4ba74fca2e58ef927159bb3"
+checksum = "13e3bf6590cbc649f4d1a3eefc9d5d6eb746f5200ffb04e5e142700b8faa56e7"
 
 [[package]]
 name = "libm"
-version = "0.2.7"
+version = "0.2.8"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "4ec2a862134d2a7d32d7983ddcdd1c4923530833c9f2ea1a44fc5fa473989058"
+
+[[package]]
+name = "libredox"
+version = "0.0.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f7012b1bbb0719e1097c47611d3898568c546d597c2e74d66f6087edd5233ff4"
+checksum = "85c833ca1e66078851dba29046874e38f08b2c883700aa29a03ddd3b23814ee8"
+dependencies = [
+ "bitflags 2.4.1",
+ "libc",
+ "redox_syscall",
+]
 
 [[package]]
 name = "linked-hash-map"
@@ -983,9 +985,9 @@ checksum = "0717cef1bc8b636c6e1c1bbdefc09e6322da8a9321966e8928ef80d20f7f770f"
 
 [[package]]
 name = "linux-raw-sys"
-version = "0.4.5"
+version = "0.4.12"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "57bcfdad1b858c2db7c38303a6d2ad4dfaf5eb53dfeb0910128b2c26d6158503"
+checksum = "c4cd1a83af159aa67994778be9070f0ae1bd732942279cabb14f86f986a21456"
 
 [[package]]
 name = "log"
@@ -995,18 +997,9 @@ checksum = "b5e6163cb8c49088c2c36f57875e58ccd8c87c7427f7fbd50ea6710b2f3f2e8f"
 
 [[package]]
 name = "memchr"
-version = "2.6.1"
+version = "2.7.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f478948fd84d9f8e86967bf432640e46adfb5a4bd4f14ef7e864ab38220534ae"
-
-[[package]]
-name = "memoffset"
-version = "0.9.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "5a634b1c61a95585bd15607c6ab0c4e5b226e695ff2800ba0cdccddf208c406c"
-dependencies = [
- "autocfg",
-]
+checksum = "523dc4f511e55ab87b694dc30d0f820d60906ef06413f93d4d7a1385599cc149"
 
 [[package]]
 name = "nibble_vec"
@@ -1028,16 +1021,6 @@ dependencies = [
  "libc",
 ]
 
-[[package]]
-name = "nom"
-version = "4.2.3"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "2ad2a91a8e869eeb30b9cb3119ae87773a8f4ae617f41b1eb9c154b2905f7bd6"
-dependencies = [
- "memchr",
- "version_check 0.1.5",
-]
-
 [[package]]
 name = "num"
 version = "0.4.1"
@@ -1110,24 +1093,14 @@ dependencies = [
 
 [[package]]
 name = "num-traits"
-version = "0.2.16"
+version = "0.2.17"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f30b0abd723be7e2ffca1272140fac1a2f084c77ec3e123c192b66af1ee9e6c2"
+checksum = "39e3200413f237f41ab11ad6d161bc7239c84dcb631773ccd7de3dfe4b5c267c"
 dependencies = [
  "autocfg",
  "libm",
 ]
 
-[[package]]
-name = "num_cpus"
-version = "1.16.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "4161fcb6d602d4d2081af7c3a45852d875a03dd337a6bfdd6e06407b61342a43"
-dependencies = [
- "hermit-abi 0.3.2",
- "libc",
-]
-
 [[package]]
 name = "num_threads"
 version = "0.1.6"
@@ -1139,9 +1112,9 @@ dependencies = [
 
 [[package]]
 name = "once_cell"
-version = "1.18.0"
+version = "1.19.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "dd8b5dd2ae5ed71462c540258bedcb51965123ad7e7ccf4b9a8cafaa4a63576d"
+checksum = "3fdb12b2476b595f9358c5161aa467c2438859caa136dec86c26fdd2efe17b92"
 
 [[package]]
 name = "oorandom"
@@ -1157,10 +1130,11 @@ checksum = "c1b04fb49957986fdce4d6ee7a65027d55d4b6d2265e5848bbb507b58ccfdb6f"
 
 [[package]]
 name = "pest"
-version = "2.7.2"
+version = "2.7.6"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "1acb4a4365a13f749a93f1a094a7805e5cfa0955373a9de860d962eaa3a5fe5a"
+checksum = "1f200d8d83c44a45b21764d1916299752ca035d15ecd46faca3e9a2a2bf6ad06"
 dependencies = [
+ "memchr",
  "thiserror",
  "ucd-trie",
 ]
@@ -1189,9 +1163,9 @@ dependencies = [
 
 [[package]]
 name = "pest_derive"
-version = "2.7.2"
+version = "2.7.6"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "666d00490d4ac815001da55838c500eafb0320019bbaa44444137c48b443a853"
+checksum = "bcd6ab1236bbdb3a49027e920e693192ebfe8913f6d60e294de57463a493cfde"
 dependencies = [
  "pest",
  "pest_generator",
@@ -1199,22 +1173,22 @@ dependencies = [
 
 [[package]]
 name = "pest_generator"
-version = "2.7.2"
+version = "2.7.6"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "68ca01446f50dbda87c1786af8770d535423fa8a53aec03b8f4e3d7eb10e0929"
+checksum = "2a31940305ffc96863a735bef7c7994a00b325a7138fdbc5bda0f1a0476d3275"
 dependencies = [
  "pest",
  "pest_meta",
  "proc-macro2",
  "quote",
- "syn 2.0.29",
+ "syn 2.0.48",
 ]
 
 [[package]]
 name = "pest_meta"
-version = "2.7.2"
+version = "2.7.6"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "56af0a30af74d0445c0bf6d9d051c979b516a1a5af790d251daee76005420a48"
+checksum = "a7ff62f5259e53b78d1af898941cdcdccfae7385cf7d793a6e55de5d05bb4b7d"
 dependencies = [
  "once_cell",
  "pest",
@@ -1228,7 +1202,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "e1d3afd2628e69da2be385eb6f2fd57c8ac7977ceeff6dc166ff1657b0e386a9"
 dependencies = [
  "fixedbitset",
- "indexmap 2.0.0",
+ "indexmap 2.1.0",
 ]
 
 [[package]]
@@ -1259,6 +1233,12 @@ dependencies = [
  "plotters-backend",
 ]
 
+[[package]]
+name = "powerfmt"
+version = "0.2.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "439ee305def115ba05938db6eb1644ff94165c5ab5e9420d1c1bcedbba909391"
+
 [[package]]
 name = "ppv-lite86"
 version = "0.2.17"
@@ -1279,28 +1259,28 @@ dependencies = [
 
 [[package]]
 name = "proc-macro2"
-version = "1.0.66"
+version = "1.0.76"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "18fb31db3f9bddb2ea821cde30a9f70117e3f119938b5ee630b7403aa6e2ead9"
+checksum = "95fc56cda0b5c3325f5fbbd7ff9fda9e02bb00bb3dac51252d2f1bfa1cb8cc8c"
 dependencies = [
  "unicode-ident",
 ]
 
 [[package]]
 name = "proptest"
-version = "1.2.0"
+version = "1.4.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "4e35c06b98bf36aba164cc17cb25f7e232f5c4aeea73baa14b8a9f0d92dbfa65"
+checksum = "31b476131c3c86cb68032fdc5cb6d5a1045e3e42d96b69fa599fd77701e1f5bf"
 dependencies = [
  "bit-set",
- "bitflags 1.3.2",
- "byteorder",
+ "bit-vec",
+ "bitflags 2.4.1",
  "lazy_static",
  "num-traits",
  "rand",
  "rand_chacha",
  "rand_xorshift",
- "regex-syntax 0.6.29",
+ "regex-syntax",
  "rusty-fork",
  "tempfile",
  "unarray",
@@ -1324,9 +1304,9 @@ dependencies = [
 
 [[package]]
 name = "quote"
-version = "1.0.33"
+version = "1.0.35"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "5267fca4496028628a95160fc423a33e8b2e6af8a5302579e322e4b520293cae"
+checksum = "291ec9ab5efd934aaf503a6466c5d5251535d108ee747472c3977cc5acc868ef"
 dependencies = [
  "proc-macro2",
 ]
@@ -1388,9 +1368,9 @@ dependencies = [
 
 [[package]]
 name = "rayon"
-version = "1.7.0"
+version = "1.8.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "1d2df5196e37bcc87abebc0053e20787d73847bb33134a69841207dd0a47f03b"
+checksum = "9c27db03db7734835b3f53954b534c91069375ce6ccaa2e065441e07d9b6cdb1"
 dependencies = [
  "either",
  "rayon-core",
@@ -1398,91 +1378,74 @@ dependencies = [
 
 [[package]]
 name = "rayon-core"
-version = "1.11.0"
+version = "1.12.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "4b8f95bd6966f5c87776639160a66bd8ab9895d9d4ab01ddba9fc60661aebe8d"
+checksum = "5ce3fb6ad83f861aac485e76e1985cd109d9a3713802152be56c3b1f0e0658ed"
 dependencies = [
- "crossbeam-channel",
  "crossbeam-deque",
  "crossbeam-utils",
- "num_cpus",
-]
-
-[[package]]
-name = "redox_syscall"
-version = "0.2.16"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "fb5a58c1855b4b6819d59012155603f0b22ad30cad752600aadfcb695265519a"
-dependencies = [
- "bitflags 1.3.2",
 ]
 
 [[package]]
 name = "redox_syscall"
-version = "0.3.5"
+version = "0.4.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "567664f262709473930a4bf9e51bf2ebf3348f2e748ccc50dea20646858f8f29"
+checksum = "4722d768eff46b75989dd134e5c353f0d6296e5aaa3132e776cbdb56be7731aa"
 dependencies = [
  "bitflags 1.3.2",
 ]
 
 [[package]]
 name = "redox_users"
-version = "0.4.3"
+version = "0.4.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b033d837a7cf162d7993aded9304e30a83213c648b6e389db233191f891e5c2b"
+checksum = "a18479200779601e498ada4e8c1e1f50e3ee19deb0259c25825a98b5603b2cb4"
 dependencies = [
  "getrandom",
- "redox_syscall 0.2.16",
+ "libredox",
  "thiserror",
 ]
 
 [[package]]
 name = "regex"
-version = "1.9.4"
+version = "1.10.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "12de2eff854e5fa4b1295edd650e227e9d8fb0c9e90b12e7f36d6a6811791a29"
+checksum = "380b951a9c5e80ddfd6136919eef32310721aa4aacd4889a8d39124b026ab343"
 dependencies = [
  "aho-corasick",
  "memchr",
  "regex-automata",
- "regex-syntax 0.7.5",
+ "regex-syntax",
 ]
 
 [[package]]
 name = "regex-automata"
-version = "0.3.7"
+version = "0.4.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "49530408a136e16e5b486e883fbb6ba058e8e4e8ae6621a77b048b314336e629"
+checksum = "5f804c7828047e88b2d32e2d7fe5a105da8ee3264f01902f796c8e067dc2483f"
 dependencies = [
  "aho-corasick",
  "memchr",
- "regex-syntax 0.7.5",
+ "regex-syntax",
 ]
 
 [[package]]
 name = "regex-syntax"
-version = "0.6.29"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f162c6dd7b008981e4d40210aca20b4bd0f9b60ca9271061b07f78537722f2e1"
-
-[[package]]
-name = "regex-syntax"
-version = "0.7.5"
+version = "0.8.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "dbb5fb1acd8a1a18b3dd5be62d25485eb770e05afb408a9627d14d451bae12da"
+checksum = "c08c74e62047bb2de4ff487b251e4a92e24f48745648451635cec7d591162d9f"
 
 [[package]]
 name = "rustix"
-version = "0.38.10"
+version = "0.38.28"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "ed6248e1caa625eb708e266e06159f135e8c26f2bb7ceb72dc4b2766d0340964"
+checksum = "72e572a5e8ca657d7366229cdde4bd14c4eb5499a9573d4d366fe1b599daa316"
 dependencies = [
- "bitflags 2.4.0",
+ "bitflags 2.4.1",
  "errno",
  "libc",
  "linux-raw-sys",
- "windows-sys",
+ "windows-sys 0.52.0",
 ]
 
 [[package]]
@@ -1528,9 +1491,9 @@ dependencies = [
 
 [[package]]
 name = "ryu"
-version = "1.0.15"
+version = "1.0.16"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "1ad4cc8da4ef723ed60bced201181d83791ad433213d8c24efffda1eec85d741"
+checksum = "f98d2aa92eebf49b69786be48e4477826b256916e84a57ff2a4f21923b48eb4c"
 
 [[package]]
 name = "same-file"
@@ -1549,13 +1512,23 @@ checksum = "94143f37725109f92c262ed2cf5e59bce7498c01bcc1502d7b9afe439a4e9f49"
 
 [[package]]
 name = "serde"
-version = "1.0.188"
+version = "1.0.195"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "cf9e0fcba69a370eed61bcf2b728575f726b50b55cba78064753d708ddc7549e"
+checksum = "63261df402c67811e9ac6def069e4786148c4563f4b50fd4bf30aa370d626b02"
 dependencies = [
  "serde_derive",
 ]
 
+[[package]]
+name = "serde-lexpr"
+version = "0.1.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "bb4cda13396159f59e7946118cdac0beadeecfb7cf76b197f4147e546f4ead6f"
+dependencies = [
+ "lexpr",
+ "serde",
+]
+
 [[package]]
 name = "serde_cbor"
 version = "0.11.2"
@@ -1568,36 +1541,26 @@ dependencies = [
 
 [[package]]
 name = "serde_derive"
-version = "1.0.188"
+version = "1.0.195"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "4eca7ac642d82aa35b60049a6eccb4be6be75e599bd2e9adb5f875a737654af2"
+checksum = "46fe8f8603d81ba86327b23a2e9cdf49e1255fb94a4c5f297f6ee0547178ea2c"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.29",
+ "syn 2.0.48",
 ]
 
 [[package]]
 name = "serde_json"
-version = "1.0.105"
+version = "1.0.111"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "693151e1ac27563d6dbcec9dee9fbd5da8539b20fa14ad3752b2e6d363ace360"
+checksum = "176e46fa42316f18edd598015a5166857fc835ec732f5215eac6b7bdbf0a84f4"
 dependencies = [
  "itoa",
  "ryu",
  "serde",
 ]
 
-[[package]]
-name = "serde_sexpr"
-version = "0.1.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "5318bfeed779c64075ce317c81462ed54dc00021be1c6b34957d798e11a68bdb"
-dependencies = [
- "nom",
- "serde",
-]
-
 [[package]]
 name = "serde_with"
 version = "1.14.0"
@@ -1610,18 +1573,18 @@ dependencies = [
 
 [[package]]
 name = "serde_with"
-version = "3.3.0"
+version = "3.4.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "1ca3b16a3d82c4088f343b7480a93550b3eabe1a358569c2dfe38bbcead07237"
+checksum = "64cd236ccc1b7a29e7e2739f27c0b2dd199804abc4290e32f59f3b68d6405c23"
 dependencies = [
- "base64 0.21.3",
+ "base64 0.21.7",
  "chrono",
  "hex",
  "indexmap 1.9.3",
- "indexmap 2.0.0",
+ "indexmap 2.1.0",
  "serde",
  "serde_json",
- "serde_with_macros 3.3.0",
+ "serde_with_macros 3.4.0",
  "time",
 ]
 
@@ -1639,21 +1602,21 @@ dependencies = [
 
 [[package]]
 name = "serde_with_macros"
-version = "3.3.0"
+version = "3.4.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "2e6be15c453eb305019bfa438b1593c731f36a289a7853f7707ee29e870b3b3c"
+checksum = "93634eb5f75a2323b16de4748022ac4297f9e76b6dced2be287a099f41b5e788"
 dependencies = [
  "darling 0.20.3",
  "proc-macro2",
  "quote",
- "syn 2.0.29",
+ "syn 2.0.48",
 ]
 
 [[package]]
 name = "sha2"
-version = "0.10.7"
+version = "0.10.8"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "479fb9d862239e610720565ca91403019f2f00410f1864c5aa7479b950a76ed8"
+checksum = "793db75ad2bcafc3ffa7c68b215fee268f537982cd901d132f89c6343f3a3dc8"
 dependencies = [
  "cfg-if",
  "cpufeatures",
@@ -1693,9 +1656,9 @@ dependencies = [
 
 [[package]]
 name = "smallvec"
-version = "1.11.0"
+version = "1.11.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "62bb4feee49fdd9f707ef802e22365a35de4b7b299de4763d44bfea899442ff9"
+checksum = "4dccd0940a2dcdf68d092b8cbab7dc0ad8fa938bf95787e1b916b0e3d0e8e970"
 dependencies = [
  "serde",
 ]
@@ -1737,15 +1700,15 @@ checksum = "290d54ea6f91c969195bdbcd7442c8c2a2ba87da8bf60a7ee86a235d4bc1e125"
 
 [[package]]
 name = "strum_macros"
-version = "0.25.2"
+version = "0.25.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "ad8d03b598d3d0fff69bf533ee3ef19b8eeb342729596df84bcc7e1f96ec4059"
+checksum = "23dc1fa9ac9c169a78ba62f0b841814b7abae11bdd047b9c58f893439e309ea0"
 dependencies = [
  "heck",
  "proc-macro2",
  "quote",
  "rustversion",
- "syn 2.0.29",
+ "syn 2.0.48",
 ]
 
 [[package]]
@@ -1754,7 +1717,7 @@ version = "0.3.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "828f672b631c220bf6ea8a1d3b82c7d0fc998e5ba8373383d8604bc1e2a6245a"
 dependencies = [
- "ahash 0.7.6",
+ "ahash 0.7.7",
  "hashbrown 0.12.3",
  "serde",
 ]
@@ -1772,9 +1735,9 @@ dependencies = [
 
 [[package]]
 name = "syn"
-version = "2.0.29"
+version = "2.0.48"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "c324c494eba9d92503e6f1ef2e6df781e78f6a7705a0202d9801b198807d518a"
+checksum = "0f3531638e407dfc0814761abb7c00a5b54992b849452a0646b7f65c9f770f3f"
 dependencies = [
  "proc-macro2",
  "quote",
@@ -1795,15 +1758,15 @@ checksum = "55937e1799185b12863d447f42597ed69d9928686b8d88a1df17376a097d8369"
 
 [[package]]
 name = "tempfile"
-version = "3.8.0"
+version = "3.9.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "cb94d2f3cc536af71caac6b6fcebf65860b347e7ce0cc9ebe8f70d3e521054ef"
+checksum = "01ce4141aa927a6d1bd34a041795abd0db1cccba5d5f24b009f694bdf3a1f3fa"
 dependencies = [
  "cfg-if",
  "fastrand",
- "redox_syscall 0.3.5",
+ "redox_syscall",
  "rustix",
- "windows-sys",
+ "windows-sys 0.52.0",
 ]
 
 [[package]]
@@ -1819,9 +1782,9 @@ dependencies = [
 
 [[package]]
 name = "termcolor"
-version = "1.2.0"
+version = "1.4.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "be55cf8942feac5c765c2c993422806843c9a9a45d4d5c407ad6dd2ea95eb9b6"
+checksum = "06794f8f6c5c898b3275aebefa6b8a1cb24cd2c6c79397ab15774837a0bc5755"
 dependencies = [
  "winapi-util",
 ]
@@ -1837,22 +1800,22 @@ dependencies = [
 
 [[package]]
 name = "thiserror"
-version = "1.0.47"
+version = "1.0.56"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "97a802ec30afc17eee47b2855fc72e0c4cd62be9b4efe6591edde0ec5bd68d8f"
+checksum = "d54378c645627613241d077a3a79db965db602882668f9136ac42af9ecb730ad"
 dependencies = [
  "thiserror-impl",
 ]
 
 [[package]]
 name = "thiserror-impl"
-version = "1.0.47"
+version = "1.0.56"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "6bb623b56e39ab7dcd4b1b98bb6c8f8d907ed255b18de254088016b27a8ee19b"
+checksum = "fa0faa943b50f3db30a20aa7e265dbc66076993efed8463e8de414e5d06d3471"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.29",
+ "syn 2.0.48",
 ]
 
 [[package]]
@@ -1867,14 +1830,15 @@ dependencies = [
 
 [[package]]
 name = "time"
-version = "0.3.28"
+version = "0.3.31"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "17f6bb557fd245c28e6411aa56b6403c689ad95061f50e4be16c274e70a17e48"
+checksum = "f657ba42c3f86e7680e53c8cd3af8abbe56b5491790b46e22e19c0d57463583e"
 dependencies = [
  "deranged",
  "itoa",
  "libc",
  "num_threads",
+ "powerfmt",
  "serde",
  "time-core",
  "time-macros",
@@ -1882,15 +1846,15 @@ dependencies = [
 
 [[package]]
 name = "time-core"
-version = "0.1.1"
+version = "0.1.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "7300fbefb4dadc1af235a9cef3737cea692a9d97e1b9cbcd4ebdae6f8868e6fb"
+checksum = "ef927ca75afb808a4d64dd374f00a2adf8d0fcff8e7b184af886c3c87ec4a3f3"
 
 [[package]]
 name = "time-macros"
-version = "0.2.14"
+version = "0.2.16"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "1a942f44339478ef67935ab2bbaec2fb0322496cf3cbe84b261e06ac3814c572"
+checksum = "26197e33420244aeb70c3e8c78376ca46571bc4e701e4791c2cd9f57dcb3a43f"
 dependencies = [
  "time-core",
 ]
@@ -1913,9 +1877,9 @@ checksum = "6af6ae20167a9ece4bcb41af5b80f8a1f1df981f6391189ce00fd257af04126a"
 
 [[package]]
 name = "typenum"
-version = "1.16.0"
+version = "1.17.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "497961ef93d974e23eb6f433eb5fe1b7930b659f06d12dec6fc44a8f554c0bba"
+checksum = "42ff0bf0c66b8238c6f3b578df37d0b7848e55df8577b3f74f92a69acceeb825"
 
 [[package]]
 name = "ucd-trie"
@@ -1931,9 +1895,9 @@ checksum = "eaea85b334db583fe3274d12b4cd1880032beab409c0d774be044d4480ab9a94"
 
 [[package]]
 name = "unicode-ident"
-version = "1.0.11"
+version = "1.0.12"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "301abaae475aa91687eb82514b328ab47a211a533026cb25fc3e519b86adfc3c"
+checksum = "3354b9ac3fae1ff6755cb6db53683adb661634f67557942dea4facebec0fee4b"
 
 [[package]]
 name = "unicode-segmentation"
@@ -1943,9 +1907,9 @@ checksum = "1dd624098567895118886609431a7c3b8f516e41d30e0643f03d94592a147e36"
 
 [[package]]
 name = "unicode-width"
-version = "0.1.10"
+version = "0.1.11"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "c0edd1e5b14653f783770bce4a4dabb4a5108a5370a5f5d8cfe8710c361f6c8b"
+checksum = "e51733f11c9c4f72aa0c160008246859e340b00807569a0da0e7a1079b27ba85"
 
 [[package]]
 name = "utf8parse"
@@ -1963,12 +1927,6 @@ dependencies = [
  "pretty",
 ]
 
-[[package]]
-name = "version_check"
-version = "0.1.5"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "914b1a6776c4c929a602fafd8bc742e06365d4bcbe48c30f9cca5824f70dc9dd"
-
 [[package]]
 name = "version_check"
 version = "0.9.4"
@@ -1986,9 +1944,9 @@ dependencies = [
 
 [[package]]
 name = "walkdir"
-version = "2.3.3"
+version = "2.4.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "36df944cda56c7d8d8b7496af378e6b16de9284591917d307c9b4d313c44e698"
+checksum = "d71d857dc86794ca4c280d616f7da00d2dbfd8cd788846559a6813e6aa4b54ee"
 dependencies = [
  "same-file",
  "winapi-util",
@@ -2084,9 +2042,9 @@ checksum = "ac3b87c63620426dd9b991e5ce0329eff545bccbbb34f3be09ff6fb6ab51b7b6"
 
 [[package]]
 name = "winapi-util"
-version = "0.1.5"
+version = "0.1.6"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "70ec6ce85bb158151cae5e5c87f95a8e97d2c0c4b001223f33a334e3ce5de178"
+checksum = "f29e6f9198ba0d26b4c9f07dbe6f9ed633e1f3d5b8b414090084349e46a52596"
 dependencies = [
  "winapi",
 ]
@@ -2098,12 +2056,12 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "712e227841d057c1ee1cd2fb22fa7e5a5461ae8e48fa2ca79ec42cfc1931183f"
 
 [[package]]
-name = "windows"
-version = "0.48.0"
+name = "windows-core"
+version = "0.52.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e686886bc078bc1b0b600cac0147aadb815089b6e4da64016cbd754b6342700f"
+checksum = "33ab640c8d7e35bf8ba19b884ba838ceb4fba93a4e8c65a9059d08afcfc683d9"
 dependencies = [
- "windows-targets",
+ "windows-targets 0.52.0",
 ]
 
 [[package]]
@@ -2112,7 +2070,16 @@ version = "0.48.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "677d2418bec65e3338edb076e806bc1ec15693c5d0104683f2efe857f61056a9"
 dependencies = [
- "windows-targets",
+ "windows-targets 0.48.5",
+]
+
+[[package]]
+name = "windows-sys"
+version = "0.52.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "282be5f36a8ce781fad8c8ae18fa3f9beff57ec1b52cb3de0789201425d9a33d"
+dependencies = [
+ "windows-targets 0.52.0",
 ]
 
 [[package]]
@@ -2121,13 +2088,28 @@ version = "0.48.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "9a2fa6e2155d7247be68c096456083145c183cbbbc2764150dda45a87197940c"
 dependencies = [
- "windows_aarch64_gnullvm",
- "windows_aarch64_msvc",
- "windows_i686_gnu",
- "windows_i686_msvc",
- "windows_x86_64_gnu",
- "windows_x86_64_gnullvm",
- "windows_x86_64_msvc",
+ "windows_aarch64_gnullvm 0.48.5",
+ "windows_aarch64_msvc 0.48.5",
+ "windows_i686_gnu 0.48.5",
+ "windows_i686_msvc 0.48.5",
+ "windows_x86_64_gnu 0.48.5",
+ "windows_x86_64_gnullvm 0.48.5",
+ "windows_x86_64_msvc 0.48.5",
+]
+
+[[package]]
+name = "windows-targets"
+version = "0.52.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8a18201040b24831fbb9e4eb208f8892e1f50a37feb53cc7ff887feb8f50e7cd"
+dependencies = [
+ "windows_aarch64_gnullvm 0.52.0",
+ "windows_aarch64_msvc 0.52.0",
+ "windows_i686_gnu 0.52.0",
+ "windows_i686_msvc 0.52.0",
+ "windows_x86_64_gnu 0.52.0",
+ "windows_x86_64_gnullvm 0.52.0",
+ "windows_x86_64_msvc 0.52.0",
 ]
 
 [[package]]
@@ -2136,42 +2118,84 @@ version = "0.48.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "2b38e32f0abccf9987a4e3079dfb67dcd799fb61361e53e2882c3cbaf0d905d8"
 
+[[package]]
+name = "windows_aarch64_gnullvm"
+version = "0.52.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "cb7764e35d4db8a7921e09562a0304bf2f93e0a51bfccee0bd0bb0b666b015ea"
+
 [[package]]
 name = "windows_aarch64_msvc"
 version = "0.48.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "dc35310971f3b2dbbf3f0690a219f40e2d9afcf64f9ab7cc1be722937c26b4bc"
 
+[[package]]
+name = "windows_aarch64_msvc"
+version = "0.52.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "bbaa0368d4f1d2aaefc55b6fcfee13f41544ddf36801e793edbbfd7d7df075ef"
+
 [[package]]
 name = "windows_i686_gnu"
 version = "0.48.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "a75915e7def60c94dcef72200b9a8e58e5091744960da64ec734a6c6e9b3743e"
 
+[[package]]
+name = "windows_i686_gnu"
+version = "0.52.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a28637cb1fa3560a16915793afb20081aba2c92ee8af57b4d5f28e4b3e7df313"
+
 [[package]]
 name = "windows_i686_msvc"
 version = "0.48.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "8f55c233f70c4b27f66c523580f78f1004e8b5a8b659e05a4eb49d4166cca406"
 
+[[package]]
+name = "windows_i686_msvc"
+version = "0.52.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ffe5e8e31046ce6230cc7215707b816e339ff4d4d67c65dffa206fd0f7aa7b9a"
+
 [[package]]
 name = "windows_x86_64_gnu"
 version = "0.48.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "53d40abd2583d23e4718fddf1ebec84dbff8381c07cae67ff7768bbf19c6718e"
 
+[[package]]
+name = "windows_x86_64_gnu"
+version = "0.52.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "3d6fa32db2bc4a2f5abeacf2b69f7992cd09dca97498da74a151a3132c26befd"
+
 [[package]]
 name = "windows_x86_64_gnullvm"
 version = "0.48.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "0b7b52767868a23d5bab768e390dc5f5c55825b6d30b86c844ff2dc7414044cc"
 
+[[package]]
+name = "windows_x86_64_gnullvm"
+version = "0.52.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1a657e1e9d3f514745a572a6846d3c7aa7dbe1658c056ed9c3344c4109a6949e"
+
 [[package]]
 name = "windows_x86_64_msvc"
 version = "0.48.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "ed94fce61571a4006852b7389a063ab983c02eb1bb37b47f8272ce92d06d9538"
 
+[[package]]
+name = "windows_x86_64_msvc"
+version = "0.52.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "dff9641d1cd4be8d1a070daf9e3773c5f67e78b4d9d42263020c057706765c04"
+
 [[package]]
 name = "wyz"
 version = "0.5.1"
@@ -2180,3 +2204,23 @@ checksum = "05f360fc0b24296329c78fda852a1e9ae82de9cf7b27dae4b7f62f118f77b9ed"
 dependencies = [
  "tap",
 ]
+
+[[package]]
+name = "zerocopy"
+version = "0.7.32"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "74d4d3961e53fa4c9a25a8637fc2bfaf2595b3d3ae34875568a5cf64787716be"
+dependencies = [
+ "zerocopy-derive",
+]
+
+[[package]]
+name = "zerocopy-derive"
+version = "0.7.32"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9ce1b18ccd8e73a9321186f97e46f9f04b778851177567b1975109d26a08d2a6"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn 2.0.48",
+]
diff --git a/Cargo.toml b/Cargo.toml
index ca029447d2..3faffccdb9 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -36,6 +36,7 @@ lazy_static = "1"
 linked-hash-map = "0.5"
 smallvec = "1"
 serde = { version = "1.0", features = ["derive"] }
+serde-lexpr = "0.1.3"
 serde_json = "1.0"
 serde_sexpr = "0.1.0"
 serde_with = "3"
diff --git a/calyx-backend/Cargo.toml b/calyx-backend/Cargo.toml
index 9ccd175e33..27b84e057e 100644
--- a/calyx-backend/Cargo.toml
+++ b/calyx-backend/Cargo.toml
@@ -20,7 +20,7 @@ linked-hash-map.workspace = true
 serde = { workspace = true }
 serde_json.workspace = true
 serde_with = { workspace = true, optional = true }
-serde_sexpr = { workspace = true, optional = true }
+serde-lexpr = { workspace = true, optional = true }
 smallvec.workspace = true
 
 calyx-utils.workspace = true
@@ -41,4 +41,4 @@ default = []
 mlir = []
 xilinx = ["dep:quick-xml"]
 resources = ["dep:csv"]
-sexp = ["dep:serde_with", "dep:serde_sexpr", "serde/rc", "calyx-ir/serialize"]
+sexp = ["dep:serde_with", "dep:serde-lexpr", "serde/rc", "calyx-ir/serialize"]
diff --git a/calyx-backend/src/sexp.rs b/calyx-backend/src/sexp.rs
index 7670edcea0..be77398726 100644
--- a/calyx-backend/src/sexp.rs
+++ b/calyx-backend/src/sexp.rs
@@ -28,7 +28,7 @@ impl Backend for SexpBackend {
 
     fn emit(ctx: &ir::Context, file: &mut OutputFile) -> CalyxResult<()> {
         let out = &mut file.get_write();
-        writeln!(out, "{}", serde_sexpr::to_string(ctx).unwrap())?;
+        writeln!(out, "{}", serde_lexpr::to_string(ctx).unwrap())?;
 
         Ok(())
     }
diff --git a/calyx-frontend/src/attributes.rs b/calyx-frontend/src/attributes.rs
index 1bde201c88..6e4d906333 100644
--- a/calyx-frontend/src/attributes.rs
+++ b/calyx-frontend/src/attributes.rs
@@ -13,7 +13,6 @@ struct HeapAttrInfo {
 
 /// Attributes associated with a specific IR structure.
 #[derive(Default, Debug, Clone)]
-#[cfg_attr(feature = "serialize", derive(serde::Serialize))]
 pub struct Attributes {
     /// Inlined attributes
     inl: InlineAttributes,
@@ -21,6 +20,16 @@ pub struct Attributes {
     hinfo: Box<HeapAttrInfo>,
 }
 
+#[cfg(feature = "serialize")]
+impl serde::Serialize for Attributes {
+    fn serialize<S>(&self, ser: S) -> Result<S::Ok, S::Error>
+    where
+        S: serde::Serializer,
+    {
+        ser.collect_map(self.to_owned().iter())
+    }
+}
+
 impl TryFrom<Vec<(Attribute, u64)>> for Attributes {
     type Error = calyx_utils::Error;
 
@@ -129,6 +138,14 @@ impl Attributes {
         self
     }
 
+    pub fn iter(&self) -> impl Iterator<Item = (Attribute, u64)> + '_ {
+        self.hinfo
+            .attrs
+            .iter()
+            .map(|(k, v)| (*k, *v))
+            .chain(self.inl.iter().map(|k| (Attribute::Bool(k), 1)))
+    }
+
     pub fn to_string_with<F>(&self, sep: &'static str, fmt: F) -> String
     where
         F: Fn(String, u64) -> String,
diff --git a/calyx-ir/src/serializers.rs b/calyx-ir/src/serializers.rs
index aed9768725..a1f623685d 100644
--- a/calyx-ir/src/serializers.rs
+++ b/calyx-ir/src/serializers.rs
@@ -73,13 +73,16 @@ impl Serialize for PortParent {
     {
         match &self {
             PortParent::Cell(weak_cell_ref) => {
-                weak_cell_ref.upgrade().borrow().name().serialize(ser)
+                (weak_cell_ref.upgrade().borrow().name().to_string())
+                    .serialize(ser)
             }
             PortParent::Group(weak_group_ref) => {
-                weak_group_ref.upgrade().borrow().name().serialize(ser)
+                (weak_group_ref.upgrade().borrow().name().to_string())
+                    .serialize(ser)
             }
             PortParent::StaticGroup(weak_sgroup_ref) => {
-                weak_sgroup_ref.upgrade().borrow().name().serialize(ser)
+                (weak_sgroup_ref.upgrade().borrow().name().to_string())
+                    .serialize(ser)
             }
         }
     }
diff --git a/fud/fud/config.py b/fud/fud/config.py
index 3c7e5645f2..76e1dcbd35 100644
--- a/fud/fud/config.py
+++ b/fud/fud/config.py
@@ -37,6 +37,12 @@
             "data": None,
             "round_float_to_fixed": True,
         },
+        "vcalyx": {
+            "exec": "_build/default/ocaml/vcx.exe interp",
+            "flags": None,
+            "data": None,
+            "round_float_to_fixed": True,
+        },
         "debugger": {"flags": None},
         "dahlia": {
             "exec": "dahlia",
diff --git a/fud/fud/main.py b/fud/fud/main.py
index 5b89d86bcb..3ad1e2e041 100644
--- a/fud/fud/main.py
+++ b/fud/fud/main.py
@@ -16,6 +16,7 @@
     systolic,
     vcdump,
     jq,
+    vcalyx,
     verilator,
     vivado,
     xilinx,
@@ -108,6 +109,13 @@ def register_stages(registry):
             "Compile Calyx for interpretation with CIDR",
         )
     )
+    registry.register(
+        futil.CalyxStage(
+            "calyx-sexp",
+            "-b sexp -p canonicalize --log info",
+            "Convert Calyx to s-expression format for VCalyx",
+        )
+    )
     registry.register(
         futil.CalyxStage(
             "resources",
@@ -145,6 +153,7 @@ def register_stages(registry):
     registry.register(jq.JqStage("vcd_json"))
     registry.register(jq.JqStage("dat"))
     registry.register(jq.JqStage("interpreter-out"))
+    registry.register(jq.JqStage("vcalyx-out"))
 
     # Xilinx
     registry.register(xilinx.XilinxStage())
@@ -155,6 +164,8 @@ def register_stages(registry):
     registry.register(interpreter.InterpreterStage.debugger("", "", "Run the debugger"))
     registry.register(interpreter.InterpreterStage.data_converter())
 
+    # VCalyx
+    registry.register(vcalyx.VCalyxStage("", "", "Run the VCalyx interpreter"))
 
 def register_external_stages(cfg, registry):
     """
diff --git a/fud/fud/stages/vcalyx.py b/fud/fud/stages/vcalyx.py
new file mode 100644
index 0000000000..604df02758
--- /dev/null
+++ b/fud/fud/stages/vcalyx.py
@@ -0,0 +1,106 @@
+from fud.stages import Stage, SourceType, Source
+from pathlib import Path
+import simplejson as sjson
+import numpy as np
+from fud.stages.verilator.numeric_types import FixedPoint, Bitnum
+from fud.errors import InvalidNumericType
+from fud.stages.verilator.json_to_dat import parse_fp_widths, float_to_fixed
+from fud.utils import shell, TmpDir, unwrap_or, transparent_shell
+from fud import config as cfg
+from enum import Enum, auto
+
+# A local constant used only within this file largely for organizational
+# purposes and to avoid magic strings
+_FILE_NAME = "data.json"
+
+class VCalyxStage(Stage):
+    name = "vcalyx"
+
+    def __init__(
+        self,
+        flags="",
+        debugger_flags="",
+        desc="Run the VCalyx interpreter",
+        output_type=SourceType.Stream,
+        output_name="vcalyx-out",
+    ):
+        super().__init__(
+            src_state="calyx-sexp",
+            target_state=output_name,
+            input_type=SourceType.Stream,
+            output_type=output_type,
+            description=desc,
+        )
+
+        self.flags = flags
+        self.debugger_flags = debugger_flags
+
+    def _define_steps(self, input_data, builder, config):
+        script = config["stages", self.name, "exec"]
+        data_path_exists: bool = (config["stages", "verilog", "data"] or
+                                  config.get(["stages", "mrxl", "data"]))
+
+        cmd = [
+            script,
+            self.flags,
+            unwrap_or(config["stages", self.name, "flags"], ""),
+            "-l",
+            config["global", cfg.ROOT],
+            "--data" if data_path_exists else "",
+            "{data_file}" if data_path_exists else "",
+            "{target}",
+        ]
+
+        cmd = " ".join(cmd)
+
+        @builder.step()
+        def mktmp() -> SourceType.Directory:
+            """
+            Make temporary directory to store Verilator build files.
+            """
+            return TmpDir()
+
+        @builder.step(description="Dynamically retrieve the value of stages.verilog.data")
+        def get_verilog_data() -> SourceType.Path:
+            data_path = config.get(["stages", "verilog", "data"])
+            return Path(data_path) if data_path else None
+
+        @builder.step()
+        def output_data(
+            tmpdir: SourceType.Directory,
+        ) -> SourceType.Path:
+            """
+            Output converted data for the interpreter-data target
+            """
+            path = Path(tmpdir.name) / _FILE_NAME
+            return path
+
+        @builder.step(description=cmd)
+        def interpret(
+            target: SourceType.Path, data: SourceType.Path
+        ) -> SourceType.Stream:
+            """
+            Invoke the interpreter
+            """
+
+            command = cmd.format(
+                data_file=data, target=target
+            )
+
+            return shell(command)
+
+        # schedule
+        tmpdir = mktmp()
+        data_path = get_verilog_data()
+
+        return interpret(input_data, data_path)
+
+    @staticmethod
+    def pre_install():
+        pass
+
+    @staticmethod
+    def defaults():
+        return {}
+
+__STAGES__ = [VCalyxStage]
diff --git a/vcalyx/.ocamlformat b/vcalyx/.ocamlformat
new file mode 100644
index 0000000000..40f3dfeb0c
--- /dev/null
+++ b/vcalyx/.ocamlformat
@@ -0,0 +1,3 @@
+profile = default
+version = 0.25.1
+cases-exp-indent = 2
diff --git a/vcalyx/README.md b/vcalyx/README.md
new file mode 100644
index 0000000000..c896974842
--- /dev/null
+++ b/vcalyx/README.md
@@ -0,0 +1,29 @@
+# VCalyx
+
+## Parsing a single file
+
+Install flit:
+
+    python3 -m pip install flit
+
+In the `fud` directory, run:
+
+    flit install --symlink
+
+Finally, run the `fud` command:
+
+    fud e <path/to/futil> --to vcalyx
+
+To obtain the S-expression form of a Calyx program, run:
+
+    fud e <path/to/futil> --to vcalyx-sexp 
+
+## Running the test suite
+
+Install runt:
+
+    cargo install runt
+
+In the root directory of the repo, run:
+
+    runt -d vcalyx
diff --git a/vcalyx/_CoqProject b/vcalyx/_CoqProject
new file mode 100644
index 0000000000..87534c7558
--- /dev/null
+++ b/vcalyx/_CoqProject
@@ -0,0 +1,2 @@
+-Q _build/default/coq VCalyx
+
diff --git a/vcalyx/coq/Arith.v b/vcalyx/coq/Arith.v
new file mode 100644
index 0000000000..5cf1fc71d8
--- /dev/null
+++ b/vcalyx/coq/Arith.v
@@ -0,0 +1,28 @@
+From stdpp Require Import
+     base
+     numbers.
+Require Import VCalyx.Value.
+Definition value_lift_binop (f: N -> N -> N) : value -> value -> value :=
+  fun u v =>
+    match u, v with
+    | Bot, _
+    | _, Bot => Bot
+    | V u, V v => V (f u v)
+    | Top, _
+    | _, Top => Top
+    end.
+
+Definition value_lt : value -> value -> value :=
+  value_lift_binop (fun n m => bool_to_N (N.ltb n m)).
+
+Definition value_or : value -> value -> value :=
+  value_lift_binop N.lor.
+
+Definition value_add : value -> value -> value :=
+  value_lift_binop N.add.
+
+Definition value_div_quotient : value -> value -> value :=
+  value_lift_binop N.div.
+
+Definition value_div_remainder : value -> value -> value :=
+  value_lift_binop (fun a b => (N.div_eucl a b).2).
diff --git a/vcalyx/coq/Exception.v b/vcalyx/coq/Exception.v
new file mode 100644
index 0000000000..e39d95cfa8
--- /dev/null
+++ b/vcalyx/coq/Exception.v
@@ -0,0 +1,33 @@
+From stdpp Require Import
+     base
+     strings.
+
+Definition exn (A: Type) : Type :=
+  A + string.
+#[global]
+Instance exn_FMap : FMap exn :=
+  fun _ _ f x =>
+    match x with
+    | inl a => inl (f a)
+    | inr exn => inr exn
+    end.
+
+#[global]
+Instance exn_MRet : MRet exn :=
+  fun _ => inl.
+
+#[global]
+Instance exn_MBind : MBind exn :=
+  fun _ _ k c =>
+    match c with
+    | inl a => k a
+    | inr exn => inr exn
+    end.
+
+Definition lift_opt {A} (msg: string) (o: option A) : exn A :=
+  match o with
+  | Some a => inl a
+  | None => inr msg
+  end.
+
+Definition err {A} : string -> exn A := inr.
diff --git a/vcalyx/coq/IRSyntax.v b/vcalyx/coq/IRSyntax.v
new file mode 100644
index 0000000000..93147c8019
--- /dev/null
+++ b/vcalyx/coq/IRSyntax.v
@@ -0,0 +1,254 @@
+From stdpp Require Import
+     decidable
+     fin_maps
+     strings.
+From Coq Require Import
+     Numbers.BinNums.
+
+(** * Calyx Syntax *)
+(** This file defines the syntax of Calyx. It is mostly based on the
+    contents of the calyx/src/ir folder in the calyx repo and the Calyx language
+    documentation. *)
+
+(** Calyx identifiers are strings. *)
+Definition ident := string.
+#[global]
+Instance ident_EqDecision: EqDecision ident.
+Proof.
+  solve_decision.
+Defined.
+
+(** https://docs.calyxir.org/lang/attribute.html?highlight=attribute#attribute *)
+Inductive bool_attr :=
+| TopLevel
+| External
+| NoInterface
+| Reset
+| Clk
+| Stable
+| Data
+| Control
+| Share
+| StateShare
+| Generated
+| NewFSM
+| Inline.
+
+Inductive num_attr :=
+| Go
+| Done
+| Static
+| WriteTogether
+| ReadTogether.
+Inductive internal_attr := .
+Inductive attribute :=
+| NumAttr (attr_name: num_attr) (n: nat)
+| BoolAttr (attr_name: bool_attr) (b: bool)
+| UnknownAttr (attr_name: ident) (n: nat).
+
+Definition attributes := list attribute.
+
+(** Directions for ports. *)
+Inductive direction :=
+| Input
+| Output
+| InOut.
+
+Definition is_in (d: direction) : bool :=
+  match d with
+  | Input
+  | InOut => true
+  | _ => false
+  end.
+
+Definition is_out (d: direction) : bool :=
+  match d with
+  | Output
+  | InOut => true
+  | _ => false
+  end.
+
+
+(** Ports. *)
+Record port :=
+  Port {
+      port_name: ident;
+      port_width: N;
+      port_dir: direction;
+      parent: ident;
+      port_attribute: attributes;
+    }.
+
+(** Collections of port definitions. *)
+Definition ports :=
+  list port.
+
+(** Primitives. *)
+Record prim :=
+  Prim {
+      prim_name: ident;
+      prim_params: list ident;
+      prim_comb: bool;
+      prim_attribute: attributes;
+      prim_ports: ports;
+      (* for inlined primitives *)
+      prim_body: option string
+    }.
+    
+(** Externs. *)
+Record extern :=
+  Extern {
+      extern_path: string;
+      extern_prims: list prim
+    }.
+
+(** Cell prototype references. *)
+Inductive proto :=
+| ProtoPrim (name: ident)
+            (param_binding: list (ident * N))
+            (is_comb: bool)
+| ProtoComp (name: ident)
+(* For use when referencing a defined component within itself  *)
+| ProtoThis
+| ProtoConst (val: N) (width: N).
+
+(** Cells. *)
+Record cell :=
+  Cell {
+      (* name of this cell. *)
+      cell_name: ident;
+      (* attributes *)
+      cell_attrs: attributes;
+      (* ports *)
+      cell_in_ports: list port;
+      cell_out_ports: list port;
+      (* name of the prototype this cell was built from. *)
+      cell_proto: proto;
+      (* whether this cell is by-reference or not *)
+      cell_ref: bool;
+    }.
+
+Definition cells := list cell.
+
+(** Relative references to ports. *)
+Inductive port_ref :=
+(* refers to the port named [port] on the thing [parent]. *)
+| PRef (parent: ident) (port: ident)
+(* refers to the port named [port] on the enclosing component. *)
+| PThis (port: ident).
+
+(** Nonnegative integers of a fixed bit-width. *)
+Record num :=
+  { num_width: positive;
+    num_val: N; }.
+
+(** Comparisons that can be used in guard expressions. *)
+Inductive guard_cmp :=
+| Eq
+| Neq
+| Gt
+| Lt
+| Geq
+| Leq.
+
+(** Guard expressions. *)
+(* https://docs.calyxir.org/lang/ref.html?highlight=guard#guards *)
+Inductive guard_expr :=
+| GAnd (e1 e2: guard_expr)
+| GOr (e1 e2: guard_expr)
+| GNot (e: guard_expr)
+| GCompOp (op: guard_cmp) (p1 p2: port)
+(* Same as p == true *)
+| GPort (p: port)
+(* The constant true *)
+| GTrue.
+
+(* From AST wires *)
+Record assignment := 
+  Assign {
+    dst: port_ref;
+    src: port_ref;
+    assign_guard: guard_expr;
+    attrs: attributes;
+  }.
+
+Definition assignments :=
+  list assignment.
+
+(** Control statements. Each constructor has its own attribute [attribute]. *)
+Inductive control :=
+| CSeq (stmts: list control)
+       (attrs: attributes)
+| CPar (stmts: list control)
+       (attrs: attributes)
+| CIf (cond_port: port_ref)
+      (cond: option ident)
+      (tru: control)
+      (fls: control)
+      (attrs: attributes)
+| CWhile (cond_port: port_ref)
+         (cond: option ident)
+         (body: control)
+         (attrs: attributes)
+| CEnable (group: ident)
+          (attrs: attributes)
+| CWaitGroup (group: ident)
+             (attrs: attributes) (* Administrative redex for CEnable *)
+| CInvoke (comp: ident)
+          (inputs: list (ident * port_ref))
+          (outputs: list (ident * port_ref))
+          (attrs: attributes)
+          (comb_group: option ident)
+          (ref_cells: list (ident * ident))
+| CWaitComp (comp: ident)
+            (attrs: attributes) (* Administrative redex for CInvoke *)
+| CEmpty (attrs: attributes).
+
+(** Groups. *)
+Record group :=
+  Group {
+      group_attrs: attributes;
+      group_name: ident;
+      group_assns: assignments;
+      group_holes: ports; 
+  }.
+
+(** Combinational groups. *)
+Record comb_group :=
+  CombGroup {
+      comb_group_attrs: attributes;
+      comb_group_name: ident;
+      comb_group_assns: assignments;
+  }.
+
+(** Static groups. *)
+Record static_group :=
+  StaticGroup {
+      static_group_attrs: attributes;
+      static_group_name: ident;
+      static_group_assns: assignments;
+      static_group_holes: ports;
+      static_latency: nat;
+  }.
+
+(** Components. *)
+Record comp :=
+  Comp {
+      comp_attrs: attributes; 
+      comp_name: ident;
+      (* aka signature *)
+      comp_sig: cell;
+      comp_cells: cells;
+      comp_groups: list group;
+      comp_comb_groups: list comb_group;
+      comp_static_groups: list static_group;
+      comp_cont_assns: assignments;
+      comp_control: control;
+      comp_is_comb: bool
+  }.
+
+Record context :=
+  Context {
+      ctx_comps: list comp;
+      ctx_entrypoint: ident;
+  }.
diff --git a/vcalyx/coq/Mealy.v b/vcalyx/coq/Mealy.v
new file mode 100644
index 0000000000..764bd02a76
--- /dev/null
+++ b/vcalyx/coq/Mealy.v
@@ -0,0 +1,61 @@
+Require VCalyx.Vect.
+From stdpp Require Import streams.
+(** * Mealy Machines *)
+
+(** Definition of a Mealy machine: a map [S -> (O x S) ^ I].  In the
+    textbook definition each of the three parameters would need to be
+    finite; we unbundle this requirement. *)
+Definition mealy (S I O: Type) :=
+  S -> I -> O * S.
+
+(** First component of the transition map: the output observation. *)
+Definition obs {S I O: Type} (m: mealy S I O) : S -> I -> O :=
+    fun s i => fst (m s i).
+  
+(** Second component of the transition map: the next state. *)
+Definition step {S I O: Type} (m: mealy S I O) : S -> I -> S :=
+    fun s i => snd (m s i).
+
+(** A [tuple_mealy] is a Mealy machine where inputs and outputs are
+    tuples [V^n] and [V^m], represented as untyped lists. *)
+Definition tuple_mealy (V S: Type) (n m : nat) :=
+  mealy S (list V) (list V).
+
+(* Sequential composition of two mealy machines, where the second
+   machine consumes all the outputs of the first machine as inputs. *)
+Definition seq (S1 S2 X Y Z: Type) (m1: mealy S1 X Y) (m2: mealy S2 Y Z) : mealy (S1 * S2) X Z :=
+  (* destructuring bindings '(pat : typ) are indicated with a tick
+     mark ' and allow you to put anything you'd put in a let
+     expression or the left hand side of a pattern match into a
+     function parameter. The type annotations here are optional
+     because Coq can infer them from the return type of this function
+     [mealy (S1 * S2) X Z]. *)
+  fun '((s1, s2): S1 * S2) (x: X) =>
+    let (y, s1') := m1 s1 x in
+    let (z, s2') := m2 s2 y in
+    (z, (s1', s2')).
+
+(* Parallel composition of two mealy machines. *)
+Definition par (S1 S2 U V X Y: Type) (m1: mealy S1 U V) (m2: mealy S2 X Y) : mealy (S1 * S2) (U * X) (V * Y) :=
+  fun '((s1, s2): S1 * S2) '((u, x): U * X) =>
+    let (v, s1') := m1 s1 u in
+    let (y, s2') := m2 s2 x in
+    ((v, y), (s1', s2')).
+
+(** * Mealy Machine Semantics: Stream Functions *)
+Section StreamFnInterp.
+  Variable (S I O : Type).
+  Variable (m: mealy S I O).
+
+  (** Interpret a Mealy machine as a stream function. This requires
+      you to provide an initial state [cur]. *)
+  CoFixpoint interp (cur: S) : streams.stream I -> streams.stream O :=
+    fun input =>
+      match input with
+      | i :.: rest =>
+          obs m cur i :.: interp (step m cur i) rest
+      end.
+
+End StreamFnInterp.
+
+    
diff --git a/vcalyx/coq/Parse.v b/vcalyx/coq/Parse.v
new file mode 100644
index 0000000000..82567e4ec1
--- /dev/null
+++ b/vcalyx/coq/Parse.v
@@ -0,0 +1,73 @@
+(** * Parsing Calyx Syntax from S-expressions *)
+(** This file defines a parser (deserializer) which turns an
+    s-expression format for Calyx programs into Calyx ASTs, as defined
+    in the Syntax module. We use the [coq-ceres] library. *)
+
+From stdpp Require Import list strings.
+From VCalyx Require Import IRSyntax.
+From Ceres Require Import Ceres.
+
+Definition oops : forall {A}, () -> A.
+Admitted.
+
+Global Instance Deserialize_direction : Deserialize direction :=
+    Deser.match_con "direction"
+                    [ ("input", Input);
+                      ("output", Output) ]
+                    [].
+
+Global Instance Deserialize_port : Deserialize port :=
+  fun _ _ => oops ().
+
+Global Instance Deserialize_prim : Deserialize prim :=
+  fun _ _ => oops ().
+
+Global Instance Deserialize_extern : Deserialize extern :=
+  fun _ _ => oops ().
+
+Global Instance Deserialize_proto : Deserialize proto :=
+  fun _ _ => oops ().
+
+Global Instance Deserialize_cell : Deserialize cell :=
+  fun _ _ => oops ().
+
+Global Instance Deserialize_port_ref : Deserialize port_ref :=
+  fun _ _ => oops ().
+
+Global Instance Deserialize_num : Deserialize num :=
+  fun _ _ => oops ().
+
+Global Instance Deserialize_atom : Deserialize atom :=
+  fun _ _ => oops ().
+
+Global Instance Deserialize_guard_cmp : Deserialize guard_cmp :=
+    Deser.match_con "guard_cmp"
+                    [ ("eq", Eq);
+                      ("neq", Neq);
+                      ("gt", Gt);
+                      ("lt", Lt);
+                      ("geq", Geq);
+                      ("leq", Leq) ]
+                    [].
+
+Global Instance Deserialize_guard_expr : Deserialize guard_expr :=
+  fun _ _ => oops ().
+
+Global Instance Deserialize_assignment : Deserialize assignment :=
+  fun _ _ => oops ().
+
+Global Instance Deserialize_control : Deserialize control :=
+  fun _ _ => oops ().
+
+Global Instance Deserialize_group : Deserialize group :=
+  fun _ _ => oops ().
+
+Global Instance Deserialize_comp : Deserialize comp :=
+  fun _ _ => oops ().
+
+Global Instance Deserialize_context : Deserialize context :=
+  fun _ _ => oops ().
+
+(* Entry point for the parser *)
+Definition parse_context (s: string) : error + context :=
+  from_string s.
diff --git a/vcalyx/coq/Semantics.v b/vcalyx/coq/Semantics.v
new file mode 100644
index 0000000000..c7f83025a2
--- /dev/null
+++ b/vcalyx/coq/Semantics.v
@@ -0,0 +1,617 @@
+From stdpp Require Import
+     base
+     fin_maps
+     gmap
+     numbers
+     list
+     strings
+     option.
+Require Import Coq.Classes.EquivDec.
+Require Import VCalyx.IRSyntax.
+Require Import VCalyx.Exception.
+Require Import VCalyx.Value.
+Require Import VCalyx.Arith.
+
+Inductive numtype :=
+| Bitnum
+| FixedPoint.
+    
+Record mem_fmt := { is_signed: bool;
+                    numeric_type: numtype;
+                    width: nat; }.
+
+Definition mem_data := list N.
+
+Inductive state : Type :=
+(* std_reg *)
+| StateReg (write_done: value) (val: value)
+(* std_mem_d1 *)
+| StateMemD1 (write_done: value) (fmt: mem_fmt) (contents: mem_data)
+| StateDiv (div_done: value) (quotient remainder: value)
+(* A primitive with no internal state *)
+| StateComb.
+
+Definition get_reg_state (st: state) :=
+  match st with
+  | StateReg write_done v => mret (write_done, v)
+  | _ => err "get_reg_state"
+  end.
+
+Definition get_mem_d1_state (st: state) :=
+  match st with
+  | StateMemD1 write_done fmt contents => mret (write_done, fmt, contents)
+  | StateReg _ _ => err "get_mem_d1_state: got reg"
+  | StateDiv _ _ _ => err "get_mem_d1_state: got div"
+  | StateComb => err "get_mem_d1_state: got comb"
+  end.
+
+Definition is_mem_state_bool (st: state) : bool :=
+  match st with
+  | StateMemD1 _ _ _ => true
+  | _ => false
+  end.
+
+Definition get_div_state (st: state) :=
+  match st with
+  | StateDiv div_done quot rem => mret (div_done, quot, rem)
+  | _ => err "get_div_state"
+  end.
+
+Section Semantics.
+  (* ENVIRONMENTS AND STORES *)
+  (* Definitions of types of finite maps used in the semantics. *)
+  Context (ident_map: Type -> Type).
+  Context `{FinMap ident ident_map}.
+  (* TODO put the computations in here *)
+  (* map from port names to values *)
+  Definition val_map : Type := ident_map value.
+  (* map from cell names to port names to values *)
+  Definition cell_map : Type := ident_map val_map.
+  (* map from cell name to state *)
+  Definition state_map : Type := ident_map state.
+
+  (* environment collecting all defined cells *)
+  Definition cell_env : Type := ident_map cell.
+
+  Record prim_sem :=
+    { prim_sem_poke: state -> val_map -> exn val_map;
+      prim_sem_tick: state -> val_map -> exn state }.
+  
+  (* An environment collecting all defined primitives *)
+  Definition prim_map : Type := ident_map prim_sem.
+
+  (* An environment collecting all defined groups *)
+  Definition group_env : Type := ident_map group.
+  (* map from group name to active flag + values of its holes *)
+  Definition group_map : Type := ident_map (bool * val_map).
+
+  Variable (calyx_prims : prim_map).
+
+  Open Scope stdpp_scope.
+  Definition is_entrypoint (entrypoint: ident) (c: comp) : bool :=
+    bool_decide (entrypoint = c.(comp_name)).
+
+  (* LOADING AND ALLOCATION *)
+  Definition load_group (ge: group_env) (g: group) : group_env :=
+    <[g.(group_name) := g]>ge.
+
+  Definition load_groups (ge: group_env) (c: comp) :=
+    foldl load_group ge c.(comp_groups).
+
+  Definition load_cell (ce: cell_env) (c: cell) : cell_env :=
+    <[c.(cell_name) := c]>ce.
+
+  Definition load_cells (ce: cell_env) (c: comp) :=
+    foldl load_cell ce c.(comp_cells).
+
+  Definition load_comp : cell_env * group_env -> comp -> cell_env * group_env :=
+    fun '(ce, ge) (c: comp) =>
+      (load_cells ce c, load_groups ge c).
+
+  Definition load_cells_groups (c: context) : cell_env * group_env := 
+    foldl load_comp (empty, empty) c.(ctx_comps).
+
+  Definition allocate_val_map (c: cell) : val_map :=
+    foldl (fun σ p => <[p.(port_name) := Bot]>σ)
+          empty
+          (c.(cell_in_ports) ++ c.(cell_out_ports)).
+
+  Definition allocate_cell_map (ce: cell_env) : cell_map :=
+    fmap allocate_val_map ce.
+
+  (* Initialize go and done holes to undef *)
+  Definition allocate_group_map (ge: group_env) : group_map :=
+    fmap (fun (g: group) => (false, <["go" := Bot]>(<["done" := Bot]>empty))) ge.
+
+  Definition prim_initial_state (name: ident) : exn state :=
+    if decide (name = "std_reg")
+    then mret (StateReg Bot Bot)
+    else if decide (name = "std_add")
+    then mret StateComb
+    else if decide (name = "std_lt")
+    then mret StateComb
+    else if decide (name = "std_or")
+    then mret StateComb
+    else if decide (name = "std_const")
+    then mret StateComb
+    else if decide (name = "std_div_pipe")
+    then mret (StateDiv Bot Bot Bot)
+    else err ("prim_initial_state: " +:+ name +:+ " is unimplemented").
+
+  Definition allocate_state_for_cell (c: cell) (ρ: state_map) : exn state_map :=
+    match c.(cell_proto) with
+    | ProtoPrim prim_name bindings is_comb =>
+        st ← prim_initial_state prim_name;
+        mret (<[c.(cell_name) := st]>ρ)
+    | ProtoThis
+    | ProtoConst _ _
+    | ProtoComp _ => mret ρ (* TODO FIX *)
+    end.
+
+  Definition allocate_state_map (ce: cell_env) (initial: state_map) : exn state_map :=
+    map_fold (fun name (c: cell) (ρ0: exn state_map) =>
+                ρ ← ρ0;
+                match initial !! c.(cell_name) with
+                | Some st__init => mret (<[c.(cell_name) := st__init]>ρ)
+                | None => allocate_state_for_cell c ρ
+                end)
+             (inl empty)
+             ce.
+
+  (* COMBINATIONAL UPDATES *)
+  Definition poke_prim (prim: ident) (param_binding: list (ident * N)) (st: state) (inputs: val_map) : exn val_map := 
+    fns ← lift_opt ("poke_prim: " +:+ prim +:+ " not found")
+                   (calyx_prims !! prim);
+    fns.(prim_sem_poke) st inputs.
+  
+  Definition poke_cell (c: cell) (ρ: state_map) (σ: cell_map) : exn cell_map :=
+    match c.(cell_proto) with
+    | ProtoPrim prim param_binding _ =>
+        st ← lift_opt "poke_cell" (ρ !! c.(cell_name));
+        vs ← lift_opt "poke_cell" (σ !! c.(cell_name));
+        vs' ← poke_prim prim param_binding st vs;
+        mret (<[c.(cell_name) := vs']>σ)
+    | ProtoComp c => err "tick_cell: ProtoComp unimplemented"
+    | ProtoThis => err "tick_cell: ProtoThis unimplemented"
+    | ProtoConst val width =>
+        let vs := <["out" := V val]>empty in
+        mret (<[c.(cell_name) := vs]>σ)
+    end.
+
+  Definition tick_prim (prim: ident) (param_binding: list (ident * N)) (st: state) (inputs: val_map) : exn state := 
+    fns ← lift_opt ("tick_prim: " +:+ prim +:+ " not found")
+                   (calyx_prims !! prim);
+    match fns.(prim_sem_tick) st inputs with 
+    | inl ok => inl ok
+    | inr error => inr ("tick_prim for " +:+ prim +:+ ": " +:+ error)
+    end.
+
+  Definition tick_cell (c: cell) (ρ: state_map) (σ: cell_map) : exn state_map :=
+    match c.(cell_proto) with
+    | ProtoPrim prim param_binding _ =>
+        st ← lift_opt ("tick_cell: " +:+ c.(cell_name) +:+ " not found in state_map")
+                      (ρ !! c.(cell_name));
+        vs ← lift_opt ("tick_cell: " +:+ c.(cell_name) +:+ " not found in cell_map")
+                      (σ !! c.(cell_name));
+        st' ← tick_prim prim param_binding st vs;
+        mret (<[c.(cell_name) := st']>ρ)
+    | ProtoComp c => err "tick_cell: ProtoComp unimplemented"
+    | ProtoThis => err "tick_cell: ProtoThis unimplemented"
+    | ProtoConst _ _ => mret ρ
+    end.
+
+  Definition poke_all_cells (ce: cell_env) (ρ: state_map) (σ: cell_map) : exn cell_map :=
+    map_fold (fun _ cell σ_opt =>
+                σ ← σ_opt;
+                poke_cell cell ρ σ)
+             (inl σ)
+             ce.
+
+  (* Update the state, invalidate outgoing wires *)
+  Definition tick_all_cells (ce: cell_env) (ρ: state_map) (σ: cell_map) : exn state_map :=
+    (*
+    err (map_fold (fun key cell acc =>
+                     let prim := match cell.(cell_proto) with
+                                 | ProtoPrim prim param_binding _ => prim
+                                 | _ => "<no prim>"
+                                 end in
+                key +:+ ":" +:+ prim +:+ " " +:+ acc)
+             ""
+             ce). *)
+    map_fold (fun _ cell ρ_opt =>
+                ρ ← ρ_opt;
+                tick_cell cell ρ σ)
+             (inl ρ)
+             ce.
+
+  Definition catch {X} (c1 c2: option X) : option X :=
+    match c1 with
+    | Some x => Some x
+    | None => c2
+    end.
+
+  Definition read_port_ref (p: port_ref) (σ: cell_map) (γ: group_map) : exn value :=
+    match p with
+    | PRef parent port =>
+        lift_opt "read_port_ref: port not found"
+                 (catch (σ !! parent ≫= (!!) port)
+                        (γ !! parent ≫= (!!) port ∘ snd))
+    | _ => err "read_port_ref: ports other than PRef unimplemented"
+    end.
+
+  Definition write_port_ref (p: port_ref) (v: value) (σ: cell_map) (γ: group_map) : exn (cell_map * group_map) :=
+    match p with
+    | PRef parent port =>
+        if decide (is_Some (σ !! parent))
+        then mret (alter (insert port v) parent σ, γ)
+        else if decide (is_Some (γ !! parent))
+             then mret (σ, alter (fun '(active, holes) => (active, insert port v holes)) parent γ)
+             else err "write_port_ref: parent not found in group_map"
+    | _ => err "write_port_ref: ports other than PRef unimplemented"
+    end.
+
+  Definition set_group_active_bit (b: bool) (g: ident) (γ: group_map) : group_map :=
+    alter (fun '(active, holes) => (b, holes)) g γ.
+
+  Definition mark_group_active : ident -> group_map -> group_map :=
+    set_group_active_bit true.
+
+  Definition mark_group_inactive : ident -> group_map -> group_map :=
+    set_group_active_bit false.
+
+  Definition incorp (lhs rhs: value) : value :=
+    match lhs with
+    | Bot => rhs
+    | _ => Top
+    end.
+  
+  Definition interp_assign
+             (ce: cell_env)
+             (ρ: state_map)
+             (σ: cell_map) 
+             (γ: group_map)
+             (op: assignment)
+    : exn (cell_map * group_map) :=
+    σ' ← poke_all_cells ce ρ σ;
+    lhs ← read_port_ref op.(dst) σ' γ;
+    rhs ← read_port_ref op.(src) σ' γ;
+    '(σ'', γ') ← write_port_ref op.(dst) rhs σ' γ;
+    mret (σ'', γ').
+
+  Definition poke_group ce ρ σ γ (g: group) : exn (cell_map * group_map) := 
+    (* there is probably a monad sequencing operation that should be used here *)
+    (* n.b. this defintion using foldl assumes the assignments are
+            already in dataflow order and will not require iteration
+            to reach a fixed point. *)
+    foldl (fun res op =>
+             '(σ, γ) ← res;
+             interp_assign ce ρ σ γ op)
+          (mret (σ, γ))
+          g.(group_assns).
+
+  Definition is_done (γ: group_map) (g: ident) : bool :=
+    match '(_, holes) ← γ !! g;
+          holes !! "done" with
+    | Some v => is_one v
+    | None => false
+    end.
+
+  Definition cycle_group (ce: cell_env) (ρ: state_map) (σ: cell_map) (γ: group_map) (g: group) : exn (state_map * cell_map * group_map) :=
+    ρ ← tick_all_cells ce ρ σ;
+    '(σ, γ) ← poke_group ce ρ σ γ g;
+    inl (ρ, σ, γ).
+
+  Definition cycle_groups (ce: cell_env) (ρ: state_map) (σ: cell_map) (γ: group_map) (gs: list group) : exn (state_map * cell_map * group_map) :=
+    foldl (fun res g =>
+             '(ρ, σ, γ) ← res;
+             cycle_group ce ρ σ γ g)
+          (mret (ρ, σ, γ)) gs.
+
+  (* Two size functions for getting a handle on nested recursion *)
+  Fixpoint control_size (ctrl: control) : nat :=
+    match ctrl with
+    | CSeq ctrls _ =>
+        1 + (fix controls_size cs :=
+               match cs with
+               | c :: cs => control_size c + controls_size cs
+               | [] => 0
+               end) ctrls
+    | _ => 1
+    end.
+
+  Fixpoint control_size_exn (ctrl: control) : exn nat :=
+    match ctrl with
+    | CSeq ctrls _ =>
+        v ← (fix controls_size_exn cs : exn nat :=
+               match cs with
+               | c :: cs =>
+                   n ← control_size_exn c;
+                   m ← controls_size_exn cs;
+                   mret $ n + m
+               | [] => mret $ 0
+               end) ctrls;
+       mret (1 + v)
+    | _ => mret 1
+    end.
+
+  Definition ctrl_is_done (ctrl: control) : bool :=
+    match ctrl with
+    | CSeq [] _
+    | CPar [] _
+    | CEmpty _ => true
+    | CSeq _ _
+    | CPar _ _
+    | CIf _ _ _ _ _
+    | CWhile _ _ _ _
+    | CEnable _ _
+    | CWaitGroup _ _
+    | CInvoke _ _ _ _ _ _
+    | CWaitComp _ _ => false
+    end.
+
+  Fixpoint open_control (ctrl: control) : exn control :=
+    match ctrl with
+    | CEnable group attrs =>
+        mret $ CWaitGroup group attrs
+    | CSeq ctrls attrs =>
+        ctrls' ← (fix open_controls (cs: list control) : exn (list control) :=
+                    match cs with
+                    | c :: cs =>
+                        if ctrl_is_done c
+                        then open_controls cs
+                        else c ← open_control c;
+                             cs ← open_controls cs;
+                             mret $ c :: cs
+                    | [] => mret $ []
+                    end) ctrls;
+        mret $ match ctrls' with
+               | [] => CEmpty attrs
+               | ctrls' => CSeq ctrls' attrs
+               end
+    | CPar ctrls attrs =>
+        if forallb ctrl_is_done ctrls
+        then mret $ CEmpty attrs
+        else ctrls' ← mapM (open_control) ctrls;
+        mret $ CPar ctrls' attrs
+    | CWaitGroup g attrs => mret $ CWaitGroup g attrs
+    | CWaitComp c attrs => mret $ CWaitComp c attrs
+    | CEmpty attrs => mret $ CEmpty attrs
+    | CIf cond_port cond_group then_ctrl else_ctrl attrs =>
+        mret $ CIf cond_port cond_group then_ctrl else_ctrl attrs
+    | CWhile cond_port cond_group body_ctrl attrs =>
+        mret $ CWhile cond_port cond_group body_ctrl attrs
+    | CInvoke _ _ _ _ _ _ => err "open_control: CInvoke unimplemented"
+    end.
+
+  Fixpoint close_control γ (ctrl: control) {struct ctrl} : exn control :=
+    match ctrl with
+    | CEnable group attrs =>
+      mret $ CEnable group attrs
+    | CSeq stmts attrs =>
+        stmts' ← (fix close_controls (stmts: list control) : exn (list control) :=
+           match stmts with
+           | stmt :: stmts =>
+               if ctrl_is_done stmt
+               then close_controls stmts
+               else stmt' ← close_control γ stmt;
+                    mret $ stmt' :: stmts
+           | [] => mret $ []
+           end) stmts;
+        mret $ match stmts' with
+               | [] => CEmpty attrs
+               | ctrls' => CSeq stmts' attrs
+               end
+    | CPar stmts attrs =>
+        stmts' ← mapM (close_control γ) stmts;
+        mret $ CPar stmts' attrs
+    | CWaitGroup group attrs =>
+        if is_done γ group
+        then mret $ CEmpty attrs
+        else mret $ CWaitGroup group attrs
+    | CWaitComp comp _ => err "close_control: CWaitComp unimplemented"
+    | CEmpty attrs => mret $ CEmpty attrs
+    | CIf cond_port cond tru fls attrs =>
+        err "close_control: CIf unimplemented"
+    | CWhile cond_port cond body attrs =>
+        err "close_control: CWhile unimplemented"
+    | CInvoke _ _ _ _ _ _ => err "close_control: CInvoke unimplemented"
+    end.
+
+  Fixpoint cycle_active_cells (ce: cell_env) (ge: group_env) (ρ: state_map) (σ: cell_map) (γ: group_map) (ctrl: control) : exn (state_map * cell_map * group_map) :=
+      match ctrl with
+      | CWaitGroup group _ =>
+        g ← lift_opt ("cycle_active_cells: group " +:+ group +:+ " not found in group_env")
+                    (ge !! group);
+        cycle_group ce ρ σ γ g
+      | CSeq (ctrl :: ctrls) attrs =>
+        cycle_active_cells ce ge ρ σ γ ctrl
+      | CSeq [] _ => mret (ρ, σ, γ)
+      | CIf cond_port cond_group then_ctrl else_ctrl _ =>
+        (* n.b. we don't implement with right now *)
+        port_val ← read_port_ref cond_port σ γ;
+        if is_nonzero port_val
+        then cycle_active_cells ce ge ρ σ γ then_ctrl
+        else cycle_active_cells ce ge ρ σ γ else_ctrl
+      | CEnable _ _
+      | CInvoke _ _ _ _ _ _
+      | CEmpty _ => mret (ρ, σ, γ)
+      | CPar ctrls attrs => err "cycle_active_cells: CPar unimplemented"
+      | CWhile _ _ _ _ => err "cycle_active_cells: CWhile unimplemented"
+      | CWaitComp _ _ => err "cycle_active_cells: CWaitComp unimplemented"
+      end.
+
+  Definition find_entrypoint (name: ident) (comps: list comp) :=
+    lift_opt ("find_entrypoint: " +:+ name +:+ " not found")
+             (List.find (is_entrypoint name) comps).
+
+  Definition load_context (c: context) (mems: state_map) :=
+    main ← find_entrypoint c.(ctx_entrypoint) c.(ctx_comps);
+    let '(ce, ge) := load_cells_groups c in
+    let σ := allocate_cell_map ce in
+    let γ := allocate_group_map ge in
+    ρ ← allocate_state_map ce mems;
+    mret (ce, ge, ρ, σ, γ, main.(comp_control)).
+
+  Definition tick_control (ce: cell_env) (ge: group_env) (ρ: state_map) (σ: cell_map) (γ: group_map) (ctrl: control) : exn (control * state_map * cell_map * group_map) :=
+    ctrl ← open_control ctrl;
+    '(ρ, σ, γ) ← cycle_active_cells ce ge ρ σ γ ctrl;
+    ctrl ← close_control γ ctrl;
+    mret (ctrl, ρ, σ, γ).
+
+  Fixpoint interp_control (ce: cell_env) (ge: group_env) (ρ: state_map) (σ: cell_map) (γ: group_map) (ctrl: control) (gas: nat) : exn (state_map * cell_map * group_map) :=
+    match gas with
+    | 0 => err "interp_control: out of gas"
+    | S gas => if ctrl_is_done ctrl
+              then mret (ρ, σ, γ)
+              else '(ctrl, ρ, σ, γ) ← tick_control ce ge ρ σ γ ctrl;
+                   interp_control ce ge ρ σ γ ctrl gas
+    end.
+
+  Definition interp_context (c: context) (mems: state_map) (gas: nat) : exn (state_map * cell_map * group_map) :=
+    '(ce, ge, ρ, σ, γ, ctrl) ← load_context c mems;
+    interp_control ce ge ρ σ γ ctrl gas.
+
+  Definition extract_mems (ρ: state_map) : list (ident * state) :=
+    List.filter (fun '(name, st) => is_mem_state_bool st) (map_to_list ρ).
+
+End Semantics.
+
+Definition assoc_list K V := list (K * V).
+#[export] Instance assoc_list_FMap (K: Type) : FMap (assoc_list K) :=
+  fun V V' f => List.map (fun '(k, v) => (k, f v)).
+
+#[export] Instance assoc_list_Lookup : forall V, Lookup string V (assoc_list string V) :=
+  fun _ needle haystack =>
+    match List.find (fun '(k, v) => if string_eq_dec k needle then true else false) haystack with
+    | Some (_, v) => Some v
+    | None => None
+    end.
+
+#[export] Instance assoc_list_Empty: forall V, Empty (assoc_list string V) :=
+  fun _ => [].
+
+Fixpoint assoc_list_partial_alter (V: Type) (f: option V -> option V) (k: string) (l: assoc_list string V) : assoc_list string V :=
+  match l with
+  | [] =>
+      match f None with
+      | Some fv => [(k, fv)]
+      | None => []
+      end
+  | (k', v)::l =>
+      if string_eq_dec k k'
+      then match f (Some v) with
+           | Some fv => (k, fv)::l
+           | None => l
+           end
+      else (k', v)::assoc_list_partial_alter V f k l
+  end.
+
+#[export] Instance assoc_list_PartialAlter: ∀ V : Type, PartialAlter string V (assoc_list string V) :=
+  assoc_list_partial_alter.
+
+#[export] Instance assoc_list_OMap: OMap (assoc_list string) :=
+  fun V B f m =>
+    [].
+
+#[export] Instance assoc_list_Merge: Merge (assoc_list string) :=
+  fun _ _ _ _ _ _ => [].
+
+#[export] Instance assoc_list_FinMapToList: forall V, FinMapToList string V (assoc_list string V) :=
+  fun _ => id.
+
+#[export] Instance assoc_list_finmap: FinMap string (assoc_list string).
+Admitted.
+
+Definition calyx_prims : prim_map (assoc_list string) :=
+  [
+    ("std_reg",
+      {| prim_sem_poke st inputs :=
+        '(write_done, v) ← get_reg_state st;
+        mret (<["done" := write_done]>(<["out" := v]>inputs));
+        prim_sem_tick st inputs :=
+        '(_, val_old) ← get_reg_state st;
+        write_en ← lift_opt "std_reg tick: write_en missing"
+                 (inputs !! "write_en");
+        if is_one write_en
+        then val_in ← lift_opt "std_reg tick: in missing" (inputs !! "in");
+          mret (StateReg (V 1%N) val_in)
+        else mret (StateReg (V 0%N) val_old)
+      |});
+    ("std_mem_d1",
+      {| prim_sem_poke st inputs :=
+        '(write_done, fmt, contents) ← get_mem_d1_state st;
+        addr ← lift_opt "std_mem_d1 poke: addr0 missing" (inputs !! "addr0");
+        mem_val ← match addr with
+                  | Top => mret Top
+                  | V idx => V <$> lift_opt "std_mem_d1 poke: out of bounds access" (contents !! (N.to_nat idx))
+                  | Bot => mret Bot
+                  end;
+        mret (<["done" := write_done]>(<["read_data" := mem_val]>inputs));
+        prim_sem_tick st inputs :=
+        '(_, fmt, contents) ← get_mem_d1_state st;
+        write_en ← lift_opt "std_mem_d1 tick: write_en missing"
+                 (inputs !! "write_en");
+        if is_one write_en
+        then val_in ← lift_opt "std_mem_d1 tick: write_data missing" (inputs !! "write_data");
+          val ← expect_V val_in;
+          addr ← lift_opt "st_mem_d1 tick: addr0 missing" (inputs !! "addr0");
+          idx ← expect_V addr;
+          mret (StateMemD1 (V 1%N) fmt (<[N.to_nat idx := val]>contents))
+        else mret (StateMemD1 (V 0%N) fmt contents)
+      |});
+    ("std_const",
+      {| prim_sem_poke st inputs := mret inputs;
+         prim_sem_tick st inputs := mret st;
+      |});
+    ("std_lt",
+      {| prim_sem_poke st inputs :=
+           val_left ← lift_opt "std_lt poke: left missing" (inputs !! "left");
+           val_right ← lift_opt "std_lt poke: right missing" (inputs !! "right");
+           let val_out := value_lt val_left val_right in
+           mret (<["out" := val_out]>inputs);
+         prim_sem_tick st inputs := mret st;
+      |});
+    ("std_or",
+      {| prim_sem_poke st inputs :=
+           val_left ← lift_opt "std_or poke: left missing" (inputs !! "left");
+           val_right ← lift_opt "std_or poke: right missing" (inputs !! "right");
+           let val_out := value_or val_left val_right in
+           mret (<["out" := val_out]>inputs);
+         prim_sem_tick st inputs := mret st;
+      |});
+    ("std_add",
+      {| prim_sem_poke st inputs :=
+           val_left ← lift_opt "std_add poke: left missing" (inputs !! "left");
+           val_right ← lift_opt "std_add poke: right missing" (inputs !! "right");
+           let val_out := value_add val_left val_right in
+           mret (<["out" := val_out]>inputs);
+         prim_sem_tick st inputs := mret st;
+      |});
+    ("std_div_pipe",
+      {| prim_sem_poke st inputs :=
+           '(div_done, div_quotient, div_remainder) ← get_div_state st;
+           mret (<["done" := div_done]>
+                   (<["out_quotient" := div_quotient]>
+                      (<["out_remainder" := div_remainder]>
+                         inputs)));
+         prim_sem_tick st inputs :=
+           '(div_done, div) ← get_div_state st;
+           go ← lift_opt "std_div_pipe tick: go missing"
+                         (inputs !! "go");
+           if is_one go
+           then val_left ← lift_opt "std_div_pipe poke: left missing" (inputs !! "left");
+                val_right ← lift_opt "std_div_pipe poke: right missing" (inputs !! "right");
+                let val_out_quotient := value_div_quotient val_left val_right in
+                let val_out_remainder := value_div_remainder val_left val_right in
+                mret (StateDiv (V 1%N) val_out_quotient val_out_remainder)
+           else mret (StateDiv (V 0%N) Bot Bot)
+      |})
+  ].
+
+(* interp_context instantiated with the gmap finite map data structure *)
+Definition interp_with_mems (c: context) (mems: list (ident * state)) (gas: nat) :=
+  let mems := list_to_map mems in
+  '(ρ, σ, γ) ← interp_context (assoc_list ident) calyx_prims c mems gas;
+  mret (extract_mems _ ρ).
+
+Definition find_prim s := calyx_prims !! s.
diff --git a/vcalyx/coq/Value.v b/vcalyx/coq/Value.v
new file mode 100644
index 0000000000..f0a4b2de35
--- /dev/null
+++ b/vcalyx/coq/Value.v
@@ -0,0 +1,35 @@
+From stdpp Require Import
+     base
+     strings
+     numbers.
+Require Import Coq.Classes.EquivDec.
+Require Import VCalyx.Exception.
+
+Inductive value := 
+(* Top: more than 1 assignment to this port has occurred *)
+| Top 
+(* If only 1 assignment has occurred, this value is in port.in *)
+| V (val: N)
+(* Bottom: no assignment to this port has occurred *)
+| Bot.
+Scheme Equality for value.
+#[export] Instance value_EqDec : EqDec value eq :=
+  value_eq_dec.
+
+Definition expect_V (v: value) : exn N :=
+  match v with
+  | V val => mret val
+  | _ => err "expect_V"
+  end.
+
+Definition is_one (v: value) :=
+  v ==b (V 1%N).
+
+Definition is_nonzero (v: value) :=
+  v <>b (V 0%N).
+
+Definition bool_to_N (b: bool) : N :=
+  if b then 1%N else 0%N.
+
+Definition bool_to_value (b: bool) : value :=
+  V (bool_to_N b).
diff --git a/vcalyx/coq/Vect.v b/vcalyx/coq/Vect.v
new file mode 100644
index 0000000000..87450e8883
--- /dev/null
+++ b/vcalyx/coq/Vect.v
@@ -0,0 +1,16 @@
+(** * Vectors *)
+
+(** This vector type indexes the tuple types [unit], [T * unit], [T *
+    T * unit], etc., as a fixpoint. The approach in the Coq standard
+    library uses an inductive type. We use a fixpoint so that for
+    particular values of [n] the type [vect T n] is _definitionally
+    equal_ to the corresponding tuple type [T * T * ... * unit],
+    rather than merely isomorphic. *)
+Fixpoint vect T n : Type :=
+  match n with
+  | 0 => unit
+  | S n => vect T n * T
+  end.
+
+Definition bitvec n : Type :=
+  vect bool n.
diff --git a/vcalyx/coq/dune b/vcalyx/coq/dune
new file mode 100644
index 0000000000..18526071e7
--- /dev/null
+++ b/vcalyx/coq/dune
@@ -0,0 +1,5 @@
+(coq.theory
+ (name VCalyx)
+ (package vcalyx)
+ (theories stdpp Ceres)
+ (modules (:standard)))
diff --git a/vcalyx/dune-project b/vcalyx/dune-project
new file mode 100644
index 0000000000..664a9271e0
--- /dev/null
+++ b/vcalyx/dune-project
@@ -0,0 +1,26 @@
+(lang dune 3.8)
+(using coq 0.8)
+(using menhir 2.1)
+(name vcalyx)
+
+(generate_opam_files true)
+
+(package
+ (name vcalyx)
+ (version dev)
+ (synopsis     "Coq formalization of the Calyx language")
+ (maintainers  "Ryan Doenges and Priya Srikumar")
+ (authors      "Ryan Doenges and Priya Srikumar")
+ (homepage     "https://github.com/cucapra/calyx/tree/vcalyx")
+ (bug_reports  "https://github.com/cucapra/calyx/tree/vcalyx")
+ (license      "MIT")
+ (depends
+   (core (>= "0.15.0"))
+   (ppx_let (>= "0.15.0"))
+   (stdlib-shims (>= "0.3.0"))
+   (coq-ceres (>= "0.4.0"))
+   (coq-stdpp (>= "1.8.0"))
+   (coq (>= "8.15.2"))
+   (menhir (>= "20230608"))
+   (yojson (>= "2.1.0"))
+   (ocamlformat (and :build (>= "0.24.1")))))
diff --git a/vcalyx/examples/basic.expect b/vcalyx/examples/basic.expect
new file mode 100644
index 0000000000..0967ef424b
--- /dev/null
+++ b/vcalyx/examples/basic.expect
@@ -0,0 +1 @@
+{}
diff --git a/vcalyx/examples/basic.futil b/vcalyx/examples/basic.futil
new file mode 100644
index 0000000000..961f32c828
--- /dev/null
+++ b/vcalyx/examples/basic.futil
@@ -0,0 +1,21 @@
+import "primitives/core.futil";
+
+component main() -> () {
+  cells {
+    reg1 = std_reg(32);
+    const0 = std_const(32, 2);
+  }
+
+  wires {
+    group move {
+      reg1.write_en = 1'd1;
+      reg1.in = const0.out;
+
+      move[done] = reg1.done;
+    }
+  }
+
+  control {
+    move;
+  }
+}
\ No newline at end of file
diff --git a/vcalyx/examples/basic.futil.data b/vcalyx/examples/basic.futil.data
new file mode 100644
index 0000000000..0967ef424b
--- /dev/null
+++ b/vcalyx/examples/basic.futil.data
@@ -0,0 +1 @@
+{}
diff --git a/vcalyx/examples/comb.expect b/vcalyx/examples/comb.expect
new file mode 100644
index 0000000000..0967ef424b
--- /dev/null
+++ b/vcalyx/examples/comb.expect
@@ -0,0 +1 @@
+{}
diff --git a/vcalyx/examples/comb.futil b/vcalyx/examples/comb.futil
new file mode 100644
index 0000000000..83b258d754
--- /dev/null
+++ b/vcalyx/examples/comb.futil
@@ -0,0 +1,44 @@
+import "primitives/core.futil";
+import "primitives/binary_operators.futil";
+
+component main() -> () {
+  cells {
+    input0 = std_const(32, 21);
+    input1 = std_const(32, 2);
+    reg_q = std_reg(32);
+    reg_r = std_reg(32);
+    div = std_div_pipe(32);
+    or0 = std_or(32);
+    result = std_reg(32);
+  }
+
+  wires {
+    group div_group {
+      div.go = 1'd1; 
+      div.left = input0.out; 
+      div.right = input1.out; 
+      reg_q.write_en = div.done ? 1'd1; 
+      reg_r.write_en = div.done ? 1'd1; 
+      reg_q.in = div.out_quotient;
+      reg_r.in = div.out_remainder; 
+      div_group[done] = reg_q.done & reg_r.done ? 1'd1;
+    }
+    // reg_r should be 1, reg_q should be 10
+    group or_group {
+      or0.left = reg_q.out;
+      or0.right = reg_r.out; 
+
+      result.write_en = 1'd1;
+      result.in = or0.out; 
+      or_group[done] = result.done;
+    }
+    // result should be 11
+  }
+
+  control {
+    seq {
+      div_group;
+      or_group;
+    }
+  }
+}
\ No newline at end of file
diff --git a/vcalyx/examples/comb.futil.data b/vcalyx/examples/comb.futil.data
new file mode 100644
index 0000000000..0967ef424b
--- /dev/null
+++ b/vcalyx/examples/comb.futil.data
@@ -0,0 +1 @@
+{}
diff --git a/vcalyx/examples/empty.expect b/vcalyx/examples/empty.expect
new file mode 100644
index 0000000000..0967ef424b
--- /dev/null
+++ b/vcalyx/examples/empty.expect
@@ -0,0 +1 @@
+{}
diff --git a/vcalyx/examples/empty.futil b/vcalyx/examples/empty.futil
new file mode 100644
index 0000000000..2134bebc17
--- /dev/null
+++ b/vcalyx/examples/empty.futil
@@ -0,0 +1,14 @@
+component main() -> () {
+  cells {
+  }
+
+  wires {
+    group g {
+      g[done] = 1'd1;
+    }
+  }
+
+  control {
+    g;
+  }
+}
diff --git a/vcalyx/examples/empty.futil.data b/vcalyx/examples/empty.futil.data
new file mode 100644
index 0000000000..0967ef424b
--- /dev/null
+++ b/vcalyx/examples/empty.futil.data
@@ -0,0 +1 @@
+{}
diff --git a/vcalyx/examples/ex.expect b/vcalyx/examples/ex.expect
new file mode 100644
index 0000000000..0967ef424b
--- /dev/null
+++ b/vcalyx/examples/ex.expect
@@ -0,0 +1 @@
+{}
diff --git a/vcalyx/examples/ex.futil b/vcalyx/examples/ex.futil
new file mode 100644
index 0000000000..86c2501765
--- /dev/null
+++ b/vcalyx/examples/ex.futil
@@ -0,0 +1,38 @@
+// -b sexp
+import "primitives/core.futil";
+
+component main() -> () {
+  cells {
+    reg0 = std_reg(32);
+    reg1 = std_reg(32);
+    adder = std_add(32);
+    result = std_reg(32);
+  }
+
+  wires {
+    group init {
+      reg0.write_en = 1'd1;
+      reg0.in = 32'd2;
+
+      reg1.write_en = 1'd1;
+      reg1.in = 32'd1;
+      init[done] = reg0.done & reg1.done ? 1'd1;
+    }
+
+    group incr {
+      adder.left = reg0.out;
+      adder.right = reg1.out;
+
+      result.write_en = 1'd1;
+      result.in = adder.out; 
+      incr[done] = result.done;
+    }
+  }
+
+  control {
+    seq {
+      init;
+      incr;
+    }
+  }
+}
\ No newline at end of file
diff --git a/vcalyx/examples/ex.futil.data b/vcalyx/examples/ex.futil.data
new file mode 100644
index 0000000000..0967ef424b
--- /dev/null
+++ b/vcalyx/examples/ex.futil.data
@@ -0,0 +1 @@
+{}
diff --git a/vcalyx/examples/if-reg.expect b/vcalyx/examples/if-reg.expect
new file mode 100644
index 0000000000..0967ef424b
--- /dev/null
+++ b/vcalyx/examples/if-reg.expect
@@ -0,0 +1 @@
+{}
diff --git a/vcalyx/examples/if-reg.futil b/vcalyx/examples/if-reg.futil
new file mode 100644
index 0000000000..1d2c6cdb0c
--- /dev/null
+++ b/vcalyx/examples/if-reg.futil
@@ -0,0 +1,48 @@
+import "primitives/core.futil";
+
+component main() -> () {
+  cells {
+    const0 = std_const(32, 15);
+    const1 = std_const(32, 10);
+    @external reg1 = std_reg(32);
+    @external reg0 = std_reg(1);
+    lt0 = std_lt(32);
+  }
+
+  wires {
+    group cond<"static"=1> {
+      reg0.write_en = 1'd1;
+      lt0.left = const0.out;
+      lt0.right = const1.out;
+      reg0.in = lt0.out;
+      cond[done] = reg0.done;
+    }
+
+    group mytrue<"static"=1> {
+      reg1.write_en = 1'd1;
+      reg1.in = 32'd15;
+      mytrue[done] = reg1.done;
+    }
+
+    group myfalse<"static"=1> {
+      reg1.write_en = 1'd1;
+      reg1.in = 32'd10;
+      myfalse[done] = reg1.done;
+    }
+  }
+
+  control {
+    //similar to [if.futil],
+    //b/c this isn't just 1 group prog, 
+    //reg1 should have [done] low 
+    //at the end of execution (tho prog. ends when reg1.done is high)
+    seq {
+      cond;
+      if reg0.out {
+        mytrue;
+      } else {
+        myfalse;
+      }
+    }
+  }
+}
\ No newline at end of file
diff --git a/vcalyx/examples/if-reg.futil.data b/vcalyx/examples/if-reg.futil.data
new file mode 100644
index 0000000000..0967ef424b
--- /dev/null
+++ b/vcalyx/examples/if-reg.futil.data
@@ -0,0 +1 @@
+{}
diff --git a/vcalyx/ocaml/dune b/vcalyx/ocaml/dune
new file mode 100644
index 0000000000..a5b70f45c7
--- /dev/null
+++ b/vcalyx/ocaml/dune
@@ -0,0 +1,30 @@
+(menhir
+ (modules parser)
+ ;(flags --trace)
+ )
+
+;(ocamllex
+; (modules lexer))
+(rule
+ (target lexer.ml)
+ (deps   lexer.mll)
+ (action (chdir %{workspace_root}
+          (run %{bin:ocamllex} -ml -q -o %{target} %{deps}))))
+
+(library
+ (name vcalyx)
+ (public_name vcalyx)
+ (modules parser lexer)
+ (libraries extr core yojson))
+
+(executable
+ (name vcx)
+ (public_name vcx)
+ (modules vcx)
+ (libraries core core_unix.command_unix extr vcalyx yojson)
+ (preprocess
+  (pps ppx_let ppx_deriving.show)))
+
+(test
+ (name test)
+ (modules test))
diff --git a/vcalyx/ocaml/extr/Extraction.v b/vcalyx/ocaml/extr/Extraction.v
new file mode 100644
index 0000000000..c0ba46fbc9
--- /dev/null
+++ b/vcalyx/ocaml/extr/Extraction.v
@@ -0,0 +1,23 @@
+(*! Extraction to OCaml !*)
+Set Warnings "-extraction-reserved-identifier".
+From VCalyx Require
+     IRSyntax
+     Parse
+     Semantics.
+Require Coq.extraction.Extraction.
+From Coq.extraction Require Import
+     ExtrOcamlBasic
+     ExtrOcamlNativeString
+     ExtrOcamlNatInt
+     ExtrOcamlZInt.
+
+Extract Constant VCalyx.Parse.oops => "(fun _ -> failwith ""oops!"")".
+
+(* This will extract all the listed identifiers and all their
+transitive dependencies. *)
+Extraction "extr.ml"
+           VCalyx.Semantics.interp_with_mems
+           VCalyx.Semantics.find_prim
+           VCalyx.IRSyntax.context
+           VCalyx.IRSyntax.is_in
+           VCalyx.IRSyntax.is_out.
diff --git a/vcalyx/ocaml/extr/dune b/vcalyx/ocaml/extr/dune
new file mode 100644
index 0000000000..73bf8c867a
--- /dev/null
+++ b/vcalyx/ocaml/extr/dune
@@ -0,0 +1,11 @@
+(library
+ (name extr)
+ (public_name vcalyx.extr)
+ (libraries stdlib-shims)
+ (flags
+  (:standard -w -3 -w -39 -w -33 -w -20 -w -27)))
+
+(coq.extraction
+ (prelude Extraction)
+ (extracted_modules extr)
+ (theories VCalyx stdpp Ceres))
diff --git a/vcalyx/ocaml/lexer.mll b/vcalyx/ocaml/lexer.mll
new file mode 100644
index 0000000000..b8397d9989
--- /dev/null
+++ b/vcalyx/ocaml/lexer.mll
@@ -0,0 +1,101 @@
+{ 
+  open Parser 
+  exception SyntaxError of string
+}
+
+let id = ['a'-'z' 'A'-'Z' '_'] ['a'-'z' 'A'-'Z' '0'-'9' '_' '.']*
+let whitespace = [' ' '\t']+
+let newline = '\r' | '\n' | "\r\n"
+
+rule tokens = parse 
+| eof             { EOF }
+(* i.e., 1'd1 *)
+| ['0'-'9']+ as i { INT (int_of_string i) } 
+| whitespace      { tokens lexbuf }
+| newline         { Lexing.new_line lexbuf; tokens lexbuf }
+| ['"']([^'"']* as s)['"'] { STRING s }
+| "."             { DOT }
+| "#("            { LPAREN }
+| "("             { LPAREN }
+| ")"             { RPAREN }
+| "components"    { COMPONENTS }
+| "Component"     { COMPONENT }
+| "entrypoint"    { ENTRYPOINT }
+| "name"          { NAME }
+| "signature"     { SIGNATURE }
+| "cells"         { CELLS }
+| "ports"         { PORTS }
+| "prototype"     { PROTOTYPE }
+| "ThisComponent" { THIS_COMPONENT }
+| "reference"     { REFERENCE }
+| "group"         { GROUP }
+| "groups"        { GROUPS }
+| "static_groups" { STATIC_GROUPS }
+| "comb_groups"   { COMB_GROUPS }
+| "continuous_assignments" {CONT_ASSNS}
+| "dst"           { DST }
+| "src"           { SRC }
+| "guard"         { GUARD }
+| "attributes"    { ATTRIBUTES }
+| "control"       { CONTROL }
+| "is_comb"       { IS_COMB }
+| "True"          { TRUE }
+| "#t"            { TRUE }
+| "#f"            { FALSE }
+| "Num"           { NUM }
+| "Go"            { GO }
+| "Done"          { DONE }
+| "Static"        { STATIC }
+| "WriteTogether" { WRITE_TOGETHER }
+| "ReadTogether"  { READ_TOGETHER }
+| "Bool"          { BOOL }
+| "TopLevel"      { TOP_LEVEL }
+| "External"      { EXTERNAL }
+| "NoInterface"   { NO_INTERFACE }
+| "Reset"         { RESET }
+| "Clk"           { CLK }
+| "Stable"        { STABLE }
+| "Data"          { DATA }
+| "Control"       { CAPS_CONTROL }
+| "Share"         { SHARE }
+| "StateShare"    { STATE_SHARE }
+| "Generated"     { GENERATED }
+| "NewFSM"        { NEW_FSM }
+| "Inline"        { INLINE }
+| "Input"         { INPUT }
+| "Output"        { OUTPUT }
+| "Inout"         { INOUT }
+| "width"         { WIDTH }
+| "holes"         { HOLES }
+| "parent"        { PARENT }
+| "direction"     { DIRECTION }
+| "assignments"   { ASSIGNMENTS }
+| "latency"       { LATENCY }
+| "Empty"         { EMPTY }
+| "Seq"           { SEQ }
+| "Par"           { PAR }
+| "If"            { IF }
+| "While"         { WHILE }
+| "Enable"        { ENABLE }
+| "Invoke"        { INVOKE }
+| "comp"          { COMP }
+| "inputs"        { INPUTS }
+| "outputs"       { OUTPUTS }
+| "comb_group"    { COMB_GROUP }
+| "ref_cells"     { REF_CELLS }
+| "stmts"         { STMTS }
+| "Primitive"     { PRIMITIVE }
+| "val"           { VAL }
+| "width"         { WIDTH }
+| "param_binding" { PARAM_BINDING }
+| "Constant"      { CONSTANT }
+| "Port"          { PORT }
+| "port"          { PORT }
+| "And"           { AND }
+| "cond"          { COND }
+| "tbranch"       { TBRANCH }
+| "fbranch"       { FBRANCH }
+| "body"          { BODY }
+| "Not"           { NOT }
+| id as x         { ID x }
+| _ { raise (SyntaxError (Printf.sprintf "At offset %d: unexpected character %s" (Lexing.lexeme_start lexbuf) (Lexing.lexeme lexbuf))) }
\ No newline at end of file
diff --git a/vcalyx/ocaml/parser.mly b/vcalyx/ocaml/parser.mly
new file mode 100644
index 0000000000..ea73e6df5e
--- /dev/null
+++ b/vcalyx/ocaml/parser.mly
@@ -0,0 +1,287 @@
+%{
+  open Core
+  open Extr
+%}
+
+%token <int> INT 
+%token <string> ID
+%token <string> STRING
+%token DOT
+(* numerical attributes *)
+%token NUM GO DONE STATIC WRITE_TOGETHER READ_TOGETHER
+(* boolean attributes *)
+%token BOOL TOP_LEVEL EXTERNAL NO_INTERFACE RESET CLK STABLE DATA
+(* more boolean attributes *)
+%token CAPS_CONTROL SHARE STATE_SHARE GENERATED NEW_FSM INLINE
+%token COMPONENTS ENTRYPOINT
+%token NAME SIGNATURE CELLS GROUPS STATIC_GROUPS COMB_GROUPS CONT_ASSNS CONTROL IS_COMB ATTRIBUTES
+%token TRUE FALSE DST SRC GUARD PORTS PROTOTYPE THIS_COMPONENT REFERENCE
+%token LPAREN RPAREN EOF
+%token INPUT OUTPUT INOUT
+%token WIDTH
+%token HOLES
+%token PARENT
+%token DIRECTION
+%token ASSIGNMENTS
+%token LATENCY
+%token PRIMITIVE
+%token VAL
+%token PARAM_BINDING
+%token CONSTANT
+(* Guard expressions. *)
+%token PORT AND
+(* Control statements. *)
+%token SEQ PAR INVOKE ENABLE EMPTY STMTS GROUP
+%token IF COND TBRANCH FBRANCH
+%token WHILE BODY
+%token COMP INPUTS OUTPUTS COMB_GROUP REF_CELLS
+%token COMPONENT
+%token NOT
+
+%start <Extr.context> main
+%%
+
+main: 
+  | LPAREN;
+      LPAREN; COMPONENTS; comps = list(paren_component); RPAREN; 
+      LPAREN; ENTRYPOINT; DOT; entry = STRING; RPAREN;
+    RPAREN; EOF
+  { {ctx_comps = comps; ctx_entrypoint = entry} }
+
+attrs_clause:
+  | LPAREN; ATTRIBUTES; attrs = list(attribute); RPAREN
+   { attrs }
+
+paren_component:
+  | LPAREN; component = component; RPAREN { component }
+
+component: 
+  | LPAREN; NAME; DOT; name = STRING; RPAREN; 
+    LPAREN; SIGNATURE; signature = cell; RPAREN; 
+    LPAREN; CELLS; cells = list(paren_cell); RPAREN;
+    LPAREN; GROUPS; groups = list(paren_group); RPAREN; 
+    LPAREN; STATIC_GROUPS; sgroups = list(sgroup); RPAREN; 
+    LPAREN; COMB_GROUPS; cgroups = list(paren_cgroup); RPAREN; 
+    LPAREN; CONT_ASSNS; assns = list(assignment); RPAREN; 
+    LPAREN; CONTROL; ctl = control; RPAREN; 
+    attributes = attrs_clause;
+    LPAREN; IS_COMB; DOT; is_comb = bool; RPAREN;
+    LPAREN; LATENCY; RPAREN
+{ {comp_attrs = attributes; comp_name = name; comp_sig = signature;
+comp_cells = cells; comp_groups = groups; comp_comb_groups = cgroups;
+comp_static_groups = sgroups; comp_cont_assns = assns; comp_control = ctl;
+comp_is_comb = is_comb} }
+
+paren_cgroup:
+| LPAREN; cgroup = cgroup; RPAREN { cgroup }
+
+cgroup:
+  | LPAREN; NAME; DOT; comb_group_name = STRING; RPAREN;
+    LPAREN; ASSIGNMENTS; comb_group_assns = list(assignment); RPAREN;
+    comb_group_attrs = attrs_clause;
+    { { comb_group_name;
+        comb_group_attrs;
+        comb_group_assns } }
+
+paren_cell:
+  | LPAREN; cell = cell; RPAREN { cell }
+
+cell:
+  | LPAREN; NAME; DOT; name = STRING; RPAREN; 
+    LPAREN; PORTS; ports = list(paren_port); RPAREN;
+    LPAREN; PROTOTYPE; proto = prototype; RPAREN; 
+    attributes = attrs_clause;
+    LPAREN; REFERENCE; DOT; reference = bool; RPAREN;
+{ let ins = List.filter ports ~f:(fun p -> is_in p.port_dir) in
+  let outs = List.filter ports ~f:(fun p -> is_out p.port_dir) in
+  {cell_name = name;
+   cell_attrs = attributes;
+   cell_in_ports = ins;
+   cell_out_ports = outs;
+   cell_proto = proto;
+   cell_ref = reference} }
+
+paren_port:
+| LPAREN; port = port; RPAREN { port }
+port: 
+| LPAREN; NAME; DOT; name = STRING; RPAREN; 
+    LPAREN; WIDTH; DOT; width = INT; RPAREN;
+    LPAREN; DIRECTION; DOT; dir = direction; RPAREN;
+    LPAREN; PARENT; DOT; par = STRING; RPAREN; 
+    attributes = attrs_clause
+  { {port_name = name; port_width = width; port_dir = dir; parent = par; 
+     port_attribute = attributes} }
+
+port_ref: 
+| LPAREN; NAME; DOT; name = STRING; RPAREN; 
+  LPAREN; WIDTH; DOT; width = INT; RPAREN;
+  LPAREN; DIRECTION; DOT; dir = direction; RPAREN;
+  LPAREN; PARENT; DOT; par = STRING; RPAREN; 
+  attributes = attrs_clause;
+    { let _ = attributes in
+      let _ = width in
+      let _ = dir in
+      if String.equal par "_this"
+      then PThis name
+      else PRef (par, name) }
+
+direction: 
+| INPUT { Input }
+| OUTPUT { Output }
+| INOUT { InOut }
+
+paren_group:
+  | LPAREN; group = group; RPAREN { group }
+
+group:
+  | LPAREN; NAME; DOT; group_name = STRING; RPAREN;
+    LPAREN; ASSIGNMENTS; group_assns = list(assignment); RPAREN;
+    LPAREN; HOLES; group_holes = list(paren_port); RPAREN;
+    group_attrs = attrs_clause
+    { { group_attrs;
+        group_name;
+        group_assns;
+        group_holes; } }
+
+paren_guard:
+| LPAREN; guard = guard; RPAREN { guard }
+
+guard:
+| DOT; TRUE
+| TRUE
+  { GTrue }
+| PORT; p = port
+  { GPort p }
+| AND; g1 = paren_guard; g2 = paren_guard
+  { GAnd (g1, g2) }
+| NOT; g = guard
+  { GNot g }
+
+assignment: 
+  | LPAREN;
+      LPAREN; DST; dst = port_ref; RPAREN;
+      LPAREN; SRC; src = port_ref; RPAREN; 
+      LPAREN; GUARD; assign_guard = guard; RPAREN; 
+      attrs = attrs_clause;
+    RPAREN
+    { { dst; src; assign_guard; attrs } }
+
+paren_control:
+  | LPAREN; control = control; RPAREN { control }
+
+port_binding:
+  | LPAREN; name = STRING; LPAREN; port = port_ref RPAREN; RPAREN
+    { (name, port) }
+
+control: 
+  | EMPTY; attrs = attrs_clause
+    { CEmpty attrs }
+  | SEQ; LPAREN; STMTS; stmts = list(paren_control); RPAREN; attrs = attrs_clause;
+    { CSeq (stmts, attrs) }
+  | PAR; LPAREN; STMTS; stmts = list(paren_control); RPAREN; attrs = attrs_clause;
+    { CPar (stmts, attrs) }
+  | ENABLE; LPAREN; GROUP; grp = group; RPAREN; attrs = attrs_clause
+    { CEnable (grp.group_name, attrs) }
+  | INVOKE; LPAREN; COMP; comp = cell; RPAREN;
+            LPAREN; INPUTS; inputs = list(port_binding); RPAREN;
+            LPAREN; OUTPUTS; outputs = list(port_binding); RPAREN;
+            attrs = attrs_clause;
+            LPAREN; COMB_GROUP; comb_group = option(paren_cgroup); RPAREN
+            LPAREN; REF_CELLS; RPAREN
+    {
+      let cg_name =
+        match comb_group with
+        | Some comb_group -> Some comb_group.comb_group_name
+        | None -> None in
+      CInvoke (comp.cell_name, inputs, outputs, attrs, cg_name, []) }
+  | IF; LPAREN; PORT; cond_port = port_ref; RPAREN;
+        LPAREN; COND; RPAREN;
+        LPAREN; TBRANCH; tru = control; RPAREN;
+        LPAREN; FBRANCH; fls = control; RPAREN;
+        attrs = attrs_clause
+    { CIf (cond_port, None, tru, fls, attrs) }
+  | IF; LPAREN; PORT; cond_port = port_ref; RPAREN;
+        LPAREN; COND; cgroup = paren_cgroup RPAREN;
+        LPAREN; TBRANCH; tru = control; RPAREN;
+        LPAREN; FBRANCH; fls = control; RPAREN;
+        attrs = attrs_clause
+    { CIf (cond_port, Some cgroup.comb_group_name, tru, fls, attrs) }
+  | WHILE; LPAREN; PORT; cond_port = port_ref; RPAREN;
+        LPAREN; COND; RPAREN;
+        LPAREN; BODY; body = control; RPAREN;
+        attrs = attrs_clause
+    { CWhile (cond_port, None, body, attrs) }
+  | WHILE; LPAREN; PORT; cond_port = port_ref; RPAREN;
+        LPAREN; COND; cgroup = paren_cgroup RPAREN;
+        LPAREN; BODY; body = control; RPAREN;
+        attrs = attrs_clause
+    { CWhile (cond_port, Some cgroup.comb_group_name, body, attrs) }
+
+
+num_attr_name:
+| GO { Go }
+| DONE { Done }
+| STATIC { Static }
+| WRITE_TOGETHER { WriteTogether }
+| READ_TOGETHER { ReadTogether }
+
+
+bool_attr_name:
+| TOP_LEVEL { TopLevel }
+| EXTERNAL { External }
+| NO_INTERFACE { NoInterface }
+| RESET { Reset }
+| CLK { Clk }
+| STABLE { Stable }
+| DATA { Data }
+| CAPS_CONTROL { Control }
+| SHARE { Share }
+| STATE_SHARE { StateShare }
+| GENERATED { Generated }
+| NEW_FSM { NewFSM }
+| INLINE { Inline }
+
+attribute:
+| LPAREN; LPAREN; NUM; DOT; name = num_attr_name; RPAREN; DOT; value = INT; RPAREN
+   { NumAttr (name, value) }
+| LPAREN; LPAREN; BOOL; DOT; name = bool_attr_name; RPAREN; DOT; value = INT; RPAREN
+   { BoolAttr (name, value <> 0) }
+
+bool: 
+| TRUE { true }
+| FALSE { false }
+
+param_binding:
+| LPAREN; name = STRING; value = INT; RPAREN
+  { (name, value) }
+
+prototype:
+  (* TODO other cases *)
+  | DOT; THIS_COMPONENT
+  | THIS_COMPONENT
+    { ProtoThis }
+  | PRIMITIVE;
+    LPAREN; NAME; DOT; name = STRING; RPAREN; 
+    LPAREN; PARAM_BINDING; param_binding = list(param_binding); RPAREN; 
+    LPAREN; IS_COMB; DOT; is_comb = bool; RPAREN;
+    LPAREN; LATENCY; RPAREN;
+    { ProtoPrim (name, param_binding, is_comb) }
+  | CONSTANT;
+      LPAREN; VAL; DOT; value = INT; RPAREN;
+      LPAREN; WIDTH; DOT; width = INT; RPAREN;
+    { ProtoConst (value, width) }
+  | COMPONENT; LPAREN; NAME; DOT; name = STRING; RPAREN; 
+    { ProtoComp name }
+
+sgroup:
+  | LPAREN;
+      LPAREN; NAME; static_group_name = ID; RPAREN;
+      LPAREN; ASSIGNMENTS; static_group_assns = list(assignment); RPAREN;
+      LPAREN; HOLES; static_group_holes = list(paren_port); RPAREN;
+      static_group_attrs = attrs_clause;
+    RPAREN
+    { { static_group_attrs;
+        static_group_name;
+        static_group_assns;
+        static_group_holes;
+        static_latency = failwith "couldn't parse latency of a static group" } }
diff --git a/vcalyx/ocaml/test.ml b/vcalyx/ocaml/test.ml
new file mode 100644
index 0000000000..f0602555bc
--- /dev/null
+++ b/vcalyx/ocaml/test.ml
@@ -0,0 +1 @@
+(*let test = ()*)
diff --git a/vcalyx/ocaml/utils.ml b/vcalyx/ocaml/utils.ml
new file mode 100644
index 0000000000..c0d2e14787
--- /dev/null
+++ b/vcalyx/ocaml/utils.ml
@@ -0,0 +1,22 @@
+open Core
+open Lexing
+
+let print_position outx lexbuf =
+  let pos = lexbuf.lex_curr_p in
+  fprintf outx "%s:%d:%d" pos.pos_fname
+    pos.pos_lnum (pos.pos_cnum - pos.pos_bol + 1)
+
+let parse_with_error lexbuf =
+  try Parser.main Lexer.tokens lexbuf with
+  | _ -> 
+    fprintf stderr "%a: %s\n" print_position lexbuf "nooo";
+    Some 5
+  (* | Parser.Error ->
+    fprintf stderr "%a: syntax error\n" print_position lexbuf;
+    exit (-1) *)
+let rec parse_and_print lexbuf =
+  match parse_with_error lexbuf with
+  | Some value ->
+    printf "%d\n" value;
+    parse_and_print lexbuf
+  | None -> ()
diff --git a/vcalyx/ocaml/vcx.ml b/vcalyx/ocaml/vcx.ml
new file mode 100644
index 0000000000..ba8f4fb9c3
--- /dev/null
+++ b/vcalyx/ocaml/vcx.ml
@@ -0,0 +1,94 @@
+open Core
+open Vcalyx
+open Lexing
+
+let load_mem obj : Extr.state =
+  let open Yojson.Safe.Util in
+  let mem_data = obj
+                 |> member "data" 
+                 |> to_list
+                 |> List.map ~f:to_int in
+  Extr.StateMemD1 (Bot,
+                   {is_signed = false;
+                    numeric_type = Bitnum;
+                    width = 32},
+                   mem_data)
+
+let load_mems file =
+  let obj = Yojson.Safe.from_file file in
+  match obj with
+  | `Assoc kvs ->
+    List.map ~f:(fun (k, v) -> (k, load_mem v)) kvs
+  | _ -> failwith "unexpected JSON object"
+
+let dump_mem =
+  function
+  | Extr.StateMemD1 (_, _, mem_data) ->
+    `List (List.map ~f:(fun i -> `Int i) mem_data)
+  | _ -> failwith "unexpected @external state to dump"
+
+let dump_mems chan mems =
+  let kvs = List.map ~f:(fun (k, v) -> (k, dump_mem v)) mems in
+  Yojson.Safe.to_channel chan (`Assoc kvs)
+
+(* from https://dev.realworldocaml.org/parsing-with-ocamllex-and-menhir.html *)
+let print_position outx lexbuf =
+  let pos = lexbuf.lex_curr_p in
+  fprintf outx "%s:%d:%d" pos.pos_fname pos.pos_lnum
+    (pos.pos_cnum - pos.pos_bol + 1)
+
+let parse_with_error lexbuf =
+  try Some (Parser.main Lexer.tokens lexbuf) with
+  (* | SyntaxError msg ->
+    fprintf stderr "%a: %s\n" print_position lexbuf msg;
+    None *)
+  | Parser.Error ->
+    fprintf stderr "%a: syntax error\n" print_position lexbuf;
+    None
+
+let parse_context lexbuf source_location : Extr.context =
+  match parse_with_error lexbuf with
+  | Some ctx -> ctx
+  | None -> failwith (Printf.sprintf "Error parsing %s." source_location)
+
+let interp_exn ctx mems_initial =
+  match Extr.interp_with_mems ctx mems_initial 100000 with
+  | Inl mems_final -> mems_final
+  | Inr msg -> failwith msg
+
+let vcx_interp : Command.t =
+  let open Command.Let_syntax in
+  Command.basic ~summary:"interpret a Calyx program with Coq semantics"
+    [%map_open
+      let source_arg = anon (maybe ("prog.futils" %: string))
+      and data_arg = flag ~aliases:["-d"] "--data" (optional string)
+          ~doc:"file.json JSON data for memories, etc"
+      and _ = flag ~aliases:["-l"] "--lib" (optional string)
+          ~doc:"dir Path to primitives library"
+      in fun () ->
+        let mems_initial =
+          match data_arg with
+          | Some data_arg -> load_mems data_arg
+          | None -> []
+        in
+        let source_name = 
+          match source_arg with
+          | Some source_location -> source_location
+          | None -> "<stdin>" in
+        let source_chan =
+          match source_arg with
+          | Some source_location -> In_channel.create source_location
+          | None -> In_channel.stdin in
+        let source_lexbuf = Lexing.from_channel source_chan in
+        Lexing.set_filename source_lexbuf source_name;
+        let ctx = parse_context source_lexbuf source_name in
+        In_channel.close source_chan;
+        (* need to print out the result appropriately and include # of cycles... *)
+        let mems_final = interp_exn ctx mems_initial in
+        dump_mems Out_channel.stdout mems_final]
+
+let vcx_cmd : Command.t =
+  Command.group ~summary:"vcx: the vcalyx command-line interface"
+    [ ("interp", vcx_interp) ]
+
+let () = Command_unix.run ~version:"dev" vcx_cmd
diff --git a/vcalyx/runt.toml b/vcalyx/runt.toml
new file mode 100644
index 0000000000..3affd6ef70
--- /dev/null
+++ b/vcalyx/runt.toml
@@ -0,0 +1,205 @@
+ver = "0.4.1"
+
+# Check basic functionality of the interpreter
+[[tests]]
+  name = "vcalyx examples"
+  paths = ["./examples/*.futil"]
+  cmd = """
+  fud exec --to jq \
+           --through vcalyx-out \
+           -s verilog.data {}.data \
+           -s calyx.exec '../target/debug/calyx' \
+           {} -q
+  """
+  timeout = 3
+
+# [[tests]]
+#   name = "correctness dynamic"
+#   paths = ["../tests/correctness/*.futil"]
+#   cmd = """
+#   fud exec --to jq \
+#            --through vcalyx-out \
+#            -s verilog.data {}.data \
+#            {} -q
+#   """
+#   timeout = 3
+# 
+
+# [[tests]]
+#  name = "unit"
+#  paths = ["../interp/tests/unit/*.futil"]
+#  cmd = """
+#    ./_build/default/ocaml/vcx.exe parse {}
+#  """
+#  timeout = 3
+
+# # [[tests]]
+# name = "errors"
+# paths = ["../interp/tests/errors/*.futil"]
+
+# cmd = """
+# ./_build/default/ocaml/vcx.exe parse {}
+# """
+# timeout = 3
+
+# [[tests]]
+# name = "complex"
+# paths = ["../interp/tests/complex/*.futil"]
+
+# cmd = """
+# ./_build/default/ocaml/vcx.exe parse {}
+# """
+# timeout = 3
+
+# [[tests]]
+# name = "primitives"
+# paths = ["../interp/tests/primitives/*.futil"]
+# cmd = """
+# ./_build/default/ocaml/vcx.exe parse {}
+# """
+# timeout = 3
+
+# [[tests]]
+# name = "par to seq"
+# paths = ["../interp/tests/control/par_reg.futil", "../interp/tests/control/par_mem.futil"]
+# cmd = """
+# ../target/debug/futil {} -p par-to-seq -l ../ | ./_build/default/ocaml/vcx.exe parse {}
+# """
+# timeout = 3
+
+# [[tests]]
+# name = "control"
+# paths = [
+#   "../interp/tests/control/*.futil",
+#   "../interp/tests/control/iteration/*.futil",
+#   "../interp/tests/control/static/*.futil",
+# ]
+# cmd = """
+# ./_build/default/ocaml/vcx.exe parse {}
+# """
+# timeout = 3
+
+# # TODO support data files
+# [[tests]]
+# name = "invoke"
+# paths = ["../interp/tests/control/invoke/*.futil"]
+# cmd = """
+# fud e {} --to vcx -s interpreter.flags " -q" -s verilog.data {}.data -q | jq .memories
+# """
+
+# [[tests]]
+# name = "invoke comp"
+# paths = ["../interp/tests/control/invoke/*.futil"]
+# cmd = """
+# fud e {} --to interpreter-out -s futil.flags "-p compile-invoke" -s interpreter.flags " -q" -s verilog.data {}.data -q | jq .memories
+# """
+
+# [[tests]]
+# name = "fully structural"
+# paths = [
+#   "../interp/tests/control/*.futil",
+#   # Disabled iteration tests due to bug
+#   #    "../interp/tests/control/iteration/*.futil"
+# ]
+# cmd = """
+# ../target/debug/futil {} -d pre-opt -d post-opt -p remove-comb-groups -l ../ | ./_build/default/ocaml/vcx.exe parse
+# """
+# expect_dir = "../interp/tests/lowered/"
+# timeout = 3
+
+# [[tests]]
+# name = "fully structural static"
+# paths = ["../interp/tests/control/static*.futil"]
+# cmd = """
+# ../target/debug/futil {} -d pre-opt -d post-opt  -l ../ | ./_build/default/ocaml/vcx.exe parse
+# """
+# expect_dir = "../interp/tests/lowered/"
+# timeout = 3
+
+# [[tests]]
+# name = "correctness dynamic"
+# paths = ["../tests/correctness/*.futil"]
+# cmd = """
+# fud exec --to jq \
+#          --through interpreter-out \
+#          -s verilog.data {}.data \
+#          -s interpreter.flags " --raw" \
+#          -s jq.expr ".main" \
+#          {} -q
+# """
+
+# [[tests]]
+# name = "numeric types correctness and parsing"
+# paths = [
+#   "../tests/correctness/numeric-types/parsing/*.futil",
+#   "../tests/correctness/numeric-types/bitnum/*.futil",
+#   "../tests/correctness/numeric-types/fixed-point/*.futil",
+# ]
+# cmd = """
+# fud exec --to jq \
+#          --through interpreter-out \
+#          -s interpreter.flags "--raw " \
+#          -s verilog.data {}.data \
+#          -s jq.expr ".main" \
+#          {} -q
+# """
+
+# [[tests]]
+# name = "[frontend] tcam testing"
+# paths = ["../tests/correctness/tcam/*.futil"]
+# cmd = """
+# fud exec --to jq \
+#       --through interpreter-out \
+#       -s interpreter.flags "--raw " \
+#       -s verilog.data {}.data \
+#       -s jq.expr ".main" \
+#       {} -q
+# """
+
+# [[tests]]
+# name = "[frontend] systolic array correctness"
+# paths = ["../tests/correctness/systolic/*.systolic"]
+# cmd = """
+# fud e --from systolic --to jq \
+#       --through interpreter-out \
+#       -s interpreter.flags "--raw " \
+#       -s verilog.data {}.data \
+#       -s jq.expr ".main" \
+#       {} -q
+# """
+
+# [[tests]]
+# name = "[frontend] NTT pipeline correctness"
+# paths = ["../tests/correctness/ntt-pipeline/*.txt"]
+# cmd = """
+# fud e --from ntt --to jq \
+#       --through interpreter-out \
+#       -s interpreter.flags "--raw " \
+#       -s verilog.data {}.data \
+#       -s jq.expr ".main" \
+#       {} -q
+# """
+# expect_dir = "../interp/tests/ntt-results/"
+
+
+# [[tests]]
+# name = "[frontend] mrxl correctness"
+# paths = ["../frontends/mrxl/test/*.mrxl"]
+# cmd = """
+# fud e -q {} --from mrxl --to jq \
+#             --through interpreter-out \
+#             -s interpreter.flags "--raw " \
+#             -s verilog.data {}.data \
+#             -s jq.expr ".main"
+# """
+
+# [[tests]]
+# name = "[frontend] relay correctness"
+# paths = ["../tests/correctness/relay/*.relay"]
+# cmd = """
+# fud e -q {} --from relay --to jq \
+#             --through interpreter-out \
+#             -s interpreter.flags "--raw " \
+#             -s verilog.data {}.data \
+#             -s jq.expr ".main"
+# """
diff --git a/vcalyx/vcalyx.opam b/vcalyx/vcalyx.opam
new file mode 100644
index 0000000000..c8319de36e
--- /dev/null
+++ b/vcalyx/vcalyx.opam
@@ -0,0 +1,36 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+version: "dev"
+synopsis: "Coq formalization of the Calyx language"
+maintainer: ["Ryan Doenges and Priya Srikumar"]
+authors: ["Ryan Doenges and Priya Srikumar"]
+license: "MIT"
+homepage: "https://github.com/cucapra/calyx/tree/vcalyx"
+bug-reports: "https://github.com/cucapra/calyx/tree/vcalyx"
+depends: [
+  "dune" {>= "3.8"}
+  "core" {>= "0.15.0"}
+  "ppx_let" {>= "0.15.0"}
+  "stdlib-shims" {>= "0.3.0"}
+  "coq-ceres" {>= "0.4.0"}
+  "coq-stdpp" {>= "1.8.0"}
+  "coq" {>= "8.15.2"}
+  "menhir" {>= "20230608"}
+  "yojson" {>= "2.1.0"}
+  "ocamlformat" {build & >= "0.24.1"}
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]