sir: text format for Vars

sir/README.md

@@ -33,7 +33,13 @@ deterministic witness.
   progress families arrive with the halting-operations work.
 - [`Sir/Theorems.lean`](Sir/Theorems.lean) — the aggregate exported surface.
 - [`Sir/Examples/`](Sir/Examples/) — well-formedness, (non-)determinism,
-  halting-callee, machine-level execution, and memory/allocation witnesses.
+  halting-callee, machine-level execution, round-trip, and memory/allocation
+  witnesses.
+- [`Sir/Vars/Spec/Check.lean`](Sir/Vars/Spec/Check.lean) — one check, returning a
+  proof of the well-formedness clause it discharges.
+- [`Sir/Text/`](Sir/Text/) — the text format: printing a program and parsing it
+  back returns the same program up to renaming, in normal form; an extractor
+  emits a parsed program as Lean source.
 - [`Sir/Audit.lean`](Sir/Audit.lean) — build-time audit of the exported
   surface.
 
@@ -42,3 +48,9 @@ deterministic witness.
 ```sh
 lake build
 ```
+
+Extract a `.sir` file into a Lean module:
+
+```sh
+lake env lean --run SirExtract.lean input.sir Output.lean programName
+```

sir/Sir.lean

@@ -11,5 +11,7 @@ import Sir.Examples.TwoFunction
 import Sir.Examples.Memory
 import Sir.Examples.HaltedCall
 import Sir.Examples.Jump
-import Sir.Audit
 import Sir.Examples.Machine
+import Sir.Examples.Text
+import Sir.Text.Extract
+import Sir.Audit

sir/Sir/Audit.lean

@@ -15,6 +15,7 @@ import Sir.Examples.Jump
 import Sir.Examples.Machine
 import Sir.Examples.Lowering
 import Sir.Examples.Corpus
+import Sir.Examples.Text
 
 open Lean Elab Command
 
