IntervalAnalysis.h

Go to the documentation of this file.

//===-- IntervalAnalysis.h --------------------------------------*- C++ -*-===//
//
// Part of the LLZK Project, under the Apache License v2.0.
// See LICENSE.txt for license information.
// Copyright 2025 Veridise Inc.
// SPDX-License-Identifier: Apache-2.0
//
//===----------------------------------------------------------------------===//
 
#pragma once
 
#include "llzk/Analysis/AbstractLatticeValue.h"
#include "llzk/Analysis/AnalysisWrappers.h"
#include "llzk/Analysis/ConstraintDependencyGraph.h"
#include "llzk/Analysis/DenseAnalysis.h"
#include "llzk/Dialect/Array/IR/Ops.h"
#include "llzk/Dialect/Bool/IR/Ops.h"
#include "llzk/Dialect/Cast/IR/Ops.h"
#include "llzk/Dialect/Constrain/IR/Ops.h"
#include "llzk/Dialect/Felt/IR/Ops.h"
#include "llzk/Dialect/Function/IR/Ops.h"
#include "llzk/Dialect/Global/IR/Ops.h"
#include "llzk/Dialect/Polymorphic/IR/Ops.h"
#include "llzk/Util/APIntHelper.h"
#include "llzk/Util/Compare.h"
 
#include <mlir/IR/BuiltinOps.h>
#include <mlir/Pass/AnalysisManager.h>
#include <mlir/Support/LLVM.h>
 
#include <llvm/ADT/MapVector.h>
#include <llvm/Support/SMTAPI.h>
 
#include <array>
#include <mutex>
 
namespace llzk {
 
/* Field */

class Field {
public:
  static const Field &getField(const char *fieldName);
 
  Field() = delete;
  Field(const Field &) = default;
  Field(Field &&) = default;
  Field &operator=(const Field &) = default;

  llvm::APSInt prime() const { return primeMod; }

  llvm::APSInt half() const { return halfPrime; }

  inline llvm::APSInt felt(unsigned i) const { return reduce(i); }

  inline llvm::APSInt zero() const { return felt(0); }

  inline llvm::APSInt one() const { return felt(1); }

  inline llvm::APSInt maxVal() const { return prime() - one(); }

  llvm::APSInt reduce(llvm::APSInt i) const;
  llvm::APSInt reduce(unsigned i) const;
 
  inline unsigned bitWidth() const { return primeMod.getBitWidth(); }

  llvm::SMTExprRef createSymbol(llvm::SMTSolverRef solver, const char *name) const {
    return solver->mkSymbol(name, solver->getBitvectorSort(bitWidth()));
  }
 
  friend bool operator==(const Field &lhs, const Field &rhs) {
    return lhs.primeMod == rhs.primeMod;
  }
 
private:
  Field(std::string_view primeStr);
  Field(llvm::APSInt p, llvm::APSInt h) : primeMod(p), halfPrime(h) {}
 
  llvm::APSInt primeMod, halfPrime;
 
  static void initKnownFields(llvm::DenseMap<llvm::StringRef, Field> &knownFields);
};
 
/* UnreducedInterval */
 
class Interval;

class UnreducedInterval {
public:
  static size_t getMaxBitWidth(const UnreducedInterval &lhs, const UnreducedInterval &rhs) {
    return std::max(
        {lhs.a.getBitWidth(), lhs.b.getBitWidth(), rhs.a.getBitWidth(), rhs.b.getBitWidth()}
    );
  }
 
  UnreducedInterval(llvm::APSInt x, llvm::APSInt y) : a(x), b(y) {}
  UnreducedInterval(llvm::APInt x, llvm::APInt y) : a(x), b(y) {}
  UnreducedInterval(uint64_t x, uint64_t y) : a(llvm::APInt(64, x)), b(llvm::APInt(64, y)) {}
 
  /* Operations */

  Interval reduce(const Field &field) const;

  UnreducedInterval intersect(const UnreducedInterval &rhs) const;

