theory Frontend
  imports X86
begin

fun finish :: "string \<Rightarrow> string list \<Rightarrow> string list" where
  "finish [] out = out"
| "finish word out = rev word # out"

fun scan :: "string \<Rightarrow> string \<Rightarrow> string list \<Rightarrow> bool \<Rightarrow> string list" where
  "scan [] word out comment = rev (finish word out)"
| "scan (c # cs) word out comment = (if comment then
      scan cs [] out (c \<noteq> CHR 0x0A \<and> c \<noteq> CHR 0x0D)
    else if c = CHR '';'' then scan cs [] (finish word out) True
    else if c = CHR '' '' \<or> c = CHR 0x09 \<or> c = CHR 0x0A \<or> c = CHR 0x0D
    then scan cs [] (finish word out) False
    else if c = CHR ''('' \<or> c = CHR '')'' then scan cs [] ([c] # finish word out) False
    else scan cs (c # word) out False)"

definition lex :: "string \<Rightarrow> string \<Rightarrow> string list \<Rightarrow> string list" where
  "lex s word out = scan s word out False"

fun digit :: "char \<Rightarrow> nat" where
  "digit c = (let n = nat_of_char c in
    if 48 \<le> n \<and> n < 58 then n - 48 else
    if 65 \<le> n \<and> n < 71 then n - 55 else
    if 97 \<le> n \<and> n < 103 then n - 87 else 16)"

definition parse_digits :: "nat \<Rightarrow> string \<Rightarrow> nat option" where
  "parse_digits base s = (if s = [] \<or> \<not> list_all (\<lambda>c. digit c < base) s
    then None else let n = foldl (\<lambda>n c. min (2 ^ 64) (base * n + digit c)) 0 s in
    if n < 2 ^ 64 then Some n else None)"

definition number :: "string \<Rightarrow> nat option" where
  "number s = (case s of a # b # rest \<Rightarrow>
    if a = CHR ''0'' \<and> (b = CHR ''x'' \<or> b = CHR ''X'') then parse_digits 16 rest
    else parse_digits 10 s | _ \<Rightarrow> parse_digits 10 s)"

lemma parse_digits_bound: "parse_digits base s = Some n \<Longrightarrow> n < 2 ^ 64"
  by (auto simp only: parse_digits_def Let_def option.inject option.distinct split: if_splits)

theorem number_bound: "number s = Some n \<Longrightarrow> n < 2 ^ 64"
  using parse_digits_bound by (auto simp: number_def split: list.splits if_splits)

definition valid_name :: "string \<Rightarrow> bool" where
  "valid_name s = (case s of [] \<Rightarrow> False | c # cs \<Rightarrow>
    97 \<le> nat_of_char c \<and> nat_of_char c \<le> 122 \<and>
    list_all (\<lambda>d. (97 \<le> nat_of_char d \<and> nat_of_char d \<le> 122) \<or>
      (48 \<le> nat_of_char d \<and> nat_of_char d < 58)) cs \<and> s \<noteq> ''let'' \<and> s \<noteq> ''if'')"

fun lookup :: "string \<Rightarrow> string list \<Rightarrow> nat option" where
  "lookup name [] = None"
| "lookup name (x # xs) = (if name = x then Some 0 else map_option Suc (lookup name xs))"

lemma lookup_bound: "lookup name names = Some i \<Longrightarrow> i < length names"
  by (induction names arbitrary: i) (auto split: if_splits option.splits)

fun operator :: "string \<Rightarrow> operator option" where
  "operator s = (if s = ''+'' then Some Add else if s = ''-'' then Some Sub else if s = ''*'' then Some Mul
    else if s = ''and'' then Some And else if s = ''or'' then Some Or else if s = ''xor'' then Some Xor
    else if s = ''shl'' then Some Shl else if s = ''shr'' then Some Shr else if s = ''<'' then Some Less else None)"

definition atom :: "string list \<Rightarrow> string \<Rightarrow> expression option" where
  "atom names s = (case lookup s names of Some i \<Rightarrow> Some (Variable i) | None \<Rightarrow>
    if s = ''x'' then Some (Input X) else if s = ''y'' then Some (Input Y) else if s = ''t'' then Some (Input T)
    else map_option (Literal \<circ> word_of_nat) (number s))"

