6 files changed, 227 insertions(+), 6 deletions(-)

M README.md
M ROOT
A src/Branches.thy
M src/Frontend.thy
M tests/cli.py
M tests/native.py

@@ 31,6 31,6 @@ Each `let` pushes a binding onto the evaluation stack. [Compilation](src/core/Co
 
 Arithmetic wraps modulo `2^64` and shifts mask their count to six bits
 
-Both branches of a nonconstant conditional run before selection which preserves the result because expressions have no side effects. The HolyC runner masks each pixel result to four bits for the TempleOS palette
+Nonconstant conditionals use forward `jz` and `jmp` instructions so only the selected arm runs. The validator checks both arms for matching stack heights and protected input registers. The HolyC runner masks each result to four bits for the TempleOS palette
 
 The execution theorem is relative to the instruction block model. Actual x86 execution + the HolyC calling bridge and the extracted runtime and the OS are outside its scope. Tests compare emitted code against an independent evaluator on Linux and against HOL results inside the recorded TempleOS guest

@@ 15,6 15,7 @@ session Remy in src = Remybase +
   sessions "HOL-Library"
   theories
     Allocation
+    Branches
     Frontend
     Examples
     Export

@@ 0,0 1,169 @@
+theory Branches
+  imports Allocation
+begin
+
+datatype flow = Basic "opcode list" | Sequence flow flow | Choice flow flow
+
+fun flowrun :: "flow \<Rightarrow> machine \<Rightarrow> machine option" where
+  "flowrun (Basic code) s = run code s"
+| "flowrun (Sequence a b) s = Option.bind (flowrun a s) (flowrun b)"
+| "flowrun (Choice a b) s = flowrun (if registers s Rax = 0 then b else a) s"
+
+fun chain :: "flow list \<Rightarrow> flow" where
+  "chain [] = Basic []"
+| "chain (a # code) = Sequence a (chain code)"
+
+fun branch_allocate :: "bool \<Rightarrow> expression \<Rightarrow> nat list \<Rightarrow> flow" where
+  "branch_allocate free (Literal v) slots = Basic [Immediate v]"
+| "branch_allocate free (Input i) slots = Basic [Move Rax (input_register i)]"
+| "branch_allocate free (Variable i) slots = Basic [Peek (slots ! i)]"
+| "branch_allocate free (Binary op a b) slots = (if free then
+    chain [branch_allocate True a slots, Basic [Move Rbx Rax], branch_allocate False b slots,
+      Basic [Move Rcx Rbx, Arithmetic op]]
+    else chain [branch_allocate False a slots, Basic [Push Rax], branch_allocate False b (map Suc slots),
+      Basic [Pop Rcx, Arithmetic op]])"
+| "branch_allocate free (Cond c a b) slots = Sequence (branch_allocate free c slots)
+    (Choice (branch_allocate free a slots) (branch_allocate free b slots))"
+| "branch_allocate free (Let a b) slots = chain [branch_allocate free a slots, Basic [Push Rax],
+    branch_allocate free b (0 # map Suc slots), Basic [Pop Rcx]]"
+
+theorem branch_allocate_correct:
+  assumes "scoped (length env) e" "represents slots (stack s) env"
+  shows "\<exists>q. flowrun (branch_allocate free e slots) s = Some q \<and> allocated_result free e env s q"
+  using assms
+proof (induction e arbitrary: free slots env s)
+  case (Literal v)
+  then show ?case by (auto simp: allocated_result_def chain.simps)
+next
+  case (Input i)
+  then show ?case by (auto simp: allocated_result_def inputs_def fun_eq_iff)
+next
+  case (Variable i)
+  then show ?case by (auto simp: allocated_result_def represents_def)
+next
+  case (Binary op a b)
+  obtain p where a: "flowrun (branch_allocate free a slots) s = Some p"
+    and p: "allocated_result free a env s p"
+    using Binary.IH(1)[of env slots s free] Binary.prems by auto
+  show ?case
+  proof (cases free)
+    case True
+    let ?p = "p\<lparr>registers := (registers p)(Rbx := registers p Rax)\<rparr>"
+    obtain q where b: "flowrun (branch_allocate False b slots) ?p = Some q"
+      and q: "allocated_result False b env ?p q"
+      using Binary.IH(2)[of env slots ?p False] Binary.prems p
+      by (auto simp: allocated_result_def chain.simps)
+    show ?thesis using a b p q True
+      by (auto simp: allocated_result_def run_append flowrun.simps chain.simps; auto simp: inputs_def fun_eq_iff)
+  next
+    case False
+    let ?p = "p\<lparr>stack := registers p Rax # stack p\<rparr>"
+    obtain q where b: "flowrun (branch_allocate False b (map Suc slots)) ?p = Some q"
+      and q: "allocated_result False b env ?p q"
+      using Binary.IH(2)[of env "map Suc slots" ?p False] Binary.prems p
+        represents_push[OF Binary.prems(2), of "registers p Rax"]
+      by (auto simp: allocated_result_def chain.simps)
+    show ?thesis using a b p q False
+      by (auto simp: allocated_result_def run_append flowrun.simps chain.simps; auto simp: inputs_def fun_eq_iff)
+  qed
+next
+  case (Cond c a b)
+  obtain p where c: "flowrun (branch_allocate free c slots) s = Some p"
+    and p: "allocated_result free c env s p"
+    using Cond.IH(1)[of env slots s free] Cond.prems by auto
+  show ?case
+    using Cond.IH(2)[of env slots p free] Cond.IH(3)[of env slots p free]
+      Cond.prems c p
+    by (auto simp: allocated_result_def split: if_splits)
+next
+  case (Let a b)
+  obtain p where a: "flowrun (branch_allocate free a slots) s = Some p"
+    and p: "allocated_result free a env s p"
+    using Let.IH(1)[of env slots s free] Let.prems by auto
+  let ?p = "p\<lparr>stack := registers p Rax # stack p\<rparr>"
+  obtain q where b: "flowrun (branch_allocate free b (0 # map Suc slots)) ?p = Some q"
+    and q: "allocated_result free b (registers p Rax # env) ?p q"
+    using Let.IH(2)[of "registers p Rax # env" "0 # map Suc slots" ?p free]
+      Let.prems p represents_bind[OF Let.prems(2), of "registers p Rax"]
+    by (auto simp: allocated_result_def chain.simps)
+  show ?case using a b p q
+    by (auto simp: allocated_result_def run_append flowrun.simps chain.simps; auto simp: inputs_def fun_eq_iff)
+qed
+
+definition branching :: "expression \<Rightarrow> flow" where
+  "branching e = branch_allocate True (optimise e) []"
+
+theorem branching_return:
+  "scoped 0 e \<Longrightarrow> \<exists>q. flowrun (branching e) s = Some q \<and>
+    registers q Rax = evaluate e [] (inputs s) \<and> stack q = stack s \<and> inputs q = inputs s"
+  using branch_allocate_correct[where env="[]" and slots="[]" and free=True and e="optimise e"]
+    optimise_scoped
+  by (auto simp: branching_def allocated_result_def represents_def optimise_correct)
+
+fun flowaudit :: "flow \<Rightarrow> nat \<Rightarrow> nat option" where
+  "flowaudit (Basic code) n = audit code n"
+| "flowaudit (Sequence a b) n = Option.bind (flowaudit a n) (flowaudit b)"
+| "flowaudit (Choice a b) n = (case (flowaudit a n, flowaudit b n) of
+    (Some x,Some y) \<Rightarrow> if x = y then Some x else None | _ \<Rightarrow> None)"
+
+theorem flowaudit_sound:
+  "flowaudit code (length (stack s)) = Some n \<Longrightarrow>
+    \<exists>q. flowrun code s = Some q \<and> length (stack q) = n \<and> inputs q = inputs s"
+proof (induction code arbitrary: s n)
+  case (Basic code)
+  then show ?case using audit_sound audit_inputs by fastforce
+next
+  case (Sequence a b)
+  then show ?case by (auto split: option.splits bind_splits; fastforce)
+next
+  case (Choice a b)
+  then show ?case by (auto split: option.splits if_splits; fastforce)
+qed
+
+fun flowbytes :: "flow \<Rightarrow> nat list" where
+  "flowbytes (Basic code) = concat (map encode code)"
+| "flowbytes (Sequence a b) = flowbytes a @ flowbytes b"
+| "flowbytes (Choice a b) = [72,133,192,15,132] @ octets 4 (length (flowbytes a) + 5) @
+    flowbytes a @ [233] @ octets 4 (length (flowbytes b)) @ flowbytes b"
+
+fun flowvalid :: "flow \<Rightarrow> bool" where
+  "flowvalid (Basic code) = list_all encodable code"
+| "flowvalid (Sequence a b) = (flowvalid a \<and> flowvalid b)"
+| "flowvalid (Choice a b) = (flowvalid a \<and> flowvalid b \<and>
+    length (flowbytes a) + 5 < 2 ^ 31 \<and> length (flowbytes b) < 2 ^ 31)"
+
+lemma flowbytes_bytes: "set (flowbytes code) \<subseteq> {..<256}"
+  by (induction code) (auto dest: subsetD[OF encode_bytes] subsetD[OF octets_bytes])
+
+function unpack :: "nat \<Rightarrow> nat list \<Rightarrow> flow option" where
+  "unpack 0 bytes = (if bytes = [] then Some (Basic []) else None)"
+| "unpack (Suc fuel) bytes = (if bytes = [] then Some (Basic []) else
+    if take 5 bytes = [72,133,192,15,132] then
+      let offset = integer (take 4 (drop 5 bytes)); pos = 9 + (offset - 5);
+        count = integer (take 4 (drop (Suc pos) bytes)) in
+      if 9 \<le> length bytes \<and> 5 \<le> offset \<and> pos + 5 + count \<le> length bytes \<and>
+        bytes ! pos = 233 then
+        Option.bind (unpack fuel (take (offset - 5) (drop 9 bytes))) (\<lambda>a.
+        Option.bind (unpack fuel (take count (drop (pos + 5) bytes))) (\<lambda>b.
+        map_option (Sequence (Choice a b)) (unpack fuel (drop (pos + 5 + count) bytes))))
+      else None
+    else Option.bind (decode bytes) (\<lambda>(op,rest).
+      map_option (Sequence (Basic [op])) (unpack fuel rest)))"
+  by pat_completeness auto
+termination by (relation "measure (\<lambda>(fuel,bytes). fuel)") auto
+
+declare unpack.simps [simp del]
+
+definition inspect :: "nat list \<Rightarrow> flow option" where
+  "inspect bytes = (if bytes = [] \<or> last bytes \<noteq> 195 \<or> \<not> list_all (\<lambda>b. b < 256) bytes then None else
+    Option.bind (unpack (length bytes) (butlast bytes)) (\<lambda>code.
+      if flowvalid code \<and> flowbytes code = butlast bytes \<and> flowaudit code 0 = Some 0
+      then Some code else None))"
+
+theorem inspected_sound:
+  "inspect bytes = Some code \<Longrightarrow> \<exists>q. flowrun code (s\<lparr>stack := []\<rparr>) = Some q \<and>
+    stack q = [] \<and> inputs q = inputs s"
+  using flowaudit_sound[where s="s\<lparr>stack := []\<rparr>" and n=0]
+  by (auto simp: inspect_def split: if_splits option.splits bind_splits)
+
+end