  UnreducedInterval doUnion(const UnreducedInterval &rhs) const;

  UnreducedInterval computeLTPart(const UnreducedInterval &rhs) const;

  UnreducedInterval computeLEPart(const UnreducedInterval &rhs) const;

  UnreducedInterval computeGTPart(const UnreducedInterval &rhs) const;

  UnreducedInterval computeGEPart(const UnreducedInterval &rhs) const;
 
  UnreducedInterval operator-() const;
  friend UnreducedInterval operator+(const UnreducedInterval &lhs, const UnreducedInterval &rhs);
  friend UnreducedInterval operator-(const UnreducedInterval &lhs, const UnreducedInterval &rhs);
  friend UnreducedInterval operator*(const UnreducedInterval &lhs, const UnreducedInterval &rhs);
 
  /* Comparisons */
 
  bool overlaps(const UnreducedInterval &rhs) const;
 
  friend std::strong_ordering
  operator<=>(const UnreducedInterval &lhs, const UnreducedInterval &rhs);
 
  friend bool operator==(const UnreducedInterval &lhs, const UnreducedInterval &rhs) {
    return std::is_eq(lhs <=> rhs);
  };
 
  /* Utility */
  llvm::APSInt getLHS() const { return a; }
  llvm::APSInt getRHS() const { return b; }

  llvm::APSInt width() const;

  bool isEmpty() const;
 
  bool isNotEmpty() const { return !isEmpty(); }
 
  void print(llvm::raw_ostream &os) const { os << "Unreduced:[ " << a << ", " << b << " ]"; }
 
  friend llvm::raw_ostream &operator<<(llvm::raw_ostream &os, const UnreducedInterval &ui) {
    ui.print(os);
    return os;
  }
 
private:
  llvm::APSInt a, b;
};
 
/* Interval */

class Interval {
public:
  enum class Type { TypeA = 0, TypeB, TypeC, TypeF, Empty, Degenerate, Entire };
  static constexpr std::array<std::string_view, 7> TypeNames = {"TypeA", "TypeB", "TypeC",
                                                                "TypeF", "Empty", "Degenerate",
                                                                "Entire"};
 
  static std::string_view TypeName(Type t) { return TypeNames.at(static_cast<size_t>(t)); }
 
  /* Static constructors for convenience */
 
  static Interval Empty(const Field &f) { return Interval(Type::Empty, f); }
 
  static Interval Degenerate(const Field &f, llvm::APSInt val) {
    return Interval(Type::Degenerate, f, val, val);
  }
 
  static Interval Boolean(const Field &f) { return Interval::TypeA(f, f.zero(), f.one()); }
 
  static Interval Entire(const Field &f) { return Interval(Type::Entire, f); }
 
  static Interval TypeA(const Field &f, llvm::APSInt a, llvm::APSInt b) {
    return Interval(Type::TypeA, f, a, b);
  }
 
  static Interval TypeB(const Field &f, llvm::APSInt a, llvm::APSInt b) {
    return Interval(Type::TypeB, f, a, b);
  }
 
  static Interval TypeC(const Field &f, llvm::APSInt a, llvm::APSInt b) {
    return Interval(Type::TypeC, f, a, b);
  }
 
  static Interval TypeF(const Field &f, llvm::APSInt a, llvm::APSInt b) {
    return Interval(Type::TypeF, f, a, b);
  }

  Interval() : Interval(Type::Entire, Field::getField("bn128")) {}

  UnreducedInterval toUnreduced() const;

  UnreducedInterval firstUnreduced() const;

  UnreducedInterval secondUnreduced() const;
 
  template <std::pair<Type, Type>... Pairs>
  static bool areOneOf(const Interval &a, const Interval &b) {
    return ((a.ty == std::get<0>(Pairs) && b.ty == std::get<1>(Pairs)) || ...);
  }

  Interval join(const Interval &rhs) const;

  Interval intersect(const Interval &rhs) const;

