diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json
index 819513e07d..c5f50c6789 100644
--- a/.devcontainer/devcontainer.json
+++ b/.devcontainer/devcontainer.json
@@ -31,7 +31,8 @@
         "zhwu95.riscv",
         "mathematic.vscode-pdf",
         "CraigMaslowski.erb",
-        "HowerLimited.udb-extension-pack-vscode"
+        "HowerLimited.udb-extension-pack-vscode",
+        "sorbet.sorbet-vscode-extension"
       ]
     }
   },
diff --git a/.gitignore b/.gitignore
index e0ca947a49..543d159dd6 100644
--- a/.gitignore
+++ b/.gitignore
@@ -21,3 +21,4 @@ __pycache__/
 .pytest_cache/
 *.bak
 *.log
+sorbet
diff --git a/.gitmodules b/.gitmodules
index 2265f46f88..8b4533e0e0 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -14,3 +14,6 @@
 [submodule "ext/riscv-tests"]
 	path = ext/riscv-tests
 	url = https://github.com/riscv-software-src/riscv-tests.git
+[submodule "ext/rbi-central"]
+	path = ext/rbi-central
+	url = https://github.com/Shopify/rbi-central
diff --git a/.pre-commit-config.yaml b/.pre-commit-config.yaml
index 0a3b6467e8..9920b68d4e 100755
--- a/.pre-commit-config.yaml
+++ b/.pre-commit-config.yaml
@@ -119,7 +119,7 @@ repos:
     rev: v5.0.2
     hooks:
       - id: reuse-lint-file
-        exclude: COMMIT_EDITMSG
+        exclude: COMMIT_EDITMSG|MERGE_MSG
 
   - repo: https://github.com/alessandrojcm/commitlint-pre-commit-hook
     rev: v9.22.0
diff --git a/.sorbet-config b/.sorbet-config
new file mode 100644
index 0000000000..99082b0e19
--- /dev/null
+++ b/.sorbet-config
@@ -0,0 +1,10 @@
+--dir
+lib
+--dir
+sorbet/rbi
+--file
+Rakefile
+--file
+backends/ext_pdf_doc/idl_lexer.rb
+--file
+backends/cpp_hart_gen/lib/template_helpers.rb
diff --git a/.tapioca-config.yml b/.tapioca-config.yml
new file mode 100644
index 0000000000..0ffc27ea6a
--- /dev/null
+++ b/.tapioca-config.yml
@@ -0,0 +1,27 @@
+gem:
+  outdir: .home/.sorbet/rbi/gems
+  file_header: true
+  exclude:
+    [
+      rdoc,
+      asciidoctor-pdf,
+      solargraph,
+      webrick,
+      ttfunk,
+      tapioca,
+      rubocop,
+      rubocop-minitest,
+      spoom,
+      rdbg,
+      parser,
+    ]
+dsl:
+  outdir: .home/.sorbet/rbi/dsl
+  # Add your `dsl` command parameters here:
+  #
+  # exclude:
+  # - SomeGeneratorName
+  # workers: 5
+annotations:
+  sources:
+    - ext/rbi-central
diff --git a/Gemfile b/Gemfile
index 2f064d3170..38f8457460 100644
--- a/Gemfile
+++ b/Gemfile
@@ -16,6 +16,7 @@ gem "pygments.rb"
 gem "rake", "~> 13.0"
 gem "rouge"
 gem "ruby-progressbar", "~> 1.13"
+gem "sorbet-runtime"
 gem "treetop", "1.6.12"
 gem "ttfunk", "1.7" # needed to avoid having asciidoctor-pdf dependencies pulling in a buggy version of ttunk (1.8)
 gem "webrick"
@@ -31,4 +32,7 @@ group :development do
   gem "ruby-prof"
   gem "ruby-prof-flamegraph", git: "https://github.com/oozou/ruby-prof-flamegraph.git", ref: "fc3c437", require: false
   gem "solargraph"
+  gem "sorbet"
+  gem "spoom"
+  gem "tapioca", require: false
 end
diff --git a/Gemfile.lock b/Gemfile.lock
index a53fe95832..89fd36b8f2 100644
--- a/Gemfile.lock
+++ b/Gemfile.lock
@@ -65,6 +65,7 @@ GEM
       reline (>= 0.3.8)
     diff-lcs (1.6.0)
     drb (2.2.1)
+    erubi (1.13.1)
     hana (1.3.7)
     hashery (2.1.2)
     i18n (1.14.7)
@@ -89,6 +90,7 @@ GEM
     logger (1.6.6)
     matrix (0.4.2)
     minitest (5.25.5)
+    netrc (0.11.0)
     nkf (0.2.0)
     nokogiri (1.18.6-aarch64-linux-gnu)
       racc (~> 1.4)
@@ -126,6 +128,7 @@ GEM
       pdf-reader (~> 2.0)
       prawn (~> 2.2)
     prettyprint (0.2.0)
+    prism (1.4.0)
     psych (5.2.3)
       date
       stringio
@@ -134,6 +137,10 @@ GEM
     racc (1.8.1)
     rainbow (3.1.1)
     rake (13.2.1)
+    rbi (0.3.1)
+      prism (~> 1.0)
+      rbs (>= 3.4.4)
+      sorbet-runtime (>= 0.5.9204)
     rbs (3.9.1)
       logger
     rdbg (0.1.0)
@@ -189,7 +196,31 @@ GEM
       tilt (~> 2.0)
       yard (~> 0.9, >= 0.9.24)
       yard-solargraph (~> 0.1)
+    sorbet (0.5.11966)
+      sorbet-static (= 0.5.11966)
+    sorbet-runtime (0.5.11966)
+    sorbet-static (0.5.11966-aarch64-linux)
+    sorbet-static (0.5.11966-x86_64-linux)
+    sorbet-static-and-runtime (0.5.11966)
+      sorbet (= 0.5.11966)
+      sorbet-runtime (= 0.5.11966)
+    spoom (1.6.1)
+      erubi (>= 1.10.0)
+      prism (>= 0.28.0)
+      rbi (>= 0.2.3)
+      sorbet-static-and-runtime (>= 0.5.10187)
+      thor (>= 0.19.2)
     stringio (3.1.5)
+    tapioca (0.16.11)
+      benchmark
+      bundler (>= 2.2.25)
+      netrc (>= 0.11.0)
+      parallel (>= 1.21.0)
+      rbi (~> 0.2)
+      sorbet-static-and-runtime (>= 0.5.11087)
+      spoom (>= 1.2.0)
+      thor (>= 1.2.0)
+      yard-sorbet
     thor (1.3.2)
     tilt (2.6.0)
     treetop (1.6.12)
@@ -208,6 +239,9 @@ GEM
     yard (0.9.37)
     yard-solargraph (0.1.0)
       yard (~> 0.9)
+    yard-sorbet (0.9.0)
+      sorbet-runtime
+      yard
 
 PLATFORMS
   aarch64-linux-gnu
@@ -234,6 +268,10 @@ DEPENDENCIES
   ruby-prof-flamegraph!
   ruby-progressbar (~> 1.13)
   solargraph
+  sorbet
+  sorbet-runtime
+  spoom
+  tapioca
   treetop (= 1.6.12)
   ttfunk (= 1.7)
   webrick
diff --git a/Rakefile b/Rakefile
index 1e16b20f3b..7d27e9ca8c 100755
--- a/Rakefile
+++ b/Rakefile
@@ -1,4 +1,9 @@
 # frozen_string_literal: true
+# typed: true
+
+require "sorbet-runtime"
+T.bind(self, T.all(Rake::DSL, Object))
+extend T::Sig
 
 Encoding.default_external = "UTF-8"
 
@@ -37,8 +42,8 @@ directory "#{$root}/.stamps"
 
 # @param config_locator [String or Pathname]
 # @return [ConfiguredArchitecture]
+sig { params(config_locator: T.any(String, Pathname)).returns(ConfiguredArchitecture) }
 def cfg_arch_for(config_locator)
-  raise ArgumentError, "expecting String or Pathname" unless config_locator.is_a?(String) || config_locator.is_a?(Pathname)
   config_locator = config_locator.to_s
 
   $cfg_archs ||= {}
@@ -163,6 +168,11 @@ namespace :serve do
   end
 end
 
+sig { params(test_files: T::Array[String]).returns(String) }
+def make_test_cmd(test_files)
+  "-Ilib:test -w -e 'require \"minitest/autorun\"; #{test_files.map{ |f| "require \"#{f}\""}.join("; ")}' --"
+end
+
 namespace :test do
 
   # "Run the cross-validation against LLVM"
@@ -175,18 +185,20 @@ namespace :test do
   end
   # "Run the IDL compiler test suite"
   task :idl_compiler do
-    t = Minitest::TestTask.new(:lib_test)
-    t.test_globs = ["#{$root}/lib/idl/tests/test_*.rb"]
-    t.process_env
-    ruby t.make_test_cmd
+    test_files = Dir["#{$root}/lib/idl/tests/test_*.rb"]
+    ruby make_test_cmd(test_files)
   end
 
   # "Run the Ruby library test suite"
   task :lib do
-    t = Minitest::TestTask.new(:lib_test)
-    t.test_globs = ["#{$root}/lib/test/test_*.rb"]
-    t.process_env
-    ruby t.make_test_cmd
+    test_files = Dir["#{$root}/lib/test/test_*.rb"]
+
+    ruby make_test_cmd(test_files)
+  end
+
+  desc "Type-check the Ruby library"
+  task :sorbet do
+    sh "srb tc @.sorbet-config"
   end
 end
 
@@ -208,13 +220,13 @@ namespace :test do
 
     cfg_arch = cfg_arch_for("_")
     insts = cfg_arch.instructions
-    failed = false
+    failed = T.let(false, T::Boolean)
     insts.each_with_index do |inst, idx|
       [32, 64].each do |xlen|
         next unless inst.defined_in_base?(xlen)
 
         (idx...insts.size).each do |other_idx|
-          other_inst = insts[other_idx]
+          other_inst = T.must(insts[other_idx])
           next unless other_inst.defined_in_base?(xlen)
           next if other_inst == inst
 
@@ -236,13 +248,13 @@ namespace :test do
 
     cfg_arch = cfg_arch_for("_")
     csrs = cfg_arch.csrs
-    failed = false
+    failed = T.let(false, T::Boolean)
     csrs.each_with_index do |csr, idx|
       [32, 64].each do |xlen|
         next unless csr.defined_in_base?(xlen)
 
         (idx...csrs.size).each do |other_idx|
-          other_csr = csrs[other_idx]
+          other_csr = T.must(csrs[other_idx])
           next unless other_csr.defined_in_base?(xlen)
           next if other_csr == csr
 
@@ -284,7 +296,6 @@ def insert_warning(str, from)
   first_line = lines.shift
   lines.unshift(first_line, "\n# WARNING: This file is auto-generated from #{Pathname.new(from).relative_path_from($root)}").join("")
 end