@@ 1,5 1,5 @@
 theory Frontend
-  imports Allocation
+  imports Branches
 begin
 
 fun finish :: "string \<Rightarrow> string list \<Rightarrow> string list" where


@@ 206,14 206,33 @@ fun listing :: "nat \<Rightarrow> (nat list \<times> opcode) list \<Rightarrow> 
     ''  ['' @ 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> (False,''invalid native block stream'' @ newline)
+    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> (False,''invalid native block stream'' @ newline)
+    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))"


@@ 272,8 291,8 @@ definition source_error_with :: "limits \<Rightarrow> string \<Rightarrow> strin
 
 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 = allocated e; bytes = allocated_bytes e in
-      if audit code 0 = Some 0 \<and> list_all encodable code then
+    | 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))"

@@ 58,6 58,21 @@ def main():
         invoke(source,binary)
         listing = invoke('disassemble',binary)
         assert 'push rax' in listing and 'pop rcx' in listing
+        source.write_text('(if x (+ y 7) (- t 9))')
+        invoke(source,binary)
+        listing = invoke('disassemble',binary)
+        assert 'jz ' in listing and 'jmp ' in listing and 'conditional ' not in listing
+        invoke('check',binary)
+        original = binary.read_bytes()
+        branch = original.index(bytes.fromhex('48 85 c0 0f 84'))
+        for offset in (0,4,0x7fffffff,0xffffffff):
+            damaged = bytearray(original)
+            damaged[branch+5:branch+9] = offset.to_bytes(4,'little')
+            binary.write_bytes(damaged)
+            invoke('check',binary,ok=False)
+        for cut in range(branch+1,branch+9):
+            binary.write_bytes(original[:cut]+bytes([195]))
+            invoke('check',binary,ok=False)
         for malformed in [b'',bytes([195,0]),bytes([72,199,192,0]),bytes([80])]:
             binary.write_bytes(malformed)
             assert 'invalid native' in invoke('disassemble',binary,ok=False)

