Merge pull request #21 from functionally/cli

API & CLI

Author: bwbush

lake-manifest.json

@@ -37,14 +37,14 @@
    "inputRev": "v0.0.30",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/lean4-cli",
+  {"url": "https://github.com/leanprover/lean4-cli.git",
    "type": "git",
    "subDir": null,
-   "rev": "be8fa79a28b8b6897dce0713ef50e89c4a0f6ef5",
+   "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
+   "inputRev": "v2.2.0-lv4.7.0",
+   "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/import-graph.git",
    "type": "git",

lakefile.lean

@@ -19,11 +19,15 @@ require mathlib from git
 require LSpec from git
   "https://github.com/argumentcomputer/LSpec.git"
 
+require Cli from git
+  "https://github.com/leanprover/lean4-cli.git"
+  @ "v2.2.0-lv4.7.0"
+
 @[default_target]
 lean_exe «crypto» where
   root := `Main
   srcDir := "src"
   -- Enables the use of the Lean interpreter by the executable (e.g.,
   -- `runFrontend`) at the expense of increased binary size on Linux.
   -- Remove this line if you do not need such functionality.
-  supportInterpreter := true
+  supportInterpreter := false

src/Crypto.lean

@@ -1,4 +1,6 @@
 
+import Crypto.API
+
 import Crypto.Field.Fp
 import Crypto.Field.Fp.Test
 

src/Crypto/API.lean

@@ -0,0 +1,43 @@
+
+import Crypto.Hash
+import Crypto.Serial
+
+open Crypto
+
+
+namespace Crypto.API
+
+
+def bytesToHex (inFile : System.FilePath) (outFile : System.FilePath) : IO Unit :=
+  do
+    let src ← IO.FS.readBinFile inFile
+    let dst := Serial.bytesToHex src
+    IO.FS.writeFile outFile $ dst ++ "\n"
+
+
+def bytesToNat (inFile : System.FilePath) (outFile : System.FilePath) : IO Unit :=
+  do
+    let src ← IO.FS.readBinFile inFile
+    let dst : Nat := Serial.Words.fromWords src.toList.toArray
+    IO.FS.writeFile outFile $ toString dst ++ "\n"
+
+
+def parseHashAlgorithm : String → Option (CHash.Algorithm)
+| "SHA2_224" => some CHash.Algorithm.SHA2_224
+| "SHA2_256" => some CHash.Algorithm.SHA2_256
+| "SHA2_384" => some CHash.Algorithm.SHA2_384
+| "SHA2_512" => some CHash.Algorithm.SHA2_512
+| _ => none
+
+def hash (alg : CHash.Algorithm) (inFile : System.FilePath) (outFile : System.FilePath) : IO Unit :=
+  do
+    let src ← IO.FS.readBinFile inFile
+    let dst :=
+      Serial.bytesToHex
+        ∘ CHash.data
+        ∘ alg.chash
+        $ src
+    IO.FS.writeFile outFile $ dst ++ "\n"
+
+
+end Crypto.API

src/Crypto/Hash.lean

@@ -32,11 +32,11 @@ namespace CHash
     | SHA2_384 => 56
     | SHA2_512 => 64
 
-  def chash [Serializable a] : a → (alg : Algorithm) → CHash alg.length
-  | x , SHA2_224 => CHash.mk ∘ SHA2.sha224 $ Serializable.encode x
-  | x , SHA2_256 => CHash.mk ∘ SHA2.sha256 $ Serializable.encode x
-  | x , SHA2_384 => CHash.mk ∘ SHA2.sha384 $ Serializable.encode x
-  | x , SHA2_512 => CHash.mk ∘ SHA2.sha512 $ Serializable.encode x
+    def chash [Serializable a] : a → (alg : Algorithm) → CHash alg.length
+    | x , SHA2_224 => CHash.mk ∘ SHA2.sha224 $ Serializable.encode x
+    | x , SHA2_256 => CHash.mk ∘ SHA2.sha256 $ Serializable.encode x
+    | x , SHA2_384 => CHash.mk ∘ SHA2.sha384 $ Serializable.encode x
+    | x , SHA2_512 => CHash.mk ∘ SHA2.sha512 $ Serializable.encode x
 
   end Algorithm
 

src/Main.lean

@@ -0,0 +1,78 @@
+import Cli
+import Crypto.API
+
+open Cli
+open Crypto
+
+
+def getInFile (p : Parsed) : System.FilePath :=
+  if p.hasFlag "input" then (p.flag! "input").value else "/dev/stdin"
+
+def getOutFile (p : Parsed) : System.FilePath :=
+  if p.hasFlag "output" then (p.flag! "output").value else "/dev/stdout"
+
+
+def bytesToHexExec (p : Parsed) : IO UInt32 :=
+  do
+    API.bytesToHex (getInFile p) (getOutFile p)
+    pure 0
+
+def bytesToHex : Cmd := `[Cli|
+  bytesToHex VIA bytesToHexExec;
+  "Convert bytes to hexadecimal."
+  FLAGS:
+    i, input  : String ; "Input file."
+    o, output : String ; "Output file."
+]
+
+
+def bytesToNatExec (p : Parsed) : IO UInt32 :=
+  do
+    API.bytesToNat (getInFile p) (getOutFile p)
+    pure 0
+
+def bytesToNat : Cmd := `[Cli|
+  bytesToNat VIA bytesToNatExec;
+  "Convert bytes to a natural number."
+  FLAGS:
+    i, input  : String ; "Input file."
+    o, output : String ; "Output file."
+]
+
+
+def HashAlg : ParamType :=
+  ParamType.mk
+    "Hash algorithm"
+    $ not ∘ BEq.beq none ∘ API.parseHashAlgorithm
+
+def hashExec (p : Parsed) : IO UInt32 :=
+  match API.parseHashAlgorithm (p.positionalArg! "alg").value with
+  | some alg =>
+      do
+        API.hash alg (getInFile p) (getOutFile p)
+        pure 0
+  | none => pure 0
+
+def hash : Cmd := `[Cli|
+  hash VIA hashExec;
+  "Hash bytes."
+  FLAGS:
+    i, input  : String ; "Input file."
+    o, output : String ; "Output file."
+  ARGS:
+    alg : HashAlg; "SHA2_224 | SHA2_256 | SHA2_384 | SHA2_512"
+]
+
+
+def crypto : Cmd := `[Cli|
+  crypto NOOP;
+  "Cryptographic operations."
+  SUBCOMMANDS:
+    bytesToHex;
+    bytesToNat;
+    hash
+]
+
+
+def main (args : List String) : IO UInt32 :=
+  crypto.validate args