  Interval difference(const Interval &other) const;
 
  /* arithmetic ops */
 
  Interval operator-() const;
  friend Interval operator+(const Interval &lhs, const Interval &rhs);
  friend Interval operator-(const Interval &lhs, const Interval &rhs);
  friend Interval operator*(const Interval &lhs, const Interval &rhs);
  friend Interval operator%(const Interval &lhs, const Interval &rhs);
  friend mlir::FailureOr<Interval> operator/(const Interval &lhs, const Interval &rhs);
 
  /* Checks and Comparisons */
 
  inline bool isEmpty() const { return ty == Type::Empty; }
  inline bool isNotEmpty() const { return !isEmpty(); }
  inline bool isDegenerate() const { return ty == Type::Degenerate; }
  inline bool isEntire() const { return ty == Type::Entire; }
  inline bool isTypeA() const { return ty == Type::TypeA; }
  inline bool isTypeB() const { return ty == Type::TypeB; }
  inline bool isTypeC() const { return ty == Type::TypeC; }
  inline bool isTypeF() const { return ty == Type::TypeF; }
 
  template <Type... Types> bool is() const { return ((ty == Types) || ...); }
 
  bool operator==(const Interval &rhs) const { return ty == rhs.ty && a == rhs.a && b == rhs.b; }
 
  /* Getters */
 
  const Field &getField() const { return field.get(); }
 
  llvm::APSInt width() const { return llvm::APSInt((b - a).abs().zext(field.get().bitWidth())); }
 
  llvm::APSInt lhs() const { return a; }
  llvm::APSInt rhs() const { return b; }
 
  /* Utility */
  struct Hash {
    unsigned operator()(const Interval &i) const {
      return std::hash<const Field *> {}(&i.field.get()) ^ std::hash<Type> {}(i.ty) ^
             llvm::hash_value(i.a) ^ llvm::hash_value(i.b);
    }
  };
 
  void print(mlir::raw_ostream &os) const;
 
  friend mlir::raw_ostream &operator<<(mlir::raw_ostream &os, const Interval &i) {
    i.print(os);
    return os;
  }
 
private:
  Interval(Type t, const Field &f) : field(f), ty(t), a(f.zero()), b(f.zero()) {}
  Interval(Type t, const Field &f, llvm::APSInt lhs, llvm::APSInt rhs)
      : field(f), ty(t), a(lhs.extend(f.bitWidth())), b(rhs.extend(f.bitWidth())) {}
 
  std::reference_wrapper<const Field> field;
  Type ty;
  llvm::APSInt a, b;
};
 
/* ExpressionValue */

class ExpressionValue {
public:
  /* Must be default initializable to be a ScalarLatticeValue. */
  ExpressionValue() : i(), expr(nullptr) {}
 
  explicit ExpressionValue(const Field &f, llvm::SMTExprRef exprRef)
      : i(Interval::Entire(f)), expr(exprRef) {}
 
  ExpressionValue(const Field &f, llvm::SMTExprRef exprRef, llvm::APSInt singleVal)
      : i(Interval::Degenerate(f, singleVal)), expr(exprRef) {}
 
  ExpressionValue(llvm::SMTExprRef exprRef, Interval interval) : i(interval), expr(exprRef) {}
 
  llvm::SMTExprRef getExpr() const { return expr; }
 
  const Interval &getInterval() const { return i; }
 
  const Field &getField() const { return i.getField(); }

  ExpressionValue withInterval(const Interval &newInterval) const {
    return ExpressionValue(expr, newInterval);
  }
 
  /* Required to be a ScalarLatticeValue. */
  ExpressionValue &join(const ExpressionValue &rhs) {
    i = Interval::Entire(getField());
    return *this;
  }
 
  bool operator==(const ExpressionValue &rhs) const;

  friend ExpressionValue
  intersection(llvm::SMTSolverRef solver, const ExpressionValue &lhs, const ExpressionValue &rhs);

