diff --git a/Apps/ZKVoting/Common.lean b/Apps/ZKVoting/Common.lean deleted file mode 100644 index 2a3d0120..00000000 --- a/Apps/ZKVoting/Common.lean +++ /dev/null @@ -1,10 +0,0 @@ -import Ix.BuiltIn - -inductive Candidate - | abe | bam | cot - deriving Inhabited, Lean.ToExpr - -abbrev Vote := Commitment Candidate - -abbrev proofPath : System.FilePath := - "Apps" / "ZKVoting" / "proof" diff --git a/Apps/ZKVoting/Prover.lean b/Apps/ZKVoting/Prover.lean index 9f5a4415..c09760dc 100644 --- a/Apps/ZKVoting/Prover.lean +++ b/Apps/ZKVoting/Prover.lean @@ -1,52 +1,64 @@ -import Ix -import Apps.ZKVoting.ProverInit -import Apps.ZKVoting.Common +import Ix.Claim +import Ix.Address +import Ix.Meta +import Ix.CompileM +import Batteries -open Lean +inductive Candidate + | alice | bob | charlie + deriving Inhabited, Lean.ToExpr, Repr, BEq, Ord -partial def collectVotes (env : Environment) : IO $ List Vote := - collectVotesLoop [] initSecret (0 : UInt64) -where - collectVotesLoop votes secret count := do - let input := (← (← IO.getStdin).getLine).trim - let consts := env.constants - let voteAbe ← mkCommit secret Candidate.abe consts - let voteBam ← mkCommit secret Candidate.bam consts - let voteCot ← mkCommit secret Candidate.cot consts - IO.println s!"a: Abe | {voteAbe}" - IO.println s!"b: Bam | {voteBam}" - IO.println s!"b: Cot | {voteCot}" - IO.println "_: End voting" - let vote ← match input with - | "a" => pure voteAbe | "b" => pure voteBam | "c" => pure voteCot - | _ => return votes - let secret' := (← mkCommit secret count consts).adr - IO.println vote - collectVotesLoop (vote :: votes) secret' (count + 1) +structure Result where + aliceVotes: Nat + bobVotes: Nat + charlieVotes: Nat +deriving Repr, Lean.ToExpr -structure VoteCounts where - abe : UInt64 - bam : UInt64 - cot : UInt64 - deriving ToExpr +def privateVotes : List Candidate := + [.alice, .alice, .bob] -def countVotes : List Vote → VoteCounts - | [] => ⟨0, 0, 0⟩ - | vote :: votes => - let counts := countVotes votes - match (reveal vote : Candidate) with - | .abe => { counts with abe := counts.abe + 1 } - | .bam => { counts with bam := counts.bam + 1 } - | .cot => { counts with cot := counts.cot + 1 } +def runElection (votes: List Candidate) : Result := + votes.foldr tally ⟨0,0,0⟩ + where + tally (comm: Candidate) (res: Result): Result := + match comm, res with + | .alice, ⟨a, b, c⟩ => ⟨a+1, b, c⟩ + | .bob, ⟨a, b, c⟩ => ⟨a, b+1, c⟩ + | .charlie, ⟨a, b, c⟩ => ⟨a, b, c+1⟩ + +open Ix.Compile def main : IO UInt32 := do - let env ← get_env! - let votes ← collectVotes env - let .defnInfo countVotesDefn ← runCore (getConstInfo ``countVotes) env - | unreachable! - let claimValue := .app countVotesDefn.value (toExpr votes) - let claimType ← runMeta (Meta.inferType claimValue) env - let claimAdr := computeIxAddress (mkAnonDefInfoRaw claimType claimValue) env.constants - match ← prove claimAdr with - | .ok proof => IO.FS.writeBinFile proofPath $ Ixon.Serialize.put proof; return 0 - | .error err => IO.eprintln $ toString err; return 1 + let mut stt : CompileState := .init (<- 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' + 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 (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 + 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 + IO.println s!"{claim}" + -- Ix.prove claim stt + return 0 + diff --git a/Apps/ZKVoting/ProverInit.lean b/Apps/ZKVoting/ProverInit.lean deleted file mode 100644 index 5e5ce063..00000000 --- a/Apps/ZKVoting/ProverInit.lean +++ /dev/null @@ -1,9 +0,0 @@ -import Ix.Address - -initialize initSecret : Address ← do - IO.setRandSeed (← IO.monoNanosNow) - let mut secret : ByteArray := default - for _ in [:32] do - let rand ← IO.rand 0 (UInt8.size - 1) - secret := secret.push rand.toUInt8 - return ⟨secret⟩ diff --git a/Apps/ZKVoting/Verifier.lean b/Apps/ZKVoting/Verifier.lean index 16a6e52b..eee11247 100644 --- a/Apps/ZKVoting/Verifier.lean +++ b/Apps/ZKVoting/Verifier.lean @@ -1,18 +1,18 @@ import Ix.Ixon.Serialize import Ix.Prove -import Apps.ZKVoting.Common def main (args : List String) : IO UInt32 := do - let mut votes := #[] - for commStr in args do - match Commitment.ofString commStr with - | none => IO.eprintln s!"Couldn't parse {commStr} as a commitment"; return 1 - | some (comm : Vote) => votes := votes.push comm - let proofBytes ← IO.FS.readBinFile proofPath - match Ixon.Serialize.get proofBytes with - | .error err => IO.eprintln s!"Proof deserialization error: {err}"; return 1 - | .ok (_proof : Proof) => - -- TODO: print the resulting vote counts in the claim - -- TODO: assert that every vote in `votes` is in the proof claim - -- TODO: verify proof +-- TODO +-- let mut votes := #[] +-- for commStr in args do +-- match Commitment.ofString commStr with +-- | none => IO.eprintln s!"Couldn't parse {commStr} as a commitment"; return 1 +-- | some (comm : Vote) => votes := votes.push comm +-- let proofBytes ← IO.FS.readBinFile proofPath +-- match Ixon.Serialize.get proofBytes with +-- | .error err => IO.eprintln s!"Proof deserialization error: {err}"; return 1 +-- | .ok (_proof : Proof) => +-- -- TODO: print the resulting vote counts in the claim +-- -- TODO: assert that every vote in `votes` is in the proof claim +-- -- TODO: verify proof return 0 diff --git a/Ix.lean b/Ix.lean index 5ed23ad6..3da4f8da 100644 --- a/Ix.lean +++ b/Ix.lean @@ -1,9 +1,9 @@ -- This module serves as the root of the `Ix` library. -- Import modules here that should be built as part of the library. -import Ix.BuiltIn import Ix.Ixon -import Ix.CanonM import Ix.TransportM import Ix.IR import Ix.Meta +import Ix.CompileM +import Ix.Claim import Ix.Prove diff --git a/Ix/Address.lean b/Ix/Address.lean index f012a70e..85016381 100644 --- a/Ix/Address.lean +++ b/Ix/Address.lean @@ -9,33 +9,98 @@ structure Address where hash : ByteArray deriving Inhabited, Lean.ToExpr, BEq, Hashable -def Address.ofChars (_adrChars : List Char) : Option Address := - some default -- TODO - -def Address.ofString (adrStr: String) : Option Address := - Address.ofChars adrStr.data - def Address.blake3 (x: ByteArray) : Address := ⟨(Blake3.hash x).val⟩ -open Lean +def hexOfNat : Nat -> Option Char +| 0 => .some '0' +| 1 => .some '1' +| 2 => .some '2' +| 3 => .some '3' +| 4 => .some '4' +| 5 => .some '5' +| 6 => .some '6' +| 7 => .some '7' +| 8 => .some '8' +| 9 => .some '9' +| 10 => .some 'a' +| 11 => .some 'b' +| 12 => .some 'c' +| 13 => .some 'd' +| 14 => .some 'e' +| 15 => .some 'f' +| _ => .none + +def natOfHex : Char -> Option Nat +| '0' => .some 0 +| '1' => .some 1 +| '2' => .some 2 +| '3' => .some 3 +| '4' => .some 4 +| '5' => .some 5 +| '6' => .some 6 +| '7' => .some 7 +| '8' => .some 8 +| '9' => .some 9 +| 'a' => .some 10 +| 'b' => .some 11 +| 'c' => .some 12 +| 'd' => .some 13 +| 'e' => .some 14 +| 'f' => .some 15 +| 'A' => .some 10 +| 'B' => .some 11 +| 'C' => .some 12 +| 'D' => .some 13 +| 'E' => .some 14 +| 'F' => .some 15 +| _ => .none -/-- Convert a byte (UInt8) to a two‐digit hex string. -/ -def byteToHex (b : UInt8) : String := - let hexDigits := - #['0', '1', '2', '3', '4', '5', '6', '7', '8', '9', 'a', 'b', 'c', 'd', 'e', 'f'] - let hi := hexDigits[(UInt8.toNat (b >>> 4))]! - let lo := hexDigits[(UInt8.toNat (b &&& 0xF))]! - String.mk [hi, lo] +/-- Convert a byte (UInt8) to a two‐digit big-endian hexadecimal string. -/ +def hexOfByte (b : UInt8) : String := + let hi := hexOfNat (UInt8.toNat (b >>> 4)) + let lo := hexOfNat (UInt8.toNat (b &&& 0xF)) + String.mk [hi.get!, lo.get!] -/-- Convert a ByteArray to a hexadecimal string. -/ -def byteArrayToHex (ba : ByteArray) : String := - (ba.toList.map byteToHex).foldl (· ++ ·) "" +/-- Convert a ByteArray to a big-endian hexadecimal string. -/ +def hexOfBytes (ba : ByteArray) : String := + (ba.toList.map hexOfByte).foldl (· ++ ·) "" instance : ToString Address where - toString adr := byteArrayToHex adr.hash + toString adr := hexOfBytes adr.hash instance : Repr Address where reprPrec a _ := "#" ++ (toString a).toFormat instance : Ord Address where compare a b := compare a.hash.data.toList b.hash.data.toList + +def byteOfHex : Char -> Char -> Option UInt8 +| hi, lo => do + let hi <- natOfHex hi + let lo <- natOfHex lo + UInt8.ofNat (hi <<< 4 + lo) + +def bytesOfHex (s: String) : Option ByteArray := do + let bs <- go s.toList + return ⟨bs.toArray⟩ + where + go : List Char -> Option (List UInt8) + | hi::lo::rest => do + let b <- byteOfHex hi lo + let bs <- go rest + b :: bs + | [] => return [] + | _ => .none + +def Address.fromString (s: String) : Option Address := do + let ba <- bytesOfHex s + if ba.size == 32 then .some ⟨ba⟩ else .none + +def Address.toUniqueName (addr: Address): Lean.Name := + .str (.str (.str .anonymous "Ix") "_#") (hexOfBytes addr.hash) + +def Address.fromUniqueName (name: Lean.Name) : Option Address := + match name with + | .str (.str (.str .anonymous "Ix") "_#") s => Address.fromString s + | _ => .none + diff --git a/Ix/BuiltIn.lean b/Ix/BuiltIn.lean deleted file mode 100644 index 42a28ddb..00000000 --- a/Ix/BuiltIn.lean +++ /dev/null @@ -1,34 +0,0 @@ -import Blake3 -import Ix.Address -import Ix.Meta - -structure Commitment (α : Type _) where - adr : Address - deriving Inhabited, Lean.ToExpr - -instance : ToString (Commitment α) where - toString comm := "c" ++ toString comm.adr - -def Commitment.ofString (s : String) : Option $ Commitment α := - match s.data with - | 'c' :: adrChars => .mk <$> Address.ofChars adrChars - | _ => none - --- TODO: secrets should be 32-bytes long -opaque commit (secret : Address) (payload : α) : Commitment α -opaque secret (comm : Commitment α) : Address -opaque reveal [Inhabited α] (comm : Commitment α) : α -opaque revealThen [Inhabited β] (comm : Commitment α) (f : β) : β - -def persistCommit (secret : Address) (payload : Address) : IO $ Commitment α := - let commAdr := Blake3.hash $ secret.hash ++ payload.hash - -- TODO: persist commitment preimages as private data - return ⟨⟨commAdr.val⟩⟩ - -def mkCommitRaw (secret : Address) (type : Lean.Expr) (value : Lean.Expr) - (consts : Lean.ConstMap) : IO $ Commitment α := - persistCommit secret $ computeIxAddress (mkAnonDefInfoRaw type value) consts - -def mkCommit [Lean.ToExpr α] (secret : Address) (a : α) (consts : Lean.ConstMap) : - IO $ Commitment α := - persistCommit secret $ computeIxAddress (mkAnonDefInfo a) consts diff --git a/Ix/CanonM.lean b/Ix/CanonM.lean deleted file mode 100644 index a31efd4b..00000000 --- a/Ix/CanonM.lean +++ /dev/null @@ -1,547 +0,0 @@ -import Batteries.Data.RBMap -import Ix.TransportM -import Ix.Ixon.Metadata -import Ix.Ixon.Const -import Ix.Ixon.Serialize -import Ix.Common - -open Batteries (RBMap) -open Batteries (RBSet) -open Ix.TransportM - -namespace Ix.CanonM - -inductive CanonMError - | unknownConstant : Lean.Name → CanonMError - | unfilledLevelMetavariable : Lean.Level → CanonMError - | unfilledExprMetavariable : Lean.Expr → CanonMError - | invalidBVarIndex : Nat → CanonMError - | freeVariableExpr : Lean.Expr → CanonMError - | metaVariableExpr : Lean.Expr → CanonMError - | metaDataExpr : Lean.Expr → CanonMError - | levelNotFound : Lean.Name → List Lean.Name → CanonMError - | invalidConstantKind : Lean.Name → String → String → CanonMError - | constantNotContentAddressed : Lean.Name → CanonMError - | nonRecursorExtractedFromChildren : Lean.Name → CanonMError - | cantFindMutDefIndex : Lean.Name → CanonMError - | transportError : TransportError → CanonMError - deriving Inhabited - -instance : ToString CanonMError where toString - | .unknownConstant n => s!"Unknown constant '{n}'" - | .unfilledLevelMetavariable l => s!"Unfilled level metavariable on universe '{l}'" - | .unfilledExprMetavariable e => s!"Unfilled level metavariable on expression '{e}'" - | .invalidBVarIndex idx => s!"Invalid index {idx} for bound variable context" - | .freeVariableExpr e => s!"Free variable in expression '{e}'" - | .metaVariableExpr e => s!"Meta variable in expression '{e}'" - | .metaDataExpr e => s!"Meta data in expression '{e}'" - | .levelNotFound n ns => s!"'{n}' not found in '{ns}'" - | .invalidConstantKind n ex gt => - s!"Invalid constant kind for '{n}'. Expected '{ex}' but got '{gt}'" - | .constantNotContentAddressed n => s!"Constant '{n}' wasn't content-addressed" - | .nonRecursorExtractedFromChildren n => - s!"Non-recursor '{n}' extracted from children" - | .cantFindMutDefIndex n => s!"Can't find index for mutual definition '{n}'" - | .transportError n => s!"Transport error '{repr n}'" - -structure CanonMState where - names : RBMap Lean.Name (Address × Address) compare - store : RBMap Address Ixon.Const compare - consts : RBMap Address (RBMap Address Ix.Const compare) compare - commits: RBMap Ix.Const (Address × Address) compare - blocks : RBSet (Address × Address) compare - -structure CanonMCtx where - constMap: Lean.ConstMap - univCtx : List Lean.Name - bindCtx : List Lean.Name - recrCtx : RBMap Lean.Name Nat compare - --quick : Bool - --persist : Bool - -abbrev CanonM := ReaderT CanonMCtx $ ExceptT CanonMError $ StateT CanonMState IO - -def withBinder (name : Lean.Name) : CanonM α → CanonM α := - withReader $ fun c => { c with bindCtx := name :: c.bindCtx } - -def withLevelsAndReset (levels : List Lean.Name) : CanonM α → CanonM α := - withReader $ fun c => - { c with univCtx := levels, bindCtx := [], recrCtx := .empty } - -def withRecrs (recrCtx : RBMap Lean.Name Nat compare) : - CanonM α → CanonM α := - withReader $ fun c => { c with recrCtx := recrCtx } - -def withLevels (lvls : List Lean.Name) : CanonM α → CanonM α := - withReader $ fun c => { c with univCtx := lvls } - -def commit (const : Ix.Const) : CanonM (Address × Address) := do - match (← get).commits.find? const with - | some (contAddr, metaAddr) => pure (contAddr, metaAddr) - | none => do - let (ixon, meta) <- match constToIxon const with - | .ok (i, m) => pure (i, m) - | .error e => throw (.transportError e) - let contAddr := Address.blake3 (Ixon.Serialize.put ixon) - let metaAddr := Address.blake3 (Ixon.Serialize.put meta) - modifyGet fun stt => ((contAddr, metaAddr), { stt with - commits := stt.commits.insert const (contAddr, metaAddr) - store := (stt.store.insert contAddr ixon).insert metaAddr meta - consts := stt.consts.modify contAddr (fun m => m.insert metaAddr const) - }) - -@[inline] def addConstToStt (name : Lean.Name) (constAddr metaAddr: Address) : CanonM Unit := - modify fun stt => - { stt with names := stt.names.insert name (constAddr, metaAddr) } - -@[inline] def addBlockToStt (blockAddr blockMeta : Address) : CanonM Unit := - modify fun stt => { stt with blocks := stt.blocks.insert (blockAddr, blockMeta) } - -scoped instance : HMul Ordering Ordering Ordering where hMul - | .gt, _ => .gt - | .lt, _ => .lt - | .eq, x => x - -def concatOrds : List Ordering → Ordering := - List.foldl (· * ·) .eq - -/-- Defines an ordering for Lean universes -/ -def cmpLevel (x : Lean.Level) (y : Lean.Level) : CanonM Ordering := - match x, y with - | .mvar .., _ => throw $ .unfilledLevelMetavariable x - | _, .mvar .. => throw $ .unfilledLevelMetavariable y - | .zero, .zero => return .eq - | .zero, _ => return .lt - | _, .zero => return .gt - | .succ x, .succ y => cmpLevel x y - | .succ .., _ => return .lt - | _, .succ .. => return .gt - | .max lx ly, .max rx ry => (· * ·) <$> cmpLevel lx rx <*> cmpLevel ly ry - | .max .., _ => return .lt - | _, .max .. => return .gt - | .imax lx ly, .imax rx ry => (· * ·) <$> cmpLevel lx rx <*> cmpLevel ly ry - | .imax .., _ => return .lt - | _, .imax .. => return .gt - | .param x, .param y => do - let lvls := (← read).univCtx - match (lvls.idxOf? x), (lvls.idxOf? y) with - | some xi, some yi => return (compare xi yi) - | none, _ => throw $ .levelNotFound x lvls - | _, none => throw $ .levelNotFound y lvls - -/-- Canonicalizes a Lean universe level and adds it to the store -/ -def canonUniv : Lean.Level → CanonM Ix.Univ - | .zero => pure .zero - | .succ u => return .succ (← canonUniv u) - | .max a b => return .max (← canonUniv a) (← canonUniv b) - | .imax a b => return .imax (← canonUniv a) (← canonUniv b) - | .param name => do - let lvls := (← read).univCtx - match lvls.idxOf? name with - | some n => pure $ .var name n - | none => throw $ .levelNotFound name lvls - | l@(.mvar ..) => throw $ .unfilledLevelMetavariable l - - -/-- Retrieves a Lean constant from the environment by its name -/ -def getLeanConstant (name : Lean.Name) : CanonM Lean.ConstantInfo := do - match (← read).constMap.find? name with - | some const => pure const - | none => throw $ .unknownConstant name - -def isInternalRec (expr : Lean.Expr) (name : Lean.Name) : Bool := - match expr with - | .forallE _ t e _ => match e with - | .forallE .. => isInternalRec e name - | _ => isInternalRec t name -- t is the major premise - | .app e .. => isInternalRec e name - | .const n .. => n == name - | _ => false - -mutual - -partial def canonConst (const : Lean.ConstantInfo) : CanonM (Address × Address) := do - match (← get).names.find? const.name with - | some (constAddr, metaAddr) => pure (constAddr, metaAddr) - | none => match const with - | .defnInfo val => withLevelsAndReset val.levelParams $ canonDefinition val - | .inductInfo val => withLevelsAndReset val.levelParams $ canonInductive val - | .ctorInfo val => do - match ← getLeanConstant val.induct with - | .inductInfo ind => discard $ canonConst (.inductInfo ind) - | const => throw $ .invalidConstantKind const.name "inductive" const.ctorName - canonConst const - | .recInfo val => do - match ← getLeanConstant val.getMajorInduct with - | .inductInfo ind => discard $ canonConst (.inductInfo ind) - | const => throw $ .invalidConstantKind const.name "inductive" const.ctorName - canonConst const - -- The rest adds the constants to the cache one by one - | const => withLevelsAndReset const.levelParams do - let obj ← match const with - | .defnInfo _ | .inductInfo _ | .ctorInfo _ | .recInfo _ => unreachable! - | .axiomInfo val => - pure $ .axiom ⟨val.levelParams.length, ← canonExpr val.type⟩ - | .thmInfo val => - -- Theorems are never truly recursive - pure $ .theorem ⟨val.levelParams.length, ← canonExpr val.type, - ← canonExpr val.value⟩ - | .opaqueInfo val => - let recrs := .single val.name 0 - pure $ .opaque ⟨val.levelParams.length, ← canonExpr val.type, - ← withRecrs recrs $ canonExpr val.value⟩ - | .quotInfo val => - pure $ .quotient ⟨val.levelParams.length, ← canonExpr val.type, val.kind⟩ - let (constAddr, metaAddr) ← commit obj - addConstToStt const.name constAddr metaAddr - return (constAddr, metaAddr) - -partial def canonDefinition (struct : Lean.DefinitionVal) : CanonM (Address × Address):= do - -- If the mutual size is one, simply content address the single definition - if struct.all matches [_] then - let (constAddr, metaAddr) ← commit $ .definition - (← withRecrs (.single struct.name 0) $ definitionToIR struct) - addConstToStt struct.name constAddr metaAddr - return (constAddr, metaAddr) - - -- Collecting and sorting all definitions in the mutual block - let mutualDefs ← struct.all.mapM fun name => do - match ← getLeanConstant name with - | .defnInfo defn => pure defn - | const => throw $ .invalidConstantKind const.name "definition" const.ctorName - let mutualDefs ← sortDefs [mutualDefs] - - -- Building the `recrCtx` - let mut recrCtx := default - for (ds, i) in List.zipIdx mutualDefs do - for d in ds do - recrCtx := recrCtx.insert d.name i - - let definitions ← withRecrs recrCtx $ mutualDefs.mapM (·.mapM definitionToIR) - - -- Building and storing the block - let definitionsIr := (definitions.map (match ·.head? with - | some d => [d] | none => [])).flatten - let (blockContAddr, blockMetaAddr) ← commit $ .mutDefBlock definitionsIr - addBlockToStt blockContAddr blockMetaAddr - - -- While iterating on the definitions from the mutual block, we need to track - -- the correct objects to return - let mut ret? : Option (Address × Address) := none - - for name in struct.all do - -- Storing and caching the definition projection - -- Also adds the constant to the array of constants - let some idx := recrCtx.find? name | throw $ .cantFindMutDefIndex name - let (constAddr, metaAddr) ← - commit $ .definitionProj ⟨blockContAddr, blockMetaAddr, idx⟩ - addConstToStt name constAddr metaAddr - if struct.name == name then ret? := some (constAddr, metaAddr) - - match ret? with - | some ret => return ret - | none => throw $ .constantNotContentAddressed struct.name - -partial def definitionToIR (defn : Lean.DefinitionVal) : CanonM Ix.Definition := - return ⟨defn.levelParams.length, ← canonExpr defn.type, - ← canonExpr defn.value, defn.safety == .partial⟩ - -/-- -Content-addresses an inductive and all inductives in the mutual block as a -mutual block, even if the inductive itself is not in a mutual block. - -Content-addressing an inductive involves content-addressing its associated -constructors and recursors, hence the length of this function. --/ -partial def canonInductive (initInd : Lean.InductiveVal) : CanonM (Address × Address):= do - -- `mutualConsts` is the list of the names of all constants associated with an inductive block - -- it has the form: ind₁ ++ ctors₁ ++ recrs₁ ++ ... ++ indₙ ++ ctorsₙ ++ recrsₙ - let mut inds := [] - let mut indCtors := [] - let mut indRecs := [] - let mut nameData : RBMap Lean.Name (List Lean.Name × List Lean.Name) compare - := .empty - for indName in initInd.all do - match ← getLeanConstant indName with - | .inductInfo ind => - let indRecrs := ((← read).constMap.childrenOfWith ind.name - fun c => match c with | .recInfo _ => true | _ => false).map (·.name) - inds := inds ++ [indName] - indCtors := indCtors ++ ind.ctors - indRecs := indRecs ++ indRecrs - nameData := nameData.insert indName (ind.ctors, indRecrs) - | const => throw $ .invalidConstantKind const.name "inductive" const.ctorName - - -- `mutualConsts` is the list of the names of all constants associated with an - -- inductive block: the inductives themselves, the constructors and the recursors - let mutualConsts := inds ++ indCtors ++ indRecs - - let recrCtx := mutualConsts.zipIdx.foldl (init := default) - fun acc (n, i) => acc.insert n i - - -- This part will build the inductive block and add all inductives, - -- constructors and recursors to `consts` - let irInds ← initInd.all.mapM fun name => do match ← getLeanConstant name with - | .inductInfo ind => withRecrs recrCtx do pure $ (← inductiveToIR ind) - | const => throw $ .invalidConstantKind const.name "inductive" const.ctorName - let (blockContAddr, blockMetaAddr) ← commit $ .mutIndBlock irInds - addBlockToStt blockContAddr blockMetaAddr - - -- While iterating on the inductives from the mutual block, we need to track - -- the correct objects to return - let mut ret? : Option (Address × Address) := none - for (indName, indIdx) in initInd.all.zipIdx do - -- Store and cache inductive projections - let name := indName - let (constAddr, metaAddr) ← - commit $ .inductiveProj ⟨blockContAddr, blockMetaAddr, indIdx⟩ - addConstToStt name constAddr metaAddr - if name == initInd.name then ret? := some (constAddr, metaAddr) - - let some (ctors, recrs) := nameData.find? indName - | throw $ .cantFindMutDefIndex indName - - for (ctorName, ctorIdx) in ctors.zipIdx do - -- Store and cache constructor projections - let (constAddr, metaAddr) ← - commit $ .constructorProj ⟨blockContAddr, blockMetaAddr, indIdx, ctorIdx⟩ - addConstToStt ctorName constAddr metaAddr - - for (recrName, recrIdx) in recrs.zipIdx do - -- Store and cache recursor projections - let (constAddr, metaAddr) ← - commit $ .recursorProj ⟨blockContAddr, blockMetaAddr, indIdx, recrIdx⟩ - addConstToStt recrName constAddr metaAddr - - match ret? with - | some ret => return ret - | none => throw $ .constantNotContentAddressed initInd.name - -partial def inductiveToIR (ind : Lean.InductiveVal) : CanonM Ix.Inductive := do - let leanRecs := (← read).constMap.childrenOfWith ind.name - fun c => match c with | .recInfo _ => true | _ => false - let (recs, ctors) ← leanRecs.foldrM (init := ([], [])) - fun r (recs, ctors) => match r with - | .recInfo rv => - if isInternalRec rv.type ind.name then do - let (thisRec, thisCtors) := ← internalRecToIR ind.ctors r - pure (thisRec :: recs, thisCtors) - else do - let thisRec ← externalRecToIR r - pure (thisRec :: recs, ctors) - | _ => throw $ .nonRecursorExtractedFromChildren r.name - let (struct, unit) ← if ind.isRec || ind.numIndices != 0 then pure (false, false) else - match ctors with - -- Structures can only have one constructor - | [ctor] => pure (true, ctor.fields == 0) - | _ => pure (false, false) - return ⟨ind.levelParams.length, ← canonExpr ind.type, ind.numParams, ind.numIndices, - -- NOTE: for the purpose of extraction, the order of `ctors` and `recs` MUST - -- match the order used in `recrCtx` - ctors, recs, ind.isRec, ind.isReflexive, struct, unit⟩ - -partial def internalRecToIR (ctors : List Lean.Name) - : Lean.ConstantInfo → CanonM (Ix.Recursor × List Ix.Constructor) - | .recInfo rec => withLevels rec.levelParams do - let typ ← canonExpr rec.type - let (retCtors, retRules) ← rec.rules.foldrM (init := ([], [])) - fun r (retCtors, retRules) => do - if ctors.contains r.ctor then - let (ctor, rule) ← recRuleToIR r - pure $ (ctor :: retCtors, rule :: retRules) - else pure (retCtors, retRules) -- this is an external recursor rule - let recr := ⟨rec.levelParams.length, typ, rec.numParams, rec.numIndices, - rec.numMotives, rec.numMinors, retRules, rec.k, true⟩ - return (recr, retCtors) - | const => throw $ .invalidConstantKind const.name "recursor" const.ctorName - -partial def recRuleToIR (rule : Lean.RecursorRule) - : CanonM (Ix.Constructor × Ix.RecursorRule) := do - let rhs ← canonExpr rule.rhs - match ← getLeanConstant rule.ctor with - | .ctorInfo ctor => withLevels ctor.levelParams do - let typ ← canonExpr ctor.type - let ctor := ⟨ctor.levelParams.length, typ, ctor.cidx, ctor.numParams, ctor.numFields⟩ - pure (ctor, ⟨rule.nfields, rhs⟩) - | const => throw $ .invalidConstantKind const.name "constructor" const.ctorName - -partial def externalRecToIR : Lean.ConstantInfo → CanonM Recursor - | .recInfo rec => withLevels rec.levelParams do - let typ ← canonExpr rec.type - let rules ← rec.rules.mapM externalRecRuleToIR - return ⟨rec.levelParams.length, typ, rec.numParams, rec.numIndices, - rec.numMotives, rec.numMinors, rules, rec.k, false⟩ - | const => throw $ .invalidConstantKind const.name "recursor" const.ctorName - -partial def externalRecRuleToIR (rule : Lean.RecursorRule) : CanonM RecursorRule := - return ⟨rule.nfields, ← canonExpr rule.rhs⟩ - -/-- -Content-addresses a Lean expression and adds it to the store. - -Constants are the tricky case, for which there are two possibilities: -* The constant belongs to `recrCtx`, representing a recursive call. Those are -encoded as variables with indexes that go beyond the bind indexes -* The constant doesn't belong to `recrCtx`, meaning that it's not a recursion -and thus we can canon the actual constant right away --/ -partial def canonExpr : Lean.Expr → CanonM Expr - | .mdata _ e => canonExpr e - | expr => match expr with - | .bvar idx => do match (← read).bindCtx[idx]? with - -- Bound variables must be in the bind context - | some _ => return .var idx - | none => throw $ .invalidBVarIndex idx - | .sort lvl => return .sort $ ← canonUniv lvl - | .const name lvls => do - let univs ← lvls.mapM canonUniv - match (← read).recrCtx.find? name with - | some i => -- recursing! - return .rec_ i univs - | none => do - let (contAddr, metaAddr) ← canonConst (← getLeanConstant name) - return .const name contAddr metaAddr univs - | .app fnc arg => return .app (← canonExpr fnc) (← canonExpr arg) - | .lam name typ bod info => - return .lam name info (← canonExpr typ) (← withBinder name $ canonExpr bod) - | .forallE name dom img info => - return .pi name info (← canonExpr dom) (← withBinder name $ canonExpr img) - | .letE name typ exp bod nD => - return .letE name (← canonExpr typ) (← canonExpr exp) - (← withBinder name $ canonExpr bod) nD - | .lit lit => return .lit lit - | .proj name idx exp => do - let (contAddr, metaAddr) ← canonConst (← getLeanConstant name) - return .proj name contAddr metaAddr idx (← canonExpr exp) - | .fvar .. => throw $ .freeVariableExpr expr - | .mvar .. => throw $ .metaVariableExpr expr - | .mdata .. => throw $ .metaDataExpr expr - -/-- -A name-irrelevant ordering of Lean expressions. -`weakOrd` contains the best known current mutual ordering --/ -partial def cmpExpr (weakOrd : RBMap Lean.Name Nat compare) : - Lean.Expr → Lean.Expr → CanonM Ordering - | e@(.mvar ..), _ => throw $ .unfilledExprMetavariable e - | _, e@(.mvar ..) => throw $ .unfilledExprMetavariable e - | e@(.fvar ..), _ => throw $ .freeVariableExpr e - | _, e@(.fvar ..) => throw $ .freeVariableExpr e - | .mdata _ x, .mdata _ y => cmpExpr weakOrd x y - | .mdata _ x, y => cmpExpr weakOrd x y - | x, .mdata _ y => cmpExpr weakOrd x y - | .bvar x, .bvar y => return (compare x y) - | .bvar .., _ => return .lt - | _, .bvar .. => return .gt - | .sort x, .sort y => cmpLevel x y - | .sort .., _ => return .lt - | _, .sort .. => return .gt - | .const x xls, .const y yls => do - let univs ← concatOrds <$> (xls.zip yls).mapM fun (x,y) => cmpLevel x y - if univs != .eq then return univs - match weakOrd.find? x, weakOrd.find? y with - | some nx, some ny => return compare nx ny - | none, some _ => return .gt - | some _, none => return .lt - | none, none => - return compare (← canonConst $ ← getLeanConstant x) - (← canonConst $ ← getLeanConstant y) - | .const .., _ => return .lt - | _, .const .. => return .gt - | .app xf xa, .app yf ya => - (· * ·) <$> cmpExpr weakOrd xf yf <*> cmpExpr weakOrd xa ya - | .app .., _ => return .lt - | _, .app .. => return .gt - | .lam _ xt xb _, .lam _ yt yb _ => - (· * ·) <$> cmpExpr weakOrd xt yt <*> cmpExpr weakOrd xb yb - | .lam .., _ => return .lt - | _, .lam .. => return .gt - | .forallE _ xt xb _, .forallE _ yt yb _ => - (· * ·) <$> cmpExpr weakOrd xt yt <*> cmpExpr weakOrd xb yb - | .forallE .., _ => return .lt - | _, .forallE .. => return .gt - | .letE _ xt xv xb _, .letE _ yt yv yb _ => - (· * · * ·) <$> cmpExpr weakOrd xt yt <*> cmpExpr weakOrd xv yv <*> cmpExpr weakOrd xb yb - | .letE .., _ => return .lt - | _, .letE .. => return .gt - | .lit x, .lit y => - return if x < y then .lt else if x == y then .eq else .gt - | .lit .., _ => return .lt - | _, .lit .. => return .gt - | .proj _ nx tx, .proj _ ny ty => do - let ts ← cmpExpr weakOrd tx ty - return concatOrds [compare nx ny, ts] - -/-- AST comparison of two Lean definitions. - `weakOrd` contains the best known current mutual ordering -/ -partial def cmpDef (weakOrd : RBMap Lean.Name Nat compare) - (x : Lean.DefinitionVal) (y : Lean.DefinitionVal) : - CanonM Ordering := do - let ls := compare x.levelParams.length y.levelParams.length - let ts ← cmpExpr weakOrd x.type y.type - let vs ← cmpExpr weakOrd x.value y.value - return concatOrds [ls, ts, vs] - -/-- AST equality between two Lean definitions. - `weakOrd` contains the best known current mutual ordering -/ -@[inline] partial def eqDef (weakOrd : RBMap Lean.Name Nat compare) - (x y : Lean.DefinitionVal) : CanonM Bool := - return (← cmpDef weakOrd x y) == .eq - -/-- -`sortDefs` recursively sorts a list of mutual definitions into weakly equal blocks. -At each stage, we take as input the current best approximation of known weakly equal -blocks as a List of blocks, hence the `List (List DefinitionVal)` as the argument type. -We recursively take the input blocks and resort to improve the approximate known -weakly equal blocks, obtaining a sequence of list of blocks: -``` -dss₀ := [startDefs] -dss₁ := sortDefs dss₀ -dss₂ := sortDefs dss₁ -dss₍ᵢ₊₁₎ := sortDefs dssᵢ ... -``` -Initially, `startDefs` is simply the list of definitions we receive from `DefinitionVal.all`; -since there is no order yet, we treat it as one block all weakly equal. On the other hand, -at the end, there is some point where `dss₍ᵢ₊₁₎ := dssᵢ`, then we have hit a fixed point -and we may end the sorting process. (We claim that such a fixed point exists, although -technically we don't really have a proof.) - -On each iteration, we hope to improve our knowledge of weakly equal blocks and use that -knowledge in the next iteration. e.g. We start with just one block with everything in it, -but the first sort may differentiate the one block into 3 blocks. Then in the second -iteration, we have more information than than first, since the relationship of the 3 blocks -gives us more information; this information may then be used to sort again, turning 3 blocks -into 4 blocks, and again 4 blocks into 6 blocks, etc, until we have hit a fixed point. -This step is done in the computation of `newDss` and then comparing it to the original `dss`. - -Two optimizations: - -1. `names := enum dss` records the ordering information in a map for faster access. - Directly using `List.findIdx?` on dss is slow and introduces `Option` everywhere. - `names` is used as a custom comparison in `ds.sortByM (cmpDef names)`. -2. `normDss/normNewDss`. We want to compare if two lists of blocks are equal. - Technically blocks are sets and their order doesn't matter, but we have encoded - them as lists. To fix this, we sort the list by name before comparing. Note we - could maybe also use `List (RBTree ..)` everywhere, but it seemed like a hassle. --/ -partial def sortDefs (dss : List (List Lean.DefinitionVal)) : - CanonM (List (List Lean.DefinitionVal)) := do - let enum (ll : List (List Lean.DefinitionVal)) := - RBMap.ofList (ll.zipIdx.map fun (xs, n) => xs.map (·.name, n)).flatten - let weakOrd := enum dss _ - let newDss ← (← dss.mapM fun ds => - match ds with - | [] => unreachable! - | [d] => pure [[d]] - | ds => do pure $ (← List.groupByM (eqDef weakOrd) $ - ← ds.sortByM (cmpDef weakOrd))).joinM - - -- must normalize, see comments - let normDss := dss.map fun ds => ds.map (·.name) |>.sort - let normNewDss := newDss.map fun ds => ds.map (·.name) |>.sort - if normDss == normNewDss then return newDss - else sortDefs newDss - -end - -end Ix.CanonM diff --git a/Ix/Claim.lean b/Ix/Claim.lean new file mode 100644 index 00000000..19b43b00 --- /dev/null +++ b/Ix/Claim.lean @@ -0,0 +1,13 @@ +import Ix.Address + +inductive Claim where +| checks (lvls type value: Address) : Claim +| evals (lvls input output type: Address) : Claim +deriving Inhabited, BEq + +instance : ToString Claim where + toString + | .checks lvls type value => s!"#{value} : #{type} @ #{lvls}" + | .evals lvls inp out type => s!"#{inp} ~> #{out} : #{type} @ #{lvls}" + + diff --git a/Ix/Cli/HashCmd.lean b/Ix/Cli/HashCmd.lean index e8f5bb92..3efbd27e 100644 --- a/Ix/Cli/HashCmd.lean +++ b/Ix/Cli/HashCmd.lean @@ -1,17 +1,48 @@ -import Cli - -def runHash (p : Cli.Parsed) : IO UInt32 := do - let input : String := p.positionalArg! "input" |>.as! String - IO.println <| "Input: " ++ input - return 0 - -def hashCmd : Cli.Cmd := `[Cli| - hash VIA runHash; - "Hashes a given Lean source file" - - FLAGS: - e, "example" : String; "Example flag" - - ARGS: - input : String; "Source file input" -] +--import Cli +--import Ix.Cronos +--import Ix.Common +--import Ix.CanonM +--import Lean +-- +--def runHash (p : Cli.Parsed) : IO UInt32 := do +-- -- Get Lean source file name +-- let source : String := p.positionalArg! "input" |>.as! String +-- IO.println <| "Source: " ++ source +-- -- Run Lean frontend +-- let mut cronos ← Cronos.new.clock "Run Lean frontend" +-- Lean.setLibsPaths source +-- --IO.println <| "setlibs" +-- let path := ⟨source⟩ +-- let leanEnv ← Lean.runFrontend (← IO.FS.readFile path) path +-- IO.println <| s!"constant len {leanEnv.constants.toList.length}" +-- leanEnv.constants.forM fun n _info => do +-- IO.println <| s!"constants {n}" +-- let (constMap, delta) := leanEnv.getConstsAndDelta +-- IO.println <| s!"constMap len {constMap.toList.length}" +-- constMap.forM (fun n _info => IO.println <| s!"constMap {n}") +-- IO.println <| s!"delta len {delta.length}" +-- delta.forM fun x => do +-- IO.println <| s!"delta {x.name}" +-- +-- -- IO.println <| "content-address" +-- -- -- Start content-addressing +-- -- cronos ← cronos.clock "Content-address" +-- -- let stt ← match ← Ix.CanonM.canon constMap delta with +-- -- | .error err => IO.eprintln err; return 1 +-- -- | .ok stt => pure stt +-- -- cronos ← cronos.clock "Content-address" +-- -- stt.store.forM fun adr _ => do +-- -- IO.println <| s!"{adr}" +-- +-- return 0 +-- +--def hashCmd : Cli.Cmd := `[Cli| +-- hash VIA runHash; +-- "Hashes a given Lean source file" +-- +-- FLAGS: +-- e, "example" : String; "Example flag" +-- +-- ARGS: +-- input : String; "Source file input" +--] diff --git a/Ix/Cli/ProveCmd.lean b/Ix/Cli/ProveCmd.lean index a1f40698..20a9e7c4 100644 --- a/Ix/Cli/ProveCmd.lean +++ b/Ix/Cli/ProveCmd.lean @@ -1,17 +1,100 @@ import Cli +import Ix.Cronos +import Ix.Common +import Ix.CompileM +import Ix.Store +import Ix.Address +import Ix.Meta +import Lean -def runProve (p : Cli.Parsed) : IO UInt32 := do - let input : String := p.positionalArg! "input" |>.as! String - IO.println <| "Input: " ++ input +--❯ ix prove IxTest.lean "id'" +--typechecking: +--id' (A : Type) (x : A) : A +--claim: #bbd740022aa44acd553c52e156807a5571428220a926377fe3c57d63b06a99f4 : #ba33b735b743386477f7a0e6802c67d388c165cab0e34b04880b50270205f265 @ #0000000000000000000000000000000000000000000000000000000000000000 +def runProveCheck + (env: Lean.Environment) + (constInfo: Lean.ConstantInfo) + (commit: Bool) + : IO UInt32 + := do + let constSort <- runMeta (Lean.Meta.inferType constInfo.type) env + let signature <- runMeta (Lean.PrettyPrinter.ppSignature constInfo.name) env + 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) + IO.println $ s!"claim: {claim}" + -- TODO: prove return 0 +def mkConst' (constName : Lean.Name) : Lean.MetaM Lean.Expr := do + return Lean.mkConst constName (← (← Lean.getConstInfo constName).levelParams.mapM fun _ => Lean.Meta.mkFreshLevelMVar) + +--ix prove IxTest.lean "id'" --eval=Nat,one +--evaluating: +--id' (A : Type) (x : A) : A +--id' Nat one +-- ~> 1 +-- : Nat +-- @ [] +--claim: #88ba2a7b099ce94a030eef202dc26ee3d9eb088057830049b926c7e88044bba1 ~> #d5ea7e6e7a3ee02780ba254a0becfe1fe712436a5a30832095ab71f7c64e25cd : #41ba41a9691e8167a387046f736a82ce0ec1601e7fb996c58d5930887c4b7764 @ #0000000000000000000000000000000000000000000000000000000000000000 +def runProveEval + (env: Lean.Environment) + (constInfo: Lean.ConstantInfo) + (args: Array String) + (commit: Bool) + : IO UInt32 + := do + let signature <- runMeta (Lean.PrettyPrinter.ppSignature constInfo.name) env + let args : Array Lean.Expr <- args.mapM $ fun a => do + let argInfo <- match env.constants.find? a.toName with + | some c => runMeta (mkConst' c.name) env + | none => throw $ IO.userError s!"unknown constant {a.toName}" + let (lvls, input, output, type, sort) <- + runMeta (metaMakeEvalClaim constInfo.name (args.toList)) env + IO.println "evaluating:" + IO.println signature.fmt.pretty + 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!"{inputPretty}" + 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) + IO.println $ s!"claim: {claim}" + -- TODO: prove + return 0 + + + +def runProve (p: Cli.Parsed): IO UInt32 := do + let input : String := p.positionalArg! "input" |>.as! String + let const : String := p.positionalArg! "const" |>.as! String + let path := ⟨input⟩ + Lean.setLibsPaths input + let env ← Lean.runFrontend (← IO.FS.readFile path) path + let constInfo <- match env.constants.find? const.toName with + | some c => pure c + | none => throw $ IO.userError s!"unknown constant {const.toName}" + let commit := p.hasFlag "commit" + if let some evalArgs := p.flag? "eval" + then runProveEval env constInfo (evalArgs.as! (Array String)) commit + else runProveCheck env constInfo commit + return 0 + + def proveCmd : Cli.Cmd := `[Cli| prove VIA runProve; - "Generates a ZK proof of a given Lean source file" + "Generates a ZK proof of a given Lean constant" FLAGS: - e, "example" : String; "Example flag" + cron, "cronos" : String; "enable Cronos timings" + eval, "eval" : Array String; "prove evaluation with arguments" ARGS: input : String; "Source file input" + const : String; "constant name" ] diff --git a/Ix/Cli/StoreCmd.lean b/Ix/Cli/StoreCmd.lean new file mode 100644 index 00000000..40ef5196 --- /dev/null +++ b/Ix/Cli/StoreCmd.lean @@ -0,0 +1,72 @@ +import Cli +import Ix.Cronos +import Ix.Common +import Ix.CompileM +import Ix.Store +import Ix.Address +import Lean + +-- ix store +-- ix store get
+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 + stt.names.forM fun name (const, meta) => do + IO.println <| s!"{name}:" + IO.println <| s!" #{const}" + --IO.println <| s!" {repr <| stt.store.find! const}" + --IO.println <| s!" {hexOfBytes (Ixon.Serialize.put (stt.store.find! const))}" + IO.println <| s!" #{meta}" + --IO.println <| s!" {repr <| stt.store.find! meta}" + --IO.println <| s!" {hexOfBytes (Ixon.Serialize.put (stt.store.find! meta))}" + --stt.store.forM fun adr const => do + -- IO.println <| s!"adr' {adr}" + -- IO.println <| s!"const {repr const}" + -- let adr' <- StoreIO.toIO (writeConst const) + -- IO.println <| s!"adr' {adr}" + -- let const' <- StoreIO.toIO (readConst adr') + -- IO.println <| s!"const' {repr const'}" + cronos ← cronos.clock "content-address" + IO.println cronos.summary + return 0 + +def runGet (p : Cli.Parsed) : IO UInt32 := do + let input : String := p.positionalArg! "address" |>.as! String + let address : Address <- IO.ofExcept $ + match Address.fromString input with + | .some a => .ok a + | .none => .error "bad address" + let const <- StoreIO.toIO (Store.readConst address) + IO.println <| s!"{repr const}" + return 0 + +def storeGetCmd : Cli.Cmd := `[Cli| + get VIA runGet; + "print a store entry" + ARGS: + address : String; "Ix address" +] + +def storeCmd : Cli.Cmd := `[Cli| + store VIA runStore; + "Interact with the Ix store" + + FLAGS: + cron, "cronos" : String; "enable Cronos timings" + + ARGS: + source : String; "Source file input" + + SUBCOMMANDS: + storeGetCmd +] + diff --git a/Ix/Cli/TestCmd.lean b/Ix/Cli/TestCmd.lean deleted file mode 100644 index 33b3f1f3..00000000 --- a/Ix/Cli/TestCmd.lean +++ /dev/null @@ -1,46 +0,0 @@ -import Cli -import Blake3 -import Ix.Address -import Ix.Store -import Ix.Ixon.Expr -import Ix.Ixon.Const -import Ix.Ixon.Serialize -import Init.System.FilePath -import Init.System.IO -import Init.System.IOError - -def runTest (p : Cli.Parsed) : IO UInt32 := do - let input : String := p.positionalArg! "input" |>.as! String - IO.println s!"Input: {input}" - let inputBA := input.toUTF8 - IO.println s!"Input UTF8: {byteArrayToHex inputBA}" - let const : Ixon.Const := .defn - { lvls := 0, type := .strl "BAD", value := .strl input, part := .true} - IO.println s!"Const: {repr const}" - let bytes := Ixon.Serialize.put const - IO.println s!"Bytes: {byteArrayToHex bytes}" - let addr := Address.blake3 bytes - IO.println s!"Address: {byteArrayToHex addr.hash}" - let home ← EIO.toIO storeErrorToIOError getHomeDir - IO.println s!"HOME at {home}" - let store ← EIO.toIO storeErrorToIOError storeDir - IO.println s!"Store at {store}" - EIO.toIO storeErrorToIOError ensureStoreDir - IO.println s!"write entry at {store / (byteArrayToHex addr.hash)}" - EIO.toIO storeErrorToIOError (writeConst const) - IO.println s!"read entry at {store / (byteArrayToHex addr.hash)}" - let const' ← EIO.toIO storeErrorToIOError (readConst addr) - IO.println s!"Const': {repr const'}" - IO.println s!"matching {const == const'}" - return 0 - -def testCmd : Cli.Cmd := `[Cli| - test VIA runTest; - "run a test" - - FLAGS: - e, "example" : String; "Example flag" - - ARGS: - input : String; "Source file input" -] diff --git a/Ix/Common.lean b/Ix/Common.lean index b361d8f6..266fe2f7 100644 --- a/Ix/Common.lean +++ b/Ix/Common.lean @@ -1,4 +1,5 @@ import Lean +import Batteries -- TODO: move to a utils namespace def compareList [Ord α] : List α -> List α -> Ordering @@ -110,6 +111,12 @@ end List namespace Lean +def ConstantInfo.formatAll (c : ConstantInfo) : String := + match c.all with + | [ ] + | [_] => "" + | all => " " ++ all.toString + def ConstantInfo.ctorName : ConstantInfo → String | .axiomInfo _ => "axiom" | .defnInfo _ => "definition" @@ -127,4 +134,86 @@ def ConstMap.childrenOfWith (map : ConstMap) (name : Name) | .num n .. => if n == name && p c then c :: acc else acc | _ => acc +--def ConstMap.patchUnsafeRec (cs : ConstMap) : ConstMap := +-- let unsafes : Batteries.RBSet Name compare := cs.fold (init := .empty) +-- fun acc n _ => match n with +-- | .str n "_unsafe_rec" => acc.insert n +-- | _ => acc +-- cs.map fun c => match c with +-- | .opaqueInfo o => +-- if unsafes.contains o.name then +-- .opaqueInfo ⟨ +-- o.toConstantVal, mkConst (o.name ++ `_unsafe_rec), +-- o.isUnsafe, o.levelParams ⟩ +-- else .opaqueInfo o +-- | _ => c + +def PersistentHashMap.filter [BEq α] [Hashable α] + (map : PersistentHashMap α β) (p : α → β → Bool) : PersistentHashMap α β := + map.foldl (init := .empty) fun acc x y => + match p x y with + | true => acc.insert x y + | false => acc + +def Environment.getDelta (env : Environment) + : PersistentHashMap Name ConstantInfo := + env.constants.map₂.filter (fun n _ => !n.isInternal) + +def Environment.getConstMap (env : Environment) + : Std.HashMap Name ConstantInfo := + env.constants.map₁.filter (fun n _ => !n.isInternal) + +/-- +Sets the directories where `olean` files can be found. + +This function must be called before `runFrontend` if the file to be compiled has +imports (the automatic imports from `Init` also count). +-/ + +-- TODO: parse JSON properly +-- TODO: Get import of Init and Std working +def setLibsPaths (s: String) : IO Unit := do + let out ← IO.Process.output { + cmd := "lake" + args := #["setup-file", s] + } + --IO.println s!"setup-file {out.stdout}" + --IO.println s!"setup-file {out.stderr}" + let split := out.stdout.splitOn "\"oleanPath\":[" |>.getD 1 "" + let split := split.splitOn "],\"loadDynlibPaths\":[" |>.getD 0 "" + let paths := split.replace "\"" "" |>.splitOn ","|>.map System.FilePath.mk + --IO.println s!"paths {paths}" + Lean.initSearchPath (← Lean.findSysroot) paths + +def runCmd' (cmd : String) (args : Array String) : IO $ Except String String := do + let out ← IO.Process.output { cmd := cmd, args := args } + return if out.exitCode != 0 then .error out.stderr + else .ok out.stdout + +def checkToolchain : IO Unit := do + match ← runCmd' "lake" #["--version"] with + | .error e => throw $ IO.userError e + | .ok out => + let version := (out.splitOn "(Lean version ")[1]! + let version := version.splitOn ")" |>.head! + let expectedVersion := Lean.versionString + if version != expectedVersion then + IO.println s!"Warning: expected toolchain '{expectedVersion}' but got '{version}'" + +open Elab in +open System (FilePath) in +def runFrontend (input : String) (filePath : FilePath) : IO Environment := do + checkToolchain + let inputCtx := Parser.mkInputContext input filePath.toString + let (header, parserState, messages) ← Parser.parseHeader inputCtx + let (env, messages) ← processHeader header default messages inputCtx 0 + let env := env.setMainModule default + let commandState := Command.mkState env messages default + let s ← IO.processCommands inputCtx parserState commandState + let msgs := s.commandState.messages + if msgs.hasErrors then + throw $ IO.userError $ "\n\n".intercalate $ + (← msgs.toList.mapM (·.toString)).map String.trim + else return s.commandState.env + end Lean diff --git a/Ix/CompileM.lean b/Ix/CompileM.lean new file mode 100644 index 00000000..761a3a18 --- /dev/null +++ b/Ix/CompileM.lean @@ -0,0 +1,761 @@ +import Batteries.Data.RBMap +import Ix.TransportM +import Ix.Ixon.Metadata +import Ix.Ixon.Const +import Ix.Ixon.Serialize +import Ix.Common +import Ix.Store + +open Batteries (RBMap) +open Batteries (RBSet) +open Ix.TransportM + +namespace Ix.Compile + +inductive CompileError +| unknownConstant : Lean.Name → CompileError +| unfilledLevelMetavariable : Lean.Level → CompileError +| unfilledExprMetavariable : Lean.Expr → CompileError +| invalidBVarIndex : Nat → CompileError +| freeVariableExpr : Lean.Expr → CompileError +| metaVariableExpr : Lean.Expr → CompileError +| metaDataExpr : Lean.Expr → CompileError +| levelNotFound : Lean.Name → List Lean.Name → CompileError +| invalidConstantKind : Lean.Name → String → String → CompileError +| constantNotContentAddressed : Lean.Name → CompileError +| nonRecursorExtractedFromChildren : Lean.Name → CompileError +| cantFindMutDefIndex : Lean.Name → CompileError +| transportError : TransportError → CompileError +| kernelException : String → CompileError +| storeError : StoreError → CompileError +| todo + +instance : ToString CompileError where toString +| .unknownConstant n => s!"Unknown constant '{n}'" +| .unfilledLevelMetavariable l => s!"Unfilled level metavariable on universe '{l}'" +| .unfilledExprMetavariable e => s!"Unfilled level metavariable on expression '{e}'" +| .invalidBVarIndex idx => s!"Invalid index {idx} for bound variable context" +| .freeVariableExpr e => s!"Free variable in expression '{e}'" +| .metaVariableExpr e => s!"Metavariable in expression '{e}'" +| .metaDataExpr e => s!"Meta data in expression '{e}'" +| .levelNotFound n ns => s!"'Level {n}' not found in '{ns}'" +| .invalidConstantKind n ex gt => + s!"Invalid constant kind for '{n}'. Expected '{ex}' but got '{gt}'" +| .constantNotContentAddressed n => s!"Constant '{n}' wasn't content-addressed" +| .nonRecursorExtractedFromChildren n => + s!"Non-recursor '{n}' extracted from children" +| .cantFindMutDefIndex n => s!"Can't find index for mutual definition '{n}'" +| .transportError n => s!"Transport error '{repr n}'" +| .kernelException e => e +| _ => s!"todo" + +structure CompileEnv where + univCtx : List Lean.Name + bindCtx : List Lean.Name + mutCtx : RBMap Lean.Name Nat compare + maxHeartBeats: USize + persist : Bool + +def CompileEnv.init (maxHeartBeats: USize): CompileEnv := + ⟨default, default, default, maxHeartBeats, true⟩ + +structure CompileState where + env: Lean.Environment + names: RBMap Lean.Name (Address × Address) compare + store: RBMap Address Ixon.Const compare + cache: RBMap Ix.Const (Address × Address) compare + comms: RBMap Lean.Name (Address × Address) compare + axioms: RBMap Lean.Name (Address × Address) compare + blocks: RBSet (Address × Address) compare + +def CompileState.init (env: Lean.Environment): CompileState := + ⟨env, default, default, default, default, default, default⟩ + +abbrev CompileM := + ReaderT CompileEnv <| ExceptT CompileError <| StateT CompileState IO + +def CompileM.runIO (maxHeartBeats: USize) (stt: CompileState) (c : CompileM α) + : IO (Except CompileError α × CompileState) := do + StateT.run (ReaderT.run c (.init maxHeartBeats)) stt + +def CompileM.runIO' (maxHeartBeats: USize) (stt: CompileState) (c : CompileM α) + : IO (α × CompileState) := do + let (res, stt) <- c.runIO maxHeartBeats stt + let res <- IO.ofExcept res + return (res, stt) + +def CompileM.liftIO (io: IO α): CompileM α := + monadLift io + +def liftStoreIO (io: StoreIO α): CompileM α := do + match <- CompileM.liftIO (EIO.toIO' io) with + | .ok a => return a + | .error e => throw (.storeError e) + +def writeToStore (const: Ixon.Const): CompileM Address := do + let addr <- if (<- read).persist + then liftStoreIO (Store.writeConst const) + else pure (Address.blake3 (Ixon.Serialize.put const)) + modifyGet fun stt => (addr, { stt with + store := stt.store.insert addr const + }) + +def IO.freshSecret : IO Address := do + IO.setRandSeed (← IO.monoNanosNow) + let mut secret : ByteArray := default + for _ in [:32] do + let rand ← IO.rand 0 (UInt8.size - 1) + secret := secret.push rand.toUInt8 + return ⟨secret⟩ + +def freshSecret : CompileM Address := do + CompileM.liftIO IO.freshSecret + +-- add binding name to local context +def withBinder (name: Lean.Name) : CompileM α -> CompileM α := + withReader $ fun c => { c with bindCtx := name :: c.bindCtx } + +-- add levels to local context +def withLevels (lvls : List Lean.Name) : CompileM α -> CompileM α := + withReader $ fun c => { c with univCtx := lvls } + +-- add mutual recursion info to local context +def withMutCtx (mutCtx : RBMap Lean.Name Nat compare) : CompileM α -> CompileM α := + withReader $ fun c => { c with mutCtx := mutCtx } + +-- reset local context +def resetCtx : CompileM α -> CompileM α := + withReader $ fun c => { c with univCtx := [], bindCtx := [], mutCtx := .empty } + +def resetCtxWithLevels (lvls: List Lean.Name) : CompileM α -> CompileM α := + withReader $ fun c => { c with univCtx := lvls, bindCtx := [], mutCtx := .empty } + +-- lookup or compute the addresses of a constant +def hashConst (const: Ix.Const) : CompileM (Address × Address) := do + match (<- get).cache.find? const with + | some (anonAddr, metaAddr) => pure (anonAddr, metaAddr) + | none => do + let (anonIxon, metaIxon) <- match constToIxon const with + | .ok (a, m) => pure (a, m) + | .error e => throw (.transportError e) + let anonAddr <- writeToStore anonIxon + let metaAddr <- writeToStore metaIxon + modifyGet fun stt => ((anonAddr, metaAddr), { stt with + cache := stt.cache.insert const (anonAddr, metaAddr) + }) + +scoped instance : HMul Ordering Ordering Ordering where hMul + | .gt, _ => .gt + | .lt, _ => .lt + | .eq, x => x + +def concatOrds : List Ordering → Ordering := + List.foldl (· * ·) .eq + +/-- Defines an ordering for Lean universes -/ +def compareLevel (x : Lean.Level) (y : Lean.Level) : CompileM Ordering := + match x, y with + | .mvar .., _ => throw $ .unfilledLevelMetavariable x + | _, .mvar .. => throw $ .unfilledLevelMetavariable y + | .zero, .zero => return .eq + | .zero, _ => return .lt + | _, .zero => return .gt + | .succ x, .succ y => compareLevel x y + | .succ .., _ => return .lt + | _, .succ .. => return .gt + | .max lx ly, .max rx ry => + (· * ·) <$> compareLevel lx rx <*> compareLevel ly ry + | .max .., _ => return .lt + | _, .max .. => return .gt + | .imax lx ly, .imax rx ry => + (· * ·) <$> compareLevel lx rx <*> compareLevel ly ry + | .imax .., _ => return .lt + | _, .imax .. => return .gt + | .param x, .param y => do + let lvls := (← read).univCtx + match (lvls.idxOf? x), (lvls.idxOf? y) with + | some xi, some yi => return (compare xi yi) + | none, _ => throw $ .levelNotFound x lvls + | _, none => throw $ .levelNotFound y lvls + +/-- Canonicalizes a Lean universe level and adds it to the store -/ +def compileLevel : Lean.Level → CompileM Ix.Univ +| .zero => pure .zero +| .succ u => return .succ (← compileLevel u) +| .max a b => return .max (← compileLevel a) (← compileLevel b) +| .imax a b => return .imax (← compileLevel a) (← compileLevel b) +| .param name => do + let lvls := (← read).univCtx + match lvls.idxOf? name with + | some n => pure $ .var name n + | none => throw $ .levelNotFound name lvls +| l@(.mvar ..) => throw $ .unfilledLevelMetavariable l + +/-- Retrieves a Lean constant from the environment by its name -/ +def findLeanConst (name : Lean.Name) : CompileM Lean.ConstantInfo := do + match (← get).env.constants.find? name with + | some const => pure const + | none => throw $ .unknownConstant name + +/-- Check if expression is an internal recursor --/ +def isInternalRec (expr : Lean.Expr) (name : Lean.Name) : Bool := + match expr with + | .forallE _ t e _ => match e with + | .forallE .. => isInternalRec e name + | _ => isInternalRec t name -- t is the major premise + | .app e .. => isInternalRec e name + | .const n .. => n == name + | _ => false + +mutual + +/-- compile Lean Constant --/ +partial def compileConst (const : Lean.ConstantInfo) + : CompileM (Address × Address) := do + match (← get).names.find? const.name with + | some (anonAddr, metaAddr) => pure (anonAddr, metaAddr) + | none => match const with + | .defnInfo val => + resetCtxWithLevels val.levelParams $ compileDefinition val + | .inductInfo val => + resetCtxWithLevels val.levelParams $ compileInductive val + | .ctorInfo val => do + match ← findLeanConst val.induct with + | .inductInfo ind => discard $ compileConst (.inductInfo ind) + | const => + throw $ .invalidConstantKind const.name "inductive" const.ctorName + -- this should return by finding the ctor in names via the above some case + compileConst const + | .recInfo val => do + match ← findLeanConst val.getMajorInduct with + | .inductInfo ind => discard $ compileConst (.inductInfo ind) + | const => + throw $ .invalidConstantKind const.name "inductive" const.ctorName + -- this should return by finding the recr in names via the above some case + compileConst const + -- The rest adds the constants to the cache one by one + | .axiomInfo val => resetCtxWithLevels const.levelParams do + let c := .axiom ⟨val.levelParams.length, ← compileExpr val.type⟩ + let (anonAddr, metaAddr) ← hashConst c + modify fun stt => { stt with + axioms := stt.axioms.insert const.name (anonAddr, metaAddr) + names := stt.names.insert const.name (anonAddr, metaAddr) + } + return (metaAddr, metaAddr) + | .thmInfo val => resetCtxWithLevels const.levelParams do + let type <- compileExpr val.type + let value <- compileExpr val.value + let c := .theorem ⟨val.levelParams.length, type, value⟩ + let (anonAddr, metaAddr) ← hashConst c + modify fun stt => { stt with + names := stt.names.insert const.name (anonAddr, metaAddr) + } + return (metaAddr, metaAddr) + | .opaqueInfo val => resetCtxWithLevels const.levelParams do + let mutCtx := .single val.name 0 + let type <- compileExpr val.type + let value <- withMutCtx mutCtx $ compileExpr val.value + let c := .opaque ⟨val.levelParams.length, type, value⟩ + let (anonAddr, metaAddr) ← hashConst c + modify fun stt => { stt with + names := stt.names.insert const.name (anonAddr, metaAddr) + } + return (metaAddr, metaAddr) + | .quotInfo val => resetCtxWithLevels const.levelParams do + let type <- compileExpr val.type + let c := .quotient ⟨val.levelParams.length, type, val.kind⟩ + let (anonAddr, metaAddr) ← hashConst c + modify fun stt => { stt with + axioms := (stt.axioms.insert const.name (anonAddr, metaAddr)) + names := stt.names.insert const.name (anonAddr, metaAddr) + } + return (metaAddr, metaAddr) + +/-- compile possibly mutual Lean definition --/ +partial def compileDefinition (struct: Lean.DefinitionVal) + : CompileM (Address × Address) := do + -- If the mutual size is one, simply content address the single definition + if struct.all matches [_] then + let defn <- withMutCtx (.single struct.name 0) $ definitionToIR struct + let (anonAddr, metaAddr) <- hashConst $ .definition defn + modify fun stt => { stt with + names := stt.names.insert struct.name (anonAddr, metaAddr) + } + return (anonAddr, metaAddr) + -- Collecting and sorting all definitions in the mutual block + let mutualDefs <- struct.all.mapM fun name => do + match <- findLeanConst name with + | .defnInfo defn => pure defn + | const => + throw $ .invalidConstantKind const.name "definition" const.ctorName + let mutualDefs <- sortDefs [mutualDefs] + -- Building the `mutCtx` + let mut mutCtx := default + for (ds, i) in List.zipIdx mutualDefs do + for d in ds do + mutCtx := mutCtx.insert d.name i + let definitions ← withMutCtx mutCtx $ mutualDefs.mapM (·.mapM definitionToIR) + -- Building and storing the block + -- TODO: check if this flatten call actually makes sense + let definitionsIR := (definitions.map (match ·.head? with + | some d => [d] | none => [])).flatten + let (blockAnonAddr, blockMetaAddr) ← hashConst $ .mutDefBlock definitionsIR + modify fun stt => + { stt with blocks := stt.blocks.insert (blockAnonAddr, blockMetaAddr) } + -- While iterating on the definitions from the mutual block, we need to track + -- the correct objects to return + let mut ret? : Option (Address × Address) := none + for name in struct.all do + -- Storing and caching the definition projection + -- Also adds the constant to the array of constants + let some idx := mutCtx.find? name | throw $ .cantFindMutDefIndex name + let (anonAddr, metaAddr) ← + hashConst $ .definitionProj ⟨blockAnonAddr, blockMetaAddr, idx⟩ + modify fun stt => { stt with + names := stt.names.insert name (anonAddr, metaAddr) + } + if struct.name == name then ret? := some (anonAddr, metaAddr) + match ret? with + | some ret => return ret + | none => throw $ .constantNotContentAddressed struct.name + + +partial def definitionToIR (defn: Lean.DefinitionVal) + : CompileM Ix.Definition := do + let type <- compileExpr defn.type + let value <- compileExpr defn.value + return ⟨defn.levelParams.length, type, value, defn.safety == .partial⟩ + +/-- +Content-addresses an inductive and all inductives in the mutual block as a +mutual block, even if the inductive itself is not in a mutual block. + +Content-addressing an inductive involves content-addressing its associated +constructors and recursors, hence the complexity of this function. +-/ +partial def compileInductive (initInd: Lean.InductiveVal) + : CompileM (Address × Address) := do + let mut inds := [] + let mut indCtors := [] + let mut indRecs := [] + let mut nameData : RBMap Lean.Name (List Lean.Name × List Lean.Name) compare + := .empty + for indName in initInd.all do + match ← findLeanConst indName with + | .inductInfo ind => + let indRecrs := ((← get).env.constants.childrenOfWith ind.name + fun c => match c with | .recInfo _ => true | _ => false).map (·.name) + inds := inds ++ [indName] + indCtors := indCtors ++ ind.ctors + indRecs := indRecs ++ indRecrs + nameData := nameData.insert indName (ind.ctors, indRecrs) + | const => throw $ .invalidConstantKind const.name "inductive" const.ctorName + -- `mutualConsts` is the list of the names of all constants associated with an + -- inductive block: the inductives themselves, the constructors and the recursors + let mutualConsts := inds ++ indCtors ++ indRecs + let mutCtx := mutualConsts.zipIdx.foldl (init := default) + fun acc (n, i) => acc.insert n i + -- This part builds the inductive block + -- and adds all inductives, constructors and recursors to `consts` + let irInds ← initInd.all.mapM fun name => do match ← findLeanConst name with + | .inductInfo ind => withMutCtx mutCtx do pure $ (← inductiveToIR ind) + | const => throw $ .invalidConstantKind const.name "inductive" const.ctorName + let (blockAnonAddr, blockMetaAddr) ← hashConst $ .mutIndBlock irInds + modify fun stt => + { stt with blocks := stt.blocks.insert (blockAnonAddr, blockMetaAddr) } + -- While iterating on the inductives from the mutual block, we need to track + -- the correct objects to return + let mut ret? : Option (Address × Address) := none + for (indName, indIdx) in initInd.all.zipIdx do + -- Store and cache inductive projections + let name := indName + let (anonAddr, metaAddr) ← + hashConst $ .inductiveProj ⟨blockAnonAddr, blockMetaAddr, indIdx⟩ + modify fun stt => { stt with + names := stt.names.insert name (anonAddr, metaAddr) + } + if name == initInd.name then ret? := some (anonAddr, metaAddr) + let some (ctors, recrs) := nameData.find? indName + | throw $ .cantFindMutDefIndex indName + for (ctorName, ctorIdx) in ctors.zipIdx do + -- Store and cache constructor projections + let (anonAddr, metaAddr) ← + hashConst $ .constructorProj + ⟨blockAnonAddr, blockMetaAddr, indIdx, ctorIdx⟩ + modify fun stt => { stt with + names := stt.names.insert ctorName (anonAddr, metaAddr) + } + for (recrName, recrIdx) in recrs.zipIdx do + -- Store and cache recursor projections + let (anonAddr, metaAddr) ← + hashConst $ .recursorProj + ⟨blockAnonAddr, blockMetaAddr, indIdx, recrIdx⟩ + modify fun stt => { stt with + names := stt.names.insert recrName (anonAddr, metaAddr) + } + match ret? with + | some ret => return ret + | none => throw $ .constantNotContentAddressed initInd.name + +partial def inductiveToIR (ind : Lean.InductiveVal) : CompileM Ix.Inductive := do + let leanRecs := (← get).env.constants.childrenOfWith ind.name + fun c => match c with | .recInfo _ => true | _ => false + let (recs, ctors) ← leanRecs.foldrM (init := ([], [])) + fun r (recs, ctors) => match r with + | .recInfo rv => + if isInternalRec rv.type ind.name then do + let (thisRec, thisCtors) := ← internalRecToIR ind.ctors r + pure (thisRec :: recs, thisCtors) + else do + let thisRec ← externalRecToIR r + pure (thisRec :: recs, ctors) + | _ => throw $ .nonRecursorExtractedFromChildren r.name + let (struct, unit) ← if ind.isRec || ind.numIndices != 0 + then pure (false, false) + else + match ctors with + -- Structures can only have one constructor + | [ctor] => pure (true, ctor.fields == 0) + | _ => pure (false, false) + return ⟨ind.levelParams.length, ← compileExpr ind.type, ind.numParams, ind.numIndices, + -- NOTE: for the purpose of extraction, the order of `ctors` and `recs` MUST + -- match the order used in `recrCtx` + ctors, recs, ind.isRec, ind.isReflexive, struct, unit⟩ + +partial def internalRecToIR (ctors : List Lean.Name) + : Lean.ConstantInfo → CompileM (Ix.Recursor × List Ix.Constructor) + | .recInfo rec => withLevels rec.levelParams do + let typ ← compileExpr rec.type + let (retCtors, retRules) ← rec.rules.foldrM (init := ([], [])) + fun r (retCtors, retRules) => do + if ctors.contains r.ctor then + let (ctor, rule) ← recRuleToIR r + pure $ (ctor :: retCtors, rule :: retRules) + else pure (retCtors, retRules) -- this is an external recursor rule + let recr := ⟨rec.levelParams.length, typ, rec.numParams, rec.numIndices, + rec.numMotives, rec.numMinors, retRules, rec.k, true⟩ + return (recr, retCtors) + | const => throw $ .invalidConstantKind const.name "recursor" const.ctorName + +partial def recRuleToIR (rule : Lean.RecursorRule) + : CompileM (Ix.Constructor × Ix.RecursorRule) := do + let rhs ← compileExpr rule.rhs + match ← findLeanConst rule.ctor with + | .ctorInfo ctor => withLevels ctor.levelParams do + let typ ← compileExpr ctor.type + let ctor := + ⟨ctor.levelParams.length, typ, ctor.cidx, ctor.numParams, ctor.numFields⟩ + pure (ctor, ⟨rule.nfields, rhs⟩) + | const => + throw $ .invalidConstantKind const.name "constructor" const.ctorName + +partial def externalRecToIR : Lean.ConstantInfo → CompileM Recursor + | .recInfo rec => withLevels rec.levelParams do + let typ ← compileExpr rec.type + let rules ← rec.rules.mapM externalRecRuleToIR + return ⟨rec.levelParams.length, typ, rec.numParams, rec.numIndices, + rec.numMotives, rec.numMinors, rules, rec.k, false⟩ + | const => throw $ .invalidConstantKind const.name "recursor" const.ctorName + +partial def externalRecRuleToIR (rule : Lean.RecursorRule) + : CompileM RecursorRule := + return ⟨rule.nfields, ← compileExpr rule.rhs⟩ + +/-- +Content-addresses a Lean expression and adds it to the store. + +Constants are the tricky case, for which there are two possibilities: +* The constant belongs to `mutCtx`, representing a recursive call. Those are +encoded as `.rec_` with indexes based on order in the mutual definition +* The constant doesn't belong to `mutCtx`, meaning that it's not a recursion +and thus we can canon the actual constant right away +-/ +partial def compileExpr : Lean.Expr → CompileM Expr +| .mdata _ e => compileExpr e +| expr => match expr with + | .bvar idx => do match (← read).bindCtx[idx]? with + -- Bound variables must be in the bind context + | some _ => return .var idx + | none => throw $ .invalidBVarIndex idx + | .sort lvl => return .sort $ ← compileLevel lvl + | .const name lvls => do + let univs ← lvls.mapM compileLevel + match (← read).mutCtx.find? name with + -- recursing! + | some i => return .rec_ i univs + | none => match (<- get).comms.find? name with + | some (commAddr, metaAddr) => do + return .const name commAddr metaAddr univs + | none => do + let (contAddr, metaAddr) ← compileConst (← findLeanConst name) + return .const name contAddr metaAddr univs + | .app fnc arg => return .app (← compileExpr fnc) (← compileExpr arg) + | .lam name typ bod info => + return .lam name info (← compileExpr typ) (← withBinder name $ compileExpr bod) + | .forallE name dom img info => + return .pi name info (← compileExpr dom) (← withBinder name $ compileExpr img) + | .letE name typ exp bod nD => + return .letE name (← compileExpr typ) (← compileExpr exp) + (← withBinder name $ compileExpr bod) nD + | .lit lit => return .lit lit + | .proj name idx exp => do + let (contAddr, metaAddr) ← compileConst (← findLeanConst name) + return .proj name contAddr metaAddr idx (← compileExpr exp) + | .fvar .. => throw $ .freeVariableExpr expr + | .mvar .. => throw $ .metaVariableExpr expr + | .mdata .. => throw $ .metaDataExpr expr + +partial def makeLeanDef + (name: Lean.Name) (levelParams: List Lean.Name) (type value: Lean.Expr) + : Lean.DefinitionVal := + { name, levelParams, type, value, hints := .opaque, safety := .safe } + +partial def tryAddLeanDecl (defn: Lean.DefinitionVal) : CompileM Unit := do + match (<- get).env.constants.find? defn.name with + | some _ => pure () + | none => do + let env <- (·.env) <$> get + let maxHeartBeats <- (·.maxHeartBeats) <$> read + let decl := Lean.Declaration.defnDecl defn + match Lean.Environment.addDeclCore env maxHeartBeats decl .none with + | .ok e => do + modify fun stt => { stt with env := e } + return () + | .error e => do + let x <- (e.toMessageData .empty).format + throw $ .kernelException (x.pretty 80) + +partial def addDef (lvls: List Lean.Name) (typ val: Lean.Expr) + : CompileM (Address × Address) := do + let typ' <- compileExpr typ + let val' <- compileExpr val + let (a, m) <- hashConst $ Ix.Const.definition ⟨lvls.length, typ', val', true⟩ + tryAddLeanDecl (makeLeanDef a.toUniqueName lvls typ val) + return (a, m) + +partial def commitConst (anon meta: Address) + : CompileM (Address × Address) := do + let secret <- freshSecret + let comm := .comm ⟨secret, anon⟩ + let commAddr <- writeToStore comm + let commMeta := .comm ⟨secret, meta⟩ + let commMetaAddr <- writeToStore commMeta + modify fun stt => { stt with + comms := stt.comms.insert commAddr.toUniqueName (commAddr, commMetaAddr) + } + return (commAddr, commMetaAddr) + +partial def commitDef (lvls: List Lean.Name) (typ val: Lean.Expr) + : CompileM (Address × Address) := do + let (a, m) <- addDef lvls typ val + let (ca, cm) <- commitConst a m + tryAddLeanDecl (makeLeanDef ca.toUniqueName lvls typ val) + --tryAddLeanDecl (makeLeanDef ca.toUniqueName lvls typ (mkConst a.toUniqueName [])) + return (ca, cm) + +/-- +A name-irrelevant ordering of Lean expressions. +`weakOrd` contains the best known current mutual ordering +-/ +partial def compareExpr (weakOrd : RBMap Lean.Name Nat compare) + : Lean.Expr → Lean.Expr → CompileM Ordering + | e@(.mvar ..), _ => throw $ .unfilledExprMetavariable e + | _, e@(.mvar ..) => throw $ .unfilledExprMetavariable e + | e@(.fvar ..), _ => throw $ .freeVariableExpr e + | _, e@(.fvar ..) => throw $ .freeVariableExpr e + | .mdata _ x, .mdata _ y => compareExpr weakOrd x y + | .mdata _ x, y => compareExpr weakOrd x y + | x, .mdata _ y => compareExpr weakOrd x y + | .bvar x, .bvar y => return (compare x y) + | .bvar .., _ => return .lt + | _, .bvar .. => return .gt + | .sort x, .sort y => compareLevel x y + | .sort .., _ => return .lt + | _, .sort .. => return .gt + | .const x xls, .const y yls => do + let univs ← concatOrds <$> (xls.zip yls).mapM fun (x,y) => compareLevel x y + if univs != .eq then return univs + match weakOrd.find? x, weakOrd.find? y with + | some nx, some ny => return compare nx ny + | none, some _ => return .gt + | some _, none => return .lt + | none, none => + return compare + (← compileConst $ ← findLeanConst x) + (← compileConst $ ← findLeanConst y) + | .const .., _ => return .lt + | _, .const .. => return .gt + | .app xf xa, .app yf ya => + (· * ·) <$> compareExpr weakOrd xf yf <*> compareExpr weakOrd xa ya + | .app .., _ => return .lt + | _, .app .. => return .gt + | .lam _ xt xb _, .lam _ yt yb _ => + (· * ·) <$> compareExpr weakOrd xt yt <*> compareExpr weakOrd xb yb + | .lam .., _ => return .lt + | _, .lam .. => return .gt + | .forallE _ xt xb _, .forallE _ yt yb _ => + (· * ·) <$> compareExpr weakOrd xt yt <*> compareExpr weakOrd xb yb + | .forallE .., _ => return .lt + | _, .forallE .. => return .gt + | .letE _ xt xv xb _, .letE _ yt yv yb _ => + (· * · * ·) <$> compareExpr weakOrd xt yt <*> compareExpr weakOrd xv yv <*> compareExpr weakOrd xb yb + | .letE .., _ => return .lt + | _, .letE .. => return .gt + | .lit x, .lit y => + return if x < y then .lt else if x == y then .eq else .gt + | .lit .., _ => return .lt + | _, .lit .. => return .gt + | .proj _ nx tx, .proj _ ny ty => do + let ts ← compareExpr weakOrd tx ty + return concatOrds [compare nx ny, ts] + +/-- AST comparison of two Lean definitions. + `weakOrd` contains the best known current mutual ordering -/ +partial def compareDef + (weakOrd : RBMap Lean.Name Nat compare) + (x : Lean.DefinitionVal) + (y : Lean.DefinitionVal) + : CompileM Ordering := do + let ls := compare x.levelParams.length y.levelParams.length + let ts ← compareExpr weakOrd x.type y.type + let vs ← compareExpr weakOrd x.value y.value + return concatOrds [ls, ts, vs] + +/-- AST equality between two Lean definitions. + `weakOrd` contains the best known current mutual ordering -/ +@[inline] partial def eqDef + (weakOrd : RBMap Lean.Name Nat compare) + (x y : Lean.DefinitionVal) + : CompileM Bool := + return (← compareDef weakOrd x y) == .eq + +/-- +`sortDefs` recursively sorts a list of mutual definitions into weakly equal blocks. +At each stage, we take as input the current best approximation of known weakly equal +blocks as a List of blocks, hence the `List (List DefinitionVal)` as the argument type. +We recursively take the input blocks and resort to improve the approximate known +weakly equal blocks, obtaining a sequence of list of blocks: +``` +dss₀ := [startDefs] +dss₁ := sortDefs dss₀ +dss₂ := sortDefs dss₁ +dss₍ᵢ₊₁₎ := sortDefs dssᵢ ... +``` +Initially, `startDefs` is simply the list of definitions we receive from `DefinitionVal.all`; +since there is no order yet, we treat it as one block all weakly equal. On the other hand, +at the end, there is some point where `dss₍ᵢ₊₁₎ := dssᵢ`, then we have hit a fixed point +and we may end the sorting process. (We claim that such a fixed point exists, although +technically we don't really have a proof.) + +On each iteration, we hope to improve our knowledge of weakly equal blocks and use that +knowledge in the next iteration. e.g. We start with just one block with everything in it, +but the first sort may differentiate the one block into 3 blocks. Then in the second +iteration, we have more information than than first, since the relationship of the 3 blocks +gives us more information; this information may then be used to sort again, turning 3 blocks +into 4 blocks, and again 4 blocks into 6 blocks, etc, until we have hit a fixed point. +This step is done in the computation of `newDss` and then comparing it to the original `dss`. + +Two optimizations: + +1. `names := enum dss` records the ordering information in a map for faster access. + Directly using `List.findIdx?` on dss is slow and introduces `Option` everywhere. + `names` is used as a custom comparison in `ds.sortByM (cmpDef names)`. +2. `normDss/normNewDss`. We want to compare if two lists of blocks are equal. + Technically blocks are sets and their order doesn't matter, but we have encoded + them as lists. To fix this, we sort the list by name before comparing. Note we + could maybe also use `List (RBTree ..)` everywhere, but it seemed like a hassle. +-/ +partial def sortDefs (dss : List (List Lean.DefinitionVal)) : + CompileM (List (List Lean.DefinitionVal)) := do + let enum (ll : List (List Lean.DefinitionVal)) := + RBMap.ofList (ll.zipIdx.map fun (xs, n) => xs.map (·.name, n)).flatten + let weakOrd := enum dss _ + let newDss ← (← dss.mapM fun ds => + match ds with + | [] => unreachable! + | [d] => pure [[d]] + | ds => do pure $ (← List.groupByM (eqDef weakOrd) $ + ← ds.sortByM (compareDef weakOrd))).joinM + + -- must normalize, see comments + let normDss := dss.map fun ds => ds.map (·.name) |>.sort + let normNewDss := newDss.map fun ds => ds.map (·.name) |>.sort + if normDss == normNewDss then return newDss + else sortDefs newDss + +end + +partial def packLevel (lvls: Nat) (commit: Bool): CompileM Address := + match Ixon.natPackAsAddress lvls with + | some lvlsAddr => do + if commit then + let secret <- freshSecret + let comm := .comm (Ixon.Comm.mk secret lvlsAddr) + let commAddr <- writeToStore comm + modify fun stt => { stt with + comms := stt.comms.insert commAddr.toUniqueName (commAddr, commAddr) + } + return commAddr + else return lvlsAddr + | .none => throw .todo + +partial def checkClaim + (const: Lean.Name) + (type: Lean.Expr) + (sort: Lean.Expr) + (lvls: List Lean.Name) + (commit: Bool) + : CompileM (Claim × Address × Address) := do + let leanConst <- findLeanConst const + let (value, valMeta) <- compileConst leanConst >>= comm + let (type, typeMeta) <- addDef lvls sort type >>= comm + let lvls <- packLevel lvls.length commit + return (Claim.checks lvls type value, typeMeta, valMeta) + where + comm a := if commit then commitConst (Prod.fst a) (Prod.snd a) else pure a + +partial def evalClaim + (lvls: List Lean.Name) + (input: Lean.Expr) + (output: Lean.Expr) + (type: Lean.Expr) + (sort: Lean.Expr) + (commit: Bool) + : CompileM (Claim × Address × Address × Address) := do + let (input, inputMeta) <- addDef lvls type input >>= comm + let (output, outputMeta) <- addDef lvls type output >>= comm + let (type, typeMeta) <- addDef lvls sort type >>= comm + let lvlsAddr <- packLevel lvls.length commit + return (Claim.evals lvlsAddr input output type, inputMeta, outputMeta, typeMeta) + where + comm a := if commit then commitConst (Prod.fst a) (Prod.snd a) else pure a + +def compileConstIO (env : Lean.Environment ) (const: Lean.ConstantInfo) + : IO $ (Address × Address) × CompileState := do + let (a, s) <- (compileConst const).runIO 200000 (.init env) + let a <- IO.ofExcept a + return (a, s) + +def compileDelta (delta : Lean.PersistentHashMap Lean.Name Lean.ConstantInfo) + : CompileM Unit := do + delta.forM fun _ c => if !c.isUnsafe then discard $ compileConst c else pure () + +/-- +Content-addresses the "delta" of an environment, that is, the content that is +added on top of the imports. + +Important: constants with open references in their expressions are filtered out. +Open references are variables that point to names which aren't present in the +`Lean.ConstMap`. +-/ +def compileDeltaIO + (env: Lean.Environment) + (delta : Lean.PersistentHashMap Lean.Name Lean.ConstantInfo) + : IO CompileState := do + let (res, stt) <- (compileDelta delta).runIO 200000 (.init env) + IO.ofExcept res + return stt + +def compileEnvIO (env: Lean.Environment) : IO CompileState := do + compileDeltaIO env env.getDelta + diff --git a/Ix/Cronos.lean b/Ix/Cronos.lean new file mode 100644 index 00000000..a5dd7c27 --- /dev/null +++ b/Ix/Cronos.lean @@ -0,0 +1,28 @@ +import Batteries + +open Batteries (RBMap) + +structure Cronos where + refs : RBMap String Nat compare + data : RBMap String Nat compare + deriving Inhabited + +namespace Cronos + +def new : Cronos := + default + +def clock (c: Cronos) (tag : String) : IO Cronos := do + let now ← IO.monoNanosNow + match c.refs.find? tag with + | none => return { c with refs := c.refs.insert tag now } + | some ref => return { + refs := c.refs.insert tag now, + data := c.data.insert tag (now - ref) } + +def summary (c: Cronos) : String := + let timings := c.data.foldl (init := "") + fun acc tag time => s!"{acc}\n {tag} | {(Float.ofNat time) / 1000000000}s" + s!"Timings:{timings}" + +end Cronos diff --git a/Ix/Ixon/Const.lean b/Ix/Ixon/Const.lean index cf9a85ff..962f7ef3 100644 --- a/Ix/Ixon/Const.lean +++ b/Ix/Ixon/Const.lean @@ -1,4 +1,5 @@ import Ix.Address +import Ix.Prove import Lean.Declaration import Ix.Ixon.Serialize import Ix.Ixon.Metadata @@ -100,6 +101,11 @@ structure DefinitionProj where idx : Nat deriving BEq, Repr +structure Comm where + secret: Address + payload: Address + deriving BEq, Repr + inductive Const where -- 0xC0 | axio : Axiom -> Const @@ -112,48 +118,40 @@ inductive Const where -- 0xC4 | quot : Quotient -> Const -- 0xC5 - --| ctor : Constructor -> Const - ---- 0xC6 - --| recr : Recursor -> Const - ---- 0xC7 - --| indc : Inductive -> Const - -- 0xC8 | ctorProj : ConstructorProj -> Const - -- 0xC9 + -- 0xC6 | recrProj : RecursorProj -> Const - -- 0xCA + -- 0xC7 | indcProj : InductiveProj -> Const - -- 0xCB + -- 0xC8 | defnProj : DefinitionProj -> Const - -- 0xCC + -- 0xC9 | mutDef : List Definition -> Const - -- 0xCD + -- 0xCA | mutInd : List Inductive -> Const - -- 0xCE + -- 0xCB | meta : Metadata -> Const + -- 0xCC + | proof : Proof -> Const + -- 0xCD + | comm: Comm -> Const deriving BEq, Repr, Inhabited -def putDefn (x: Definition) : PutM := - putUInt8 0xC3 *> - - putNatl x.lvls *> putExpr x.type *> putExpr x.value *> putBool x.part - def putConst : Const → PutM | .axio x => putUInt8 0xC0 *> putNatl x.lvls *> putExpr x.type | .theo x => putUInt8 0xC1 *> putNatl x.lvls *> putExpr x.type *> putExpr x.value | .opaq x => putUInt8 0xC2 *> putNatl x.lvls *> putExpr x.type *> putExpr x.value | .defn x => putUInt8 0xC3 *> putDefn x | .quot x => putUInt8 0xC4 *> putNatl x.lvls *> putExpr x.type *> putQuotKind x.kind ---| .ctor x => putUInt8 0xC5 *> putCtor x ---| .recr x => putUInt8 0xC6 *> putRecr x ---| .indc x => putUInt8 0xC7 *> putIndc x -| .ctorProj x => putUInt8 0xC8 *> putBytes x.block.hash *> putNatl x.idx *> putNatl x.cidx -| .recrProj x => putUInt8 0xC9 *> putBytes x.block.hash *> putNatl x.idx *> putNatl x.ridx -| .indcProj x => putUInt8 0xCA *> putBytes x.block.hash *> putNatl x.idx -| .defnProj x => putUInt8 0xCB *> putBytes x.block.hash *> putNatl x.idx -| .mutDef xs => putUInt8 0xCC *> putArray (putDefn <$> xs) -| .mutInd xs => putUInt8 0xCD *> putArray (putIndc <$> xs) -| .meta m => putUInt8 0xCE *> putMetadata m +| .ctorProj x => putUInt8 0xC5 *> putBytes x.block.hash *> putNatl x.idx *> putNatl x.cidx +| .recrProj x => putUInt8 0xC6 *> putBytes x.block.hash *> putNatl x.idx *> putNatl x.ridx +| .indcProj x => putUInt8 0xC7 *> putBytes x.block.hash *> putNatl x.idx +| .defnProj x => putUInt8 0xC8 *> putBytes x.block.hash *> putNatl x.idx +| .mutDef xs => putUInt8 0xC9 *> putArray (putDefn <$> xs) +| .mutInd xs => putUInt8 0xCA *> putArray (putIndc <$> xs) +| .meta m => putUInt8 0xCB *> putMetadata m +| .proof p => putUInt8 0xCC *> putProof p +| .comm c => putUInt8 0xCD *> putComm c where putDefn (x: Definition) := putNatl x.lvls *> putExpr x.type *> putExpr x.value *> putBool x.part @@ -171,8 +169,23 @@ def putConst : Const → PutM *> putNatl x.params *> putNatl x.indices *> putArray (putCtor <$> x.ctors) *> putArray (putRecr <$> x.recrs) *> putBools [x.recr, x.refl, x.struct, x.unit] - -def getDefn : GetM Definition := .mk <$> getNatl <*> getExpr <*> getExpr <*> getBool + putProof (p: Proof) : PutM := + match p.claim with + | .checks lvls type value => + putUInt8 0 + *> putBytes lvls.hash + *> putBytes type.hash + *> putBytes value.hash + *> putByteArray p.bin + | .evals lvls inp out type => + putUInt8 1 + *> putBytes lvls.hash + *> putBytes inp.hash + *> putBytes out.hash + *> putBytes type.hash + *> putByteArray p.bin + putComm (c: Comm) : PutM := + putBytes c.secret.hash *> putBytes c.payload.hash def getConst : GetM Const := do let tag ← getUInt8 @@ -182,20 +195,23 @@ def getConst : GetM Const := do | 0xC2 => .opaq <$> (.mk <$> getNatl <*> getExpr <*> getExpr) | 0xC3 => .defn <$> getDefn | 0xC4 => .quot <$> (.mk <$> getNatl <*> getExpr <*> getQuotKind) - -- | 0xC5 => .ctor <$> getCtor - -- | 0xC6 => .recr <$> getRecr - -- | 0xC7 => .indc <$> getIndc - | 0xC8 => .ctorProj <$> (.mk <$> (.mk <$> getBytes 32) <*> getNatl <*> getNatl) - | 0xC9 => .recrProj <$> (.mk <$> (.mk <$> getBytes 32) <*> getNatl <*> getNatl) - | 0xCA => .indcProj <$> (.mk <$> (.mk <$> getBytes 32) <*> getNatl) - | 0xCB => .defnProj <$> (.mk <$> (.mk <$> getBytes 32) <*> getNatl) - | 0xCC => .mutDef <$> getArray getDefn - | 0xCD => .mutInd <$> getArray getIndc - | 0xCE => .meta <$> getMetadata + | 0xC5 => .ctorProj <$> (.mk <$> getAddr <*> getNatl <*> getNatl) + | 0xC6 => .recrProj <$> (.mk <$> getAddr <*> getNatl <*> getNatl) + | 0xC7 => .indcProj <$> (.mk <$> getAddr <*> getNatl) + | 0xC8 => .defnProj <$> (.mk <$> getAddr <*> getNatl) + | 0xC9 => .mutDef <$> getArray getDefn + | 0xCA => .mutInd <$> getArray getIndc + | 0xCB => .meta <$> getMetadata + | 0xCC => .proof <$> getProof + | 0xCD => .comm <$> getComm | e => throw s!"expected Const tag, got {e}" where - getCtor := .mk <$> getNatl <*> getExpr <*> getNatl <*> getNatl <*> getNatl - getRecrRule := RecursorRule.mk <$> getNatl <*> getExpr + getDefn : GetM Definition := + .mk <$> getNatl <*> getExpr <*> getExpr <*> getBool + getCtor : GetM Constructor := + .mk <$> getNatl <*> getExpr <*> getNatl <*> getNatl <*> getNatl + getRecrRule : GetM RecursorRule := + RecursorRule.mk <$> getNatl <*> getExpr getRecr : GetM Recursor := do let f ← Recursor.mk <$> getNatl <*> getExpr <*> getNatl <*> getNatl <*> getNatl <*> getNatl <*> getArray getRecrRule @@ -208,6 +224,14 @@ def getConst : GetM Const := do match ← getBools 4 with | [w, x, y, z] => return f w x y z | _ => throw s!"unreachable" + getAddr : GetM Address := .mk <$> getBytes 32 + getProof : GetM Proof := do + match (<- getUInt8) with + | 0 => .mk <$> (.checks <$> getAddr <*> getAddr <*> getAddr) <*> getByteArray + | 1 => .mk <$> (.evals <$> getAddr <*> getAddr <*> getAddr <*> getAddr) <*> getByteArray + | e => throw s!"expect proof variant tag, got {e}" + getComm : GetM Comm := + .mk <$> getAddr <*> getAddr instance : Serialize Const where put := runPut ∘ putConst diff --git a/Ix/Ixon/Expr.lean b/Ix/Ixon/Expr.lean index cfb93c11..8db1c7e8 100644 --- a/Ix/Ixon/Expr.lean +++ b/Ix/Ixon/Expr.lean @@ -32,6 +32,7 @@ inductive Expr where -- array: 0xB -- const: 0xC + def putExprTag (tag: UInt8) (val: UInt64) : PutM := let t := UInt8.shiftLeft tag 4 if val < 8 @@ -136,6 +137,10 @@ def putArray (xs : List PutM) := do putExprTag 0xB (UInt64.ofNat xs.length) List.forM xs id +def putByteArray (x: ByteArray) := do + putExprTag 0xB (UInt64.ofNat x.size) + x.toList.forM putUInt8 + def getArray (getM: GetM A) : GetM (List A) := do let tagByte ← getUInt8 let tag := UInt8.shiftRight tagByte 4 @@ -147,6 +152,10 @@ def getArray (getM: GetM A) : GetM (List A) := do List.mapM (λ _ => getM) (List.range len) | e => throw s!"expected Array with tag 0xB, got {e}" +def getByteArray : GetM ByteArray := do + let xs <- getArray getUInt8 + return ⟨xs.toArray⟩ + def putOption (putM: A -> PutM): Option A → PutM | .none => putArray [] diff --git a/Ix/Ixon/Serialize.lean b/Ix/Ixon/Serialize.lean index 88215b5e..13acf07e 100644 --- a/Ix/Ixon/Serialize.lean +++ b/Ix/Ixon/Serialize.lean @@ -1,4 +1,5 @@ import Lean.Declaration +import Ix.Address namespace Ixon @@ -88,6 +89,14 @@ def natToBytesLE (x: Nat) : Array UInt8 := def natFromBytesLE (xs: Array UInt8) : Nat := (xs.toList.zipIdx 0).foldl (fun acc (b, i) => acc + (UInt8.toNat b) * 256 ^ i) 0 +def natPackAsAddress (x: Nat) : Option Address := + let bytes := natToBytesLE x + if bytes.size > 32 then .none + else .some (Address.mk ⟨bytes.append (mkArray (32 - bytes.size) 0)⟩) + +def natUnpackFromAddress (x: Address) : Nat := + natFromBytesLE x.hash.data + def fromTrimmedLE (xs: Array UInt8) : UInt64 := List.foldr step 0 xs.toList where step byte acc := UInt64.shiftLeft acc 8 + (UInt8.toUInt64 byte) diff --git a/Ix/Meta.lean b/Ix/Meta.lean index ce7f4a78..d439e56f 100644 --- a/Ix/Meta.lean +++ b/Ix/Meta.lean @@ -1,11 +1,9 @@ import Lean import Ix.Address +import Ix.CompileM open Lean -def computeIxAddress (_const : ConstantInfo) (_constMap: ConstMap) : Address := - default -- TODO - open System (FilePath) open Elab in @@ -40,21 +38,33 @@ elab "this_file!" : term => do macro "get_env!" : term => `(getFileEnv this_file!) -def mkAnonDefInfoRaw (type : Expr) (value : Expr) : ConstantInfo := - .defnInfo { - name := .anonymous - levelParams := [] - type - value - hints := .opaque - safety := .safe - } - -def mkAnonDefInfo [inst : ToExpr α] (a : α) : ConstantInfo := - mkAnonDefInfoRaw inst.toTypeExpr (toExpr a) +def computeIxAddress (env: Lean.Environment) (const : ConstantInfo) : IO Address := do + let ((a, _), _) <- Ix.Compile.compileConstIO env const + return a def runCore (f : CoreM α) (env : Environment) : IO α := Prod.fst <$> f.toIO { fileName := default, fileMap := default } { env } def runMeta (f : MetaM α) (env : Environment) : IO α := Prod.fst <$> f.toIO { fileName := default, fileMap := default } { env } + +def metaMakeList (α: Lean.Expr) (names: List Lean.Name) : MetaM Expr := do + let nil <- Meta.mkAppOptM ``List.nil #[.some α] + names.foldrM (fun n t => Meta.mkAppOptM ``List.cons #[.some α, mkConst n, t]) nil + +def metaMakeDef [Lean.ToExpr α] (a: α) : MetaM (List Lean.Name × Lean.Expr × Lean.Expr) := do + let val := Lean.toExpr a + let typ <- Meta.inferType val + let lvls := (Lean.collectLevelParams default typ).params.toList + return (lvls, typ, val) + +def metaMakeEvalClaim (func: Lean.Name) (args : List Lean.Expr) + : MetaM (List Lean.Name × Lean.Expr × Lean.Expr × Lean.Expr × Lean.Expr) := do + let input <- Meta.mkAppM func args.toArray + let output <- Meta.reduce input + let type <- Meta.inferType output + let sort <- Meta.inferType type + let lvls := (Lean.collectLevelParams default input).params.toList + return (lvls, input, output, type, sort) + + diff --git a/Ix/Prove.lean b/Ix/Prove.lean index 72ef3a8c..423d1d95 100644 --- a/Ix/Prove.lean +++ b/Ix/Prove.lean @@ -1,29 +1,27 @@ import Ix.Address import Ix.Ixon.Serialize +import Ix.Claim +import Ix.Common -inductive ProveError - | todo +--inductive ProveError +-- | todo +-- +--instance : ToString ProveError := ⟨fun _ => "TODO"⟩ +-- +--abbrev ProveM := ExceptT ProveError IO -instance : ToString ProveError := ⟨fun _ => "TODO"⟩ - -abbrev ProveM := ExceptT ProveError IO structure Proof where - inp : Address - out : Address - typ : Address + claim: Claim /-- Bytes of the Binius proof -/ bin : ByteArray - deriving Inhabited + deriving Inhabited, BEq -instance : Ixon.Serialize Proof where - put proof := proof.inp.hash ++ proof.out.hash ++ proof.typ.hash ++ proof.bin - get bytes := - let inpBytes := bytes.extract 0 32 - let outBytes := bytes.extract 32 64 - let typBytes := bytes.extract 64 96 - let binBytes := bytes.extract 96 bytes.size - .ok ⟨⟨inpBytes⟩, ⟨outBytes⟩, ⟨typBytes⟩, binBytes⟩ +instance : ToString Proof where + toString p := s!"<{toString p.claim} := {hexOfBytes p.bin}>" -def prove (_hash : Address) : ProveM Proof := - default -- TODO +instance : Repr Proof where + reprPrec p _ := toString p +-- +--def prove (claim : Claim) : ProveM Proof := +-- default -- TODO diff --git a/Ix/Store.lean b/Ix/Store.lean index 60b70302..9f5da80c 100644 --- a/Ix/Store.lean +++ b/Ix/Store.lean @@ -1,7 +1,3 @@ - --- --- ix/store/f942e5170f2493c9bd65471871d0d0ce89097c08c42b73a108515eab1ff4dc48 - import Ix.Address import Ix.Ixon import Ix.Ixon.Serialize @@ -24,9 +20,13 @@ def storeErrorToIOError : StoreError -> IO.Error | .ixonError e => IO.Error.userError s!"ixon error {e}" | .noHome => IO.Error.userError s!"no HOME environment variable" - abbrev StoreIO := EIO StoreError +def StoreIO.toIO (sio: StoreIO α) : IO α := + EIO.toIO storeErrorToIOError sio + +namespace Store + def getHomeDir : StoreIO FilePath := do match ← IO.getEnv "HOME" with | .some path => return ⟨path⟩ @@ -40,19 +40,20 @@ def ensureStoreDir : StoreIO Unit := do let store ← storeDir IO.toEIO .ioError (IO.FS.createDirAll store) -def writeConst (x: Ixon.Const) : StoreIO Unit := do +def writeConst (x: Ixon.Const) : StoreIO Address := do let bytes := Ixon.Serialize.put x let addr := Address.blake3 bytes let store ← storeDir - let path := store / byteArrayToHex addr.hash - IO.toEIO .ioError (IO.FS.writeBinFile path bytes) + let path := store / hexOfBytes addr.hash + let _ <- IO.toEIO .ioError (IO.FS.writeBinFile path bytes) + return addr def readConst (a: Address) : StoreIO Ixon.Const := do let store ← storeDir - let path := store / byteArrayToHex a.hash + let path := store / hexOfBytes a.hash let bytes ← IO.toEIO .ioError (IO.FS.readBinFile path) match Ixon.Serialize.get bytes with | .ok c => return c | .error e => throw (.ixonError e) - +end Store diff --git a/Ix/TransportM.lean b/Ix/TransportM.lean index ab2ecc16..aebcf6c1 100644 --- a/Ix/TransportM.lean +++ b/Ix/TransportM.lean @@ -8,6 +8,7 @@ import Ix.Common import Ix.Address import Ix.Ixon.Metadata import Ix.Ixon.Serialize +import Ix.Prove import Batteries.Data.RBMap namespace Ix.TransportM @@ -25,7 +26,17 @@ inductive TransportError | unknownIndex (idx: Nat) (m: Ixon.Metadata) | unexpectedNode (idx: Nat) (m: Ixon.Metadata) | rawMetadata (m: Ixon.Metadata) - deriving Repr + | rawProof (m: Proof) + | rawComm (m: Ixon.Comm) + deriving BEq, Repr + +instance : ToString TransportError where toString +| .natTooBig idx x => s!"At index {idx}, natural number {x} too big to fit in UInt64" +| .unknownIndex idx x => s!"Unknown index {idx} with metadata {repr x}" +| .unexpectedNode idx x => s!"Unexpected node at {idx} with metadata {repr x}" +| .rawMetadata x => s!"Can't rematerialize raw metadata {repr x}" +| .rawProof x => s!"Can't rematerialize raw proof {repr x}" +| .rawComm x => s!"Can't rematerialize raw commitment {repr x}" abbrev DematM := EStateM TransportError DematState @@ -279,6 +290,9 @@ partial def rematConst : Ixon.Const -> RematM Ix.Const | .mutDef xs => .mutDefBlock <$> (xs.mapM rematDefn) | .mutInd xs => .mutIndBlock <$> (xs.mapM rematInd) | .meta m => throw (.rawMetadata m) +-- TODO: This could return a Proof inductive, since proofs have no metadata +| .proof p => throw (.rawProof p) +| .comm p => throw (.rawComm p) where rematDefn : Ixon.Definition -> RematM Ix.Definition | x => .mk x.lvls <$> rematExpr x.type <*> rematExpr x.value <*> pure x.part diff --git a/Main.lean b/Main.lean index 7946e954..2288ac76 100644 --- a/Main.lean +++ b/Main.lean @@ -1,6 +1,5 @@ import Ix.Cli.ProveCmd -import Ix.Cli.HashCmd -import Ix.Cli.TestCmd +import Ix.Cli.StoreCmd import Ix.Cli.SendCmd import Ix.Cli.RecvCmd import Ix @@ -14,8 +13,7 @@ def ixCmd : Cli.Cmd := `[Cli| SUBCOMMANDS: proveCmd; - hashCmd; - testCmd; + storeCmd; sendCmd; recvCmd ] diff --git a/Tests/Ix/Canon.lean b/Tests/Ix/Canon.lean new file mode 100644 index 00000000..28a4d3df --- /dev/null +++ b/Tests/Ix/Canon.lean @@ -0,0 +1,107 @@ +import LSpec + +import Ix.Ixon +import Ix.Address +import Ix.Common +import Ix.CanonM +import Ix.Meta +import Lean +import Tests.Ix.Fixtures + +@[specialize] +def withExceptOkM + [Monad m] (descr : String) (exc : Except ε α) [ToString ε] (f : α → m LSpec.TestSeq) + : m LSpec.TestSeq := + match exc with + | .error e => return LSpec.test descr (LSpec.ExpectationFailure "ok _" s!"error {e}") + | .ok a => return LSpec.test descr true $ ← f a + +--abbrev CanonTest := Ix.CanonM.CanonMState → LSpec.TestSeq +--abbrev IOCanonTest := Ix.CanonM.CanonMState → IO LSpec.TestSeq + + +def Test.Ix.Canon.wellfounded : IO LSpec.TestSeq := do + let env <- get_env! + let stt <- match <- Ix.CanonM.canonicalizeDelta env.constants env.getDelta with + | .error e => return LSpec.test "canonicalizeFailure" (LSpec.ExpectationFailure "ok _" s!"error {e}") + | .ok stt => pure stt + let (a,_) := stt.names.find! `WellFounded.A + let (b,_) := stt.names.find! `WellFounded.A' + return LSpec.test "A == A'" (a == b) + +-- `WellFounded.A == `WellFounded.A' + +--def Tests.Ix.Canon.suite : List LSpec.TestSeq := +-- [ +-- +-- ] + +--/-- Run tests from extractors given a Lean source file -/ +--def canonTestsFromFile (source : FilePath) +-- (canon : List Extractor) (ioExtractors : List IOExtractor) +-- (setPaths quick : Bool := true) : IO TestSeq := do +-- if setPaths then Lean.setLibsPaths +-- let leanEnv ← Lean.runFrontend (← IO.FS.readFile source) source +-- let (constMap, delta) := leanEnv.getConstsAndDelta +-- withExceptOkM s!"Content-addresses {source}" +-- (← contAddr constMap delta quick false) fun stt => do +-- let pureTests := extractors.foldl (init := .done) +-- fun acc ext => acc ++ (ext stt) +-- ioExtractors.foldlM (init := pureTests) fun acc ext => +-- do pure $ acc ++ (← ext stt) + +--/-- Calls `ensembleTestExtractors` for multiple sources -/ +--def ensembleTestExtractors' (sources : List FilePath) +-- (extractors : List Extractor) (ioExtractors : List IOExtractor) +-- (setPaths : Bool := true) : IO TestSeq := +-- sources.foldlM (init := .done) fun acc source => do +-- let g := group s!"Tests for {source}" $ +-- ← ensembleTestExtractors source extractors ioExtractors setPaths +-- pure $ acc ++ g +-- +--/-- Asserts that all constants typechecks -/ +--def extractTypecheckingTests : Extractor := fun stt => +-- withExceptOk "Typechecking succeeds" (typecheckAll stt.store stt.env.constNames) +-- fun _ => .done +-- +--/-- Asserts that some constant doesn't typecheck -/ +--def extractNonTypecheckingTests : Extractor := fun stt => +-- withExceptError "Typechecking fails" (typecheckAll stt.store stt.env.constNames) +-- fun _ => .done +-- +--section AnonHashGroups +-- +--/- +--This section defines an extractor that consumes a list of groups of names and +--creates tests that assert that: +--1. Each pair of constants in the same group has the same anon hash +--2. Each pair of constants in different groups has different anon hashes +---/ +-- +--def extractAnonGroups (groups : List (List Name)) (stt : ContAddrState) : +-- Except String (Array (Array $ Name × Lurk.F)) := Id.run do +-- let mut notFound : Array Name := #[] +-- let mut hashGroups : Array (Array $ Name × Lurk.F) := #[] +-- for group in groups do +-- let mut hashGroup : Array (Name × Lurk.F) := #[] +-- for name in group do +-- match stt.env.consts.find? name with +-- | none => notFound := notFound.push name +-- | some h => hashGroup := hashGroup.push (name, h) +-- hashGroups := hashGroups.push hashGroup +-- if notFound.isEmpty then +-- return .ok hashGroups +-- else +-- return .error s!"Not found: {", ".intercalate $ notFound.data.map toString}" +-- +--def extractAnonGroupsTests (groups : List $ List Name) : Extractor := fun stt => +-- withExceptOk "All constants can be found" (extractAnonGroups groups stt) +-- fun anonGroups => +-- let anonEqTests := anonGroups.foldl (init := .done) fun tSeq anonGroup => +-- anonGroup.data.pairwise.foldl (init := tSeq) fun tSeq (x, y) => +-- tSeq ++ test s!"{x.1}ₐₙₒₙ = {y.1}ₐₙₒₙ" (x.2 == y.2) +-- anonGroups.data.pairwise.foldl (init := anonEqTests) fun tSeq (g, g') => +-- (g.data.cartesian g'.data).foldl (init := tSeq) fun tSeq (x, y) => +-- tSeq ++ test s!"{x.1}ₐₙₒₙ ≠ {y.1}ₐₙₒₙ" (x.2 != y.2) +-- +--end AnonHashGroups diff --git a/Tests/Ix/Compile.lean b/Tests/Ix/Compile.lean new file mode 100644 index 00000000..39f2f995 --- /dev/null +++ b/Tests/Ix/Compile.lean @@ -0,0 +1,46 @@ +import LSpec + +import Ix.Ixon +import Ix.Address +import Ix.Common +import Ix.CompileM +import Ix.Meta +import Lean +import Tests.Ix.Fixtures +import Lean + +open LSpec +open Ix.Compile + +--def testCompileExpr (env: Lean.Environment) +-- (msg: String) (commit: Bool) (input: Lean.Expr) (expected: Ix.Expr) +-- : IO TestSeq := do +-- let (out, _) <- +-- CompileM.runIO' env (compileExpr commit input) +-- return test msg (out == expected) +-- +--def threeIO : IO TestSeq := do +-- return test "one isn't two" (1 == 2) +-- +--def foo : IO Lean.Expr := do +-- runMeta (Lean.Meta.whnf (Lean.toExpr 3)) (<- get_env!) +-- +--def bar : IO Ix.Expr := do +-- let env <- get_env! +-- let .defnInfo defn ← runCore (Lean.getConstInfo ``id) env +-- | unreachable! +-- let input <- runMeta (Lean.Meta.whnf defn.value) env +-- --let (out, _) <- CompileM.runIO' env (compileExpr false input) +-- return out + +--#eval bar + +def test1 : IO TestSeq := do + let env <- get_env! + let input <- runMeta (Lean.Meta.whnf (Lean.toExpr 3)) env + let expected := Lean.Expr.lit (Lean.Literal.natVal 3) + return test "expected 3" (input == expected) + +def Tests.Ix.Compile.suiteIO: List (IO TestSeq) := [ + test1 +] diff --git a/Tests/Ix/Fixtures.lean b/Tests/Ix/Fixtures.lean new file mode 100644 index 00000000..721a93ef --- /dev/null +++ b/Tests/Ix/Fixtures.lean @@ -0,0 +1,176 @@ +import Tests.Ix.Fixtures.Export + +set_option linter.all false -- prevent error messages from runFrontend +namespace WellFounded + +mutual + + def A : Nat → Nat + | 0 => 0 + | n + 1 => B n + E n + C n + 1 + + def C : Nat → Nat + | 0 => 0 + | n + 1 => B n + F n + A n + 1 + + def E : Nat → Nat + | 0 => 0 + | n + 1 => B n + A n + F n + 1 + + def F : Nat → Nat + | 0 => 0 + | n + 1 => B n + C n + E n + 1 + + def B : Nat → Nat + | 0 => 0 + | n + 1 => C n + 2 + + def G : Nat → Nat + | 0 => 0 + | n + 1 => B n + F n + H n + 2 + + def H : Nat → Nat + | 0 => 0 + | n + 1 => B n + E n + G n + 2 + +end + +mutual + + def A' : Nat → Nat + | 0 => 0 + | n + 1 => B' n + E' n + C' n + 1 + + def C' : Nat → Nat + | 0 => 0 + | n + 1 => B' n + F' n + A' n + 1 + + def E' : Nat → Nat + | 0 => 0 + | n + 1 => B' n + A' n + F' n + 1 + + def F' : Nat → Nat + | 0 => 0 + | n + 1 => B' n + C' n + E' n + 1 + + def B' : Nat → Nat + | 0 => 0 + | n + 1 => C' n + 2 + + def G' : Nat → Nat + | 0 => 0 + | n + 1 => B' n + F' n + H' n + 2 + + def H' : Nat → Nat + | 0 => 0 + | n + 1 => B' n + E' n + G' n + 2 + +end + +mutual + def I : Nat → Nat + | 0 => 0 + | n + 1 => B n + E n + G n + 2 +end + +def I' : Nat → Nat + | 0 => 0 + | n + 1 => B n + E n + G n + 2 + +end WellFounded + +namespace Partial + +mutual + + partial def A : Nat → Nat + | 0 => 0 + | n + 1 => B n + E n + C n + 1 + + partial def C : Nat → Nat + | 0 => 0 + | n + 1 => B n + F n + A n + 1 + + partial def E : Nat → Nat + | 0 => 0 + | n + 1 => B n + A n + F n + 1 + + partial def F : Nat → Nat + | 0 => 0 + | n + 1 => B n + C n + E n + 1 + + partial def B : Nat → Nat + | 0 => 0 + | n + 1 => C n + 2 + + partial def G : Nat → Nat + | 0 => 0 + | n + 1 => B n + F n + H n + 2 + + partial def H : Nat → Nat + | 0 => 0 + | n + 1 => B n + E n + G n + 2 + +end + +partial def I : Nat → Nat + | 0 => 0 + | n + 1 => B n + E n + G n + 2 + +end Partial + + +namespace Inductives + +inductive BLA + | nil + | bla : BLA → BLA → BLA + +-- an inductive with a differently named constructor but all else equal should be the same +inductive BLU + | nil + | blu : BLU → BLU → BLU + +-- an inductive with a different constructor order should be distinct +inductive BLA' + | bla : BLA' → BLA' → BLA' + | nil + +mutual + -- BLE and BLI should be distinct because we don't group by weak equality + inductive BLE | bli : BLI → BLE + inductive BLI | ble : BLE → BLI + inductive BLO | blea : BLE → BLI → BLO +end + +mutual + inductive BLE' | bli : BLI' → BLE' + inductive BLI' | ble : BLE' → BLI' + inductive BLO' | blea : BLE' → BLI' → BLO' +end + +mutual + -- BLE and BLI should be distinct because we don't group by weak equality + inductive BLE'' | bli : BLI'' → BLE'' + inductive BLO'' | blea : BLE'' → BLA' → BLO'' + inductive BLI'' | ble : BLE'' → BLI'' +end + +-- testing external reference into mutual +inductive BLEH + | bleh : BLE → BLEH + | bloh : BLO → BLEH + +end Inductives + +namespace Import + + +def Foo := MyNat -- triggering the compilation of `MyNat` +def Bar := Nat -- triggering the compilation of `Nat` + +inductive MyOtherNat + | nada + | mais : MyOtherNat → MyOtherNat + +end Import diff --git a/Tests/Ix/Fixtures/Export.lean b/Tests/Ix/Fixtures/Export.lean new file mode 100644 index 00000000..bc637a05 --- /dev/null +++ b/Tests/Ix/Fixtures/Export.lean @@ -0,0 +1,3 @@ +inductive MyNat + | nill + | next : MyNat → MyNat diff --git a/Tests/Ix/Fixtures/Inductives.lean b/Tests/Ix/Fixtures/Inductives.lean new file mode 100644 index 00000000..e69de29b diff --git a/Tests/Main.lean b/Tests/Main.lean index afadfaa3..96c5a46f 100644 --- a/Tests/Main.lean +++ b/Tests/Main.lean @@ -4,16 +4,21 @@ import Tests.Boundary import Tests.ByteArray import Tests.Unsigned import Tests.Ix +import Tests.Ix.Compile import Tests.Keccak -def main := LSpec.lspecIO (.ofList [ - ("arith-expr", Tests.ArithExpr.suite), - ("boundary", Tests.Boundary.suite), - ("binius-bindings", Tests.Binius.bindingsSuite), - ("binius-witness", Tests.Binius.witnessSuite), - ("binius-transparent", Tests.Binius.transparentSuite), - ("byte-array", Tests.ByteArray.suite), - ("unsigned", Tests.Unsigned.suite), - ("ix", Tests.Ix.suite), - ("keccak", Tests.Keccak.suite), - ]) +def main (args: List String) : IO UInt32 := do + if args.contains "compile" + then LSpec.lspecEachIO Tests.Ix.Compile.suiteIO id + else + LSpec.lspecIO (.ofList [ + ("arith-expr", Tests.ArithExpr.suite), + ("boundary", Tests.Boundary.suite), + ("binius-bindings", Tests.Binius.bindingsSuite), + ("binius-witness", Tests.Binius.witnessSuite), + ("binius-transparent", Tests.Binius.transparentSuite), + ("byte-array", Tests.ByteArray.suite), + ("unsigned", Tests.Unsigned.suite), + ("ix", Tests.Ix.suite), + ("keccak", Tests.Keccak.suite), + ]) args diff --git a/ix_test/.github/workflows/lean_action_ci.yml b/ix_test/.github/workflows/lean_action_ci.yml new file mode 100644 index 00000000..09cd4ca6 --- /dev/null +++ b/ix_test/.github/workflows/lean_action_ci.yml @@ -0,0 +1,14 @@ +name: Lean Action CI + +on: + push: + pull_request: + workflow_dispatch: + +jobs: + build: + runs-on: ubuntu-latest + + steps: + - uses: actions/checkout@v4 + - uses: leanprover/lean-action@v1 diff --git a/ix_test/.gitignore b/ix_test/.gitignore new file mode 100644 index 00000000..bfb30ec8 --- /dev/null +++ b/ix_test/.gitignore @@ -0,0 +1 @@ +/.lake diff --git a/ix_test/IxTest.lean b/ix_test/IxTest.lean new file mode 100644 index 00000000..795208bd --- /dev/null +++ b/ix_test/IxTest.lean @@ -0,0 +1,10 @@ +-- This module serves as the root of the `IxTest` library. +-- Import modules here that should be built as part of the library. +import IxTest.Basic +import Init +import Std + +def id' (A: Type) (x: A) := x +--def ref (A: Type) (x y: A) := hello + +def one : Nat := 1 diff --git a/ix_test/IxTest/Basic.lean b/ix_test/IxTest/Basic.lean new file mode 100644 index 00000000..1d48bfba --- /dev/null +++ b/ix_test/IxTest/Basic.lean @@ -0,0 +1 @@ +def hello (A: Type) (x y : A) : A := x diff --git a/ix_test/Main.lean b/ix_test/Main.lean new file mode 100644 index 00000000..1c8c23e9 --- /dev/null +++ b/ix_test/Main.lean @@ -0,0 +1,4 @@ +import IxTest + +def main : IO Unit := + IO.println s!"Hello, world!" diff --git a/ix_test/README.md b/ix_test/README.md new file mode 100644 index 00000000..afd8772b --- /dev/null +++ b/ix_test/README.md @@ -0,0 +1 @@ +# ix_test \ No newline at end of file diff --git a/ix_test/lake-manifest.json b/ix_test/lake-manifest.json new file mode 100644 index 00000000..9a82a6ac --- /dev/null +++ b/ix_test/lake-manifest.json @@ -0,0 +1,5 @@ +{"version": "1.1.0", + "packagesDir": ".lake/packages", + "packages": [], + "name": "ix_test", + "lakeDir": ".lake"} diff --git a/ix_test/lakefile.toml b/ix_test/lakefile.toml new file mode 100644 index 00000000..ff2fd985 --- /dev/null +++ b/ix_test/lakefile.toml @@ -0,0 +1,10 @@ +name = "ix_test" +version = "0.1.0" +defaultTargets = ["ix_test"] + +[[lean_lib]] +name = "IxTest" + +[[lean_exe]] +name = "ix_test" +root = "Main" diff --git a/ix_test/lean-toolchain b/ix_test/lean-toolchain new file mode 100644 index 00000000..db29c97c --- /dev/null +++ b/ix_test/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:4.17.0 diff --git a/lakefile.lean b/lakefile.lean index 961c56bb..17cb5196 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -9,6 +9,7 @@ lean_lib Ix lean_exe ix where root := `Main + supportInterpreter := true require LSpec from git "https://github.com/argumentcomputer/LSpec" @ "24cceb69c20fadca0fd3acabe39fa9270dfb47e6" @@ -28,7 +29,8 @@ section Tests lean_lib Tests @[test_driver] -lean_exe Tests.Main +lean_exe Tests.Main where + supportInterpreter := true end Tests