lemma atom_scoped: "atom names s = Some e \<Longrightarrow> scoped (length names) e"
  by (auto simp: atom_def split: option.splits if_splits dest: lookup_bound)

fun close :: "expression \<Rightarrow> string list \<Rightarrow> (expression \<times> string list) option" where
  "close e (s # rest) = (if s = '')'' then Some (e,rest) else None)"
| "close e [] = None"

lemma close_expression: "close e tokens = Some (a,rest) \<Longrightarrow> a = e"
  by (cases tokens) (auto split: if_splits)

function parse :: "nat \<Rightarrow> string list \<Rightarrow> string list \<Rightarrow> (expression \<times> string list) option" where
  "parse fuel names tokens = (if fuel = 0 then None else case tokens of [] \<Rightarrow> None | s # rest \<Rightarrow>
    if s \<noteq> ''('' then map_option (\<lambda>e. (e,rest)) (atom names s)
    else case rest of [] \<Rightarrow> None | op # args \<Rightarrow>
      if op = ''let'' then (case args of [] \<Rightarrow> None | name # body \<Rightarrow>
        if \<not> valid_name name then None else
        Option.bind (parse (fuel - 1) names body) (\<lambda>(a,tail).
        Option.bind (parse (fuel - 1) (name # names) tail) (\<lambda>(b,tail). close (Let a b) tail)))
      else if op = ''if'' then
        Option.bind (parse (fuel - 1) names args) (\<lambda>(c,tail).
        Option.bind (parse (fuel - 1) names tail) (\<lambda>(a,tail).
        Option.bind (parse (fuel - 1) names tail) (\<lambda>(b,tail). close (Cond c a b) tail)))
      else Option.bind (operator op) (\<lambda>f.
        Option.bind (parse (fuel - 1) names args) (\<lambda>(a,tail).
        Option.bind (parse (fuel - 1) names tail) (\<lambda>(b,tail). close (Binary f a b) tail))))"
  by pat_completeness auto
termination by (relation "measure (\<lambda>(fuel,names,tokens). fuel)") auto

declare parse.simps [simp del]

theorem parse_scoped:
  "parse fuel names tokens = Some (e,rest) \<Longrightarrow> scoped (length names) e"
proof (induction fuel arbitrary: names tokens e rest)
  case 0
  then show ?case by (subst (asm) parse.simps) auto
next
  case (Suc fuel)
  from Suc.prems show ?case
    by (subst (asm) parse.simps)
      (auto simp del: operator.simps dest: atom_scoped split: list.splits if_splits bind_splits option.splits prod.splits;
        drule close_expression; auto dest: Suc.IH)
qed

record limits =
  depth_budget :: nat
  node_budget :: nat
  stack_budget :: nat

definition defaults :: limits where
  "defaults = \<lparr>depth_budget = 128, node_budget = 4096, stack_budget = 512\<rparr>"

definition valid_limits :: "limits \<Rightarrow> bool" where
  "valid_limits lim = (depth_budget lim \<le> 128 \<and> node_budget lim \<le> 4096 \<and> stack_budget lim \<le> 512)"

definition prepare_with :: "limits \<Rightarrow> string \<Rightarrow> expression option" where
  "prepare_with lim s = (if \<not> valid_limits lim \<or> \<not> list_all (\<lambda>c. nat_of_char c < 128) s then None else
    Option.bind (parse (depth_budget lim) [] (lex s [] [])) (\<lambda>(e,rest).
      if rest = [] \<and> nodes e \<le> node_budget lim then
        let code = compile (optimise e) [] in
        if check code 0 = Some 1 \<and> demand (optimise e) \<le> stack_budget lim \<and> list_all encodable (native code)
        then Some e else None else None))"

definition prepare :: "string \<Rightarrow> expression option" where
  "prepare = prepare_with defaults"

lemma prepare_with_scoped: "prepare_with lim s = Some e \<Longrightarrow> scoped 0 e"
  by (auto simp: prepare_with_def Let_def dest: parse_scoped split: if_splits bind_splits prod.splits)

lemma prepare_with_bounded:
  "prepare_with lim s = Some e \<Longrightarrow> bounded (stack_budget lim) (compile (optimise e) []) 0"
  by (auto simp: prepare_with_def Let_def closed_demand optimise_scoped dest: parse_scoped split: if_splits bind_splits prod.splits)

lemma prepare_scoped: "prepare s = Some e \<Longrightarrow> scoped 0 e"
  unfolding prepare_def using prepare_with_scoped by blast

lemma prepare_bounded:
  "prepare s = Some e \<Longrightarrow> bounded 512 (compile (optimise e) []) 0"
  using prepare_with_bounded[where lim=defaults] by (simp add: prepare_def defaults_def)

lemma prepare_encodable:
  "prepare s = Some e \<Longrightarrow> list_all encodable (native (compile (optimise e) []))"
  by (auto simp: prepare_def prepare_with_def Let_def split: if_splits bind_splits prod.splits)

lemma prepare_program:
  "prepare s = Some e \<Longrightarrow> list_all encodable (program e)"
  unfolding program_def using prepare_encodable
  by (auto intro: transfers_property)

theorem prepared_correct:
  "prepare source = Some e \<Longrightarrow>
    execute values (compile (optimise e) []) [] = Some [evaluate e [] values]"
  using compile_closed prepare_scoped by blast

theorem prepared_native:
  "prepare source = Some e \<Longrightarrow>
    map_option observe (run (native (compile (optimise e) [])) s) =
    Some (inputs s, evaluate e [] (inputs s) # stack s)"
  using native_expression prepare_scoped by blast

theorem prepared_bytes:
  "prepare source = Some e \<Longrightarrow>
    recover (length (program e)) (executable e) =
    Some (program e, [195])"
  unfolding executable_def using recover_encode prepare_program by blast

theorem prepared_stacks:
  "prepare source = Some e \<Longrightarrow>
    \<exists>frames. snapshots values (compile (optimise e) []) [] = Some frames \<and>
      list_all (\<lambda>s. length s \<le> 512) frames"
  using bounded_execution[where s="[]" and limit=512] prepare_bounded by auto

function decimal :: "nat \<Rightarrow> string" where
  "decimal n = (if n < 10 then [char_of_nat (48+n)] else decimal (n div 10) @ [char_of_nat (48+n mod 10)])"
  by pat_completeness auto
termination by (relation "measure id") (auto simp: div_less_dividend)

definition newline :: string where "newline = [CHR 0x0A]"

fun regname :: "register \<Rightarrow> string" where
  "regname Rax = ''rax''" | "regname Rcx = ''rcx''" | "regname Rbx = ''rbx''"
| "regname Rdx = ''rdx''" | "regname R8 = ''r8''" | "regname R9 = ''r9''"

fun opname :: "operator \<Rightarrow> string" where
  "opname Add = ''add''" | "opname Sub = ''sub''" | "opname Mul = ''mul''"
| "opname And = ''and''" | "opname Or = ''or''" | "opname Xor = ''xor''"
| "opname Shl = ''shl''" | "opname Shr = ''shr''" | "opname Less = ''less''"

fun mnemonic :: "opcode \<Rightarrow> string" where
  "mnemonic (Immediate v) = ''immediate rax '' @ decimal (unat v)"
| "mnemonic (Push r) = ''push '' @ regname r"
| "mnemonic (Pop r) = ''pop '' @ regname r"
| "mnemonic (Move dst src) = ''mov '' @ regname dst @ '' '' @ regname src"
| "mnemonic (Peek i) = ''peek rax stack['' @ decimal i @ '']''"
| "mnemonic (Arithmetic op) = ''arithmetic '' @ opname op"
| "mnemonic Conditional = ''conditional rax rcx rbx''"

fun listing :: "nat \<Rightarrow> (nat list \<times> opcode) list \<Rightarrow> string" where
  "listing offset [] = decimal offset @ ''  ret'' @ newline"
| "listing offset ((bytes,op) # code) = decimal offset @ ''  '' @ mnemonic op @
    ''  ['' @ concat (map (\<lambda>b. decimal b @ '' '') bytes) @ '']'' @ newline @
    listing (offset + length bytes) code"

fun linear_listing :: "nat \<Rightarrow> opcode list \<Rightarrow> string" where
  "linear_listing offset [] = []"
| "linear_listing offset (op # code) = decimal offset @ ''  '' @ mnemonic op @ newline @
    linear_listing (offset + length (encode op)) code"

fun flowlisting :: "nat \<Rightarrow> flow \<Rightarrow> string" where
  "flowlisting offset (Basic code) = linear_listing offset code"
| "flowlisting offset (Sequence a b) = flowlisting offset a @
    flowlisting (offset + length (flowbytes a)) b"
| "flowlisting offset (Choice a b) = decimal offset @ ''  test rax rax'' @ newline @
    decimal (offset + 3) @ ''  jz '' @ decimal (offset + 14 + length (flowbytes a)) @ newline @
    flowlisting (offset + 9) a @ decimal (offset + 9 + length (flowbytes a)) @ ''  jmp '' @
    decimal (offset + length (flowbytes (Choice a b))) @ newline @
    flowlisting (offset + 14 + length (flowbytes a)) b"

definition disassemble :: "string \<Rightarrow> bool \<times> string" where
  "disassemble bytes = (case blocks (map nat_of_char bytes) of
    None \<Rightarrow> (case inspect (map nat_of_char bytes) of
      None \<Rightarrow> (False,''invalid native block stream'' @ newline)
      | Some code \<Rightarrow> (True,flowlisting 0 code @ decimal (length (flowbytes code)) @ ''  ret'' @ newline))
    | Some code \<Rightarrow> (True,listing 0 code))"

definition validate :: "string \<Rightarrow> bool \<times> string" where
  "validate bytes = (case blocks (map nat_of_char bytes) of
    None \<Rightarrow> (case inspect (map nat_of_char bytes) of
      None \<Rightarrow> (False,''invalid native block stream'' @ newline)
      | Some code \<Rightarrow> (True,''native branch, stack and register effects verified'' @ newline))
    | Some code \<Rightarrow> if audit (map snd code) 0 = Some 0
      then (True,''native stack and register effects verified'' @ newline)
      else (False,''invalid native stack or register effects'' @ newline))"

datatype problem = Unexpected nat | Exhausted nat

datatype 'a outcome = Failed problem | Parsed 'a

fun parsed_bind :: "'a outcome \<Rightarrow> ('a \<Rightarrow> 'b outcome) \<Rightarrow> 'b outcome" where
  "parsed_bind (Failed p) f = Failed p"
| "parsed_bind (Parsed x) f = f x"

fun close_at :: "expression \<Rightarrow> string list \<Rightarrow> nat \<Rightarrow> (expression \<times> string list \<times> nat) outcome" where
  "close_at e [] pos = Failed (Unexpected pos)"
| "close_at e (s # rest) pos = (if s = '')'' then Parsed (e,rest,Suc pos) else Failed (Unexpected pos))"

lemma close_at_cursor:
  "close_at e tokens pos = Parsed (a,rest,nextpos) \<Longrightarrow> a = e \<and> nextpos = Suc pos"
  by (cases tokens) (auto split: if_splits)

function diagnose :: "nat \<Rightarrow> string list \<Rightarrow> string list \<Rightarrow> nat \<Rightarrow>
    (expression \<times> string list \<times> nat) outcome" where
  "diagnose fuel names tokens pos = (if fuel = 0 then Failed (Exhausted pos)
    else case tokens of [] \<Rightarrow> Failed (Unexpected pos) | s # rest \<Rightarrow>
    if s \<noteq> ''('' then (case atom names s of None \<Rightarrow> Failed (Unexpected pos)
      | Some e \<Rightarrow> Parsed (e,rest,Suc pos))
    else case rest of [] \<Rightarrow> Failed (Unexpected (Suc pos)) | op # args \<Rightarrow>
      if op = ''let'' then (case args of [] \<Rightarrow> Failed (Unexpected (pos + 2)) | name # body \<Rightarrow>
        if \<not> valid_name name then Failed (Unexpected (pos + 2)) else
        parsed_bind (diagnose (fuel - 1) names body (pos + 3)) (\<lambda>(a,tail,nextpos).
        parsed_bind (diagnose (fuel - 1) (name # names) tail nextpos) (\<lambda>(b,tail,lastpos).
          close_at (Let a b) tail lastpos)))
      else if op = ''if'' then
        parsed_bind (diagnose (fuel - 1) names args (pos + 2)) (\<lambda>(c,tail,nextpos).
        parsed_bind (diagnose (fuel - 1) names tail nextpos) (\<lambda>(a,tail,nextpos).
        parsed_bind (diagnose (fuel - 1) names tail nextpos) (\<lambda>(b,tail,lastpos).
          close_at (Cond c a b) tail lastpos)))
      else case operator op of None \<Rightarrow> Failed (Unexpected (Suc pos)) | Some f \<Rightarrow>
        parsed_bind (diagnose (fuel - 1) names args (pos + 2)) (\<lambda>(a,tail,nextpos).
        parsed_bind (diagnose (fuel - 1) names tail nextpos) (\<lambda>(b,tail,lastpos).
          close_at (Binary f a b) tail lastpos)))"
  by pat_completeness auto
termination by (relation "measure (\<lambda>(fuel,names,tokens,pos). fuel)") auto

declare diagnose.simps [simp del]

definition source_error_with :: "limits \<Rightarrow> string \<Rightarrow> string" where
  "source_error_with lim s = (if \<not> valid_limits lim then ''limits exceed compiler bounds'' @ newline else if \<not> list_all (\<lambda>c. nat_of_char c < 128) s then ''source must contain ASCII'' @ newline else
    case diagnose (depth_budget lim) [] (lex s [] []) 0 of
    Failed (Unexpected pos) \<Rightarrow> ''syntax error at token '' @ decimal pos @ newline
    | Failed (Exhausted pos) \<Rightarrow> ''parse depth limit exceeded at token '' @ decimal pos @ newline
    | Parsed (e,rest,pos) \<Rightarrow> if rest \<noteq> [] then ''syntax error at token '' @ decimal pos @ newline
      else if nodes e > node_budget lim then ''program exceeds '' @ decimal (node_budget lim) @ '' nodes'' @ newline
      else if demand (optimise e) > stack_budget lim then ''evaluation stack exceeds '' @ decimal (stack_budget lim) @ '' words'' @ newline
      else ''native validation failed'' @ newline)"

definition artifact_with :: "limits \<Rightarrow> string \<Rightarrow> (bool \<times> string) \<times> string" where
  "artifact_with lim s = (case prepare_with lim s of None \<Rightarrow> ((False,[]), source_error_with lim s)
    | Some e \<Rightarrow> let opt = optimise e; code = branching e; bytes = flowbytes code @ [195] in
      if flowaudit code 0 = Some 0 \<and> flowvalid code then
        ((True, map char_of_nat bytes), decimal (nodes e) @ '' nodes -> '' @ decimal (nodes opt) @
          '' nodes, '' @ decimal (length bytes) @ '' bytes, '' @ decimal (demand opt) @ '' stack words'' @ newline)
      else ((False,[]),''allocated code exceeds native limits'' @ newline))"

definition source_error :: "string \<Rightarrow> string" where
  "source_error = source_error_with defaults"

definition artifact :: "string \<Rightarrow> (bool \<times> string) \<times> string" where
  "artifact = artifact_with defaults"

theorem artifact_execution:
  assumes "artifact source = ((True,bytes),report)"
  shows "\<exists>e d. prepare source = Some e \<and>
    bytes = map char_of_nat (flowbytes (branching e) @ [195]) \<and>
    executes64 (flowbytes (branching e)) c d \<and>
    registers (state64 d) Rax = evaluate e [] (inputs (state64 c)) \<and>
    stack (state64 d) = stack (state64 c) \<and> inputs (state64 d) = inputs (state64 c)"
proof -
  obtain e where e: "prepare source = Some e" "flowvalid (branching e)"
    "bytes = map char_of_nat (flowbytes (branching e) @ [195])"
    using assms by (auto simp: artifact_def artifact_with_def prepare_def Let_def split: option.splits if_splits)
  show ?thesis using compiled_execution[OF prepare_scoped[OF e(1)] e(2), of c] e by blast
qed

definition baseline :: "string \<Rightarrow> (bool \<times> string) \<times> string" where
  "baseline s = (case prepare s of None \<Rightarrow> ((False,[]),source_error s)
    | Some e \<Rightarrow> ((True,map char_of_nat (executable e)),''stack backend'' @ newline))"