@@ -33,7 +34,7 @@ private def auditedModule (moduleName : Name) : Bool :=
 private def allowedModule (theoremModule moduleName : Name) : Bool :=
   ((`Sir).isPrefixOf moduleName && moduleContainsSpec moduleName) ||
     [`Init, `Lean, `Std, `Evm].any (·.isPrefixOf moduleName) ||
-    (`Sir.Examples).isPrefixOf theoremModule && moduleName == theoremModule
+    ((`Sir.Examples).isPrefixOf theoremModule && (`Sir.Examples).isPrefixOf moduleName)
 
 private def auditTheorem (env : Environment) (theoremModule theoremName : Name)
     (theoremInfo : ConstantInfo) : CommandElabM Nat := do

sir/Sir/Examples/Text.lean

@@ -0,0 +1,79 @@
+import Sir.Theorems
+import Sir.Examples.TwoFunction
+import Sir.Examples.Jump
+import Sir.Examples.Memory
+import Sir.Examples.HaltedCall
+import Sir.Examples.ZeroedMalloc
+
+namespace Sir.Examples
+
+open Sir.Vars Sir.Vars.Text
+
+def witnessAddSource : String :=
+  "fn init:\nentry {\na = const 2\nb = const 3\nr = icall @add2 a b\nstop\n}\n" ++
+  "fn add2:\nentry x y -> z {\nz = add x y\niret\n}\n"
+
+theorem parse_witnessAddSource : parse witnessAddSource = .ok witnessAddProgram := by
+  parse_rfl
+
+theorem parse_print_witnessAdd : parse (print witnessAddProgram) = .ok witnessAddProgram := by
+  exact parse_print parse_witnessAddSource
+
+def jumpPrinted : String :=
+  "fn init : \nblock0 -> v0 { \nv0 = const 7 \n=> @block1 \n} \n" ++
+  "block1 v1 { \nv2 = add v1 v1 \nstop \n} \n"
+
+theorem parse_print_jump : parse (print jumpProgram) = .ok jumpProgram := by
+  exact parse_print (source := jumpPrinted) (by parse_rfl)
+
+def initializedLoadPrinted : String :=
+  "fn init : \nblock0 { \nv0 = const 32 \nv1 = mallocany v0 \nv2 = const 42 \n" ++
+  "mstore256 v1 v2 \nv3 = mload256 v1 \nsstore v3 v3 \nstop \n} \n"
+
+theorem parse_print_initializedLoad : parse (print initializedLoad) = .ok initializedLoad := by
+  exact parse_print (source := initializedLoadPrinted) (by parse_rfl)
+
+def zeroSizeStorePrinted : String :=
+  "fn init : \nblock0 { \nv0 = const 0 \nv1 = mallocany v0 \nsstore v1 v1 \nstop \n} \n"
+
+theorem parse_print_zeroSizeStore : parse (print zeroSizeStore) = .ok zeroSizeStore := by
+  exact parse_print (source := zeroSizeStorePrinted) (by parse_rfl)
+
+def zeroedMallocLoadPrinted : String :=
+  "fn init : \nblock0 { \nv0 = const 32 \nv1 = malloc v0 \nv2 = mload256 v1 \nstop \n} \n"
+
+theorem parse_print_zeroedMallocLoad :
+    parse (print zeroedMallocLoad) = .ok zeroedMallocLoad := by
+  exact parse_print (source := zeroedMallocLoadPrinted) (by parse_rfl)
+
+def haltedCallPrinted : String :=
+  "fn init : \nblock0 { \nicall @main \nstop \n} \nfn main : \nblock0 { \nstop \n} \n"
+
+theorem parse_print_haltedCall : parse (print haltedCallProgram) = .ok haltedCallProgram := by
+  exact parse_print (source := haltedCallPrinted) (by parse_rfl)
+
+def selfCallProgram : Program :=
+  { init :=
+      { entry :=
+          { inputs := #[]
+            statements := #[.icall ⟨0⟩ #[] #[]]
+            terminator := .halt
+            outputs := #[] }
+        rest := #[] }
+    main := none
+    rest := #[] }
+
+theorem witnessAdd_wellFormed : witnessAddProgram.WellFormed :=
+  Vars.Program.wellFormed_of_check (by rfl)
+
+theorem haltedCall_wellFormed : haltedCallProgram.WellFormed :=
+  Vars.Program.wellFormed_of_check (by rfl)
+
+theorem jump_wellFormed : jumpProgram.WellFormed :=
+  Vars.Program.wellFormed_of_check (by rfl)
+
+theorem checkWellFormed_selfCall :
+    checkWellFormed selfCallProgram = .error (.recursiveCall ⟨0⟩ ⟨0⟩) := by
+  rfl
+
+end Sir.Examples

sir/Sir/Text/Extract.lean

@@ -0,0 +1,118 @@
+import Sir.Text.Spec.Parser
+import Sir.Vars.Spec.Check
+
+namespace Sir.Vars.Text
+
+def idLit (id : Nat) : String := "⟨" ++ decimalString id ++ "⟩"
+
+def varLit (identifier : VarId) : String := idLit identifier.id
+
+def arrayLit (elements : List String) : String :=
+  if elements.isEmpty then "#[]" else "#[" ++ String.intercalate ", " elements ++ "]"
+
+def varArrayLit (identifiers : Array VarId) : String :=
+  arrayLit (identifiers.toList.map varLit)
+
+def exprLit : Expr → String
+  | .constant value => "(.constant (.ofNat " ++ decimalString value.toNat ++ "))"
+  | .var source => "(.var " ++ varLit source ++ ")"
+  | .add lhs rhs => "(.add " ++ varLit lhs ++ " " ++ varLit rhs ++ ")"
+  | .lt lhs rhs => "(.lt " ++ varLit lhs ++ " " ++ varLit rhs ++ ")"
+  | .sload key => "(.sload " ++ varLit key ++ ")"
+
+def stmtLit : Stmt → String
+  | .assign result value => ".assign " ++ varLit result ++ " " ++ exprLit value
+  | .sstore key value => ".sstore " ++ varLit key ++ " " ++ varLit value
+  | .gas result => ".gas " ++ varLit result
+  | .call callData =>
+      ".call { callee := " ++ varLit callData.callee ++ ", gas := " ++ varLit callData.gas ++
+        ", result := " ++ varLit callData.result ++ " }"
+  | .malloc result size => ".malloc " ++ varLit result ++ " " ++ varLit size
+  | .mallocUninit result size => ".mallocUninit " ++ varLit result ++ " " ++ varLit size
+  | .mstore32 offset value => ".mstore32 " ++ varLit offset ++ " " ++ varLit value
+  | .mload32 result offset => ".mload32 " ++ varLit result ++ " " ++ varLit offset
+  | .icall callee args dests =>
+      ".icall " ++ idLit callee.id ++ " " ++ varArrayLit args ++ " " ++ varArrayLit dests
+
+def terminatorLit : Terminator → String
+  | .halt => ".halt"
+  | .iret => ".iret"
+  | .jump target => ".jump " ++ idLit target.id
+  | .branch condition thenTarget elseTarget =>
+      ".branch " ++ varLit condition ++ " " ++ idLit thenTarget.id ++ " " ++ idLit elseTarget.id
+
+def indent (depth : Nat) : String :=
+  String.ofList (List.replicate (2 * depth) ' ')
+
+def blockLit (depth : Nat) (block : Block) : String :=
+  let statements :=
+    if block.statements.isEmpty then "#[]"
+    else "#[\n" ++
+      String.intercalate ",\n"
+        (block.statements.toList.map fun statement =>
+          indent (depth + 2) ++ stmtLit statement) ++ "]"
+  "{ inputs := " ++ varArrayLit block.inputs ++ ",\n" ++
+    indent (depth + 1) ++ "statements := " ++ statements ++ ",\n" ++
+    indent (depth + 1) ++ "terminator := " ++ terminatorLit block.terminator ++ ",\n" ++
+    indent (depth + 1) ++ "outputs := " ++ varArrayLit block.outputs ++ " }"
+
+def functionLit (depth : Nat) (function : Function) : String :=
+  "{ entry := " ++ blockLit (depth + 1) function.entry ++ ",\n" ++
+    indent (depth + 1) ++ "rest := " ++
+    (if function.rest.isEmpty then "#[]"
+     else "#[\n" ++
+       String.intercalate ",\n"
+         (function.rest.toList.map fun block =>
+           indent (depth + 2) ++ blockLit (depth + 2) block) ++ "]") ++ " }"
+
+def functionArrayLit (depth : Nat) (functions : Array Function) : String :=
+  if functions.isEmpty then "#[]"
+  else "#[\n" ++
+    String.intercalate ",\n"
+      (functions.toList.map fun function =>
+        indent (depth + 1) ++ functionLit (depth + 1) function) ++ "]"
+
+def toLeanModule (declaration : String) (program : Program) : String :=
+  "import Sir.Vars.Spec\n\nnamespace Sir.Vars\n\ndef " ++ declaration ++ " : Program :=\n" ++
+  "  { init := " ++ functionLit 2 program.init ++ ",\n" ++
+  "    main := " ++
+    (match program.main with
+     | none => "none"
+     | some function => "some " ++ functionLit 2 function) ++ ",\n" ++
+  "    rest := " ++ functionArrayLit 2 program.rest ++ " }\n\nend Sir.Vars\n"
+
+def isDeclarationStart (character : Char) : Bool :=
+  character.isAlpha || character == '_'
+
+def isDeclarationRest (character : Char) : Bool :=
+  character.isAlphanum || character == '_' || character == '\''
+
+def isDeclarationName (name : String) : Bool :=
+  match name.toList with
+  | [] => false
+  | first :: rest => isDeclarationStart first && rest.all isDeclarationRest
+
+def diagnosticMessage : Diagnostic → String
+  | .icallArity callee args dests =>
+      s!"icall of function {callee.id} passes {args} arguments and binds {dests} results"
+  | .iretArity declared actual =>
+      s!"iret returns {actual} values but the function declares {declared}"
+  | .recursiveCall caller callee =>
+      s!"function {caller.id} calls function {callee.id} recursively"
+  | .entryArity function params outputs =>
+      s!"entry function {function.id} takes {params} arguments and returns {outputs} values"
+  | .jumpTarget target none _ => s!"jump to missing block {target.id}"
+  | .jumpTarget target (some inputs) outputs =>
+      s!"jump to block {target.id} passes {outputs} values to {inputs} parameters"
+  | .variableUse identifier =>
+      s!"variable {identifier.id} is used before it is defined"
+
+def extract (source declaration : String) : Except String String := do
+  if !isDeclarationName declaration then
+    throw s!"invalid declaration name {String.quote declaration}"
+  let program ← parse source
+  match checkWellFormed program with
+  | .error diagnostic => throw (diagnosticMessage diagnostic)
+  | .ok () => return toLeanModule declaration program
+
+end Sir.Vars.Text