diff --git a/sir/README.md b/sir/README.md index d20b08ed..8200b4fc 100644 --- a/sir/README.md +++ b/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 +``` diff --git a/sir/Sir.lean b/sir/Sir.lean index 23471deb..d806d25f 100644 --- a/sir/Sir.lean +++ b/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 diff --git a/sir/Sir/Audit.lean b/sir/Sir/Audit.lean index ef2695ae..e35d6b8d 100644 --- a/sir/Sir/Audit.lean +++ b/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 diff --git a/sir/Sir/Examples/Text.lean b/sir/Sir/Examples/Text.lean new file mode 100644 index 00000000..ff2ddb63 --- /dev/null +++ b/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 diff --git a/sir/Sir/Text/Extract.lean b/sir/Sir/Text/Extract.lean new file mode 100644 index 00000000..09317e58 --- /dev/null +++ b/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 diff --git a/sir/Sir/Text/Proofs/Lexer.lean b/sir/Sir/Text/Proofs/Lexer.lean new file mode 100644 index 00000000..6326395c --- /dev/null +++ b/sir/Sir/Text/Proofs/Lexer.lean @@ -0,0 +1,238 @@ +import Sir.Text.Spec.Lexer + +namespace Sir.Vars.Text + +theorem digitValue_decimalDigitChar {value : Nat} (h : value < 10) : + digitValue (decimalDigitChar value) = value := by + match value, h with + | 0, _ => rfl + | 1, _ => rfl + | 2, _ => rfl + | 3, _ => rfl + | 4, _ => rfl + | 5, _ => rfl + | 6, _ => rfl + | 7, _ => rfl + | 8, _ => rfl + | 9, _ => rfl + | _ + 10, h => omega + +theorem digitsValue_append_singleton (base : Nat) (digits : List Char) (digit : Char) : + digitsValue base (digits ++ [digit]) = digitsValue base digits * base + digitValue digit := by + simp [digitsValue, List.foldl_append] + +theorem digitsValue_decimalDigitsAux : ∀ (fuel value : Nat), value ≤ fuel → + digitsValue 10 (decimalDigitsAux fuel value) = value + | 0, value, h => by + have : value = 0 := Nat.le_zero.mp h + subst this + rfl + | fuel + 1, value, h => by + rw [decimalDigitsAux] + by_cases hsmall : value < 10 + · rw [if_pos hsmall] + simpa [digitsValue] using digitValue_decimalDigitChar hsmall + · have hten : 10 ≤ value := Nat.le_of_not_lt hsmall + have hlt : value / 10 < value := Nat.div_lt_self (by omega) (by omega) + have hrec := digitsValue_decimalDigitsAux fuel (value / 10) (by omega) + rw [if_neg hsmall, digitsValue_append_singleton, hrec, + digitValue_decimalDigitChar (Nat.mod_lt _ (by omega))] + omega + +theorem digitsValue_decimalDigits (value : Nat) : + digitsValue 10 (decimalDigits value) = value := + digitsValue_decimalDigitsAux value value (Nat.le_refl value) + +theorem decimalDigitChar_isDigit (value : Nat) : (decimalDigitChar value).isDigit = true := by + match value with + | 0 => rfl + | 1 => rfl + | 2 => rfl + | 3 => rfl + | 4 => rfl + | 5 => rfl + | 6 => rfl + | 7 => rfl + | 8 => rfl + | _ + 9 => rfl + +theorem decimalDigitsAux_ne_nil : ∀ (fuel value : Nat), decimalDigitsAux fuel value ≠ [] + | 0, _ => by simp [decimalDigitsAux] + | fuel + 1, value => by + rw [decimalDigitsAux] + by_cases hsmall : value < 10 + · rw [if_pos hsmall]; simp + · rw [if_neg hsmall]; simp + +theorem decimalDigitsAux_all_isDigit : ∀ (fuel value : Nat), + (decimalDigitsAux fuel value).all Char.isDigit = true + | 0, value => by simp [decimalDigitsAux, decimalDigitChar_isDigit] + | fuel + 1, value => by + rw [decimalDigitsAux] + by_cases hsmall : value < 10 + · rw [if_pos hsmall]; simp [decimalDigitChar_isDigit] + · rw [if_neg hsmall] + simp [decimalDigitsAux_all_isDigit fuel, decimalDigitChar_isDigit] + +theorem decimalDigits_ne_nil (value : Nat) : decimalDigits value ≠ [] := + decimalDigitsAux_ne_nil value value + +theorem decimalDigits_all_isDigit (value : Nat) : + (decimalDigits value).all Char.isDigit = true := + decimalDigitsAux_all_isDigit value value + +theorem isIdentifierBody_of_isDigit {character : Char} (h : character.isDigit = true) : + isIdentifierBody character = true := by + simp [isIdentifierBody, Char.isAlphanum, h] + +theorem tokenizeAux_idle_newline (characters : List Char) : + tokenizeAux .idle ('\n' :: characters) = .newline :: tokenizeAux .idle characters := rfl + +theorem tokenizeAux_idle_at (characters : List Char) : + tokenizeAux .idle ('@' :: characters) = tokenizeAux (.label []) characters := rfl + +theorem tokenizeAux_word_space (accumulator characters : List Char) : + tokenizeAux (.word accumulator) (' ' :: characters) = + wordToken accumulator.reverse :: tokenizeAux .idle characters := rfl + +theorem tokenizeAux_label_space (accumulator characters : List Char) : + tokenizeAux (.label accumulator) (' ' :: characters) = + flush (.label accumulator) ++ tokenizeAux .idle characters := by + cases accumulator <;> rfl + +theorem tokenizeAux_idle_body {character : Char} (h : isIdentifierBody character = true) + (characters : List Char) : + tokenizeAux .idle (character :: characters) = tokenizeAux (.word [character]) characters := by + rw [tokenizeAux.eq_def] + split <;> simp_all <;> exact absurd h (by decide) + +theorem tokenizeAux_word_body {character : Char} (h : isIdentifierBody character = true) + (accumulator characters : List Char) : + tokenizeAux (.word accumulator) (character :: characters) = + tokenizeAux (.word (character :: accumulator)) characters := by + rw [tokenizeAux.eq_def] + split <;> simp_all <;> exact absurd h (by decide) + +theorem tokenizeAux_label_body {character : Char} (h : isIdentifierBody character = true) + (accumulator characters : List Char) : + tokenizeAux (.label accumulator) (character :: characters) = + tokenizeAux (.label (character :: accumulator)) characters := by + rw [tokenizeAux.eq_def] + split <;> simp_all <;> exact absurd h (by decide) + +theorem tokenizeAux_word_run : ∀ (word : List Char), word.all isIdentifierBody = true → + ∀ (accumulator characters : List Char), + tokenizeAux (.word accumulator) (word ++ ' ' :: characters) = + wordToken (accumulator.reverse ++ word) :: tokenizeAux .idle characters + | [], _, accumulator, characters => by simp [tokenizeAux_word_space] + | first :: rest, h, accumulator, characters => by + simp only [List.all_cons, Bool.and_eq_true] at h + rw [List.cons_append, tokenizeAux_word_body h.left, + tokenizeAux_word_run rest h.right] + simp + +theorem tokenizeAux_label_run : ∀ (word : List Char), word.all isIdentifierBody = true → + ∀ (accumulator characters : List Char), + tokenizeAux (.label accumulator) (word ++ ' ' :: characters) = + flush (.label (word.reverse ++ accumulator)) ++ tokenizeAux .idle characters + | [], _, accumulator, characters => by simp [tokenizeAux_label_space] + | first :: rest, h, accumulator, characters => by + simp only [List.all_cons, Bool.and_eq_true] at h + rw [List.cons_append, tokenizeAux_label_body h.left, + tokenizeAux_label_run rest h.right] + simp + +theorem flush_label_of_ne_nil {characters : List Char} (h : characters ≠ []) : + flush (.label characters) = [.label (String.ofList characters.reverse)] := by + cases characters with + | nil => exact absurd rfl h + | cons first rest => rfl + +theorem wordToken_identifier {first : Char} {rest : List Char} (h : first.isDigit = false) : + wordToken (first :: rest) = .identifier (String.ofList (first :: rest)) := by + rw [wordToken.eq_def] + split <;> simp_all + +theorem wordToken_number {characters : List Char} (hne : characters ≠ []) + (h : characters.all Char.isDigit = true) : + wordToken characters = .number (digitsValue 10 characters) := by + rw [wordToken.eq_def] + split <;> simp_all + +theorem all_isIdentifierBody_of_all_isDigit : ∀ {characters : List Char}, + characters.all Char.isDigit = true → characters.all isIdentifierBody = true + | [], _ => rfl + | _ :: rest, h => by + simp only [List.all_cons, Bool.and_eq_true] at h ⊢ + exact ⟨isIdentifierBody_of_isDigit h.left, all_isIdentifierBody_of_all_isDigit h.right⟩ + +def Token.Renderable : Token → Prop + | .identifier name => + ∃ first rest, name.toList = first :: rest ∧ first.isDigit = false ∧ + (first :: rest).all isIdentifierBody = true + | .label name => + ∃ first rest, name.toList = first :: rest ∧ (first :: rest).all isIdentifierBody = true + | .invalid _ => False + | _ => True + +theorem tokenizeAux_idle_characters {token : Token} (h : token.Renderable) + (characters : List Char) : + tokenizeAux .idle (token.characters ++ ' ' :: characters) = + token :: tokenizeAux .idle characters := by + cases token with + | identifier name => + obtain ⟨first, rest, hname, hdigit, hbody⟩ := h + simp only [List.all_cons, Bool.and_eq_true] at hbody + show tokenizeAux .idle (name.toList ++ ' ' :: characters) = _ + rw [hname, List.cons_append, tokenizeAux_idle_body hbody.left, + tokenizeAux_word_run rest hbody.right] + simp only [List.reverse_cons, List.reverse_nil, List.nil_append, List.singleton_append] + rw [wordToken_identifier hdigit, ← hname, String.ofList_toList] + | label name => + obtain ⟨first, rest, hname, hbody⟩ := h + show tokenizeAux .idle ('@' :: name.toList ++ ' ' :: characters) = _ + rw [List.cons_append, tokenizeAux_idle_at, hname, + tokenizeAux_label_run _ hbody, List.append_nil, + flush_label_of_ne_nil (by simp), List.reverse_reverse, ← hname, + String.ofList_toList] + rfl + | number value => + obtain ⟨first, rest, hdigits⟩ := List.exists_cons_of_ne_nil (decimalDigits_ne_nil value) + have hall := decimalDigits_all_isDigit value + have hbody := all_isIdentifierBody_of_all_isDigit hall + rw [hdigits] at hbody + simp only [List.all_cons, Bool.and_eq_true] at hbody + show tokenizeAux .idle (decimalDigits value ++ ' ' :: characters) = _ + rw [hdigits, List.cons_append, tokenizeAux_idle_body hbody.left, + tokenizeAux_word_run rest hbody.right] + simp only [List.reverse_cons, List.reverse_nil, List.nil_append, List.singleton_append] + rw [← hdigits, wordToken_number (decimalDigits_ne_nil value) hall, + digitsValue_decimalDigits] + | invalid character => exact h.elim + | _ => rfl + +theorem renderChars_cons {token : Token} (h : token ≠ .newline) (tokens : List Token) : + renderChars (token :: tokens) = token.characters ++ ' ' :: renderChars tokens := by + cases token <;> first | rfl | exact absurd rfl h + +theorem tokenizeAux_idle_renderChars : ∀ (tokens : List Token), + (∀ token ∈ tokens, token.Renderable) → tokenizeAux .idle (renderChars tokens) = tokens := by + intro tokens + induction tokens with + | nil => intro _; rfl + | cons token rest ih => + intro h + have hrest : ∀ t ∈ rest, t.Renderable := fun t ht => h t (List.mem_cons_of_mem _ ht) + have htoken : token.Renderable := h token (by simp) + by_cases hnewline : token = .newline + · subst hnewline + rw [show renderChars (Token.newline :: rest) = '\n' :: renderChars rest from rfl, + tokenizeAux_idle_newline, ih hrest] + · rw [renderChars_cons hnewline, tokenizeAux_idle_characters htoken, ih hrest] + +theorem tokenize_render {tokens : List Token} (h : ∀ token ∈ tokens, token.Renderable) : + tokenize (render tokens) = tokens := by + simp only [tokenize, render, String.toList_ofList] + exact tokenizeAux_idle_renderChars tokens h + +end Sir.Vars.Text diff --git a/sir/Sir/Text/Proofs/Mnemonic.lean b/sir/Sir/Text/Proofs/Mnemonic.lean new file mode 100644 index 00000000..e3db55d1 --- /dev/null +++ b/sir/Sir/Text/Proofs/Mnemonic.lean @@ -0,0 +1,54 @@ +import Sir.Text.Spec.Mnemonic +import Sir.Vars.Spec.Normalize + +namespace Sir.Vars.Text + +private theorem vector_toList_zero {α : Type} (vector : Vector α 0) : vector.toList = [] := + List.eq_nil_of_length_eq_zero (by simp) + +private theorem vector_toList_one {α : Type} (vector : Vector α 1) : + vector.toList = [vector[0]] := by + obtain ⟨⟨l⟩, h⟩ := vector + match l, h with | [a], _ => rfl + +private theorem vector_toList_two {α : Type} (vector : Vector α 2) : + vector.toList = [vector[0], vector[1]] := by + obtain ⟨⟨l⟩, h⟩ := vector + match l, h with | [a, b], _ => rfl + +theorem spelling_build {entry : Mnemonic} (member : entry ∈ mnemonics) + (results : Vector VarId entry.results) (operands : Vector VarId entry.operands) : + spelling (entry.build results operands) = + ⟨entry.name, results.toList, operands.toList⟩ := by + simp only [mnemonics, List.mem_cons, List.mem_nil_iff, or_false] at member + rcases member with rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl <;> + simp [spelling, vector_toList_zero, vector_toList_one, vector_toList_two] + +theorem mnemonic_name {entry : Mnemonic} (member : entry ∈ mnemonics) : + entry.name ≠ "const" ∧ entry.name ≠ "icall" := by + simp only [mnemonics, List.mem_cons, List.mem_nil_iff, or_false] at member + rcases member with rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl <;> decide + +theorem variableOccurrences_spelling (statement : Stmt) : + statement.variableOccurrences = + (spelling statement).results ++ (spelling statement).operands := by + cases statement with + | assign result value => cases value <;> rfl + | _ => rfl + +theorem build_spelling (statement : Stmt) (rename : VarId → VarId) + (notConst : (spelling statement).name ≠ "const") + (notIcall : (spelling statement).name ≠ "icall") : + ∃ entry, mnemonics.find? (·.name == (spelling statement).name) = some entry ∧ + ∃ (resultsOk : ((spelling statement).results.map rename).toArray.size = entry.results) + (operandsOk : ((spelling statement).operands.map rename).toArray.size = entry.operands), + entry.build ⟨_, resultsOk⟩ ⟨_, operandsOk⟩ = statement.renameVariables rename := by + cases statement with + | assign result value => + cases value with + | constant => exact (notConst rfl).elim + | _ => exact ⟨_, rfl, rfl, rfl, rfl⟩ + | icall => exact (notIcall rfl).elim + | _ => exact ⟨_, rfl, rfl, rfl, rfl⟩ + +end Sir.Vars.Text diff --git a/sir/Sir/Text/Proofs/ParseNormal.lean b/sir/Sir/Text/Proofs/ParseNormal.lean new file mode 100644 index 00000000..c6f68b44 --- /dev/null +++ b/sir/Sir/Text/Proofs/ParseNormal.lean @@ -0,0 +1,806 @@ +import Sir.Text.Spec.Parser +import Sir.Text.Proofs.Mnemonic +import Sir.Vars.Proofs.Normalize + +namespace Sir.Vars.Text + +inductive InterningInvariant : List String → List VarId → Prop where + | empty : InterningInvariant [] [] + | existing {names occurrences identifier} + (invariant : InterningInvariant names occurrences) + (bound : identifier.id < names.length) : + InterningInvariant names (occurrences ++ [identifier]) + | fresh {names occurrences name} + (invariant : InterningInvariant names occurrences) : + InterningInvariant (names ++ [name]) + (occurrences ++ [⟨names.length⟩]) + +namespace InterningInvariant + +theorem append_existing {names occurrences : List _} {identifier : VarId} + (invariant : InterningInvariant names occurrences) + (bound : identifier.id < names.length) : + InterningInvariant names (occurrences ++ [identifier]) := + .existing invariant bound + +theorem append_fresh {names occurrences : List _} {name : String} + (invariant : InterningInvariant names occurrences) : + InterningInvariant (names ++ [name]) + (occurrences ++ [⟨names.length⟩]) := + .fresh invariant + +theorem identifiers_bounded {names occurrences} + (invariant : InterningInvariant names occurrences) : + ∀ identifier ∈ occurrences, identifier.id < names.length := by + induction invariant with + | empty => simp + | existing invariant bound induction => + intro identifier member + simp only [List.mem_append, List.mem_singleton] at member + exact member.elim (induction identifier) (fun equality => equality ▸ bound) + | fresh invariant induction => + intro identifier member + simp only [List.mem_append, List.mem_singleton] at member + rw [List.length_append, List.length_singleton] + exact member.elim + (fun previous => Nat.lt_succ_of_lt (induction identifier previous)) + (fun equality => by subst identifier; simp) + +theorem contains_all {names occurrences} + (invariant : InterningInvariant names occurrences) : + ∀ index, index < names.length → (⟨index⟩ : VarId) ∈ occurrences := by + induction invariant with + | empty => simp + | existing invariant _ induction => + intro index bound + exact List.mem_append_left _ (induction index bound) + | fresh invariant induction => + intro index bound + rw [List.length_append, List.length_singleton] at bound + rcases Nat.lt_or_eq_of_le (Nat.le_of_lt_succ bound) with previous | current + · exact List.mem_append_left _ (induction index previous) + · exact List.mem_append_right _ (by simp [current]) + +theorem eraseDups_eq_range {names occurrences} + (invariant : InterningInvariant names occurrences) : + occurrences.eraseDups = (List.range names.length).map VarId.mk := by + induction invariant with + | empty => rfl + | @existing names occurrences identifier invariant bound induction => + rw [List.eraseDups_append, induction] + have member : identifier ∈ occurrences := + contains_all invariant identifier.id bound + rw [singleton_removeAll_eq_nil member] + simp [List.eraseDups] + | @fresh names occurrences name invariant induction => + rw [List.eraseDups_append, induction] + have notMember : (⟨names.length⟩ : VarId) ∉ occurrences := by + intro member + exact Nat.lt_irrefl _ (identifiers_bounded invariant _ member) + rw [singleton_removeAll_eq_self notMember] + rw [List.eraseDups_cons] + simp [List.range_succ] + +where + singleton_removeAll_eq_nil {identifier : VarId} {identifiers : List VarId} + (member : identifier ∈ identifiers) : + [identifier].removeAll identifiers = [] := by + induction identifiers with + | nil => simp at member + | cons head tail induction => + by_cases equal : identifier = head + · subst head + simp [List.removeAll_cons] + · have tailMember : identifier ∈ tail := by simpa [equal] using member + simpa [List.removeAll_cons, equal] using induction tailMember + singleton_removeAll_eq_self {identifier : VarId} {identifiers : List VarId} + (notMember : identifier ∉ identifiers) : + [identifier].removeAll identifiers = [identifier] := by + induction identifiers with + | nil => rfl + | cons head tail induction => + have unequal : identifier ≠ head := by + intro equality + exact notMember (by simp [equality]) + have tailNotMember : identifier ∉ tail := by + intro member + exact notMember (by simp [member]) + simpa [List.removeAll_cons, unequal] using induction tailNotMember + +private theorem idxOf_range (index count : Nat) (bound : index < count) : + ((List.range count).map VarId.mk).idxOf ⟨index⟩ = index := by + induction count with + | zero => omega + | succ count induction => + rw [List.range_succ, List.map_append, List.idxOf_append] + by_cases previous : index < count + · have member : (⟨index⟩ : VarId) ∈ (List.range count).map VarId.mk := by + simp [previous] + simp [member, induction previous] + · have current : index = count := by omega + subst index + have notMember : (⟨count⟩ : VarId) ∉ (List.range count).map VarId.mk := by + simp + simp [notMember] + +theorem normalVariable_eq {program : Program} {names occurrences} + (invariant : InterningInvariant names occurrences) + (occurrences_eq : occurrences = program.variableOccurrences) + {identifier : VarId} (member : identifier ∈ program.variableOccurrences) : + program.normalVariable identifier = identifier := by + have bound : identifier.id < names.length := + identifiers_bounded invariant identifier (occurrences_eq ▸ member) + simp only [Program.normalVariable] + rw [← occurrences_eq, eraseDups_eq_range invariant, idxOf_range _ _ bound] + +theorem normal {program : Program} {names : List String} + (invariant : InterningInvariant names program.variableOccurrences) : + program.Normal := by + rw [Program.Normal, Program.normalize] + calc + program.renameVariables program.normalVariable = + program.renameVariables id := by + apply Vars.Proofs.Program.renameVariables_congr + intro identifier member + exact normalVariable_eq invariant rfl member + _ = program := Vars.Proofs.Program.renameVariables_id program + +end InterningInvariant + +def PreservesInterning {α : Type} (action : ParserM α) (occurrences : α → List VarId) : Prop := + ∀ names prior value finalNames, + InterningInvariant names prior → + action.run names = .ok (value, finalNames) → + InterningInvariant finalNames (prior ++ occurrences value) + +theorem internVariable_preserves (name : String) : + PreservesInterning (internVariable name) (fun identifier => [identifier]) := by + intro names prior identifier finalNames invariant run + simp [internVariable, StateT.run, bind, StateT.bind, get, getThe, MonadStateOf.get, StateT.get, + set, pure, Except.pure, Except.bind] at run + generalize foundEq : names.findIdx? (· == name) = found at run + cases found with + | none => + simp [bind, StateT.bind, StateT.set, pure, StateT.pure, Except.pure, Except.bind] at run + rcases run with ⟨rfl, rfl⟩ + exact InterningInvariant.fresh invariant + | some index => + simp [pure, StateT.pure, Except.pure] at run + rcases run with ⟨rfl, rfl⟩ + apply InterningInvariant.existing invariant + exact (List.findIdx?_eq_some_iff_findIdx_eq.mp foundEq).1 + +theorem freshVariable_preserves : + PreservesInterning freshVariable (fun identifier => [identifier]) := by + intro names prior identifier finalNames invariant run + change (Except.ok (⟨names.length⟩, names ++ [temporaryName ⟨names.length⟩]) = + Except.ok (identifier, finalNames)) at run + simp only [Except.ok.injEq, Prod.mk.injEq] at run + rcases run with ⟨rfl, rfl⟩ + exact InterningInvariant.fresh invariant + +private theorem run_bind_ok {α β : Type} {action : ParserM α} + {next : α → ParserM β} {initial final : List String} {result : β} + (run : (action >>= next).run initial = .ok (result, final)) : + ∃ value middle, + action.run initial = .ok (value, middle) ∧ + (next value).run middle = .ok (result, final) := by + rw [StateT.run_bind] at run + cases firstRun : action.run initial with + | error message => simp [firstRun, bind, Except.bind] at run + | ok pair => + refine ⟨pair.1, pair.2, by simp only [Prod.eta], ?_⟩ + simpa [firstRun] using run + +theorem variableList_preserves (tokens : List Token) : + PreservesInterning (variableList tokens) (fun identifiers => identifiers.toList) := by + induction tokens with + | nil => + intro names prior identifiers finalNames invariant run + simp [variableList, StateT.run, pure, StateT.pure, Except.pure] at run + rcases run with ⟨rfl, rfl⟩ + simpa using invariant + | cons token rest induction => + cases token with + | identifier name => + intro names prior identifiers finalNames invariant run + rw [variableList] at run + obtain ⟨head, middleNames, headRun, followingRun⟩ := run_bind_ok run + obtain ⟨following, followingNames, restRun, returnRun⟩ := + run_bind_ok followingRun + have afterHead := internVariable_preserves name names prior head middleNames + invariant headRun + have afterRest := induction middleNames (prior ++ [head]) following + followingNames afterHead restRun + simp [StateT.run, pure, StateT.pure, Except.pure] at returnRun + rcases returnRun with ⟨rfl, rfl⟩ + simpa [List.append_assoc] using afterRest + | _ => + intro names prior identifiers finalNames invariant run + simp [variableList, StateT.run, throw, throwThe, MonadExceptOf.throw, + StateT.lift] at run + +def statementOccurrences (statements : List Stmt) : List VarId := + statements.flatMap Stmt.variableOccurrences + +theorem liftNumbers_preserves (tokens : List Token) : + PreservesInterning (liftNumbers tokens) + (fun result => statementOccurrences result.1) := by + induction tokens with + | nil => + intro names prior result finalNames invariant run + simp [liftNumbers, StateT.run, pure, StateT.pure, Except.pure] at run + rcases run with ⟨rfl, rfl⟩ + simpa [statementOccurrences] using invariant + | cons token rest induction => + cases token with + | number value => + intro names prior result finalNames invariant run + rw [liftNumbers] at run + obtain ⟨target, targetNames, targetRun, followingRun⟩ := run_bind_ok run + obtain ⟨following, followingNames, restRun, returnRun⟩ := + run_bind_ok followingRun + have afterTarget := freshVariable_preserves names prior target targetNames + invariant targetRun + have afterRest := induction targetNames (prior ++ [target]) following + followingNames afterTarget restRun + simp [StateT.run, pure, StateT.pure, Except.pure] at returnRun + rcases returnRun with ⟨rfl, rfl⟩ + simpa [statementOccurrences, Stmt.variableOccurrences, + List.append_assoc] using afterRest + | _ => + intro names prior result finalNames invariant run + simp only [liftNumbers] at run + obtain ⟨following, followingNames, restRun, returnRun⟩ := + run_bind_ok run + have afterRest := induction names prior following followingNames invariant restRun + simp [StateT.run, pure, StateT.pure, Except.pure] at returnRun + rcases returnRun with ⟨rfl, rfl⟩ + simpa using afterRest + +theorem operand_preserves (token : Token) : + PreservesInterning (operand token) + (fun result => statementOccurrences result.1 ++ [result.2]) := by + cases token with + | identifier name => + intro names prior result finalNames invariant run + rw [operand] at run + obtain ⟨identifier, middleNames, internRun, returnRun⟩ := run_bind_ok run + have afterIntern := internVariable_preserves name names prior identifier middleNames + invariant internRun + simp [StateT.run, pure, StateT.pure, Except.pure] at returnRun + rcases returnRun with ⟨rfl, rfl⟩ + simpa [statementOccurrences] using afterIntern + | number value => + intro names prior result finalNames invariant run + rw [operand] at run + obtain ⟨identifier, middleNames, freshRun, returnRun⟩ := run_bind_ok run + have afterFresh := freshVariable_preserves names prior identifier middleNames + invariant freshRun + simp [StateT.run, pure, StateT.pure, Except.pure] at returnRun + rcases returnRun with ⟨rfl, rfl⟩ + simpa [statementOccurrences, Stmt.variableOccurrences, List.append_assoc] using + InterningInvariant.existing afterFresh + (InterningInvariant.identifiers_bounded afterFresh identifier (by simp)) + | _ => + intro names prior result finalNames invariant run + simp [operand, StateT.run, throw, throwThe, MonadExceptOf.throw, + StateT.lift] at run + +def ContainsNoNumbers (tokens : List Token) : Prop := + ∀ value, Token.number value ∉ tokens + +theorem liftNumbers_containsNoNumbers {tokens result names finalNames} + (run : (liftNumbers tokens).run names = .ok (result, finalNames)) : + ContainsNoNumbers result.2 := by + induction tokens generalizing names result finalNames with + | nil => + simp [liftNumbers, StateT.run, pure, StateT.pure, Except.pure] at run + rcases run with ⟨rfl, rfl⟩ + simp [ContainsNoNumbers] + | cons token rest induction => + cases token with + | number value => + rw [liftNumbers] at run + obtain ⟨target, targetNames, targetRun, followingRun⟩ := run_bind_ok run + obtain ⟨following, followingNames, restRun, returnRun⟩ := + run_bind_ok followingRun + simp [StateT.run, pure, StateT.pure, Except.pure] at returnRun + rcases returnRun with ⟨rfl, rfl⟩ + have followingNoNumbers := induction restRun + intro other member + simp only [List.mem_cons] at member + exact member.elim Token.noConfusion (followingNoNumbers other) + | _ => + simp only [liftNumbers] at run + obtain ⟨following, followingNames, restRun, returnRun⟩ := run_bind_ok run + simp [StateT.run, pure, StateT.pure, Except.pure] at returnRun + rcases returnRun with ⟨rfl, rfl⟩ + have followingNoNumbers := induction restRun + intro value member + simp only [List.mem_cons] at member + exact member.elim (by simp_all) (followingNoNumbers value) + +theorem operand_preserves_of_not_number {token : Token} + (notNumber : ∀ value, token ≠ .number value) : + PreservesInterning (operand token) (fun result => [result.2]) := by + cases token with + | identifier name => + intro names prior result finalNames invariant run + rw [operand] at run + obtain ⟨identifier, middleNames, internRun, returnRun⟩ := run_bind_ok run + have afterIntern := internVariable_preserves name names prior identifier middleNames + invariant internRun + simp [StateT.run, pure, StateT.pure, Except.pure] at returnRun + rcases returnRun with ⟨rfl, rfl⟩ + simpa using afterIntern + | number value => exact (notNumber value rfl).elim + | _ => + intro names prior result finalNames invariant run + simp [operand, StateT.run, throw, throwThe, MonadExceptOf.throw, + StateT.lift] at run + +theorem operands_preserves_of_containsNoNumbers {tokens : List Token} + (noNumbers : ContainsNoNumbers tokens) : + PreservesInterning (operands tokens) (fun result => result.2.toList) := by + induction tokens with + | nil => + intro names prior result finalNames invariant run + simp [operands, StateT.run, pure, StateT.pure, Except.pure] at run + rcases run with ⟨rfl, rfl⟩ + simpa using invariant + | cons token rest induction => + intro names prior result finalNames invariant run + rw [operands] at run + obtain ⟨head, headNames, headRun, followingRun⟩ := run_bind_ok run + obtain ⟨following, followingNames, restRun, returnRun⟩ := + run_bind_ok followingRun + have tokenNotNumber : ∀ value, token ≠ .number value := by + intro value equality + exact noNumbers value (by simp [equality]) + have restNoNumbers : ContainsNoNumbers rest := by + intro value member + exact noNumbers value (by simp [member]) + have afterHead := operand_preserves_of_not_number tokenNotNumber names prior + head headNames invariant headRun + have afterRest := induction restNoNumbers headNames (prior ++ [head.2]) following + followingNames afterHead restRun + simp [StateT.run, pure, StateT.pure, Except.pure] at returnRun + rcases returnRun with ⟨rfl, rfl⟩ + simpa [List.append_assoc] using afterRest + +theorem parseMnemonic_preserves (functions : List String) (line : Line) + (mnemonic : String) (results : List VarId) (parameters : List Token) + (noNumbers : ContainsNoNumbers parameters) : + ∀ names prior statements finalNames, + InterningInvariant names (prior ++ results) → + (parseMnemonic functions line mnemonic results parameters).run names = + .ok (statements, finalNames) → + InterningInvariant finalNames (prior ++ statementOccurrences statements) := by + intro names prior statements finalNames invariant run + unfold parseMnemonic at run + split at run + · unfold parseInternalCall at run + split at run + case h_1 calleeName args => + generalize foundEq : functions.findIdx? (· == calleeName) = found at run + cases found with + | none => + simp [StateT.run, throw, throwThe, MonadExceptOf.throw, StateT.lift] at run + | some calleeIndex => + obtain ⟨argumentResult, argumentNames, argumentRun, returnRun⟩ := run_bind_ok run + have argsNoNumbers : ContainsNoNumbers args := by + intro value member + exact noNumbers value (by simp [member]) + have afterArguments := operands_preserves_of_containsNoNumbers argsNoNumbers + names (prior ++ results) argumentResult argumentNames invariant argumentRun + simp [StateT.run, pure, StateT.pure, Except.pure] at returnRun + rcases returnRun with ⟨rfl, rfl⟩ + simpa [statementOccurrences, Stmt.variableOccurrences, List.append_assoc] using + afterArguments + case h_2 => + simp [StateT.run, throw, throwThe, MonadExceptOf.throw, StateT.lift] at run + · unfold parseOperation at run + generalize foundEq : mnemonics.find? (·.name == mnemonic) = found at run + cases found with + | none => + simp [StateT.run, throw, throwThe, MonadExceptOf.throw, StateT.lift] at run + | some entry => + have member := List.mem_of_find?_eq_some foundEq + simp only at run + split at run + · obtain ⟨operandResult, operandNames, operandRun, returnRun⟩ := run_bind_ok run + rcases operandResult with ⟨preludes, operandIds⟩ + have afterOperands := operands_preserves_of_containsNoNumbers noNumbers names + (prior ++ results) (preludes, operandIds) operandNames invariant operandRun + simp only at returnRun + split at returnRun + · simp [StateT.run, pure, StateT.pure, Except.pure] at returnRun + rcases returnRun with ⟨rfl, rfl⟩ + simpa [statementOccurrences, variableOccurrences_spelling, spelling_build member, + List.append_assoc] using afterOperands + · simp [StateT.run, throw, throwThe, MonadExceptOf.throw, StateT.lift] at returnRun + · simp [StateT.run, throw, throwThe, MonadExceptOf.throw, StateT.lift] at run + +theorem parseStatement_preserves (functions : List String) (line : Line) : + PreservesInterning (parseStatement functions line) statementOccurrences := by + intro names prior statements finalNames invariant run + unfold parseStatement at run + generalize partsEq : statementParts line = parts at run + rcases parts with ⟨resultTokens, operandTokens⟩ + cases operandTokens with + | nil => + simp [StateT.run, throw, throwThe, MonadExceptOf.throw, StateT.lift] at run + | cons operation parameters => + cases operation with + | identifier mnemonic => + by_cases constant : mnemonic = "const" + · subst mnemonic + simp only at run + obtain ⟨results, resultNames, resultsRun, followingRun⟩ := run_bind_ok run + have afterResults := variableList_preserves resultTokens names prior results + resultNames invariant resultsRun + cases resultListEq : results.toList with + | nil => + simp [resultListEq, StateT.run, throw, throwThe, + MonadExceptOf.throw, StateT.lift] at followingRun + | cons result otherResults => + cases otherResults with + | cons second rest => + simp [resultListEq, StateT.run, throw, throwThe, + MonadExceptOf.throw, StateT.lift] at followingRun + | nil => + cases parameters with + | nil => + simp [resultListEq, StateT.run, throw, throwThe, + MonadExceptOf.throw, StateT.lift] at followingRun + | cons parameter otherParameters => + cases parameter with + | number value => + cases otherParameters with + | cons next rest => + simp [resultListEq, StateT.run, throw, throwThe, + MonadExceptOf.throw, StateT.lift] at followingRun + | nil => + simp [resultListEq, StateT.run, pure, StateT.pure, + Except.pure] at followingRun + rcases followingRun with ⟨rfl, rfl⟩ + simpa [statementOccurrences, Stmt.variableOccurrences, + resultListEq] using afterResults + | _ => + simp [resultListEq, StateT.run, throw, throwThe, + MonadExceptOf.throw, StateT.lift] at followingRun + · simp only at run + obtain ⟨liftedResult, liftedNames, liftedRun, afterLiftRun⟩ := + run_bind_ok run + rcases liftedResult with ⟨lifted, liftedTokens⟩ + obtain ⟨results, resultNames, resultsRun, bodyRun⟩ := + run_bind_ok afterLiftRun + obtain ⟨body, bodyNames, mnemonicRun, returnRun⟩ := run_bind_ok bodyRun + have afterLift := liftNumbers_preserves parameters names prior + (lifted, liftedTokens) liftedNames invariant liftedRun + have afterResults := variableList_preserves resultTokens liftedNames + (prior ++ statementOccurrences lifted) results resultNames afterLift resultsRun + have noNumbers := liftNumbers_containsNoNumbers liftedRun + have afterBody := parseMnemonic_preserves functions line mnemonic results.toList + liftedTokens noNumbers resultNames (prior ++ statementOccurrences lifted) body + bodyNames afterResults mnemonicRun + simp [StateT.run, pure, StateT.pure, Except.pure] at returnRun + rcases returnRun with ⟨rfl, rfl⟩ + simpa [statementOccurrences, List.flatMap_append, + List.append_assoc] using afterBody + | _ => + simp [StateT.run, throw, throwThe, MonadExceptOf.throw, StateT.lift] at run + +private theorem resolveBlock_preserves_state {blocks : List String} {name : String} + {initial final : List String} {identifier : BlockId} + (run : (resolveBlock blocks name).run initial = .ok (identifier, final)) : + final = initial := by + unfold resolveBlock at run + generalize foundEq : blocks.findIdx? (· == name) = found at run + cases found with + | none => + simp [StateT.run, bind, Except.bind, throw, throwThe, MonadExceptOf.throw, + StateT.lift] at run + | some index => + simp [StateT.run, pure, StateT.pure, Except.pure] at run + exact run.2.symm + +theorem parseTerminator_preserves (blocks : List String) (line : Line) : + PreservesInterning (parseTerminator blocks line) Terminator.variableOccurrences := by + intro names prior terminator finalNames invariant run + unfold parseTerminator at run + split at run + case h_1 => + simp [StateT.run, pure, StateT.pure, Except.pure] at run + rcases run with ⟨rfl, rfl⟩ + simpa [Terminator.variableOccurrences] using invariant + case h_2 => + simp [StateT.run, pure, StateT.pure, Except.pure] at run + rcases run with ⟨rfl, rfl⟩ + simpa [Terminator.variableOccurrences] using invariant + case h_3 => + obtain ⟨target, targetNames, targetRun, returnRun⟩ := run_bind_ok run + have targetNamesEq := resolveBlock_preserves_state targetRun + subst targetNames + simp [StateT.run, pure, StateT.pure, Except.pure] at returnRun + rcases returnRun with ⟨rfl, rfl⟩ + simpa [Terminator.variableOccurrences] using invariant + case h_4 _ condition _ _ => + obtain ⟨conditionId, conditionNames, conditionRun, afterConditionRun⟩ := + run_bind_ok run + have afterCondition := internVariable_preserves condition names prior conditionId + conditionNames invariant conditionRun + obtain ⟨thenTarget, thenNames, thenRun, afterThenRun⟩ := + run_bind_ok afterConditionRun + obtain ⟨elseTarget, elseNames, elseRun, returnRun⟩ := run_bind_ok afterThenRun + have thenNamesEq := resolveBlock_preserves_state thenRun + have elseNamesEq := resolveBlock_preserves_state elseRun + subst thenNames + subst elseNames + simp [StateT.run, pure, StateT.pure, Except.pure] at returnRun + rcases returnRun with ⟨rfl, rfl⟩ + simpa [Terminator.variableOccurrences] using afterCondition + case h_5 => + simp [StateT.run, throw, throwThe, MonadExceptOf.throw, StateT.lift] at run + +def blockBodyOccurrences (body : Array Stmt × Terminator) : List VarId := + statementOccurrences body.1.toList ++ body.2.variableOccurrences + +theorem parseBlockBody_preserves (functions blocks : List String) (lines : List Line) : + PreservesInterning (parseBlockBody functions blocks lines) blockBodyOccurrences := by + induction lines with + | nil => + intro names prior body finalNames invariant run + simp [parseBlockBody, StateT.run, throw, throwThe, MonadExceptOf.throw, + StateT.lift] at run + | cons line rest induction => + cases rest with + | nil => + intro names prior body finalNames invariant run + simp only [parseBlockBody] at run + obtain ⟨terminator, terminatorNames, terminatorRun, returnRun⟩ := run_bind_ok run + have afterTerminator := parseTerminator_preserves blocks line names prior + terminator terminatorNames invariant terminatorRun + simp [StateT.run, pure, StateT.pure, Except.pure] at returnRun + rcases returnRun with ⟨rfl, rfl⟩ + simpa [blockBodyOccurrences, statementOccurrences] using afterTerminator + | cons next following => + intro names prior body finalNames invariant run + simp only [parseBlockBody] at run + obtain ⟨statements, statementNames, statementRun, followingRun⟩ := + run_bind_ok run + obtain ⟨bodyResult, bodyNames, bodyRun, returnRun⟩ := + run_bind_ok followingRun + have afterStatements := parseStatement_preserves functions line names prior + statements statementNames invariant statementRun + have afterBody := induction statementNames + (prior ++ statementOccurrences statements) bodyResult bodyNames + afterStatements bodyRun + simp [StateT.run, pure, StateT.pure, Except.pure] at returnRun + rcases bodyResult with ⟨followingStatements, terminator⟩ + rcases returnRun with ⟨rfl, rfl⟩ + simpa [blockBodyOccurrences, statementOccurrences, List.flatMap_append, + List.append_assoc] using afterBody + +def blockHeaderOccurrences (header : Array VarId × Array VarId) : List VarId := + header.1.toList ++ header.2.toList + +theorem parseBlockHeader_preserves (line : Line) : + PreservesInterning (parseBlockHeader line) blockHeaderOccurrences := by + intro names prior header finalNames invariant run + unfold parseBlockHeader at run + split at run + · rename_i name rest + split at run + · rename_i reversedSignature equality + obtain ⟨inputs, inputNames, inputRun, outputRun⟩ := run_bind_ok run + obtain ⟨outputs, outputNames, outputsRun, returnRun⟩ := run_bind_ok outputRun + have afterInputs := variableList_preserves _ names prior inputs inputNames + invariant inputRun + have afterOutputs := variableList_preserves _ inputNames + (prior ++ inputs.toList) outputs outputNames afterInputs outputsRun + simp [StateT.run, pure, StateT.pure, Except.pure] at returnRun + rcases returnRun with ⟨rfl, rfl⟩ + simpa [blockHeaderOccurrences, List.append_assoc] using afterOutputs + · simp [StateT.run, throw, throwThe, MonadExceptOf.throw, StateT.lift] at run + · simp [StateT.run, throw, throwThe, MonadExceptOf.throw, StateT.lift] at run + +theorem parseBlock_preserves (functions blocks : List String) (header : Line) + (body : List Line) : + PreservesInterning (parseBlock functions blocks header body) + Block.variableOccurrences := by + intro names prior block finalNames invariant run + unfold parseBlock at run + obtain ⟨headerResult, headerNames, headerRun, bodyFollowingRun⟩ := run_bind_ok run + obtain ⟨bodyResult, bodyNames, bodyRun, returnRun⟩ := run_bind_ok bodyFollowingRun + rcases headerResult with ⟨inputs, outputs⟩ + rcases bodyResult with ⟨statements, terminator⟩ + have afterHeader := parseBlockHeader_preserves header names prior (inputs, outputs) + headerNames invariant headerRun + have afterBody := parseBlockBody_preserves functions blocks body headerNames + (prior ++ blockHeaderOccurrences (inputs, outputs)) (statements, terminator) + bodyNames afterHeader bodyRun + simp [StateT.run, pure, StateT.pure, Except.pure] at returnRun + rcases returnRun with ⟨rfl, rfl⟩ + simpa [blockHeaderOccurrences, blockBodyOccurrences, statementOccurrences, + Block.variableOccurrences, List.append_assoc] using afterBody + +def blocksOccurrences (blocks : List Block) : List VarId := + blocks.flatMap Block.variableOccurrences + +theorem mapM_parseBlock_preserves (functions blocks : List String) + (groups : List (Line × List Line)) : + PreservesInterning + (groups.mapM fun group => parseBlock functions blocks group.fst group.snd) + blocksOccurrences := by + induction groups with + | nil => + intro names prior parsed finalNames invariant run + simp [StateT.run, pure, StateT.pure, Except.pure] at run + rcases run with ⟨rfl, rfl⟩ + change InterningInvariant names (prior ++ []) + simpa using invariant + | cons group rest induction => + intro names prior parsed finalNames invariant run + simp only [List.mapM_cons] at run + obtain ⟨block, blockNames, blockRun, restFollowingRun⟩ := run_bind_ok run + obtain ⟨following, followingNames, restRun, returnRun⟩ := + run_bind_ok restFollowingRun + have afterBlock := parseBlock_preserves functions blocks group.fst group.snd names + prior block blockNames invariant blockRun + have afterRest := induction blockNames + (prior ++ block.variableOccurrences) following followingNames afterBlock restRun + simp [StateT.run, pure, StateT.pure, Except.pure] at returnRun + rcases returnRun with ⟨rfl, rfl⟩ + simpa [blocksOccurrences, List.append_assoc] using afterRest + +theorem parseFunction_preserves (functions : List String) (body : List Line) : + PreservesInterning (parseFunction functions body) Function.variableOccurrences := by + intro names prior function finalNames invariant run + unfold parseFunction at run + generalize groupsEq : splitBlocks body = groupsResult at run + cases groupsResult with + | error message => + simp [StateT.run, bind, Except.bind, throw, throwThe, MonadExceptOf.throw, + StateT.lift] at run + | ok groups => + unfold parseFunctionGroups at run + simp [StateT.run, bind, StateT.bind, liftM, monadLift, MonadLift.monadLift, + StateT.lift, Except.bind] at run + generalize blocksEq : groups.mapM (fun group => blockHeaderName group.fst) = + blocksResult at run + cases blocksResult with + | error message => simp at run + | ok blockNames => + by_cases duplicates : hasDuplicates blockNames + · simp [duplicates, bind, StateT.bind, pure, Except.pure, Except.bind, throw, throwThe, + MonadExceptOf.throw, StateT.lift] at run + · simp [duplicates, bind, StateT.bind, pure, StateT.pure, Except.pure, + Except.bind] at run + generalize parsedEq : + (groups.mapM fun group => parseBlock functions blockNames group.fst group.snd) + names = parsedResult + rw [parsedEq] at run + cases parsedResult with + | error message => contradiction + | ok result => + rcases result with ⟨parsed, parsedNames⟩ + have afterParsed := mapM_parseBlock_preserves functions blockNames groups + names prior parsed parsedNames invariant parsedEq + cases parsed with + | nil => + simp [throw, throwThe, MonadExceptOf.throw, StateT.lift] at run + | cons entry rest => + change Except.ok + ({ entry := entry, rest := rest.toArray }, parsedNames) = + Except.ok (function, finalNames) at run + simp only [Except.ok.injEq, Prod.mk.injEq] at run + rcases run with ⟨rfl, rfl⟩ + simpa [Function.variableOccurrences, Function.blocks, + blocksOccurrences] using afterParsed + +def functionsOccurrences (functions : List Function) : List VarId := + functions.flatMap Function.variableOccurrences + +theorem mapM_parseFunction_preserves (names : List String) + (groups : List (String × List Line)) : + PreservesInterning + (groups.mapM fun group => parseFunction names group.snd) + functionsOccurrences := by + induction groups with + | nil => + intro stateNames prior parsed finalNames invariant run + simp [StateT.run, pure, StateT.pure, Except.pure] at run + rcases run with ⟨rfl, rfl⟩ + simpa [functionsOccurrences] using invariant + | cons group rest induction => + intro stateNames prior parsed finalNames invariant run + simp only [List.mapM_cons] at run + obtain ⟨function, functionNames, functionRun, restFollowingRun⟩ := run_bind_ok run + obtain ⟨following, followingNames, restRun, returnRun⟩ := + run_bind_ok restFollowingRun + have afterFunction := parseFunction_preserves names group.snd stateNames prior + function functionNames invariant functionRun + have afterRest := induction functionNames + (prior ++ function.variableOccurrences) following followingNames afterFunction restRun + simp [StateT.run, pure, StateT.pure, Except.pure] at returnRun + rcases returnRun with ⟨rfl, rfl⟩ + simpa [functionsOccurrences, List.append_assoc] using afterRest + +theorem parseFunctionSlots_preserves (names : List String) (initGroup : String × List Line) + (following : List (String × List Line)) : + PreservesInterning (parseFunctionSlots names initGroup following) + (fun slots => slots.1.variableOccurrences ++ functionsOccurrences slots.2) := by + intro stateNames prior slots finalNames invariant run + unfold parseFunctionSlots at run + obtain ⟨init, initNames, initRun, followingRun⟩ := run_bind_ok run + obtain ⟨following, followingNames, followingParsedRun, returnRun⟩ := + run_bind_ok followingRun + have afterInit := parseFunction_preserves names initGroup.snd stateNames prior init + initNames invariant initRun + have afterFollowing := mapM_parseFunction_preserves names _ initNames + (prior ++ init.variableOccurrences) following followingNames afterInit followingParsedRun + simp [StateT.run, pure, StateT.pure, Except.pure] at returnRun + rcases returnRun with ⟨rfl, rfl⟩ + simpa [List.append_assoc] using afterFollowing + +theorem programOfSlots_functions (hasMain : Bool) (init : Function) + (following : List Function) : + (programOfSlots hasMain init following).functions = #[init] ++ following.toArray := by + cases hasMain <;> cases following <;> simp [programOfSlots, Program.functions] + +theorem programOfSlots_variableOccurrences (hasMain : Bool) (init : Function) + (following : List Function) : + (programOfSlots hasMain init following).variableOccurrences = + init.variableOccurrences ++ functionsOccurrences following := by + simp [Program.variableOccurrences, programOfSlots_functions, functionsOccurrences] + +theorem parseProgramSlots_normal {initGroup : String × List Line} + {mainGroup : Option (String × List Line)} {others : List (String × List Line)} + {program : Program} (parsed : parseProgramSlots initGroup mainGroup others = .ok program) : + program.Normal := by + unfold parseProgramSlots at parsed + simp only [] at parsed + split at parsed + · simp at parsed + · rename_i result slotsEq + rcases result with ⟨slots, slotNames⟩ + simp only [Except.ok.injEq] at parsed + subst program + have invariant := parseFunctionSlots_preserves _ initGroup _ [] [] slots slotNames + .empty slotsEq + apply InterningInvariant.normal + simpa [programOfSlots_variableOccurrences] using invariant + +theorem parseProgramGroups_normal {groups : List (String × List Line)} {program : Program} + (parsed : parseProgramGroups groups = .ok program) : program.Normal := by + unfold parseProgramGroups at parsed + by_cases duplicates : hasDuplicates (groups.map Prod.fst) + · simp [duplicates, bind, Except.bind] at parsed + · simp only [duplicates, Bool.false_eq_true, if_false, bind, Except.bind, pure, + Except.pure] at parsed + cases initEq : groups.find? (fun group => group.fst == "init") with + | none => + rw [initEq] at parsed + simp at parsed + | some initGroup => + rw [initEq] at parsed + exact parseProgramSlots_normal parsed + +theorem parseTokens_normal {tokens : List Token} {program : Program} + (parsed : parseTokens tokens = .ok program) : program.Normal := by + unfold parseTokens at parsed + generalize splitEq : splitFunctions (splitLines tokens) = groupsResult at parsed + cases groupsResult with + | error message => contradiction + | ok groups => exact parseProgramGroups_normal parsed + +namespace Proofs + +theorem parse_normal {source : String} {program : Program} + (parsed : parse source = .ok program) : program.Normal := + parseTokens_normal parsed + +end Proofs +end Sir.Vars.Text diff --git a/sir/Sir/Text/Proofs/Printer.lean b/sir/Sir/Text/Proofs/Printer.lean new file mode 100644 index 00000000..b83d3e04 --- /dev/null +++ b/sir/Sir/Text/Proofs/Printer.lean @@ -0,0 +1,166 @@ +import Sir.Text.Proofs.Lexer +import Sir.Text.Spec.Printer + +namespace Sir.Vars.Text + +theorem toList_decimalString (value : Nat) : + (decimalString value).toList = decimalDigits value := by + simp [decimalString, String.toList_ofList] + +theorem toList_append_decimalString {lead : String} {first : Char} {rest : List Char} + (hname : lead.toList = first :: rest) (value : Nat) : + (lead ++ decimalString value).toList = first :: (rest ++ decimalDigits value) := by + rw [String.toList_append, toList_decimalString, hname, List.cons_append] + +theorem all_isIdentifierBody_append_decimalDigits {first : Char} {rest : List Char} + (hbody : (first :: rest).all isIdentifierBody = true) (value : Nat) : + (first :: (rest ++ decimalDigits value)).all isIdentifierBody = true := by + simp only [List.all_cons, Bool.and_eq_true, List.all_append] at hbody ⊢ + exact ⟨hbody.left, hbody.right, + all_isIdentifierBody_of_all_isDigit (decimalDigits_all_isDigit value)⟩ + +theorem renderable_identifier_decimal {lead : String} {first : Char} {rest : List Char} + (hname : lead.toList = first :: rest) (hdigit : first.isDigit = false) + (hbody : (first :: rest).all isIdentifierBody = true) (value : Nat) : + (Token.identifier (lead ++ decimalString value)).Renderable := + ⟨first, rest ++ decimalDigits value, toList_append_decimalString hname value, hdigit, + all_isIdentifierBody_append_decimalDigits hbody value⟩ + +theorem renderable_label_decimal {lead : String} {first : Char} {rest : List Char} + (hname : lead.toList = first :: rest) + (hbody : (first :: rest).all isIdentifierBody = true) (value : Nat) : + (Token.label (lead ++ decimalString value)).Renderable := + ⟨first, rest ++ decimalDigits value, toList_append_decimalString hname value, + all_isIdentifierBody_append_decimalDigits hbody value⟩ + +@[simp] theorem renderable_number (value : Nat) : (Token.number value).Renderable := trivial +@[simp] theorem renderable_equals : Token.equals.Renderable := trivial +@[simp] theorem renderable_arrow : Token.arrow.Renderable := trivial +@[simp] theorem renderable_fatArrow : Token.fatArrow.Renderable := trivial +@[simp] theorem renderable_colon : Token.colon.Renderable := trivial +@[simp] theorem renderable_question : Token.question.Renderable := trivial +@[simp] theorem renderable_leftBrace : Token.leftBrace.Renderable := trivial +@[simp] theorem renderable_rightBrace : Token.rightBrace.Renderable := trivial +@[simp] theorem renderable_newline : Token.newline.Renderable := trivial + +@[simp] theorem renderable_variableToken (identifier : VarId) : + (variableToken identifier).Renderable := + renderable_identifier_decimal (lead := "v") rfl (by decide) (by decide) identifier.id + +@[simp] theorem renderable_blockNameToken (block : BlockId) : + (Token.identifier (blockName block)).Renderable := + renderable_identifier_decimal (lead := "block") rfl (by decide) (by decide) block.id + +@[simp] theorem renderable_blockNameLabel (block : BlockId) : + (Token.label (blockName block)).Renderable := + renderable_label_decimal (lead := "block") rfl (by decide) block.id + +@[simp] theorem renderable_functionNameToken (program : Program) (function : FunctionId) : + (Token.identifier (functionName program function)).Renderable := by + rw [functionName] + split + · exact ⟨'i', _, rfl, by decide, by decide⟩ + split + · exact ⟨'m', _, rfl, by decide, by decide⟩ + · exact renderable_identifier_decimal (lead := "fn") rfl (by decide) (by decide) function.id + +@[simp] theorem renderable_functionNameLabel (program : Program) (function : FunctionId) : + (Token.label (functionName program function)).Renderable := by + rw [functionName] + split + · exact ⟨'i', _, rfl, by decide⟩ + split + · exact ⟨'m', _, rfl, by decide⟩ + · exact renderable_label_decimal (lead := "fn") rfl (by decide) function.id + +@[simp] theorem renderable_variableTokens (identifiers : Array VarId) : + ∀ token ∈ variableTokens identifiers, token.Renderable := by + simp [variableTokens] + +@[simp] theorem renderable_definitionTokens (results : List VarId) : + ∀ token ∈ definitionTokens results, token.Renderable := by + rw [definitionTokens] + split + · simp + · simp only [List.forall_mem_append, List.forall_mem_cons, List.forall_mem_map] + simp + +theorem renderable_identifier_of_chars {name : String} (nonempty : name.toList ≠ []) + (notDigit : name.toList.head!.isDigit = false) + (body : name.toList.all isIdentifierBody = true) : (Token.identifier name).Renderable := by + generalize chars : name.toList = characters at * + cases characters with + | nil => exact (nonempty rfl).elim + | cons first rest => exact ⟨first, rest, chars, by simpa using notDigit, body⟩ + +@[simp] theorem renderable_spellingName (statement : Stmt) : + (Token.identifier (spelling statement).name).Renderable := by + cases statement with + | assign result value => + cases value <;> simp only [spelling] <;> + exact renderable_identifier_of_chars (by decide) (by decide) (by decide) + | _ => + simp only [spelling] + exact renderable_identifier_of_chars (by decide) (by decide) (by decide) + +@[simp] theorem renderable_immediateTokens (program : Program) (statement : Stmt) : + ∀ token ∈ immediateTokens program statement, token.Renderable := by + cases statement with + | assign result value => cases value <;> simp [immediateTokens] + | _ => simp [immediateTokens] + +@[simp] theorem renderable_stmtTokens (program : Program) (statement : Stmt) : + ∀ token ∈ stmtTokens program statement, token.Renderable := by + simp only [stmtTokens, List.forall_mem_append, List.forall_mem_cons, List.forall_mem_map] + exact ⟨renderable_definitionTokens _, renderable_spellingName _, + renderable_immediateTokens _ _, fun _ _ => renderable_variableToken _⟩ + +@[simp] theorem renderable_terminatorTokens (terminator : Terminator) : + ∀ token ∈ terminatorTokens terminator, token.Renderable := by + cases terminator <;> + simp only [terminatorTokens, List.forall_mem_cons] + all_goals repeat' apply And.intro + all_goals first + | exact ⟨_, _, rfl, by decide, by decide⟩ + | simp + +@[simp] theorem renderable_blockTokens (program : Program) (identifier : BlockId) + (block : Block) : + ∀ token ∈ blockTokens program identifier block, token.Renderable := by + rw [blockTokens] + split <;> + simp only [List.forall_mem_append, List.forall_mem_cons, List.forall_mem_flatMap] + all_goals repeat' apply And.intro + all_goals first + | exact renderable_variableTokens _ + | exact renderable_terminatorTokens _ + | simp + all_goals + intro _ _ + exact renderable_stmtTokens _ _ + +@[simp] theorem renderable_functionTokens (program : Program) (identifier : FunctionId) + (function : Function) : + ∀ token ∈ functionTokens program identifier function, token.Renderable := by + simp only [functionTokens, List.forall_mem_append, List.forall_mem_cons, + List.forall_mem_flatMap] + repeat' apply And.intro + all_goals first + | exact ⟨_, _, rfl, by decide, by decide⟩ + | (intro _ _; exact renderable_blockTokens _ _ _) + | simp + +theorem renderable_programTokens (program : Program) : + ∀ token ∈ programTokens program, token.Renderable := by + simp only [programTokens, List.forall_mem_flatMap] + intro _ _ + exact renderable_functionTokens _ _ _ + +namespace Proofs + +theorem tokenize_print (program : Program) : + tokenize (print program) = programTokens program := + tokenize_render (renderable_programTokens program) + +end Proofs +end Sir.Vars.Text diff --git a/sir/Sir/Text/Proofs/References.lean b/sir/Sir/Text/Proofs/References.lean new file mode 100644 index 00000000..6afcdd75 --- /dev/null +++ b/sir/Sir/Text/Proofs/References.lean @@ -0,0 +1,507 @@ +import Sir.Text.Proofs.ParseNormal + +namespace Sir.Vars + +def Stmt.FunctionReferencesInRange (functionCount : Nat) : Stmt → Prop + | .icall callee _ _ => callee.id < functionCount + | _ => True + +def Terminator.BlockReferencesInRange (blockCount : Nat) : Terminator → Prop + | .jump target => target.id < blockCount + | .branch _ thenTarget elseTarget => + thenTarget.id < blockCount ∧ elseTarget.id < blockCount + | _ => True + +def Block.ReferencesInRange (functionCount blockCount : Nat) + (block : Block) : Prop := + (∀ statement ∈ block.statements, + statement.FunctionReferencesInRange functionCount) ∧ + block.terminator.BlockReferencesInRange blockCount + +def Function.ReferencesInRange (functionCount : Nat) (function : Function) : Prop := + ∀ block ∈ function.blocks, + block.ReferencesInRange functionCount function.blocks.size + +def Program.ReferencesInRange (program : Program) : Prop := + ∀ function ∈ program.functions, + function.ReferencesInRange program.functions.size + +end Sir.Vars + +namespace Sir.Vars.Text + +private theorem findIdx?_bound {α : Type} {values : List α} + {predicate : α → Bool} {index : Nat} + (found : values.findIdx? predicate = some index) : + index < values.length := + (List.findIdx?_eq_some_iff_findIdx_eq.mp found).1 + +private theorem run_bind_ok {α β : Type} {action : ParserM α} + {next : α → ParserM β} {initial final : List String} {result : β} + (run : (action >>= next).run initial = .ok (result, final)) : + ∃ value middle, + action.run initial = .ok (value, middle) ∧ + (next value).run middle = .ok (result, final) := by + rw [StateT.run_bind] at run + cases firstRun : action.run initial with + | error message => simp [firstRun, bind, Except.bind] at run + | ok pair => + refine ⟨pair.1, pair.2, by simp only [Prod.eta], ?_⟩ + simpa [firstRun] using run + +private theorem build_functionReferencesInRange {entry : Mnemonic} (member : entry ∈ mnemonics) + (results : Vector VarId entry.results) (operands : Vector VarId entry.operands) + (functionCount : Nat) : + (entry.build results operands).FunctionReferencesInRange functionCount := by + have spelled := spelling_build member results operands + cases built : entry.build results operands with + | icall callee args dests => + rw [built] at spelled + exact ((mnemonic_name member).2 + (by simpa [spelling] using congrArg Spelling.name spelled.symm)).elim + | _ => trivial + +private theorem parseMnemonic_functionReferencesInRange + (functions : List String) (line : Line) (mnemonic : String) + (results : List VarId) (parameters : List Token) + {names finalNames : List String} {statements : List Stmt} + (run : (parseMnemonic functions line mnemonic results parameters).run names = + .ok (statements, finalNames)) : + ∀ statement ∈ statements, + statement.FunctionReferencesInRange functions.length := by + unfold parseMnemonic at run + split at run + · unfold parseInternalCall at run + split at run + all_goals repeat' split at run + all_goals + simp_all [StateT.run, bind, StateT.bind, pure, StateT.pure, Except.bind, + Except.pure, throw, throwThe, MonadExceptOf.throw, StateT.lift, + Stmt.FunctionReferencesInRange] + all_goals grind [findIdx?_bound] + · unfold parseOperation at run + generalize foundEq : mnemonics.find? (·.name == mnemonic) = found at run + cases found with + | none => + simp [StateT.run, throw, throwThe, MonadExceptOf.throw, StateT.lift] at run + | some entry => + have member := List.mem_of_find?_eq_some foundEq + simp only at run + split at run + · obtain ⟨operandResult, operandNames, operandRun, returnRun⟩ := run_bind_ok run + rcases operandResult with ⟨preludes, operandIds⟩ + simp only at returnRun + split at returnRun + · simp [StateT.run, pure, StateT.pure, Except.pure] at returnRun + rcases returnRun with ⟨rfl, rfl⟩ + simpa using build_functionReferencesInRange member _ _ functions.length + · simp [StateT.run, throw, throwThe, MonadExceptOf.throw, StateT.lift] at returnRun + · simp [StateT.run, throw, throwThe, MonadExceptOf.throw, StateT.lift] at run + +private theorem liftNumbers_functionReferencesInRange (functionCount : Nat) + (tokens : List Token) + {names finalNames : List String} {result : List Stmt × List Token} + (run : (liftNumbers tokens).run names = .ok (result, finalNames)) : + ∀ statement ∈ result.1, + statement.FunctionReferencesInRange functionCount := by + induction tokens generalizing names finalNames result with + | nil => + simp [liftNumbers, StateT.run, pure, StateT.pure, Except.pure] at run + rcases run with ⟨rfl, rfl⟩ + simp + | cons token rest induction => + cases token with + | number value => + simp only [liftNumbers] at run + obtain ⟨target, targetNames, targetRun, followingRun⟩ := run_bind_ok run + obtain ⟨following, followingNames, restRun, returnRun⟩ := + run_bind_ok followingRun + have valid := induction restRun + rcases following with ⟨preludes, liftedTokens⟩ + simp [StateT.run, pure, StateT.pure, Except.pure] at returnRun + rcases returnRun with ⟨rfl, rfl⟩ + simpa [Stmt.FunctionReferencesInRange] using valid + | identifier | label | equals | arrow | fatArrow | colon | question | + leftBrace | rightBrace | newline | invalid => + simp only [liftNumbers] at run + obtain ⟨following, followingNames, restRun, returnRun⟩ := run_bind_ok run + have valid := induction restRun + rcases following with ⟨preludes, liftedTokens⟩ + simp [StateT.run, pure, StateT.pure, Except.pure] at returnRun + rcases returnRun with ⟨rfl, rfl⟩ + exact valid + +private theorem parseStatement_functionReferencesInRange + (functions : List String) (line : Line) + {names finalNames : List String} {statements : List Stmt} + (run : (parseStatement functions line).run names = .ok (statements, finalNames)) : + ∀ statement ∈ statements, + statement.FunctionReferencesInRange functions.length := by + unfold parseStatement at run + generalize partsEq : statementParts line = parts at run + rcases parts with ⟨resultTokens, operandTokens⟩ + cases operandTokens with + | nil => + simp [StateT.run, throw, throwThe, MonadExceptOf.throw, StateT.lift] at run + | cons operation parameters => + cases operation with + | identifier mnemonic => + by_cases constant : mnemonic = "const" + · subst mnemonic + simp only at run + obtain ⟨results, resultNames, resultsRun, followingRun⟩ := run_bind_ok run + cases resultListEq : results.toList with + | nil => + simp [resultListEq, StateT.run, throw, throwThe, + MonadExceptOf.throw, StateT.lift] at followingRun + | cons result otherResults => + cases otherResults with + | cons second rest => + simp [resultListEq, StateT.run, throw, throwThe, + MonadExceptOf.throw, StateT.lift] at followingRun + | nil => + cases parameters with + | nil => + simp [resultListEq, StateT.run, throw, throwThe, + MonadExceptOf.throw, StateT.lift] at followingRun + | cons parameter otherParameters => + cases parameter with + | number value => + cases otherParameters with + | cons next rest => + simp [resultListEq, StateT.run, throw, throwThe, + MonadExceptOf.throw, StateT.lift] at followingRun + | nil => + simp [resultListEq, StateT.run, pure, StateT.pure, + Except.pure] at followingRun + rcases followingRun with ⟨rfl, rfl⟩ + simp [Stmt.FunctionReferencesInRange] + | _ => + simp [resultListEq, StateT.run, throw, throwThe, + MonadExceptOf.throw, StateT.lift] at followingRun + · simp only at run + obtain ⟨liftedResult, liftedNames, liftedRun, afterLiftRun⟩ := + run_bind_ok run + rcases liftedResult with ⟨lifted, liftedTokens⟩ + obtain ⟨results, resultNames, resultsRun, bodyRun⟩ := + run_bind_ok afterLiftRun + obtain ⟨body, bodyNames, mnemonicRun, returnRun⟩ := run_bind_ok bodyRun + have liftedValid := + liftNumbers_functionReferencesInRange (functionCount := functions.length) + parameters liftedRun + have bodyValid := parseMnemonic_functionReferencesInRange functions line mnemonic + results.toList liftedTokens mnemonicRun + simp [StateT.run, pure, StateT.pure, Except.pure] at returnRun + rcases returnRun with ⟨rfl, rfl⟩ + simpa using List.forall_mem_append.mpr ⟨liftedValid, bodyValid⟩ + | _ => + simp [StateT.run, throw, throwThe, MonadExceptOf.throw, StateT.lift] at run + +private theorem resolveBlock_bound {blocks : List String} {name : String} + {initial final : List String} {identifier : BlockId} + (run : (resolveBlock blocks name).run initial = .ok (identifier, final)) : + identifier.id < blocks.length := by + unfold resolveBlock at run + generalize foundEq : blocks.findIdx? (· == name) = found at run + cases found with + | none => + simp [StateT.run, bind, Except.bind, throw, throwThe, MonadExceptOf.throw, + StateT.lift] at run + | some index => + simp [StateT.run, pure, StateT.pure, Except.pure] at run + rcases run with ⟨rfl, rfl⟩ + exact findIdx?_bound foundEq + +private theorem parseTerminator_blockReferencesInRange + (blocks : List String) (line : Line) + {names finalNames : List String} {terminator : Terminator} + (run : (parseTerminator blocks line).run names = .ok (terminator, finalNames)) : + terminator.BlockReferencesInRange blocks.length := by + unfold parseTerminator at run + split at run + case h_1 => + simp [StateT.run, pure, StateT.pure, Except.pure] at run + rcases run with ⟨rfl, rfl⟩ + trivial + case h_2 => + simp [StateT.run, pure, StateT.pure, Except.pure] at run + rcases run with ⟨rfl, rfl⟩ + trivial + case h_3 => + obtain ⟨target, targetNames, targetRun, returnRun⟩ := run_bind_ok run + have targetBound := resolveBlock_bound targetRun + simp [StateT.run, pure, StateT.pure, Except.pure] at returnRun + rcases returnRun with ⟨rfl, rfl⟩ + exact targetBound + case h_4 => + obtain ⟨condition, conditionNames, conditionRun, afterConditionRun⟩ := + run_bind_ok run + obtain ⟨thenTarget, thenNames, thenRun, afterThenRun⟩ := + run_bind_ok afterConditionRun + obtain ⟨elseTarget, elseNames, elseRun, returnRun⟩ := run_bind_ok afterThenRun + have thenBound := resolveBlock_bound thenRun + have elseBound := resolveBlock_bound elseRun + simp [StateT.run, pure, StateT.pure, Except.pure] at returnRun + rcases returnRun with ⟨rfl, rfl⟩ + exact ⟨thenBound, elseBound⟩ + case h_5 => + simp [StateT.run, throw, throwThe, MonadExceptOf.throw, StateT.lift] at run + +private theorem parseBlockBody_referencesInRange + (functions blocks : List String) (lines : List Line) + {names finalNames : List String} {body : Array Stmt × Terminator} + (run : (parseBlockBody functions blocks lines).run names = .ok (body, finalNames)) : + (∀ statement ∈ body.1, + statement.FunctionReferencesInRange functions.length) ∧ + body.2.BlockReferencesInRange blocks.length := by + induction lines generalizing names finalNames body with + | nil => + simp [parseBlockBody, StateT.run, throw, throwThe, MonadExceptOf.throw, + StateT.lift] at run + | cons line rest induction => + cases rest with + | nil => + simp only [parseBlockBody] at run + obtain ⟨terminator, terminatorNames, terminatorRun, returnRun⟩ := run_bind_ok run + have terminatorValid := + parseTerminator_blockReferencesInRange blocks line terminatorRun + simp [StateT.run, pure, StateT.pure, Except.pure] at returnRun + rcases returnRun with ⟨rfl, rfl⟩ + exact ⟨by simp, terminatorValid⟩ + | cons next following => + simp only [parseBlockBody] at run + obtain ⟨statements, statementNames, statementRun, followingRun⟩ := + run_bind_ok run + obtain ⟨bodyResult, bodyNames, bodyRun, returnRun⟩ := + run_bind_ok followingRun + have statementsValid := + parseStatement_functionReferencesInRange functions line statementRun + have bodyValid := induction bodyRun + rcases bodyResult with ⟨followingStatements, terminator⟩ + simp [StateT.run, pure, StateT.pure, Except.pure] at returnRun + rcases returnRun with ⟨rfl, rfl⟩ + refine ⟨?_, bodyValid.2⟩ + intro statement member + simp only [Array.mem_append, List.mem_toArray] at member + exact member.elim (statementsValid statement) (bodyValid.1 statement) + +private theorem parseBlock_referencesInRange + (functions blocks : List String) (header : Line) (lines : List Line) + {names finalNames : List String} {block : Block} + (run : (parseBlock functions blocks header lines).run names = + .ok (block, finalNames)) : + block.ReferencesInRange functions.length blocks.length := by + unfold parseBlock at run + obtain ⟨headerResult, headerNames, headerRun, bodyFollowingRun⟩ := run_bind_ok run + obtain ⟨bodyResult, bodyNames, bodyRun, returnRun⟩ := run_bind_ok bodyFollowingRun + rcases headerResult with ⟨inputs, outputs⟩ + rcases bodyResult with ⟨statements, terminator⟩ + have bodyValid := parseBlockBody_referencesInRange functions blocks lines bodyRun + simp [StateT.run, pure, StateT.pure, Except.pure] at returnRun + rcases returnRun with ⟨rfl, rfl⟩ + exact bodyValid + +private theorem except_mapM_length {α β ε : Type} (action : α → Except ε β) : + ∀ {values : List α} {results : List β}, + values.mapM action = .ok results → results.length = values.length := by + intro values + induction values with + | nil => + intro results run + simp [pure, Except.pure] at run + rcases run with rfl + rfl + | cons value following induction => + intro results run + simp only [List.mapM_cons, bind, Except.bind] at run + cases actionRun : action value with + | error message => simp [actionRun] at run + | ok result => + simp only [actionRun] at run + cases followingRun : following.mapM action with + | error message => simp [followingRun] at run + | ok followingResults => + simp [followingRun, pure, Except.pure] at run + rcases run with rfl + simp [induction followingRun] + +private theorem mapM_parseBlock_referencesInRange + (functions blocks : List String) (groups : List (Line × List Line)) + {names finalNames : List String} {parsed : List Block} + (run : (groups.mapM fun group => + parseBlock functions blocks group.fst group.snd).run names = + .ok (parsed, finalNames)) : + parsed.length = groups.length ∧ + ∀ block ∈ parsed, + block.ReferencesInRange functions.length blocks.length := by + induction groups generalizing names finalNames parsed with + | nil => + simp [StateT.run, pure, StateT.pure, Except.pure] at run + rcases run with ⟨rfl, rfl⟩ + simp + | cons group rest induction => + simp only [List.mapM_cons] at run + obtain ⟨block, blockNames, blockRun, restFollowingRun⟩ := run_bind_ok run + obtain ⟨following, followingNames, restRun, returnRun⟩ := + run_bind_ok restFollowingRun + have blockValid := parseBlock_referencesInRange functions blocks + group.fst group.snd blockRun + have followingValid := induction restRun + simp [StateT.run, pure, StateT.pure, Except.pure] at returnRun + rcases returnRun with ⟨rfl, rfl⟩ + refine ⟨by simp [followingValid.1], ?_⟩ + intro candidate member + rcases List.mem_cons.mp member with rfl | followingMember + · exact blockValid + · exact followingValid.2 candidate followingMember + +private theorem parseFunction_referencesInRange (functions : List String) (body : List Line) + {names finalNames : List String} {function : Function} + (run : (parseFunction functions body).run names = .ok (function, finalNames)) : + function.ReferencesInRange functions.length := by + unfold parseFunction at run + generalize groupsEq : splitBlocks body = groupsResult at run + cases groupsResult with + | error message => + simp [StateT.run, bind, Except.bind, throw, throwThe, MonadExceptOf.throw, + StateT.lift] at run + | ok groups => + unfold parseFunctionGroups at run + simp [StateT.run, bind, StateT.bind, liftM, monadLift, MonadLift.monadLift, + StateT.lift, Except.bind] at run + generalize blocksEq : groups.mapM (fun group => blockHeaderName group.fst) = + blocksResult at run + cases blocksResult with + | error message => simp at run + | ok blockNames => + by_cases duplicates : hasDuplicates blockNames + · simp [duplicates, bind, StateT.bind, pure, Except.pure, Except.bind, throw, throwThe, + MonadExceptOf.throw, StateT.lift] at run + · simp [duplicates, bind, StateT.bind, pure, StateT.pure, Except.pure, + Except.bind] at run + generalize parsedEq : + (groups.mapM fun group => parseBlock functions blockNames group.fst group.snd) + names = parsedResult + rw [parsedEq] at run + cases parsedResult with + | error message => contradiction + | ok result => + rcases result with ⟨parsed, parsedNames⟩ + have blockNamesLength := except_mapM_length + (fun group : Line × List Line => blockHeaderName group.fst) blocksEq + have parsedValid := mapM_parseBlock_referencesInRange + functions blockNames groups parsedEq + cases parsed with + | nil => + simp [throw, throwThe, MonadExceptOf.throw, StateT.lift] at run + | cons entry rest => + change Except.ok + ({ entry := entry, rest := rest.toArray }, parsedNames) = + Except.ok (function, finalNames) at run + simp only [Except.ok.injEq, Prod.mk.injEq] at run + rcases run with ⟨rfl, rfl⟩ + intro block member + have blockValid := parsedValid.2 block + (by simpa [Function.blocks] using member) + simpa [Function.blocks, parsedValid.1, blockNamesLength] using blockValid + +private theorem mapM_parseFunction_referencesInRange + (names : List String) (groups : List (String × List Line)) + {stateNames finalNames : List String} {functions : List Function} + (run : (parseFunctionGroupsList names groups).run stateNames = + .ok (functions, finalNames)) : + functions.length = groups.length ∧ + ∀ function ∈ functions, function.ReferencesInRange names.length := by + induction groups generalizing stateNames finalNames functions with + | nil => + simp [parseFunctionGroupsList, StateT.run, pure, StateT.pure, Except.pure] at run + rcases run with ⟨rfl, rfl⟩ + simp + | cons group rest induction => + simp only [parseFunctionGroupsList, List.mapM_cons] at run + obtain ⟨function, functionNames, functionRun, restFollowingRun⟩ := run_bind_ok run + obtain ⟨following, followingNames, restRun, returnRun⟩ := + run_bind_ok restFollowingRun + have functionValid := parseFunction_referencesInRange names group.snd functionRun + have followingValid := induction restRun + simp [StateT.run, pure, StateT.pure, Except.pure] at returnRun + rcases returnRun with ⟨rfl, rfl⟩ + refine ⟨by simp [followingValid.1], ?_⟩ + intro candidate member + rcases List.mem_cons.mp member with rfl | followingMember + · exact functionValid + · exact followingValid.2 candidate followingMember + +private theorem parseFunctionSlots_referencesInRange (names : List String) + (initGroup : String × List Line) (following : List (String × List Line)) + {stateNames finalNames : List String} {slots : Function × List Function} + (run : (parseFunctionSlots names initGroup following).run stateNames = + .ok (slots, finalNames)) : + slots.2.length = following.length ∧ + ∀ function ∈ slots.1 :: slots.2, function.ReferencesInRange names.length := by + unfold parseFunctionSlots at run + obtain ⟨init, initNames, initRun, followingRun⟩ := run_bind_ok run + obtain ⟨parsed, parsedNames, parsedRun, returnRun⟩ := run_bind_ok followingRun + have initValid := parseFunction_referencesInRange names initGroup.snd initRun + have followingValid := mapM_parseFunction_referencesInRange names following parsedRun + simp [StateT.run, pure, StateT.pure, Except.pure] at returnRun + rcases returnRun with ⟨rfl, rfl⟩ + refine ⟨followingValid.1, ?_⟩ + intro function member + rcases List.mem_cons.mp member with rfl | followingMember + · exact initValid + · exact followingValid.2 function followingMember + +private theorem parseProgramSlots_referencesInRange {initGroup : String × List Line} + {mainGroup : Option (String × List Line)} {others : List (String × List Line)} + {program : Program} + (parsed : parseProgramSlots initGroup mainGroup others = .ok program) : + program.ReferencesInRange := by + unfold parseProgramSlots at parsed + simp only [] at parsed + split at parsed + · simp at parsed + · rename_i result slotsEq + rcases result with ⟨slots, slotNames⟩ + simp only [Except.ok.injEq] at parsed + subst program + have valid := parseFunctionSlots_referencesInRange _ initGroup _ slotsEq + have sizeEq : (programOfSlots mainGroup.isSome slots.1 slots.2).functions.size = + (initGroup.fst :: (mainGroup.toList ++ others).map Prod.fst).length := by + simp [programOfSlots_functions, valid.1] + intro function member + rw [sizeEq] + exact valid.2 function (by simpa [programOfSlots_functions] using member) + +private theorem parseProgramGroups_referencesInRange {groups : List (String × List Line)} + {program : Program} (parsed : parseProgramGroups groups = .ok program) : + program.ReferencesInRange := by + unfold parseProgramGroups at parsed + by_cases duplicates : hasDuplicates (groups.map Prod.fst) + · simp [duplicates, bind, Except.bind] at parsed + · simp only [duplicates, Bool.false_eq_true, if_false, bind, Except.bind, pure, + Except.pure] at parsed + cases initEq : groups.find? (fun group => group.fst == "init") with + | none => + rw [initEq] at parsed + simp at parsed + | some initGroup => + rw [initEq] at parsed + exact parseProgramSlots_referencesInRange parsed + +private theorem parseTokens_referencesInRange {tokens : List Token} {program : Program} + (parsed : parseTokens tokens = .ok program) : program.ReferencesInRange := by + unfold parseTokens at parsed + generalize splitEq : splitFunctions (splitLines tokens) = groupsResult at parsed + cases groupsResult with + | error message => contradiction + | ok groups => exact parseProgramGroups_referencesInRange parsed + +namespace Proofs + +theorem parse_referencesInRange {source : String} {program : Program} + (parsed : parse source = .ok program) : program.ReferencesInRange := + parseTokens_referencesInRange parsed + +end Proofs +end Sir.Vars.Text diff --git a/sir/Sir/Text/Proofs/RoundTrip.lean b/sir/Sir/Text/Proofs/RoundTrip.lean new file mode 100644 index 00000000..bd3a7b13 --- /dev/null +++ b/sir/Sir/Text/Proofs/RoundTrip.lean @@ -0,0 +1,1774 @@ +import Sir.Text.Proofs.Printer +import Sir.Text.Proofs.References + +namespace Sir.Vars.Text + +private def lineTokens (lines : List Line) : List Token := + lines.flatMap fun line => line ++ [.newline] + +private def blockLines (program : Program) (identifier : BlockId) + (block : Block) : List Line := + ([.identifier (blockName identifier)] ++ variableTokens block.inputs ++ + (if block.outputs.isEmpty then [] else .arrow :: variableTokens block.outputs) ++ + [.leftBrace]) :: + block.statements.toList.map (stmtTokens program) ++ + [terminatorTokens block.terminator, [.rightBrace]] + +private def functionLines (program : Program) (identifier : FunctionId) + (function : Function) : List Line := + [.identifier "fn", .identifier (functionName program identifier), .colon] :: + (function.blocks.toList.zipIdx.flatMap fun (block, index) => + blockLines program ⟨index⟩ block) + +private def programLines (program : Program) : List Line := + program.functions.toList.zipIdx.flatMap fun (function, index) => + functionLines program ⟨index⟩ function + +private def functionBodyLines (program : Program) (function : Function) : List Line := + function.blocks.toList.zipIdx.flatMap fun (block, index) => + blockLines program ⟨index⟩ block + +private def printedFunctionGroups (program : Program) : List (String × List Line) := + program.functions.toList.zipIdx.map fun (function, index) => + (functionName program ⟨index⟩, functionBodyLines program function) + +private def printedFunctionNames (program : Program) : List String := + (printedFunctionGroups program).map Prod.fst + +private theorem blockTokens_eq_lineTokens (program : Program) (identifier : BlockId) + (block : Block) : + blockTokens program identifier block = lineTokens (blockLines program identifier block) := by + simp [blockTokens, blockLines, lineTokens, List.flatMap_append, List.flatMap_map] + +private theorem lineTokens_append (first second : List Line) : + lineTokens (first ++ second) = lineTokens first ++ lineTokens second := by + simp [lineTokens, List.flatMap_append] + +private theorem lineTokens_flatMap {α : Type} (values : List α) (lines : α → List Line) : + lineTokens (values.flatMap lines) = + values.flatMap fun value => lineTokens (lines value) := by + induction values with + | nil => rfl + | cons value following induction => + simp only [List.flatMap_cons, lineTokens_append, induction] + +private theorem functionTokens_eq_lineTokens (program : Program) (identifier : FunctionId) + (function : Function) : + functionTokens program identifier function = + lineTokens (functionLines program identifier function) := by + rw [functionTokens, functionLines] + simp only [lineTokens, List.flatMap_cons] + rw [show List.flatMap (fun line => line ++ [Token.newline]) + (List.flatMap + (fun x => blockLines program { id := x.2 } x.1) + function.blocks.toList.zipIdx) = + lineTokens (List.flatMap + (fun x => blockLines program { id := x.2 } x.1) + function.blocks.toList.zipIdx) by rfl] + rw [lineTokens_flatMap] + congr 1 + apply List.flatMap_congr + intro pair member + rcases pair with ⟨block, index⟩ + exact blockTokens_eq_lineTokens program ⟨index⟩ block + +private theorem programTokens_eq_lineTokens (program : Program) : + programTokens program = lineTokens (programLines program) := by + rw [programTokens, programLines, lineTokens_flatMap] + apply List.flatMap_congr + intro pair member + rcases pair with ⟨function, index⟩ + exact functionTokens_eq_lineTokens program ⟨index⟩ function + +private theorem splitLinesAux_append_line (current line rest : List Token) + (currentNe : current ≠ []) (noNewline : .newline ∉ line) : + splitLinesAux current (line ++ .newline :: rest) = + (current.reverse ++ line) :: splitLinesAux [] rest := by + induction line generalizing current with + | nil => simp [splitLinesAux, currentNe] + | cons token following induction => + have tokenNe : token ≠ .newline := by + intro equality + subst token + exact noNewline (by simp) + rw [List.cons_append] + simp [splitLinesAux] + rw [induction (token :: current) (by simp)] + · simp + · intro member + exact noNewline (List.mem_cons_of_mem token member) + +private theorem splitLines_lineTokens (lines : List Line) + (nonempty : ∀ line ∈ lines, line ≠ []) + (noNewline : ∀ line ∈ lines, Token.newline ∉ line) : + splitLines (lineTokens lines) = lines := by + induction lines with + | nil => rfl + | cons line following induction => + rw [splitLines] + rw [lineTokens, List.flatMap_cons] + rw [show line ++ [.newline] ++ + List.flatMap (fun line => line ++ [.newline]) following = + line ++ .newline :: List.flatMap (fun line => line ++ [.newline]) following by + simp] + cases line with + | nil => exact False.elim (nonempty [] (by simp) rfl) + | cons token rest => + have tokenNe : token ≠ .newline := by + intro equality + subst token + exact noNewline (.newline :: rest) (by simp) (by simp) + simp only [List.cons_append] + simp [splitLinesAux] + rw [splitLinesAux_append_line [token] rest + (List.flatMap (fun line => line ++ [Token.newline]) following) + (by simp) (by + intro member + exact noNewline (token :: rest) (by simp) (by simp [member]))] + simp only [List.reverse_singleton, List.singleton_append] + rw [← splitLines] + exact congrArg (List.cons (token :: rest)) + (induction (fun line member => nonempty line (by simp [member])) + (fun line member => noNewline line (by simp [member]))) + +private theorem spelling_name_ne_fn (statement : Stmt) : (spelling statement).name ≠ "fn" := by + cases statement with + | assign _ value => cases value <;> simp [spelling] + | _ => simp [spelling] + +private theorem stmtTokens_head (program : Program) (statement : Stmt) : + (∃ identifier rest, stmtTokens program statement = variableToken identifier :: rest) ∨ + ∃ rest, + stmtTokens program statement = Token.identifier (spelling statement).name :: rest := by + rw [stmtTokens, definitionTokens] + split + · exact .inr ⟨_, rfl⟩ + · rename_i nonempty + cases results : (spelling statement).results with + | nil => simp [results] at nonempty + | cons identifier following => + refine .inl ⟨identifier, List.map variableToken following ++ [Token.equals] ++ + Token.identifier (spelling statement).name :: + (immediateTokens program statement ++ + List.map variableToken (spelling statement).operands), ?_⟩ + simp + +private theorem stmtTokens_noNewline (program : Program) (statement : Stmt) : + Token.newline ∉ stmtTokens program statement := by + cases statement with + | assign _ value => + cases value <;> simp [stmtTokens, spelling, immediateTokens, definitionTokens, variableToken] + | _ => simp [stmtTokens, spelling, immediateTokens, definitionTokens, variableToken] + +private theorem programLines_nonempty (program : Program) : + ∀ line ∈ programLines program, line ≠ [] := by + intro line member + simp only [programLines, List.mem_flatMap] at member + rcases member with ⟨pair, _, member⟩ + rcases pair with ⟨function, index⟩ + simp only [functionLines, List.mem_cons, List.mem_flatMap] at member + rcases member with rfl | ⟨pair, _, member⟩ + · simp + rcases pair with ⟨block, blockIndex⟩ + simp only [blockLines, List.mem_cons, List.mem_append, List.mem_map] at member + rcases member with (rfl | ⟨statement, _, rfl⟩) | following + · simp + · simp [stmtTokens] + rcases following with rfl | following + · cases block.terminator <;> simp [terminatorTokens] + rcases following with rfl | impossible + · simp + · simp at impossible + +private theorem programLines_noNewline (program : Program) : + ∀ line ∈ programLines program, Token.newline ∉ line := by + intro line member + simp only [programLines, List.mem_flatMap] at member + rcases member with ⟨pair, _, member⟩ + rcases pair with ⟨function, index⟩ + simp only [functionLines, List.mem_cons, List.mem_flatMap] at member + rcases member with rfl | ⟨pair, _, member⟩ + · simp + rcases pair with ⟨block, blockIndex⟩ + simp only [blockLines, List.mem_cons, List.mem_append, List.mem_map] at member + rcases member with (rfl | ⟨statement, _, rfl⟩) | following + · simp [variableTokens, variableToken] + · exact stmtTokens_noNewline program statement + rcases following with rfl | following + · cases block.terminator <;> + simp [terminatorTokens, variableToken] + rcases following with rfl | impossible + · simp + · simp at impossible + +private theorem splitLines_programTokens (program : Program) : + splitLines (programTokens program) = programLines program := by + rw [programTokens_eq_lineTokens] + exact splitLines_lineTokens _ (programLines_nonempty program) + (programLines_noNewline program) + +@[simp] private theorem blockName_ne_fn (identifier : BlockId) : + blockName identifier ≠ "fn" := by + intro equality + have characters := congrArg String.toList equality + simp [blockName, String.toList_append] at characters + +@[simp] private theorem variableName_ne_fn (identifier : VarId) : + variableName identifier ≠ "fn" := by + intro equality + have characters := congrArg String.toList equality + simp [variableName, String.toList_append] at characters + +private theorem functionBodyLines_not_header (program : Program) (function : Function) : + ∀ line ∈ functionBodyLines program function, + ∀ name, line ≠ [.identifier "fn", .identifier name, .colon] := by + intro line member name + simp only [functionBodyLines, List.mem_flatMap] at member + rcases member with ⟨pair, _, member⟩ + rcases pair with ⟨block, blockIndex⟩ + simp only [blockLines, List.mem_cons, List.mem_append, List.mem_map] at member + rcases member with (lineEq | ⟨statement, _, lineEq⟩) | following + · subst line + simp + · subst line + rcases stmtTokens_head program statement with + ⟨identifier, rest, lineEq⟩ | ⟨rest, lineEq⟩ <;> + simp [lineEq, variableToken, spelling_name_ne_fn] + rcases following with lineEq | following + · subst line + cases block.terminator <;> simp [terminatorTokens] + rcases following with lineEq | impossible + · subst line + simp + · simp at impossible + +private theorem splitFunctionsAux_body (groups : List (String × List Line)) + (name : String) (accumulated body rest : List Line) + (notHeader : ∀ line ∈ body, + ∀ functionName, line ≠ [.identifier "fn", .identifier functionName, .colon]) : + splitFunctionsAux ((name, accumulated) :: groups) (body ++ rest) = + splitFunctionsAux ((name, body.reverse ++ accumulated) :: groups) rest := by + induction body generalizing accumulated with + | nil => rfl + | cons line following induction => + rw [List.cons_append] + rw [splitFunctionsAux] + · rw [induction (line :: accumulated)] + · simp + · intro next member functionName equality + exact notHeader next (by simp [member]) functionName equality + · exact notHeader line (by simp) + +private theorem splitFunctionsAux_programLines (program : Program) + (groupsPrefix : List (String × List Line)) : + splitFunctionsAux groupsPrefix (programLines program) = + .ok (groupsPrefix.reverse.map (fun group => (group.fst, group.snd.reverse)) ++ + printedFunctionGroups program) := by + rw [programLines, printedFunctionGroups] + generalize valuesEq : program.functions.toList.zipIdx = values + clear valuesEq + induction values generalizing groupsPrefix with + | nil => simp [splitFunctionsAux] + | cons pair following induction => + rcases pair with ⟨function, index⟩ + simp only [List.flatMap_cons, List.map_cons, functionLines] + rw [splitFunctionsAux.eq_def] + change splitFunctionsAux ((functionName program ⟨index⟩, []) :: groupsPrefix) + (functionBodyLines program function ++ + List.flatMap (fun x => functionLines program { id := x.2 } x.1) following) = _ + rw [splitFunctionsAux_body groupsPrefix (functionName program ⟨index⟩) [] + (functionBodyLines program function) + (List.flatMap (fun x => functionLines program { id := x.2 } x.1) following) + (functionBodyLines_not_header program function)] + rw [induction] + simp + +private theorem splitFunctions_programLines (program : Program) : + splitFunctions (programLines program) = .ok (printedFunctionGroups program) := by + rw [splitFunctions, splitFunctionsAux_programLines] + rfl + +@[simp] private theorem decimalString_inj {left right : Nat} : + decimalString left = decimalString right ↔ left = right := by + constructor + · intro equality + have characters := congrArg String.toList equality + rw [toList_decimalString, toList_decimalString] at characters + have values := congrArg (digitsValue 10) characters + simpa [digitsValue_decimalDigits] using values + · exact congrArg decimalString + +@[simp] private theorem fn_decimal_inj {left right : Nat} : + "fn" ++ decimalString left = "fn" ++ decimalString right ↔ left = right := by + constructor + · intro equality + have characters := congrArg String.toList equality + rw [String.toList_append, String.toList_append] at characters + have digits := List.append_cancel_left characters + rw [toList_decimalString, toList_decimalString] at digits + have values := congrArg (digitsValue 10) digits + simpa [digitsValue_decimalDigits] using values + · exact fun equality => congrArg _ (congrArg decimalString equality) + +@[simp] private theorem fn_decimal_ne_init (identifier : Nat) : + "fn" ++ decimalString identifier ≠ "init" := by + intro equality + have characters := congrArg String.toList equality + simp [String.toList_append] at characters + +@[simp] private theorem fn_decimal_ne_main (identifier : Nat) : + "fn" ++ decimalString identifier ≠ "main" := by + intro equality + have characters := congrArg String.toList equality + simp [String.toList_append] at characters + +@[simp] private theorem init_ne_fn_decimal (identifier : Nat) : + "init" ≠ "fn" ++ decimalString identifier := + Ne.symm (fn_decimal_ne_init identifier) + +@[simp] private theorem main_ne_fn_decimal (identifier : Nat) : + "main" ≠ "fn" ++ decimalString identifier := + Ne.symm (fn_decimal_ne_main identifier) + +private theorem functionName_cases (program : Program) (identifier : FunctionId) : + (functionName program identifier = "init" ∧ identifier.id = 0) ∨ + (functionName program identifier = "main" ∧ identifier.id = 1) ∨ + functionName program identifier = "fn" ++ decimalString identifier.id := by + by_cases isInit : identifier = program.initId + · exact Or.inl ⟨by simp [functionName, isInit], by simp [isInit, Program.initId]⟩ + · by_cases isMain : program.mainId? = some identifier + · refine Or.inr (Or.inl ⟨by simp [functionName, isInit, isMain], ?_⟩) + simp only [Program.mainId?, Option.map_eq_some_iff] at isMain + obtain ⟨_, _, identity⟩ := isMain + exact congrArg FunctionId.id identity.symm + · exact Or.inr (Or.inr (by simp [functionName, isInit, isMain])) + +private theorem functionName_injective {program : Program} {left right : FunctionId} + (equality : functionName program left = functionName program right) : + left = right := by + rcases left with ⟨left⟩ + rcases right with ⟨right⟩ + apply congrArg FunctionId.mk + rcases functionName_cases program ⟨left⟩ with ⟨leftName, leftId⟩ | ⟨leftName, leftId⟩ | + leftName <;> + rcases functionName_cases program ⟨right⟩ with ⟨rightName, rightId⟩ | + ⟨rightName, rightId⟩ | rightName <;> + rw [leftName, rightName] at equality <;> simp_all + +private theorem printedFunctionNames_eq (program : Program) : + printedFunctionNames program = + program.functions.toList.zipIdx.map fun pair => + functionName program ⟨pair.2⟩ := by + simp [printedFunctionNames, printedFunctionGroups, Function.comp_def] + +private theorem printedFunctionNames_length (program : Program) : + (printedFunctionNames program).length = program.functions.size := by + simp [printedFunctionNames_eq] + +private theorem printedFunctionNames_getElem (program : Program) (index : Nat) + (bound : index < (printedFunctionNames program).length) : + (printedFunctionNames program)[index] = functionName program ⟨index⟩ := by + simp [printedFunctionNames, printedFunctionGroups] + +private theorem printedFunctionNames_findIdx (program : Program) + (identifier : FunctionId) (bound : identifier.id < program.functions.size) : + (printedFunctionNames program).findIdx? (· == functionName program identifier) = + some identifier.id := by + rw [List.findIdx?_eq_some_iff_findIdx_eq] + have listBound : identifier.id < (printedFunctionNames program).length := by + simpa [printedFunctionNames_length] using bound + refine ⟨listBound, (List.findIdx_eq listBound).2 ⟨?_, ?_⟩⟩ + · simp [printedFunctionNames_getElem] + · intro index indexBound + simp only [beq_eq_false_iff_ne] + intro equality + have nameEquality : functionName program ⟨index⟩ = + functionName program identifier := by + rw [← printedFunctionNames_getElem program index (by omega)] + exact equality + have identifiersEqual : (⟨index⟩ : FunctionId) = identifier := + functionName_injective nameEquality + exact Nat.ne_of_lt indexBound (congrArg FunctionId.id identifiersEqual) + +private def printedVariableNames (identifiers : List VarId) : List String := + identifiers.eraseDups.map variableName + +@[simp] private theorem variableName_inj {left right : VarId} : + variableName left = variableName right ↔ left = right := by + rcases left with ⟨left⟩ + rcases right with ⟨right⟩ + simp [variableName] + +private theorem printedVariableNames_findIdx (identifiers : List VarId) + (identifier : VarId) : + (printedVariableNames identifiers).findIdx? (· == variableName identifier) = + identifiers.eraseDups.idxOf? identifier := by + rw [printedVariableNames, List.findIdx?_map] + apply congrArg (fun predicate => identifiers.eraseDups.findIdx? predicate) + funext other + simp + +private theorem singleton_removeAll_eq_nil {identifier : VarId} {identifiers : List VarId} + (member : identifier ∈ identifiers) : + [identifier].removeAll identifiers = [] := by + induction identifiers with + | nil => simp at member + | cons head tail induction => + by_cases equal : identifier = head + · subst head + simp [List.removeAll_cons] + · have tailMember : identifier ∈ tail := by simpa [equal] using member + simpa [List.removeAll_cons, equal] using induction tailMember + +private theorem singleton_removeAll_eq_self {identifier : VarId} {identifiers : List VarId} + (notMember : identifier ∉ identifiers) : + [identifier].removeAll identifiers = [identifier] := by + induction identifiers with + | nil => rfl + | cons head tail induction => + have unequal : identifier ≠ head := by + intro equality + exact notMember (by simp [equality]) + have tailNotMember : identifier ∉ tail := by + intro member + exact notMember (by simp [member]) + simpa [List.removeAll_cons, unequal] using induction tailNotMember + +private theorem internVariable_printed (prior : List VarId) (identifier : VarId) : + (internVariable (variableName identifier)).run (printedVariableNames prior) = + .ok (⟨prior.eraseDups.idxOf identifier⟩, + printedVariableNames (prior ++ [identifier])) := by + simp only [internVariable, StateT.run, bind, StateT.bind, get, getThe, MonadStateOf.get, + StateT.get, set, pure, Except.pure, Except.bind] + rw [printedVariableNames_findIdx] + by_cases member : identifier ∈ prior + · have eraseMember : identifier ∈ prior.eraseDups := + List.mem_eraseDups.mpr member + have indexBound := List.idxOf_lt_length_of_mem eraseMember + have found : prior.eraseDups.idxOf? identifier = + some (prior.eraseDups.idxOf identifier) := by + rw [List.idxOf?, List.findIdx?_eq_some_iff_findIdx_eq] + exact ⟨indexBound, rfl⟩ + rw [found] + rw [show printedVariableNames (prior ++ [identifier]) = + printedVariableNames prior by + simp [printedVariableNames, List.eraseDups_append, + singleton_removeAll_eq_nil member]] + simp [pure, StateT.pure, Except.pure] + · have eraseNotMember : identifier ∉ prior.eraseDups := by + simpa using member + rw [List.idxOf?_eq_none_iff.mpr eraseNotMember] + rw [show printedVariableNames (prior ++ [identifier]) = + printedVariableNames prior ++ [variableName identifier] by + rw [printedVariableNames, List.eraseDups_append, + singleton_removeAll_eq_self member] + simp only [List.eraseDups_cons, List.filter_nil, List.eraseDups_nil, + List.map_append, List.map_singleton] + rfl] + simp [bind, StateT.bind, StateT.set, pure, StateT.pure, Except.pure, Except.bind, + printedVariableNames, List.idxOf_eq_length eraseNotMember] + +private theorem eraseDups_idxOf_of_prefix {listPrefix full : List VarId} + {identifier : VarId} (isPrefix : listPrefix <+: full) + (member : identifier ∈ listPrefix) : + full.eraseDups.idxOf identifier = listPrefix.eraseDups.idxOf identifier := by + rcases isPrefix with ⟨suffix, rfl⟩ + rw [List.eraseDups_append, List.idxOf_append] + simp [List.mem_eraseDups.mpr member] + +private theorem eraseDups_idxOf_append_self (prior : List VarId) (identifier : VarId) : + (prior ++ [identifier]).eraseDups.idxOf identifier = + prior.eraseDups.idxOf identifier := by + by_cases member : identifier ∈ prior + · rw [List.eraseDups_append, singleton_removeAll_eq_nil member] + simp + · have eraseNotMember : identifier ∉ prior.eraseDups := by simpa using member + rw [List.eraseDups_append, singleton_removeAll_eq_self member, + List.eraseDups_cons] + simp [List.idxOf_append, eraseNotMember] + +private theorem internVariable_normal (full prior : List VarId) (identifier : VarId) + (isPrefix : prior ++ [identifier] <+: full) : + (internVariable (variableName identifier)).run (printedVariableNames prior) = + .ok (⟨full.eraseDups.idxOf identifier⟩, + printedVariableNames (prior ++ [identifier])) := by + rw [internVariable_printed] + rw [eraseDups_idxOf_of_prefix (identifier := identifier) isPrefix (by simp), + eraseDups_idxOf_append_self] + +private theorem variableList_printed (full prior identifiers : List VarId) + (isPrefix : prior ++ identifiers <+: full) : + (variableList (identifiers.map variableToken)).run (printedVariableNames prior) = + .ok ((identifiers.map fun identifier => + (⟨full.eraseDups.idxOf identifier⟩ : VarId)).toArray, + printedVariableNames (prior ++ identifiers)) := by + induction identifiers generalizing prior with + | nil => + simp [variableList, StateT.run, pure, StateT.pure, Except.pure] + | cons identifier following induction => + simp only [List.map_cons, variableToken, variableList] + simp only [StateT.run, bind, StateT.bind, Except.bind] + have headPrefix : prior ++ [identifier] <+: full := + (show prior ++ [identifier] <+: prior ++ identifier :: following from + ⟨following, by simp⟩).trans isPrefix + rw [show internVariable (variableName identifier) + (printedVariableNames prior) = + .ok (⟨full.eraseDups.idxOf identifier⟩, + printedVariableNames (prior ++ [identifier])) from + internVariable_normal full prior identifier headPrefix] + simp only [pure, StateT.pure, Except.pure] + have tailPrefix : (prior ++ [identifier]) ++ following <+: full := by + simpa [List.append_assoc] using isPrefix + rw [show variableList (following.map variableToken) + (printedVariableNames (prior ++ [identifier])) = + .ok ((following.map fun identifier => + (⟨full.eraseDups.idxOf identifier⟩ : VarId)).toArray, + printedVariableNames ((prior ++ [identifier]) ++ following)) from + induction (prior ++ [identifier]) tailPrefix] + simp [List.append_assoc] + +private def normalRename (full : List VarId) (identifier : VarId) : VarId := + ⟨full.eraseDups.idxOf identifier⟩ + +@[simp] private theorem identifier_ne_equals (name : String) : + (Token.identifier name != Token.equals) = true := by + rfl + +@[simp] private theorem label_ne_equals (name : String) : + (Token.label name != Token.equals) = true := by + rfl + +private theorem span_variableTokens_end_aux (identifiers : List VarId) + (accumulated : List Token) : + List.span.loop (· != Token.equals) (identifiers.map variableToken) accumulated = + (accumulated.reverse ++ identifiers.map variableToken, []) := by + induction identifiers generalizing accumulated with + | nil => simp [List.span.loop] + | cons identifier following induction => + simp only [List.map_cons, variableToken, List.span.loop, identifier_ne_equals] + rw [induction (Token.identifier (variableName identifier) :: accumulated)] + simp + +private theorem span_variableTokens_equals_aux (identifiers : List VarId) + (rest accumulated : List Token) : + List.span.loop (· != Token.equals) + (identifiers.map variableToken ++ Token.equals :: rest) accumulated = + (accumulated.reverse ++ identifiers.map variableToken, Token.equals :: rest) := by + induction identifiers generalizing accumulated with + | nil => simp [List.span.loop] + | cons identifier following induction => + simp only [List.map_cons, List.cons_append, variableToken, List.span.loop, + identifier_ne_equals] + rw [induction (Token.identifier (variableName identifier) :: accumulated)] + simp + +private theorem span_variableTokens_equals (identifiers : List VarId) (rest : List Token) : + (identifiers.map variableToken ++ Token.equals :: rest).span (· != Token.equals) = + (identifiers.map variableToken, Token.equals :: rest) := by + simpa [List.span] using span_variableTokens_equals_aux identifiers rest [] + +private theorem statementParts_icall_no_results (name : String) (args : List VarId) : + statementParts + (Token.identifier "icall" :: Token.label name :: args.map variableToken) = + ([], Token.identifier "icall" :: Token.label name :: args.map variableToken) := by + rw [statementParts] + simp only [List.span, List.span.loop, identifier_ne_equals, label_ne_equals] + rw [span_variableTokens_end_aux args [Token.label name, Token.identifier "icall"]] + +private theorem statementParts_results (results : List VarId) (rest : List Token) : + statementParts (results.map variableToken ++ Token.equals :: rest) = + (results.map variableToken, rest) := by + rw [statementParts, span_variableTokens_equals] + +@[simp] private theorem word_ofNat_toNat (value : Word) : + (.ofNat value.toNat : Word) = value := by + calc + (.ofNat value.toNat : Word) = + Evm.UInt256.ofBitVec (BitVec.ofNat 256 value.toNat) := by + have bound : value.toNat < 2 ^ 256 := value.toBitVec.isLt + simp only [Evm.UInt256.ofNat, Evm.UInt256.ofBitVec, Evm.UInt256.mk.injEq] + repeat' apply And.intro + all_goals apply UInt32.toBitVec_inj.mp + all_goals + simp only [UInt32.toBitVec_ofNat', BitVec.extractLsb', BitVec.toNat_ofNat] + norm_num at bound ⊢ + rw [Nat.mod_eq_of_lt bound] + _ = Evm.UInt256.ofBitVec value.toBitVec := by + change Evm.UInt256.ofBitVec (BitVec.ofNat 256 value.toBitVec.toNat) = _ + rw [BitVec.ofNat_toNat] + simp + _ = value := Evm.UInt256.ofBitVec_toBitVec value + +private theorem parseStatement_assign_constant (program : Program) (functions : List String) + (full prior : List VarId) (result : VarId) (value : Word) + (isPrefix : prior ++ [result] <+: full) : + (parseStatement functions + (stmtTokens program (.assign result (.constant value)))).run (printedVariableNames prior) = + .ok ([.assign (normalRename full result) (.constant value)], + printedVariableNames (prior ++ [result])) := by + simp [stmtTokens, definitionTokens, spelling, immediateTokens, parseStatement, + statementParts, variableToken, List.span, List.span.loop] + simp only [StateT.run, bind, Except.bind] + rw [show variableList [Token.identifier (variableName result)] + (printedVariableNames prior) = + .ok (#[normalRename full result], printedVariableNames (prior ++ [result])) from by + simpa [normalRename] using variableList_printed full prior [result] isPrefix] + simp [pure, StateT.pure, Except.pure] + +@[simp] private theorem liftNumbers_variableTokens (identifiers : List VarId) + (names : List String) : + (liftNumbers (identifiers.map variableToken)).run names = + .ok (([], identifiers.map variableToken), names) := by + induction identifiers with + | nil => simp [liftNumbers, StateT.run, pure, StateT.pure, Except.pure] + | cons identifier following induction => + simp only [List.map_cons, liftNumbers, variableToken, StateT.run, bind, + StateT.bind, Except.bind] + rw [show liftNumbers (following.map variableToken) names = + .ok (([], following.map variableToken), names) from induction] + simp [pure, StateT.pure, Except.pure] + +private theorem liftNumbers_icall (name : String) (identifiers : List VarId) + (names : List String) : + liftNumbers (Token.label name :: identifiers.map variableToken) names = + .ok (([], Token.label name :: identifiers.map variableToken), names) := by + simp only [liftNumbers, bind, StateT.bind, Except.bind] + rw [show liftNumbers (identifiers.map variableToken) names = + .ok (([], identifiers.map variableToken), names) from + liftNumbers_variableTokens identifiers names] + simp [pure, StateT.pure, Except.pure] + +private theorem operand_printed (full prior : List VarId) (identifier : VarId) + (isPrefix : prior ++ [identifier] <+: full) : + (operand (variableToken identifier)).run (printedVariableNames prior) = + .ok (([], normalRename full identifier), + printedVariableNames (prior ++ [identifier])) := by + simp only [operand, variableToken, StateT.run, bind, StateT.bind, Except.bind] + rw [show internVariable (variableName identifier) (printedVariableNames prior) = + .ok (normalRename full identifier, + printedVariableNames (prior ++ [identifier])) from by + simpa [normalRename] using internVariable_normal full prior identifier isPrefix] + simp [pure, StateT.pure, Except.pure] + +private theorem operands_printed (full prior identifiers : List VarId) + (isPrefix : prior ++ identifiers <+: full) : + (operands (identifiers.map variableToken)).run (printedVariableNames prior) = + .ok (([], identifiers.map (normalRename full) |>.toArray), + printedVariableNames (prior ++ identifiers)) := by + induction identifiers generalizing prior with + | nil => simp [operands, StateT.run, pure, StateT.pure, Except.pure] + | cons identifier following induction => + simp only [List.map_cons, operands, StateT.run, bind, StateT.bind, Except.bind] + rw [show operand (variableToken identifier) (printedVariableNames prior) = + .ok (([], normalRename full identifier), + printedVariableNames (prior ++ [identifier])) from + operand_printed full prior identifier + ((show prior ++ [identifier] <+: prior ++ identifier :: following from + ⟨following, by simp⟩).trans isPrefix)] + simp only + rw [show operands (following.map variableToken) + (printedVariableNames (prior ++ [identifier])) = + .ok (([], following.map (normalRename full) |>.toArray), + printedVariableNames ((prior ++ [identifier]) ++ following)) from + induction (prior ++ [identifier]) (by simpa [List.append_assoc] using isPrefix)] + simp [pure, StateT.pure, Except.pure, List.append_assoc] + +private theorem statementParts_definition (results : List VarId) + (operandTokens : List Token) + (headless : statementParts operandTokens = ([], operandTokens)) : + statementParts (definitionTokens results ++ operandTokens) = + (results.map variableToken, operandTokens) := by + cases results with + | nil => simpa [definitionTokens] using headless + | cons head tail => + simpa [definitionTokens] using + statementParts_results (head :: tail) operandTokens + +private theorem parseStatement_printed_head (functions : List String) + (full prior results : List VarId) (mnemonic : String) (parameters : List Token) + (notConst : mnemonic ≠ "const") + (headless : statementParts (Token.identifier mnemonic :: parameters) = + ([], Token.identifier mnemonic :: parameters)) + (numberFree : liftNumbers parameters (printedVariableNames prior) = + .ok (([], parameters), printedVariableNames prior)) + (isPrefix : prior ++ results <+: full) : + (parseStatement functions + (definitionTokens results ++ Token.identifier mnemonic :: parameters)).run + (printedVariableNames prior) = + (parseMnemonic functions + (definitionTokens results ++ Token.identifier mnemonic :: parameters) + mnemonic (results.map (normalRename full)) parameters).run + (printedVariableNames (prior ++ results)) := by + rw [parseStatement] + simp only [statementParts_definition results (Token.identifier mnemonic :: parameters) + headless] + simp only [StateT.run, bind, StateT.bind, Except.bind] + rw [numberFree] + simp only [] + rw [show variableList (results.map variableToken) (printedVariableNames prior) = + .ok ((results.map (normalRename full)).toArray, + printedVariableNames (prior ++ results)) from by + simpa [normalRename] using variableList_printed full prior results isPrefix] + simp only [] + cases outcome : parseMnemonic functions + (definitionTokens results ++ Token.identifier mnemonic :: parameters) mnemonic + (results.map (normalRename full)) parameters + (printedVariableNames (prior ++ results)) with + | error message => rfl + | ok pair => rfl + +private theorem statementParts_operation (name : String) (operands : List VarId) : + statementParts (Token.identifier name :: operands.map variableToken) = + ([], Token.identifier name :: operands.map variableToken) := by + rw [statementParts] + simp only [List.span, List.span.loop, identifier_ne_equals] + rw [span_variableTokens_end_aux operands [Token.identifier name]] + +private theorem immediateTokens_operation (program : Program) (statement : Stmt) + (notConst : (spelling statement).name ≠ "const") + (notIcall : (spelling statement).name ≠ "icall") : + immediateTokens program statement = [] := by + cases statement with + | assign result value => + cases value with + | constant => exact (notConst rfl).elim + | _ => rfl + | icall => exact (notIcall rfl).elim + | _ => rfl + +private theorem parseStatement_printed_operation (program : Program) + (full prior : List VarId) (statement : Stmt) + (notConst : (spelling statement).name ≠ "const") + (notIcall : (spelling statement).name ≠ "icall") + (isPrefix : prior ++ statement.variableOccurrences <+: full) : + (parseStatement (printedFunctionNames program) (stmtTokens program statement)).run + (printedVariableNames prior) = + .ok ([statement.renameVariables (normalRename full)], + printedVariableNames (prior ++ statement.variableOccurrences)) := by + have occurrences := variableOccurrences_spelling statement + rw [occurrences] at isPrefix ⊢ + rw [show stmtTokens program statement = + definitionTokens (spelling statement).results ++ + Token.identifier (spelling statement).name :: + (spelling statement).operands.map variableToken from by + rw [stmtTokens, immediateTokens_operation program statement notConst notIcall] + rfl] + rw [parseStatement_printed_head (printedFunctionNames program) full prior + (spelling statement).results (spelling statement).name + ((spelling statement).operands.map variableToken) notConst + (statementParts_operation _ _) + (liftNumbers_variableTokens (spelling statement).operands (printedVariableNames prior)) + ((show prior ++ (spelling statement).results <+: + prior ++ ((spelling statement).results ++ (spelling statement).operands) from + ⟨(spelling statement).operands, by simp⟩).trans isPrefix)] + rw [parseMnemonic, if_neg notIcall, parseOperation] + obtain ⟨entry, foundEq, resultsOk, operandsOk, buildEq⟩ := + build_spelling statement (normalRename full) notConst notIcall + simp only [StateT.run, foundEq] + rw [dif_pos (by simpa using resultsOk)] + simp only [bind, StateT.bind] + rw [show operands ((spelling statement).operands.map variableToken) + (printedVariableNames (prior ++ (spelling statement).results)) = + .ok (([], (spelling statement).operands.map (normalRename full) |>.toArray), + printedVariableNames + (prior ++ (spelling statement).results ++ (spelling statement).operands)) from + operands_printed full (prior ++ (spelling statement).results) + (spelling statement).operands (by simpa [List.append_assoc] using isPrefix)] + simp only [Except.bind] + rw [dif_pos operandsOk] + simp only [pure, StateT.pure, Except.pure, List.append_assoc, buildEq] + +private theorem parseStatement_printed (program : Program) + (full prior : List VarId) (statement : Stmt) + (references : statement.FunctionReferencesInRange program.functions.size) + (isPrefix : prior ++ statement.variableOccurrences <+: full) : + (parseStatement (printedFunctionNames program) (stmtTokens program statement)).run + (printedVariableNames prior) = + .ok ([statement.renameVariables (normalRename full)], + printedVariableNames (prior ++ statement.variableOccurrences)) := by + cases statement with + | assign result value => + cases value with + | constant value => + simpa [Stmt.variableOccurrences, Stmt.renameVariables] using + parseStatement_assign_constant program (printedFunctionNames program) full prior + result value isPrefix + | var | add | lt | sload => + exact parseStatement_printed_operation program full prior _ + (by simp [spelling]) (by simp [spelling]) isPrefix + | icall callee args dests => + rcases args with ⟨args⟩ + rcases dests with ⟨dests⟩ + simp only [Stmt.variableOccurrences, + Stmt.FunctionReferencesInRange] at references isPrefix ⊢ + cases dests with + | nil => + simp only [List.nil_append] at isPrefix ⊢ + rw [show stmtTokens program (.icall callee ⟨args⟩ ⟨[]⟩) = + definitionTokens ([] : List VarId) ++ + Token.identifier "icall" :: Token.label (functionName program callee) :: + args.map variableToken from rfl, + parseStatement_printed_head (printedFunctionNames program) full prior [] "icall" + (Token.label (functionName program callee) :: args.map variableToken) + (by decide) (statementParts_icall_no_results _ args) + (liftNumbers_icall (functionName program callee) args _) + (by simpa using + (show prior <+: prior ++ args from ⟨args, rfl⟩).trans isPrefix)] + simp only [List.map_nil, List.append_nil, parseMnemonic, reduceIte, + parseInternalCall, StateT.run, bind] + rw [printedFunctionNames_findIdx program callee references] + simp only [StateT.bind] + rw [show operands (args.map variableToken) (printedVariableNames prior) = + .ok (([], args.map (normalRename full) |>.toArray), + printedVariableNames (prior ++ args)) from + operands_printed full prior args isPrefix] + simp [bind, Except.bind, pure, StateT.pure, Except.pure, Stmt.renameVariables] + | cons destination following => + simp only [List.cons_append] at isPrefix ⊢ + rw [show stmtTokens program (.icall callee ⟨args⟩ ⟨destination :: following⟩) = + definitionTokens (destination :: following : List VarId) ++ + Token.identifier "icall" :: Token.label (functionName program callee) :: + args.map variableToken from by + simp [stmtTokens, spelling, immediateTokens], + parseStatement_printed_head (printedFunctionNames program) full prior + (destination :: following) "icall" + (Token.label (functionName program callee) :: args.map variableToken) + (by decide) (statementParts_icall_no_results _ args) + (liftNumbers_icall (functionName program callee) args _) + ((show prior ++ (destination :: following) <+: + prior ++ (destination :: following) ++ args from ⟨args, by simp⟩).trans + (by simpa [List.append_assoc] using isPrefix))] + simp only [parseMnemonic, reduceIte, parseInternalCall, StateT.run, bind] + rw [printedFunctionNames_findIdx program callee references] + simp only [StateT.bind] + rw [show operands (args.map variableToken) + (printedVariableNames (prior ++ destination :: following)) = + .ok (([], args.map (normalRename full) |>.toArray), + printedVariableNames (prior ++ destination :: following ++ args)) from + operands_printed full (prior ++ destination :: following) args + (by simpa [List.append_assoc] using isPrefix)] + simp [bind, Except.bind, pure, StateT.pure, Except.pure, List.append_assoc, + Stmt.renameVariables] + | sstore | gas | call | malloc | mallocUninit | mstore32 | mload32 => + exact parseStatement_printed_operation program full prior _ + (by simp [spelling]) (by simp [spelling]) isPrefix + +private def printedBlockNames (function : Function) : List String := + function.blocks.toList.zipIdx.map fun pair => blockName ⟨pair.2⟩ + +private theorem printedBlockNames_length (function : Function) : + (printedBlockNames function).length = function.blocks.size := by + simp [printedBlockNames] + +private theorem printedBlockNames_getElem (function : Function) (index : Nat) + (bound : index < (printedBlockNames function).length) : + (printedBlockNames function)[index] = blockName ⟨index⟩ := by + simp [printedBlockNames] + +private theorem printedBlockNames_findIdx (function : Function) (identifier : BlockId) + (bound : identifier.id < function.blocks.size) : + (printedBlockNames function).findIdx? (· == blockName identifier) = + some identifier.id := by + rw [List.findIdx?_eq_some_iff_findIdx_eq] + have listBound : identifier.id < (printedBlockNames function).length := by + simpa [printedBlockNames_length] using bound + refine ⟨listBound, (List.findIdx_eq listBound).2 ⟨?_, ?_⟩⟩ + · simp [printedBlockNames_getElem] + · intro index indexBound + simp only [beq_eq_false_iff_ne] + intro equality + have nameEquality : blockName ⟨index⟩ = blockName identifier := by + rw [← printedBlockNames_getElem function index (by omega)] + exact equality + have identifiersEqual : (⟨index⟩ : BlockId) = identifier := by + cases identifier + simp [blockName] at nameEquality ⊢ + exact nameEquality + exact Nat.ne_of_lt indexBound (congrArg BlockId.id identifiersEqual) + +private theorem parseTerminator_printed (function : Function) (full prior : List VarId) + (terminator : Terminator) + (references : terminator.BlockReferencesInRange function.blocks.size) + (isPrefix : prior ++ terminator.variableOccurrences <+: full) : + (parseTerminator (printedBlockNames function) (terminatorTokens terminator)).run + (printedVariableNames prior) = + .ok (terminator.renameVariables (normalRename full), + printedVariableNames (prior ++ terminator.variableOccurrences)) := by + cases terminator with + | halt => simp [parseTerminator, terminatorTokens, Terminator.renameVariables, + Terminator.variableOccurrences, StateT.run, pure, StateT.pure, Except.pure] + | iret => simp [parseTerminator, terminatorTokens, Terminator.renameVariables, + Terminator.variableOccurrences, StateT.run, pure, StateT.pure, Except.pure] + | jump target => + simp only [Terminator.BlockReferencesInRange] at references + simp [parseTerminator, terminatorTokens, resolveBlock, Terminator.renameVariables, + Terminator.variableOccurrences, StateT.run, bind, StateT.bind, Except.bind] + rw [printedBlockNames_findIdx function target references] + simp [pure, StateT.pure, Except.pure] + | branch condition thenTarget elseTarget => + rcases references with ⟨thenBound, elseBound⟩ + simp only [Terminator.variableOccurrences] at isPrefix ⊢ + simp [parseTerminator, terminatorTokens, resolveBlock, Terminator.renameVariables, + variableToken, StateT.run, bind, StateT.bind, Except.bind] + rw [show internVariable (variableName condition) (printedVariableNames prior) = + .ok (normalRename full condition, printedVariableNames (prior ++ [condition])) from by + simpa [normalRename] using + internVariable_normal full prior condition isPrefix] + simp only + rw [printedBlockNames_findIdx function thenTarget thenBound] + simp only + rw [printedBlockNames_findIdx function elseTarget elseBound] + simp [pure, StateT.pure, Except.pure] + +private theorem parseBlockBody_printed (program : Program) + (function : Function) (full prior : List VarId) (statements : List Stmt) + (terminator : Terminator) + (statementReferences : ∀ statement ∈ statements, + statement.FunctionReferencesInRange program.functions.size) + (terminatorReferences : terminator.BlockReferencesInRange function.blocks.size) + (isPrefix : prior ++ statements.flatMap Stmt.variableOccurrences ++ + terminator.variableOccurrences <+: full) : + (parseBlockBody (printedFunctionNames program) (printedBlockNames function) + (statements.map (stmtTokens program) ++ [terminatorTokens terminator])).run + (printedVariableNames prior) = + .ok (((statements.map (·.renameVariables (normalRename full))).toArray, + terminator.renameVariables (normalRename full)), + printedVariableNames (prior ++ statements.flatMap Stmt.variableOccurrences ++ + terminator.variableOccurrences)) := by + induction statements generalizing prior with + | nil => + simp only [List.map_nil, List.nil_append, List.flatMap_nil, List.nil_append] at isPrefix ⊢ + rw [parseBlockBody.eq_2] + simp only [StateT.run, bind, StateT.bind, Except.bind] + rw [show parseTerminator (printedBlockNames function) (terminatorTokens terminator) + (printedVariableNames prior) = + .ok (terminator.renameVariables (normalRename full), + printedVariableNames (prior ++ terminator.variableOccurrences)) from + parseTerminator_printed function full prior terminator terminatorReferences + (by simpa using isPrefix)] + simp [pure, StateT.pure, Except.pure] + | cons statement following induction => + simp only [List.map_cons, List.cons_append, List.flatMap_cons] at isPrefix ⊢ + have isPrefix' : prior ++ statement.variableOccurrences ++ + following.flatMap Stmt.variableOccurrences ++ terminator.variableOccurrences <+: + full := by + simpa [List.append_assoc] using isPrefix + rw [parseBlockBody.eq_3 _ _ _ _ (by simp)] + simp only [StateT.run, bind, StateT.bind, Except.bind] + rw [show parseStatement (printedFunctionNames program) (stmtTokens program statement) + (printedVariableNames prior) = + .ok ([statement.renameVariables (normalRename full)], + printedVariableNames (prior ++ statement.variableOccurrences)) from + parseStatement_printed program full prior statement + (statementReferences statement (by simp)) + ((show prior ++ statement.variableOccurrences <+: + prior ++ statement.variableOccurrences ++ + following.flatMap Stmt.variableOccurrences ++ + terminator.variableOccurrences from + ⟨following.flatMap Stmt.variableOccurrences ++ terminator.variableOccurrences, + by simp [List.append_assoc]⟩).trans isPrefix')] + simp only + rw [show parseBlockBody (printedFunctionNames program) (printedBlockNames function) + (following.map (stmtTokens program) ++ [terminatorTokens terminator]) + (printedVariableNames (prior ++ statement.variableOccurrences)) = + .ok (((following.map (·.renameVariables (normalRename full))).toArray, + terminator.renameVariables (normalRename full)), + printedVariableNames ((prior ++ statement.variableOccurrences) ++ + following.flatMap Stmt.variableOccurrences ++ terminator.variableOccurrences)) from + induction (prior ++ statement.variableOccurrences) + (fun followingStatement member => + statementReferences followingStatement (by simp [member])) + (by simpa [List.append_assoc] using isPrefix')] + simp [pure, StateT.pure, Except.pure, List.append_assoc] + +@[simp] private theorem variableToken_ne_arrow (identifier : VarId) : + (variableToken identifier != Token.arrow) = true := by + rfl + +private theorem spanVariableTokensToEndAux (identifiers : List VarId) + (accumulated : List Token) : + List.span.loop (· != Token.arrow) (identifiers.map variableToken) accumulated = + (accumulated.reverse ++ identifiers.map variableToken, []) := by + induction identifiers generalizing accumulated with + | nil => simp [List.span.loop] + | cons identifier following induction => + simp only [List.map_cons, List.span.loop, variableToken_ne_arrow] + rw [induction (variableToken identifier :: accumulated)] + simp + +private theorem spanVariableTokensToEnd (identifiers : List VarId) : + (identifiers.map variableToken).span (· != Token.arrow) = + (identifiers.map variableToken, []) := by + simpa [List.span] using spanVariableTokensToEndAux identifiers [] + +private theorem spanVariableTokensToArrowAux (identifiers : List VarId) + (rest accumulated : List Token) : + List.span.loop (· != Token.arrow) + (identifiers.map variableToken ++ Token.arrow :: rest) accumulated = + (accumulated.reverse ++ identifiers.map variableToken, Token.arrow :: rest) := by + induction identifiers generalizing accumulated with + | nil => simp [List.span.loop] + | cons identifier following induction => + simp only [List.map_cons, List.cons_append, List.span.loop, variableToken_ne_arrow] + rw [induction (variableToken identifier :: accumulated)] + simp + +private theorem spanVariableTokensToArrow (identifiers : List VarId) (rest : List Token) : + (identifiers.map variableToken ++ Token.arrow :: rest).span (· != Token.arrow) = + (identifiers.map variableToken, Token.arrow :: rest) := by + simpa [List.span] using spanVariableTokensToArrowAux identifiers rest [] + +private theorem parseBlockHeader_printed (full prior : List VarId) (identifier : BlockId) + (block : Block) + (isPrefix : prior ++ block.inputs.toList ++ block.outputs.toList <+: full) : + (parseBlockHeader + ([Token.identifier (blockName identifier)] ++ variableTokens block.inputs ++ + (if block.outputs.isEmpty then [] else + Token.arrow :: variableTokens block.outputs) ++ [Token.leftBrace])).run + (printedVariableNames prior) = + .ok ((block.inputs.map (normalRename full), + block.outputs.map (normalRename full)), + printedVariableNames (prior ++ block.inputs.toList ++ block.outputs.toList)) := by + rcases block with ⟨inputs, statements, terminator, outputs⟩ + rcases inputs with ⟨inputs⟩ + rcases outputs with ⟨outputs⟩ + cases outputs with + | nil => + simp only [List.append_nil] at isPrefix ⊢ + simp [parseBlockHeader, variableTokens] + rw [← List.span_eq_takeWhile_dropWhile, spanVariableTokensToEnd] + simp only + rw [show StateT.run (variableList (inputs.map variableToken)) + (printedVariableNames prior) = + .ok (inputs.map (normalRename full) |>.toArray, + printedVariableNames (prior ++ inputs)) from + variableList_printed full prior inputs (by + simpa using isPrefix)] + simp [variableList, StateT.run, bind, pure, StateT.pure, Except.bind, Except.pure, + Functor.map, Except.map] + | cons output following => + simp only at isPrefix ⊢ + simp [parseBlockHeader, variableTokens] + rw [← List.span_eq_takeWhile_dropWhile, spanVariableTokensToArrow] + simp only + rw [show StateT.run (variableList (inputs.map variableToken)) + (printedVariableNames prior) = + .ok (inputs.map (normalRename full) |>.toArray, + printedVariableNames (prior ++ inputs)) from + variableList_printed full prior inputs + ((show prior ++ inputs <+: prior ++ inputs ++ output :: following from + ⟨output :: following, rfl⟩).trans isPrefix)] + simp only [bind, Except.bind] + rw [show StateT.run + (variableList (variableToken output :: following.map variableToken)) + (printedVariableNames (prior ++ inputs)) = + .ok ((output :: following).map (normalRename full) |>.toArray, + printedVariableNames ((prior ++ inputs) ++ output :: following)) from by + simpa [List.map_cons] using + variableList_printed full (prior ++ inputs) (output :: following) + (by simpa [List.append_assoc] using isPrefix)] + simp [List.append_assoc] + +private theorem parseBlock_printed (program : Program) + (function : Function) (full prior : List VarId) (identifier : BlockId) + (block : Block) + (references : block.ReferencesInRange program.functions.size function.blocks.size) + (isPrefix : prior ++ block.variableOccurrences <+: full) : + (parseBlock (printedFunctionNames program) (printedBlockNames function) + ([Token.identifier (blockName identifier)] ++ variableTokens block.inputs ++ + (if block.outputs.isEmpty then [] else + Token.arrow :: variableTokens block.outputs) ++ [Token.leftBrace]) + (block.statements.toList.map (stmtTokens program) ++ + [terminatorTokens block.terminator])).run (printedVariableNames prior) = + .ok (block.renameVariables (normalRename full), + printedVariableNames (prior ++ block.variableOccurrences)) := by + rcases references with ⟨statementReferences, terminatorReferences⟩ + simp only [parseBlock, StateT.run, bind, StateT.bind, Except.bind] + rw [show parseBlockHeader + ([Token.identifier (blockName identifier)] ++ variableTokens block.inputs ++ + (if block.outputs.isEmpty then [] else + Token.arrow :: variableTokens block.outputs) ++ [Token.leftBrace]) + (printedVariableNames prior) = + .ok ((block.inputs.map (normalRename full), + block.outputs.map (normalRename full)), + printedVariableNames + (prior ++ block.inputs.toList ++ block.outputs.toList)) from + parseBlockHeader_printed full prior identifier block + ((show prior ++ block.inputs.toList ++ block.outputs.toList <+: + prior ++ block.variableOccurrences from + ⟨block.statements.toList.flatMap Stmt.variableOccurrences ++ + block.terminator.variableOccurrences, + by simp [Block.variableOccurrences, List.append_assoc]⟩).trans isPrefix)] + simp only + rw [show parseBlockBody (printedFunctionNames program) (printedBlockNames function) + (block.statements.toList.map (stmtTokens program) ++ + [terminatorTokens block.terminator]) + (printedVariableNames + (prior ++ block.inputs.toList ++ block.outputs.toList)) = + .ok (((block.statements.toList.map + (·.renameVariables (normalRename full))).toArray, + block.terminator.renameVariables (normalRename full)), + printedVariableNames + ((prior ++ block.inputs.toList ++ block.outputs.toList) ++ + block.statements.toList.flatMap Stmt.variableOccurrences ++ + block.terminator.variableOccurrences)) from + parseBlockBody_printed program function full + (prior ++ block.inputs.toList ++ block.outputs.toList) block.statements.toList + block.terminator + (fun statement member => statementReferences statement (by simpa using member)) + terminatorReferences (by + simpa [Block.variableOccurrences, List.append_assoc] using isPrefix)] + have statementMap : + (block.statements.toList.map + (·.renameVariables (normalRename full))).toArray = + block.statements.map (·.renameVariables (normalRename full)) := by + cases block.statements + simp + rw [statementMap] + simp [Block.renameVariables, Block.variableOccurrences, pure, StateT.pure, Except.pure, + List.append_assoc] + +private def printedBlockHeader (identifier : BlockId) (block : Block) : Line := + [Token.identifier (blockName identifier)] ++ variableTokens block.inputs ++ + (if block.outputs.isEmpty then [] else + Token.arrow :: variableTokens block.outputs) ++ [Token.leftBrace] + +private def printedBlockBody (program : Program) (block : Block) : List Line := + block.statements.toList.map (stmtTokens program) ++ + [terminatorTokens block.terminator] + +private def printedBlockGroups (program : Program) (function : Function) : + List (Line × List Line) := + function.blocks.toList.zipIdx.map fun pair => + (printedBlockHeader ⟨pair.2⟩ pair.1, printedBlockBody program pair.1) + +private theorem blockLines_eq (program : Program) (identifier : BlockId) + (block : Block) : + blockLines program identifier block = + printedBlockHeader identifier block :: + printedBlockBody program block ++ [[Token.rightBrace]] := by + simp [blockLines, printedBlockHeader, printedBlockBody] + +private theorem printedBlockHeader_isHeader (identifier : BlockId) (block : Block) : + isBlockHeader (printedBlockHeader identifier block) = true := by + rw [show printedBlockHeader identifier block = + ([Token.identifier (blockName identifier)] ++ variableTokens block.inputs ++ + (if block.outputs.isEmpty then [] else + Token.arrow :: variableTokens block.outputs)) ++ [Token.leftBrace] by + simp [printedBlockHeader, List.append_assoc]] + unfold isBlockHeader + rw [List.getLast?_append] + rfl + +private theorem printedBlockBody_ne_rightBrace (program : Program) (block : Block) : + ∀ line ∈ printedBlockBody program block, line ≠ [Token.rightBrace] := by + intro line member + simp only [printedBlockBody, List.mem_append, List.mem_map, List.mem_singleton] at member + rcases member with ⟨statement, _, rfl⟩ | rfl + · rcases stmtTokens_head program statement with + ⟨identifier, rest, lineEq⟩ | ⟨rest, lineEq⟩ <;> + simp [lineEq, variableToken] + · cases block.terminator <;> simp [terminatorTokens] + +private theorem splitBlocksAux_body (groups : List (Line × List Line)) + (header : Line) (accumulated body rest : List Line) + (notRightBrace : ∀ line ∈ body, line ≠ [Token.rightBrace]) : + splitBlocksAux ((header, accumulated) :: groups) true + (body ++ [Token.rightBrace] :: rest) = + splitBlocksAux ((header, body.reverse ++ accumulated) :: groups) false rest := by + induction body generalizing accumulated with + | nil => simp [splitBlocksAux] + | cons line following induction => + rw [List.cons_append, splitBlocksAux.eq_def] + simp only + rw [show (line == [Token.rightBrace]) = false by + simp [notRightBrace line (by simp)]] + simp only [Bool.false_eq_true, if_false] + rw [induction (line :: accumulated)] + · simp + · intro next member + exact notRightBrace next (by simp [member]) + +private theorem splitBlocksAux_functionBodyLines (program : Program) (function : Function) + (groupsPrefix : List (Line × List Line)) : + splitBlocksAux groupsPrefix false (functionBodyLines program function) = + .ok (groupsPrefix.reverse.map (fun group => (group.fst, group.snd.reverse)) ++ + printedBlockGroups program function) := by + rw [functionBodyLines, printedBlockGroups] + generalize valuesEq : function.blocks.toList.zipIdx = values + clear valuesEq + induction values generalizing groupsPrefix with + | nil => simp [splitBlocksAux] + | cons pair following induction => + rcases pair with ⟨block, index⟩ + simp only [List.flatMap_cons, List.map_cons] + rw [blockLines_eq] + rw [show printedBlockHeader ⟨index⟩ block :: + printedBlockBody program block ++ [[Token.rightBrace]] ++ + following.flatMap (fun pair => blockLines program ⟨pair.2⟩ pair.1) = + printedBlockHeader ⟨index⟩ block :: + (printedBlockBody program block ++ [Token.rightBrace] :: + following.flatMap (fun pair => blockLines program ⟨pair.2⟩ pair.1)) by + simp [List.append_assoc]] + rw [splitBlocksAux.eq_def] + simp only [Bool.false_eq_true, if_false] + rw [if_pos (printedBlockHeader_isHeader ⟨index⟩ block)] + rw [splitBlocksAux_body groupsPrefix (printedBlockHeader ⟨index⟩ block) [] + (printedBlockBody program block) + (following.flatMap fun pair => blockLines program ⟨pair.2⟩ pair.1) + (printedBlockBody_ne_rightBrace program block)] + rw [induction] + simp + +private theorem splitBlocks_functionBodyLines (program : Program) (function : Function) : + splitBlocks (functionBodyLines program function) = + .ok (printedBlockGroups program function) := by + rw [splitBlocks, splitBlocksAux_functionBodyLines] + rfl + +private theorem hasDuplicates_blockNames (identifiers : List Nat) + (nodup : identifiers.Nodup) : + hasDuplicates (identifiers.map fun identifier => blockName ⟨identifier⟩) = false := by + induction identifiers with + | nil => rfl + | cons identifier following induction => + simp only [List.nodup_cons] at nodup + have notMember : blockName ⟨identifier⟩ ∉ + following.map fun followingIdentifier => blockName ⟨followingIdentifier⟩ := by + simpa [blockName] using nodup.1 + have notContained : + (following.map fun followingIdentifier => + blockName ⟨followingIdentifier⟩).contains (blockName ⟨identifier⟩) = false := by + cases contained : (following.map fun followingIdentifier => + blockName ⟨followingIdentifier⟩).contains (blockName ⟨identifier⟩) with + | false => rfl + | true => exact False.elim (notMember (List.contains_iff_mem.mp contained)) + rw [List.map_cons, hasDuplicates.eq_def] + simp only + rw [notContained, induction nodup.2] + rfl + +private theorem printedBlockNames_noDuplicates (function : Function) : + hasDuplicates (printedBlockNames function) = false := by + rw [printedBlockNames] + rw [show (function.blocks.toList.zipIdx.map fun pair => blockName ⟨pair.2⟩) = + (function.blocks.toList.zipIdx.map Prod.snd).map fun identifier => + blockName ⟨identifier⟩ by + rw [List.map_map] + rfl] + rw [show function.blocks.toList.zipIdx.map Prod.snd = + List.range' 0 function.blocks.toList.length by simp] + apply hasDuplicates_blockNames + exact List.nodup_range' + +private theorem mapM_blockHeaderName_printedBlockGroups (program : Program) + (function : Function) : + (printedBlockGroups program function).mapM (fun group => blockHeaderName group.fst) = + .ok (printedBlockNames function) := by + rw [printedBlockGroups, printedBlockNames] + generalize valuesEq : function.blocks.toList.zipIdx = values + clear valuesEq + induction values with + | nil => rfl + | cons pair following induction => + rcases pair with ⟨block, index⟩ + simp only [List.map_cons, List.mapM_cons] + rw [show blockHeaderName (printedBlockHeader ⟨index⟩ block) = + .ok (blockName ⟨index⟩) by + simp [blockHeaderName, printedBlockHeader]] + simp [induction, bind, Except.bind, pure, Except.pure] + +private theorem mapM_parseBlock_printed (program : Program) + (function : Function) (full prior : List VarId) + (values : List (Block × Nat)) + (references : ∀ pair ∈ values, + pair.1.ReferencesInRange program.functions.size function.blocks.size) + (isPrefix : prior ++ values.flatMap (fun pair => pair.1.variableOccurrences) <+: + full) : + ((values.map fun pair => + (printedBlockHeader ⟨pair.2⟩ pair.1, printedBlockBody program pair.1)).mapM + (fun group => parseBlock (printedFunctionNames program) (printedBlockNames function) + group.fst group.snd)).run (printedVariableNames prior) = + .ok (values.map (fun pair => + pair.1.renameVariables (normalRename full)), + printedVariableNames + (prior ++ values.flatMap (fun pair => pair.1.variableOccurrences))) := by + induction values generalizing prior with + | nil => simp [StateT.run, pure, StateT.pure, Except.pure] + | cons pair following induction => + rcases pair with ⟨block, index⟩ + simp only [List.map_cons, List.mapM_cons, List.flatMap_cons] + simp only [StateT.run, bind, StateT.bind, Except.bind] + rw [show parseBlock (printedFunctionNames program) (printedBlockNames function) + (printedBlockHeader ⟨index⟩ block) (printedBlockBody program block) + (printedVariableNames prior) = + .ok (block.renameVariables (normalRename full), + printedVariableNames (prior ++ block.variableOccurrences)) from by + simpa [printedBlockHeader, printedBlockBody] using + parseBlock_printed program function full prior ⟨index⟩ block + (references (block, index) (by simp)) + ((show prior ++ block.variableOccurrences <+: + prior ++ block.variableOccurrences ++ + following.flatMap (fun pair => pair.1.variableOccurrences) from + ⟨following.flatMap (fun pair => pair.1.variableOccurrences), rfl⟩).trans + (by simpa [List.append_assoc] using isPrefix))] + simp only + rw [show ((following.map fun pair => + (printedBlockHeader ⟨pair.2⟩ pair.1, + printedBlockBody program pair.1)).mapM + (fun group => parseBlock (printedFunctionNames program) + (printedBlockNames function) group.fst group.snd)) + (printedVariableNames (prior ++ block.variableOccurrences)) = + .ok (following.map (fun pair => + pair.1.renameVariables (normalRename full)), + printedVariableNames ((prior ++ block.variableOccurrences) ++ + following.flatMap (fun pair => pair.1.variableOccurrences))) from + induction (prior ++ block.variableOccurrences) + (fun followingPair member => references followingPair (by simp [member])) + (by simpa [List.append_assoc] using isPrefix)] + simp [pure, StateT.pure, Except.pure, List.append_assoc] + +private theorem parseFunctionGroups_printed (program : Program) + (function : Function) + (functionReferences : function.ReferencesInRange program.functions.size) + (full prior : List VarId) + (isPrefix : prior ++ function.variableOccurrences <+: full) : + (parseFunctionGroups (printedFunctionNames program) + (printedBlockGroups program function)).run (printedVariableNames prior) = + .ok (function.renameVariables (normalRename full), + printedVariableNames (prior ++ function.variableOccurrences)) := by + have references := functionReferences + simp only [parseFunctionGroups, StateT.run, bind, StateT.bind, Except.bind] + rw [mapM_blockHeaderName_printedBlockGroups program function] + simp only [bind, liftM, monadLift, MonadLift.monadLift, StateT.lift, Except.bind] + simp only [pure, Except.pure] + rw [printedBlockNames_noDuplicates function] + simp only [Bool.false_eq_true, if_false] + simp only [bind, StateT.bind, pure, StateT.pure, Except.pure, Except.bind] + rw [show ((printedBlockGroups program function).mapM fun group => + parseBlock (printedFunctionNames program) (printedBlockNames function) + group.fst group.snd) (printedVariableNames prior) = + .ok (function.blocks.toList.zipIdx.map (fun pair => + pair.1.renameVariables (normalRename full)), + printedVariableNames (prior ++ function.blocks.toList.zipIdx.flatMap + (fun pair => pair.1.variableOccurrences))) from by + simpa [printedBlockGroups] using + mapM_parseBlock_printed program function full prior + function.blocks.toList.zipIdx + (fun pair member => references pair.1 (by + have : pair.1 ∈ function.blocks.toList := by + exact List.fst_mem_of_mem_zipIdx member + simpa using this)) + (by + have occurrencesEq : + function.blocks.toList.zipIdx.flatMap + (fun pair => pair.1.variableOccurrences) = + function.blocks.toList.flatMap Block.variableOccurrences := by + rw [← List.flatMap_map, List.zipIdx_map_fst] + simpa [Function.variableOccurrences, occurrencesEq] using isPrefix)] + have parsedBlocksEq : + function.blocks.toList.zipIdx.map (fun pair => + pair.1.renameVariables (normalRename full)) = + function.blocks.toList.map + (·.renameVariables (normalRename full)) := by + rw [show function.blocks.toList.zipIdx.map (fun pair => + pair.1.renameVariables (normalRename full)) = + (function.blocks.toList.zipIdx.map Prod.fst).map + (·.renameVariables (normalRename full)) by + rw [List.map_map] + rfl] + rw [List.zipIdx_map_fst] + have occurrencesEq : + function.blocks.toList.zipIdx.flatMap (fun pair => pair.1.variableOccurrences) = + function.blocks.toList.flatMap Block.variableOccurrences := by + rw [← List.flatMap_map, List.zipIdx_map_fst] + rw [parsedBlocksEq, occurrencesEq] + rw [show function.blocks.toList = function.entry :: function.rest.toList from by + simp [Function.blocks]] + have restMap : + (function.rest.toList.map (·.renameVariables (normalRename full))).toArray = + function.rest.map (·.renameVariables (normalRename full)) := by + cases function.rest + simp + simp [Function.renameVariables, Function.variableOccurrences, Function.blocks, restMap, + pure, StateT.pure, Except.pure] + +private theorem parseFunction_printed (program : Program) + (function : Function) (functionReferences : function.ReferencesInRange program.functions.size) + (full prior : List VarId) + (isPrefix : prior ++ function.variableOccurrences <+: full) : + (parseFunction (printedFunctionNames program) + (functionBodyLines program function)).run (printedVariableNames prior) = + .ok (function.renameVariables (normalRename full), + printedVariableNames (prior ++ function.variableOccurrences)) := by + rw [parseFunction, splitBlocks_functionBodyLines] + exact parseFunctionGroups_printed program function functionReferences full prior isPrefix + +private theorem hasDuplicates_eq_false_of_nodup (names : List String) + (nodup : names.Nodup) : hasDuplicates names = false := by + induction names with + | nil => rfl + | cons name following induction => + simp only [List.nodup_cons] at nodup + have notContained : following.contains name = false := by + cases contained : following.contains name with + | false => rfl + | true => exact False.elim (nodup.1 (List.contains_iff_mem.mp contained)) + rw [hasDuplicates.eq_def] + simp only + rw [notContained, induction nodup.2] + rfl + +private theorem printedFunctionNames_noDuplicates (program : Program) : + hasDuplicates (printedFunctionNames program) = false := by + apply hasDuplicates_eq_false_of_nodup + rw [printedFunctionNames_eq] + rw [show (program.functions.toList.zipIdx.map fun pair => + functionName program ⟨pair.2⟩) = + (program.functions.toList.zipIdx.map Prod.snd).map fun identifier => + functionName program ⟨identifier⟩ by + rw [List.map_map] + rfl] + rw [show program.functions.toList.zipIdx.map Prod.snd = + List.range' 0 program.functions.toList.length by simp] + apply List.Nodup.map_on + · intro left _ right _ equality + exact congrArg FunctionId.id (functionName_injective equality) + · exact List.nodup_range' + +private theorem mapM_parseFunction_printed (program : Program) + (full prior : List VarId) + (values : List (Function × Nat)) + (functionReferencesAll : ∀ pair ∈ values, + pair.1.ReferencesInRange program.functions.size) + (isPrefix : prior ++ values.flatMap (fun pair => pair.1.variableOccurrences) <+: + full) : + ((values.map fun pair => + (functionName program ⟨pair.2⟩, functionBodyLines program pair.1)).mapM + (fun group => parseFunction (printedFunctionNames program) group.snd)).run + (printedVariableNames prior) = + .ok (values.map (fun pair => + pair.1.renameVariables (normalRename full)), + printedVariableNames + (prior ++ values.flatMap (fun pair => pair.1.variableOccurrences))) := by + induction values generalizing prior with + | nil => simp [StateT.run, pure, StateT.pure, Except.pure] + | cons pair following induction => + rcases pair with ⟨function, index⟩ + simp only [List.map_cons, List.mapM_cons, List.flatMap_cons] + simp only [StateT.run, bind, StateT.bind, Except.bind] + rw [show parseFunction (printedFunctionNames program) + (functionBodyLines program function) (printedVariableNames prior) = + .ok (function.renameVariables (normalRename full), + printedVariableNames (prior ++ function.variableOccurrences)) from + parseFunction_printed program function + (functionReferencesAll (function, index) (by simp)) full prior + ((show prior ++ function.variableOccurrences <+: + prior ++ function.variableOccurrences ++ + following.flatMap (fun pair => pair.1.variableOccurrences) from + ⟨following.flatMap (fun pair => pair.1.variableOccurrences), rfl⟩).trans + (by simpa [List.append_assoc] using isPrefix))] + simp only + rw [show ((following.map fun pair => + (functionName program ⟨pair.2⟩, functionBodyLines program pair.1)).mapM + (fun group => parseFunction (printedFunctionNames program) group.snd)) + (printedVariableNames (prior ++ function.variableOccurrences)) = + .ok (following.map (fun pair => + pair.1.renameVariables (normalRename full)), + printedVariableNames ((prior ++ function.variableOccurrences) ++ + following.flatMap (fun pair => pair.1.variableOccurrences))) from + induction (prior ++ function.variableOccurrences) + (fun followingPair member => functionReferencesAll followingPair (by simp [member])) + (by simpa [List.append_assoc] using isPrefix)] + simp [pure, StateT.pure, Except.pure, List.append_assoc] + +private def printedFollowingGroups (program : Program) : List (String × List Line) := + ((program.main.toList ++ program.rest.toList).zipIdx 1).map fun pair => + (functionName program ⟨pair.2⟩, functionBodyLines program pair.1) + +private def printedRestGroups (program : Program) (start : Nat) : + List (String × List Line) := + (program.rest.toList.zipIdx start).map fun pair => + (functionName program ⟨pair.2⟩, functionBodyLines program pair.1) + +private theorem functions_toList (program : Program) : + program.functions.toList = + program.init :: (program.main.toList ++ program.rest.toList) := by + simp [Program.functions] + +private theorem printedFunctionGroups_cons (program : Program) : + printedFunctionGroups program = + ("init", functionBodyLines program program.init) :: printedFollowingGroups program := by + rw [printedFunctionGroups, printedFollowingGroups, functions_toList] + simp [functionName, Program.initId] + +private theorem printedFunctionNames_cons (program : Program) : + printedFunctionNames program = + "init" :: (printedFollowingGroups program).map Prod.fst := by + rw [printedFunctionNames, printedFunctionGroups_cons] + simp + +private theorem le_of_mem_zipIdx {α : Type} {values : List α} {start : Nat} + {pair : α × Nat} (member : pair ∈ values.zipIdx start) : start ≤ pair.2 := by + induction values generalizing start with + | nil => simp at member + | cons value following induction => + rw [List.zipIdx_cons] at member + rcases List.mem_cons.mp member with rfl | following' + · exact Nat.le_refl _ + · exact Nat.le_of_succ_le (induction following') + +private theorem functionName_fn_of_main_none (program : Program) + (mainEq : program.main = none) {index : Nat} (notInit : index ≠ 0) : + functionName program ⟨index⟩ = "fn" ++ decimalString index := by + simp [functionName, Program.initId, Program.mainId?, mainEq, notInit] + +private theorem functionName_fn_of_two_le (program : Program) {index : Nat} + (bound : 2 ≤ index) : + functionName program ⟨index⟩ = "fn" ++ decimalString index := by + have notInit : index ≠ 0 := by omega + have notMain : ¬ (1 = index) := by omega + simp [functionName, Program.initId, Program.mainId?, notInit, notMain] + +private theorem printedRestGroups_names (program : Program) {start : Nat} + (bound : 2 ≤ start) : + ∀ group ∈ printedRestGroups program start, + group.fst ≠ "init" ∧ group.fst ≠ "main" := by + intro group member + simp only [printedRestGroups, List.mem_map] at member + rcases member with ⟨pair, memberPair, rfl⟩ + have indexBound := le_of_mem_zipIdx memberPair + rw [functionName_fn_of_two_le program (by omega)] + simp + +private theorem printedFollowingGroups_names_of_main_none (program : Program) + (mainEq : program.main = none) : + ∀ group ∈ printedFollowingGroups program, + group.fst ≠ "init" ∧ group.fst ≠ "main" := by + intro group member + simp only [printedFollowingGroups, List.mem_map] at member + rcases member with ⟨pair, memberPair, rfl⟩ + have indexBound := le_of_mem_zipIdx memberPair + rw [functionName_fn_of_main_none program mainEq (by omega)] + simp + +private theorem printedFollowingGroups_of_main_some (program : Program) {main : Function} + (mainEq : program.main = some main) : + printedFollowingGroups program = + ("main", functionBodyLines program main) :: printedRestGroups program 2 := by + rw [printedFollowingGroups, printedRestGroups, mainEq] + simp [List.zipIdx_cons, functionName, Program.initId, Program.mainId?, mainEq] + +private theorem find?_init_printed (program : Program) : + (printedFunctionGroups program).find? (fun group => group.fst == "init") = + some ("init", functionBodyLines program program.init) := by + rw [printedFunctionGroups_cons] + simp + +private theorem find?_main_printed (program : Program) : + ((printedFunctionGroups program).find? (fun group => group.fst == "main")).toList ++ + (printedFunctionGroups program).filter + (fun group => group.fst != "init" && group.fst != "main") = + printedFollowingGroups program ∧ + ((printedFunctionGroups program).find? + (fun group => group.fst == "main")).isSome = program.main.isSome := by + rw [printedFunctionGroups_cons] + cases mainEq : program.main with + | none => + have names := printedFollowingGroups_names_of_main_none program mainEq + have findNone : (printedFollowingGroups program).find? + (fun group => group.fst == "main") = none := by + rw [List.find?_eq_none] + intro group member + simpa using (names group member).2 + have filterSelf : (printedFollowingGroups program).filter + (fun group => group.fst != "init" && group.fst != "main") = + printedFollowingGroups program := by + rw [List.filter_eq_self] + intro group member + have valid := names group member + simp [valid.1, valid.2] + refine ⟨?_, ?_⟩ <;> simp [findNone, filterSelf] + | some main => + have restNames := printedRestGroups_names program (start := 2) (by omega) + have splitEq := printedFollowingGroups_of_main_some program mainEq + have findMain : (printedFollowingGroups program).find? + (fun group => group.fst == "main") = + some ("main", functionBodyLines program main) := by + rw [splitEq] + simp + have filterRest : (printedRestGroups program 2).filter + (fun group => group.fst != "init" && group.fst != "main") = + printedRestGroups program 2 := by + rw [List.filter_eq_self] + intro group member + have valid := restNames group member + simp [valid.1, valid.2] + refine ⟨?_, ?_⟩ + · rw [splitEq] + simp [filterRest] + · simp [findMain] + +private theorem parseFunctionSlots_printed (program : Program) + (inRange : program.ReferencesInRange) : + (parseFunctionSlots (printedFunctionNames program) + ("init", functionBodyLines program program.init) + (printedFollowingGroups program)).run [] = + .ok ((program.init.renameVariables (normalRename program.variableOccurrences), + (program.main.toList ++ program.rest.toList).map + (·.renameVariables (normalRename program.variableOccurrences))), + printedVariableNames program.variableOccurrences) := by + have occurrencesEq : program.variableOccurrences = + program.init.variableOccurrences ++ + (program.main.toList ++ program.rest.toList).flatMap Function.variableOccurrences := by + rw [Program.variableOccurrences, functions_toList] + simp + have zipOccurrencesEq : + ((program.main.toList ++ program.rest.toList).zipIdx 1).flatMap + (fun pair => pair.1.variableOccurrences) = + (program.main.toList ++ program.rest.toList).flatMap Function.variableOccurrences := by + rw [← List.flatMap_map, List.zipIdx_map_fst] + simp only [parseFunctionSlots, StateT.run, bind, StateT.bind, Except.bind] + rw [show parseFunction (printedFunctionNames program) + (functionBodyLines program program.init) [] = + .ok (program.init.renameVariables (normalRename program.variableOccurrences), + printedVariableNames ([] ++ program.init.variableOccurrences)) from + parseFunction_printed program program.init + (inRange program.init (by simp [Program.functions])) + program.variableOccurrences [] + ⟨(program.main.toList ++ program.rest.toList).flatMap Function.variableOccurrences, by + simpa using occurrencesEq.symm⟩] + simp only [List.nil_append] + rw [show (parseFunctionGroupsList (printedFunctionNames program) + (printedFollowingGroups program)) + (printedVariableNames program.init.variableOccurrences) = + .ok (((program.main.toList ++ program.rest.toList).zipIdx 1).map + (fun pair => pair.1.renameVariables (normalRename program.variableOccurrences)), + printedVariableNames (program.init.variableOccurrences ++ + ((program.main.toList ++ program.rest.toList).zipIdx 1).flatMap + (fun pair => pair.1.variableOccurrences))) from + mapM_parseFunction_printed program program.variableOccurrences + program.init.variableOccurrences ((program.main.toList ++ program.rest.toList).zipIdx 1) + (fun pair member => inRange pair.1 (by + have memberList : pair.1 ∈ program.main.toList ++ program.rest.toList := + List.fst_mem_of_mem_zipIdx member + refine Array.mem_toList_iff.mp ?_ + rw [functions_toList] + exact List.mem_cons_of_mem program.init memberList)) + (by rw [zipOccurrencesEq]; exact ⟨[], by simpa using occurrencesEq.symm⟩)] + rw [zipOccurrencesEq, ← occurrencesEq] + have mappedEq : + ((program.main.toList ++ program.rest.toList).zipIdx 1).map + (fun pair => pair.1.renameVariables (normalRename program.variableOccurrences)) = + (program.main.toList ++ program.rest.toList).map + (·.renameVariables (normalRename program.variableOccurrences)) := by + rw [show ((program.main.toList ++ program.rest.toList).zipIdx 1).map (fun pair => + pair.1.renameVariables (normalRename program.variableOccurrences)) = + (((program.main.toList ++ program.rest.toList).zipIdx 1).map Prod.fst).map + (·.renameVariables (normalRename program.variableOccurrences)) by + rw [List.map_map] + rfl] + rw [List.zipIdx_map_fst] + rw [mappedEq] + simp [pure, StateT.pure, Except.pure] + +private theorem parseProgramSlots_printed (program : Program) + (inRange : program.ReferencesInRange) {initGroup : String × List Line} + {mainGroup : Option (String × List Line)} {others : List (String × List Line)} + (initEq : initGroup = ("init", functionBodyLines program program.init)) + (followingEq : mainGroup.toList ++ others = printedFollowingGroups program) + (isSomeEq : mainGroup.isSome = program.main.isSome) : + parseProgramSlots initGroup mainGroup others = .ok program.normalize := by + unfold parseProgramSlots + simp only [] + rw [followingEq, initEq, isSomeEq] + rw [show (("init", functionBodyLines program program.init) : String × List Line).fst :: + (printedFollowingGroups program).map Prod.fst = printedFunctionNames program from + (printedFunctionNames_cons program).symm] + rw [parseFunctionSlots_printed program inRange] + have renameEq : normalRename program.variableOccurrences = program.normalVariable := by + funext identifier + rfl + have restMap : + (program.rest.toList.map (·.renameVariables program.normalVariable)).toArray = + program.rest.map (·.renameVariables program.normalVariable) := by + cases program.rest + simp + cases mainEq : program.main with + | none => + simp [programOfSlots, Program.normalize, Program.renameVariables, mainEq, renameEq, + restMap] + | some main => + simp [programOfSlots, Program.normalize, Program.renameVariables, mainEq, renameEq, + restMap] + +private theorem parseProgramGroups_printed (program : Program) + (inRange : program.ReferencesInRange) : + parseProgramGroups (printedFunctionGroups program) = + .ok (program.normalize) := by + rw [parseProgramGroups] + rw [show (printedFunctionGroups program).map Prod.fst = + printedFunctionNames program by rfl] + rw [printedFunctionNames_noDuplicates program] + simp only [Bool.false_eq_true, if_false, bind, Except.bind, pure, Except.pure] + rw [find?_init_printed program] + exact parseProgramSlots_printed program inRange rfl + (find?_main_printed program).1 (find?_main_printed program).2 + +private theorem parseTokens_programTokens (program : Program) + (inRange : program.ReferencesInRange) : + parseTokens (programTokens program) = .ok program.normalize := by + rw [parseTokens, splitLines_programTokens, splitFunctions_programLines] + exact parseProgramGroups_printed program inRange + +private theorem parse_print_normalize_of_referencesInRange {program : Program} + (inRange : program.ReferencesInRange) : + parse (print program) = .ok program.normalize := by + rw [parse, Proofs.tokenize_print] + exact parseTokens_programTokens program inRange + +private theorem referencesInRange_of_wellFormed {program : Program} + (wellFormed : program.WellFormed) : program.ReferencesInRange := by + intro function member block blockMember + refine ⟨fun statement statementMember => ?_, ?_⟩ + · cases statement with + | icall callee args dests => + obtain ⟨outputs, ⟨target, targetEq, _⟩, _⟩ := + wellFormed.icallArity callee args dests + ⟨function, member, block, blockMember, statementMember⟩ + simp only [Program.function?, Array.getElem?_eq_some_iff] at targetEq + exact targetEq.1 + | _ => trivial + · have targets := wellFormed.validJumpTargets function member block blockMember + cases terminatorEq : block.terminator with + | jump target => + rw [terminatorEq] at targets + simp only [Terminator.jumpTargets, List.mem_singleton, forall_eq] at targets + obtain ⟨targetBlock, targetEq, _⟩ := targets + simp only [Function.block?, Array.getElem?_eq_some_iff] at targetEq + exact targetEq.1 + | branch condition thenTarget elseTarget => + rw [terminatorEq] at targets + simp only [Terminator.jumpTargets, List.mem_cons, List.not_mem_nil, + or_false] at targets + obtain ⟨thenBlock, thenEq, _⟩ := targets thenTarget (by simp) + obtain ⟨elseBlock, elseEq, _⟩ := targets elseTarget (by simp) + simp only [Function.block?, Array.getElem?_eq_some_iff] at thenEq elseEq + exact ⟨thenEq.1, elseEq.1⟩ + | halt => trivial + | iret => trivial + +namespace Proofs + +theorem parse_print_normalize {program : Program} (wellFormed : program.WellFormed) : + parse (print program) = .ok program.normalize := + parse_print_normalize_of_referencesInRange (referencesInRange_of_wellFormed wellFormed) + +theorem parse_print {source : String} {program : Program} + (parsed : parse source = .ok program) : + parse (print program) = .ok program := by + rw [parse_print_normalize_of_referencesInRange (parse_referencesInRange parsed), + parse_normal parsed] + +end Proofs +end Sir.Vars.Text diff --git a/sir/Sir/Text/Spec/Lexer.lean b/sir/Sir/Text/Spec/Lexer.lean new file mode 100644 index 00000000..34c6ef0b --- /dev/null +++ b/sir/Sir/Text/Spec/Lexer.lean @@ -0,0 +1,137 @@ +import Sir.Vars.Spec + +namespace Sir.Vars.Text + +inductive Token where + | identifier (name : String) + | label (name : String) + | number (value : Nat) + | equals + | arrow + | fatArrow + | colon + | question + | leftBrace + | rightBrace + | newline + | invalid (character : Char) +deriving DecidableEq, Repr, Inhabited + +def isIdentifierBody (character : Char) : Bool := + character.isAlphanum || character == '_' + +def isHexDigit (character : Char) : Bool := + character.isDigit || ('a' ≤ character && character ≤ 'f') || + ('A' ≤ character && character ≤ 'F') + +def digitValue (character : Char) : Nat := + if character.isDigit then character.toNat - '0'.toNat + else if character ≤ 'F' then character.toNat - 'A'.toNat + 10 + else character.toNat - 'a'.toNat + 10 + +def digitsValue (base : Nat) (digits : List Char) : Nat := + digits.foldl (fun value digit => value * base + digitValue digit) 0 + +def decimalDigitChar : Nat → Char + | 0 => '0' | 1 => '1' | 2 => '2' | 3 => '3' | 4 => '4' + | 5 => '5' | 6 => '6' | 7 => '7' | 8 => '8' | _ => '9' + +def decimalDigitsAux : Nat → Nat → List Char + | 0, value => [decimalDigitChar value] + | fuel + 1, value => + if value < 10 then [decimalDigitChar value] + else decimalDigitsAux fuel (value / 10) ++ [decimalDigitChar (value % 10)] + +def decimalDigits (value : Nat) : List Char := + decimalDigitsAux value value + +def decimalString (value : Nat) : String := + String.ofList (decimalDigits value) + +inductive Pending where + | idle + | word (characters : List Char) + | label (characters : List Char) + | lineComment + | blockComment + | blockCommentStar + +def wordToken : List Char → Token + | '0' :: 'x' :: digits => + if digits.isEmpty || !digits.all isHexDigit then .invalid '0' + else .number (digitsValue 16 digits) + | first :: rest => + if first.isDigit then + if (first :: rest).all Char.isDigit then .number (digitsValue 10 (first :: rest)) + else .invalid first + else .identifier (String.ofList (first :: rest)) + | [] => .invalid ' ' + +def flush : Pending → List Token + | .word characters => [wordToken characters.reverse] + | .label [] => [.invalid '@'] + | .label characters => [.label (String.ofList characters.reverse)] + | _ => [] + +def separatorTokens : Char → List Token + | '@' => [] + | '=' => [.equals] + | ':' => [.colon] + | '?' => [.question] + | '{' => [.leftBrace] + | '}' => [.rightBrace] + | '\n' => [.newline] + | ' ' | '\t' | '\r' => [] + | character => [.invalid character] + +def tokenizeAux : Pending → List Char → List Token + | pending, [] => flush pending + | .lineComment, '\n' :: rest => .newline :: tokenizeAux .idle rest + | .lineComment, _ :: rest => tokenizeAux .lineComment rest + | .blockComment, '*' :: rest => tokenizeAux .blockCommentStar rest + | .blockComment, '\n' :: rest => .newline :: tokenizeAux .blockComment rest + | .blockComment, _ :: rest => tokenizeAux .blockComment rest + | .blockCommentStar, '/' :: rest => tokenizeAux .idle rest + | .blockCommentStar, '*' :: rest => tokenizeAux .blockCommentStar rest + | .blockCommentStar, '\n' :: rest => .newline :: tokenizeAux .blockComment rest + | .blockCommentStar, _ :: rest => tokenizeAux .blockComment rest + | pending, '/' :: '/' :: rest => flush pending ++ tokenizeAux .lineComment rest + | pending, '/' :: '*' :: rest => flush pending ++ tokenizeAux .blockComment rest + | pending, '-' :: '>' :: rest => flush pending ++ .arrow :: tokenizeAux .idle rest + | pending, '=' :: '>' :: rest => flush pending ++ .fatArrow :: tokenizeAux .idle rest + | pending, character :: rest => + if isIdentifierBody character then + match pending with + | .word characters => tokenizeAux (.word (character :: characters)) rest + | .label characters => tokenizeAux (.label (character :: characters)) rest + | _ => tokenizeAux (.word [character]) rest + else + flush pending ++ separatorTokens character ++ + tokenizeAux (if character == '@' then .label [] else .idle) rest + +def tokenize (source : String) : List Token := + tokenizeAux .idle source.toList + +def Token.characters : Token → List Char + | .identifier name => name.toList + | .label name => '@' :: name.toList + | .number value => decimalDigits value + | .equals => ['='] + | .arrow => ['-', '>'] + | .fatArrow => ['=', '>'] + | .colon => [':'] + | .question => ['?'] + | .leftBrace => ['{'] + | .rightBrace => ['}'] + | .newline => ['\n'] + | .invalid character => [character] + +def renderChars : List Token → List Char + | [] => [] + | .newline :: rest => '\n' :: renderChars rest + | token :: rest => token.characters ++ ' ' :: renderChars rest + +def render (tokens : List Token) : String := + String.ofList (renderChars tokens) + +end Sir.Vars.Text diff --git a/sir/Sir/Text/Spec/Mnemonic.lean b/sir/Sir/Text/Spec/Mnemonic.lean new file mode 100644 index 00000000..b3e937af --- /dev/null +++ b/sir/Sir/Text/Spec/Mnemonic.lean @@ -0,0 +1,44 @@ +import Sir.Text.Spec.Lexer + +namespace Sir.Vars.Text + +structure Mnemonic where + name : String + results : Nat + operands : Nat + build : Vector VarId results → Vector VarId operands → Stmt + +def mnemonics : List Mnemonic := [ + ⟨"copy", 1, 1, fun r o => .assign r[0] (.var o[0])⟩, + ⟨"add", 1, 2, fun r o => .assign r[0] (.add o[0] o[1])⟩, + ⟨"lt", 1, 2, fun r o => .assign r[0] (.lt o[0] o[1])⟩, + ⟨"sload", 1, 1, fun r o => .assign r[0] (.sload o[0])⟩, + ⟨"sstore", 0, 2, fun _ o => .sstore o[0] o[1]⟩, + ⟨"gas", 1, 0, fun r _ => .gas r[0]⟩, + ⟨"call", 1, 2, fun r o => .call { callee := o[1], gas := o[0], result := r[0] }⟩, + ⟨"malloc", 1, 1, fun r o => .malloc r[0] o[0]⟩, + ⟨"mallocany", 1, 1, fun r o => .mallocUninit r[0] o[0]⟩, + ⟨"mstore256", 0, 2, fun _ o => .mstore32 o[0] o[1]⟩, + ⟨"mload256", 1, 1, fun r o => .mload32 r[0] o[0]⟩] + +structure Spelling where + name : String + results : List VarId + operands : List VarId + +def spelling : Stmt → Spelling + | .assign result (.constant _) => ⟨"const", [result], []⟩ + | .assign result (.var source) => ⟨"copy", [result], [source]⟩ + | .assign result (.add lhs rhs) => ⟨"add", [result], [lhs, rhs]⟩ + | .assign result (.lt lhs rhs) => ⟨"lt", [result], [lhs, rhs]⟩ + | .assign result (.sload key) => ⟨"sload", [result], [key]⟩ + | .sstore key value => ⟨"sstore", [], [key, value]⟩ + | .gas result => ⟨"gas", [result], []⟩ + | .call callData => ⟨"call", [callData.result], [callData.gas, callData.callee]⟩ + | .malloc result size => ⟨"malloc", [result], [size]⟩ + | .mallocUninit result size => ⟨"mallocany", [result], [size]⟩ + | .mstore32 offset value => ⟨"mstore256", [], [offset, value]⟩ + | .mload32 result offset => ⟨"mload256", [result], [offset]⟩ + | .icall _ args dests => ⟨"icall", dests.toList, args.toList⟩ + +end Sir.Vars.Text diff --git a/sir/Sir/Text/Spec/Parser.lean b/sir/Sir/Text/Spec/Parser.lean new file mode 100644 index 00000000..2652e689 --- /dev/null +++ b/sir/Sir/Text/Spec/Parser.lean @@ -0,0 +1,264 @@ +import Sir.Text.Spec.Mnemonic + +namespace Sir.Vars.Text + +abbrev Line := List Token + +def splitLinesAux (current : List Token) : List Token → List Line + | [] => if current.isEmpty then [] else [current.reverse] + | .newline :: rest => + if current.isEmpty then splitLinesAux [] rest + else current.reverse :: splitLinesAux [] rest + | token :: rest => splitLinesAux (token :: current) rest + +def splitLines (tokens : List Token) : List Line := + splitLinesAux [] tokens + +def describe (line : Line) : String := + render line + +abbrev ParserM := StateT (List String) (Except String) + +def internVariable (name : String) : ParserM VarId := do + let names ← get + match names.findIdx? (· == name) with + | some index => return ⟨index⟩ + | none => + set (names ++ [name]) + return ⟨names.length⟩ + +def temporaryName (identifier : VarId) : String := + "%" ++ decimalString identifier.id + +def freshVariable : ParserM VarId := do + let names ← get + set (names ++ [temporaryName ⟨names.length⟩]) + return ⟨names.length⟩ + +def liftNumbers : List Token → ParserM (List Stmt × List Token) + | [] => return ([], []) + | .number value :: rest => do + let target ← freshVariable + let (preludes, tokens) ← liftNumbers rest + return (.assign target (.constant (.ofNat value)) :: preludes, + .identifier (temporaryName target) :: tokens) + | token :: rest => do + let (preludes, tokens) ← liftNumbers rest + return (preludes, token :: tokens) + +def variableList : List Token → ParserM (Array VarId) + | [] => return #[] + | .identifier name :: rest => do + let head ← internVariable name + return #[head] ++ (← variableList rest) + | token :: _ => throw s!"expected a local name, got '{describe [token]}'" + +def operand : Token → ParserM (List Stmt × VarId) + | .identifier name => do return ([], ← internVariable name) + | .number value => do + let target ← freshVariable + return ([.assign target (.constant (.ofNat value))], target) + | token => throw s!"expected a local name or a number, got '{describe [token]}'" + +def operands : List Token → ParserM (List Stmt × Array VarId) + | [] => return ([], #[]) + | token :: rest => do + let (prelude, identifier) ← operand token + let (preludes, identifiers) ← operands rest + return (prelude ++ preludes, #[identifier] ++ identifiers) + +def parseInternalCall (functions : List String) (line : Line) (dests : List VarId) : + List Token → ParserM (List Stmt) + | .label calleeName :: args => do + let some calleeIndex := functions.findIdx? (· == calleeName) + | throw s!"unknown function '@{calleeName}'" + let (_, arguments) ← operands args + pure [.icall ⟨calleeIndex⟩ arguments dests.toArray] + | _ => throw s!"expected a function label in '{describe line}'" + +def parseOperation (line : Line) (mnemonic : String) (results : List VarId) + (parameters : List Token) : ParserM (List Stmt) := do + let some entry := mnemonics.find? (·.name == mnemonic) + | throw s!"unknown operation '{mnemonic}' in '{describe line}'" + if resultsOk : results.length = entry.results then + let (_, operandIds) ← operands parameters + if operandsOk : operandIds.size = entry.operands then + pure [entry.build ⟨results.toArray, by simpa using resultsOk⟩ + ⟨operandIds, operandsOk⟩] + else throw s!"'{mnemonic}' takes {entry.operands} operands in '{describe line}'" + else throw s!"'{mnemonic}' defines {entry.results} results in '{describe line}'" + +def parseMnemonic (functions : List String) (line : Line) (mnemonic : String) + (results : List VarId) (parameters : List Token) : ParserM (List Stmt) := + if mnemonic = "icall" then parseInternalCall functions line results parameters + else parseOperation line mnemonic results parameters + +def statementParts (line : Line) : List Token × List Token := + match line.span (· != .equals) with + | (before, .equals :: after) => (before, after) + | _ => ([], line) + +def parseStatement (functions : List String) (line : Line) : ParserM (List Stmt) := do + let (resultTokens, operandTokens) := statementParts line + match operandTokens with + | .identifier "const" :: parameters => do + let results ← variableList resultTokens + match results.toList, parameters with + | [result], [.number value] => + return [.assign result (.constant (.ofNat value))] + | _, _ => throw s!"unsupported operation '{describe line}'" + | .identifier mnemonic :: rawParameters => do + let (lifted, parameters) ← liftNumbers rawParameters + let results ← variableList resultTokens + let body ← parseMnemonic functions line mnemonic results.toList parameters + pure (lifted ++ body) + | _ => throw s!"expected an operation mnemonic in '{describe line}'" + +def resolveBlock (blocks : List String) (name : String) : ParserM BlockId := do + let some index := blocks.findIdx? (· == name) | throw s!"unknown block '@{name}'" + return ⟨index⟩ + +def parseTerminator (blocks : List String) : Line → ParserM Terminator + | [.identifier "stop"] => return .halt + | [.identifier "iret"] => return .iret + | [.fatArrow, .label target] => return .jump (← resolveBlock blocks target) + | [.fatArrow, .identifier condition, .question, .label thenTarget, .colon, + .label elseTarget] => do + return .branch (← internVariable condition) (← resolveBlock blocks thenTarget) + (← resolveBlock blocks elseTarget) + | line => throw s!"expected a terminator, got '{describe line}'" + +def parseBlockBody (functions blocks : List String) : + List Line → ParserM (Array Stmt × Terminator) + | [] => throw "a block must end with a terminator" + | [line] => do return (#[], ← parseTerminator blocks line) + | line :: rest => do + let statements ← parseStatement functions line + let (following, terminator) ← parseBlockBody functions blocks rest + return (statements.toArray ++ following, terminator) + +def parseBlockHeader : Line → ParserM (Array VarId × Array VarId) + | .identifier _ :: rest => + match rest.reverse with + | .leftBrace :: reversedSignature => do + let signature := reversedSignature.reverse + let (inputTokens, outputTokens) := + match signature.span (· != .arrow) with + | (before, .arrow :: after) => (before, after) + | _ => (signature, []) + return (← variableList inputTokens, ← variableList outputTokens) + | _ => throw "expected '{' at the end of a block header" + | line => throw s!"expected a block header, got '{describe line}'" + +def parseBlock (functions blocks : List String) (header : Line) (body : List Line) : + ParserM Block := do + let (inputs, outputs) ← parseBlockHeader header + let (statements, terminator) ← parseBlockBody functions blocks body + return { inputs := inputs, statements := statements, terminator := terminator, + outputs := outputs } + +def blockHeaderName : Line → Except String String + | .identifier name :: _ => .ok name + | line => .error s!"expected a block header, got '{describe line}'" + +def isBlockHeader (line : Line) : Bool := + line.getLast? == some Token.leftBrace + +def splitBlocksAux (groups : List (Line × List Line)) (isOpen : Bool) : + List Line → Except String (List (Line × List Line)) + | [] => + if isOpen then .error "a block is missing its '}'" + else .ok (groups.reverse.map fun group => (group.fst, group.snd.reverse)) + | line :: rest => + if isOpen then + if line == [Token.rightBrace] then splitBlocksAux groups false rest + else + match groups with + | [] => .error s!"unexpected line '{describe line}'" + | (header, body) :: others => + splitBlocksAux ((header, line :: body) :: others) true rest + else if isBlockHeader line then splitBlocksAux ((line, []) :: groups) true rest + else .error s!"expected a block header, got '{describe line}'" + +def splitBlocks (lines : List Line) : Except String (List (Line × List Line)) := + splitBlocksAux [] false lines + +def splitFunctionsAux (groups : List (String × List Line)) : + List Line → Except String (List (String × List Line)) + | [] => .ok (groups.reverse.map fun group => (group.fst, group.snd.reverse)) + | line :: rest => + match line with + | [.identifier "fn", .identifier name, .colon] => + splitFunctionsAux ((name, []) :: groups) rest + | _ => + match groups with + | [] => .error s!"expected a function header, got '{describe line}'" + | (name, body) :: others => splitFunctionsAux ((name, line :: body) :: others) rest + +def splitFunctions (lines : List Line) : Except String (List (String × List Line)) := + splitFunctionsAux [] lines + +def hasDuplicates : List String → Bool + | [] => false + | name :: rest => rest.contains name || hasDuplicates rest + +def parseFunctionGroups (functions : List String) (groups : List (Line × List Line)) : + ParserM Function := do + let blocks ← liftM (groups.mapM fun group => blockHeaderName group.fst) + if hasDuplicates blocks then throw "duplicate block name" + let parsed ← groups.mapM fun group => parseBlock functions blocks group.fst group.snd + match parsed with + | [] => throw "a function must have at least one block" + | entry :: rest => return { entry := entry, rest := rest.toArray } + +def parseFunction (functions : List String) (body : List Line) : ParserM Function := + match splitBlocks body with + | .error message => throw message + | .ok groups => parseFunctionGroups functions groups + +def parseFunctionGroupsList (names : List String) (groups : List (String × List Line)) : + ParserM (List Function) := + groups.mapM fun group => parseFunction names group.snd + +def parseFunctionSlots (names : List String) (initGroup : String × List Line) + (following : List (String × List Line)) : ParserM (Function × List Function) := do + let init ← parseFunction names initGroup.snd + let parsed ← parseFunctionGroupsList names following + return (init, parsed) + +def programOfSlots (hasMain : Bool) (init : Function) (following : List Function) : Program := + if hasMain then + { init := init, main := following.head?, rest := following.tail.toArray } + else + { init := init, main := none, rest := following.toArray } + +def parseProgramSlots (initGroup : String × List Line) + (mainGroup : Option (String × List Line)) + (others : List (String × List Line)) : Except String Program := + let following := mainGroup.toList ++ others + match (parseFunctionSlots (initGroup.fst :: following.map Prod.fst) + initGroup following).run [] with + | .error message => .error message + | .ok result => .ok (programOfSlots mainGroup.isSome result.1.1 result.1.2) + +def parseProgramGroups (groups : List (String × List Line)) : Except String Program := do + let names := groups.map Prod.fst + if hasDuplicates names then .error "duplicate function name" + let some initGroup := groups.find? (fun group => group.fst == "init") + | .error "the program has no function named 'init'" + parseProgramSlots initGroup (groups.find? (fun group => group.fst == "main")) + (groups.filter (fun group => group.fst != "init" && group.fst != "main")) + +def parseTokens (tokens : List Token) : Except String Program := + match splitFunctions (splitLines tokens) with + | .error message => .error message + | .ok groups => parseProgramGroups groups + +def parse (source : String) : Except String Program := + parseTokens (tokenize source) + +-- Smart unfolding copies the unreduced lexer term once per unfolding attempt; delta does not. +macro "parse_rfl" : tactic => + `(tactic| set_option smartUnfolding false in set_option maxRecDepth 100000 in rfl) + +end Sir.Vars.Text diff --git a/sir/Sir/Text/Spec/Printer.lean b/sir/Sir/Text/Spec/Printer.lean new file mode 100644 index 00000000..3c22c1a9 --- /dev/null +++ b/sir/Sir/Text/Spec/Printer.lean @@ -0,0 +1,64 @@ +import Sir.Text.Spec.Mnemonic + +namespace Sir.Vars.Text + +def functionName (program : Program) (function : FunctionId) : String := + if function = program.initId then "init" + else if program.mainId? = some function then "main" + else "fn" ++ decimalString function.id + +def blockName (block : BlockId) : String := + "block" ++ decimalString block.id + +def variableName (identifier : VarId) : String := + "v" ++ decimalString identifier.id + +def variableToken (identifier : VarId) : Token := + .identifier (variableName identifier) + +def variableTokens (identifiers : Array VarId) : List Token := + identifiers.toList.map variableToken + +def definitionTokens (results : List VarId) : List Token := + if results.isEmpty then [] else results.map variableToken ++ [.equals] + +def immediateTokens (program : Program) : Stmt → List Token + | .assign _ (.constant value) => [.number value.toNat] + | .icall callee _ _ => [.label (functionName program callee)] + | _ => [] + +def stmtTokens (program : Program) (statement : Stmt) : List Token := + definitionTokens (spelling statement).results ++ + .identifier (spelling statement).name :: + (immediateTokens program statement ++ (spelling statement).operands.map variableToken) + +def terminatorTokens : Terminator → List Token + | .halt => [.identifier "stop"] + | .iret => [.identifier "iret"] + | .jump target => [.fatArrow, .label (blockName target)] + | .branch condition thenTarget elseTarget => + [.fatArrow, variableToken condition, .question, .label (blockName thenTarget), + .colon, .label (blockName elseTarget)] + +def blockTokens (program : Program) (identifier : BlockId) (block : Block) : + List Token := + [.identifier (blockName identifier)] ++ variableTokens block.inputs ++ + (if block.outputs.isEmpty then [] else .arrow :: variableTokens block.outputs) ++ + [.leftBrace, .newline] ++ + (block.statements.toList.flatMap fun statement => stmtTokens program statement ++ [.newline]) ++ + terminatorTokens block.terminator ++ [.newline, .rightBrace, .newline] + +def functionTokens (program : Program) (identifier : FunctionId) (function : Function) : + List Token := + [.identifier "fn", .identifier (functionName program identifier), .colon, .newline] ++ + (function.blocks.toList.zipIdx.flatMap fun (block, index) => + blockTokens program ⟨index⟩ block) + +def programTokens (program : Program) : List Token := + program.functions.toList.zipIdx.flatMap fun (function, index) => + functionTokens program ⟨index⟩ function + +def print (program : Program) : String := + render (programTokens program) + +end Sir.Vars.Text diff --git a/sir/Sir/Text/Theorems.lean b/sir/Sir/Text/Theorems.lean new file mode 100644 index 00000000..f559772c --- /dev/null +++ b/sir/Sir/Text/Theorems.lean @@ -0,0 +1,22 @@ +import Sir.Text.Proofs.RoundTrip + +namespace Sir.Vars.Text + +theorem tokenize_print (program : Program) : + tokenize (print program) = programTokens program := + Proofs.tokenize_print program + +theorem parse_normal {source : String} {program : Program} + (parsed : parse source = .ok program) : program.Normal := + Proofs.parse_normal parsed + +theorem parse_print_normalize {program : Program} (wellFormed : program.WellFormed) : + parse (print program) = .ok program.normalize := + Proofs.parse_print_normalize wellFormed + +theorem parse_print {source : String} {program : Program} + (parsed : parse source = .ok program) : + parse (print program) = .ok program := + Proofs.parse_print parsed + +end Sir.Vars.Text diff --git a/sir/Sir/Theorems.lean b/sir/Sir/Theorems.lean index 29527078..d380e1bb 100644 --- a/sir/Sir/Theorems.lean +++ b/sir/Sir/Theorems.lean @@ -2,3 +2,4 @@ import Sir.Machine.Theorems import Sir.Vars.Theorems import Sir.Stack.Theorems import Sir.Lowering.Theorems +import Sir.Text.Theorems diff --git a/sir/Sir/Vars/Proofs/Check.lean b/sir/Sir/Vars/Proofs/Check.lean new file mode 100644 index 00000000..cd0d3251 --- /dev/null +++ b/sir/Sir/Vars/Proofs/Check.lean @@ -0,0 +1,140 @@ +import Sir.Vars.Spec.Check +import Sir.Vars.Proofs.Rank + +namespace Sir.Vars.Proofs + +theorem lt_size_of_getElem? {α : Type} {xs : Array α} {index : Nat} {x : α} + (h : xs[index]? = some x) : index < xs.size := by + by_contra hle + rw [Array.getElem?_eq_none (Nat.le_of_not_lt hle)] at h + simp at h + +theorem bind_eq_ok {α β : Type} {x : CheckM α} {f : α → CheckM β} {b : β} + (h : (x >>= f) = .ok b) : ∃ a, x = .ok a ∧ f a = .ok b := by + cases x with + | error d => simp [Bind.bind, Except.bind] at h + | ok a => exact ⟨a, rfl, h⟩ + +theorem ensure_eq_ok {d : Diagnostic} {b : Bool} (h : ensure d b = .ok ()) : b = true := by + cases b with + | true => rfl + | false => simp [ensure] at h + +theorem checkList_eq_ok {α : Type} {check : α → CheckM Unit} : + {xs : List α} → checkList check xs = .ok () → ∀ x ∈ xs, check x = .ok () + | [], _, _, hx => by simp at hx + | x :: rest, h, y, hy => by + obtain ⟨_, hx, hrest⟩ := bind_eq_ok h + rcases List.mem_cons.mp hy with rfl | hy + · exact hx + · exact checkList_eq_ok hrest y hy + +theorem checkArray_eq_ok {α : Type} {check : α → CheckM Unit} {xs : Array α} + (h : checkArray check xs = .ok ()) : ∀ x ∈ xs, check x = .ok () := + fun x hx => checkList_eq_ok h x (Array.mem_toList_iff.mpr hx) + +theorem checkBlocks_eq_ok {p : Program} {check : Function → Block → CheckM Unit} + (h : checkBlocks p check = .ok ()) : + ∀ fn ∈ p.functions, ∀ block ∈ fn.blocks, check fn block = .ok () := + fun fn hfn block hblock => checkArray_eq_ok (checkArray_eq_ok h fn hfn) block hblock + +theorem icallArity_of_check {p : Program} (h : checkIcallArity p = .ok ()) : + ∀ callee args dests, p.HasStmt (.icall callee args dests) → + ∃ outputs, p.FunctionInputOutputArity args.size outputs callee ∧ + outputs.getD 0 = dests.size := by + rintro callee args dests ⟨fn, hfn, block, hblock, hstmt⟩ + have hcheck := checkArray_eq_ok (checkBlocks_eq_ok h fn hfn block hblock) _ hstmt + simp only [checkIcallArityStmt] at hcheck + split at hcheck + · simp at hcheck + · rename_i target htarget + have := ensure_eq_ok hcheck + simp only [Bool.and_eq_true, beq_iff_eq] at this + exact ⟨target.outputs?, ⟨target, htarget, this.1, rfl⟩, this.2⟩ + +theorem iretArity_of_check {p : Program} (h : checkIretArity p = .ok ()) : + ∀ fn ∈ p.functions, ∀ block ∈ fn.blocks, + block.terminator = .iret → some block.outputs.size = fn.outputs? := by + intro fn hfn block hblock hiret + have hcheck := checkBlocks_eq_ok h fn hfn block hblock + unfold checkIretArityBlock at hcheck + rw [hiret] at hcheck + simpa using ensure_eq_ok hcheck + +theorem rankDecreases_of_check {p : Program} {rank : FunctionId → Nat} + (h : checkRankDecreases p rank = .ok ()) : RankDecreases p rank := by + rintro f g ⟨args, dests, fn, hfn, block, hblock, hstmt⟩ + have hlt : f.id < p.functions.size := lt_size_of_getElem? hfn + have hblocks : p.blocksOf f = fn.blocks := by simp [Program.blocksOf, hfn] + have hcheck := checkArray_eq_ok + (checkArray_eq_ok (checkList_eq_ok h f.id (List.mem_range.mpr hlt)) block (hblocks ▸ hblock)) + _ hstmt + simpa [checkRankStmt] using ensure_eq_ok hcheck + +theorem acyclicCalls_of_check {p : Program} (h : checkAcyclicCalls p = .ok ()) : + ∀ f, ¬ Relation.TransGen p.callEdge f f := + acyclic_of_rank (rankDecreases_of_check h) + +theorem entryFunction_of_check {function : FunctionId} {fn : Function} + (h : checkEntryFunction function fn = .ok ()) : + fn.paramsOf.size = 0 ∧ fn.outputs? = none := by + simpa [Bool.and_eq_true, Option.isNone_iff_eq_none] using ensure_eq_ok h + +theorem entryArity_of_check {p : Program} (h : checkEntryArity p = .ok ()) : + (p.init.paramsOf.size = 0 ∧ p.init.outputs? = none) ∧ + ∀ m, p.main = some m → m.paramsOf.size = 0 ∧ m.outputs? = none := by + obtain ⟨_, hinit, hmain⟩ := bind_eq_ok h + refine ⟨entryFunction_of_check hinit, fun m hm => ?_⟩ + rw [hm] at hmain + exact entryFunction_of_check hmain + +theorem validJumpTargets_of_check {p : Program} (h : checkValidJumpTargets p = .ok ()) : + ∀ fn ∈ p.functions, + ∀ block ∈ fn.blocks, ∀ target ∈ block.terminator.jumpTargets, + ∃ targetBlock, fn.block? target = some targetBlock ∧ + targetBlock.inputs.size = block.outputs.size := by + intro fn hfn block hblock target htarget + have hcheck := checkList_eq_ok (checkBlocks_eq_ok h fn hfn block hblock) target htarget + unfold checkJumpTarget at hcheck + split at hcheck + · simp at hcheck + · rename_i targetBlock hblock? + exact ⟨targetBlock, hblock?, by simpa using ensure_eq_ok hcheck⟩ + +theorem Block.variablesDefinedBeforeUse_of_undefinedUse? {block : Block} + (h : block.undefinedUse? = none) : block.VariablesDefinedBeforeUse := by + unfold Block.undefinedUse? at h + split at h + · simp at h + · rename_i hstatements + refine ⟨fun index statement hstatement identifier hread => ?_, fun identifier hread => ?_⟩ + · have hindex := List.findSome?_eq_none_iff.mp hstatements index + (List.mem_range.mpr (lt_size_of_getElem? hstatement)) + rw [hstatement] at hindex + simpa using List.find?_eq_none.mp hindex identifier hread + · simpa using List.find?_eq_none.mp h identifier hread + +theorem variablesDefinedBeforeUse_of_check {p : Program} + (h : checkVariablesDefinedBeforeUse p = .ok ()) : + ∀ fn ∈ p.functions, ∀ block ∈ fn.blocks, block.VariablesDefinedBeforeUse := by + intro fn hfn block hblock + have hcheck := checkBlocks_eq_ok h fn hfn block hblock + split at hcheck + · simp at hcheck + · exact Block.variablesDefinedBeforeUse_of_undefinedUse? (by assumption) + +theorem Program.wellFormed_of_check {p : Program} (h : checkWellFormed p = .ok ()) : + p.WellFormed := by + obtain ⟨_, hicall, h⟩ := bind_eq_ok h + obtain ⟨_, hiret, h⟩ := bind_eq_ok h + obtain ⟨_, hacyclic, h⟩ := bind_eq_ok h + obtain ⟨_, hentry, h⟩ := bind_eq_ok h + obtain ⟨_, hjump, hvars⟩ := bind_eq_ok h + exact { icallArity := icallArity_of_check hicall + iretArity := iretArity_of_check hiret + acyclicCalls := acyclicCalls_of_check hacyclic + entryArity := entryArity_of_check hentry + validJumpTargets := validJumpTargets_of_check hjump + variablesDefinedBeforeUse := variablesDefinedBeforeUse_of_check hvars } + +end Sir.Vars.Proofs diff --git a/sir/Sir/Vars/Proofs/Normalize.lean b/sir/Sir/Vars/Proofs/Normalize.lean new file mode 100644 index 00000000..a1eb9345 --- /dev/null +++ b/sir/Sir/Vars/Proofs/Normalize.lean @@ -0,0 +1,404 @@ +import Sir.Vars.Spec.Normalize + +namespace Sir.Vars.Proofs + +@[simp] theorem Expr.renameVariables_id (value : Expr) : + value.renameVariables id = value := by + cases value <;> rfl + +@[simp] theorem Expr.renameVariables_compose (outer inner : VarId → VarId) (value : Expr) : + (value.renameVariables inner).renameVariables outer = + value.renameVariables (outer ∘ inner) := by + cases value <;> rfl + +@[simp] theorem Stmt.renameVariables_id (statement : Stmt) : + statement.renameVariables id = statement := by + cases statement <;> simp [Stmt.renameVariables] + +@[simp] theorem Stmt.renameVariables_compose (outer inner : VarId → VarId) + (statement : Stmt) : + (statement.renameVariables inner).renameVariables outer = + statement.renameVariables (outer ∘ inner) := by + cases statement <;> simp [Stmt.renameVariables, Function.comp_def] + +@[simp] theorem Terminator.renameVariables_id (terminator : Terminator) : + terminator.renameVariables id = terminator := by + cases terminator <;> rfl + +@[simp] theorem Terminator.renameVariables_compose (outer inner : VarId → VarId) + (terminator : Terminator) : + (terminator.renameVariables inner).renameVariables outer = + terminator.renameVariables (outer ∘ inner) := by + cases terminator <;> rfl + +@[simp] theorem Block.renameVariables_id (block : Block) : + block.renameVariables id = block := by + have hstatement : Stmt.renameVariables id = id := funext Stmt.renameVariables_id + cases block + simp [Block.renameVariables, hstatement] + +@[simp] theorem Block.renameVariables_compose (outer inner : VarId → VarId) + (block : Block) : + (block.renameVariables inner).renameVariables outer = + block.renameVariables (outer ∘ inner) := by + cases block + simp [Block.renameVariables, Function.comp_def] + +@[simp] theorem Function.renameVariables_id (function : Function) : + function.renameVariables id = function := by + have hblock : Block.renameVariables id = id := funext Block.renameVariables_id + cases function + simp [Function.renameVariables, hblock] + +@[simp] theorem Function.renameVariables_compose (outer inner : VarId → VarId) + (function : Function) : + (function.renameVariables inner).renameVariables outer = + function.renameVariables (outer ∘ inner) := by + cases function + simp [Function.renameVariables, Function.comp_def] + +@[simp] theorem Function.blocks_renameVariables (rename : VarId → VarId) + (function : Function) : + (function.renameVariables rename).blocks = + function.blocks.map (Block.renameVariables rename) := by + simp [Function.renameVariables, Function.blocks] + +@[simp] theorem Program.functions_renameVariables (rename : VarId → VarId) + (program : Program) : + (program.renameVariables rename).functions = + program.functions.map (Function.renameVariables rename) := by + rcases program with ⟨init, main, rest⟩ + cases main <;> simp [Program.renameVariables, Program.functions] + +theorem Program.renameVariables_id (program : Program) : + program.renameVariables id = program := by + have hfunction : Function.renameVariables id = id := funext Function.renameVariables_id + cases program + simp [Program.renameVariables, hfunction] + +theorem Program.renameVariables_compose (outer inner : VarId → VarId) (program : Program) : + (program.renameVariables inner).renameVariables outer = + program.renameVariables (outer ∘ inner) := by + cases program + simp [Program.renameVariables, Function.comp_def] + +@[simp] theorem Expr.variableOccurrences_renameVariables (rename : VarId → VarId) + (value : Expr) : + (value.renameVariables rename).variableOccurrences = + value.variableOccurrences.map rename := by + cases value <;> rfl + +@[simp] theorem Stmt.variableOccurrences_renameVariables (rename : VarId → VarId) + (statement : Stmt) : + (statement.renameVariables rename).variableOccurrences = + statement.variableOccurrences.map rename := by + cases statement <;> simp [Stmt.renameVariables, Stmt.variableOccurrences] + +@[simp] theorem Terminator.variableOccurrences_renameVariables (rename : VarId → VarId) + (terminator : Terminator) : + (terminator.renameVariables rename).variableOccurrences = + terminator.variableOccurrences.map rename := by + cases terminator <;> rfl + +@[simp] theorem Block.variableOccurrences_renameVariables (rename : VarId → VarId) + (block : Block) : + (block.renameVariables rename).variableOccurrences = + block.variableOccurrences.map rename := by + cases block + simp [Block.renameVariables, Block.variableOccurrences, List.map_append, + List.map_flatMap, List.flatMap_map] + +@[simp] theorem Function.variableOccurrences_renameVariables (rename : VarId → VarId) + (function : Function) : + (function.renameVariables rename).variableOccurrences = + function.variableOccurrences.map rename := by + simp [Function.variableOccurrences, List.map_flatMap, List.flatMap_map] + +@[simp] theorem Program.variableOccurrences_renameVariables (rename : VarId → VarId) + (program : Program) : + (program.renameVariables rename).variableOccurrences = + program.variableOccurrences.map rename := by + simp [Program.variableOccurrences, List.map_flatMap, List.flatMap_map] + +theorem Expr.renameVariables_congr {left right : VarId → VarId} {value : Expr} + (h : ∀ identifier ∈ value.variableOccurrences, left identifier = right identifier) : + value.renameVariables left = value.renameVariables right := by + cases value <;> simp_all [Expr.renameVariables, Expr.variableOccurrences] + +theorem Stmt.renameVariables_congr {left right : VarId → VarId} {statement : Stmt} + (h : ∀ identifier ∈ statement.variableOccurrences, + left identifier = right identifier) : + statement.renameVariables left = statement.renameVariables right := by + cases statement with + | assign result value => + have hresult := h result (by simp [Stmt.variableOccurrences]) + have hvalue : value.renameVariables left = value.renameVariables right := by + apply Expr.renameVariables_congr + intro identifier hidentifier + exact h identifier (by simp [Stmt.variableOccurrences, hidentifier]) + simp [Stmt.renameVariables, hresult, hvalue] + | sstore key value => simp_all [Stmt.renameVariables, Stmt.variableOccurrences] + | gas result => simp_all [Stmt.renameVariables, Stmt.variableOccurrences] + | call callData => + simp_all [Stmt.renameVariables, Stmt.variableOccurrences] + | malloc result size | mallocUninit result size => + simp_all [Stmt.renameVariables, Stmt.variableOccurrences] + | mstore32 offset value => simp_all [Stmt.renameVariables, Stmt.variableOccurrences] + | mload32 result offset => simp_all [Stmt.renameVariables, Stmt.variableOccurrences] + | icall callee args dests => + have hargs : args.map left = args.map right := by + apply Array.map_congr_left + intro identifier hidentifier + exact h identifier (by simp [Stmt.variableOccurrences, hidentifier]) + have hdests : dests.map left = dests.map right := by + apply Array.map_congr_left + intro identifier hidentifier + exact h identifier (by simp [Stmt.variableOccurrences, hidentifier]) + simp [Stmt.renameVariables, hargs, hdests] + +theorem Terminator.renameVariables_congr {left right : VarId → VarId} + {terminator : Terminator} + (h : ∀ identifier ∈ terminator.variableOccurrences, + left identifier = right identifier) : + terminator.renameVariables left = terminator.renameVariables right := by + cases terminator <;> + simp_all [Terminator.renameVariables, Terminator.variableOccurrences] + +theorem Block.renameVariables_congr {left right : VarId → VarId} + {block : Block} + (h : ∀ identifier ∈ block.variableOccurrences, + left identifier = right identifier) : + block.renameVariables left = block.renameVariables right := by + have hinputs : block.inputs.map left = block.inputs.map right := by + apply Array.map_congr_left + intro identifier hidentifier + exact h identifier (by simp [Block.variableOccurrences, hidentifier]) + have hstatements : block.statements.map (Stmt.renameVariables left) = + block.statements.map (Stmt.renameVariables right) := by + apply Array.map_congr_left + intro statement hstatement + apply Stmt.renameVariables_congr + intro identifier hidentifier + have hstatement' : statement ∈ block.statements.toList := by simpa using hstatement + exact h identifier (by + simp only [Block.variableOccurrences, List.mem_append, List.mem_flatMap] + exact Or.inl (Or.inr ⟨statement, hstatement', hidentifier⟩)) + have hterminator : block.terminator.renameVariables left = + block.terminator.renameVariables right := by + apply Terminator.renameVariables_congr + intro identifier hidentifier + exact h identifier (by simp [Block.variableOccurrences, hidentifier]) + have houtputs : block.outputs.map left = block.outputs.map right := by + apply Array.map_congr_left + intro identifier hidentifier + exact h identifier (by simp [Block.variableOccurrences, hidentifier]) + simp [Block.renameVariables, hinputs, hstatements, hterminator, houtputs] + +theorem Function.renameVariables_congr {left right : VarId → VarId} + {function : Function} + (h : ∀ identifier ∈ function.variableOccurrences, + left identifier = right identifier) : + function.renameVariables left = function.renameVariables right := by + have hblock : ∀ block ∈ function.blocks, + block.renameVariables left = block.renameVariables right := by + intro block hblock + apply Block.renameVariables_congr + intro identifier hidentifier + have hblock' : block ∈ function.blocks.toList := by simpa using hblock + exact h identifier (by + simp only [Function.variableOccurrences, List.mem_flatMap] + exact ⟨block, hblock', hidentifier⟩) + have hentry : function.entry.renameVariables left = + function.entry.renameVariables right := + hblock function.entry (by simp [Function.blocks]) + have hrest : function.rest.map (Block.renameVariables left) = + function.rest.map (Block.renameVariables right) := by + apply Array.map_congr_left + intro block hblock' + exact hblock block (by simp [Function.blocks, hblock']) + simp [Function.renameVariables, hentry, hrest] + +theorem Program.renameVariables_congr {left right : VarId → VarId} {program : Program} + (h : ∀ identifier ∈ program.variableOccurrences, + left identifier = right identifier) : + program.renameVariables left = program.renameVariables right := by + have hfunction : ∀ function ∈ program.functions, + function.renameVariables left = function.renameVariables right := by + intro function hfunction + apply Function.renameVariables_congr + intro identifier hidentifier + have hfunction' : function ∈ program.functions.toList := by simpa using hfunction + exact h identifier (by + simp only [Program.variableOccurrences, List.mem_flatMap] + exact ⟨function, hfunction', hidentifier⟩) + have hinit : program.init.renameVariables left = program.init.renameVariables right := + hfunction program.init (by simp [Program.functions]) + have hmain : program.main.map (Function.renameVariables left) = + program.main.map (Function.renameVariables right) := by + cases hmainEq : program.main with + | none => rfl + | some function => + simp [hfunction function (by simp [Program.functions, hmainEq])] + have hrest : program.rest.map (Function.renameVariables left) = + program.rest.map (Function.renameVariables right) := by + apply Array.map_congr_left + intro function hfunction' + exact hfunction function (by simp [Program.functions, hfunction']) + simp [Program.renameVariables, hinit, hmain, hrest] + +private theorem eraseDups_map_of_injective_on {rename : VarId → VarId} + {identifiers : List VarId} + (hinjective : ∀ left ∈ identifiers, ∀ right ∈ identifiers, + rename left = rename right → left = right) : + (identifiers.map rename).eraseDups = identifiers.eraseDups.map rename := by + match identifiers with + | [] => rfl + | head :: tail => + have htail : ∀ left ∈ tail, ∀ right ∈ tail, + rename left = rename right → left = right := by + intro left hleft right hright hequal + exact hinjective left (by simp [hleft]) right (by simp [hright]) hequal + have hfilter : + (tail.map rename).filter (fun identifier => !identifier == rename head) = + (tail.filter fun identifier => !identifier == head).map rename := by + rw [List.filter_map] + apply congrArg (List.map rename) + apply List.filter_congr + intro identifier hidentifier + by_cases hequal : identifier = head + · subst identifier + simp + · have hrenamed : rename identifier ≠ rename head := by + intro hrename + exact hequal (hinjective identifier (by simp [hidentifier]) head (by simp) hrename) + simp [Function.comp_apply, beq_eq_false_iff_ne.mpr hequal, + beq_eq_false_iff_ne.mpr hrenamed] + rw [List.eraseDups_cons, List.map_cons, List.eraseDups_cons, hfilter] + congr 1 + apply eraseDups_map_of_injective_on + intro left hleft right hright hequal + exact htail left (List.mem_of_mem_filter hleft) right + (List.mem_of_mem_filter hright) hequal +termination_by identifiers.length +decreasing_by + simpa using Nat.lt_succ_of_le (List.length_filter_le _ tail) + +private theorem idxOf_map_of_injective_on {rename : VarId → VarId} + {identifiers : List VarId} {identifier : VarId} + (hidentifier : identifier ∈ identifiers) + (hinjective : ∀ left ∈ identifiers, ∀ right ∈ identifiers, + rename left = rename right → left = right) : + (identifiers.map rename).idxOf (rename identifier) = identifiers.idxOf identifier := by + induction identifiers with + | nil => simp_all + | cons head tail induction => + by_cases hequal : head = identifier + · subst head + simp + · have hrename : rename head ≠ rename identifier := by + intro hrenamed + exact hequal (hinjective head (by simp) identifier hidentifier hrenamed) + have hinTail : identifier ∈ tail := by + simp only [List.mem_cons] at hidentifier + exact hidentifier.resolve_left (fun equality => hequal equality.symm) + rw [List.map_cons, List.idxOf_cons, List.idxOf_cons, + beq_eq_false_iff_ne.mpr hrename, + beq_eq_false_iff_ne.mpr hequal] + apply congrArg (fun index => index + 1) + apply induction hinTail + intro left hleft right hright hrenamed + exact hinjective left (by simp [hleft]) right (by simp [hright]) hrenamed + +theorem Program.AlphaEquiv.refl (program : Program) : Program.AlphaEquiv program program := by + exact ⟨id, id, Program.renameVariables_id program, Program.renameVariables_id program⟩ + +theorem Program.AlphaEquiv.symm {left right : Program} : + Program.AlphaEquiv left right → Program.AlphaEquiv right left := by + rintro ⟨forward, backward, hforward, hbackward⟩ + exact ⟨backward, forward, hbackward, hforward⟩ + +theorem Program.AlphaEquiv.trans {first second third : Program} : + Program.AlphaEquiv first second → Program.AlphaEquiv second third → + Program.AlphaEquiv first third := by + rintro ⟨forward₁, backward₁, hforward₁, hbackward₁⟩ + ⟨forward₂, backward₂, hforward₂, hbackward₂⟩ + refine ⟨forward₂ ∘ forward₁, backward₁ ∘ backward₂, ?_, ?_⟩ + · rw [← Program.renameVariables_compose, hforward₁, hforward₂] + · rw [← Program.renameVariables_compose, hbackward₂, hbackward₁] + +theorem Program.normalize_alphaEquiv (program : Program) : + Program.AlphaEquiv program.normalize program := by + let identifiers := program.variableOccurrences.eraseDups + let restore : VarId → VarId := fun identifier => + identifiers.getD identifier.id ⟨0⟩ + refine ⟨restore, program.normalVariable, ?_, rfl⟩ + rw [Program.normalize, Program.renameVariables_compose] + calc + program.renameVariables (restore ∘ program.normalVariable) = + program.renameVariables id := by + apply Program.renameVariables_congr + intro identifier hidentifier + simp only [Function.comp_apply, id_eq] + have hinIdentifiers : identifier ∈ identifiers := by + exact List.mem_eraseDups.mpr hidentifier + have hindex := List.idxOf_lt_length_of_mem hinIdentifiers + change identifiers.getD (identifiers.idxOf identifier) ⟨0⟩ = identifier + rw [← List.getElem_eq_getD (h := hindex) ⟨0⟩] + exact List.getElem_idxOf hindex + _ = program := Program.renameVariables_id program + +private theorem normalVariable_renameVariables {left right : Program} + {rename : VarId → VarId} + (hrenamed : left.renameVariables rename = right) + (hinjective : ∀ first ∈ left.variableOccurrences, + ∀ second ∈ left.variableOccurrences, + rename first = rename second → first = second) + {identifier : VarId} (hidentifier : identifier ∈ left.variableOccurrences) : + right.normalVariable (rename identifier) = left.normalVariable identifier := by + have hoccurrences := congrArg Program.variableOccurrences hrenamed + rw [Program.variableOccurrences_renameVariables] at hoccurrences + simp only [Program.normalVariable] + rw [← hoccurrences] + rw [eraseDups_map_of_injective_on hinjective] + apply congrArg VarId.mk + apply idxOf_map_of_injective_on + · exact List.mem_eraseDups.mpr hidentifier + · intro first hfirst second hsecond hequal + exact hinjective first (List.mem_eraseDups.mp hfirst) second + (List.mem_eraseDups.mp hsecond) hequal + +theorem Program.alphaEquiv_iff_normalize_eq {left right : Program} : + Program.AlphaEquiv left right ↔ left.normalize = right.normalize := by + constructor + · rintro ⟨forward, backward, hforward, hbackward⟩ + have hforwardOccurrences := congrArg Program.variableOccurrences hforward + have hbackwardOccurrences := congrArg Program.variableOccurrences hbackward + rw [Program.variableOccurrences_renameVariables] at hforwardOccurrences + rw [Program.variableOccurrences_renameVariables] at hbackwardOccurrences + have hinverse : ∀ identifier ∈ left.variableOccurrences, + backward (forward identifier) = identifier := by + have hmapped : left.variableOccurrences.map (backward ∘ forward) = + left.variableOccurrences.map id := by + rw [← List.map_map, hforwardOccurrences, hbackwardOccurrences] + simp + exact List.map_inj_left.mp hmapped + have hinjective : ∀ first ∈ left.variableOccurrences, + ∀ second ∈ left.variableOccurrences, + forward first = forward second → first = second := by + intro first hfirst second hsecond hequal + rw [← hinverse first hfirst, ← hinverse second hsecond, hequal] + rw [Program.normalize, Program.normalize, ← hforward, + Program.renameVariables_compose] + apply Program.renameVariables_congr + intro identifier hidentifier + simpa only [Function.comp_apply, hforward] using + (normalVariable_renameVariables hforward hinjective hidentifier).symm + · intro hequal + exact Program.AlphaEquiv.trans (Program.AlphaEquiv.symm (Program.normalize_alphaEquiv left)) + (hequal ▸ Program.normalize_alphaEquiv right) + +theorem Program.normalize_normal (program : Program) : + program.normalize.Normal := + Program.alphaEquiv_iff_normalize_eq.mp (Program.normalize_alphaEquiv program) + +end Sir.Vars.Proofs diff --git a/sir/Sir/Vars/Proofs/Rank.lean b/sir/Sir/Vars/Proofs/Rank.lean new file mode 100644 index 00000000..7813bcef --- /dev/null +++ b/sir/Sir/Vars/Proofs/Rank.lean @@ -0,0 +1,17 @@ +import Sir.Vars.Spec.Rank + +namespace Sir.Vars.Proofs + +theorem rank_lt_of_transGen {p : Program} {rank : FunctionId → Nat} + (decreasing : RankDecreases p rank) {f g} (path : Relation.TransGen p.callEdge f g) : + rank g < rank f := by + induction path with + | single edge => exact decreasing _ _ edge + | tail _ edge ih => exact Nat.lt_trans (decreasing _ _ edge) ih + +theorem acyclic_of_rank {p : Program} {rank : FunctionId → Nat} + (decreasing : RankDecreases p rank) (f : FunctionId) : + ¬ Relation.TransGen p.callEdge f f := + fun path => Nat.lt_irrefl _ (rank_lt_of_transGen decreasing path) + +end Sir.Vars.Proofs diff --git a/sir/Sir/Vars/Spec/Check.lean b/sir/Sir/Vars/Spec/Check.lean new file mode 100644 index 00000000..7d77de40 --- /dev/null +++ b/sir/Sir/Vars/Spec/Check.lean @@ -0,0 +1,135 @@ +import Sir.Vars.Spec + +namespace Sir.Vars + +inductive Diagnostic where + | icallArity (callee : FunctionId) (args dests : Nat) + | iretArity (declared actual : Nat) + | recursiveCall (caller callee : FunctionId) + | entryArity (function : FunctionId) (params outputs : Nat) + | jumpTarget (target : BlockId) (inputs : Option Nat) (outputs : Nat) + | variableUse (identifier : VarId) + +abbrev CheckM := Except Diagnostic + +def ensure (diagnostic : Diagnostic) (condition : Bool) : CheckM Unit := + if condition then .ok () else .error diagnostic + +def checkList {α : Type} (check : α → CheckM Unit) : List α → CheckM Unit + | [] => .ok () + | x :: rest => do + check x + checkList check rest + +def checkArray {α : Type} (check : α → CheckM Unit) (xs : Array α) : CheckM Unit := + checkList check xs.toList + +def checkBlocks (p : Program) (check : Function → Block → CheckM Unit) : CheckM Unit := + checkArray (fun fn => checkArray (check fn) fn.blocks) p.functions + +def checkIcallArityStmt (p : Program) : Stmt → CheckM Unit + | .icall callee args dests => + match p.function? callee with + | none => .error (.icallArity callee args.size dests.size) + | some fn => + ensure (.icallArity callee args.size dests.size) + (fn.paramsOf.size == args.size && fn.outputs?.getD 0 == dests.size) + | .assign _ _ | .sstore _ _ | .gas _ | .call _ | .malloc _ _ | .mallocUninit _ _ + | .mstore32 _ _ | .mload32 _ _ => .ok () + +def checkIcallArity (p : Program) : CheckM Unit := + checkBlocks p fun _ block => checkArray (checkIcallArityStmt p) block.statements + +def checkIretArityBlock (fn : Function) (block : Block) : CheckM Unit := + match block.terminator with + | .iret => + ensure (.iretArity (fn.outputs?.getD 0) block.outputs.size) + (some block.outputs.size == fn.outputs?) + | .halt | .jump _ | .branch _ _ _ => .ok () + +def checkIretArity (p : Program) : CheckM Unit := + checkBlocks p checkIretArityBlock + +def Program.blocksOf (p : Program) (f : FunctionId) : Array Block := + ((p.function? f).map (·.blocks)).getD #[] + +def Stmt.calleeId? : Stmt → Option FunctionId + | .icall callee _ _ => some callee + | _ => none + +def Program.callees (p : Program) (f : FunctionId) : List FunctionId := + (p.blocksOf f).toList.flatMap fun block => block.statements.toList.filterMap Stmt.calleeId? + +def rankRound (p : Program) (previous : List Nat) : List Nat := + (List.range p.functions.size).map fun index => + (p.callees ⟨index⟩).foldl (fun bound callee => max bound (previous.getD callee.id 0 + 1)) 0 + +def rankRounds (p : Program) : Nat → List Nat + | 0 => List.replicate p.functions.size 0 + | rounds + 1 => rankRound p (rankRounds p rounds) + +def Program.rank (p : Program) (f : FunctionId) : Nat := + (rankRounds p p.functions.size).getD f.id 0 + +def checkRankStmt (rank : FunctionId → Nat) (caller : FunctionId) : Stmt → CheckM Unit + | .icall callee _ _ => + ensure (.recursiveCall caller callee) (decide (rank callee < rank caller)) + | .assign _ _ | .sstore _ _ | .gas _ | .call _ | .malloc _ _ | .mallocUninit _ _ + | .mstore32 _ _ | .mload32 _ _ => .ok () + +def checkRankDecreases (p : Program) (rank : FunctionId → Nat) : CheckM Unit := + checkList + (fun index => checkArray + (fun block => checkArray (checkRankStmt rank ⟨index⟩) block.statements) + (p.blocksOf ⟨index⟩)) + (List.range p.functions.size) + +def checkAcyclicCalls (p : Program) : CheckM Unit := + checkRankDecreases p p.rank + +def checkEntryFunction (function : FunctionId) (fn : Function) : CheckM Unit := + ensure (.entryArity function fn.paramsOf.size (fn.outputs?.getD 0)) + (fn.paramsOf.size == 0 && fn.outputs?.isNone) + +def checkEntryArity (p : Program) : CheckM Unit := do + checkEntryFunction ⟨0⟩ p.init + match p.main with + | none => .ok () + | some m => checkEntryFunction ⟨1⟩ m + +def checkJumpTarget (fn : Function) (block : Block) (target : BlockId) : CheckM Unit := + match fn.block? target with + | none => .error (.jumpTarget target none block.outputs.size) + | some targetBlock => + ensure (.jumpTarget target (some targetBlock.inputs.size) block.outputs.size) + (targetBlock.inputs.size == block.outputs.size) + +def checkValidJumpTargets (p : Program) : CheckM Unit := + checkBlocks p fun fn block => + checkList (checkJumpTarget fn block) block.terminator.jumpTargets + +def Block.undefinedUse? (block : Block) : Option VarId := + match (List.range block.statements.size).findSome? fun index => + (block.statements[index]?).bind fun statement => + statement.variablesRead.find? fun identifier => + decide (identifier ∉ block.variablesDefinedBefore index) with + | some identifier => some identifier + | none => + (block.terminator.variablesRead ++ block.outputs.toList).find? fun identifier => + decide (identifier ∉ block.variablesDefinedBefore block.statements.size) + +def checkVariablesDefinedBeforeUse (p : Program) : CheckM Unit := + checkBlocks p fun _ block => + match block.undefinedUse? with + | some identifier => .error (.variableUse identifier) + | none => .ok () + +def checkWellFormed (p : Program) : CheckM Unit := do + checkIcallArity p + checkIretArity p + checkAcyclicCalls p + checkEntryArity p + checkValidJumpTargets p + checkVariablesDefinedBeforeUse p + +end Sir.Vars diff --git a/sir/Sir/Vars/Spec/Normalize.lean b/sir/Sir/Vars/Spec/Normalize.lean new file mode 100644 index 00000000..9d5275d4 --- /dev/null +++ b/sir/Sir/Vars/Spec/Normalize.lean @@ -0,0 +1,96 @@ +import Sir.Vars.Spec + +namespace Sir.Vars + +def Expr.renameVariables (rename : VarId → VarId) : Expr → Expr + | .constant value => .constant value + | .var source => .var (rename source) + | .add lhs rhs => .add (rename lhs) (rename rhs) + | .lt lhs rhs => .lt (rename lhs) (rename rhs) + | .sload key => .sload (rename key) + +def Stmt.renameVariables (rename : VarId → VarId) : Stmt → Stmt + | .assign result value => .assign (rename result) (value.renameVariables rename) + | .sstore key value => .sstore (rename key) (rename value) + | .gas result => .gas (rename result) + | .call callData => .call { + callee := rename callData.callee + gas := rename callData.gas + result := rename callData.result } + | .malloc result size => .malloc (rename result) (rename size) + | .mallocUninit result size => .mallocUninit (rename result) (rename size) + | .mstore32 offset value => .mstore32 (rename offset) (rename value) + | .mload32 result offset => .mload32 (rename result) (rename offset) + | .icall callee args dests => .icall callee (args.map rename) (dests.map rename) + +def Terminator.renameVariables (rename : VarId → VarId) : Terminator → Terminator + | .halt => .halt + | .jump target => .jump target + | .branch condition thenTarget elseTarget => + .branch (rename condition) thenTarget elseTarget + | .iret => .iret + +def Block.renameVariables (rename : VarId → VarId) (block : Block) : Block := + { inputs := block.inputs.map rename + statements := block.statements.map (Stmt.renameVariables rename) + terminator := block.terminator.renameVariables rename + outputs := block.outputs.map rename } + +def Function.renameVariables (rename : VarId → VarId) (function : Function) : Function := + { entry := function.entry.renameVariables rename + rest := function.rest.map (Block.renameVariables rename) } + +def Program.renameVariables (rename : VarId → VarId) (program : Program) : Program := + { init := program.init.renameVariables rename + main := program.main.map (Function.renameVariables rename) + rest := program.rest.map (Function.renameVariables rename) } + +def Expr.variableOccurrences : Expr → List VarId + | .constant _ => [] + | .var source => [source] + | .add lhs rhs => [lhs, rhs] + | .lt lhs rhs => [lhs, rhs] + | .sload key => [key] + +def Stmt.variableOccurrences : Stmt → List VarId + | .assign result value => result :: value.variableOccurrences + | .sstore key value => [key, value] + | .gas result => [result] + | .call callData => [callData.result, callData.gas, callData.callee] + | .malloc result size => [result, size] + | .mallocUninit result size => [result, size] + | .mstore32 offset value => [offset, value] + | .mload32 result offset => [result, offset] + | .icall _ args dests => dests.toList ++ args.toList + +def Terminator.variableOccurrences : Terminator → List VarId + | .halt => [] + | .jump _ => [] + | .branch condition _ _ => [condition] + | .iret => [] + +def Block.variableOccurrences (block : Block) : List VarId := + block.inputs.toList ++ block.outputs.toList ++ + block.statements.toList.flatMap Stmt.variableOccurrences ++ + block.terminator.variableOccurrences + +def Function.variableOccurrences (function : Function) : List VarId := + function.blocks.toList.flatMap Block.variableOccurrences + +def Program.variableOccurrences (program : Program) : List VarId := + program.functions.toList.flatMap Function.variableOccurrences + +def Program.normalVariable (program : Program) (identifier : VarId) : VarId := + ⟨program.variableOccurrences.eraseDups.idxOf identifier⟩ + +def Program.normalize (program : Program) : Program := + program.renameVariables program.normalVariable + +def Program.Normal (program : Program) : Prop := + program.normalize = program + +def Program.AlphaEquiv (left right : Program) : Prop := + ∃ forward backward : VarId → VarId, + left.renameVariables forward = right ∧ right.renameVariables backward = left + +end Sir.Vars diff --git a/sir/Sir/Vars/Spec/Rank.lean b/sir/Sir/Vars/Spec/Rank.lean new file mode 100644 index 00000000..c17b1cba --- /dev/null +++ b/sir/Sir/Vars/Spec/Rank.lean @@ -0,0 +1,8 @@ +import Sir.Vars.Spec + +namespace Sir.Vars + +def RankDecreases (p : Program) (rank : FunctionId → Nat) : Prop := + ∀ f g, p.callEdge f g → rank g < rank f + +end Sir.Vars diff --git a/sir/Sir/Vars/Theorems.lean b/sir/Sir/Vars/Theorems.lean index e02112ad..803d771b 100644 --- a/sir/Sir/Vars/Theorems.lean +++ b/sir/Sir/Vars/Theorems.lean @@ -1,6 +1,9 @@ import Sir.Vars.Proofs.Determinism import Sir.Vars.Proofs.Readiness import Sir.Vars.Proofs.Bump +import Sir.Vars.Proofs.Rank +import Sir.Vars.Proofs.Check +import Sir.Vars.Proofs.Normalize namespace Sir @@ -153,4 +156,30 @@ theorem Vars.Program.icall_halted_step s =[t]=> { globals := g', environment := .empty, control := .halted } := Vars.Proofs.Program.icall_halted_step hstmt hargs hcallee +theorem Vars.rank_lt_of_transGen {rank : FunctionId → Nat} + (decreasing : Vars.RankDecreases program rank) {f g} + (path : Relation.TransGen program.callEdge f g) : rank g < rank f := + Vars.Proofs.rank_lt_of_transGen decreasing path + +theorem Vars.acyclic_of_rank {rank : FunctionId → Nat} + (decreasing : Vars.RankDecreases program rank) (f : FunctionId) : + ¬ Relation.TransGen program.callEdge f f := + Vars.Proofs.acyclic_of_rank decreasing f + +theorem Vars.Program.wellFormed_of_check + (h : Vars.checkWellFormed program = .ok ()) : program.WellFormed := + Vars.Proofs.Program.wellFormed_of_check h + +theorem Vars.Program.normalize_alphaEquiv (program : Vars.Program) : + Vars.Program.AlphaEquiv program.normalize program := + Vars.Proofs.Program.normalize_alphaEquiv program + +theorem Vars.Program.alphaEquiv_iff_normalize_eq {left right : Vars.Program} : + Vars.Program.AlphaEquiv left right ↔ left.normalize = right.normalize := + Vars.Proofs.Program.alphaEquiv_iff_normalize_eq + +theorem Vars.Program.alphaEquiv_equivalence : Equivalence Vars.Program.AlphaEquiv := + ⟨Vars.Proofs.Program.AlphaEquiv.refl, Vars.Proofs.Program.AlphaEquiv.symm, + Vars.Proofs.Program.AlphaEquiv.trans⟩ + end Sir diff --git a/sir/SirExtract.lean b/sir/SirExtract.lean new file mode 100644 index 00000000..cf09672e --- /dev/null +++ b/sir/SirExtract.lean @@ -0,0 +1,35 @@ +import Sir.Text.Extract + +private def readFile (path : System.FilePath) : IO (Except IO.Error String) := do + try + return .ok (← IO.FS.readFile path) + catch error => + return .error error + +private def writeFile (path : System.FilePath) (contents : String) : IO (Except IO.Error Unit) := do + try + return .ok (← IO.FS.writeFile path contents) + catch error => + return .error error + +def main (arguments : List String) : IO UInt32 := do + match arguments with + | [input, output, declaration] => + match ← readFile input with + | .error error => + IO.eprintln s!"{input}: {error}" + return 1 + | .ok source => + match Sir.Vars.Text.extract source declaration with + | .error message => + IO.eprintln s!"{input}: {message}" + return 1 + | .ok module => + match ← writeFile output module with + | .ok _ => return 0 + | .error error => + IO.eprintln s!"{output}: {error}" + return 1 + | _ => + IO.eprintln "usage: sir-extract " + return 1 diff --git a/sir/lakefile.lean b/sir/lakefile.lean index 7b50eb83..5ef9128b 100644 --- a/sir/lakefile.lean +++ b/sir/lakefile.lean @@ -11,3 +11,7 @@ package "sir" where @[default_target] lean_lib «Sir» where roots := #[`Sir] + +@[default_target] +lean_lib «SirExtract» where + roots := #[`SirExtract]