definition configured :: "string \<Rightarrow> string \<Rightarrow> string \<Rightarrow> string \<Rightarrow> (bool \<times> string) \<times> string" where
  "configured depth count stacktext source = (case (number depth, number count, number stacktext) of
    (Some d,Some n,Some k) \<Rightarrow> artifact_with \<lparr>depth_budget=d, node_budget=n, stack_budget=k\<rparr> source
    | _ \<Rightarrow> ((False,[]),''invalid resource limits'' @ newline))"

definition boundary :: "nat list" where
  "boundary = [0,1,63,64,65,127,255,256,2 ^ 31,2 ^ 32,2 ^ 63,2 ^ 64 - 1]"

definition sample :: "nat \<Rightarrow> input \<Rightarrow> pixel" where
  "sample i = (\<lambda>v. word_of_nat (if i < 12 then boundary ! ((i + (case v of X \<Rightarrow> 0 | Y \<Rightarrow> 3 | T \<Rightarrow> 7)) mod 12)
    else case v of X \<Rightarrow> (17*i) mod 257 | Y \<Rightarrow> (29*i) mod 131 | T \<Rightarrow> 13*i))"

definition row :: "expression \<Rightarrow> nat \<Rightarrow> nat list" where
  "row e i = concat (map (\<lambda>v. octets 8 (unat v))
    [sample i X, sample i Y, sample i T, evaluate e [] (sample i)])"