  friend ExpressionValue
  join(llvm::SMTSolverRef solver, const ExpressionValue &lhs, const ExpressionValue &rhs);
 
  // arithmetic ops
 
  friend ExpressionValue
  add(llvm::SMTSolverRef solver, const ExpressionValue &lhs, const ExpressionValue &rhs);
 
  friend ExpressionValue
  sub(llvm::SMTSolverRef solver, const ExpressionValue &lhs, const ExpressionValue &rhs);
 
  friend ExpressionValue
  mul(llvm::SMTSolverRef solver, const ExpressionValue &lhs, const ExpressionValue &rhs);
 
  friend ExpressionValue
  div(llvm::SMTSolverRef solver, felt::DivFeltOp op, const ExpressionValue &lhs,
      const ExpressionValue &rhs);
 
  friend ExpressionValue
  mod(llvm::SMTSolverRef solver, const ExpressionValue &lhs, const ExpressionValue &rhs);
 
  friend ExpressionValue
  cmp(llvm::SMTSolverRef solver, boolean::CmpOp op, const ExpressionValue &lhs,
      const ExpressionValue &rhs);

  friend ExpressionValue fallbackBinaryOp(
      llvm::SMTSolverRef solver, mlir::Operation *op, const ExpressionValue &lhs,
      const ExpressionValue &rhs
  );
 
  friend ExpressionValue neg(llvm::SMTSolverRef solver, const ExpressionValue &val);
 
  friend ExpressionValue notOp(llvm::SMTSolverRef solver, const ExpressionValue &val);
 
  friend ExpressionValue
  fallbackUnaryOp(llvm::SMTSolverRef solver, mlir::Operation *op, const ExpressionValue &val);
 
  /* Utility */
 
  void print(mlir::raw_ostream &os) const;
 
  friend mlir::raw_ostream &operator<<(mlir::raw_ostream &os, const ExpressionValue &e) {
    e.print(os);
    return os;
  }
 
  struct Hash {
    unsigned operator()(const ExpressionValue &e) const {
      return Interval::Hash {}(e.i) ^ llvm::hash_value(e.expr);
    }
  };
 
private:
  Interval i;
  llvm::SMTExprRef expr;
};
 
/* IntervalAnalysisLatticeValue */
 
class IntervalAnalysisLatticeValue
    : public dataflow::AbstractLatticeValue<IntervalAnalysisLatticeValue, ExpressionValue> {
public:
  using AbstractLatticeValue::AbstractLatticeValue;
};
 
/* IntervalAnalysisLattice */
 
class IntervalDataFlowAnalysis;

class IntervalAnalysisLattice : public dataflow::AbstractDenseLattice {
public:
  using LatticeValue = IntervalAnalysisLatticeValue;
  // Map mlir::Values to LatticeValues
  using ValueMap = mlir::DenseMap<mlir::Value, LatticeValue>;
  // Expression to interval map for convenience.
  using ExpressionIntervals = mlir::DenseMap<llvm::SMTExprRef, Interval>;
  // Tracks all constraints and assignments in insertion order
  using ConstraintSet = llvm::SetVector<ExpressionValue>;
 
  using AbstractDenseLattice::AbstractDenseLattice;
 
  mlir::ChangeResult join(const AbstractDenseLattice &other) override;
 
  mlir::ChangeResult meet(const AbstractDenseLattice &rhs) override {
    llvm::report_fatal_error("IntervalDataFlowAnalysis::meet : unsupported");
    return mlir::ChangeResult::NoChange;
  }
 
  void print(mlir::raw_ostream &os) const override;
 
  mlir::FailureOr<LatticeValue> getValue(mlir::Value v) const;
 
  mlir::ChangeResult setValue(mlir::Value v, ExpressionValue e);
 
  mlir::ChangeResult addSolverConstraint(ExpressionValue e);
 
  friend mlir::raw_ostream &operator<<(mlir::raw_ostream &os, const IntervalAnalysisLattice &l) {
    l.print(os);
    return os;
  }
 