@@ 136,6 136,23 @@ def main():
     comparisons = 0
     with tempfile.TemporaryDirectory() as directory:
         path, binary = Path(directory) / "source", Path(directory) / "binary"
+        path.write_text('(if x (+ y 7) (- t 9))')
+        subprocess.run([ROOT / '.build/remy',path,binary],check=True,capture_output=True)
+        conditional = binary.read_bytes()
+        start = conditional.index(bytes.fromhex('48 85 c0 0f 84'))
+        otherwise = start + 9 + int.from_bytes(conditional[start+5:start+9],'little')
+        damaged = bytearray(conditional)
+        damaged[otherwise:otherwise+2] = bytes.fromhex('0f 0b')
+        assert execute(bytes(damaged),[(1,3,2)]) == [10]
+        try:
+            execute(bytes(damaged),[(0,3,2)])
+        except RuntimeError as error:
+            assert 'status -4' in str(error), error
+        else:
+            raise AssertionError('selected poisoned branch did not execute')
+        damaged = bytearray(conditional)
+        damaged[start+9:start+11] = bytes.fromhex('0f 0b')
+        assert execute(bytes(damaged),[(0,3,2)]) == [MASK-6]
         for case in cases:
             path.write_text(source(case))
             result = subprocess.run([ROOT / ".build/remy", path, binary], capture_output=True, text=True, timeout=30)