HostedCompilerProofALU.patch

diff --git a/src/HostedCompilerProofALU.v b/src/HostedCompilerProofALU.v
index 536866d..cade5c9 100644
--- a/src/HostedCompilerProofALU.v
+++ b/src/HostedCompilerProofALU.v
@@ -42,6 +42,66 @@ Proof.
   congruence.
 Qed.
 
+Ltac destruct_bpf_opcode x := 
+    refine 
+      match x with
+      | BPFDecoder.BPF_ADD64_IMM => _
+      | BPFDecoder.BPF_ADD64_REG => _
+      | BPFDecoder.BPF_SUB64_IMM => _
+      | BPFDecoder.BPF_SUB64_REG => _
+      | BPFDecoder.BPF_MUL64_IMM => _
+      | BPFDecoder.BPF_MUL64_REG => _
+      | BPFDecoder.BPF_DIV64_IMM => _
+      | BPFDecoder.BPF_DIV64_REG => _
+      | BPFDecoder.BPF_OR64_IMM  => _
+      | BPFDecoder.BPF_OR64_REG  => _
+      | BPFDecoder.BPF_AND64_IMM => _
+      | BPFDecoder.BPF_AND64_REG => _
+      | BPFDecoder.BPF_LSH64_IMM => _
+      | BPFDecoder.BPF_LSH64_REG => _
+      | BPFDecoder.BPF_RSH64_IMM => _
+      | BPFDecoder.BPF_RSH64_REG => _
+      | BPFDecoder.BPF_NEG64     => _
+      | BPFDecoder.BPF_MOD64_IMM => _
+      | BPFDecoder.BPF_MOD64_REG => _
+      | BPFDecoder.BPF_XOR64_IMM => _
+      | BPFDecoder.BPF_XOR64_REG => _
+      | BPFDecoder.BPF_MOV64_IMM => _
+      | BPFDecoder.BPF_MOV64_REG => _
+      | BPFDecoder.BPF_ARSH64_IMM=> _
+      | BPFDecoder.BPF_ARSH64_REG=> _
+      | BPFDecoder.BPF_JA        => _
+      | BPFDecoder.BPF_JEQ_IMM   => _
+      | BPFDecoder.BPF_JEQ_REG   => _
+      | BPFDecoder.BPF_JGT_IMM   => _
+      | BPFDecoder.BPF_JGT_REG   => _
+      | BPFDecoder.BPF_JGE_IMM   => _
+      | BPFDecoder.BPF_JGE_REG   => _
+      | BPFDecoder.BPF_JSET_IMM  => _
+      | BPFDecoder.BPF_JSET_REG  => _
+      | BPFDecoder.BPF_JNE_IMM   => _
+      | BPFDecoder.BPF_JNE_REG   => _
+      | BPFDecoder.BPF_JSGT_IMM  => _
+      | BPFDecoder.BPF_JSGT_REG  => _
+      | BPFDecoder.BPF_JSGE_IMM  => _
+      | BPFDecoder.BPF_JSGE_REG  => _
+      | BPFDecoder.BPF_CALL      => _
+      | BPFDecoder.BPF_EXIT      => _ 
+      | _                        => _
+      end.
+
+
+  Lemma decode_add64:
+    forall (dst src : Ouro.reg) (i : BPFDecoder.bpf_insn),
+      BPFDecoder.decode_insn i = Some (Ouro.alu64_add_x dst src) ->
+      binary_value (BPFDecoder.insn_code i) = BPFDecoder.BPF_ADD64_REG %Z.
+  Proof.
+    unfold BPFDecoder.decode_insn.
+    intros dst src i.
+    destruct_bpf_opcode (binary_value i.(BPFDecoder.insn_code));
+    intros; repeat (try break_match; try discriminate; try reflexivity).
+  Qed.
+
 Theorem hosted_alu64_add_rr :
   forall dst src,
     HostedCompilerCase (Ouro.alu64_add_x dst src).
@@ -58,23 +118,42 @@ Proof.
   unfold one_instr_compiler_spec in OneInstrSpec.
   unfold encode_spec in OneInstrSpec.
   break_match.
+  
+  assert (binary_value (BPFDecoder.insn_code bpf_insn) = BPFDecoder.BPF_ADD64_REG) 
+    by eauto using decode_add64.
+