  const ConstraintSet &getConstraints() const { return constraints; }
 
  mlir::FailureOr<Interval> findInterval(llvm::SMTExprRef expr) const;
 
private:
  ValueMap valMap;
  ConstraintSet constraints;
  ExpressionIntervals intervals;
};
 
/* IntervalDataFlowAnalysis */
 
class IntervalDataFlowAnalysis
    : public dataflow::DenseForwardDataFlowAnalysis<IntervalAnalysisLattice> {
  using Base = dataflow::DenseForwardDataFlowAnalysis<IntervalAnalysisLattice>;
  using Lattice = IntervalAnalysisLattice;
  using LatticeValue = IntervalAnalysisLattice::LatticeValue;
 
  // Map fields to their symbols
  using SymbolMap = mlir::DenseMap<ConstrainRef, llvm::SMTExprRef>;
 
public:
  explicit IntervalDataFlowAnalysis(
      mlir::DataFlowSolver &solver, llvm::SMTSolverRef smt, const Field &f
  )
      : Base::DenseForwardDataFlowAnalysis(solver), dataflowSolver(solver), smtSolver(smt),
        field(f) {}
 
  void visitCallControlFlowTransfer(
      mlir::CallOpInterface call, dataflow::CallControlFlowAction action, const Lattice &before,
      Lattice *after
  ) override;
 
  void visitOperation(mlir::Operation *op, const Lattice &before, Lattice *after) override;

  llvm::SMTExprRef getOrCreateSymbol(const ConstrainRef &r);
 
private:
  mlir::DataFlowSolver &dataflowSolver;
  llvm::SMTSolverRef smtSolver;
  SymbolMap refSymbols;
  std::reference_wrapper<const Field> field;
 
  void setToEntryState(Lattice *lattice) override {
    // initial state should be empty, so do nothing here
  }
 
  llvm::SMTExprRef createFeltSymbol(const ConstrainRef &r) const;
 
  llvm::SMTExprRef createFeltSymbol(mlir::Value val) const;
 
  llvm::SMTExprRef createFeltSymbol(const char *name) const;
 
  bool isConstOp(mlir::Operation *op) const {
    return mlir::isa<
        felt::FeltConstantOp, mlir::arith::ConstantIndexOp, mlir::arith::ConstantIntOp>(op);
  }
 
  llvm::APSInt getConst(mlir::Operation *op) const;
 
  llvm::SMTExprRef createConstBitvectorExpr(llvm::APSInt v) const {
    return smtSolver->mkBitvector(v, field.get().bitWidth());
  }
 
  llvm::SMTExprRef createConstBoolExpr(bool v) const {
    return smtSolver->mkBitvector(mlir::APSInt((int)v), field.get().bitWidth());
  }
 
  bool isArithmeticOp(mlir::Operation *op) const {
    return mlir::isa<
        felt::AddFeltOp, felt::SubFeltOp, felt::MulFeltOp, felt::DivFeltOp, felt::ModFeltOp,
        felt::NegFeltOp, felt::InvFeltOp, felt::AndFeltOp, felt::OrFeltOp, felt::XorFeltOp,
        felt::NotFeltOp, felt::ShlFeltOp, felt::ShrFeltOp, boolean::CmpOp>(op);
  }
 
  ExpressionValue
  performBinaryArithmetic(mlir::Operation *op, const LatticeValue &a, const LatticeValue &b);
 
  ExpressionValue performUnaryArithmetic(mlir::Operation *op, const LatticeValue &a);

  mlir::ChangeResult
  applyInterval(mlir::Operation *originalOp, Lattice *after, mlir::Value val, Interval newInterval);
 
  bool isBoolOp(mlir::Operation *op) const {
    return mlir::isa<boolean::AndBoolOp, boolean::OrBoolOp, boolean::XorBoolOp, boolean::NotBoolOp>(
        op
    );
  }
 
  bool isConversionOp(mlir::Operation *op) const {
    return mlir::isa<cast::IntToFeltOp, cast::FeltToIndexOp>(op);
  }
 
  bool isApplyMapOp(mlir::Operation *op) const { return mlir::isa<polymorphic::ApplyMapOp>(op); }
 
  bool isAssertOp(mlir::Operation *op) const { return mlir::isa<boolean::AssertOp>(op); }
 
  bool isReadOp(mlir::Operation *op) const {
    return mlir::isa<component::FieldReadOp, polymorphic::ConstReadOp, array::ReadArrayOp>(op);
  }
 
  bool isWriteOp(mlir::Operation *op) const {
    return mlir::isa<component::FieldWriteOp, array::WriteArrayOp, array::InsertArrayOp>(op);
  }
 
  bool isArrayLengthOp(mlir::Operation *op) const { return mlir::isa<array::ArrayLengthOp>(op); }
 
  bool isEmitOp(mlir::Operation *op) const {
    return mlir::isa<constrain::EmitEqualityOp, constrain::EmitContainmentOp>(op);
  }
 
  bool isCreateOp(mlir::Operation *op) const {
    return mlir::isa<component::CreateStructOp, array::CreateArrayOp>(op);
  }
 
  bool isExtractArrayOp(mlir::Operation *op) const { return mlir::isa<array::ExtractArrayOp>(op); }
 
  bool isDefinitionOp(mlir::Operation *op) const {
    return mlir::isa<
        component::StructDefOp, function::FuncDefOp, component::FieldDefOp, global::GlobalDefOp,
        mlir::ModuleOp>(op);
  }
 
  bool isCallOp(mlir::Operation *op) const { return mlir::isa<function::CallOp>(op); }
 
  bool isReturnOp(mlir::Operation *op) const { return mlir::isa<function::ReturnOp>(op); }

  bool isConsideredOp(mlir::Operation *op) const {
    return isConstOp(op) || isArithmeticOp(op) || isBoolOp(op) || isConversionOp(op) ||
           isApplyMapOp(op) || isAssertOp(op) || isReadOp(op) || isWriteOp(op) ||
           isArrayLengthOp(op) || isEmitOp(op) || isCreateOp(op) || isDefinitionOp(op) ||
           isCallOp(op) || isReturnOp(op) || isExtractArrayOp(op);
  }
};
 
/* StructIntervals */

struct IntervalAnalysisContext {
  IntervalDataFlowAnalysis *intervalDFA;
  llvm::SMTSolverRef smtSolver;
  std::reference_wrapper<const Field> field;
 
