feat: Blake3 + LSpec

.github/workflows/ci.yml

@@ -47,7 +47,5 @@ jobs:
  # TODO: Add '.cargo/config' for list of enabled/disabled `xclippy`lints
  - name: Check clippy warnings
  run: cargo clippy -- -D warnings
- - name: Doctests
- run: cargo test --doc --workspace
  - name: Cargo-deny
  uses: EmbarkStudios/cargo-deny-action@v2

.github/workflows/lspec.yml

@@ -0,0 +1,20 @@
+name: "LSpec CI"
+on:
+ pull_request:
+ push:
+ branches:
+ - main
+jobs:
+ build:
+ name: Build
+ runs-on: ubuntu-latest
+ steps:
+ - name: install elan
+ run: |
+ set -o pipefail
+ curl -sSfL https://github.com/leanprover/elan/releases/download/v4.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+ ./elan-init -y --default-toolchain none
+ echo "$HOME/.elan/bin" >> $GITHUB_PATH
+ - uses: actions/checkout@v4
+ - name: run LSpec binary
+ run: lake exe lspec

Cargo.toml

@@ -3,15 +3,19 @@ name = "ix"
 version = "0.1.0"
 edition = "2021"
 
+[lib]
+crate-type = ["staticlib"]
+
 [dependencies]
 anyhow = "1"
-rustc-hash = "2"
 binius_core = { git = "https://gitlab.com/IrreducibleOSS/binius.git", rev = "0e5ec53f260f40fe6afcc741d4ff8f021a66dc1a" }
 binius_circuits = { git = "https://gitlab.com/IrreducibleOSS/binius.git", rev = "0e5ec53f260f40fe6afcc741d4ff8f021a66dc1a" }
 binius_field = { git = "https://gitlab.com/IrreducibleOSS/binius.git", rev = "0e5ec53f260f40fe6afcc741d4ff8f021a66dc1a" }
 binius_macros = { git = "https://gitlab.com/IrreducibleOSS/binius.git", rev = "0e5ec53f260f40fe6afcc741d4ff8f021a66dc1a" }
 binius_math = { git = "https://gitlab.com/IrreducibleOSS/binius.git", rev = "0e5ec53f260f40fe6afcc741d4ff8f021a66dc1a" }
+blake3 = "1"
 bytemuck = "1"
 bumpalo = "3"
 proptest = "1"
 rayon = "1"
+rustc-hash = "2"

Ix/Address.lean

@@ -1,3 +1,2 @@
-
 structure Address where
  adr : ByteArray

Ix/Blake3.lean

@@ -0,0 +1,2 @@
+@[extern "lean_byte_array_blake3"]
+opaque ByteArray.blake3 : @& ByteArray → ByteArray

Ix/ByteArray.lean

@@ -0,0 +1,12 @@
+namespace ByteArray
+
+def beqNoFFI (a b : ByteArray) : Bool :=
+ a.data == b.data
+
+@[extern "lean_byte_array_beq"]
+def beq : @& ByteArray → @& ByteArray → Bool :=
+ beqNoFFI
+
+instance : BEq ByteArray := ⟨ByteArray.beq⟩
+
+end ByteArray

Ix/Ixon.lean

@@ -1,11 +1,6 @@
-
 import Ix.Address
 import Lean.Declaration
 import Ix.Ixon.Serialize
 import Ix.Ixon.Univ
 import Ix.Ixon.Expr
 import Ix.Ixon.Const
-
-
-
-

Ix/Ixon/Const.lean

@@ -1,4 +1,3 @@
-
 import Ix.Address
 import Lean.Declaration
 import Ix.Ixon.Serialize

Ix/Ixon/Expr.lean

@@ -1,4 +1,3 @@
-
 import Ix.Address
 import Lean.Declaration
 import Ix.Ixon.Serialize
@@ -9,7 +8,7 @@ namespace Ixon
 -- 0xTTTT_LXXX
 inductive Expr where
  -- 0x0, ^1
- | vari (idx: UInt64) : Expr
+ | vari (idx: UInt64) : Expr
  -- 0x1, {max (add 1 2) (var 1)}
  | sort (univ: Univ) : Expr
  -- 0x2 #dead_beef_cafe_babe {u1, u2, ... }
@@ -24,7 +23,7 @@ inductive Expr where
  | alls (types: List Expr) (body: Expr) : Expr
  -- 0x7 (let d : A in b)
  | let_ (type: Expr) (defn: Expr) (body: Expr) : Expr
- -- 0x8 .1
+ -- 0x8 .1
  | proj : UInt64 -> Expr -> Expr
  -- 0x9 "foobar"
  | strl (lit: String) : Expr
@@ -33,7 +32,7 @@ inductive Expr where
 -- array: 0xB
 -- const: 0xC
 
-def putExprTag (tag: UInt8) (val: UInt64) : PutM Unit :=
+def putExprTag (tag: UInt8) (val: UInt64) : PutM Unit :=
  let t := UInt8.shiftLeft tag 4
  if val < 8
  then putUInt8 (UInt8.lor t (Nat.toUInt8 (UInt64.toNat val))) *> pure ()

Ix/Ixon/Serialize.lean

@@ -1,4 +1,3 @@
-
 namespace Ixon
 
 class Serialize (A: Type) where
@@ -13,7 +12,7 @@ structure GetState where
 
 abbrev GetM A := EStateM String GetState A
 
-def runGet (getm: GetM A) (bytes: ByteArray) : Except String A :=
+def runGet (getm: GetM A) (bytes: ByteArray) : Except String A :=
  match EStateM.run getm { index := 0, bytes } with
  | .ok a _ => .ok a
  | .error e _ => .error e

README.md

@@ -1 +1,3 @@
-# ix
+# ix
+
+A verifiable computing platform

Tests/Blake3.lean

@@ -0,0 +1,16 @@
+import LSpec
+import Ix.Blake3
+
+def pairs : List $ (List UInt8 × List UInt8) := [
+ ([0], [ 45, 58, 222, 223, 241, 27, 97, 241,
+ 76, 136, 110, 53, 175, 160, 54, 115,
+ 109, 205, 135, 167, 77, 39, 181, 193,
+ 81, 2, 37, 208, 245, 146, 226, 19,])
+]
+
+open LSpec in
+def main := lspecIO $
+ pairs.foldl (init := .done) fun tSeq (i, o) =>
+ let input := ByteArray.mk ⟨i⟩
+ let output := ByteArray.mk ⟨o⟩
+ tSeq ++ (test s!"blake3 on {input}" $ input.blake3.data = output.data)

Tests/ByteArray.lean

@@ -0,0 +1,22 @@
+import LSpec
+import Ix.ByteArray
+
+def arrays : List ByteArray := [
+ ⟨#[]⟩, ⟨#[1]⟩, ⟨#[0, 3]⟩, ⟨#[1, 1, 1]⟩, ⟨#[3, 3, 3, 3]⟩, ⟨#[13]⟩
+]
+
+def arrays' : List ByteArray := [
+ ⟨#[1]⟩, ⟨#[2]⟩, ⟨#[0, 3, 0]⟩, ⟨#[1, 2, 1]⟩, ⟨#[3, 3, 4, 3]⟩, ⟨#[13, 0]⟩
+]
+
+open LSpec
+
+def beq : TestSeq :=
+ arrays.zip arrays |>.foldl (init := .done) fun tSeq (x, y) =>
+ tSeq ++ (test s!"{x} == {y}" $ x.beq y && x.beqNoFFI y && y.beq x && y.beqNoFFI x)
+
+def neq : TestSeq :=
+ arrays.zip arrays.reverse |>.foldl (init := .done) fun tSeq (x, y) =>
+ tSeq ++ (test s!"{x} != {y}" $ !x.beq y && !x.beqNoFFI y && !y.beq x && !y.beqNoFFI x)
+
+def main := lspecIO $ beq ++ neq

deny.toml

@@ -92,6 +92,7 @@ allow = [
  "MIT",
  "Apache-2.0",
  "Unicode-3.0",
+ "BSD-2-Clause",
  "BSD-3-Clause",
  "CC0-1.0",
  "Zlib",

ffi.c

@@ -0,0 +1,39 @@
+#include <lean/lean.h>
+#include <string.h>
+
+#define intern inline static
+#define l_arg b_lean_obj_arg
+#define l_res lean_obj_res
+
+// Interfaces targeting Rust implementations
+
+void blake3(uint8_t*, size_t, uint8_t*);
+
+// Auxiliary implementations
+
+intern lean_sarray_object* mk_byte_array(size_t len) {
+ lean_sarray_object* o = (lean_sarray_object*)lean_alloc_object(
+ sizeof(lean_sarray_object) + len
+ );
+ lean_set_st_header((lean_object*)o, LeanScalarArray, 1);
+ o->m_size = len;
+ o->m_capacity = len;
+ return o;
+}
+
+// Implementations to serve Lean 4
+
+extern l_res lean_byte_array_blake3(l_arg a) {
+ lean_sarray_object* oa = lean_to_sarray(a);
+ lean_sarray_object* res = mk_byte_array(32);
+ blake3(res->m_data, oa->m_size, oa->m_data);
+ return (lean_object*)res;
+}
+
+extern bool lean_byte_array_beq(l_arg a, l_arg b) {
+ lean_sarray_object* oa = lean_to_sarray(a);
+ lean_sarray_object* ob = lean_to_sarray(b);
+ size_t sa = oa->m_size;
+ if (sa == ob->m_size) return memcmp(oa->m_data, ob->m_data, sa) == 0;
+ return false;
+}

lake-manifest.json

@@ -1,5 +1,15 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
- "packages": [],
+ "packages":
+ [{"url": "https://github.com/argumentcomputer/LSpec",
+ "type": "git",
+ "subDir": null,
+ "scope": "",
+ "rev": "ca8e2803f89f0c12bf9743ae7abbfb2ea6b0eeec",
+ "name": "LSpec",
+ "manifestFile": "lake-manifest.json",
+ "inputRev": "ca8e2803f89f0c12bf9743ae7abbfb2ea6b0eeec",
+ "inherited": false,
+ "configFile": "lakefile.toml"}],
  "name": "ix",
  "lakeDir": ".lake"}

lakefile.lean