-private :insert_warning
 
 (3..31).each do |hpm_num|
   file "#{$root}/arch/csr/Zihpm/mhpmcounter#{hpm_num}.yaml" => [
@@ -437,6 +448,8 @@ namespace :test do
     Rake::Task["test:idl_compiler"].invoke
     $logger.info "Running test:lib"
     Rake::Task["test:lib"].invoke
+    $logger.info "UPDATE: Running test:sorbet"
+    Rake::Task["test:sorbet"].invoke
     $logger.info "Running test:schema"
     Rake::Task["test:schema"].invoke
     $logger.info "UPDATE: Running test:idl for rv32"
diff --git a/backends/cpp_hart_gen/templates/csrs_impl.hxx.erb b/backends/cpp_hart_gen/templates/csrs_impl.hxx.erb
index 1a222b2580..5362814fa3 100644
--- a/backends/cpp_hart_gen/templates/csrs_impl.hxx.erb
+++ b/backends/cpp_hart_gen/templates/csrs_impl.hxx.erb
@@ -56,11 +56,7 @@ void <%= name_of(:csr_field, cfg_arch, csr.name, field.name) %><SocType>::reset(
   <%- end -%>
   <%- else -%>
   auto val_fn = [this]() ->
-    <%- if field.could_be_undefined? -%>
     PossiblyUnknownBits<<%= max_width + 1 %>>
-    <%- else -%>
-    Bits<<%= max_width + 1 %>>
-    <%- end -%>
   {
     <%= ast.gen_cpp(cfg_arch.symtab, 8) %>
   };
diff --git a/backends/ext_pdf_doc/tasks.rake b/backends/ext_pdf_doc/tasks.rake
index 99ef981d91..7d6ea737ae 100644
--- a/backends/ext_pdf_doc/tasks.rake
+++ b/backends/ext_pdf_doc/tasks.rake
@@ -2,9 +2,6 @@
 
 require "pathname"
 
-require "asciidoctor-pdf"
-require "asciidoctor-diagram"
-
 require_relative "#{$lib}/idl/passes/gen_adoc"
 
 EXT_PDF_DOC_DIR = Pathname.new "#{$root}/backends/ext_pdf_doc"
diff --git a/backends/portfolio/tasks.rake b/backends/portfolio/tasks.rake
index 12de93e92a..474360882b 100644
--- a/backends/portfolio/tasks.rake
+++ b/backends/portfolio/tasks.rake
@@ -3,8 +3,6 @@
 # Contains common methods called from portfolio-based tasks.rake files.
 
 require "pathname"
-require "asciidoctor-pdf"
-require "asciidoctor-diagram"
 require_relative "#{$lib}/idl/passes/gen_adoc"
 
 # @return [Architecture]
diff --git a/backends/proc_cert/tasks.rake b/backends/proc_cert/tasks.rake
index baf409465e..e841e4158d 100644
--- a/backends/proc_cert/tasks.rake
+++ b/backends/proc_cert/tasks.rake
@@ -3,8 +3,6 @@
 # Contains common methods called from certification backend tasks.rake files.
 
 require "pathname"
-require "asciidoctor-pdf"
-require "asciidoctor-diagram"
 
 # @param erb_template_pname [String] Path to ERB template file
 # @param target_pname [String] Full name of adoc file being generated
diff --git a/bin/clobber b/bin/clobber
index 97f206daa2..95d31b8b1d 100755
--- a/bin/clobber
+++ b/bin/clobber
@@ -2,4 +2,11 @@
 
 ROOT=$(dirname $(dirname $(realpath ${BASH_SOURCE[0]})))
 
-rm -rf ${ROOT}/.stamps ${ROOT}/.home ${ROOT}/.bundle ${ROOT}/.singularity ${ROOT}/gen ${ROOT}/node_modules
+rm -rf                 \
+  ${ROOT}/.stamps      \
+  ${ROOT}/.home        \
+  ${ROOT}/.bundle      \
+  ${ROOT}/.singularity \
+  ${ROOT}/gen          \
+  ${ROOT}/node_modules \
+  ${ROOT}/sorbet
diff --git a/bin/setup b/bin/setup
index 683faf1883..a0f9bfd279 100755
--- a/bin/setup
+++ b/bin/setup
@@ -144,6 +144,23 @@ if [ ! -d $ROOT/.home/.gems ]; then
     cd $OLDDIR
 fi
 
+if [ ! -f $ROOT/ext/rbi-central/README.md ]; then
+    git submodule update --init ext/rbi-central
+fi
+
+if [ ! -d $ROOT/.home/.sorbet ]; then
+    mkdir .home/.sorbet
+    ln -s .home/.sorbet sorbet
+    cd .home/.sorbet
+    ln -s ../../.sorbet-config config
+    cd $ROOT
+    ${RUN} bundle exec tapioca init -c ${ROOT}/.tapioca-config.yml
+    ${RUN} bundle exec tapioca dsl -c ${ROOT}/.tapioca-config.yml
+    cd .home/.sorbet/rbi/dsl
+    ln -s ${ROOT}/lib/architecture.rbi
+    cd $ROOT
+fi
+
 if [ ! -d $ROOT/.home/.venv ]; then
     ${RUN} /usr/bin/python3 -m venv ${ROOT}/.home/.venv
 fi
diff --git a/bin/tapioca b/bin/tapioca
new file mode 100755
index 0000000000..ac3e1c0759
--- /dev/null
+++ b/bin/tapioca
@@ -0,0 +1,27 @@
+#!/usr/bin/env ruby3.2
+# frozen_string_literal: true
+
+#
+# This file was generated by Bundler.
+#
+# The application 'tapioca' is installed as part of a gem, and
+# this file is here to facilitate running it.
+#
+
+ENV["BUNDLE_GEMFILE"] ||= File.expand_path("../Gemfile", __dir__)
+
+bundle_binstub = File.expand_path("bundle", __dir__)
+
+if File.file?(bundle_binstub)
+  if File.read(bundle_binstub, 300).include?("This file was generated by Bundler")
+    load(bundle_binstub)
+  else
+    abort("Your `bin/bundle` was not generated by Bundler, so this binstub cannot run.
+Replace `bin/bundle` by running `bundle binstubs bundler --force`, then run this command again.")
+  end
+end
+
+require "rubygems"
+require "bundler/setup"
+
+load Gem.bin_path("tapioca", "tapioca")
diff --git a/ext/rbi-central b/ext/rbi-central
new file mode 160000
index 0000000000..46f1b57554
--- /dev/null
+++ b/ext/rbi-central
@@ -0,0 +1 @@
+Subproject commit 46f1b575545a73eb7a0a4997b9277d80ddcb054c
diff --git a/lib/arch_obj_models/csr.rb b/lib/arch_obj_models/csr.rb
index bd088c4ed4..45fb320136 100644
--- a/lib/arch_obj_models/csr.rb
+++ b/lib/arch_obj_models/csr.rb
@@ -1,4 +1,5 @@
 # frozen_string_literal: true
+# typed: true
 
 require_relative "database_obj"
 require_relative "certifiable_obj"
@@ -144,7 +145,7 @@ def dynamic_length?
       # VSXLEN condition applies if VS-mode is possible
       (cfg_arch.mxlen.nil?) || \
       (cfg_arch.possible_extensions.map(&:name).include?("S") && \
-      [nil, 3264].include(cfg_arch.param_values["SXLEN"])) || \
+      [nil, 3264].include?(cfg_arch.param_values["SXLEN"])) || \
       (cfg_arch.possible_extensions.map(&:name).include?("H") && \
       [nil, 3264].include?(cfg_arch.param_values["VSXLEN"]))
     else
@@ -211,7 +212,7 @@ def length(effective_xlen = nil)
     when Integer
       @data["length"]
     else
-      raise "Unexpected length field for #{csr.name}"
+      raise "Unexpected length field for #{name}"
     end
   end
 
@@ -281,7 +282,7 @@ def max_length
     when Integer
       @data["length"]
     else
-      raise "Unexpected length field for #{csr.name}"
+      raise "Unexpected length field for #{name}"
     end
   end
 
@@ -388,6 +389,7 @@ def possible_fields_for(effective_xlen)
 
   # @return [Array<CsrField>] All implemented fields for this CSR
   #                           Excluded any fields that are defined by unimplemented extensions
+  sig {returns(T::Array[CsrField])}
   def possible_fields
     @possible_fields ||= fields.select do |f|
       f.exists_in_cfg?(cfg_arch)
@@ -404,8 +406,8 @@ def fields
   # @param effective_xlen [Integer or nil] 32 or 64 for fixed xlen, nil for dynamic
   # @return [Array<CsrField>] All known fields of this CSR when XLEN == +effective_xlen+
   # equivalent to {#fields} if +effective_xlen+ is nil
+  sig {params(effective_xlen: T.nilable(Integer)).returns(T::Array[CsrField])}
   def fields_for(effective_xlen)
-    raise ArgumentError, "effective_xlen is non-nil and is a #{effective_xlen.class} but must be an Integer" unless effective_xlen.nil? || effective_xlen.is_a?(Integer)
     fields.select { |f| effective_xlen.nil? || !f.key?("base") || f.base == effective_xlen }
   end
 
@@ -497,14 +499,14 @@ def sw_read_ast(symtab)
       return_type: Idl::Type.new(:bits, width: 128), # big int to hold special return values
       name: "CSR[#{name}].sw_read()",
       input_file: __source,
-      input_line: source_line("sw_read()"),
+      input_line: source_line(["sw_read()"]),
       symtab:,
       type_check: false
     )
 
     raise "unexpected #{@sw_read_ast.class}" unless @sw_read_ast.is_a?(Idl::FunctionBodyAst)
 
-    @sw_read_ast.set_input_file_unless_already_set(__source, source_line("sw_read()"))
+    @sw_read_ast.set_input_file_unless_already_set(__source, source_line(["sw_read()"]))
 
     @sw_read_ast
   end
@@ -609,7 +611,7 @@ def wavedrom_desc(cfg_arch, effective_xlen, exclude_unimplemented: false, option
       else
         desc["reg"] << { "bits" => field.location(effective_xlen).size, "name" => field.name, type: 3 }
       end
-      last_idx = field.location(effective_xlen).max
+      last_idx = T.cast(field.location(effective_xlen).max, Integer)
     end
     if !field_list.empty? && (field_list.last.location(effective_xlen).max != (length(effective_xlen) - 1))
       # reserved space at the end
diff --git a/lib/arch_obj_models/csr_field.rb b/lib/arch_obj_models/csr_field.rb
index eb92f3822b..7c7c6de610 100644
--- a/lib/arch_obj_models/csr_field.rb
+++ b/lib/arch_obj_models/csr_field.rb
@@ -1,4 +1,7 @@
 # frozen_string_literal: true
+# typed: true
+
+require "sorbet-runtime"
 
 require_relative "database_obj"
 require_relative "../idl/passes/gen_option_adoc"
@@ -6,10 +9,12 @@
 
 # A CSR field object
 class CsrField < DatabaseObject
+  extend T::Sig
   # Add all methods in this module to this type of database object.
   include CertifiableObject
 
   # @return [Csr] The Csr that defines this field
+  sig { returns(Csr) }
   attr_reader :parent
 
   # @!attribute field
@@ -20,12 +25,14 @@ class CsrField < DatabaseObject
 
   # @return [Integer] The base XLEN required for this CsrField to exist. One of [32, 64]
   # @return [nil] if the CsrField exists in any XLEN
+  sig { returns(T.nilable(Integer)) }
   def base
     @data["base"]
   end
 
   # @param parent_csr [Csr] The Csr that defined this field
   # @param field_data [Hash<String,Object>] Field data from the arch spec
+  sig { params(parent_csr: Csr, field_name: String, field_data: T::Hash[String, T.untyped]).void }
   def initialize(parent_csr, field_name, field_data)
     super(field_data, parent_csr.data_path, parent_csr.arch)
     @name = field_name
@@ -36,14 +43,16 @@ def initialize(parent_csr, field_name, field_data)
   def __source = @parent.__source
 
   # CSR field data starts at fields: NAME: with the YAML
-  def source_line(*path)
-    super("fields", name, *path)
+  sig { params(path: T::Array[String]).returns(Integer) }
+  def source_line(path)
+    super(["fields", name].concat(path))
   end
 
   # For a full config, whether or not the field is implemented
   # For a partial config, whether or the it is possible for the field to be implemented
   #
   # @return [Boolean] True if this field might exist in a config
+  sig { params(cfg_arch: ConfiguredArchitecture).returns(T::Boolean) }
   def exists_in_cfg?(cfg_arch)
     if cfg_arch.fully_configured?
       parent.exists_in_cfg?(cfg_arch) &&
@@ -59,6 +68,7 @@ def exists_in_cfg?(cfg_arch)
   end
 
   # @return [Boolean] For a partially configured cfg_arch, whether or not the field is optional (not mandatory or prohibited)
+  sig { params(cfg_arch: ConfiguredArchitecture).returns(T::Boolean) }
   def optional_in_cfg?(cfg_arch)
     raise "optional_in_cfg? should only be called on a partially configured cfg_arch" unless cfg_arch.partially_configured?
 
@@ -77,21 +87,25 @@ def optional_in_cfg?(cfg_arch)
   # @return [Boolean] Whether or not the presence of ext_ver affects this CSR Field definition
   #                   This does not take the parent CSR into account, i.e., a field can be unaffected
   #                   by ext_ver even if the parent CSR is affected
+  sig { params(ext_ver: ExtensionVersion).returns(T::Boolean) }
   def affected_by?(ext_ver)
-    @data["definedBy"].nil? ? false : defined_by_condition.possibly_satisfied_by?(version)
+    @data["definedBy"].nil? ? false : defined_by_condition.possibly_satisfied_by?(ext_ver)
   end
 
   # @return [Idl::FunctionBodyAst] Abstract syntax tree of the type() function
   # @return [nil] if the type property is not a function
+  sig { returns(T.nilable(Idl::FunctionBodyAst)) }
   def type_ast
     return @type_ast unless @type_ast.nil?
     return nil if @data["type()"].nil?
 
+    idl_code = T.must(@data["type()"])
+
     @type_ast = @cfg_arch.idl_compiler.compile_func_body(
-      @data["type()"],
+      idl_code,
       name: "CSR[#{csr.name}].#{name}.type()",
       input_file: csr.__source,
-      input_line: csr.source_line("fields", name, "type()"),
+      input_line: csr.source_line(["fields", name, "type()"]),
       symtab: @cfg_arch.symtab,
       type_check: false
     )
@@ -106,9 +120,8 @@ def type_ast
   # @return [Idl::FunctionBodyAst] Abstract syntax tree of the type() function, after it has been type checked
   # @return [nil] if the type property is not a function
   # @param effective_xlen [32, 64] The effective xlen to evaluate for
+  sig { params(effective_xlen: T.nilable(Integer)).returns(T.nilable(Idl::FunctionBodyAst)) }
   def type_checked_type_ast(effective_xlen)
-    raise ArgumentError, "effective_xlen is non-nil and is a #{effective_xlen.class} but must be an Integer" unless effective_xlen.nil? || effective_xlen.is_a?(Integer)
-
     @type_checked_type_ast ||= { 32 => nil, 64 => nil }
     return @type_checked_type_ast[effective_xlen] unless @type_checked_type_ast[effective_xlen].nil?
 
@@ -135,9 +148,9 @@ def type_checked_type_ast(effective_xlen)
 
   # @return [Idl::FunctionBodyAst] Abstract syntax tree of the type() function, after it has been type checked and pruned
   # @return [nil] if the type property is not a function
+  # @param effective_xlen [32, 64] The effective xlen to evaluate for
+  sig { params(effective_xlen: T.nilable(Integer)).returns(T.nilable(Idl::FunctionBodyAst)) }
   def pruned_type_ast(effective_xlen)
-    raise ArgumentError, "effective_xlen is non-nil and is a #{effective_xlen.class} but must be an Integer" unless effective_xlen.nil? || effective_xlen.is_a?(Integer)
-
     @pruned_type_ast ||= { 32 => nil, 64 => nil }
     return @pruned_type_ast[effective_xlen] unless @pruned_type_ast[effective_xlen].nil?
 
@@ -178,22 +191,20 @@ def pruned_type_ast(effective_xlen)
   #      'RW-R'  => Read-write, with a restricted set of legal values
   #      'RW-H'  => Read-write, with a hardware update
   #      'RW-RH' => Read-write, with a hardware update and a restricted set of legal values
+  # @return [nil] when the type isn't knowable
+  sig { params(effective_xlen: T.nilable(Integer)).returns(T.nilable(String)) }
   def type(effective_xlen = nil)
-    raise ArgumentError, "effective_xlen is non-nil and is a #{effective_xlen.class} but must be an Integer" unless effective_xlen.nil? || effective_xlen.is_a?(Integer)
-
     @type ||= { 32 => nil, 64 => nil }
     return @type[effective_xlen] unless @type[effective_xlen].nil?
 
+    type = T.let(nil, T.untyped)
     type =
       if @data.key?("type")
         @data["type"]
       else
         # the type is config-specific...
-        idl = @data["type()"]
-        raise "type() is nil for #{csr.name}.#{name} #{@data}?" if idl.nil?
 
-        # value_result = Idl::AstNode.value_try do
-        ast = type_checked_type_ast(effective_xlen)
+        ast = T.must(type_checked_type_ast(effective_xlen))
         begin
           symtab = fill_symtab_for_type(effective_xlen, ast)
 
@@ -219,8 +230,8 @@ def type(effective_xlen = nil)
             type = nil
           end
         ensure
-          symtab.pop
-          symtab.release
+          symtab&.pop
+          symtab&.release
         end
         type
         # end
@@ -236,28 +247,25 @@ def type(effective_xlen = nil)
 
   # @return [String] A pretty-printed type string
   # @param effective_xlen [32, 64] The effective xlen to evaluate for
+  sig { params(effective_xlen: T.nilable(Integer)).returns(String) }
   def type_pretty(effective_xlen = nil)
-    raise ArgumentError, "effective_xlen is non-nil and is a #{effective_xlen.class} but must be an Integer" unless effective_xlen.nil? || effective_xlen.is_a?(Integer)
-
-    str = nil
-    value_result = Idl::AstNode.value_try do
-      str = type(effective_xlen)
-    end
-    Idl::AstNode.value_else(value_result) do
-      ast = type_ast
+    str = type(effective_xlen)
+    if str.nil?
+      ast = T.must(type_ast)
       str = ast.gen_option_adoc
     end
-    str
+    T.must(str)
   end
 
   # @return [Alias,nil] The aliased field, or nil if there is no alias
+  sig { returns(T.nilable(Alias)) }
   def alias
     return @alias unless @alias.nil?
 
     if @data.key?("alias")
       raise "Can't parse alias" unless data["alias"] =~ /^[a-z][a-z0-9]+\.[A-Z0-9]+(\[([0-9]+)(:[0-9]+)?\])?$/
 
-      csr_name = Regexp.last_match(1)
+      csr_name = T.must(Regexp.last_match(1))
       csr_field = Regexp.last_match(2)
       range = Regexp.last_match(3)
       range_start = Regexp.last_match(4)
@@ -266,7 +274,7 @@ def alias
       csr_field = cfg_arch.csr(csr_name).field(csr_field)
       range =
         if range.nil?
-          field.location
+          csr_field.location
         elsif range_end.nil?
           (range_start.to_i..range_start.to_i)
         else
@@ -280,9 +288,8 @@ def alias
   # @return [Array<Idl::FunctionDefAst>] List of functions called through this field
   # @param cfg_arch [ConfiguredArchitecture] a configuration
   # @Param effective_xlen [Integer] 32 or 64; needed because fields can change in different XLENs
+  sig { params(effective_xlen: T.nilable(Integer)).returns(T::Array[Idl::FunctionDefAst]) }
   def reachable_functions(effective_xlen)
-    raise ArgumentError, "effective_xlen is non-nil and is a #{effective_xlen.class} but must be an Integer" unless effective_xlen.nil? || effective_xlen.is_a?(Integer)
-
     return @reachable_functions unless @reachable_functions.nil?
 
     fns = []
@@ -319,6 +326,7 @@ def reachable_functions(effective_xlen)
 
   # @return [Boolean] Whether or not the location of the field changes dynamically
   #                   (e.g., based on mstatus.SXL) in the configuration
+  sig { returns(T::Boolean) }
   def dynamic_location?
     # if there is no location_rv32, the the field never changes
     return false unless @data["location"].nil?
@@ -329,6 +337,7 @@ def dynamic_location?
 
   # @return [Idl::FunctionBodyAst] Abstract syntax tree of the reset_value function
   # @return [nil] If the reset_value is not a function
+  sig { returns(T.nilable(Idl::FunctionBodyAst)) }
   def reset_value_ast
     return @reset_value_ast unless @reset_value_ast.nil?
     return nil unless @data.key?("reset_value()")
@@ -338,15 +347,15 @@ def reset_value_ast
       return_type: Idl::Type.new(:bits, width: max_width),
       name: "CSR[#{parent.name}].#{name}.reset_value()",
       input_file: csr.__source,
-      input_line: csr.source_line("fields", name, "reset_value()"),
+      input_line: csr.source_line(["fields", name, "reset_value()"]),
       symtab: cfg_arch.symtab,
       type_check: false
     )
   end
 
-  # @param symtab [Idl::SymbolTable] A symbol table with globals
   # @return [Idl::FunctionBodyAst] Abstract syntax tree of the reset_value function, after being type checked
   # @return [nil] If the reset_value is not a function
+  sig { returns(T.nilable(Idl::FunctionBodyAst)) }
   def type_checked_reset_value_ast
     return @type_checked_reset_value_ast unless @type_checked_reset_value_ast.nil?
 
@@ -367,12 +376,13 @@ def type_checked_reset_value_ast
 
   # @return [Idl::FunctionBodyAst] Abstract syntax tree of the reset_value function, type checked and pruned
   # @return [nil] If the reset_value is not a function
+  sig { returns(T.nilable(Idl::FunctionBodyAst)) }
   def pruned_reset_value_ast
     return @pruned_reset_value_ast unless @pruned_reset_value_ast.nil?
 
     return nil unless @data.key?("reset_value()")
 
-    ast = type_checked_reset_value_ast
+    ast = T.must(type_checked_reset_value_ast)
 
     symtab = fill_symtab_for_reset(ast)
     ast = ast.prune(symtab)
@@ -390,9 +400,9 @@ def reset_value
       if @data.key?("reset_value")
         @data["reset_value"]
       else
-        ast = pruned_reset_value_ast
+        ast = T.must(pruned_reset_value_ast)
         symtab = fill_symtab_for_reset(ast)
-        val = nil
+        val = T.let(nil, T.untyped)
         value_result = Idl::AstNode.value_try do
           val = ast.return_value(symtab)
         end
@@ -406,6 +416,7 @@ def reset_value
     end
   end
 
+  sig { returns(T::Boolean) }
   def dynamic_reset_value?
     return false unless @data["reset_value"].nil?
 
@@ -415,25 +426,21 @@ def dynamic_reset_value?
     end || true
   end
 
+  sig { returns(String) }
   def reset_value_pretty
-    str = nil
+    str = T.let(nil, T.nilable(String))
     value_result = Idl::AstNode.value_try do
       str = reset_value
     end
     Idl::AstNode.value_else(value_result) do
-      ast = reset_value_ast
+      ast = T.must(reset_value_ast)
       str = ast.gen_option_adoc
     end
-    str
-  end
-
-  # @return [Boolean] true if the field could have an undefined value at any point
-  def could_be_undefined?
-    (reset_value == "UNDEFINED_LEGAL") || \
-      (has_custom_sw_write? && sw_write_ast(cfg_arch.symtab).could_return_undefined?(cfg_arch.symtab))
+    T.must(str).to_s
   end
 
   # @return [Boolean] true if the CSR field has a custom sw_write function
+  sig { returns(T::Boolean) }
   def has_custom_sw_write?
     @data.key?("sw_write(csr_value)") && !@data["sw_write(csr_value)"].empty?
   end
@@ -441,9 +448,8 @@ def has_custom_sw_write?
   # @param effective_xlen [Integer] 32 or 64; the effective XLEN to evaluate this field in (relevant when fields move in different XLENs)
   # @param symtab [Idl::SymbolTable] Symbol table with globals
   # @return [FunctionBodyAst] The abstract syntax tree of the sw_write() function, after being type checked
+  sig { params(symtab: Idl::SymbolTable, effective_xlen: T.nilable(Integer)).returns(T.nilable(Idl::FunctionBodyAst)) }
   def type_checked_sw_write_ast(symtab, effective_xlen)
-    raise ArgumentError, "effective_xlen is non-nil and is a #{effective_xlen.class} but must be an Integer" unless effective_xlen.nil? || effective_xlen.is_a?(Integer)
-
     @type_checked_sw_write_asts ||= {}
     ast = @type_checked_sw_write_asts[symtab.hash]
     return ast unless ast.nil?
@@ -467,7 +473,7 @@ def type_checked_sw_write_ast(symtab, effective_xlen)
       Idl::Var.new("csr_value", csr.bitfield_type(symtab.cfg_arch, effective_xlen))
     )
 