definition vectors :: "string \<Rightarrow> bool \<times> string" where
  "vectors s = (case prepare s of None \<Rightarrow> (False, source_error s)
    | Some e \<Rightarrow> (True, map char_of_nat (concat (map (row e) [0..<512]))))"

definition reference :: "string \<Rightarrow> string \<Rightarrow> string \<Rightarrow> string \<Rightarrow> bool \<times> string" where
  "reference source x y t = (case prepare source of None \<Rightarrow> (False,source_error source) | Some e \<Rightarrow>
    case (number x, number y, number t) of (Some a,Some b,Some c) \<Rightarrow>
      (True, decimal (unat (evaluate e [] (\<lambda>v. word_of_nat (case v of X \<Rightarrow> a | Y \<Rightarrow> b | T \<Rightarrow> c)))) @ newline)
    | _ \<Rightarrow> (False,''invalid input'' @ newline))"

definition initial64 :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> processor" where
  "initial64 x y t = \<lparr>state64 = \<lparr>registers = (\<lambda>r. word_of_nat
    (if r = R8 then x else if r = R9 then y else if r = Rdx then t else 0)), stack = [0]\<rparr>,
    pointer64 = 65536, zero64 = None, carry64 = None\<rparr>"

definition simulate :: "string \<Rightarrow> string \<Rightarrow> string \<Rightarrow> string \<Rightarrow> bool \<times> string" where
  "simulate code x y t = (if \<not> fst (validate code) then (False,''invalid native image'' @ newline) else
    case (number x,number y,number t) of (Some a,Some b,Some c) \<Rightarrow>
      (case simulate64 (Suc (length code)) (map nat_of_char code) (initial64 a b c) of
        None \<Rightarrow> (False,''unsupported or incomplete x86 execution'' @ newline)
        | Some q \<Rightarrow> if stack (state64 q) = []
          then (True,decimal (unat (registers (state64 q) Rax)) @ newline)
          else (False,''return frame was not consumed'' @ newline))
    | _ \<Rightarrow> (False,''invalid input'' @ newline))"

end