  llvm::SMTExprRef getSymbol(const ConstrainRef &r) { return intervalDFA->getOrCreateSymbol(r); }
  const Field &getField() const { return field.get(); }
};
 
class StructIntervals {
public:
  static mlir::FailureOr<StructIntervals> compute(
      mlir::ModuleOp mod, component::StructDefOp s, mlir::DataFlowSolver &solver,
      mlir::AnalysisManager &am, IntervalAnalysisContext &ctx
  ) {
    StructIntervals si(mod, s);
    if (si.computeIntervals(solver, am, ctx).failed()) {
      return mlir::failure();
    }
    return si;
  }
 
  mlir::LogicalResult computeIntervals(
      mlir::DataFlowSolver &solver, mlir::AnalysisManager &am, IntervalAnalysisContext &ctx
  );
 
  void print(mlir::raw_ostream &os, bool withConstraints = false) const;
 
  const llvm::MapVector<ConstrainRef, Interval> &getIntervals() const {
    return constrainFieldRanges;
  }
 
  const llvm::SetVector<ExpressionValue> getSolverConstraints() const {
    return constrainSolverConstraints;
  }
 
  friend mlir::raw_ostream &operator<<(mlir::raw_ostream &os, const StructIntervals &si) {
    si.print(os);
    return os;
  }
 
private:
  mlir::ModuleOp mod;
  component::StructDefOp structDef;
  llvm::SMTSolverRef smtSolver;
  // llvm::MapVector keeps insertion order for consistent iteration
  llvm::MapVector<ConstrainRef, Interval> constrainFieldRanges;
  // llvm::SetVector for the same reasons as above
  llvm::SetVector<ExpressionValue> constrainSolverConstraints;
 