-    ast = sw_write_ast(symtab)
+    ast = T.must(sw_write_ast(symtab))
     symtab.cfg_arch.idl_compiler.type_check(
       ast,
       symtab,
@@ -480,10 +486,9 @@ def type_checked_sw_write_ast(symtab, effective_xlen)
 
   # @return [Idl::FunctionBodyAst] The abstract syntax tree of the sw_write() function
   # @return [nil] If there is no sw_write() function
-  # @param cfg_arch [ConfiguredArchitecture] An architecture definition
+  # @param symtab [Idl::SymbolTable] Symbols
+  sig { params(symtab: Idl::SymbolTable).returns(T.nilable(Idl::FunctionBodyAst)) }
   def sw_write_ast(symtab)
-    raise ArgumentError, "Argument should be a symtab" unless symtab.is_a?(Idl::SymbolTable)
-
     return @sw_write_ast unless @sw_write_ast.nil?
     return nil if @data["sw_write(csr_value)"].nil?
 
@@ -493,7 +498,7 @@ def sw_write_ast(symtab)
       return_type: Idl::Type.new(:bits, width: 128), # big int to hold special return values
       name: "CSR[#{csr.name}].#{name}.sw_write(csr_value)",
       input_file: csr.__source,
-      input_line: csr.source_line("fields", name, "sw_write(csr_value)"),
+      input_line: csr.source_line(["fields", name, "sw_write(csr_value)"]),
       symtab:,
       type_check: false
     )
@@ -503,6 +508,7 @@ def sw_write_ast(symtab)
     @sw_write_ast
   end
 
+  sig { params(effective_xlen: T.nilable(Integer), ast: Idl::AstNode).returns(Idl::SymbolTable) }
   def fill_symtab_for_sw_write(effective_xlen, ast)
     symtab = cfg_arch.symtab.global_clone
     symtab.push(ast)
@@ -534,9 +540,8 @@ def fill_symtab_for_sw_write(effective_xlen, ast)
     symtab
   end
 
+  sig { params(effective_xlen: T.nilable(Integer), ast: Idl::AstNode).returns(Idl::SymbolTable) }
   def fill_symtab_for_type(effective_xlen, ast)
-    raise ArgumentError, "effective_xlen is non-nil and is a #{effective_xlen.class} but must be an Integer" unless effective_xlen.nil? || effective_xlen.is_a?(Integer)
-
     symtab = cfg_arch.symtab.global_clone
     symtab.push(ast)
 
@@ -582,14 +587,13 @@ def fill_symtab_for_reset(ast)
   # @return [Idl::FunctionBodyAst] The abstract syntax tree of the sw_write() function, type checked and pruned
   # @return [nil] if there is no sw_write() function
   # @param effective_xlen [Integer] effective xlen, needed because fields can change in different bases
+  sig { params(effective_xlen: T.nilable(Integer)).returns(T.nilable(Idl::AstNode)) }
   def pruned_sw_write_ast(effective_xlen)
-    raise ArgumentError, "effective_xlen is non-nil and is a #{effective_xlen.class} but must be an Integer" unless effective_xlen.nil? || effective_xlen.is_a?(Integer)
-
     return @pruned_sw_write_ast unless @pruned_sw_write_ast.nil?
 
     return nil unless @data.key?("sw_write(csr_value)")
 
-    ast = type_checked_sw_write_ast(cfg_arch.symtab, effective_xlen)
+    ast = T.must(type_checked_sw_write_ast(cfg_arch.symtab, effective_xlen))
 
     return ast if cfg_arch.unconfigured?
 
@@ -615,9 +619,8 @@ def pruned_sw_write_ast(effective_xlen)
   # @param cfg_arch [ConfiguredArchitecture] A config. May be nil if the location is not configturation-dependent
   # @param effective_xlen [Integer] The effective xlen, needed since some fields change location with XLEN. If the field location is not determined by XLEN, then this parameter can be nil
   # @return [Range] the location within the CSR as a range (single bit fields will be a range of size 1)
+  sig { params(effective_xlen: T.nilable(Integer)).returns(T::Range[Integer]) }
   def location(effective_xlen = nil)
-    raise ArgumentError, "effective_xlen is non-nil and is a #{effective_xlen.class} but must be an Integer" unless effective_xlen.nil? || effective_xlen.is_a?(Integer)
-
     key =
       if @data.key?("location")
         "location"
@@ -641,7 +644,9 @@ def location(effective_xlen = nil)
       end
 
       @data[key]..@data[key]
-    elsif @data[key].is_a?(String)
+    else
+      raise "Unexpected location field" unless @data[key].is_a?(String)
+
       e, s = @data[key].split("-").map(&:to_i)
       raise "Invalid location" if s > e
 
@@ -661,26 +666,34 @@ def location(effective_xlen = nil)
   end
 
   # @return [Boolean] Whether or not this field only exists when XLEN == 64
+  sig { returns(T::Boolean) }
   def base64_only? = @data.key?("base") && @data["base"] == 64
 
   # @return [Boolean] Whether or not this field only exists when XLEN == 32
+  sig { returns(T::Boolean) }
   def base32_only? = @data.key?("base") && @data["base"] == 32
 
+  sig { returns(T::Boolean) }
   def defined_in_base32? = @data["base"].nil? || @data["base"] == 32
+
+  sig { returns(T::Boolean) }
   def defined_in_base64? = @data["base"].nil? || @data["base"] == 64
+
+  sig { params(xlen: Integer).returns(T::Boolean) }
   def defined_in_base?(xlen) = @data["base"].nil? || @data["base"] == xlen
 
   # @return [Boolean] Whether or not this field exists for any XLEN
+  sig { returns(T::Boolean) }
   def defined_in_all_bases? = @data["base"].nil?
 
   # @param effective_xlen [Integer] The effective xlen, needed since some fields change location with XLEN. If the field location is not determined by XLEN, then this parameter can be nil
   # @return [Integer] Number of bits in the field
+  sig { params(effective_xlen: T.nilable(Integer)).returns(Integer) }
   def width(effective_xlen)
-    raise ArgumentError, "effective_xlen is non-nil and is a #{effective_xlen.class} but must be an Integer" unless effective_xlen.nil? || effective_xlen.is_a?(Integer)
-
-    location(effective_xlen).size
+    T.must(location(effective_xlen).size)
   end
 
+  sig { returns(Integer) }
   def max_width
     @max_width ||=
       if base64_only?
@@ -694,6 +707,7 @@ def max_width
       end
   end
 
+  sig { returns(String) }
   def location_cond32
     case csr.priv_mode
     when "M"
@@ -707,6 +721,7 @@ def location_cond32
     end
   end
 
+  sig { returns(String) }
   def location_cond64
     case csr.priv_mode
     when "M"
@@ -722,8 +737,8 @@ def location_cond64
 
   # @param effective_xlen [Integer or nil] 32 or 64 for fixed xlen, nil for dynamic
   # @return [String] Pretty-printed location string
+  sig { params(effective_xlen: T.nilable(Integer)).returns(String) }
   def location_pretty(effective_xlen = nil)
-    raise ArgumentError, "effective_xlen is non-nil and is a #{effective_xlen.class} but must be an Integer" unless effective_xlen.nil? || effective_xlen.is_a?(Integer)
     derangeify = proc { |loc|
       next loc.min.to_s if loc.size == 1
 
@@ -806,9 +821,8 @@ def location_pretty(effective_xlen = nil)
   }.freeze
 
   # @return [String] Long description of the field type
+  sig { params(effective_xlen: T.nilable(Integer)).returns(String) }
   def type_desc(effective_xlen=nil)
-    raise ArgumentError, "effective_xlen is non-nil and is a #{effective_xlen.class} but must be an Integer" unless effective_xlen.nil? || effective_xlen.is_a?(Integer)
-
-    TYPE_DESC_MAP[type(effective_xlen)]
+    TYPE_DESC_MAP.fetch(type(effective_xlen), "")
   end
 end
diff --git a/lib/arch_obj_models/database_obj.rb b/lib/arch_obj_models/database_obj.rb
index e1e5af5952..817d1de350 100644
--- a/lib/arch_obj_models/database_obj.rb
+++ b/lib/arch_obj_models/database_obj.rb
@@ -1,4 +1,7 @@
 # frozen_string_literal: true
+# typed: true
+
+require "sorbet-runtime"
 
 # Base class for any object representation of the Architecture.
 # does two things:
@@ -28,100 +31,9 @@
 require_relative "doc_link"
 
 class DatabaseObject
