Jcb/ix tests

Apps/ZKVoting/Prover.lean

@@ -29,35 +29,33 @@ def runElection (votes: List Candidate) : Result :=
 open Ix.Compile
 
 def main : IO UInt32 := do
-  let mut stt : CompileState := .init (<- get_env!)
+  let mut env : Lean.Environment := <- get_env!
   -- simulate getting the votes from somewhere
   let votes : List Candidate <- pure privateVotes
   let mut as : List Lean.Name := []
-  -- default maxHeartBeats
-  let ticks : USize := 200000
   -- the type of each vote to commit
   let voteType := Lean.toTypeExpr Candidate
   -- loop over the votes
   for v in votes do
     -- add each vote to our environment as a commitment
-    let (lvls, typ, val) <- runMeta (metaMakeDef v) stt.env
-    let ((addr, _), stt') <- (commitDef lvls typ val).runIO' ticks stt
-    stt := stt'
+    let (lvls, typ, val) <- runMeta (metaMakeDef v) env
+    let ((addr, _), stt) <- (commitDef lvls typ val).runIO env
+    env := stt.env
     as := (Address.toUniqueName addr)::as
     IO.println s!"vote: {repr v}, commitment: {addr}"
   -- build a Lean list of our commitments as the argument to runElection
-  let arg : Lean.Expr <- runMeta (metaMakeList voteType as) stt.env
+  let arg : Lean.Expr <- runMeta (metaMakeList voteType as) env
   let (lvls, input, output, type, sort) <-
-    runMeta (metaMakeEvalClaim ``runElection [arg]) stt.env
-  let inputPretty <- runMeta (Lean.Meta.ppExpr input) stt.env
-  let outputPretty <- runMeta (Lean.Meta.ppExpr output) stt.env
-  let typePretty <- runMeta (Lean.Meta.ppExpr type) stt.env
+    runMeta (metaMakeEvalClaim ``runElection [arg]) env
+  let inputPretty <- runMeta (Lean.Meta.ppExpr input) env
+  let outputPretty <- runMeta (Lean.Meta.ppExpr output) env
+  let typePretty <- runMeta (Lean.Meta.ppExpr type) env
   IO.println s!"claim: {inputPretty}"
   IO.println s!"  ~> {outputPretty}"
   IO.println s!"  : {typePretty}"
   IO.println s!"  @ {repr lvls}"
-  let ((claim,_,_,_), _stt') <-
-     (evalClaim lvls input output type sort true).runIO' ticks stt
+  let ((claim,_,_,_), _stt') <- 
+    (evalClaim lvls input output type sort true).runIO env
   IO.println s!"{claim}"
   -- Ix.prove claim stt
   return 0

Ix.lean

@@ -5,5 +5,6 @@ import Ix.TransportM
 import Ix.IR
 import Ix.Meta
 import Ix.CompileM
+import Ix.DecompileM
 import Ix.Claim
 import Ix.Prove

Ix/Cli/ProveCmd.lean

@@ -7,6 +7,8 @@ import Ix.Address
 import Ix.Meta
 import Lean
 
+open Ix.Compile
+
 --❯ ix prove IxTest.lean "id'"
 --typechecking:
 --id' (A : Type) (x : A) : A
@@ -22,8 +24,7 @@ def runProveCheck
   IO.println "typechecking:"
   IO.println signature.fmt.pretty
   let ((claim, _, _), _stt) <- 
-    (Ix.Compile.checkClaim constInfo.name constInfo.type constSort
-    constInfo.levelParams commit).runIO' 200000 (.init env)
+    (checkClaim constInfo.name constInfo.type constSort constInfo.levelParams commit).runIO env
   IO.println $ s!"claim: {claim}"
   -- TODO: prove
   return 0
@@ -62,8 +63,7 @@ def runProveEval
   IO.println s!"  ~> {outputPretty}"
   IO.println s!"  : {typePretty}"
   IO.println s!"  @ {repr lvls}"
-  let ((claim, _, _), _stt) <- 
-    (Ix.Compile.evalClaim lvls input output type sort commit).runIO' 200000 (.init env)
+  let ((claim, _, _), _stt) <- (evalClaim lvls input output type sort commit).runIO env
   IO.println $ s!"claim: {claim}"
   -- TODO: prove
   return 0

Ix/Cli/StoreCmd.lean

@@ -2,24 +2,25 @@ import Cli
 import Ix.Cronos
 import Ix.Common
 import Ix.CompileM
+import Ix.TransportM
 import Ix.Store
 import Ix.Address
 import Lean
 
 -- ix store <lean file>
 -- ix store get <address>
+-- ix store remat <address> <address>
 def runStore (p : Cli.Parsed) : IO UInt32 := do
   let source : String       := p.positionalArg! "source" |>.as! String
   let mut cronos ← Cronos.new.clock "Lean-frontend"
   Lean.setLibsPaths source
   --StoreIO.toIO ensureStoreDir
   let path := ⟨source⟩
   let leanEnv ← Lean.runFrontend (← IO.FS.readFile path) path
-  let delta := leanEnv.getDelta
   cronos ← cronos.clock "Lean-frontend"
   -- Start content-addressing
   cronos ← cronos.clock "content-address"
-  let stt ← Ix.Compile.compileDeltaIO leanEnv delta
+  let stt ← Ix.Compile.compileEnvIO leanEnv
   stt.names.forM fun name (const, meta) => do
      IO.println <| s!"{name}:"
      IO.println <| s!"  #{const}"
@@ -49,13 +50,35 @@ def runGet (p : Cli.Parsed) : IO UInt32 := do
   IO.println <| s!"{repr const}"
   return 0
 
+def runRemat (p : Cli.Parsed) : IO UInt32 := do
+  let cont : String       := p.positionalArg! "constantAddress" |>.as! String
+  let meta : String       := p.positionalArg! "metadataAddress" |>.as! String
+  let (c, m) <- IO.ofExcept $
+    match Address.fromString cont, Address.fromString meta with
+    | .some c, .some m => .ok (c, m)
+    | .none, _ => .error "bad address {cont}"
+    | _, .none => .error "bad address {meta}"
+  let cont <- StoreIO.toIO (Store.readConst c)
+  let meta <- StoreIO.toIO (Store.readConst m)
+  let ix := Ix.TransportM.rematerialize cont meta
+  IO.println <| s!"{repr ix}"
+  return 0
+
 def storeGetCmd : Cli.Cmd := `[Cli|
   get VIA runGet;
   "print a store entry"
   ARGS:
     address  : String; "Ix address"
 ]
 
+def storeRematCmd : Cli.Cmd := `[Cli|
+  remat VIA runRemat;
+  "print a store entry"
+  ARGS:
+    constantAddress  : String; "Ix constant address"
+    metadataAddress  : String; "Ix metadata address"
+]
+
 def storeCmd : Cli.Cmd := `[Cli|
   store VIA runStore;
   "Interact with the Ix store"
@@ -67,6 +90,7 @@ def storeCmd : Cli.Cmd := `[Cli|
     source : String; "Source file input"
 
   SUBCOMMANDS:
-    storeGetCmd
+    storeGetCmd;
+    storeRematCmd
 ]
 

Ix/Common.lean

@@ -10,6 +10,16 @@ def compareList [Ord α] : List α -> List α -> Ordering
 | [], _::_ => .lt
 | [], [] => .eq
 
+def compareListM 
+  [Monad μ] (cmp: α -> α -> μ Ordering) : List α -> List α -> μ Ordering
+| a::as, b::bs => do
+  match (<- cmp a b) with
+  | .eq => compareListM cmp as bs
+  | x => pure x
+| _::_, [] => pure .gt
+| [], _::_ => pure .lt
+| [], [] => pure .eq
+
 instance [Ord α] : Ord (List α) where 
   compare := compareList
 
@@ -22,14 +32,36 @@ instance : Ord Lean.Name where
   compare := Lean.Name.quickCmp
 
 deriving instance Ord for Lean.Literal
+--deriving instance Ord for Lean.Expr
 deriving instance Ord for Lean.BinderInfo
-deriving instance Ord for Lean.QuotKind
+deriving instance BEq, Repr, Hashable, Ord for Lean.QuotKind
+deriving instance Hashable, Repr for Lean.ReducibilityHints
+deriving instance BEq, Ord, Hashable, Repr for Lean.DefinitionSafety
+deriving instance BEq, Repr for Lean.ConstantVal
+deriving instance BEq, Repr for Lean.QuotVal
+deriving instance BEq, Repr for Lean.AxiomVal
+deriving instance BEq, Repr for Lean.TheoremVal
+deriving instance BEq, Repr for Lean.DefinitionVal
+deriving instance BEq, Repr for Lean.OpaqueVal
+deriving instance BEq, Repr for Lean.RecursorRule
+deriving instance BEq, Repr for Lean.RecursorVal
+deriving instance BEq, Repr for Lean.ConstructorVal
+deriving instance BEq, Repr for Lean.InductiveVal
+deriving instance BEq, Repr for Lean.ConstantInfo
+deriving instance BEq, Repr for Ordering
 
 def UInt8.MAX : UInt64 := 0xFF
 def UInt16.MAX : UInt64 := 0xFFFF
 def UInt32.MAX : UInt64 := 0xFFFFFFFF
 def UInt64.MAX : UInt64 := 0xFFFFFFFFFFFFFFFF
 
+/-- Distinguish different kinds of Ix definitions --/
+inductive Ix.DefMode where
+| «definition»
+| «opaque»
+| «theorem»
+deriving BEq, Ord, Hashable, Repr, Nonempty, Inhabited
+
 namespace List
 
 partial def mergeM [Monad μ] (cmp : α → α → μ Ordering) : List α → List α → μ (List α)
@@ -72,26 +104,16 @@ mutual
 
 end
 
-def sortByM [Monad μ] (xs: List α) (cmp: α -> α -> μ Ordering) (rev := false) :
-    μ (List α) := do
-  if rev then
-    let revCmp : _ → _ → μ Ordering := fun x y => do
-      match (← cmp x y) with
-      | .gt => return Ordering.lt
-      | .eq => return Ordering.eq
-      | .lt => return Ordering.gt
-    sequencesM revCmp xs >>= mergeAllM revCmp
-  else
-    sequencesM cmp xs >>= mergeAllM cmp
+def sortByM [Monad μ] (xs: List α) (cmp: α -> α -> μ Ordering) : μ (List α) :=
+  sequencesM cmp xs >>= mergeAllM cmp
 
 /--
-Mergesort from least to greatest. To sort from greatest to
+Mergesort from least to greatest. To sort from greatest to least set `rev`
 -/
-def sortBy (cmp : α -> α -> Ordering) (xs: List α) (rev := false) : List α :=
-  Id.run do xs.sortByM (cmp <$> · <*> ·) rev
+def sortBy (cmp : α -> α -> Ordering) (xs: List α) : List α :=
+  Id.run <| xs.sortByM (fun x y => pure <| cmp x y)
 
-def sort [Ord α] (xs: List α) (rev := false) : List α :=
-  sortBy compare xs rev
+def sort [Ord α] (xs: List α) : List α := sortBy compare xs
 
 def groupByMAux [Monad μ] (eq : α → α → μ Bool) : List α → List (List α) → μ (List (List α))
   | a::as, (ag::g)::gs => do match (← eq a ag) with
@@ -216,4 +238,26 @@ def runFrontend (input : String) (filePath : FilePath) : IO Environment := do
       (← msgs.toList.mapM (·.toString)).map String.trim
   else return s.commandState.env
 
+def Expr.stripMData : Expr -> Expr
+| .mdata _ x => x.stripMData
+| .app f a => .app f.stripMData a.stripMData
+| .lam bn bt b bi => .lam bn bt.stripMData b.stripMData bi
+| .forallE bn bt b bi => .forallE bn bt.stripMData b.stripMData bi
+| .letE ln t v b nd => .letE ln t.stripMData v.stripMData b.stripMData nd
+| .proj tn i s => .proj tn i s.stripMData
+| x => x
+
+def RecursorRule.stripMData : RecursorRule -> RecursorRule
+| ⟨c, nf, rhs⟩ => ⟨c, nf, rhs.stripMData⟩
+
+def ConstantInfo.stripMData : Lean.ConstantInfo -> Lean.ConstantInfo
+| .axiomInfo x => .axiomInfo { x with type := x.type.stripMData }
+| .defnInfo x => .defnInfo { x with type := x.type.stripMData, value := x.value.stripMData }
+| .thmInfo x => .thmInfo { x with type := x.type.stripMData, value := x.value.stripMData }
+| .quotInfo x => .quotInfo { x with type := x.type.stripMData }
+| .opaqueInfo x => .opaqueInfo { x with type := x.type.stripMData, value := x.value.stripMData }
+| .inductInfo x => .inductInfo { x with type := x.type.stripMData }
+| .ctorInfo x => .ctorInfo { x with type := x.type.stripMData }
+| .recInfo x => .recInfo { x with type := x.type.stripMData, rules := x.rules.map (·.stripMData) }
 end Lean
+