  StructIntervals(mlir::ModuleOp m, component::StructDefOp s) : mod(m), structDef(s) {}
};
 
/* StructIntervalAnalysis */
 
class ModuleIntervalAnalysis;
 
class StructIntervalAnalysis : public StructAnalysis<StructIntervals, IntervalAnalysisContext> {
public:
  using StructAnalysis::StructAnalysis;
 
  mlir::LogicalResult runAnalysis(
      mlir::DataFlowSolver &solver, mlir::AnalysisManager &moduleAnalysisManager,
      IntervalAnalysisContext &ctx
  ) override {
    auto res =
        StructIntervals::compute(getModule(), getStruct(), solver, moduleAnalysisManager, ctx);
    if (mlir::failed(res)) {
      return mlir::failure();
    }
    setResult(std::move(*res));
    return mlir::success();
  }
};
 
/* ModuleIntervalAnalysis */
 
class ModuleIntervalAnalysis
    : public ModuleAnalysis<StructIntervals, IntervalAnalysisContext, StructIntervalAnalysis> {
 
public:
  ModuleIntervalAnalysis(mlir::Operation *op)
      : ModuleAnalysis(op), smtSolver(llvm::CreateZ3Solver()), field(std::nullopt) {}
 
  void setField(const Field &f) { field = f; }
 
protected:
  void initializeSolver(mlir::DataFlowSolver &solver) override {
    ensure(field.has_value(), "field not set, could not generate analysis context");
    (void)solver.load<ConstrainRefAnalysis>();
    auto smtSolverRef = smtSolver;
    intervalDFA = solver.load<IntervalDataFlowAnalysis, llvm::SMTSolverRef, const Field &>(
        std::move(smtSolverRef), field.value()
    );
  }
 
  IntervalAnalysisContext getContext() override {
    ensure(field.has_value(), "field not set, could not generate analysis context");
    return {
        .intervalDFA = intervalDFA,
        .smtSolver = smtSolver,
        .field = field.value(),
    };
  }
 
private:
  llvm::SMTSolverRef smtSolver;
  IntervalDataFlowAnalysis *intervalDFA;
  std::optional<std::reference_wrapper<const Field>> field;
};
 
} // namespace llzk
 
namespace llvm {
 
template <> struct DenseMapInfo<llzk::ExpressionValue> {
 
  static SMTExprRef getEmptyExpr() {
    static auto emptyPtr = reinterpret_cast<SMTExprRef>(1);
    return emptyPtr;
  }
  static SMTExprRef getTombstoneExpr() {
    static auto tombstonePtr = reinterpret_cast<SMTExprRef>(2);
    return tombstonePtr;
  }
 
  static llzk::ExpressionValue getEmptyKey() {
    return llzk::ExpressionValue(llzk::Field::getField("bn128"), getEmptyExpr());
  }
  static inline llzk::ExpressionValue getTombstoneKey() {
    return llzk::ExpressionValue(llzk::Field::getField("bn128"), getTombstoneExpr());
  }
  static unsigned getHashValue(const llzk::ExpressionValue &e) {
    return llzk::ExpressionValue::Hash {}(e);
  }
  static bool isEqual(const llzk::ExpressionValue &lhs, const llzk::ExpressionValue &rhs) {
    if (lhs.getExpr() == getEmptyExpr() || lhs.getExpr() == getTombstoneExpr() ||
        rhs.getExpr() == getEmptyExpr() || rhs.getExpr() == getTombstoneExpr()) {
      return lhs.getExpr() == rhs.getExpr();
    }
    return lhs == rhs;
  }
};
 
} // namespace llvm