-  attr_reader :data, :data_path, :name, :long_name
-
-  # @return [Architecture] If only a specification (no config) is known
-  # @return [ConfiguredArchitecture] If a specification and config is known
-  # @return [nil] If neither is known
-  attr_reader :arch       # Use when Architecture class is sufficient
-
-  # @return [ConfiguredArchitecture] If a specification and config is known
-  # @return [nil] Otherwise
-  attr_reader :cfg_arch   # Use when extra stuff provided by ConfiguredArchitecture is required
-
-  def kind = @data["kind"]
-
-  # @param data [Hash<String,Object>] Hash with fields to be added
-  # @param data_path [Pathname] Path to the data file
-  # @param arch [Architecture or ConfiguredArchitecture] The RISC-V database with or without a specific configuration
-  def initialize(data, data_path, arch)
-    raise ArgumentError, "Need Architecture class but it's a #{arch.class}" unless arch.is_a?(Architecture)
-    raise ArgumentError, "Bad data" unless data.is_a?(Hash)
-
-    @data = data
-    @data_path = data_path
-    @arch = arch
-    if arch.is_a?(ConfiguredArchitecture)
-      @cfg_arch = arch
-    else
-      @cfg_arch = nil
-    end
-    @name = data["name"]
-    @long_name = data["long_name"]
-
-    @sem = Concurrent::Semaphore.new(1)
-    @cache = Concurrent::Hash.new
-  end
-
-  # @return [Array<CertNormativeRule>]
-  def cert_normative_rules
-    return @cert_normative_rules unless @cert_normative_rules.nil?
-
-    @cert_normative_rules = []
-    @data["cert_normative_rules"]&.each do |cert_data|
-      @cert_normative_rules << CertNormativeRule.new(cert_data, self)
-    end
-    @cert_normative_rules
-  end
-
-  # @return [Hash<String, CertNormativeRule>] Hash with ID as key of all normative rules defined by database object
-  def cert_coverage_point_hash
-    return @cert_coverage_point_hash unless @cert_coverage_point_hash.nil?
-
-    @cert_coverage_point_hash = {}
-    cert_normative_rules.each do |cp|
-      @cert_coverage_point_hash[cp.id] = cp
-    end
-    @cert_coverage_point_hash
-  end
-
-  # @param id [String] Unique ID for the normative rule
-  # @return [CertNormativeRule]
-  # @return [nil] if there is no certification normative ruleed with ID of +id+
-  def cert_coverage_point(id)
-    cert_coverage_point_hash[id]
-  end
-
-  # @return [Array<CertTestProcedure>]
-  def cert_test_procedures
-    return @cert_test_procedures unless @cert_test_procedures.nil?
+  extend T::Sig
 
-    @cert_test_procedures = []
-    @data["cert_test_procedures"]&.each do |cert_data|
-      @cert_test_procedures << CertTestProcedure.new(cert_data, self)
-    end
-    @cert_test_procedures
-  end
-
-  # @return [Hash<String, CertTestProcedure>] Hash of all normative rules defined by database object
-  def cert_test_procedure_hash
-    return @cert_test_procedure_hash unless @cert_test_procedure_hash.nil?
-
-    @cert_test_procedure_hash = {}
-    cert_test_procedures.each do |tp|
-      @cert_test_procedure_hash[tp.id] = tp
-    end
-    @cert_test_procedure_hash
-  end
-
-  # @param id [String] Unique ID for test procedure
-  # @return [CertTestProcedure]
-  # @return [nil] if there is no certification test procedure with ID +id+
-  def cert_test_procedure(id)
-    cert_test_procedure_hash[id]
-  end
-
- # Exception raised when there is a problem with a schema file
+  # Exception raised when there is a problem with a schema file
   class SchemaError < ::StandardError
     # result from JsonSchemer.validate
     attr_reader :result
@@ -186,17 +98,41 @@ def initialize(path, result)
     end
   end
 
-  attr_reader :data, :data_path, :name, :long_name
+  # exception raised when an object does not validate, from a check other than JSON Schema
+  class ValidationError < ::StandardError
+  end
+
+  sig { returns(T::Hash[String, T.untyped]) }
+  attr_reader :data
+
+  sig { returns(Pathname) }
+  attr_reader :data_path
+
+  sig { returns(String) }
+  attr_reader :name
+
+  sig { returns(String) }
+  attr_reader :long_name
 
   # @return [Architecture] If only a specification (no config) is known
   # @return [ConfiguredArchitecture] If a specification and config is known
   # @return [nil] If neither is known
+  sig { returns(Architecture) }
   attr_reader :arch       # Use when Architecture class is sufficient
 
   # @return [ConfiguredArchitecture] If a specification and config is known
   # @return [nil] Otherwise
-  attr_reader :cfg_arch   # Use when extra stuff provided by ConfiguredArchitecture is required
+  sig { returns(ConfiguredArchitecture) }
+  def cfg_arch
+    raise "no cfg_arch" if @cfg_arch.nil?
 
+    @cfg_arch
+  end
+
+  sig { returns(T::Boolean) }
+  def cfg_arch? = !@cfg_arch.nil?
+
+  sig { returns(String) }
   def kind = @data["kind"]
 
   @@schemas ||= {}
@@ -210,6 +146,7 @@ def kind = @data["kind"]
 
   # validate the data against it's schema
   # @raise [SchemaError] if the data is invalid
+  sig { void }
   def validate
     schemas = @@schemas
     ref_resolver = @@schema_ref_resolver
@@ -227,7 +164,7 @@ def validate
             ref_resolver:,
             insert_property_defaults: true
           )
-          raise SchemaError, schemas[schema_file].validate_schema unless schemas[schema_file].valid_schema?
+          raise SchemaError, T.must(schemas[schema_file]).validate_schema unless T.must(schemas[schema_file]).valid_schema?
 
           schemas[schema_file]
         end
@@ -253,19 +190,24 @@ def validate
   end
 
   # clone this, and set the arch at the same time
-  # @return [ExtensionRequirement] The new object
+  # @return [DatabaseObject] The new object
+  sig { params(arch: T.nilable(Architecture)).returns(DatabaseObject) }
   def clone(arch: nil)
     obj = super()
     obj.instance_variable_set(:@arch, arch)
     obj
   end
 
+  sig { params(other: DatabaseObject).returns(T.nilable(Integer)) }
   def <=>(other)
+    return nil unless other.is_a?(DatabaseObject)
+
     name <=> other.name
   end
 
   # @return [String] Source file that data for this object can be attributed to
   # @return [nil] if the source isn't known
+  sig { returns(T.nilable(String)) }
   def __source
     @data["$source"]
   end
@@ -274,8 +216,8 @@ def __source
   # @note Generally, you should prefer to use {#defined_by_condition}, etc. from Ruby
   #
   # @return [String] An extension name
-  # @return [Array(String, Number)] An extension name and versions
-  # @return [Array<*>] A list of extension names or extension names and versions
+  # @return [Hash<String, Object>] A requirements entry
+  sig { returns(T.any(String, T::Hash[String, Object])) }
   def definedBy
     @data["definedBy"]
   end
@@ -284,6 +226,14 @@ def definedBy
   # @param non_normative [Boolean] Include non-normative text?
   # @param when_cb [Proc(AstNode, String)] Callback to generate text for the un-knowable ast
   # @return [String] Description of the object, from YAML
