feat(encoding): prove canonical decoding and instruction injectivity

2 files changed, +27 −0

@@ -53,6 +53,23 @@ theorem decode_encode:
53	53	by (cases op)
54	54	(auto simp: byte_join nat_less_iff div_less_iff_less_mult split: bool.splits if_splits)
55	55
	56	+theorem decode_canonical:
	57	+ "decode bs = Some (op, rest) \<Longrightarrow> encodable op \<and> bs = encode op @ rest"
	58	+ by (cases bs)
	59	+ (auto simp: nat_less_iff div_less_iff_less_mult mod_less div_eq_0_iff
	60	+ nat_add_distrib nat_mult_distrib
	61	+ split: if_splits list.splits)
	62	+
	63	+corollary decode_progress:
	64	+ "decode bs = Some (op, rest) \<Longrightarrow> length rest < length bs"
	65	+ using decode_canonical[of bs op rest]
	66	+ by (cases op) (auto split: bool.splits)
	67	+
	68	+theorem encode_injective:
	69	+ "encodable a \<Longrightarrow> encodable b \<Longrightarrow> encode a = encode b \<longleftrightarrow> a = b"
	70	+ using decode_encode[of a "[]"] decode_encode[of b "[]"]
	71	+ by (metis append_Nil option.inject prod.inject)
	72	+
56	73	fun lower :: "nat instruction list \<Rightarrow> nat set \<Rightarrow> nat \<Rightarrow> nat instruction \<Rightarrow> operation" where
57	74	"lower p W i Nop = Idle"
58	75	\| "lower p W i Inc = Raise"

@@ -59,6 +59,16 @@ lemma truncated_rejected: "decode [18,1] = None"
59	59	lemma unknown_rejected: "decode [255] = None"
60	60	by eval
61	61
	62	+lemma short_payload_rejected: "decode [16,256] = None"
	63	+ by eval
	64	+
	65	+lemma long_payload_rejected: "decode [19,0,256] = None"
	66	+ by eval
	67	+
	68	+lemma decoder_preserves_tail:
	69	+ "decode [19,255,255,3,255] = Some (Branch True True 32767, [3,255])"
	70	+ by eval
	71	+
62	72	lemma undefined_rejected:
63	73	"compile ''jmp missing'' = Error ''undefined label missing''"
64	74	by eval

~james/span