deploy: 3b720de

base64.mjs

@@ -0,0 +1,113 @@
+/**
+ * Convert between Uint8Array and Base64 strings
+ * Allows for any encoded JS string to be converted (as opposed to atob()/btoa() which only supports latin1)
+ *
+ * Original implementation by madmurphy on MDN
+ * @see https://developer.mozilla.org/en-US/docs/Web/API/WindowBase64/Base64_encoding_and_decoding#Solution_1_–_JavaScript%27s_UTF-16_%3E_base64
+ */
+
+function b64ToUint6(nChr) {
+  return nChr > 64 && nChr < 91
+    ? nChr - 65
+    : nChr > 96 && nChr < 123
+    ? nChr - 71
+    : nChr > 47 && nChr < 58
+    ? nChr + 4
+    : nChr === 43
+    ? 62
+    : nChr === 47
+    ? 63
+    : 0
+}
+
+export function decodeToArray(base64string, blockSize) {
+  var sB64Enc = base64string.replace(/[^A-Za-z0-9\+\/]/g, ''),
+    nInLen = sB64Enc.length,
+    nOutLen = blockSize
+      ? Math.ceil(((nInLen * 3 + 1) >>> 2) / blockSize) * blockSize
+      : (nInLen * 3 + 1) >>> 2,
+    aBytes = new Uint8Array(nOutLen)
+
+  for (
+    var nMod3, nMod4, nUint24 = 0, nOutIdx = 0, nInIdx = 0;
+    nInIdx < nInLen;
+    nInIdx++
+  ) {
+    nMod4 = nInIdx & 3
+    nUint24 |= b64ToUint6(sB64Enc.charCodeAt(nInIdx)) << (18 - 6 * nMod4)
+    if (nMod4 === 3 || nInLen - nInIdx === 1) {
+      for (nMod3 = 0; nMod3 < 3 && nOutIdx < nOutLen; nMod3++, nOutIdx++) {
+        aBytes[nOutIdx] = (nUint24 >>> ((16 >>> nMod3) & 24)) & 255
+      }
+      nUint24 = 0
+    }
+  }
+
+  return aBytes
+}
+
+function uint6ToB64(nUint6) {
+  return nUint6 < 26
+    ? nUint6 + 65
+    : nUint6 < 52
+    ? nUint6 + 71
+    : nUint6 < 62
+    ? nUint6 - 4
+    : nUint6 === 62
+    ? 43
+    : nUint6 === 63
+    ? 47
+    : 65
+}
+
+export function encodeFromArray(bytes) {
+  var eqLen = (3 - (bytes.length % 3)) % 3,
+    sB64Enc = ''
+
+  for (
+    var nMod3, nLen = bytes.length, nUint24 = 0, nIdx = 0;
+    nIdx < nLen;
+    nIdx++
+  ) {
+    nMod3 = nIdx % 3
+    /* Uncomment the following line in order to split the output in lines 76-character long: */
+    /*
+    if (nIdx > 0 && (nIdx * 4 / 3) % 76 === 0) { sB64Enc += "\r\n"; }
+    */
+    nUint24 |= bytes[nIdx] << ((16 >>> nMod3) & 24)
+    if (nMod3 === 2 || bytes.length - nIdx === 1) {
+      sB64Enc += String.fromCharCode(
+        uint6ToB64((nUint24 >>> 18) & 63),
+        uint6ToB64((nUint24 >>> 12) & 63),
+        uint6ToB64((nUint24 >>> 6) & 63),
+        uint6ToB64(nUint24 & 63)
+      )
+      nUint24 = 0
+    }
+  }
+
+  return eqLen === 0
+    ? sB64Enc
+    : sB64Enc.substring(0, sB64Enc.length - eqLen) + (eqLen === 1 ? '=' : '==')
+}
+
+/**
+ * URL-safe variants of Base64 conversion functions (aka base64url)
+ * @see https://tools.ietf.org/html/rfc4648#section-5
+ */
+
+export function encodeFromArrayUrlSafe(bytes) {
+  return encodeURIComponent(
+    encodeFromArray(bytes)
+      .replace(/\+/g, '-')
+      .replace(/\//g, '_')
+  )
+}
+
+export function decodeToArrayUrlSafe(base64string) {
+  return decodeToArray(
+    decodeURIComponent(base64string)
+      .replace(/-/g, '+')
+      .replace(/_/g, '/')
+  )
+}

churchroad.egg

@@ -0,0 +1,259 @@
+;;; Churchroad language definition with antiunification experiments.
+
+(sort IVec (Vec i64))
+(sort StringVec (Vec String))
+
+;;; Forward-declare Exprs and declare ExprVec.
+(sort Expr)
+(sort ExprVec (Vec Expr))
+
+
+; Ops
+(datatype Op
+  (And)
+  (Add)
+  (Or)
+  (Xor)
+  (Shr)
+  ; Returns a bitvector of width 1.
+  (Eq)
+  ; Bitwise not.
+  (Not)
+  (LogicNot)
+  ; (Mux select-expr expr expr)
+  (Mux)
+
+  ; (Op1 (Extract high low) expr)
+  ; Extraction from a bitvector.
+  (Extract i64 i64)
+
+  ; (Op2 (Concat) top-expr bottom-expr)
+  ; Concatenation of two bitvectors.
+  (Concat)
+
+  ; (Op2 (Reg init-value) clock-expr data-expr)
+  (Reg i64)
+
+  ; (Op0 (BV value bitwidth))
+  (BV i64 i64)
+
+  ; (Op1 (ZeroExtend bitwidth) expr)
+  (ZeroExtend i64)
+  )
+
+(datatype Graph 
+  ;;; Hole with a bitwidth.
+  ;(Hole i64)
+  ;;; TODO need to implement bitwidth. for now too lazy to implement the typechecking.
+  (Hole)
+
+  ;;;
+  (Op0_ Op)
+  (Op1_ Op Graph)
+  (Op2_ Op Graph Graph)
+  (Op3_ Op Graph Graph Graph)
+  )
+
+;;; Module declaration
+(sort Module)
+;;; IVec is an vector of integers holding De Bruijn indices.
+(function MakeModule (Graph IVec) Module)
+
+; Our language. Note that we do not explicitly use IDs as in the Lakeroad paper
+; (FPGA Technology Mapping via Program Synthesis, Smith et. al., ASPLOS 2024)
+; formalization. The IDs are still there, though: they're the eclass IDs!
+
+; (Var name bitwidth)
+(function Var (String i64) Expr)
+;;; I'm unsure whether we need this. This is the variant of Var we use as
+;;; arguments to `apply` nodes. This prevents the loop induced by putting
+;;; `(Var a 8) = (apply (MakeModule (Hole) [0]) [(Var a 8)])`
+;;; into the graph. If we put this in the graph, you could infinitely extract
+;;; `(apply (MakeModule ...) (apply (MakeModule ...) (apply (MakeModule ...) ...)))`
+;;; (which captures the fact that you can apply the identity function as many
+;;; times as you want).
+(function Var_ (String i64) Expr)
+
+;;; "Direct" representation of programs:
+;;; Expressing programs via direct application of Ops to leaf nodes (Vars
+;;; and Consts).
+; (OpN op input-expr...)
+; DO NOT MERGE: these costs are to force module extraction, but there should be a better way
+(function Op0 (Op) Expr :cost 1000)
+(function Op1 (Op Expr) Expr :cost 1000)
+(function Op2 (Op Expr Expr) Expr :cost 1000)
+(function Op3 (Op Expr Expr Expr) Expr :cost 1000)
+
+
+; (Wire name bitwidth)
+(function Wire (String i64) Expr)
+
+(function apply (Module ExprVec) Expr)
+
+;;; TODO(@gussmith23): need cons list instead of using built-in vec.
+;;; would love to use vec instead.
+;;; this issue kinda pertains to this: https://github.com/egraphs-good/egglog/issues/370
+(datatype StringConsList
+  (StringCons String StringConsList)
+  (StringNil))
+(datatype ExprConsList
+  (ExprCons Expr ExprConsList)
+  (ExprNil))
+
+(sort ModuleInstanceSort)
+;;; (module name: String, 
+;;;  input port names: [String],
+;;;  input port values: [Expr]) -> module instance
+(function ModuleInstance (String StringConsList ExprConsList) ModuleInstanceSort)
+;;; Get the output of a module instance.
+;;; (module instance: ModuleInstanceSort,
+;;;  output name: String) -> Churchroad expression
+(function GetOutput (ModuleInstanceSort String) Expr)
+
+;;; Types for Churchroad expressions.
+(datatype Type
+  ;;; Bitvector type.
+  (Bitvector i64)
+  ;;; Module type: when `apply`ed, gives back the indicated type. This could be
+  ;;; a lot more rigorous. Currently will not allow for checking correct input
+  ;;; types.
+  (ModuleType Type))
+
+;;; A type for port directions. Currently has two values: Input and Output.
+(datatype PortDirection (Input) (Output))
+
+;;; Indicates that a Churchroad expression is a port for the given module.
+;;; (module name: String,
+;;;  port name: String,
+;;;  port direction: PortDirection,
+;;;  Churchroad expression: Expr)
+(relation IsPort (String String PortDirection Expr))
+
+;;; Indicates that a Churchroad expression has a given type.
+(relation HasType (Expr Type))
+
+;;; Indicates that all input and output bitwidths must match for this type of 
+;;; op.
+(relation AllBitwidthsMatch (Op))
+(AllBitwidthsMatch (And))
+(AllBitwidthsMatch (Add))
+(AllBitwidthsMatch (Or))
+(AllBitwidthsMatch (Xor))
+(AllBitwidthsMatch (Shr))
+; Have to write this one as a rule, unfortunately.
+(ruleset core)
+(rule ((Reg n)) ((AllBitwidthsMatch (Reg n))) :ruleset core)
+
+;;; Indicates that, for the op, the input bitwidths must match, and the output
+;;; bitwidth is the indicated constant.
+(relation InputBitwidthsMatchOutputBitwidthConst (Op i64))
+(InputBitwidthsMatchOutputBitwidthConst (Eq) 1)
+
+;;; Bitwise: Indicates that an op `(op a b ...)` can be written 
+;;; `(concat (op a[0] b[0] ...) (op a[1] b[1] ...) ...)`.
+(relation Bitwise (Op))
+(Bitwise (And))
+(Bitwise (Or))
+(Bitwise (Xor))
+
+
+;;; Typing judgements.
+(ruleset typing)
+(rule
+  ((Wire name bw))
+  ((HasType (Wire name bw) (Bitvector bw)))
+  :ruleset typing)
+(rule
+  ((Var name bw))
+  ((HasType (Var name bw) (Bitvector bw)))
+  :ruleset typing)
+(rule
+  ((Op0 (BV val bw)))
+  ((HasType (Op0 (BV val bw)) (Bitvector bw)))
+  :ruleset typing)
+(rule
+  ((Op1 op i0)
+   (HasType i0 (Bitvector bw))
+   (AllBitwidthsMatch op))
+  ((HasType (Op1 op i0) (Bitvector bw)))
+  :ruleset typing)
+(rule
+  ((Op2 op i0 i1)
+   (HasType i0 (Bitvector bw))
+   (HasType i1 (Bitvector bw))
+   (AllBitwidthsMatch op))
+  ((HasType (Op2 op i0 i1) (Bitvector bw)))
+  :ruleset typing)
+(rule
+  ((Op3 op i0 i1 i2)
+   (HasType i0 (Bitvector bw))
+   (HasType i1 (Bitvector bw))
+   (HasType i2 (Bitvector bw))
+   (AllBitwidthsMatch op))
+  ((HasType (Op3 op i0 i1 i2) (Bitvector bw)))
+  :ruleset typing)
+(rule
+  ((Op1 op i0)
+   (HasType i0 (Bitvector bw))
+   (InputBitwidthsMatchOutputBitwidthConst op out-bw))
+  ((HasType (Op1 op i0) (Bitvector out-bw)))
+  :ruleset typing)
+(rule
+  ((Op2 op i0 i1)
+   (HasType i0 (Bitvector bw))
+   (HasType i1 (Bitvector bw))
+   (InputBitwidthsMatchOutputBitwidthConst op out-bw))
+  ((HasType (Op2 op i0 i1) (Bitvector out-bw)))
+  :ruleset typing)
+(rule
+  ((Op3 op i0 i1 i2)
+   (HasType i0 (Bitvector bw))
+   (HasType i1 (Bitvector bw))
+   (HasType i2 (Bitvector bw))
+   (InputBitwidthsMatchOutputBitwidthConst op out-bw))
+  ((HasType (Op3 op i0 i1 i2) (Bitvector out-bw)))
+  :ruleset typing)
+(rule
+  ((Op3 (Mux) sel-expr a-expr b-expr)
+   (HasType sel-expr (Bitvector 1))
+   (HasType a-expr (Bitvector bw))
+   (HasType b-expr (Bitvector bw)))
+  ((HasType (Op3 (Mux) sel-expr a-expr b-expr) (Bitvector bw)))
+  :ruleset typing)
+(rule
+  ((Op2 (Concat) a-expr b-expr)
+   (HasType a-expr (Bitvector m))
+   (HasType b-expr (Bitvector n)))
+  ((HasType (Op2 (Concat) a-expr b-expr) (Bitvector (+ m n))))
+  :ruleset typing)
+(rule
+  ((Op1 (Extract high low) expr)
+   (HasType expr (Bitvector n))
+   (>= 0 low)
+   (< high n))
+  ((HasType (Op1 (Extract high low) expr) (Bitvector (+ 1 (- high low)))))
+  :ruleset typing)
+(rule
+  ((Op1 (ZeroExtend bitwidth) expr))
+  ((HasType (Op1 (ZeroExtend bitwidth) expr) (Bitvector bitwidth)))
+  :ruleset typing)
+(rule
+  ((Op1 (Reg init) expr)
+   (HasType expr (Bitvector n)))
+  ((HasType (Op1 (Reg init) expr) (Bitvector n)))
+  :ruleset typing)
+
+;;; Rewrites that are likely to expand the egraph.
+(ruleset expansion)
+(rule 
+ ((Op2 op e1 e2)
+  (Bitwise op)
+  (HasType (Op2 op e1 e2) (Bitvector n))
+  (> n 1))
+ ((union
+   (Op2 op e1 e2)
+   (Op2 (Concat) 
+    (Op2 op 
+     (Op1 (Extract (- n 1) 1) e1) (Op1 (Extract (- n 1) 1) e2))
+    (Op2 op 
+     (Op1 (Extract 0 0) e1) (Op1 (Extract 0 0) e2))))))