+  sig {
+    params(
+      normative: T::Boolean,
+      non_normative: T::Boolean,
+      when_cb: T.proc.params(when_ast: Idl::AstNode, text: String).returns(T::Array[String])
+    )
+    .returns(String)
+  }
   def description(
     normative: true,      # display normative text?
     non_normative: true,  # display non-normative text?
@@ -306,7 +256,7 @@ def description(
             symtab: @cfg_arch.symtab,
             name: "#{name}.description[#{idx}].when",
             input_file: __source,
-            input_line: source_line("description", idx, "when()")
+            input_line: source_line(["description", idx, "when()"])
           )
 
           symtab = @cfg_arch.symtab.global_clone
@@ -349,18 +299,14 @@ def description(
 
   # @param data [Hash<String,Object>] Hash with fields to be added
   # @param data_path [Pathname] Path to the data file
-  # @param arch [Architecture] The RISC-V standard (can optionally be a ConfiguredArchitecture too)
+  sig { params(data: T::Hash[String, T.untyped], data_path: T.any(String, Pathname), arch: T.nilable(Architecture)).void }
   def initialize(data, data_path, arch)
-    raise ArgumentError, "data is a #{data.class} but needs to be a Hash" unless data.is_a?(Hash)
-    raise ArgumentError, "data_path is a #{data_path.class} but needs to be a Pathname" unless data_path.is_a?(Pathname)
-    raise ArgumentError, "arch is a #{arch.class} but needs to be an Architecture" unless arch.is_a?(Architecture)
-
     @data = data
-    @data_path = data_path
+    @data_path = Pathname.new(data_path)
     if arch.is_a?(ConfiguredArchitecture)
       @cfg_arch = arch
     end
-    @arch = arch
+    @arch = T.must(arch)
     @name = data["name"]
     @long_name = data["long_name"]
 
@@ -369,7 +315,7 @@ def initialize(data, data_path, arch)
   end
 
   def inspect
-    self.class.name + "##{name}"
+    "#{self.class.name}##{name}"
   end
 
   # make the underlying YAML description available with []
@@ -377,23 +323,25 @@ def inspect
   def_delegator :@data, :[]
 
   # @return [Array<String>] List of keys added by this DatabaseObject
+  sig { returns(T::Array[String]) }
   def keys = @data.keys
 
   # @param k (see Hash#key?)
   # @return (see Hash#key?)
+  sig { params(k: String).returns(T::Boolean) }
   def key?(k) = @data.key?(k)
 
+  # defer the calculation of 'blk' until later, then memoize the result
+  sig { params(fn_name: Symbol, block: T.proc.void).returns(T.untyped) }
   def defer(fn_name, &block)
     cache_value = @cache[fn_name]
     return cache_value unless cache_value.nil?
 
-    raise "Missing block" unless block_given?
-
     @cache[fn_name] ||= yield
   end
 
-  # @return [ExtensionRequirementExpression] Extension(s) that define the database object (e.g., Instruction, CSR).
-  #                                          If *any* requirement is met, the object is defined.
+  # @return [ExtensionRequirementExpression] Extension(s) that define the instruction. If *any* requirement is met, the instruction is defined.
+  sig { returns(ExtensionRequirementExpression) }
   def defined_by_condition
     @defined_by_condition ||=
       begin
@@ -403,7 +351,8 @@ def defined_by_condition
       end
   end
 
-  # @return [String] Name of an extension that "primarily" defines the object (i.e., is the first in a list)
+  # @return [ExtensionRequirement] Name of an extension that "primarily" defines the object (i.e., is the first in a list)
+  sig { returns(ExtensionRequirement) }
   def primary_defined_by
     defined_by_condition.first_requirement
   end
@@ -420,22 +369,24 @@ def primary_defined_by
   #   06: YAML
   #   misa_csr.source_line("sw_read()")  #=> 2
   #   mis_csr.source_line("fields", "A", "type()") #=> 5
-  def source_line(*path)
+  sig { params(path: T::Array[String]).returns(Integer) }
+  def source_line(path)
 
     # find the line number of this operation() in the *original* file
     yaml_filename = __source
     raise "No $source for #{name}" if yaml_filename.nil?
-    line = nil
+    line = T.let(nil, T.untyped)
     path_idx = 0
     Psych.parse_stream(File.read(yaml_filename), filename: yaml_filename) do |doc|
       mapping = doc.children[0]
-      data =
+      data = T.let(
         if mapping.children.size == 2
           mapping.children[1]
         else
           mapping
-        end
-      found = false
+        end,
+        Psych::Nodes::Node)
+      found = T.let(false, T::Boolean)
       while path_idx < path.size
         if data.is_a?(Psych::Nodes::Mapping)
           idx = 0
@@ -480,34 +431,45 @@ def source_line(*path)
 
 # A company description
 class Company
+  extend T::Sig
+
+  sig { params(data: T::Hash[String, String]).void }
   def initialize(data)
     @data = data
   end
 
   # @return [String] Company name
-  def name = @data["name"]
+  sig { returns(String) }
+  def name = T.must(@data["name"])
 
   # @return [String] Company website
-  def url = @data["url"]
+  sig { returns(String) }
+  def url = T.must(@data["url"])
 end
 
 # License information
 class License
+  extend T::Sig
+
+  sig { params(data: T::Hash[String, T.nilable(String)]).void }
   def initialize(data)
     @data = data
   end
 
   # @return [String] License name
-  def name = @data["name"]
+  sig { returns(String) }
+  def name = T.must(@data["name"])
 
   # @return [String] License website
   # @return [nil] if there is no website for the license
-  def url = @data["url"]
+  sig { returns(String) }
+  def url = T.must(@data["url"])
 
   # @return [String] Text of the license
+  sig { returns(String) }
   def text
     if !@data["text_url"].nil?
-      Net::HTTP.get(URI(@data["text_url"]))
+      Net::HTTP.get(URI(T.must(@data["text_url"])))
     else
       @data["text"]
     end
@@ -516,715 +478,32 @@ def text
 
 # Personal information about a contributor
 class Person
+  extend T::Sig
   include Comparable
 
   # @return [String] Person's name
-  def name = @data["name"]
+  sig { returns(String) }
+  def name = T.must(@data["name"])
 
   # @return [String] Email address
   # @return [nil] if email address is not known
+  sig { returns(T.nilable(String)) }
   def email = @data["email"]
 
   # @return [String] Company the person works for
   # @return [nil] if the company is not known, or if the person is an individual contributor
+  sig { returns(T.nilable(String)) }
   def company = @data["company"]
 
+  sig { params(data: T::Hash[String, T.nilable(String)]).void }
   def initialize(data)
     @data = data
   end
 
+  sig { params(other: Person).returns(T.nilable(Integer)) }
   def <=>(other)
-    raise ArgumentError, "Person is only comparable to Person (not #{other.class.name})" unless other.is_a?(Person)
+    return nil unless other.is_a?(Person)
 
     name <=> other.name
   end
 end
-
-# represents an `implies:` entry for an extension
-# which is a list of extension versions, zero or more of which
-# may be conditional (via an ExtensionRequirementExpression)
-class ConditionalExtensionVersionList
-  def initialize(ary, cfg_arch)
-    @ary = ary
-    @cfg_arch = cfg_arch
-  end
-
-  def empty? = @ary.nil? || @ary.empty?
-
-  def size = empty? ? 0 : eval.size
-
-  def each(&block)
-    raise "Missing block" unless block_given?
-
-    eval.each(&block)
-  end
-
-  def map(&block)
-    eval.map(&block)
-  end
-
-  # Returns array of ExtensionVersions, along with a condition under which it is in the list
-  #
-  # @example
-  #   list.eval #=> [{ :ext_ver => ExtensionVersion.new(:A, "2.1.0"), :cond => ExtensionRequirementExpression.new(...) }]
-  #
-  # @return [Array<Hash{Symbol => ExtensionVersion, ExtensionRequirementExpression}>]
-  #           The extension versions in the list after evaluation, and the condition under which it applies
-  def eval
-    result = []
-    if @ary.is_a?(Hash)
-      result << { ext_ver: entry_to_ext_ver(@ary), cond: AlwaysTrueExtensionRequirementExpression.new }
-    else
-      @ary.each do |elem|
-        if elem.is_a?(Hash) && elem.keys[0] == "if"
-          cond_expr = ExtensionRequirementExpression.new(elem["if"], @cfg_arch)
-          result << { ext_ver: entry_to_ext_ver(elem["then"]), cond: cond_expr }
-        else
-          result << { ext_ver: entry_to_ext_ver(elem), cond: AlwaysTrueExtensionRequirementExpression.new }
-        end
-      end
-    end
-    result
-  end
-  alias to_a eval
-
-  def entry_to_ext_ver(entry)
-    ExtensionVersion.new(entry["name"], entry["version"], @cfg_arch, fail_if_version_does_not_exist: true)
-  end
-  private :entry_to_ext_ver
-end
-
-# represents a JSON Schema composition of extension requirements, e.g.:
-#
-# anyOf:
-#   - oneOf:
-#     - A
-#     - B
-#   - C
-#
-class ExtensionRequirementExpression
-  # @param composition_hash [Hash] A possibly recursive hash of "allOf", "anyOf", "oneOf", "not", "if"
-  def initialize(composition_hash, cfg_arch)
-    raise ArgumentError, "composition_hash is nil" if composition_hash.nil?
-
-    unless is_a_condition?(composition_hash)
-      raise ArgumentError, "Expecting a JSON schema comdition (got #{composition_hash})"
-    end
-
-    unless cfg_arch.is_a?(ConfiguredArchitecture)
-      raise ArgumentError, "Must provide a cfg_arch"
-    end
-
-    @hsh = composition_hash
-    @arch = cfg_arch
-  end
-
-  def to_h = @hsh
-
-  def empty? = false
-
-  def is_a_version_requirement(ver)
-    case ver
-    when String
-      ver =~ RequirementSpec::REQUIREMENT_REGEX
-    when Array
-      ver.all? { |v| v =~ RequirementSpec::REQUIREMENT_REGEX }
-    else
-      false
-    end
-  end
-  private :is_a_version_requirement
-
-  # @return [Boolean] True if the condition is a join of N terms over the same operator
-  #
-  #  A or B or C   #=> true
-  #  A and B       #=> true
-  #  A or B and C  #=> false
-  def flat?
-    case @hsh
-    when String
-      true
-    when Hash
-      @hsh.key?("name") || @hsh[@hsh.keys.first].all? { |child| child.is_a?(String) || (child.is_a?(Hash) && child.key?("name")) }
-    else
-      raise "unexpected"
-    end
-  end
-
-  # @return [:or, :and] The operator for a flat condition
-  #                     Only valid if #flat? is true
-  def flat_op
-    case @hsh
-    when String
-      :or
-    when Hash
-      @hsh.key?("name") ? :or : { "allOf" => :and, "anyOf" => :or }[@hsh.keys.first]
-    else
-      raise "unexpected"
-    end
-  end
-
-  # @return [Array<ExtensionRequirement>] The elements of the flat join
-  #                                       Only valid if #flat? is true
-  def flat_versions
-    case @hsh
-    when String
-      [ExtensionRequirement.new(@hsh, arch: @arch)]
-    when Hash
-      if @hsh.key?("name")
-        if @hsh.key?("version").nil?
-          [ExtensionRequirement.new(@hsh["name"], arch: @arch)]
-        else
-          [ExtensionRequirement.new(@hsh["name"], @hsh["version"], arch: @arch)]
-        end
-      else
-        @hsh[@hsh.keys.first].map do |r|
-          if r.is_a?(String)
-            ExtensionRequirement.new(r, arch: @arch)
-          else
-            if r.key?("version").nil?
-              ExtensionRequirement.new(r["name"], arch: @arch)
-            else
-              ExtensionRequirement.new(r["name"], r["version"], arch: @arch)
-            end
-          end
-        end
-      end
-    else
-      raise "unexpected"
-    end
-  end
-
-  def to_asciidoc(cond = @hsh, indent = 0, join: "\n")
-    case cond
-    when String
-      "#{'*' * indent}* #{cond}, version >= #{@arch.extension(cond).min_version}"
-    when Hash
-      if cond.key?("name")
-        if cond.key?("version")
-          "#{'*' * indent}* #{cond['name']}, version #{cond['version']}#{join}"
-        else
-          "#{'*' * indent}* #{cond['name']}, version >= #{@arch.extension(cond['name']).min_version}#{join}"
-        end
-      else
-        "#{'*' * indent}* #{cond.keys[0]}:#{join}" + to_asciidoc(cond[cond.keys[0]], indent + 2)
-      end
-    when Array
-      cond.map { |e| to_asciidoc(e, indent) }.join(join)
-    else
-      raise "Unknown condition type: #{cond}"
-    end
-  end
-
-  # @overload is_a_condition?(hsh)
-  #   @param hsh [String] Extension name (case sensitive)
-  #   @return [Boolean] True
-  # @overload is_a_condition?(hsh)
-  #   @param hsh [Hash<String, Object>] Extension name (case sensitive)
-  #   @return [Boolean] True if hash is a JSON schema condition
-  def is_a_condition?(hsh)
-    case hsh
-    when String
-      true
-    when Hash
-      if hsh.key?("name")
-        return false if hsh.size > 2
-
-        if hsh.size > 1
-          return false unless hsh.key?("version")
-
-          return false unless is_a_version_requirement(hsh["version"])
-        end
-
-      elsif hsh.key?("not")
-        return false unless hsh.size == 1
-
-        return is_a_condition?(hsh["not"])
-
-      else
-        return false unless hsh.size == 1
-
-        return false unless ["allOf", "anyOf", "oneOf", "if"].include?(hsh.keys[0])
-
-        hsh[hsh.keys[0]].each do |element|
-          return false unless is_a_condition?(element)
-        end
-      end
-    else
-      raise "unexpected #{hsh.class.name} #{hsh} #{@hsh}"
-    end
-
-    true
-  end
-  private :is_a_condition?
-
-  # @return [ExtensionRequirement] First requirement found, without considering any boolean operators
-  def first_requirement(req = @hsh)
-    case req
-    when String
-      ExtensionRequirement.new(req, arch: @arch)
-    when Hash
-      if req.key?("name")
-        if req["version"].nil?
-          ExtensionRequirement.new(req["name"], arch: @arch)
-        else
-          ExtensionRequirement.new(req["name"], req["version"], arch: @arch)
-        end
-      else
-        first_requirement(req[req.keys[0]])
-      end
-    when Array
-      first_requirement(req[0])
-    else
-      raise "unexpected"
-    end
-  end
-
-  # combine all conds into one using AND
-  def self.all_of(*conds, cfg_arch:)
-    cond = ExtensionRequirementExpression.new({
-      "allOf" => conds
-    }, cfg_arch)
-
-    ExtensionRequirementExpression.new(cond.minimize, cfg_arch)
-  end
-
-  # @return [Object] Schema for this expression, with basic logic minimization
-  def minimize(hsh = @hsh)
-    case hsh
-    when Hash
-      if hsh.key?("name")
-        hsh
-      else
-        min_ary = key = nil
-        if hsh.key?("allOf")
-          min_ary = hsh["allOf"].map { |element| minimize(element) }
-          key = "allOf"
-        elsif hsh.key?("anyOf")
-          min_ary = hsh["anyOf"].map { |element| minimize(element) }
-          key = "anyOf"
-        elsif hsh.key?("oneOf")
-          min_ary = hsh["oneOf"].map { |element| minimize(element) }
-          key = "oneOf"
-        elsif hsh.key?("not")
-          min_ary = hsh.dup
-          key = "not"
-        elsif hsh.key?("if")
-          return hsh
-        end
-        min_ary = min_ary.uniq
-        if min_ary.size == 1
-          min_ary.first
-        else
-          { key => min_ary }
-        end
-      end
-    else
-      hsh
-    end
-  end
-
-  def to_rb_helper(hsh)
-    if hsh.is_a?(Hash)
-      if hsh.key?("name")
-        if hsh.key?("version")
-          if hsh["version"].is_a?(String)
-            "(yield ExtensionRequirement.new('#{hsh["name"]}', '#{hsh["version"]}', arch: @arch))"
-          elsif hsh["version"].is_a?(Array)
-            "(yield ExtensionRequirement.new('#{hsh["name"]}', #{hsh["version"].map { |v| "'#{v}'" }.join(', ')}, arch: @arch))"
-          else
-            raise "unexpected"
-          end
-        else
-          "(yield ExtensionRequirement.new('#{hsh["name"]}', arch: @arch))"
-        end
-      else
-        key = hsh.keys[0]
-
-        case key
-        when "allOf"
-          rb_str = hsh[key].map { |element| to_rb_helper(element) }.join(' && ')
-          "(#{rb_str})"
-        when "anyOf"
-          rb_str = hsh[key].map { |element| to_rb_helper(element) }.join(' || ')
-          "(#{rb_str})"
-        when "oneOf"
-          rb_str = hsh[key].map { |element| to_rb_helper(element) }.join(', ')
-          "([#{rb_str}].count(true) == 1)"
-        when "not"
-          rb_str = to_rb_helper(hsh[key])
-          "(!#{rb_str})"
-        when "if"
-          cond_rb_str = to_rb_helper(hsh["if"])
-          body_rb_str = to_rb_helper(hsh["body"])
-          "(#{body_rb_str}) if (#{cond_rb_str})"
-        else
-          raise "Unexpected"
-          "(yield #{hsh})"
-        end
-      end
-    else
-      "(yield ExtensionRequirement.new('#{hsh}', arch: @arch))"
-    end
-  end
-
-  # Given the name of a ruby array +ary_name+ containing the available objects to test,
-  # return a string that can be eval'd to determine if the objects in +ary_name+
-  # meet the Condition
-  #
-  # @param ary_name [String] Name of a ruby string in the eval binding
-  # @return [Boolean] If the condition is met
-  def to_rb
-    to_rb_helper(@hsh)
-  end
-
-  # Abstract syntax tree of the logic
-  class LogicNode
-    attr_accessor :type
-
-    TYPES = [ :term, :not, :and, :or, :if ]
-
-    def initialize(type, children, term_idx: nil)
-      raise ArgumentError, "Bad type" unless TYPES.include?(type)
-      raise ArgumentError, "Children must be an array" unless children.is_a?(Array)
-
-      raise ArgumentError, "Children must be singular" if [:term, :not].include?(type) && children.size != 1
-      raise ArgumentError, "Children must have two elements" if [:and, :or, :if].include?(type) && children.size != 2
-
-      if type == :term
-        raise ArgumentError, "Term must be an ExtensionRequirement (found #{children[0]})" unless children[0].is_a?(ExtensionRequirement)
-      else
-        raise ArgumentError, "All Children must be LogicNodes" unless children.all? { |child| child.is_a?(LogicNode) }
-      end
-
-      @type = type
-      @children = children
-
-      raise ArgumentError, "Need term_idx" if term_idx.nil? && type == :term
-      raise ArgumentError, "term_idx isn't an int" if !term_idx.is_a?(Integer) && type == :term
-
-      @term_idx = term_idx
-    end
-
-    # @return [Array<ExtensionRequirements>] The terms (leafs) of this tree
-    def terms
-      @terms ||=
-        if @type == :term
-          [@children[0]]
-        else
-          @children.map(&:terms).flatten.uniq
-        end
-    end
-
-    def eval(term_values)
-      if @type == :term
-        ext_ret = @children[0]
-        term_value = term_values.find { |tv| tv.name == ext_ret.name }
-        unless term_value.nil?
-          @children[0].satisfied_by?(term_value)
-        end
-      elsif @type == :if
-        cond_ext_ret = @children[0]
-        if cond_ext_ret.eval(term_values)
-          @children[1].eval(term_values)
-        else
-          false
-        end
-      elsif @type == :not
-        !@children[0].eval(term_values)
-      elsif @type == :and
-        @children.all? { |child| child.eval(term_values) }
-      elsif @type == :or
-        @children.any? { |child| child.eval(term_values) }
-  end
-end
-
-    def to_s
-      if @type == :term
-        "(#{@children[0].to_s})"
-      elsif @type == :not
-        "!#{@children[0]}"
-      elsif @type == :and
-        "(#{@children[0]} ^ #{@children[1]})"
-      elsif @type == :or
-        "(#{@children[0]} v #{@children[1]})"
-      elsif @type == :if
-        "(#{@children[0]} -> #{@children[1]})"
-      end
-    end
-  end
-
-  # given an extension requirement, convert it to a LogicNode term, and optionally expand it to
-  # exclude any conflicts and include any implications
-  #
-  # @param ext_req [ExtensionRequirement] An extension requirement
-  # @param expand [Boolean] Whether or not to expand the node to include conflicts / implications
-  # @return [LogicNode] Logic tree for ext_req
-  def ext_req_to_logic_node(ext_req, term_idx, expand: true)
-    n = LogicNode.new(:term, [ext_req], term_idx: term_idx[0])
-    term_idx[0] += 1
-    if expand
-      c = ext_req.extension.conflicts_condition
-      unless c.empty?
-        c = LogicNode.new(:not, [to_logic_tree(ext_req.extension.data["conflicts"], term_idx:)])
-        n = LogicNode.new(:and, [c, n])
-      end
-
-      ext_req.satisfying_versions.each do |ext_ver|
-        ext_ver.implied_by_with_condition.each do |implied_by|
-          implying_ext_ver = implied_by[:ext_ver]
-          implying_cond = implied_by[:cond]
-          implying_ext_req = ExtensionRequirement.new(implying_ext_ver.name, "= #{implying_ext_ver.version_str}", arch: @arch)
-          if implying_cond.empty?
-            # convert to an ext_req
-            n = LogicNode.new(:or, [n, ext_req_to_logic_node(implying_ext_req, term_idx)])
-          else
-            # conditional
-            # convert to an ext_req
-            cond_node = implying_cond.to_logic_tree(term_idx:, expand:)
-            cond = LogicNode.new(:if, [cond_node, ext_req_to_logic_node(implying_ext_req, term_idx)])
-            n = LogicNode.new(:or, [n, cond])
-          end
-        end
-      end
-    end
-
-    n
-  end
-
-  # convert the YAML representation of an Extension Requirement Expression into
-  # a tree of LogicNodes.
-  # Also expands any Extension Requirement to include its conflicts / implications
-  def to_logic_tree(hsh = @hsh, term_idx: [0], expand: true)
-    if hsh.is_a?(Hash)
-      if hsh.key?("name")
-        if hsh.key?("version")
-          if hsh["version"].is_a?(String)
-            ext_req_to_logic_node(ExtensionRequirement.new(hsh["name"], hsh["version"], arch: @arch), term_idx, expand:)
-          elsif hsh["version"].is_a?(Array)
-            ext_req_to_logic_node(ExtensionRequirement.new(hsh["name"], hsh["version"].map { |v| "'#{v}'" }.join(', '), arch: @arch), term_idx, expand:)
-          else
-            raise "unexpected"
-          end
-        else
-          ext_req_to_logic_node(ExtensionRequirement.new(hsh["name"], arch: @arch), term_idx, expand:)
-        end
-      else
-        key = hsh.keys[0]
-
-        case key
-        when "allOf"
-          raise "unexpected" unless hsh[key].is_a?(Array) && hsh[key].size > 1
-
-          root = LogicNode.new(:and, [to_logic_tree(hsh[key][0], term_idx:, expand:), to_logic_tree(hsh[key][1], term_idx:, expand:)])
-          (2...hsh[key].size).each do |i|
-            root = LogicNode.new(:and, [root, to_logic_tree(hsh[key][i], term_idx:, expand:)])
-          end
-          root
-        when "anyOf"
-          raise "unexpected: #{hsh}" unless hsh[key].is_a?(Array) && hsh[key].size > 1
-
-          root = LogicNode.new(:or, [to_logic_tree(hsh[key][0], term_idx:, expand:), to_logic_tree(hsh[key][1], term_idx:, expand:)])
-          (2...hsh[key].size).each do |i|
-            root = LogicNode.new(:or, [root, to_logic_tree(hsh[key][i], term_idx:, expand:)])
-          end
-          root
-        when "if"
-          raise "unexpected" unless hsh.keys.size == 2 && hsh.keys[1] == "then"
-
-          cond = to_logic_tree(hsh[key], term_idx:, expand:)
-          body = to_logic_tree(hsh["then"], term_idx:, expand:)
-          LogicNode.new(:if, [cond, body])
-        when "oneOf"
-          # expand oneOf into AND
-          roots = []
-          hsh[key].size.times do |k|
-            root =
-              if k.zero?
-                LogicNode.new(:and, [to_logic_tree(hsh[key][0], term_idx:, expand:), LogicNode.new(:not, [to_logic_tree(hsh[key][1], term_idx:, expand:)])])
-              elsif k == 1
-                LogicNode.new(:and, [LogicNode.new(:not, [to_logic_tree(hsh[key][0], term_idx:, expand:)]), to_logic_tree(hsh[key][1], term_idx:, expand:)])
-              else
-                LogicNode.new(:and, [LogicNode.new(:not, [to_logic_tree(hsh[key][0], term_idx:, expand:)]), LogicNode.new(:not, [to_logic_tree(hsh[key][1], term_idx:, expand:)])])
-              end
-            (2...hsh[key].size).each do |i|
-              root =
-                if k == i
-                  LogicNode.new(:and, [root, to_logic_tree(hsh[key][i], term_idx:, expand:)])
-                else
-                  LogicNode.new(:and, [root, LogicNode.new(:not, [to_logic_tree(hsh[key][i], term_idx:, expand:)])])
-                end
-            end
-            roots << root
-          end
-          root = LogicNode.new(:or, [roots[0], roots[1]])
-          (2...roots.size).each do |i|
-            root = LogicNode.new(:or, [root, roots[i]])
-          end
-          root
-        when "not"
-          LogicNode.new(:not, [to_logic_tree(hsh[key], term_idx:, expand:)])
-        else
-          raise "Unexpected"
-        end
-      end
-    else
-      ext_req_to_logic_node(ExtensionRequirement.new(hsh, arch: @arch), term_idx, expand:)
-    end
-  end
-
-  # convert to Negation Normal Form
-  def nnf(logic_tree)
-    if logic_tree.type == :not
-      # distribute
-      if logic_tree.children.size == 1 && logic_tree.children[0].type == :term
-        logic_tree
-      else
-        # distribute NOT
-        child = logic_tree.children[0]
-
-        if child.type == :and
-          LogicNode.new(:or, child.children.map { |child2| LogicNode.new(:not, [child2]) })
-        elsif child.type == :or
-          LogicNode.new(:and, child.children.map { |child2| LogicNode.new(:not, [child2]) })
-        elsif child.type == :xor
-          raise "TODO"
-        elsif child.type == :not
-          child
-        else
-          raise "?"
-        end
-      end
-    else
-      LogicNode.new(logic_tree.type, logic_tree.children.map { |child| nnf(child) })
-    end
-  end
-
-  # convert to Disjunctive Normal Form
-  def dnf(logic_tree)
-    logic_tree = nnf(logic_tree)
-    if logic_tree.type == :and
-      # distribute
-      if logic_tree.children.all? { |child| child.type == :term }
-        logic_tree
-      else
-        LogicTree.new(:or, logic_tree.children.map { |child| LogicTree.new(:and, dnf(child)) })
-      end
-    else
-      logic_tree
-    end
-  end
-
-  def combos_for(extension_versions)
-    ncombos = extension_versions.reduce(1) { |prod, vers| prod * (vers.size + 1) }
-    combos = []
-    ncombos.times do |i|
-      combos << []
-      extension_versions.size.times do |j|
-        m = (extension_versions[j].size + 1)
-        d = j.zero? ? 1 : extension_versions[j..0].reduce(1) { |prod, vers| prod * (vers.size + 1) }
-
-        if (i / d) % m < extension_versions[j].size
-          combos.last << extension_versions[j][(i / d) % m]
-        end
-      end
-    end
-    # get rid of any combos that can't happen because of extension conflicts
-    combos.reject do |combo|
-      combo.any? { |ext_ver1| (combo - [ext_ver1]).any? { |ext_ver2| ext_ver1.conflicts_condition.satisfied_by? { |ext_req| ext_req.satisfied_by?(ext_ver2) } } }
-    end
-  end
-
-  # @param other [ExtensionRequirementExpression] Another condition
-  # @return [Boolean] if it's possible for both to be simultaneously true
-  def compatible?(other)
-    raise ArgumentError, "Expecting a ExtensionRequirementExpression" unless other.is_a?(ExtensionRequirementExpression)
-
-    tree1 = to_logic_tree(@hsh)
-    tree2 = to_logic_tree(other.to_h)
-
-    extensions = (tree1.terms + tree2.terms).map(&:extension).uniq
-
-    extension_versions = extensions.map(&:versions)
-
-    combos = combos_for(extension_versions)
-    combos.each do |combo|
-      return true if tree1.eval(combo) && tree2.eval(combo)
-    end
-
-    # there is no combination in which both self and other can be true
-    false
-  end
-
-  # @example See if a string satisfies
-  #   cond = { "anyOf" => ["A", "B", "C"] }
-  #   string = "A"
-  #   cond.satisfied_by? { |endpoint| endpoint == string } #=> true
-  #   string = "D"
-  #   cond.satisfied_by? { |endpoint| endpoint == string } #=> false
-  #
-  # @example See if an array satisfies
-  #   cond = { "allOf" => ["A", "B", "C"] }
-  #   ary = ["A", "B", "C", "D"]
-  #   cond.satisfied_by? { |endpoint| ary.include?(endpoint) } #=> true
-  #   ary = ["A", "B"]
-  #   cond.satisfied_by? { |endpoint| ary.include?(endpoint) } #=> false
-  #
-  # @yieldparam obj [Object] An endpoint in the condition
-  # @yieldreturn [Boolean] Whether or not +obj+ is what you are looking for
-  # @return [Boolean] Whether or not the entire condition is satisfied
-  def satisfied_by?(&block)
-    raise ArgumentError, "Missing required block" unless block_given?
-
-    raise ArgumentError, "Expecting one argument to block" unless block.arity == 1
-
-    eval to_rb
-  end
-
-  # yes if:
-  #   - ext_ver affects this condition
-  #   - it is is possible for this condition to be true is ext_ver is implemented
-  def possibly_satisfied_by?(ext_ver)
-    logic_tree = to_logic_tree
-
-    return false unless logic_tree.terms.any? { |ext_req| ext_req.satisfying_versions.include?(ext_ver) }
-
-    # ok, so ext_ver affects this condition
-    # is it possible to be true with ext_ver implemented?
-    extensions = logic_tree.terms.map(&:extension).uniq
-
-    extension_versions = extensions.map(&:versions)
-
-    combos = combos_for(extension_versions)
-    combos.any? do |combo|
-      # replace ext_ver, since it doesn't change
-      logic_tree.eval(combo.map { |ev| ev.name == ext_ver.name ? ext_ver : ev })
-    end
-  end
-end
-
-class AlwaysTrueExtensionRequirementExpression
-  def to_rb = "true"
-
-  def satisfied_by? = true
-
-  def empty? = true
-
-  def compatible?(_other) = true
-
-  def to_h = {}
-  def minimize = {}
-end
-
-class AlwaysFalseExtensionRequirementExpression
-  def to_rb = "false"
-
-  def satisfied_by? = false
-
-  def empty? = true
-
-  def compatible?(_other) = false
-
-  def to_h = {}
-  def minimize = {}
-end
diff --git a/lib/arch_obj_models/extension.rb b/lib/arch_obj_models/extension.rb
index 4814a50105..07f70803bb 100644
--- a/lib/arch_obj_models/extension.rb
+++ b/lib/arch_obj_models/extension.rb
@@ -4,6 +4,7 @@
 require_relative "certifiable_obj"
 require_relative "parameter"
 require_relative "schema"
+require_relative "req_expression"
 require_relative "../presence"
 require_relative "../version"
 
diff --git a/lib/arch_obj_models/instruction.rb b/lib/arch_obj_models/instruction.rb
index 7da36a1e39..54c471a566 100644
--- a/lib/arch_obj_models/instruction.rb
+++ b/lib/arch_obj_models/instruction.rb
@@ -1,21 +1,24 @@
 # frozen_string_literal: true
+# typed: true
 
 require 'ruby-prof-flamegraph'
 
 require_relative "database_obj"
 require_relative "certifiable_obj"
 require_relative "../presence"
+require_relative "../backend_helpers"
 require "awesome_print"
 
 # model of a specific instruction in a specific base (RV32/RV64)
 class Instruction < DatabaseObject
   # Add all methods in this module to this type of database object.
   include CertifiableObject
+  include WavedromUtil
 
   def processed_wavedrom_desc(base)
     data = wavedrom_desc(base)
     processed_data = process_wavedrom(data)
-    TemplateHelpers.fix_entities(json_dump_with_hex_literals(processed_data))
+    fix_entities(json_dump_with_hex_literals(processed_data))
   end
 
   def self.ary_from_location(location_str_or_int)
@@ -187,7 +190,7 @@ def reachable_exceptions(effective_xlen)
       # pruned_ast =  pruned_operation_ast(symtab)
       # type_checked_operation_ast()
       type_checked_ast = type_checked_operation_ast( effective_xlen)
-      symtab = fill_symtab(effective_xlen, pruned_ast)
+      symtab = fill_symtab(effective_xlen, type_checked_ast)
       type_checked_ast.reachable_exceptions(symtab)
       symtab.release
     end
@@ -522,7 +525,7 @@ def extract
         elsif b.is_a?(Range)
           op = "$encoding[#{b.end}:#{b.begin}]"
           ops << op
-          so_far += b.size
+          so_far += T.must(b.size)
         end
       end
       ops << "#{@left_shift}'d0" unless @left_shift.zero?
@@ -758,7 +761,7 @@ def operation_ast
         self,
         symtab: cfg_arch.symtab,
         input_file: @data["$source"],
-        input_line: source_line("operation()")
+        input_line: source_line(["operation()"])
       )
 
       raise "unexpected #{ast.class}" unless ast.is_a?(Idl::FunctionBodyAst)
diff --git a/lib/arch_obj_models/req_expression.rb b/lib/arch_obj_models/req_expression.rb
new file mode 100644
index 0000000000..d08d4c0b42
--- /dev/null
+++ b/lib/arch_obj_models/req_expression.rb
@@ -0,0 +1,709 @@
+# frozen_string_literal: true
+# typed: true
+
+require "sorbet-runtime"
+
+class ExtensionVersion; end
+
+
+# represents a JSON Schema composition of extension requirements, e.g.:
+#
+# anyOf:
+#   - oneOf:
+#     - A
+#     - B
+#   - C
+#
+class ExtensionRequirementExpression
+  extend T::Sig
+
+  # @param composition_hash [Hash] A possibly recursive hash of "allOf", "anyOf", "oneOf", "not", "if"
+  sig { params(composition_hash: T.any(String, T::Hash[String, T.untyped]), cfg_arch: ConfiguredArchitecture).void }
+  def initialize(composition_hash, cfg_arch)
+    unless is_a_condition?(composition_hash)
+      raise ArgumentError, "Expecting a JSON schema comdition (got #{composition_hash})"
+    end
+
+    @hsh = composition_hash
+    @arch = cfg_arch
+  end
+
+  sig { returns(T.any(String, T::Hash[String, T.untyped])) }
+  def to_h = @hsh
+
+  sig { returns(T::Boolean) }
+  def empty? = false
+
+  sig { params(ver: T.untyped).returns(T::Boolean) }
+  def is_a_version_requirement(ver)
+    case ver
+    when String
+      !(ver =~ RequirementSpec::REQUIREMENT_REGEX).nil?
+    when Array
+      ver.all? { |v| v =~ RequirementSpec::REQUIREMENT_REGEX }
+    else
+      false
+    end
+  end
+  private :is_a_version_requirement
+
+  # @return [Boolean] True if the condition is a join of N terms over the same operator
+  #
+  #  A or B or C   #=> true
+  #  A and B       #=> true
+  #  A or B and C  #=> false
+  sig { returns(T::Boolean) }
+  def flat?
+    case @hsh
+    when String
+      true
+    when Hash
+      @hsh.key?("name") || @hsh[T.must(@hsh.keys.first)].all? { |child| child.is_a?(String) || (child.is_a?(Hash) && child.key?("name")) }
+    end
+  end
+
+  # @return [TYPES::Or, TYPES::And] The operator for a flat condition
+  #                     Only valid if #flat? is true
+  sig { returns(Symbol) }
+  def flat_op
+    case @hsh
+    when String
+      TYPES::Or
+    when Hash
+      @hsh.key?("name") ? TYPES::Or : { "allOf" => TYPES::And, "anyOf" => TYPES::Or }[T.must(@hsh.keys.first)]
+    end
+  end
+
+  # @return [Array<ExtensionRequirement>] The elements of the flat join
+  #                                       Only valid if #flat? is true
+  sig { returns(T::Array[ExtensionRequirement]) }
+  def flat_versions
+    case @hsh
+    when String
+      [ExtensionRequirement.new(@hsh, arch: @arch)]
+    when Hash
+      if @hsh.key?("name")
+        if @hsh.key?("version").nil?
+          [ExtensionRequirement.new(@hsh["name"], arch: @arch)]
+        else
+          [ExtensionRequirement.new(@hsh["name"], @hsh["version"], arch: @arch)]
+        end
+      else
+        @hsh[T.must(@hsh.keys.first)].map do |r|
+          if r.is_a?(String)
+            ExtensionRequirement.new(r, arch: @arch)
+          else
+            if r.key?("version").nil?
+              ExtensionRequirement.new(r["name"], arch: @arch)
+            else
+              ExtensionRequirement.new(r["name"], r["version"], arch: @arch)
+            end
+          end
+        end
+      end
+    end
+  end
+
+  sig { params(cond: T.any(String, T::Hash[String, T.untyped], T::Array[T.untyped]), indent: Integer, join: String).returns(String) }
+  def to_asciidoc(cond = @hsh, indent = 0, join: "\n")
+    case cond
+    when String
+      "#{'*' * indent}* #{cond}, version >= #{@arch.extension(cond).min_version}"
+    when Hash
+      if cond.key?("name")
+        if cond.key?("version")
+          "#{'*' * indent}* #{cond['name']}, version #{cond['version']}#{join}"
+        else
+          "#{'*' * indent}* #{cond['name']}, version >= #{@arch.extension(cond['name']).min_version}#{join}"
+        end
+      else
+        "#{'*' * indent}* #{cond.keys[0]}:#{join}" + to_asciidoc(cond[T.must(cond.keys[0])], indent + 2)
+      end
+    when Array
+      cond.map { |e| to_asciidoc(e, indent) }.join(join)
+    else
+      T.absurd(cond)
+    end
+  end
+
+  sig { params(hsh: T.any(String, T::Hash[String, T.untyped])).returns(T::Boolean) }
+  def is_a_condition?(hsh)
+    case hsh
+    when String
+      true
+    when Hash
+      if hsh.key?("name")
+        return false if hsh.size > 2
+
+        if hsh.size > 1
+          return false unless hsh.key?("version")
+
+          return false unless is_a_version_requirement(hsh["version"])
+        end
+
+      elsif hsh.key?("not")
+        return false unless hsh.size == 1
+
+        return is_a_condition?(hsh["not"])
+
+      else
+        return false unless hsh.size == 1
+
+        return false unless ["allOf", "anyOf", "oneOf", "if"].include?(hsh.keys[0])
+
+        hsh[T.must(hsh.keys[0])].each do |element|
+          return false unless is_a_condition?(element)
+        end
+      end
+    else
+      T.absurd(hsh)
+    end
+
+    true
+  end
+  private :is_a_condition?
+
+  # @return [ExtensionRequirement] First requirement found, without considering any boolean operators
+  sig { params(req: T.any(String, T::Hash[String, T.untyped], T::Array[T.untyped])).returns(ExtensionRequirement) }
+  def first_requirement(req = @hsh)
+    case req
+    when String
+      ExtensionRequirement.new(req, arch: @arch)
+    when Hash
+      if req.key?("name")
+        if req["version"].nil?
+          ExtensionRequirement.new(req["name"], arch: @arch)
+        else
+          ExtensionRequirement.new(req["name"], req["version"], arch: @arch)
+        end
+      else
+        first_requirement(req[T.must(req.keys[0])])
+      end
+    when Array
+      first_requirement(req[0])
+    else
+      T.absurd(req)
+    end
+  end
+
+  # combine all conds into one using AND
+  sig { params(conds: T::Array[T.untyped], cfg_arch: ConfiguredArchitecture).void }
+  def self.all_of(*conds, cfg_arch:)
+    cond = ExtensionRequirementExpression.new({
+      "allOf" => conds
+    }, cfg_arch)
+
+    ExtensionRequirementExpression.new(cond.minimize, cfg_arch)
+  end
+
+  # @return [Object] Schema for this expression, with basic logic minimization
+  sig { params(hsh: T.any(String, T::Hash[String, T.untyped])).returns(T.any(String, T::Hash[String, T.untyped])) }
+  def minimize(hsh = @hsh)
+    case hsh
+    when Hash
+      if hsh.key?("name")
+        hsh
+      else
+        min_ary = key = nil
+        if hsh.key?("allOf")
+          min_ary = hsh["allOf"].map { |element| minimize(element) }
+          key = "allOf"
+        elsif hsh.key?("anyOf")
+          min_ary = hsh["anyOf"].map { |element| minimize(element) }
+          key = "anyOf"
+        elsif hsh.key?("oneOf")
+          min_ary = hsh["oneOf"].map { |element| minimize(element) }
+          key = "oneOf"
+        elsif hsh.key?("not")
+          min_ary = hsh.dup
+          key = "not"
+        elsif hsh.key?("if")
+          return hsh
+        end
+        min_ary = min_ary.uniq
+        if min_ary.size == 1
+          min_ary.first
+        else
+          { key => min_ary }
+        end
+      end
+    else
+      hsh
+    end
+  end
+
+  sig { params(hsh: T.any(String, T::Hash[String, T.untyped])).returns(String) }
+  def to_rb_helper(hsh)
+    if hsh.is_a?(Hash)
+      if hsh.key?("name")
+        if hsh.key?("version")
+          if hsh["version"].is_a?(String)
+            "(yield ExtensionRequirement.new('#{hsh["name"]}', '#{hsh["version"]}', arch: @arch))"
+          elsif hsh["version"].is_a?(Array)
+            "(yield ExtensionRequirement.new('#{hsh["name"]}', #{hsh["version"].map { |v| "'#{v}'" }.join(', ')}, arch: @arch))"
+          else
+            raise "unexpected"
+          end
+        else
+          "(yield ExtensionRequirement.new('#{hsh["name"]}', arch: @arch))"
+        end
+      else
+        key = hsh.keys[0]
+
+        case key
+        when "allOf"
+          rb_str = hsh["allOf"].map { |element| to_rb_helper(element) }.join(' && ')
+          "(#{rb_str})"
+        when "anyOf"
+          rb_str = hsh["anyOf"].map { |element| to_rb_helper(element) }.join(' || ')
+          "(#{rb_str})"
+        when "oneOf"
+          rb_str = hsh["oneOf"].map { |element| to_rb_helper(element) }.join(', ')
+          "([#{rb_str}].count(true) == 1)"
+        when "not"
+          rb_str = to_rb_helper(hsh["not"])
+          "(!#{rb_str})"
+        when "if"
+          cond_rb_str = to_rb_helper(hsh["if"])
+          body_rb_str = to_rb_helper(hsh["body"])
+          "(#{body_rb_str}) if (#{cond_rb_str})"
+        else
+          raise "Unexpected"
+          # "(yield #{hsh})"
+        end
+      end
+    else
+      "(yield ExtensionRequirement.new('#{hsh}', arch: @arch))"
+    end
+  end
+
+  # Given the name of a ruby array +ary_name+ containing the available objects to test,
+  # return a string that can be eval'd to determine if the objects in +ary_name+
+  # meet the Condition
+  #
+  # @param ary_name [String] Name of a ruby string in the eval binding
+  # @return [Boolean] If the condition is met
+  sig { returns(String) }
+  def to_rb
+    to_rb_helper(@hsh)
+  end
+
+  class TYPES < T::Enum
+    enums do
+      Term = new
+      Not = new
+      And = new
+      Or = new
+      If = new
+    end
+  end
+
+  # Abstract syntax tree of the logic
+  class LogicNode
+    extend T::Sig
+
+    sig { returns(TYPES) }
+    attr_accessor :type
+
+    sig { params(type: TYPES, children: T::Array[T.any(LogicNode, ExtensionRequirement)], term_idx: T.nilable(Integer)).void }
+    def initialize(type, children, term_idx: nil)
+      raise ArgumentError, "Children must be singular" if [TYPES::Term, TYPES::Not].include?(type) && children.size != 1
+      raise ArgumentError, "Children must have two elements" if [TYPES::And, TYPES::Or, TYPES::If].include?(type) && children.size != 2
+
+      if type == TYPES::Term
+        raise ArgumentError, "Term must be an ExtensionRequirement (found #{children[0]})" unless children[0].is_a?(ExtensionRequirement)
+      else
+        raise ArgumentError, "All Children must be LogicNodes" unless children.all? { |child| child.is_a?(LogicNode) }
+      end
+
+      @type = type
+      @children = children
+
+      raise ArgumentError, "Need term_idx" if term_idx.nil? && type == TYPES::Term
+      raise ArgumentError, "term_idx isn't an int" if !term_idx.is_a?(Integer) && type == TYPES::Term
+
+      @term_idx = term_idx
+    end
+
+    # @return [Array<ExtensionRequirements>] The terms (leafs) of this tree
+    sig { returns(T::Array[ExtensionRequirement]) }
+    def terms
+      @terms ||=
+        if @type == TYPES::Term
+          [@children[0]]
+        else
+          @children.map { |child| T.cast(child, LogicNode).terms }.flatten.uniq
+        end
+    end
+
+    sig { params(term_values: T::Array[ExtensionVersion]).returns(T::Boolean) }
+    def eval(term_values)
+      if @type == TYPES::Term
+        ext_req = T.cast(@children[0], ExtensionRequirement)
+        term_value = term_values.find { |tv| tv.name == ext_req.name }
+        return false if term_value.nil?
+
+        ext_req.satisfied_by?(term_value)
+      elsif @type == TYPES::If
+        cond_ext_ret = T.cast(@children[0], LogicNode)
+        if cond_ext_ret.eval(term_values)
+          T.cast(@children[1], LogicNode).eval(term_values)
+        else
+          false
+        end
+      elsif @type == TYPES::Not
+        !T.cast(@children[0], LogicNode).eval(term_values)
+      elsif @type == TYPES::And
+        @children.all? { |child| T.cast(child, LogicNode).eval(term_values) }
+      elsif @type == TYPES::Or
+        @children.any? { |child| T.cast(child, LogicNode).eval(term_values) }
+      end
+    end
+
+    sig { returns(String) }
+    def to_s
+      if @type == TYPES::Term
+        "(#{@children[0].to_s})"
+      elsif @type == TYPES::Not
+        "!#{@children[0]}"
+      elsif @type == TYPES::And
+        "(#{@children[0]} ^ #{@children[1]})"
+      elsif @type == TYPES::Or
+        "(#{@children[0]} v #{@children[1]})"
+      elsif @type == TYPES::If
+        "(#{@children[0]} -> #{@children[1]})"
+      else
+        T.absurd(@type)
+      end
+    end
+  end
+
+  # given an extension requirement, convert it to a LogicNode term, and optionally expand it to
+  # exclude any conflicts and include any implications
+  #
+  # @param ext_req [ExtensionRequirement] An extension requirement
+  # @param expand [Boolean] Whether or not to expand the node to include conflicts / implications
+  # @return [LogicNode] Logic tree for ext_req
+  sig { params(ext_req: ExtensionRequirement, term_idx: T::Array[Integer], expand: T::Boolean).returns(LogicNode) }
+  def ext_req_to_logic_node(ext_req, term_idx, expand: true)
+    n = LogicNode.new(TYPES::Term, [ext_req], term_idx: term_idx[0])
+    term_idx[0] = T.must(term_idx[0]) + 1
+    if expand
+      c = ext_req.extension.conflicts_condition
+      unless c.empty?
+        c = LogicNode.new(TYPES::Not, [to_logic_tree(ext_req.extension.data["conflicts"], term_idx:)])
+        n = LogicNode.new(TYPES::And, [c, n])
+      end
+
+      ext_req.satisfying_versions.each do |ext_ver|
+        ext_ver.implied_by_with_condition.each do |implied_by|
+          implying_ext_ver = implied_by[:ext_ver]
+          implying_cond = implied_by[:cond]
+          implying_ext_req = ExtensionRequirement.new(implying_ext_ver.name, "= #{implying_ext_ver.version_str}", arch: @arch)
+          if implying_cond.empty?
+            # convert to an ext_req
+            n = LogicNode.new(TYPES::Or, [n, ext_req_to_logic_node(implying_ext_req, term_idx)])
+          else
+            # conditional
+            # convert to an ext_req
+            cond_node = implying_cond.to_logic_tree(term_idx:, expand:)
+            cond = LogicNode.new(TYPES::If, [cond_node, ext_req_to_logic_node(implying_ext_req, term_idx)])
+            n = LogicNode.new(TYPES::Or, [n, cond])
+          end
+        end
+      end
+    end
+
+    n
+  end
+
+  # convert the YAML representation of an Extension Requirement Expression into
+  # a tree of LogicNodes.
+  # Also expands any Extension Requirement to include its conflicts / implications
+  sig { params(hsh: T.any(String, T::Hash[String, T.untyped]), term_idx: T::Array[Integer], expand: T::Boolean).returns(LogicNode) }
+  def to_logic_tree(hsh = @hsh, term_idx: [0], expand: true)
+    root = T.let(nil, T.nilable(LogicNode))
+
+    if hsh.is_a?(Hash)
+      if hsh.key?("name")
+        if hsh.key?("version")
+          if hsh["version"].is_a?(String)
+            ext_req_to_logic_node(ExtensionRequirement.new(hsh["name"], hsh["version"], arch: @arch), term_idx, expand:)
+          elsif hsh["version"].is_a?(Array)
+            ext_req_to_logic_node(ExtensionRequirement.new(hsh["name"], hsh["version"].map { |v| "'#{v}'" }.join(', '), arch: @arch), term_idx, expand:)
+          else
+            raise "unexpected"
+          end
+        else
+          ext_req_to_logic_node(ExtensionRequirement.new(hsh["name"], arch: @arch), term_idx, expand:)
+        end
+      else
+        key = hsh.keys[0]
+
+        case key
+        when "allOf"
+          raise "unexpected" unless hsh["allOf"].is_a?(Array) && hsh["allOf"].size > 1
+
+          root = LogicNode.new(TYPES::And, [to_logic_tree(hsh["allOf"][0], term_idx:, expand:), to_logic_tree(hsh["allOf"][1], term_idx:, expand:)])
+          (2...hsh["allOf"].size).each do |i|
+            root = LogicNode.new(TYPES::And, [root, to_logic_tree(hsh["allOf"][i], term_idx:, expand:)])
+          end
+          root
+        when "anyOf"
+          raise "unexpected: #{hsh}" unless hsh["anyOf"].is_a?(Array) && hsh["anyOf"].size > 1
+
+          root = LogicNode.new(TYPES::Or, [to_logic_tree(hsh["anyOf"][0], term_idx:, expand:), to_logic_tree(hsh["anyOf"][1], term_idx:, expand:)])
+          (2...hsh["anyOf"].size).each do |i|
+            root = LogicNode.new(TYPES::Or, [root, to_logic_tree(hsh["anyOf"][i], term_idx:, expand:)])
+          end
+          root
+        when "if"
+          raise "unexpected" unless hsh.keys.size == 2 && hsh.keys[1] == "then"
+
+          cond = to_logic_tree(hsh["if"], term_idx:, expand:)
+          body = to_logic_tree(hsh["then"], term_idx:, expand:)
+          LogicNode.new(TYPES::If, [cond, body])
+        when "oneOf"
+          # expand oneOf into AND
+          roots = T.let([], T::Array[LogicNode])
+          raise "unexpected" if hsh["oneOf"].size < 2
+
+          hsh["oneOf"].size.times do |k|
+            root =
+              if k.zero?
+                LogicNode.new(TYPES::And, [to_logic_tree(hsh["oneOf"][0], term_idx:, expand:), LogicNode.new(TYPES::Not, [to_logic_tree(hsh["oneOf"][1], term_idx:, expand:)])])
+              elsif k == 1
+                LogicNode.new(TYPES::And, [LogicNode.new(TYPES::Not, [to_logic_tree(hsh["oneOf"][0], term_idx:, expand:)]), to_logic_tree(hsh["oneOf"][1], term_idx:, expand:)])
+              else
+                LogicNode.new(TYPES::And, [LogicNode.new(TYPES::Not, [to_logic_tree(hsh["oneOf"][0], term_idx:, expand:)]), LogicNode.new(TYPES::Not, [to_logic_tree(hsh["oneOf"][1], term_idx:, expand:)])])
+              end
+            (2...hsh["oneOf"].size).each do |i|
+              root =
+                if k == i
+                  LogicNode.new(TYPES::And, [root, to_logic_tree(hsh["oneOf"][i], term_idx:, expand:)])
+                else
+                  LogicNode.new(TYPES::And, [root, LogicNode.new(TYPES::Not, [to_logic_tree(hsh["oneOf"][i], term_idx:, expand:)])])
+                end
+             end
+            roots << root
+          end
+          root = LogicNode.new(TYPES::Or, [T.must(roots[0]), T.must(roots[1])])
+          (2...roots.size).each do |i|
+            root = LogicNode.new(TYPES::Or, [root, T.must(roots[i])])
+          end
+          root
+        when "not"
+          LogicNode.new(TYPES::Not, [to_logic_tree(hsh["not"], term_idx:, expand:)])
+        else
+          raise "Unexpected"
+        end
+      end
+    else
+      ext_req_to_logic_node(ExtensionRequirement.new(hsh, arch: @arch), term_idx, expand:)
+    end
+  end
+
+  sig { params(extension_versions: T::Array[T::Array[ExtensionVersion]]).returns(T::Array[T::Array[ExtensionVersion]])}
+  def combos_for(extension_versions)
+    ncombos = extension_versions.reduce(1) { |prod, vers| prod * (vers.size + 1) }
+    combos = T.let([], T::Array[T::Array[ExtensionVersion]])
+    ncombos.times do |i|
+      combos << []
+      extension_versions.size.times do |j|
+        m = (T.must(extension_versions[j]).size + 1)
+        d = j.zero? ? 1 : T.must(extension_versions[j..0]).reduce(1) { |prod, vers| prod * (vers.size + 1) }
+
+        if (i / d) % m < T.must(extension_versions[j]).size
+          T.must(combos.last) << T.must(T.must(extension_versions[j])[(i / d) % m])
+        end
+      end
+    end
+    # get rid of any combos that can't happen because of extension conflicts
+    combos.reject do |combo|
+      combo.any? { |ext_ver1| (combo - [ext_ver1]).any? { |ext_ver2| ext_ver1.conflicts_condition.satisfied_by? { |ext_req| ext_req.satisfied_by?(ext_ver2) } } }
+    end
+  end
+
+  # @param other [ExtensionRequirementExpression] Another condition
+  # @return [Boolean] if it's possible for both to be simultaneously true
+  sig { params(other: ExtensionRequirementExpression).returns(T::Boolean) }
+  def compatible?(other)
+    tree1 = to_logic_tree(@hsh)
+    tree2 = to_logic_tree(other.to_h)
+
+    extensions = (tree1.terms + tree2.terms).map(&:extension).uniq
+
+    extension_versions = extensions.map(&:versions)
+
+    combos = combos_for(extension_versions)
+    combos.each do |combo|
+      return true if tree1.eval(combo) && tree2.eval(combo)
+    end
+
+    # there is no combination in which both self and other can be true
+    false
+  end
+
+  # @example See if a string satisfies
+  #   cond = { "anyOf" => ["A", "B", "C"] }
+  #   string = "A"
+  #   cond.satisfied_by? { |endpoint| endpoint == string } #=> true
+  #   string = "D"
+  #   cond.satisfied_by? { |endpoint| endpoint == string } #=> false
+  #
+  # @example See if an array satisfies
+  #   cond = { "allOf" => ["A", "B", "C"] }
+  #   ary = ["A", "B", "C", "D"]
+  #   cond.satisfied_by? { |endpoint| ary.include?(endpoint) } #=> true
+  #   ary = ["A", "B"]
+  #   cond.satisfied_by? { |endpoint| ary.include?(endpoint) } #=> false
+  #
+  # @yieldparam obj [Object] An endpoint in the condition
+  # @yieldreturn [Boolean] Whether or not +obj+ is what you are looking for
+  # @return [Boolean] Whether or not the entire condition is satisfied
+  sig { params(block: T.proc.params(arg0: ExtensionRequirement).returns(T::Boolean)).returns(T::Boolean) }
+  def satisfied_by?(&block)
+    raise ArgumentError, "Expecting one argument to block" unless block.arity == 1
+
+    eval to_rb
+  end
+
+  # yes if:
+  #   - ext_ver affects this condition
+  #   - it is is possible for this condition to be true is ext_ver is implemented
+  sig { params(ext_ver: ExtensionVersion).returns(T::Boolean) }
+  def possibly_satisfied_by?(ext_ver)
+    logic_tree = to_logic_tree
+
+    return false unless logic_tree.terms.any? { |ext_req| ext_req.satisfying_versions.include?(ext_ver) }
+
+    # ok, so ext_ver affects this condition
+    # is it possible to be true with ext_ver implemented?
+    extensions = logic_tree.terms.map(&:extension).uniq
+
+    extension_versions = extensions.map(&:versions)
+
+    combos = combos_for(extension_versions)
+    combos.any? do |combo|
+      # replace ext_ver, since it doesn't change
+      logic_tree.eval(combo.map { |ev| ev.name == ext_ver.name ? ext_ver : ev })
+    end
+  end
+end
+
+class AlwaysTrueExtensionRequirementExpression
+  extend T::Sig
+
+  sig { returns(String) }
+  def to_rb = "true"
+
+  sig { returns(T::Boolean) }
+  def satisfied_by? = true
+
+  sig { returns(T::Boolean) }
+  def empty? = true
+
+  sig { params(_other: T.untyped).returns(T::Boolean) }
+  def compatible?(_other) = true
+
+  sig { returns(T::Hash[T.untyped, T.untyped]) }
+  def to_h = {}
+
+  sig { returns(T::Hash[T.untyped, T.untyped]) }
+  def minimize = {}
+end
+
+class AlwaysFalseExtensionRequirementExpression
+  extend T::Sig
+
+  sig { returns(String) }
+  def to_rb = "false"
+
+  sig { returns(T::Boolean) }
+  def satisfied_by? = false
+
+  sig { returns(T::Boolean) }
+  def empty? = true
+
+  sig { params(_other: T.untyped).returns(T::Boolean) }
+  def compatible?(_other) = false
+
+  sig { returns(T::Hash[T.untyped, T.untyped]) }
+  def to_h = {}
+
+  sig { returns(T::Hash[T.untyped, T.untyped]) }
+  def minimize = {}
+end
+
+
+
+
+# represents an `implies:` entry for an extension
+# which is a list of extension versions, zero or more of which
+# may be conditional (via an ExtensionRequirementExpression)
+class ConditionalExtensionVersionList
+  extend T::Sig
+
+  class ConditionalExtensionVersion < T::Struct
+    prop :ext_ver, ExtensionVersion
+    prop :cond, T.any(ExtensionRequirementExpression, AlwaysFalseExtensionRequirementExpression, AlwaysTrueExtensionRequirementExpression)
+  end
+
+  YamlExtensionWithVersion = T.type_alias { T::Hash[String, String] }
+  sig { params(data: T.any(NilClass, T::Array[YamlExtensionWithVersion], T::Hash[String, T.any(String, T::Hash[String, String])]), cfg_arch: ConfiguredArchitecture).void }
+  def initialize(data, cfg_arch)
+    @data = data
+    @cfg_arch = cfg_arch
+  end
+
+  sig { returns(T::Boolean) }
+  def empty? = @data.nil? || @data.empty?
+
+  sig { returns(Integer) }
+  def size = empty? ? 0 : eval.size
+
+  sig { params(block: T.proc.params(arg0: ConditionalExtensionVersion).void).void }
+  def each(&block)
+    eval.each(&block)
+  end
+
+  sig { params(block: T.proc.params(arg0: ConditionalExtensionVersion).returns(T.untyped)).returns(T::Array[T.untyped]) }
+  def map(&block)
+    eval.map(&block)
+  end
+
+  # Returns array of ExtensionVersions, along with a condition under which it is in the list
+  #
+  # @example
+  #   list.eval #=> [{ :ext_ver => ExtensionVersion.new(:A, "2.1.0"), :cond => ExtensionRequirementExpression.new(...) }]
+  #
+  # @return [Array<Hash{Symbol => ExtensionVersion, ExtensionRequirementExpression}>]
+  #           The extension versions in the list after evaluation, and the condition under which it applies
+  sig { returns(T::Array[ConditionalExtensionVersion]) }
+  def eval
+    result = []
+    data = T.let({}, T::Hash[String, String])
+    if @data.is_a?(Hash)
+      data = T.cast(@data, T::Hash[String, String])
+      result << { ext_ver: entry_to_ext_ver(data), cond: AlwaysTrueExtensionRequirementExpression.new }
+    else
+      T.must(@data).each do |elem|
+        if elem.keys[0] == "if"
+          cond_expr = ExtensionRequirementExpression.new(T.must(elem["if"]), @cfg_arch)
+          data = T.cast(elem["then"], T::Hash[String, String])
+          result << { ext_ver: entry_to_ext_ver(data), cond: cond_expr }
+        else
+          result << { ext_ver: entry_to_ext_ver(elem), cond: AlwaysTrueExtensionRequirementExpression.new }
+        end
+      end
+    end
+    result
+  end
+  alias to_a eval
+
+  sig { params(entry: T::Hash[String, String]).returns(ExtensionVersion) }
+  def entry_to_ext_ver(entry)
+    ExtensionVersion.new(entry["name"], entry["version"], @cfg_arch, fail_if_version_does_not_exist: true)
+  end
+  private :entry_to_ext_ver
+end
diff --git a/lib/architecture.rbi b/lib/architecture.rbi
new file mode 100644
index 0000000000..cc290ce4b9
--- /dev/null
+++ b/lib/architecture.rbi
@@ -0,0 +1,21 @@
+# typed: true
+
+# since we generate Architecture methods with metaprogramming, we need an explicit interface for
+# Sorbet
+
+class Architecture
+  sig { params(name: String).returns(Csr) }
+  def csr(name); end
+
+  sig { returns(T::Array[Csr]) }
+  def csrs; end
+
+  sig { returns(T::Array[Instruction]) }
+  def instructions; end
+
+  sig { params(name: String).returns(Instruction) }
+  def instruction(name); end
+
+  sig { params(name: String).returns(Extension) }
+  def extension(name); end
+end
diff --git a/lib/backend_helpers.rb b/lib/backend_helpers.rb
index 5726b4e799..7c6f1221c0 100644
--- a/lib/backend_helpers.rb
+++ b/lib/backend_helpers.rb
@@ -16,6 +16,75 @@ class String
   def sanitize = String.new(self).gsub(".", "_").gsub("&", "_and_")
 end
 
+module WavedromUtil
+  def fix_entities(text)
+    text.to_s.gsub("&ne;", "≠")
+             .gsub("&pm;", "±")
+             .gsub("-&infin;", "−∞")
+             .gsub("+&infin;", "+∞")
+  end
+
+  # Custom JSON converter for wavedrom that handles hexadecimal literals
+  def json_dump_with_hex_literals(data)
+    # First convert to standard JSON
+    json_string = JSON.dump(data)
+
+    # Replace string hex values with actual hex literals
+    json_string.gsub(/"0x([0-9a-fA-F]+)"/) do |match|
+      # Remove the quotes, leaving just the hex literal
+      "0x#{$1}"
+    end.gsub(/"name":/, '"name": ') # Add space after colon for name field
+  end
+
+  # Helper to process wavedrom data
+  def process_wavedrom(json_data)
+    result = json_data.dup
+
+    # Process reg array if it exists
+    if result["reg"].is_a?(Array)
+      result["reg"].each do |item|
+        # For fields that are likely opcodes or immediates (type 2)
+        if item["type"] == 2
+
+          # Convert to number first (if it's a string)
+          if item["name"].is_a?(String)
+            if item["name"].start_with?("0x")
+              # Already hexadecimal
+              numeric_value = item["name"].to_i(16)
+            elsif item["name"] =~ /^[01]+$/
+              # Binary string without prefix
+              numeric_value = item["name"].to_i(2)
+            elsif item["name"] =~ /^\d+$/
+              # Decimal
+              numeric_value = item["name"].to_i
+            else
+              # Not a number, leave it alone
+              next
+            end
+          else
+            # Already a number
+            numeric_value = item["name"]
+          end
+
+          # Convert to hexadecimal string
+          hex_str = numeric_value.to_s(16).downcase
+
+          # Set the name to a specially formatted string that will be converted
+          # to a hex literal in our custom JSON converter
+          item["name"] = "0x" + hex_str
+        end
+
+        # Ensure bits is a number
+        if item["bits"].is_a?(String) && item["bits"] =~ /^\d+$/
+          item["bits"] = item["bits"].to_i
+        end
+      end
+    end
+
+    result
+  end
+end
+
 # This module is included in the CfgArch and Design classes so its methods are available to be called directly
 # from them without having to prefix a method with the module name.
 module TemplateHelpers
@@ -170,72 +239,7 @@ def check_no_periods(s)
   end
   private :check_no_periods
 
-  def fix_entities(text)
-    text.to_s.gsub("&ne;", "≠")
-             .gsub("&pm;", "±")
-             .gsub("-&infin;", "−∞")
-             .gsub("+&infin;", "+∞")
-  end
-
-  # Custom JSON converter for wavedrom that handles hexadecimal literals
-  def json_dump_with_hex_literals(data)
-    # First convert to standard JSON
-    json_string = JSON.dump(data)
-
-    # Replace string hex values with actual hex literals
-    json_string.gsub(/"0x([0-9a-fA-F]+)"/) do |match|
-      # Remove the quotes, leaving just the hex literal
-      "0x#{$1}"
-    end.gsub(/"name":/, '"name": ') # Add space after colon for name field
-  end
-
-  # Helper to process wavedrom data
-  def process_wavedrom(json_data)
-    result = json_data.dup
-
-    # Process reg array if it exists
-    if result["reg"].is_a?(Array)
-      result["reg"].each do |item|
-        # For fields that are likely opcodes or immediates (type 2)
-        if item["type"] == 2
-
-          # Convert to number first (if it's a string)
-          if item["name"].is_a?(String)
-            if item["name"].start_with?("0x")
-              # Already hexadecimal
-              numeric_value = item["name"].to_i(16)
-            elsif item["name"] =~ /^[01]+$/
-              # Binary string without prefix
-              numeric_value = item["name"].to_i(2)
-            elsif item["name"] =~ /^\d+$/
-              # Decimal
-              numeric_value = item["name"].to_i
-            else
-              # Not a number, leave it alone
-              next
-            end
-          else
-            # Already a number
-            numeric_value = item["name"]
-          end
-
-          # Convert to hexadecimal string
-          hex_str = numeric_value.to_s(16).downcase
-
-          # Set the name to a specially formatted string that will be converted
-          # to a hex literal in our custom JSON converter
-          item["name"] = "0x" + hex_str
-        end
-
-        # Ensure bits is a number
-        if item["bits"].is_a?(String) && item["bits"] =~ /^\d+$/
-          item["bits"] = item["bits"].to_i
-        end
-      end
-    end
-
-    result
-  end
+  include WavedromUtil
 end
 
 # Utilities for a backend to generate AsciiDoc.
diff --git a/lib/config.rb b/lib/config.rb
index 8ba36219c1..e4f325c50e 100644
--- a/lib/config.rb
+++ b/lib/config.rb
@@ -320,7 +320,7 @@ def initialize(portfolio_grp)
     @portfolio_grp = portfolio_grp
 
     portfolio_grp.portfolios.each do |portfolio|
-      raise "Portfolio #{portfolio.name} shouldn't have a non-nil cfg_arch member" unless portfolio.cfg_arch.nil?
+      raise "Portfolio #{portfolio.name} shouldn't have a non-nil cfg_arch member" if portfolio.cfg_arch?
       raise "Portfolio #{portfolio.name} shouldn't have a an arch member of type ConfiguredArchitecture" if portfolio.arch.is_a?(ConfiguredArchitecture)
     end
   end