@@ -0,0 +1,43 @@
+import Lake
+open System Lake DSL
+
+package ix where
+ version := v!"0.1.0"
+
+lean_lib Ix
+
+@[default_target]
+lean_exe ix where
+ root := `Main
+
+require LSpec from git
+ "https://github.com/argumentcomputer/LSpec" @ "ca8e2803f89f0c12bf9743ae7abbfb2ea6b0eeec"
+
+section Tests
+
+lean_exe Tests.Blake3
+lean_exe Tests.ByteArray
+
+end Tests
+
+section FFI
+
+target ffi.o pkg : FilePath := do
+ let oFile := pkg.buildDir / "ffi.o"
+ let srcJob ← inputTextFile "ffi.c"
+ let includeDir ← getLeanIncludeDir
+ let weakArgs := #["-I", includeDir.toString]
+ buildO oFile srcJob weakArgs #["-fPIC"] "cc" getLeanTrace
+
+extern_lib liblean_ffi pkg := do
+ let name := nameToStaticLib "ffi"
+ let ffiO ← ffi.o.fetch
+ buildStaticLib (pkg.nativeLibDir / name) #[ffiO]
+
+extern_lib rust_ffi pkg := do
+ proc { cmd := "cargo", args := #["build", "--release"], cwd := pkg.dir }
+ let name := nameToStaticLib "ix"
+ let srcPath := pkg.dir / "target" / "release" / name
+ return pure srcPath
+
+end FFI

src/lib.rs

@@ -1,5 +1,14 @@
 pub mod eiur;
 
+use blake3::hash;
+
+#[no_mangle]
+extern "C" fn blake3(mem: &mut [u8; 32], len: usize, input: *const u8) {
+ unsafe {
+ *mem = *hash(std::slice::from_raw_parts(input, len)).as_bytes();
+ }
+}
+
 #[cfg(test)]
 mod tests {
  #[test]

.github/workflows/ci.yml

@@ -47,7 +47,5 @@ jobs:
  # TODO: Add '.cargo/config' for list of enabled/disabled `xclippy`lints
  - name: Check clippy warnings
  run: cargo clippy -- -D warnings
- - name: Doctests
- run: cargo test --doc --workspace
  - name: Cargo-deny
  uses: EmbarkStudios/cargo-deny-action@v2

.github/workflows/lspec.yml

@@ -0,0 +1,20 @@
+name: "LSpec CI"
+on:
+ pull_request:
+ push:
+ branches:
+ - main
+jobs:
+ build:
+ name: Build
+ runs-on: ubuntu-latest
+ steps:
+ - name: install elan
+ run: |
+ set -o pipefail
+ curl -sSfL https://github.com/leanprover/elan/releases/download/v4.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+ ./elan-init -y --default-toolchain none
+ echo "$HOME/.elan/bin" >> $GITHUB_PATH
+ - uses: actions/checkout@v4
+ - name: run LSpec binary
+ run: lake exe lspec

Cargo.toml

@@ -3,15 +3,19 @@ name = "ix"
 version = "0.1.0"
 edition = "2021"
 
+[lib]
+crate-type = ["staticlib"]
+
 [dependencies]
 anyhow = "1"
-rustc-hash = "2"
 binius_core = { git = "https://gitlab.com/IrreducibleOSS/binius.git", rev = "0e5ec53f260f40fe6afcc741d4ff8f021a66dc1a" }
 binius_circuits = { git = "https://gitlab.com/IrreducibleOSS/binius.git", rev = "0e5ec53f260f40fe6afcc741d4ff8f021a66dc1a" }
 binius_field = { git = "https://gitlab.com/IrreducibleOSS/binius.git", rev = "0e5ec53f260f40fe6afcc741d4ff8f021a66dc1a" }
 binius_macros = { git = "https://gitlab.com/IrreducibleOSS/binius.git", rev = "0e5ec53f260f40fe6afcc741d4ff8f021a66dc1a" }
 binius_math = { git = "https://gitlab.com/IrreducibleOSS/binius.git", rev = "0e5ec53f260f40fe6afcc741d4ff8f021a66dc1a" }
+blake3 = "1"
 bytemuck = "1"
 bumpalo = "3"
 proptest = "1"
 rayon = "1"
+rustc-hash = "2"

Ix/Address.lean

@@ -1,3 +1,2 @@
-
 structure Address where
  adr : ByteArray

Ix/Blake3.lean

@@ -0,0 +1,2 @@
+@[extern "lean_byte_array_blake3"]
+opaque ByteArray.blake3 : @& ByteArray → ByteArray

Ix/ByteArray.lean

@@ -0,0 +1,12 @@
+namespace ByteArray
+
+def beqNoFFI (a b : ByteArray) : Bool :=
+ a.data == b.data
+
+@[extern "lean_byte_array_beq"]
+def beq : @& ByteArray → @& ByteArray → Bool :=
+ beqNoFFI
+
+instance : BEq ByteArray := ⟨ByteArray.beq⟩
+
+end ByteArray

Ix/Ixon.lean

@@ -1,11 +1,6 @@
-
 import Ix.Address
 import Lean.Declaration
 import Ix.Ixon.Serialize
 import Ix.Ixon.Univ
 import Ix.Ixon.Expr
 import Ix.Ixon.Const
-
-
-
-

Ix/Ixon/Const.lean

@@ -1,4 +1,3 @@
-
 import Ix.Address
 import Lean.Declaration
 import Ix.Ixon.Serialize

Ix/Ixon/Expr.lean

@@ -1,4 +1,3 @@
-
 import Ix.Address
 import Lean.Declaration
 import Ix.Ixon.Serialize
@@ -9,7 +8,7 @@ namespace Ixon
 -- 0xTTTT_LXXX
 inductive Expr where
  -- 0x0, ^1
- | vari (idx: UInt64) : Expr
+ | vari (idx: UInt64) : Expr
  -- 0x1, {max (add 1 2) (var 1)}
  | sort (univ: Univ) : Expr
  -- 0x2 #dead_beef_cafe_babe {u1, u2, ... }
@@ -24,7 +23,7 @@ inductive Expr where
  | alls (types: List Expr) (body: Expr) : Expr
  -- 0x7 (let d : A in b)
  | let_ (type: Expr) (defn: Expr) (body: Expr) : Expr
- -- 0x8 .1
+ -- 0x8 .1
  | proj : UInt64 -> Expr -> Expr
  -- 0x9 "foobar"
  | strl (lit: String) : Expr
@@ -33,7 +32,7 @@ inductive Expr where
 -- array: 0xB
 -- const: 0xC
 
-def putExprTag (tag: UInt8) (val: UInt64) : PutM Unit :=
+def putExprTag (tag: UInt8) (val: UInt64) : PutM Unit :=
  let t := UInt8.shiftLeft tag 4
  if val < 8
  then putUInt8 (UInt8.lor t (Nat.toUInt8 (UInt64.toNat val))) *> pure ()

Ix/Ixon/Serialize.lean

@@ -1,4 +1,3 @@
-
 namespace Ixon
 
 class Serialize (A: Type) where
@@ -13,7 +12,7 @@ structure GetState where
 
 abbrev GetM A := EStateM String GetState A
 
-def runGet (getm: GetM A) (bytes: ByteArray) : Except String A :=
+def runGet (getm: GetM A) (bytes: ByteArray) : Except String A :=
  match EStateM.run getm { index := 0, bytes } with
  | .ok a _ => .ok a
  | .error e _ => .error e

README.md

@@ -1 +1,3 @@
-# ix
+# ix
+
+A verifiable computing platform

Tests/Blake3.lean

@@ -0,0 +1,16 @@
+import LSpec
+import Ix.Blake3
+
+def pairs : List $ (List UInt8 × List UInt8) := [
+ ([0], [ 45, 58, 222, 223, 241, 27, 97, 241,
+ 76, 136, 110, 53, 175, 160, 54, 115,
+ 109, 205, 135, 167, 77, 39, 181, 193,
+ 81, 2, 37, 208, 245, 146, 226, 19,])
+]
+
+open LSpec in
+def main := lspecIO $
+ pairs.foldl (init := .done) fun tSeq (i, o) =>
+ let input := ByteArray.mk ⟨i⟩
+ let output := ByteArray.mk ⟨o⟩
+ tSeq ++ (test s!"blake3 on {input}" $ input.blake3.data = output.data)

Tests/ByteArray.lean

@@ -0,0 +1,22 @@
+import LSpec
+import Ix.ByteArray
+
+def arrays : List ByteArray := [
+ ⟨#[]⟩, ⟨#[1]⟩, ⟨#[0, 3]⟩, ⟨#[1, 1, 1]⟩, ⟨#[3, 3, 3, 3]⟩, ⟨#[13]⟩
+]
+
+def arrays' : List ByteArray := [
+ ⟨#[1]⟩, ⟨#[2]⟩, ⟨#[0, 3, 0]⟩, ⟨#[1, 2, 1]⟩, ⟨#[3, 3, 4, 3]⟩, ⟨#[13, 0]⟩
+]
+
+open LSpec
+
+def beq : TestSeq :=
+ arrays.zip arrays |>.foldl (init := .done) fun tSeq (x, y) =>
+ tSeq ++ (test s!"{x} == {y}" $ x.beq y && x.beqNoFFI y && y.beq x && y.beqNoFFI x)
+
+def neq : TestSeq :=
+ arrays.zip arrays.reverse |>.foldl (init := .done) fun tSeq (x, y) =>
+ tSeq ++ (test s!"{x} != {y}" $ !x.beq y && !x.beqNoFFI y && !y.beq x && !y.beqNoFFI x)
+
+def main := lspecIO $ beq ++ neq

deny.toml

@@ -92,6 +92,7 @@ allow = [
  "MIT",
  "Apache-2.0",
  "Unicode-3.0",
+ "BSD-2-Clause",
  "BSD-3-Clause",
  "CC0-1.0",
  "Zlib",

ffi.c

@@ -0,0 +1,39 @@
+#include <lean/lean.h>
+#include <string.h>
+
+#define intern inline static
+#define l_arg b_lean_obj_arg
+#define l_res lean_obj_res
+
+// Interfaces targeting Rust implementations
+
+void blake3(uint8_t*, size_t, uint8_t*);
+
+// Auxiliary implementations
+
+intern lean_sarray_object* mk_byte_array(size_t len) {
+ lean_sarray_object* o = (lean_sarray_object*)lean_alloc_object(
+ sizeof(lean_sarray_object) + len
+ );
+ lean_set_st_header((lean_object*)o, LeanScalarArray, 1);
+ o->m_size = len;
+ o->m_capacity = len;
+ return o;
+}
+
+// Implementations to serve Lean 4
+
+extern l_res lean_byte_array_blake3(l_arg a) {
+ lean_sarray_object* oa = lean_to_sarray(a);
+ lean_sarray_object* res = mk_byte_array(32);
+ blake3(res->m_data, oa->m_size, oa->m_data);
+ return (lean_object*)res;
+}
+
+extern bool lean_byte_array_beq(l_arg a, l_arg b) {
+ lean_sarray_object* oa = lean_to_sarray(a);
+ lean_sarray_object* ob = lean_to_sarray(b);
+ size_t sa = oa->m_size;
+ if (sa == ob->m_size) return memcmp(oa->m_data, ob->m_data, sa) == 0;
+ return false;
+}

lake-manifest.json

@@ -1,5 +1,15 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
- "packages": [],
+ "packages":
+ [{"url": "https://github.com/argumentcomputer/LSpec",
+ "type": "git",
+ "subDir": null,
+ "scope": "",
+ "rev": "ca8e2803f89f0c12bf9743ae7abbfb2ea6b0eeec",
+ "name": "LSpec",
+ "manifestFile": "lake-manifest.json",
+ "inputRev": "ca8e2803f89f0c12bf9743ae7abbfb2ea6b0eeec",
+ "inherited": false,
+ "configFile": "lakefile.toml"}],
  "name": "ix",
  "lakeDir": ".lake"}

lakefile.lean

@@ -0,0 +1,43 @@
+import Lake
+open System Lake DSL
+
+package ix where
+ version := v!"0.1.0"
+
+lean_lib Ix
+
+@[default_target]
+lean_exe ix where
+ root := `Main
+
+require LSpec from git
+ "https://github.com/argumentcomputer/LSpec" @ "ca8e2803f89f0c12bf9743ae7abbfb2ea6b0eeec"
+
+section Tests
+
+lean_exe Tests.Blake3
+lean_exe Tests.ByteArray
+
+end Tests
+
+section FFI
+
+target ffi.o pkg : FilePath := do
+ let oFile := pkg.buildDir / "ffi.o"
+ let srcJob ← inputTextFile "ffi.c"
+ let includeDir ← getLeanIncludeDir
+ let weakArgs := #["-I", includeDir.toString]
+ buildO oFile srcJob weakArgs #["-fPIC"] "cc" getLeanTrace
+
+extern_lib liblean_ffi pkg := do
+ let name := nameToStaticLib "ffi"
+ let ffiO ← ffi.o.fetch
+ buildStaticLib (pkg.nativeLibDir / name) #[ffiO]
+
+extern_lib rust_ffi pkg := do
+ proc { cmd := "cargo", args := #["build", "--release"], cwd := pkg.dir }
+ let name := nameToStaticLib "ix"
+ let srcPath := pkg.dir / "target" / "release" / name
+ return pure srcPath
+
+end FFI

src/lib.rs

@@ -1,5 +1,14 @@
 pub mod eiur;
 
+use blake3::hash;
+
+#[no_mangle]
+extern "C" fn blake3(mem: &mut [u8; 32], len: usize, input: *const u8) {
+ unsafe {
+ *mem = *hash(std::slice::from_raw_parts(input, len)).as_bytes();
+ }
+}
+
 #[cfg(test)]
 mod tests {
  #[test]

.github/workflows/ci.yml

@@ -47,7 +47,5 @@ jobs:
  # TODO: Add '.cargo/config' for list of enabled/disabled `xclippy`lints
  - name: Check clippy warnings
  run: cargo clippy -- -D warnings
- - name: Doctests
- run: cargo test --doc --workspace
  - name: Cargo-deny
  uses: EmbarkStudios/cargo-deny-action@v2

.github/workflows/lspec.yml

@@ -0,0 +1,20 @@
+name: "LSpec CI"
+on:
+ pull_request:
+ push:
+ branches:
+ - main
+jobs:
+ build:
+ name: Build
+ runs-on: ubuntu-latest
+ steps:
+ - name: install elan
+ run: |
+ set -o pipefail
+ curl -sSfL https://github.com/leanprover/elan/releases/download/v4.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+ ./elan-init -y --default-toolchain none
+ echo "$HOME/.elan/bin" >> $GITHUB_PATH
+ - uses: actions/checkout@v4
+ - name: run LSpec binary
+ run: lake exe lspec

Cargo.toml

@@ -3,15 +3,19 @@ name = "ix"
 version = "0.1.0"
 edition = "2021"
 
+[lib]
+crate-type = ["staticlib"]
+
 [dependencies]
 anyhow = "1"
-rustc-hash = "2"
 binius_core = { git = "https://gitlab.com/IrreducibleOSS/binius.git", rev = "0e5ec53f260f40fe6afcc741d4ff8f021a66dc1a" }
 binius_circuits = { git = "https://gitlab.com/IrreducibleOSS/binius.git", rev = "0e5ec53f260f40fe6afcc741d4ff8f021a66dc1a" }
 binius_field = { git = "https://gitlab.com/IrreducibleOSS/binius.git", rev = "0e5ec53f260f40fe6afcc741d4ff8f021a66dc1a" }
 binius_macros = { git = "https://gitlab.com/IrreducibleOSS/binius.git", rev = "0e5ec53f260f40fe6afcc741d4ff8f021a66dc1a" }
 binius_math = { git = "https://gitlab.com/IrreducibleOSS/binius.git", rev = "0e5ec53f260f40fe6afcc741d4ff8f021a66dc1a" }
+blake3 = "1"
 bytemuck = "1"
 bumpalo = "3"
 proptest = "1"
 rayon = "1"
+rustc-hash = "2"

Ix/Address.lean

@@ -1,3 +1,2 @@
-
 structure Address where
  adr : ByteArray

Ix/Blake3.lean

@@ -0,0 +1,2 @@
+@[extern "lean_byte_array_blake3"]
+opaque ByteArray.blake3 : @& ByteArray → ByteArray

Ix/ByteArray.lean

@@ -0,0 +1,12 @@
+namespace ByteArray
+
+def beqNoFFI (a b : ByteArray) : Bool :=
+ a.data == b.data
+
+@[extern "lean_byte_array_beq"]
+def beq : @& ByteArray → @& ByteArray → Bool :=
+ beqNoFFI
+
+instance : BEq ByteArray := ⟨ByteArray.beq⟩
+
+end ByteArray

Ix/Ixon.lean

@@ -1,11 +1,6 @@
-
 import Ix.Address
 import Lean.Declaration
 import Ix.Ixon.Serialize
 import Ix.Ixon.Univ
 import Ix.Ixon.Expr
 import Ix.Ixon.Const
-
-
-
-

Ix/Ixon/Const.lean

@@ -1,4 +1,3 @@
-
 import Ix.Address
 import Lean.Declaration
 import Ix.Ixon.Serialize

Ix/Ixon/Expr.lean

@@ -1,4 +1,3 @@
-
 import Ix.Address
 import Lean.Declaration
 import Ix.Ixon.Serialize
@@ -9,7 +8,7 @@ namespace Ixon
 -- 0xTTTT_LXXX
 inductive Expr where
  -- 0x0, ^1
- | vari (idx: UInt64) : Expr
+ | vari (idx: UInt64) : Expr
  -- 0x1, {max (add 1 2) (var 1)}
  | sort (univ: Univ) : Expr
  -- 0x2 #dead_beef_cafe_babe {u1, u2, ... }
@@ -24,7 +23,7 @@ inductive Expr where
  | alls (types: List Expr) (body: Expr) : Expr
  -- 0x7 (let d : A in b)
  | let_ (type: Expr) (defn: Expr) (body: Expr) : Expr
- -- 0x8 .1
+ -- 0x8 .1
  | proj : UInt64 -> Expr -> Expr
  -- 0x9 "foobar"
  | strl (lit: String) : Expr
@@ -33,7 +32,7 @@ inductive Expr where
 -- array: 0xB
 -- const: 0xC
 
-def putExprTag (tag: UInt8) (val: UInt64) : PutM Unit :=
+def putExprTag (tag: UInt8) (val: UInt64) : PutM Unit :=
  let t := UInt8.shiftLeft tag 4
  if val < 8
  then putUInt8 (UInt8.lor t (Nat.toUInt8 (UInt64.toNat val))) *> pure ()

Ix/Ixon/Serialize.lean

@@ -1,4 +1,3 @@
-
 namespace Ixon
 
 class Serialize (A: Type) where
@@ -13,7 +12,7 @@ structure GetState where
 
 abbrev GetM A := EStateM String GetState A
 
-def runGet (getm: GetM A) (bytes: ByteArray) : Except String A :=
+def runGet (getm: GetM A) (bytes: ByteArray) : Except String A :=
  match EStateM.run getm { index := 0, bytes } with
  | .ok a _ => .ok a
  | .error e _ => .error e

README.md

@@ -1 +1,3 @@
-# ix
+# ix
+
+A verifiable computing platform

Tests/Blake3.lean

@@ -0,0 +1,16 @@
+import LSpec
+import Ix.Blake3
+
+def pairs : List $ (List UInt8 × List UInt8) := [
+ ([0], [ 45, 58, 222, 223, 241, 27, 97, 241,
+ 76, 136, 110, 53, 175, 160, 54, 115,
+ 109, 205, 135, 167, 77, 39, 181, 193,
+ 81, 2, 37, 208, 245, 146, 226, 19,])
+]
+
+open LSpec in
+def main := lspecIO $
+ pairs.foldl (init := .done) fun tSeq (i, o) =>
+ let input := ByteArray.mk ⟨i⟩
+ let output := ByteArray.mk ⟨o⟩
+ tSeq ++ (test s!"blake3 on {input}" $ input.blake3.data = output.data)

Tests/ByteArray.lean

@@ -0,0 +1,22 @@
+import LSpec
+import Ix.ByteArray
+
+def arrays : List ByteArray := [
+ ⟨#[]⟩, ⟨#[1]⟩, ⟨#[0, 3]⟩, ⟨#[1, 1, 1]⟩, ⟨#[3, 3, 3, 3]⟩, ⟨#[13]⟩
+]
+
+def arrays' : List ByteArray := [
+ ⟨#[1]⟩, ⟨#[2]⟩, ⟨#[0, 3, 0]⟩, ⟨#[1, 2, 1]⟩, ⟨#[3, 3, 4, 3]⟩, ⟨#[13, 0]⟩
+]
+
+open LSpec
+
+def beq : TestSeq :=
+ arrays.zip arrays |>.foldl (init := .done) fun tSeq (x, y) =>
+ tSeq ++ (test s!"{x} == {y}" $ x.beq y && x.beqNoFFI y && y.beq x && y.beqNoFFI x)
+
+def neq : TestSeq :=
+ arrays.zip arrays.reverse |>.foldl (init := .done) fun tSeq (x, y) =>
+ tSeq ++ (test s!"{x} != {y}" $ !x.beq y && !x.beqNoFFI y && !y.beq x && !y.beqNoFFI x)
+
+def main := lspecIO $ beq ++ neq

deny.toml

@@ -92,6 +92,7 @@ allow = [
  "MIT",
  "Apache-2.0",
  "Unicode-3.0",
+ "BSD-2-Clause",
  "BSD-3-Clause",
  "CC0-1.0",
  "Zlib",

ffi.c

@@ -0,0 +1,39 @@
+#include <lean/lean.h>
+#include <string.h>
+
+#define intern inline static
+#define l_arg b_lean_obj_arg
+#define l_res lean_obj_res
+
+// Interfaces targeting Rust implementations
+
+void blake3(uint8_t*, size_t, uint8_t*);
+
+// Auxiliary implementations
+
+intern lean_sarray_object* mk_byte_array(size_t len) {
+ lean_sarray_object* o = (lean_sarray_object*)lean_alloc_object(
+ sizeof(lean_sarray_object) + len
+ );
+ lean_set_st_header((lean_object*)o, LeanScalarArray, 1);
+ o->m_size = len;
+ o->m_capacity = len;
+ return o;
+}
+
+// Implementations to serve Lean 4
+
+extern l_res lean_byte_array_blake3(l_arg a) {
+ lean_sarray_object* oa = lean_to_sarray(a);
+ lean_sarray_object* res = mk_byte_array(32);
+ blake3(res->m_data, oa->m_size, oa->m_data);
+ return (lean_object*)res;
+}
+
+extern bool lean_byte_array_beq(l_arg a, l_arg b) {
+ lean_sarray_object* oa = lean_to_sarray(a);
+ lean_sarray_object* ob = lean_to_sarray(b);
+ size_t sa = oa->m_size;
+ if (sa == ob->m_size) return memcmp(oa->m_data, ob->m_data, sa) == 0;
+ return false;
+}

lake-manifest.json

@@ -1,5 +1,15 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
- "packages": [],
+ "packages":
+ [{"url": "https://github.com/argumentcomputer/LSpec",
+ "type": "git",
+ "subDir": null,
+ "scope": "",
+ "rev": "ca8e2803f89f0c12bf9743ae7abbfb2ea6b0eeec",
+ "name": "LSpec",
+ "manifestFile": "lake-manifest.json",
+ "inputRev": "ca8e2803f89f0c12bf9743ae7abbfb2ea6b0eeec",
+ "inherited": false,
+ "configFile": "lakefile.toml"}],
  "name": "ix",
  "lakeDir": ".lake"}

lakefile.lean

@@ -0,0 +1,43 @@
+import Lake
+open System Lake DSL
+
+package ix where
+ version := v!"0.1.0"
+
+lean_lib Ix
+
+@[default_target]
+lean_exe ix where
+ root := `Main
+
+require LSpec from git
+ "https://github.com/argumentcomputer/LSpec" @ "ca8e2803f89f0c12bf9743ae7abbfb2ea6b0eeec"
+
+section Tests
+
+lean_exe Tests.Blake3
+lean_exe Tests.ByteArray
+
+end Tests
+
+section FFI
+
+target ffi.o pkg : FilePath := do
+ let oFile := pkg.buildDir / "ffi.o"
+ let srcJob ← inputTextFile "ffi.c"
+ let includeDir ← getLeanIncludeDir
+ let weakArgs := #["-I", includeDir.toString]
+ buildO oFile srcJob weakArgs #["-fPIC"] "cc" getLeanTrace
+
+extern_lib liblean_ffi pkg := do
+ let name := nameToStaticLib "ffi"
+ let ffiO ← ffi.o.fetch
+ buildStaticLib (pkg.nativeLibDir / name) #[ffiO]
+
+extern_lib rust_ffi pkg := do
+ proc { cmd := "cargo", args := #["build", "--release"], cwd := pkg.dir }
+ let name := nameToStaticLib "ix"
+ let srcPath := pkg.dir / "target" / "release" / name
+ return pure srcPath
+
+end FFI

src/lib.rs

@@ -1,5 +1,14 @@
 pub mod eiur;
 
+use blake3::hash;
+
+#[no_mangle]
+extern "C" fn blake3(mem: &mut [u8; 32], len: usize, input: *const u8) {
+ unsafe {
+ *mem = *hash(std::slice::from_raw_parts(input, len)).as_bytes();
+ }
+}
+
 #[cfg(test)]
 mod tests {
  #[test]

.github/workflows/ci.yml

@@ -47,7 +47,5 @@ jobs:
  # TODO: Add '.cargo/config' for list of enabled/disabled `xclippy`lints
  - name: Check clippy warnings
  run: cargo clippy -- -D warnings
- - name: Doctests
- run: cargo test --doc --workspace
  - name: Cargo-deny
  uses: EmbarkStudios/cargo-deny-action@v2

.github/workflows/lspec.yml

@@ -0,0 +1,20 @@
+name: "LSpec CI"
+on:
+ pull_request:
+ push:
+ branches:
+ - main
+jobs:
+ build:
+ name: Build
+ runs-on: ubuntu-latest
+ steps:
+ - name: install elan
+ run: |
+ set -o pipefail
+ curl -sSfL https://github.com/leanprover/elan/releases/download/v4.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+ ./elan-init -y --default-toolchain none
+ echo "$HOME/.elan/bin" >> $GITHUB_PATH
+ - uses: actions/checkout@v4
+ - name: run LSpec binary
+ run: lake exe lspec

Cargo.toml

@@ -3,15 +3,19 @@ name = "ix"
 version = "0.1.0"
 edition = "2021"
 
+[lib]
+crate-type = ["staticlib"]
+
 [dependencies]
 anyhow = "1"
-rustc-hash = "2"
 binius_core = { git = "https://gitlab.com/IrreducibleOSS/binius.git", rev = "0e5ec53f260f40fe6afcc741d4ff8f021a66dc1a" }
 binius_circuits = { git = "https://gitlab.com/IrreducibleOSS/binius.git", rev = "0e5ec53f260f40fe6afcc741d4ff8f021a66dc1a" }
 binius_field = { git = "https://gitlab.com/IrreducibleOSS/binius.git", rev = "0e5ec53f260f40fe6afcc741d4ff8f021a66dc1a" }
 binius_macros = { git = "https://gitlab.com/IrreducibleOSS/binius.git", rev = "0e5ec53f260f40fe6afcc741d4ff8f021a66dc1a" }
 binius_math = { git = "https://gitlab.com/IrreducibleOSS/binius.git", rev = "0e5ec53f260f40fe6afcc741d4ff8f021a66dc1a" }
+blake3 = "1"
 bytemuck = "1"
 bumpalo = "3"
 proptest = "1"
 rayon = "1"
+rustc-hash = "2"

Ix/Address.lean

@@ -1,3 +1,2 @@
-
 structure Address where
  adr : ByteArray

Ix/Blake3.lean

@@ -0,0 +1,2 @@
+@[extern "lean_byte_array_blake3"]
+opaque ByteArray.blake3 : @& ByteArray → ByteArray

Ix/ByteArray.lean

@@ -0,0 +1,12 @@
+namespace ByteArray
+
+def beqNoFFI (a b : ByteArray) : Bool :=
+ a.data == b.data
+
+@[extern "lean_byte_array_beq"]
+def beq : @& ByteArray → @& ByteArray → Bool :=
+ beqNoFFI
+
+instance : BEq ByteArray := ⟨ByteArray.beq⟩
+
+end ByteArray

Ix/Ixon.lean

@@ -1,11 +1,6 @@
-
 import Ix.Address
 import Lean.Declaration
 import Ix.Ixon.Serialize
 import Ix.Ixon.Univ
 import Ix.Ixon.Expr
 import Ix.Ixon.Const
-
-
-
-

Ix/Ixon/Const.lean

@@ -1,4 +1,3 @@
-
 import Ix.Address
 import Lean.Declaration
 import Ix.Ixon.Serialize

Ix/Ixon/Expr.lean

@@ -1,4 +1,3 @@
-
 import Ix.Address
 import Lean.Declaration
 import Ix.Ixon.Serialize
@@ -9,7 +8,7 @@ namespace Ixon
 -- 0xTTTT_LXXX
 inductive Expr where
  -- 0x0, ^1
- | vari (idx: UInt64) : Expr
+ | vari (idx: UInt64) : Expr
  -- 0x1, {max (add 1 2) (var 1)}
  | sort (univ: Univ) : Expr
  -- 0x2 #dead_beef_cafe_babe {u1, u2, ... }
@@ -24,7 +23,7 @@ inductive Expr where
  | alls (types: List Expr) (body: Expr) : Expr
  -- 0x7 (let d : A in b)
  | let_ (type: Expr) (defn: Expr) (body: Expr) : Expr
- -- 0x8 .1
+ -- 0x8 .1
  | proj : UInt64 -> Expr -> Expr
  -- 0x9 "foobar"
  | strl (lit: String) : Expr
@@ -33,7 +32,7 @@ inductive Expr where
 -- array: 0xB
 -- const: 0xC
 
-def putExprTag (tag: UInt8) (val: UInt64) : PutM Unit :=
+def putExprTag (tag: UInt8) (val: UInt64) : PutM Unit :=
  let t := UInt8.shiftLeft tag 4
  if val < 8
  then putUInt8 (UInt8.lor t (Nat.toUInt8 (UInt64.toNat val))) *> pure ()

Ix/Ixon/Serialize.lean

@@ -1,4 +1,3 @@
-
 namespace Ixon
 
 class Serialize (A: Type) where
@@ -13,7 +12,7 @@ structure GetState where
 
 abbrev GetM A := EStateM String GetState A
 
-def runGet (getm: GetM A) (bytes: ByteArray) : Except String A :=
+def runGet (getm: GetM A) (bytes: ByteArray) : Except String A :=
  match EStateM.run getm { index := 0, bytes } with
  | .ok a _ => .ok a
  | .error e _ => .error e

README.md

@@ -1 +1,3 @@
-# ix
+# ix
+
+A verifiable computing platform

Tests/Blake3.lean

@@ -0,0 +1,16 @@
+import LSpec
+import Ix.Blake3
+
+def pairs : List $ (List UInt8 × List UInt8) := [
+ ([0], [ 45, 58, 222, 223, 241, 27, 97, 241,
+ 76, 136, 110, 53, 175, 160, 54, 115,
+ 109, 205, 135, 167, 77, 39, 181, 193,
+ 81, 2, 37, 208, 245, 146, 226, 19,])
+]
+
+open LSpec in
+def main := lspecIO $
+ pairs.foldl (init := .done) fun tSeq (i, o) =>
+ let input := ByteArray.mk ⟨i⟩
+ let output := ByteArray.mk ⟨o⟩
+ tSeq ++ (test s!"blake3 on {input}" $ input.blake3.data = output.data)

Tests/ByteArray.lean

@@ -0,0 +1,22 @@
+import LSpec
+import Ix.ByteArray
+
+def arrays : List ByteArray := [
+ ⟨#[]⟩, ⟨#[1]⟩, ⟨#[0, 3]⟩, ⟨#[1, 1, 1]⟩, ⟨#[3, 3, 3, 3]⟩, ⟨#[13]⟩
+]
+
+def arrays' : List ByteArray := [
+ ⟨#[1]⟩, ⟨#[2]⟩, ⟨#[0, 3, 0]⟩, ⟨#[1, 2, 1]⟩, ⟨#[3, 3, 4, 3]⟩, ⟨#[13, 0]⟩
+]
+
+open LSpec
+
+def beq : TestSeq :=
+ arrays.zip arrays |>.foldl (init := .done) fun tSeq (x, y) =>
+ tSeq ++ (test s!"{x} == {y}" $ x.beq y && x.beqNoFFI y && y.beq x && y.beqNoFFI x)
+
+def neq : TestSeq :=
+ arrays.zip arrays.reverse |>.foldl (init := .done) fun tSeq (x, y) =>
+ tSeq ++ (test s!"{x} != {y}" $ !x.beq y && !x.beqNoFFI y && !y.beq x && !y.beqNoFFI x)
+
+def main := lspecIO $ beq ++ neq

deny.toml

@@ -92,6 +92,7 @@ allow = [
  "MIT",
  "Apache-2.0",
  "Unicode-3.0",
+ "BSD-2-Clause",
  "BSD-3-Clause",
  "CC0-1.0",
  "Zlib",

ffi.c

@@ -0,0 +1,39 @@
+#include <lean/lean.h>
+#include <string.h>
+
+#define intern inline static
+#define l_arg b_lean_obj_arg
+#define l_res lean_obj_res
+
+// Interfaces targeting Rust implementations
+
+void blake3(uint8_t*, size_t, uint8_t*);
+
+// Auxiliary implementations
+
+intern lean_sarray_object* mk_byte_array(size_t len) {
+ lean_sarray_object* o = (lean_sarray_object*)lean_alloc_object(
+ sizeof(lean_sarray_object) + len
+ );
+ lean_set_st_header((lean_object*)o, LeanScalarArray, 1);
+ o->m_size = len;
+ o->m_capacity = len;
+ return o;
+}
+
+// Implementations to serve Lean 4
+
+extern l_res lean_byte_array_blake3(l_arg a) {
+ lean_sarray_object* oa = lean_to_sarray(a);
+ lean_sarray_object* res = mk_byte_array(32);
+ blake3(res->m_data, oa->m_size, oa->m_data);
+ return (lean_object*)res;
+}
+
+extern bool lean_byte_array_beq(l_arg a, l_arg b) {
+ lean_sarray_object* oa = lean_to_sarray(a);
+ lean_sarray_object* ob = lean_to_sarray(b);
+ size_t sa = oa->m_size;
+ if (sa == ob->m_size) return memcmp(oa->m_data, ob->m_data, sa) == 0;
+ return false;
+}

lake-manifest.json

@@ -1,5 +1,15 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
- "packages": [],
+ "packages":
+ [{"url": "https://github.com/argumentcomputer/LSpec",
+ "type": "git",
+ "subDir": null,
+ "scope": "",
+ "rev": "ca8e2803f89f0c12bf9743ae7abbfb2ea6b0eeec",
+ "name": "LSpec",
+ "manifestFile": "lake-manifest.json",
+ "inputRev": "ca8e2803f89f0c12bf9743ae7abbfb2ea6b0eeec",
+ "inherited": false,
+ "configFile": "lakefile.toml"}],
  "name": "ix",
  "lakeDir": ".lake"}

lakefile.lean

@@ -0,0 +1,43 @@
+import Lake
+open System Lake DSL
+
+package ix where
+ version := v!"0.1.0"
+
+lean_lib Ix
+
+@[default_target]
+lean_exe ix where
+ root := `Main
+
+require LSpec from git
+ "https://github.com/argumentcomputer/LSpec" @ "ca8e2803f89f0c12bf9743ae7abbfb2ea6b0eeec"
+
+section Tests
+
+lean_exe Tests.Blake3
+lean_exe Tests.ByteArray
+
+end Tests
+
+section FFI
+
+target ffi.o pkg : FilePath := do
+ let oFile := pkg.buildDir / "ffi.o"
+ let srcJob ← inputTextFile "ffi.c"
+ let includeDir ← getLeanIncludeDir
+ let weakArgs := #["-I", includeDir.toString]
+ buildO oFile srcJob weakArgs #["-fPIC"] "cc" getLeanTrace
+
+extern_lib liblean_ffi pkg := do
+ let name := nameToStaticLib "ffi"
+ let ffiO ← ffi.o.fetch
+ buildStaticLib (pkg.nativeLibDir / name) #[ffiO]
+
+extern_lib rust_ffi pkg := do
+ proc { cmd := "cargo", args := #["build", "--release"], cwd := pkg.dir }
+ let name := nameToStaticLib "ix"
+ let srcPath := pkg.dir / "target" / "release" / name
+ return pure srcPath
+
+end FFI

src/lib.rs

@@ -1,5 +1,14 @@
 pub mod eiur;
 
+use blake3::hash;
+
+#[no_mangle]
+extern "C" fn blake3(mem: &mut [u8; 32], len: usize, input: *const u8) {
+ unsafe {
+ *mem = *hash(std::slice::from_raw_parts(input, len)).as_bytes();
+ }
+}
+
 #[cfg(test)]
 mod tests {
  #[test]

.github/workflows/ci.yml

@@ -47,7 +47,5 @@ jobs:
  # TODO: Add '.cargo/config' for list of enabled/disabled `xclippy`lints
  - name: Check clippy warnings
  run: cargo clippy -- -D warnings
- - name: Doctests
- run: cargo test --doc --workspace
  - name: Cargo-deny
  uses: EmbarkStudios/cargo-deny-action@v2

.github/workflows/lspec.yml

@@ -0,0 +1,20 @@
+name: "LSpec CI"
+on:
+ pull_request:
+ push:
+ branches:
+ - main
+jobs:
+ build:
+ name: Build
+ runs-on: ubuntu-latest
+ steps:
+ - name: install elan
+ run: |
+ set -o pipefail
+ curl -sSfL https://github.com/leanprover/elan/releases/download/v4.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+ ./elan-init -y --default-toolchain none
+ echo "$HOME/.elan/bin" >> $GITHUB_PATH
+ - uses: actions/checkout@v4
+ - name: run LSpec binary
+ run: lake exe lspec

Cargo.toml

@@ -3,15 +3,19 @@ name = "ix"
 version = "0.1.0"
 edition = "2021"
 
+[lib]
+crate-type = ["staticlib"]
+
 [dependencies]
 anyhow = "1"
-rustc-hash = "2"
 binius_core = { git = "https://gitlab.com/IrreducibleOSS/binius.git", rev = "0e5ec53f260f40fe6afcc741d4ff8f021a66dc1a" }
 binius_circuits = { git = "https://gitlab.com/IrreducibleOSS/binius.git", rev = "0e5ec53f260f40fe6afcc741d4ff8f021a66dc1a" }
 binius_field = { git = "https://gitlab.com/IrreducibleOSS/binius.git", rev = "0e5ec53f260f40fe6afcc741d4ff8f021a66dc1a" }
 binius_macros = { git = "https://gitlab.com/IrreducibleOSS/binius.git", rev = "0e5ec53f260f40fe6afcc741d4ff8f021a66dc1a" }
 binius_math = { git = "https://gitlab.com/IrreducibleOSS/binius.git", rev = "0e5ec53f260f40fe6afcc741d4ff8f021a66dc1a" }
+blake3 = "1"
 bytemuck = "1"
 bumpalo = "3"
 proptest = "1"
 rayon = "1"
+rustc-hash = "2"

Ix/Address.lean

@@ -1,3 +1,2 @@
-
 structure Address where
  adr : ByteArray

Ix/Blake3.lean

@@ -0,0 +1,2 @@
+@[extern "lean_byte_array_blake3"]
+opaque ByteArray.blake3 : @& ByteArray → ByteArray

Ix/ByteArray.lean

@@ -0,0 +1,12 @@
+namespace ByteArray
+
+def beqNoFFI (a b : ByteArray) : Bool :=
+ a.data == b.data
+
+@[extern "lean_byte_array_beq"]
+def beq : @& ByteArray → @& ByteArray → Bool :=
+ beqNoFFI
+
+instance : BEq ByteArray := ⟨ByteArray.beq⟩
+
+end ByteArray

Ix/Ixon.lean

@@ -1,11 +1,6 @@
-
 import Ix.Address
 import Lean.Declaration
 import Ix.Ixon.Serialize
 import Ix.Ixon.Univ
 import Ix.Ixon.Expr
 import Ix.Ixon.Const
-
-
-
-

Ix/Ixon/Const.lean

@@ -1,4 +1,3 @@
-
 import Ix.Address
 import Lean.Declaration
 import Ix.Ixon.Serialize

Ix/Ixon/Expr.lean

@@ -1,4 +1,3 @@
-
 import Ix.Address
 import Lean.Declaration
 import Ix.Ixon.Serialize
@@ -9,7 +8,7 @@ namespace Ixon
 -- 0xTTTT_LXXX
 inductive Expr where
  -- 0x0, ^1
- | vari (idx: UInt64) : Expr
+ | vari (idx: UInt64) : Expr
  -- 0x1, {max (add 1 2) (var 1)}
  | sort (univ: Univ) : Expr
  -- 0x2 #dead_beef_cafe_babe {u1, u2, ... }
@@ -24,7 +23,7 @@ inductive Expr where
  | alls (types: List Expr) (body: Expr) : Expr
  -- 0x7 (let d : A in b)
  | let_ (type: Expr) (defn: Expr) (body: Expr) : Expr
- -- 0x8 .1
+ -- 0x8 .1
  | proj : UInt64 -> Expr -> Expr
  -- 0x9 "foobar"
  | strl (lit: String) : Expr
@@ -33,7 +32,7 @@ inductive Expr where
 -- array: 0xB
 -- const: 0xC
 
-def putExprTag (tag: UInt8) (val: UInt64) : PutM Unit :=
+def putExprTag (tag: UInt8) (val: UInt64) : PutM Unit :=
  let t := UInt8.shiftLeft tag 4
  if val < 8
  then putUInt8 (UInt8.lor t (Nat.toUInt8 (UInt64.toNat val))) *> pure ()

Ix/Ixon/Serialize.lean

@@ -1,4 +1,3 @@
-
 namespace Ixon
 
 class Serialize (A: Type) where
@@ -13,7 +12,7 @@ structure GetState where
 
 abbrev GetM A := EStateM String GetState A
 
-def runGet (getm: GetM A) (bytes: ByteArray) : Except String A :=
+def runGet (getm: GetM A) (bytes: ByteArray) : Except String A :=
  match EStateM.run getm { index := 0, bytes } with
  | .ok a _ => .ok a
  | .error e _ => .error e

README.md

@@ -1 +1,3 @@
-# ix
+# ix
+
+A verifiable computing platform

Tests/Blake3.lean

@@ -0,0 +1,16 @@
+import LSpec
+import Ix.Blake3
+
+def pairs : List $ (List UInt8 × List UInt8) := [
+ ([0], [ 45, 58, 222, 223, 241, 27, 97, 241,
+ 76, 136, 110, 53, 175, 160, 54, 115,
+ 109, 205, 135, 167, 77, 39, 181, 193,
+ 81, 2, 37, 208, 245, 146, 226, 19,])
+]
+
+open LSpec in
+def main := lspecIO $
+ pairs.foldl (init := .done) fun tSeq (i, o) =>
+ let input := ByteArray.mk ⟨i⟩
+ let output := ByteArray.mk ⟨o⟩
+ tSeq ++ (test s!"blake3 on {input}" $ input.blake3.data = output.data)

Tests/ByteArray.lean

@@ -0,0 +1,22 @@
+import LSpec
+import Ix.ByteArray
+
+def arrays : List ByteArray := [
+ ⟨#[]⟩, ⟨#[1]⟩, ⟨#[0, 3]⟩, ⟨#[1, 1, 1]⟩, ⟨#[3, 3, 3, 3]⟩, ⟨#[13]⟩
+]
+
+def arrays' : List ByteArray := [
+ ⟨#[1]⟩, ⟨#[2]⟩, ⟨#[0, 3, 0]⟩, ⟨#[1, 2, 1]⟩, ⟨#[3, 3, 4, 3]⟩, ⟨#[13, 0]⟩
+]
+
+open LSpec
+
+def beq : TestSeq :=
+ arrays.zip arrays |>.foldl (init := .done) fun tSeq (x, y) =>
+ tSeq ++ (test s!"{x} == {y}" $ x.beq y && x.beqNoFFI y && y.beq x && y.beqNoFFI x)
+
+def neq : TestSeq :=
+ arrays.zip arrays.reverse |>.foldl (init := .done) fun tSeq (x, y) =>
+ tSeq ++ (test s!"{x} != {y}" $ !x.beq y && !x.beqNoFFI y && !y.beq x && !y.beqNoFFI x)
+
+def main := lspecIO $ beq ++ neq

deny.toml

@@ -92,6 +92,7 @@ allow = [
  "MIT",
  "Apache-2.0",
  "Unicode-3.0",
+ "BSD-2-Clause",
  "BSD-3-Clause",
  "CC0-1.0",
  "Zlib",

ffi.c

@@ -0,0 +1,39 @@
+#include <lean/lean.h>
+#include <string.h>
+
+#define intern inline static
+#define l_arg b_lean_obj_arg
+#define l_res lean_obj_res
+
+// Interfaces targeting Rust implementations
+
+void blake3(uint8_t*, size_t, uint8_t*);
+
+// Auxiliary implementations
+
+intern lean_sarray_object* mk_byte_array(size_t len) {
+ lean_sarray_object* o = (lean_sarray_object*)lean_alloc_object(
+ sizeof(lean_sarray_object) + len
+ );
+ lean_set_st_header((lean_object*)o, LeanScalarArray, 1);
+ o->m_size = len;
+ o->m_capacity = len;
+ return o;
+}
+
+// Implementations to serve Lean 4
+
+extern l_res lean_byte_array_blake3(l_arg a) {
+ lean_sarray_object* oa = lean_to_sarray(a);
+ lean_sarray_object* res = mk_byte_array(32);
+ blake3(res->m_data, oa->m_size, oa->m_data);
+ return (lean_object*)res;
+}
+
+extern bool lean_byte_array_beq(l_arg a, l_arg b) {
+ lean_sarray_object* oa = lean_to_sarray(a);
+ lean_sarray_object* ob = lean_to_sarray(b);
+ size_t sa = oa->m_size;
+ if (sa == ob->m_size) return memcmp(oa->m_data, ob->m_data, sa) == 0;
+ return false;
+}

lake-manifest.json

@@ -1,5 +1,15 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
- "packages": [],
+ "packages":
+ [{"url": "https://github.com/argumentcomputer/LSpec",
+ "type": "git",
+ "subDir": null,
+ "scope": "",
+ "rev": "ca8e2803f89f0c12bf9743ae7abbfb2ea6b0eeec",
+ "name": "LSpec",
+ "manifestFile": "lake-manifest.json",
+ "inputRev": "ca8e2803f89f0c12bf9743ae7abbfb2ea6b0eeec",
+ "inherited": false,
+ "configFile": "lakefile.toml"}],
  "name": "ix",
  "lakeDir": ".lake"}

lakefile.lean

@@ -0,0 +1,43 @@
+import Lake
+open System Lake DSL
+
+package ix where
+ version := v!"0.1.0"
+
+lean_lib Ix
+
+@[default_target]
+lean_exe ix where
+ root := `Main
+
+require LSpec from git
+ "https://github.com/argumentcomputer/LSpec" @ "ca8e2803f89f0c12bf9743ae7abbfb2ea6b0eeec"
+
+section Tests
+
+lean_exe Tests.Blake3
+lean_exe Tests.ByteArray
+
+end Tests
+
+section FFI
+
+target ffi.o pkg : FilePath := do
+ let oFile := pkg.buildDir / "ffi.o"
+ let srcJob ← inputTextFile "ffi.c"
+ let includeDir ← getLeanIncludeDir
+ let weakArgs := #["-I", includeDir.toString]
+ buildO oFile srcJob weakArgs #["-fPIC"] "cc" getLeanTrace
+
+extern_lib liblean_ffi pkg := do
+ let name := nameToStaticLib "ffi"
+ let ffiO ← ffi.o.fetch
+ buildStaticLib (pkg.nativeLibDir / name) #[ffiO]
+
+extern_lib rust_ffi pkg := do
+ proc { cmd := "cargo", args := #["build", "--release"], cwd := pkg.dir }
+ let name := nameToStaticLib "ix"
+ let srcPath := pkg.dir / "target" / "release" / name
+ return pure srcPath
+
+end FFI

src/lib.rs

@@ -1,5 +1,14 @@
 pub mod eiur;
 
+use blake3::hash;
+
+#[no_mangle]
+extern "C" fn blake3(mem: &mut [u8; 32], len: usize, input: *const u8) {
+ unsafe {
+ *mem = *hash(std::slice::from_raw_parts(input, len)).as_bytes();
+ }
+}
+
 #[cfg(test)]
 mod tests {
  #[test]

.github/workflows/ci.yml

@@ -47,7 +47,5 @@ jobs:
  # TODO: Add '.cargo/config' for list of enabled/disabled `xclippy`lints
  - name: Check clippy warnings
  run: cargo clippy -- -D warnings
- - name: Doctests
- run: cargo test --doc --workspace
  - name: Cargo-deny
  uses: EmbarkStudios/cargo-deny-action@v2

.github/workflows/lspec.yml

@@ -0,0 +1,20 @@
+name: "LSpec CI"
+on:
+ pull_request:
+ push:
+ branches:
+ - main
+jobs:
+ build:
+ name: Build
+ runs-on: ubuntu-latest
+ steps:
+ - name: install elan
+ run: |
+ set -o pipefail
+ curl -sSfL https://github.com/leanprover/elan/releases/download/v4.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+ ./elan-init -y --default-toolchain none
+ echo "$HOME/.elan/bin" >> $GITHUB_PATH
+ - uses: actions/checkout@v4
+ - name: run LSpec binary
+ run: lake exe lspec

Cargo.toml

@@ -3,15 +3,19 @@ name = "ix"
 version = "0.1.0"
 edition = "2021"
 
+[lib]
+crate-type = ["staticlib"]
+
 [dependencies]
 anyhow = "1"
-rustc-hash = "2"
 binius_core = { git = "https://gitlab.com/IrreducibleOSS/binius.git", rev = "0e5ec53f260f40fe6afcc741d4ff8f021a66dc1a" }
 binius_circuits = { git = "https://gitlab.com/IrreducibleOSS/binius.git", rev = "0e5ec53f260f40fe6afcc741d4ff8f021a66dc1a" }
 binius_field = { git = "https://gitlab.com/IrreducibleOSS/binius.git", rev = "0e5ec53f260f40fe6afcc741d4ff8f021a66dc1a" }
 binius_macros = { git = "https://gitlab.com/IrreducibleOSS/binius.git", rev = "0e5ec53f260f40fe6afcc741d4ff8f021a66dc1a" }
 binius_math = { git = "https://gitlab.com/IrreducibleOSS/binius.git", rev = "0e5ec53f260f40fe6afcc741d4ff8f021a66dc1a" }
+blake3 = "1"
 bytemuck = "1"
 bumpalo = "3"
 proptest = "1"
 rayon = "1"
+rustc-hash = "2"

Ix/Address.lean

@@ -1,3 +1,2 @@
-
 structure Address where
  adr : ByteArray

Ix/Blake3.lean

@@ -0,0 +1,2 @@
+@[extern "lean_byte_array_blake3"]
+opaque ByteArray.blake3 : @& ByteArray → ByteArray

Ix/ByteArray.lean

@@ -0,0 +1,12 @@
+namespace ByteArray
+
+def beqNoFFI (a b : ByteArray) : Bool :=
+ a.data == b.data
+
+@[extern "lean_byte_array_beq"]
+def beq : @& ByteArray → @& ByteArray → Bool :=
+ beqNoFFI
+
+instance : BEq ByteArray := ⟨ByteArray.beq⟩
+
+end ByteArray

Ix/Ixon.lean

@@ -1,11 +1,6 @@
-
 import Ix.Address
 import Lean.Declaration
 import Ix.Ixon.Serialize
 import Ix.Ixon.Univ
 import Ix.Ixon.Expr
 import Ix.Ixon.Const
-
-
-
-

Ix/Ixon/Const.lean

@@ -1,4 +1,3 @@
-
 import Ix.Address
 import Lean.Declaration
 import Ix.Ixon.Serialize

Ix/Ixon/Expr.lean

@@ -1,4 +1,3 @@
-
 import Ix.Address
 import Lean.Declaration
 import Ix.Ixon.Serialize
@@ -9,7 +8,7 @@ namespace Ixon
 -- 0xTTTT_LXXX
 inductive Expr where
  -- 0x0, ^1
- | vari (idx: UInt64) : Expr
+ | vari (idx: UInt64) : Expr
  -- 0x1, {max (add 1 2) (var 1)}
  | sort (univ: Univ) : Expr
  -- 0x2 #dead_beef_cafe_babe {u1, u2, ... }
@@ -24,7 +23,7 @@ inductive Expr where
  | alls (types: List Expr) (body: Expr) : Expr
  -- 0x7 (let d : A in b)
  | let_ (type: Expr) (defn: Expr) (body: Expr) : Expr
- -- 0x8 .1
+ -- 0x8 .1
  | proj : UInt64 -> Expr -> Expr
  -- 0x9 "foobar"
  | strl (lit: String) : Expr
@@ -33,7 +32,7 @@ inductive Expr where
 -- array: 0xB
 -- const: 0xC
 
-def putExprTag (tag: UInt8) (val: UInt64) : PutM Unit :=
+def putExprTag (tag: UInt8) (val: UInt64) : PutM Unit :=
  let t := UInt8.shiftLeft tag 4
  if val < 8
  then putUInt8 (UInt8.lor t (Nat.toUInt8 (UInt64.toNat val))) *> pure ()

Ix/Ixon/Serialize.lean

@@ -1,4 +1,3 @@
-
 namespace Ixon
 
 class Serialize (A: Type) where
@@ -13,7 +12,7 @@ structure GetState where
 
 abbrev GetM A := EStateM String GetState A
 
-def runGet (getm: GetM A) (bytes: ByteArray) : Except String A :=
+def runGet (getm: GetM A) (bytes: ByteArray) : Except String A :=
  match EStateM.run getm { index := 0, bytes } with
  | .ok a _ => .ok a
  | .error e _ => .error e

README.md

@@ -1 +1,3 @@
-# ix
+# ix
+
+A verifiable computing platform

Tests/Blake3.lean

@@ -0,0 +1,16 @@
+import LSpec
+import Ix.Blake3
+
+def pairs : List $ (List UInt8 × List UInt8) := [
+ ([0], [ 45, 58, 222, 223, 241, 27, 97, 241,
+ 76, 136, 110, 53, 175, 160, 54, 115,
+ 109, 205, 135, 167, 77, 39, 181, 193,
+ 81, 2, 37, 208, 245, 146, 226, 19,])
+]
+
+open LSpec in
+def main := lspecIO $
+ pairs.foldl (init := .done) fun tSeq (i, o) =>
+ let input := ByteArray.mk ⟨i⟩
+ let output := ByteArray.mk ⟨o⟩
+ tSeq ++ (test s!"blake3 on {input}" $ input.blake3.data = output.data)

Tests/ByteArray.lean

@@ -0,0 +1,22 @@
+import LSpec
+import Ix.ByteArray
+
+def arrays : List ByteArray := [
+ ⟨#[]⟩, ⟨#[1]⟩, ⟨#[0, 3]⟩, ⟨#[1, 1, 1]⟩, ⟨#[3, 3, 3, 3]⟩, ⟨#[13]⟩
+]
+
+def arrays' : List ByteArray := [
+ ⟨#[1]⟩, ⟨#[2]⟩, ⟨#[0, 3, 0]⟩, ⟨#[1, 2, 1]⟩, ⟨#[3, 3, 4, 3]⟩, ⟨#[13, 0]⟩
+]
+
+open LSpec
+
+def beq : TestSeq :=
+ arrays.zip arrays |>.foldl (init := .done) fun tSeq (x, y) =>
+ tSeq ++ (test s!"{x} == {y}" $ x.beq y && x.beqNoFFI y && y.beq x && y.beqNoFFI x)
+
+def neq : TestSeq :=
+ arrays.zip arrays.reverse |>.foldl (init := .done) fun tSeq (x, y) =>
+ tSeq ++ (test s!"{x} != {y}" $ !x.beq y && !x.beqNoFFI y && !y.beq x && !y.beqNoFFI x)
+
+def main := lspecIO $ beq ++ neq

deny.toml

@@ -92,6 +92,7 @@ allow = [
  "MIT",
  "Apache-2.0",
  "Unicode-3.0",
+ "BSD-2-Clause",
  "BSD-3-Clause",
  "CC0-1.0",
  "Zlib",

ffi.c

@@ -0,0 +1,39 @@
+#include <lean/lean.h>
+#include <string.h>
+
+#define intern inline static
+#define l_arg b_lean_obj_arg
+#define l_res lean_obj_res
+
+// Interfaces targeting Rust implementations
+
+void blake3(uint8_t*, size_t, uint8_t*);
+
+// Auxiliary implementations
+
+intern lean_sarray_object* mk_byte_array(size_t len) {
+ lean_sarray_object* o = (lean_sarray_object*)lean_alloc_object(
+ sizeof(lean_sarray_object) + len
+ );
+ lean_set_st_header((lean_object*)o, LeanScalarArray, 1);
+ o->m_size = len;
+ o->m_capacity = len;
+ return o;
+}
+
+// Implementations to serve Lean 4
+
+extern l_res lean_byte_array_blake3(l_arg a) {
+ lean_sarray_object* oa = lean_to_sarray(a);
+ lean_sarray_object* res = mk_byte_array(32);
+ blake3(res->m_data, oa->m_size, oa->m_data);
+ return (lean_object*)res;
+}
+
+extern bool lean_byte_array_beq(l_arg a, l_arg b) {
+ lean_sarray_object* oa = lean_to_sarray(a);
+ lean_sarray_object* ob = lean_to_sarray(b);
+ size_t sa = oa->m_size;
+ if (sa == ob->m_size) return memcmp(oa->m_data, ob->m_data, sa) == 0;
+ return false;
+}

lake-manifest.json

@@ -1,5 +1,15 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
- "packages": [],
+ "packages":
+ [{"url": "https://github.com/argumentcomputer/LSpec",
+ "type": "git",
+ "subDir": null,
+ "scope": "",
+ "rev": "ca8e2803f89f0c12bf9743ae7abbfb2ea6b0eeec",
+ "name": "LSpec",
+ "manifestFile": "lake-manifest.json",
+ "inputRev": "ca8e2803f89f0c12bf9743ae7abbfb2ea6b0eeec",
+ "inherited": false,
+ "configFile": "lakefile.toml"}],
  "name": "ix",
  "lakeDir": ".lake"}

lakefile.lean

@@ -0,0 +1,43 @@
+import Lake
+open System Lake DSL
+
+package ix where
+ version := v!"0.1.0"
+
+lean_lib Ix
+
+@[default_target]
+lean_exe ix where
+ root := `Main
+
+require LSpec from git
+ "https://github.com/argumentcomputer/LSpec" @ "ca8e2803f89f0c12bf9743ae7abbfb2ea6b0eeec"
+
+section Tests
+
+lean_exe Tests.Blake3
+lean_exe Tests.ByteArray
+
+end Tests
+
+section FFI
+
+target ffi.o pkg : FilePath := do
+ let oFile := pkg.buildDir / "ffi.o"
+ let srcJob ← inputTextFile "ffi.c"
+ let includeDir ← getLeanIncludeDir
+ let weakArgs := #["-I", includeDir.toString]
+ buildO oFile srcJob weakArgs #["-fPIC"] "cc" getLeanTrace
+
+extern_lib liblean_ffi pkg := do
+ let name := nameToStaticLib "ffi"
+ let ffiO ← ffi.o.fetch
+ buildStaticLib (pkg.nativeLibDir / name) #[ffiO]
+
+extern_lib rust_ffi pkg := do
+ proc { cmd := "cargo", args := #["build", "--release"], cwd := pkg.dir }
+ let name := nameToStaticLib "ix"
+ let srcPath := pkg.dir / "target" / "release" / name
+ return pure srcPath
+
+end FFI

src/lib.rs

@@ -1,5 +1,14 @@
 pub mod eiur;
 
+use blake3::hash;
+
+#[no_mangle]
+extern "C" fn blake3(mem: &mut [u8; 32], len: usize, input: *const u8) {
+ unsafe {
+ *mem = *hash(std::slice::from_raw_parts(input, len)).as_bytes();
+ }
+}
+
 #[cfg(test)]
 mod tests {
  #[test]

.github/workflows/ci.yml

@@ -47,7 +47,5 @@ jobs:
  # TODO: Add '.cargo/config' for list of enabled/disabled `xclippy`lints
  - name: Check clippy warnings
  run: cargo clippy -- -D warnings
- - name: Doctests
- run: cargo test --doc --workspace
  - name: Cargo-deny
  uses: EmbarkStudios/cargo-deny-action@v2

.github/workflows/lspec.yml

@@ -0,0 +1,20 @@
+name: "LSpec CI"
+on:
+ pull_request:
+ push:
+ branches:
+ - main
+jobs:
+ build:
+ name: Build
+ runs-on: ubuntu-latest
+ steps:
+ - name: install elan
+ run: |
+ set -o pipefail
+ curl -sSfL https://github.com/leanprover/elan/releases/download/v4.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+ ./elan-init -y --default-toolchain none
+ echo "$HOME/.elan/bin" >> $GITHUB_PATH
+ - uses: actions/checkout@v4
+ - name: run LSpec binary
+ run: lake exe lspec

Cargo.toml

@@ -3,15 +3,19 @@ name = "ix"
 version = "0.1.0"
 edition = "2021"
 
+[lib]
+crate-type = ["staticlib"]
+
 [dependencies]
 anyhow = "1"
-rustc-hash = "2"
 binius_core = { git = "https://gitlab.com/IrreducibleOSS/binius.git", rev = "0e5ec53f260f40fe6afcc741d4ff8f021a66dc1a" }
 binius_circuits = { git = "https://gitlab.com/IrreducibleOSS/binius.git", rev = "0e5ec53f260f40fe6afcc741d4ff8f021a66dc1a" }
 binius_field = { git = "https://gitlab.com/IrreducibleOSS/binius.git", rev = "0e5ec53f260f40fe6afcc741d4ff8f021a66dc1a" }
 binius_macros = { git = "https://gitlab.com/IrreducibleOSS/binius.git", rev = "0e5ec53f260f40fe6afcc741d4ff8f021a66dc1a" }
 binius_math = { git = "https://gitlab.com/IrreducibleOSS/binius.git", rev = "0e5ec53f260f40fe6afcc741d4ff8f021a66dc1a" }
+blake3 = "1"
 bytemuck = "1"
 bumpalo = "3"
 proptest = "1"
 rayon = "1"
+rustc-hash = "2"

Ix/Address.lean

@@ -1,3 +1,2 @@
-
 structure Address where
  adr : ByteArray

Ix/Blake3.lean

@@ -0,0 +1,2 @@
+@[extern "lean_byte_array_blake3"]
+opaque ByteArray.blake3 : @& ByteArray → ByteArray

Ix/ByteArray.lean

@@ -0,0 +1,12 @@
+namespace ByteArray
+
+def beqNoFFI (a b : ByteArray) : Bool :=
+ a.data == b.data
+
+@[extern "lean_byte_array_beq"]
+def beq : @& ByteArray → @& ByteArray → Bool :=
+ beqNoFFI
+
+instance : BEq ByteArray := ⟨ByteArray.beq⟩
+
+end ByteArray

Ix/Ixon.lean

@@ -1,11 +1,6 @@
-
 import Ix.Address
 import Lean.Declaration
 import Ix.Ixon.Serialize
 import Ix.Ixon.Univ
 import Ix.Ixon.Expr
 import Ix.Ixon.Const
-
-
-
-

Ix/Ixon/Const.lean

@@ -1,4 +1,3 @@
-
 import Ix.Address
 import Lean.Declaration
 import Ix.Ixon.Serialize

Ix/Ixon/Expr.lean

@@ -1,4 +1,3 @@
-
 import Ix.Address
 import Lean.Declaration
 import Ix.Ixon.Serialize
@@ -9,7 +8,7 @@ namespace Ixon
 -- 0xTTTT_LXXX
 inductive Expr where
  -- 0x0, ^1
- | vari (idx: UInt64) : Expr
+ | vari (idx: UInt64) : Expr
  -- 0x1, {max (add 1 2) (var 1)}
  | sort (univ: Univ) : Expr
  -- 0x2 #dead_beef_cafe_babe {u1, u2, ... }
@@ -24,7 +23,7 @@ inductive Expr where
  | alls (types: List Expr) (body: Expr) : Expr
  -- 0x7 (let d : A in b)
  | let_ (type: Expr) (defn: Expr) (body: Expr) : Expr
- -- 0x8 .1
+ -- 0x8 .1
  | proj : UInt64 -> Expr -> Expr
  -- 0x9 "foobar"
  | strl (lit: String) : Expr
@@ -33,7 +32,7 @@ inductive Expr where
 -- array: 0xB
 -- const: 0xC
 
-def putExprTag (tag: UInt8) (val: UInt64) : PutM Unit :=
+def putExprTag (tag: UInt8) (val: UInt64) : PutM Unit :=
  let t := UInt8.shiftLeft tag 4
  if val < 8
  then putUInt8 (UInt8.lor t (Nat.toUInt8 (UInt64.toNat val))) *> pure ()

Ix/Ixon/Serialize.lean

@@ -1,4 +1,3 @@
-
 namespace Ixon
 
 class Serialize (A: Type) where
@@ -13,7 +12,7 @@ structure GetState where
 
 abbrev GetM A := EStateM String GetState A
 
-def runGet (getm: GetM A) (bytes: ByteArray) : Except String A :=
+def runGet (getm: GetM A) (bytes: ByteArray) : Except String A :=
  match EStateM.run getm { index := 0, bytes } with
  | .ok a _ => .ok a
  | .error e _ => .error e

README.md

@@ -1 +1,3 @@
-# ix
+# ix
+
+A verifiable computing platform

Tests/Blake3.lean

@@ -0,0 +1,16 @@
+import LSpec
+import Ix.Blake3
+
+def pairs : List $ (List UInt8 × List UInt8) := [
+ ([0], [ 45, 58, 222, 223, 241, 27, 97, 241,
+ 76, 136, 110, 53, 175, 160, 54, 115,
+ 109, 205, 135, 167, 77, 39, 181, 193,
+ 81, 2, 37, 208, 245, 146, 226, 19,])
+]
+
+open LSpec in
+def main := lspecIO $
+ pairs.foldl (init := .done) fun tSeq (i, o) =>
+ let input := ByteArray.mk ⟨i⟩
+ let output := ByteArray.mk ⟨o⟩
+ tSeq ++ (test s!"blake3 on {input}" $ input.blake3.data = output.data)

Tests/ByteArray.lean

@@ -0,0 +1,22 @@
+import LSpec
+import Ix.ByteArray
+
+def arrays : List ByteArray := [
+ ⟨#[]⟩, ⟨#[1]⟩, ⟨#[0, 3]⟩, ⟨#[1, 1, 1]⟩, ⟨#[3, 3, 3, 3]⟩, ⟨#[13]⟩
+]
+
+def arrays' : List ByteArray := [
+ ⟨#[1]⟩, ⟨#[2]⟩, ⟨#[0, 3, 0]⟩, ⟨#[1, 2, 1]⟩, ⟨#[3, 3, 4, 3]⟩, ⟨#[13, 0]⟩
+]
+
+open LSpec
+
+def beq : TestSeq :=
+ arrays.zip arrays |>.foldl (init := .done) fun tSeq (x, y) =>
+ tSeq ++ (test s!"{x} == {y}" $ x.beq y && x.beqNoFFI y && y.beq x && y.beqNoFFI x)
+
+def neq : TestSeq :=
+ arrays.zip arrays.reverse |>.foldl (init := .done) fun tSeq (x, y) =>
+ tSeq ++ (test s!"{x} != {y}" $ !x.beq y && !x.beqNoFFI y && !y.beq x && !y.beqNoFFI x)
+
+def main := lspecIO $ beq ++ neq

deny.toml

@@ -92,6 +92,7 @@ allow = [
  "MIT",
  "Apache-2.0",
  "Unicode-3.0",
+ "BSD-2-Clause",
  "BSD-3-Clause",
  "CC0-1.0",
  "Zlib",

ffi.c

@@ -0,0 +1,39 @@
+#include <lean/lean.h>
+#include <string.h>
+
+#define intern inline static
+#define l_arg b_lean_obj_arg
+#define l_res lean_obj_res
+
+// Interfaces targeting Rust implementations
+
+void blake3(uint8_t*, size_t, uint8_t*);
+
+// Auxiliary implementations
+
+intern lean_sarray_object* mk_byte_array(size_t len) {
+ lean_sarray_object* o = (lean_sarray_object*)lean_alloc_object(
+ sizeof(lean_sarray_object) + len
+ );
+ lean_set_st_header((lean_object*)o, LeanScalarArray, 1);
+ o->m_size = len;
+ o->m_capacity = len;
+ return o;
+}
+
+// Implementations to serve Lean 4
+
+extern l_res lean_byte_array_blake3(l_arg a) {
+ lean_sarray_object* oa = lean_to_sarray(a);
+ lean_sarray_object* res = mk_byte_array(32);
+ blake3(res->m_data, oa->m_size, oa->m_data);
+ return (lean_object*)res;
+}
+
+extern bool lean_byte_array_beq(l_arg a, l_arg b) {
+ lean_sarray_object* oa = lean_to_sarray(a);
+ lean_sarray_object* ob = lean_to_sarray(b);
+ size_t sa = oa->m_size;
+ if (sa == ob->m_size) return memcmp(oa->m_data, ob->m_data, sa) == 0;
+ return false;
+}

lake-manifest.json

@@ -1,5 +1,15 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
- "packages": [],
+ "packages":
+ [{"url": "https://github.com/argumentcomputer/LSpec",
+ "type": "git",
+ "subDir": null,
+ "scope": "",
+ "rev": "ca8e2803f89f0c12bf9743ae7abbfb2ea6b0eeec",
+ "name": "LSpec",
+ "manifestFile": "lake-manifest.json",
+ "inputRev": "ca8e2803f89f0c12bf9743ae7abbfb2ea6b0eeec",
+ "inherited": false,
+ "configFile": "lakefile.toml"}],
  "name": "ix",
  "lakeDir": ".lake"}

lakefile.lean

@@ -0,0 +1,43 @@
+import Lake
+open System Lake DSL
+
+package ix where
+ version := v!"0.1.0"
+
+lean_lib Ix
+
+@[default_target]
+lean_exe ix where
+ root := `Main
+
+require LSpec from git
+ "https://github.com/argumentcomputer/LSpec" @ "ca8e2803f89f0c12bf9743ae7abbfb2ea6b0eeec"
+
+section Tests
+
+lean_exe Tests.Blake3
+lean_exe Tests.ByteArray
+
+end Tests
+
+section FFI
+
+target ffi.o pkg : FilePath := do
+ let oFile := pkg.buildDir / "ffi.o"
+ let srcJob ← inputTextFile "ffi.c"
+ let includeDir ← getLeanIncludeDir
+ let weakArgs := #["-I", includeDir.toString]
+ buildO oFile srcJob weakArgs #["-fPIC"] "cc" getLeanTrace
+
+extern_lib liblean_ffi pkg := do
+ let name := nameToStaticLib "ffi"
+ let ffiO ← ffi.o.fetch
+ buildStaticLib (pkg.nativeLibDir / name) #[ffiO]
+
+extern_lib rust_ffi pkg := do
+ proc { cmd := "cargo", args := #["build", "--release"], cwd := pkg.dir }
+ let name := nameToStaticLib "ix"
+ let srcPath := pkg.dir / "target" / "release" / name
+ return pure srcPath
+
+end FFI

src/lib.rs

@@ -1,5 +1,14 @@
 pub mod eiur;
 
+use blake3::hash;
+
+#[no_mangle]
+extern "C" fn blake3(mem: &mut [u8; 32], len: usize, input: *const u8) {
+ unsafe {
+ *mem = *hash(std::slice::from_raw_parts(input, len)).as_bytes();
+ }
+}
+
 #[cfg(test)]
 mod tests {
  #[test]

.github/workflows/ci.yml

@@ -47,7 +47,5 @@ jobs:
  # TODO: Add '.cargo/config' for list of enabled/disabled `xclippy`lints
  - name: Check clippy warnings
  run: cargo clippy -- -D warnings
- - name: Doctests
- run: cargo test --doc --workspace
  - name: Cargo-deny
  uses: EmbarkStudios/cargo-deny-action@v2

.github/workflows/lspec.yml

@@ -0,0 +1,20 @@
+name: "LSpec CI"
+on:
+ pull_request:
+ push:
+ branches:
+ - main
+jobs:
+ build:
+ name: Build
+ runs-on: ubuntu-latest
+ steps:
+ - name: install elan
+ run: |
+ set -o pipefail
+ curl -sSfL https://github.com/leanprover/elan/releases/download/v4.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+ ./elan-init -y --default-toolchain none
+ echo "$HOME/.elan/bin" >> $GITHUB_PATH
+ - uses: actions/checkout@v4
+ - name: run LSpec binary
+ run: lake exe lspec

Cargo.toml

@@ -3,15 +3,19 @@ name = "ix"
 version = "0.1.0"
 edition = "2021"
 
+[lib]
+crate-type = ["staticlib"]
+
 [dependencies]
 anyhow = "1"
-rustc-hash = "2"
 binius_core = { git = "https://gitlab.com/IrreducibleOSS/binius.git", rev = "0e5ec53f260f40fe6afcc741d4ff8f021a66dc1a" }
 binius_circuits = { git = "https://gitlab.com/IrreducibleOSS/binius.git", rev = "0e5ec53f260f40fe6afcc741d4ff8f021a66dc1a" }
 binius_field = { git = "https://gitlab.com/IrreducibleOSS/binius.git", rev = "0e5ec53f260f40fe6afcc741d4ff8f021a66dc1a" }
 binius_macros = { git = "https://gitlab.com/IrreducibleOSS/binius.git", rev = "0e5ec53f260f40fe6afcc741d4ff8f021a66dc1a" }
 binius_math = { git = "https://gitlab.com/IrreducibleOSS/binius.git", rev = "0e5ec53f260f40fe6afcc741d4ff8f021a66dc1a" }
+blake3 = "1"
 bytemuck = "1"
 bumpalo = "3"
 proptest = "1"
 rayon = "1"
+rustc-hash = "2"

Ix/Address.lean

@@ -1,3 +1,2 @@
-
 structure Address where
  adr : ByteArray

Ix/Blake3.lean

@@ -0,0 +1,2 @@
+@[extern "lean_byte_array_blake3"]
+opaque ByteArray.blake3 : @& ByteArray → ByteArray

Ix/ByteArray.lean

@@ -0,0 +1,12 @@
+namespace ByteArray
+
+def beqNoFFI (a b : ByteArray) : Bool :=
+ a.data == b.data
+
+@[extern "lean_byte_array_beq"]
+def beq : @& ByteArray → @& ByteArray → Bool :=
+ beqNoFFI
+
+instance : BEq ByteArray := ⟨ByteArray.beq⟩
+
+end ByteArray

Ix/Ixon.lean

@@ -1,11 +1,6 @@
-
 import Ix.Address
 import Lean.Declaration
 import Ix.Ixon.Serialize
 import Ix.Ixon.Univ
 import Ix.Ixon.Expr
 import Ix.Ixon.Const
-
-
-
-

Ix/Ixon/Const.lean

@@ -1,4 +1,3 @@
-
 import Ix.Address
 import Lean.Declaration
 import Ix.Ixon.Serialize

Ix/Ixon/Expr.lean

@@ -1,4 +1,3 @@
-
 import Ix.Address
 import Lean.Declaration
 import Ix.Ixon.Serialize
@@ -9,7 +8,7 @@ namespace Ixon
 -- 0xTTTT_LXXX
 inductive Expr where
  -- 0x0, ^1
- | vari (idx: UInt64) : Expr
+ | vari (idx: UInt64) : Expr
  -- 0x1, {max (add 1 2) (var 1)}
  | sort (univ: Univ) : Expr
  -- 0x2 #dead_beef_cafe_babe {u1, u2, ... }
@@ -24,7 +23,7 @@ inductive Expr where
  | alls (types: List Expr) (body: Expr) : Expr
  -- 0x7 (let d : A in b)
  | let_ (type: Expr) (defn: Expr) (body: Expr) : Expr
- -- 0x8 .1
+ -- 0x8 .1
  | proj : UInt64 -> Expr -> Expr
  -- 0x9 "foobar"
  | strl (lit: String) : Expr
@@ -33,7 +32,7 @@ inductive Expr where
 -- array: 0xB
 -- const: 0xC
 
-def putExprTag (tag: UInt8) (val: UInt64) : PutM Unit :=
+def putExprTag (tag: UInt8) (val: UInt64) : PutM Unit :=
  let t := UInt8.shiftLeft tag 4
  if val < 8
  then putUInt8 (UInt8.lor t (Nat.toUInt8 (UInt64.toNat val))) *> pure ()

Ix/Ixon/Serialize.lean

@@ -1,4 +1,3 @@
-
 namespace Ixon
 
 class Serialize (A: Type) where
@@ -13,7 +12,7 @@ structure GetState where
 
 abbrev GetM A := EStateM String GetState A
 
-def runGet (getm: GetM A) (bytes: ByteArray) : Except String A :=
+def runGet (getm: GetM A) (bytes: ByteArray) : Except String A :=
  match EStateM.run getm { index := 0, bytes } with
  | .ok a _ => .ok a
  | .error e _ => .error e

README.md

@@ -1 +1,3 @@
-# ix
+# ix
+
+A verifiable computing platform

Tests/Blake3.lean

@@ -0,0 +1,16 @@
+import LSpec
+import Ix.Blake3
+
+def pairs : List $ (List UInt8 × List UInt8) := [
+ ([0], [ 45, 58, 222, 223, 241, 27, 97, 241,
+ 76, 136, 110, 53, 175, 160, 54, 115,
+ 109, 205, 135, 167, 77, 39, 181, 193,
+ 81, 2, 37, 208, 245, 146, 226, 19,])
+]
+
+open LSpec in
+def main := lspecIO $
+ pairs.foldl (init := .done) fun tSeq (i, o) =>
+ let input := ByteArray.mk ⟨i⟩
+ let output := ByteArray.mk ⟨o⟩
+ tSeq ++ (test s!"blake3 on {input}" $ input.blake3.data = output.data)

Tests/ByteArray.lean

@@ -0,0 +1,22 @@
+import LSpec
+import Ix.ByteArray
+
+def arrays : List ByteArray := [
+ ⟨#[]⟩, ⟨#[1]⟩, ⟨#[0, 3]⟩, ⟨#[1, 1, 1]⟩, ⟨#[3, 3, 3, 3]⟩, ⟨#[13]⟩
+]
+
+def arrays' : List ByteArray := [
+ ⟨#[1]⟩, ⟨#[2]⟩, ⟨#[0, 3, 0]⟩, ⟨#[1, 2, 1]⟩, ⟨#[3, 3, 4, 3]⟩, ⟨#[13, 0]⟩
+]
+
+open LSpec
+
+def beq : TestSeq :=
+ arrays.zip arrays |>.foldl (init := .done) fun tSeq (x, y) =>
+ tSeq ++ (test s!"{x} == {y}" $ x.beq y && x.beqNoFFI y && y.beq x && y.beqNoFFI x)
+
+def neq : TestSeq :=
+ arrays.zip arrays.reverse |>.foldl (init := .done) fun tSeq (x, y) =>
+ tSeq ++ (test s!"{x} != {y}" $ !x.beq y && !x.beqNoFFI y && !y.beq x && !y.beqNoFFI x)
+
+def main := lspecIO $ beq ++ neq

deny.toml

@@ -92,6 +92,7 @@ allow = [
  "MIT",
  "Apache-2.0",
  "Unicode-3.0",
+ "BSD-2-Clause",
  "BSD-3-Clause",
  "CC0-1.0",
  "Zlib",

ffi.c

@@ -0,0 +1,39 @@
+#include <lean/lean.h>
+#include <string.h>
+
+#define intern inline static
+#define l_arg b_lean_obj_arg
+#define l_res lean_obj_res
+
+// Interfaces targeting Rust implementations
+
+void blake3(uint8_t*, size_t, uint8_t*);
+
+// Auxiliary implementations
+
+intern lean_sarray_object* mk_byte_array(size_t len) {
+ lean_sarray_object* o = (lean_sarray_object*)lean_alloc_object(
+ sizeof(lean_sarray_object) + len
+ );
+ lean_set_st_header((lean_object*)o, LeanScalarArray, 1);
+ o->m_size = len;
+ o->m_capacity = len;
+ return o;
+}
+
+// Implementations to serve Lean 4
+
+extern l_res lean_byte_array_blake3(l_arg a) {
+ lean_sarray_object* oa = lean_to_sarray(a);
+ lean_sarray_object* res = mk_byte_array(32);
+ blake3(res->m_data, oa->m_size, oa->m_data);
+ return (lean_object*)res;
+}
+
+extern bool lean_byte_array_beq(l_arg a, l_arg b) {
+ lean_sarray_object* oa = lean_to_sarray(a);
+ lean_sarray_object* ob = lean_to_sarray(b);
+ size_t sa = oa->m_size;
+ if (sa == ob->m_size) return memcmp(oa->m_data, ob->m_data, sa) == 0;
+ return false;
+}

lake-manifest.json

@@ -1,5 +1,15 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
- "packages": [],
+ "packages":
+ [{"url": "https://github.com/argumentcomputer/LSpec",
+ "type": "git",
+ "subDir": null,
+ "scope": "",
+ "rev": "ca8e2803f89f0c12bf9743ae7abbfb2ea6b0eeec",
+ "name": "LSpec",
+ "manifestFile": "lake-manifest.json",
+ "inputRev": "ca8e2803f89f0c12bf9743ae7abbfb2ea6b0eeec",
+ "inherited": false,
+ "configFile": "lakefile.toml"}],
  "name": "ix",
  "lakeDir": ".lake"}

lakefile.lean

@@ -0,0 +1,43 @@
+import Lake
+open System Lake DSL
+
+package ix where
+ version := v!"0.1.0"
+
+lean_lib Ix
+
+@[default_target]
+lean_exe ix where
+ root := `Main
+
+require LSpec from git
+ "https://github.com/argumentcomputer/LSpec" @ "ca8e2803f89f0c12bf9743ae7abbfb2ea6b0eeec"
+
+section Tests
+
+lean_exe Tests.Blake3
+lean_exe Tests.ByteArray
+
+end Tests
+
+section FFI
+
+target ffi.o pkg : FilePath := do
+ let oFile := pkg.buildDir / "ffi.o"
+ let srcJob ← inputTextFile "ffi.c"
+ let includeDir ← getLeanIncludeDir
+ let weakArgs := #["-I", includeDir.toString]
+ buildO oFile srcJob weakArgs #["-fPIC"] "cc" getLeanTrace
+
+extern_lib liblean_ffi pkg := do
+ let name := nameToStaticLib "ffi"
+ let ffiO ← ffi.o.fetch
+ buildStaticLib (pkg.nativeLibDir / name) #[ffiO]
+
+extern_lib rust_ffi pkg := do
+ proc { cmd := "cargo", args := #["build", "--release"], cwd := pkg.dir }
+ let name := nameToStaticLib "ix"
+ let srcPath := pkg.dir / "target" / "release" / name
+ return pure srcPath
+
+end FFI

src/lib.rs

@@ -1,5 +1,14 @@
 pub mod eiur;
 
+use blake3::hash;
+
+#[no_mangle]
+extern "C" fn blake3(mem: &mut [u8; 32], len: usize, input: *const u8) {
+ unsafe {
+ *mem = *hash(std::slice::from_raw_parts(input, len)).as_bytes();
+ }
+}
+
 #[cfg(test)]
 mod tests {
  #[test]