ClockworkBase32.thy

(* This file is to be opened in Isabelle2020 available from
   https://isabelle.in.tum.de/
   Lots of symbols look nicer there. Instead of ↦, you'll see an arrow.
   Moreover, Isabelle checks definitions are definitions and theorems are theorems.
 *)

text ‹
Copyright 2020 Yoichi Hirai
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: 
The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
›

theory ClockworkBase32

imports Main "HOL-Word.Word"

begin

section ‹Clockwork Base32 Encoding›

text ‹Clockwork Base32 specified in \url{https://gist.github.com/szktty/228f85794e4187882a77734c89c384a8} 
encodes a byte sequence into a sequence of characters. The decoding recovers the original byte sequence.
This file contains theorems verifying that fact.›

section ‹Definitions›

subsection ‹Definition of Encoding and Decoding›

text ‹During the encoding and decoding, we often use the combination of five bits.›
type_synonym quinb = "5 word"

text ‹During decoding, we convert a character into five bits. This operation might fail.
The definition uses the finite map notation. Any char that's not listed is converted to None.›
definition decode_quinb :: "char ⇒ quinb option"
  where
"decode_quinb =
[ CHR ''0'' ↦ 0, CHR ''O'' ↦ 0, CHR ''o'' ↦ 0, CHR ''1'' ↦ 1
, CHR ''I'' ↦ 1, CHR ''i'' ↦ 1, CHR ''L'' ↦ 1, CHR ''l'' ↦ 1
, CHR ''2'' ↦ 2, CHR ''3'' ↦ 3, CHR ''4'' ↦ 4, CHR ''5'' ↦ 5
, CHR ''6'' ↦ 6, CHR ''7'' ↦ 7, CHR ''8'' ↦ 8, CHR ''9'' ↦ 9
, CHR ''A'' ↦ 10, CHR ''a'' ↦ 10, CHR ''B'' ↦ 11, CHR ''b'' ↦ 11
, CHR ''C'' ↦ 12, CHR ''c'' ↦ 12, CHR ''D'' ↦ 13, CHR ''d'' ↦ 13
, CHR ''E'' ↦ 14, CHR ''e'' ↦ 14, CHR ''F'' ↦ 15, CHR ''f'' ↦ 15
, CHR ''G'' ↦ 16, CHR ''g'' ↦ 16, CHR ''H'' ↦ 17, CHR ''h'' ↦ 17
, CHR ''J'' ↦ 18, CHR ''j'' ↦ 18, CHR ''K'' ↦ 19, CHR ''k'' ↦ 19
, CHR ''M'' ↦ 20, CHR ''m'' ↦ 20, CHR ''N'' ↦ 21, CHR ''n'' ↦ 21
, CHR ''P'' ↦ 22, CHR ''p'' ↦ 22, CHR ''Q'' ↦ 23, CHR ''q'' ↦ 23
, CHR ''R'' ↦ 24, CHR ''r'' ↦ 24, CHR ''S'' ↦ 25, CHR ''s'' ↦ 25
, CHR ''T'' ↦ 26, CHR ''t'' ↦ 26, CHR ''V'' ↦ 27, CHR ''v'' ↦ 27
, CHR ''W'' ↦ 28, CHR ''w'' ↦ 28, CHR ''X'' ↦ 29, CHR ''x'' ↦ 29
, CHR ''Y'' ↦ 30, CHR ''y'' ↦ 30, CHR ''Z'' ↦ 31, CHR ''z'' ↦ 31]"

text ‹During encoding, we convert five bits into a character. The specification sometimes allows
multiple encodings, but here we define the most typical encoding. This operation never fails.›

definition typical_encode_quinb :: "quinb ⇒ char" where
"typical_encode_quinb x =
   [ CHR ''0'', CHR ''1'', CHR ''2'', CHR ''3'', CHR ''4'', CHR ''5'', CHR ''6''
   , CHR ''7'', CHR ''8'', CHR ''9'', CHR ''A'', CHR ''B'', CHR ''C'', CHR ''D''
   , CHR ''E'', CHR ''F'', CHR ''G'', CHR ''H'', CHR ''J'', CHR ''K'', CHR ''M''
   , CHR ''N'', CHR ''P'', CHR ''Q'', CHR ''R'', CHR ''S'', CHR ''T'', CHR ''V''
   , CHR ''W'', CHR ''X'', CHR ''Y'', CHR ''Z''] ! unat x"

text ‹A sequence of five-bit parts can be encoded as a sequence of characters.›

definition typical_encoding_quinb_to_char_list :: "quinb list ⇒ char list" where
"typical_encoding_quinb_to_char_list l = map typical_encode_quinb l"

text ‹A sequence of characters can be decoded to a sequence of five-bit parts.›
definition decode_char_list :: "char list ⇒ quinb list option"  where
"decode_char_list cl = those (map decode_quinb cl)"

text ‹A list of boolean can be encoded as a sequence of five-bit parts.›
fun bl_to_quinb :: "bool list ⇒ quinb list" where
    "bl_to_quinb [] = []"
  | "bl_to_quinb [x] = [of_bl [x, False, False, False, False]]"
  | "bl_to_quinb [x, y] = [of_bl [x, y, False, False, False]]"
  | "bl_to_quinb [x, y, z] = [of_bl [x, y, z, False, False]]"
  | "bl_to_quinb [x, y, z, v] = [of_bl [x, y, z, v, False]]"
  | "bl_to_quinb (x # y # z # v # w # rest) = of_bl [x, y, z, v, w] # bl_to_quinb rest"

text ‹A list of five-bit parts can be decoded to a list of booleans.›
fun quinb_to_bl :: "quinb list ⇒ bool list" where
"quinb_to_bl [] = []" |
"quinb_to_bl (q # rest) = ((to_bl q) @ (quinb_to_bl rest))"

text ‹A byte is eight bits.›
type_synonym byte = "8 word"

text ‹We can decode a sequence of bits into a sequence of bytes. We ignore small tails.›
fun bl_to_byte_list :: "bool list ⇒ byte list" where
"bl_to_byte_list lst =
   (if length lst < 8 then [] else
       of_bl (take 8 lst) # bl_to_byte_list (drop 8 lst))"

text ‹A list of bytes can be transformed into a list of booleans.›
fun byte_list_to_bl :: "byte list ⇒ bool list" where
"byte_list_to_bl [] = []"
| "byte_list_to_bl (a # rest) = to_bl a @ byte_list_to_bl rest"

definition typical_encoding_to_quinb :: "byte list ⇒ quinb list" where
"typical_encoding_to_quinb x = bl_to_quinb (byte_list_to_bl x)"

definition decoding_quinb :: "quinb list ⇒ byte list" where
"decoding_quinb y = bl_to_byte_list (quinb_to_bl y)"

text ‹The typical encoding of a byte list is defined like this.›
definition typical_encoding :: "byte list ⇒ char list"
  where "typical_encoding = typical_encoding_quinb_to_char_list ∘ typical_encoding_to_quinb"

text ‹The decoding involves option type because it might fail.›
definition decoding :: "char list ⇒ byte list option"
  where "decoding = (map_option decoding_quinb) ∘ decode_char_list"

subsection ‹Test vectors provided in the specification›

definition test_input_1 :: "byte list"
  where "test_input_1 = []"

lemma test1 : "typical_encoding test_input_1 = []"
  by (simp add: test_input_1_def typical_encoding_def typical_encoding_quinb_to_char_list_def typical_encoding_to_quinb_def)

definition test_input_2 :: "byte list"
  where "test_input_2 = map (of_int ∘ int_of_integer ∘ integer_of_char) ''foobar''"

lemma test2 : "typical_encoding test_input_2 = ''CSQPYRK1E8''"
  by(simp add: test_input_2_def integer_of_char_def typical_encoding_def
  typical_encoding_to_quinb_def
  typical_encoding_quinb_to_char_list_def
  typical_encode_quinb_def)

definition test_input_3 :: "byte list"
  where "test_input_3 = map (of_int ∘ int_of_integer ∘ integer_of_char) ''Hello, world!''"

lemma test3 : "typical_encoding test_input_3 = ''91JPRV3F5GG7EVVJDHJ22''"
  by(simp add: test_input_3_def integer_of_char_def typical_encoding_def
  typical_encoding_to_quinb_def
  typical_encoding_quinb_to_char_list_def
  typical_encode_quinb_def)

definition test_input_4 :: "byte list"
  where "test_input_4 = map (of_int ∘ int_of_integer ∘ integer_of_char) ''The quick brown fox jumps over the lazy dog.''"

lemma test4 : "typical_encoding test_input_4 = ''AHM6A83HENMP6TS0C9S6YXVE41K6YY10D9TPTW3K41QQCSBJ41T6GS90DHGQMY90CHQPEBG''"
  by(simp add: test_input_4_def integer_of_char_def typical_encoding_def
  typical_encoding_to_quinb_def
  typical_encoding_quinb_to_char_list_def
  typical_encode_quinb_def)

subsection ‹All possible encoding›

text ‹Each character can be mapped to a set containing both upper and lower cases.›
definition cappy :: "char set set" where
"cappy = {{CHR ''a'', CHR ''A''}, {CHR ''b'', CHR ''B''}, {CHR ''c'', CHR ''C''},
{CHR ''d'', CHR ''D''}, {CHR ''e'', CHR ''E''}, {CHR ''f'', CHR ''F''},
{CHR ''g'', CHR ''G''}, {CHR ''h'', CHR ''H''}, {CHR ''i'', CHR ''I''},
{CHR ''j'', CHR ''J''}, {CHR ''k'', CHR ''K''}, {CHR ''l'', CHR ''L''},
{CHR ''m'', CHR ''M''}, {CHR ''n'', CHR ''N''}, {CHR ''o'', CHR ''O''},
{CHR ''p'', CHR ''P''}, {CHR ''q'', CHR ''Q''}, {CHR ''r'', CHR ''R''},
{CHR ''s'', CHR ''S''}, {CHR ''t'', CHR ''T''}, {CHR ''u'', CHR ''U''},
{CHR ''v'', CHR ''V''}, {CHR ''w'', CHR ''W''}, {CHR ''x'', CHR ''X''},
{CHR ''y'', CHR ''Y''}, {CHR ''z'', CHR ''Z''}}"

text ‹So, instead of encoding to 'E', 'e' is also allowed.›
definition blur :: "char ⇒ char set" where
"blur c = {x | x. x = c ∨ (∃ s. s ∈ cappy ∧ x ∈ s ∧ c ∈ s )}"

text "All possible encoding of five bits"
definition possible_encode_quinb :: "quinb ⇒ char set"
  where "possible_encode_quinb x = blur (typical_encode_quinb x)"

definition encoding_quinb_to_char_list :: "quinb list ⇒ char list set" where
"encoding_quinb_to_char_list l = listset (map possible_encode_quinb l)"

definition possible_encoding :: "byte list ⇒ char list set"
  where "possible_encoding = encoding_quinb_to_char_list ∘ typical_encoding_to_quinb"

section ‹Auxiliary definitions and lemmas›

text ‹This section contains auxiliary lemmas that human readers can skip.›

text ‹If you prove something for 0, 1, 2, ..., 31, you prove it for any natural number smaller than 32.›
lemma thirtytwo_possibilities:
"((x :: nat) = 0 ⟹ P) ⟹ (x = 1 ⟹ P) ⟹ (x = 2 ⟹ P) ⟹
 (x = 3 ⟹ P) ⟹ (x = 4 ⟹ P) ⟹ (x = 5 ⟹ P) ⟹
 (x = 6 ⟹ P) ⟹ (x = 7 ⟹ P) ⟹ (x = 8 ⟹ P) ⟹ (x = 9 ⟹ P) ⟹
 (x = 10 ⟹ P) ⟹ (x = 11 ⟹ P) ⟹ (x = 12 ⟹ P) ⟹
 (x = 13 ⟹ P) ⟹ (x = 14 ⟹ P) ⟹ (x = 15 ⟹ P) ⟹
 (x = 16 ⟹ P) ⟹ (x = 17 ⟹ P) ⟹ (x = 18 ⟹ P) ⟹
 (x = 19 ⟹ P) ⟹ (x = 20 ⟹ P) ⟹ (x = 21 ⟹ P) ⟹
 (x = 22 ⟹ P) ⟹ (x = 23 ⟹ P) ⟹ (x = 24 ⟹ P) ⟹
 (x = 25 ⟹ P) ⟹ (x = 26 ⟹ P) ⟹ (x = 27 ⟹ P) ⟹
 (x = 28 ⟹ P) ⟹ (x = 29 ⟹ P) ⟹ (x = 30 ⟹ P) ⟹
 (x = 31 ⟹ P) ⟹  x < 32 ⟹ P"
  apply(cases "x < 16")
   apply(cases "x < 8")
    apply(cases "x < 4")
     apply(cases "x < 2")
      apply(cases "x < 1")
       apply blast
      apply simp
     apply (metis One_nat_def Suc_1 eval_nat_numeral(2) less_antisym numeral_3_eq_3 semiring_norm(26) semiring_norm(27))
    apply (metis eval_nat_numeral(2) eval_nat_numeral(3) less_antisym semiring_norm(26) semiring_norm(27) semiring_norm(28))
   apply (metis eval_nat_numeral(2) eval_nat_numeral(3) less_antisym semiring_norm(26) semiring_norm(27) semiring_norm(28))
  apply(cases "x < 24")
   apply (metis eval_nat_numeral(2) eval_nat_numeral(3) less_antisym semiring_norm(27) semiring_norm(28))
  by (metis eval_nat_numeral(2) eval_nat_numeral(3) less_antisym semiring_norm(26) semiring_norm(27) semiring_norm(28))

text ‹If you prove something for 0, 1, 2, ..., 31, then you prove it for all possible five-bit
combinations.›
lemma five_bits_32:
"((x :: quinb) = 0 ⟹ P) ⟹ (x = 1 ⟹ P) ⟹ (x = 2 ⟹ P) ⟹
 (x = 3 ⟹ P) ⟹ (x = 4 ⟹ P) ⟹ (x = 5 ⟹ P) ⟹ (x = 6 ⟹ P) ⟹
 (x = 7 ⟹ P) ⟹ (x = 8 ⟹ P) ⟹ (x = 9 ⟹ P) ⟹ (x = 10 ⟹ P) ⟹
 (x = 11 ⟹ P) ⟹ (x = 12 ⟹ P) ⟹ (x = 13 ⟹ P) ⟹ (x = 14 ⟹ P) ⟹
 (x = 15 ⟹ P) ⟹ (x = 16 ⟹ P) ⟹ (x = 17 ⟹ P) ⟹ (x = 18 ⟹ P) ⟹
 (x = 19 ⟹ P) ⟹ (x = 20 ⟹ P) ⟹ (x = 21 ⟹ P) ⟹ (x = 22 ⟹ P) ⟹
 (x = 23 ⟹ P) ⟹ (x = 24 ⟹ P) ⟹ (x = 25 ⟹ P) ⟹ (x = 26 ⟹ P) ⟹
 (x = 27 ⟹ P) ⟹ (x = 28 ⟹ P) ⟹ (x = 29 ⟹ P) ⟹ (x = 30 ⟹ P) ⟹
 (x = 31 ⟹ P) ⟹ P"
  apply(cases x)
  apply simp
  by (metis (no_types, hide_lams) of_nat_1 of_nat_numeral semiring_1_class.of_nat_0 thirtytwo_possibilities)

lemma five_bit_encode_decode: "decode_quinb (typical_encode_quinb x) = Some x"
  apply(rule_tac x = x in five_bits_32)
  by(auto simp add: typical_encode_quinb_def decode_quinb_def)

lemma typical_cons: "typical_encoding_quinb_to_char_list (a # x) =
   typical_encode_quinb a # typical_encoding_quinb_to_char_list x"
  by (simp add: typical_encoding_quinb_to_char_list_def)

lemma decode_char_list_cons : "decode_char_list (a # rest) =
  (case decode_quinb a of
     None ⇒ None |
     Some x ⇒ (case decode_char_list rest of
       None ⇒ None |
       Some r ⇒ Some (x # r))
  )"
  apply(simp add: decode_char_list_def)
  apply(cases "decode_quinb a"; simp)
  by (simp add: decode_char_list_def map_option_case)

lemma ql_cl_ql : "decode_char_list (typical_encoding_quinb_to_char_list l) = Some l"
  apply(induction l)
   apply(simp add: typical_encoding_quinb_to_char_list_def decode_char_list_def)
  by(simp add: typical_encoding_quinb_to_char_list_def decode_char_list_def
    five_bit_encode_decode)

lemma bl_to_quinb_cons : "bl_to_quinb (x # bl) =
  (case bl of 
     [] ⇒ [of_bl [x, False, False, False, False]] |
     [y] ⇒ [of_bl [x, y, False, False, False]] |
     [y, z] ⇒ [of_bl [x, y, z, False, False]] |
     [y, z, v] ⇒ [of_bl [x, y, z, v, False]] |
     (y # z # v # w # rest) ⇒ of_bl [x, y, z, v, w] # bl_to_quinb rest)"
  apply(cases "bl = []")
   apply simp
  apply(cases "∃ y. bl = [y]")
   apply auto
  apply(cases "∃ y z. bl = [y, z]")
   apply force
  apply(cases "∃ y z v. bl = [y, z, v]")
   apply force  
  apply(cases "∃ y z v w rest. bl = y # z # v # w # rest")
   apply force
  by (meson bl_to_quinb.cases)

lemma bl_qb_bl : "∃ tail. quinb_to_bl (bl_to_quinb bl) = bl @ tail ∧ length tail < 5"
  apply(induct bl rule: bl_to_quinb.induct)
        apply auto
      apply(simp add:  word_bl.Abs_inverse)
     apply(simp add:  word_bl.Abs_inverse)
    apply(simp add:  word_bl.Abs_inverse)
   apply(simp add:  word_bl.Abs_inverse)
  by(simp add:  word_bl.Abs_inverse)

lemma length_eight_bits :
  "length x = 8 ⟹
   bl_to_byte_list (x @ rest) = of_bl x # bl_to_byte_list rest"
  by auto

lemma bl_to_byte_list_cons :
  "bl_to_byte_list (to_bl a @ rest) = a # bl_to_byte_list rest"
  by(simp add: length_eight_bits)

text ‹The encoding of five bits into a character and the corresponding decoding results in
the original five bits.›

text "byte list to bit list, might be extended up to five, and back"
lemma byte_list_back :
  "length tail < 5 ⟹ orig = bl_to_byte_list (byte_list_to_bl orig @ tail)"
  apply(induct orig arbitrary: tail)
   apply simp
  by (simp add: bl_to_byte_list_cons)

lemma typical_encoding_decoding_quinb :
  "decoding_quinb (typical_encoding_to_quinb x) = x"
  by (metis bl_qb_bl byte_list_back decoding_quinb_def typical_encoding_to_quinb_def)

text ‹If you change the capitalization, the decoded five bits don't change.›
lemma decode_blur : "x ∈ blur c ⟹ decode_quinb x = decode_quinb c"
  apply(cases c)
  apply(cases "digit0 c"; simp; cases "digit1 c"; simp; cases "digit2 c"; simp; cases "digit3 c"; simp; cases "digit4 c"; cases "digit5 c"; auto simp add: blur_def cappy_def)
  apply(simp add: decode_quinb_def)
  apply(simp add: decode_quinb_def)
  apply(simp add: decode_quinb_def)
  apply(simp add: decode_quinb_def)
  apply(simp add: decode_quinb_def)
  apply(simp add: decode_quinb_def)
  apply(simp add: decode_quinb_def)
  apply(simp add: decode_quinb_def)
  apply(simp add: decode_quinb_def)
  apply(simp add: decode_quinb_def)
  apply(simp add: decode_quinb_def)
  apply(simp add: decode_quinb_def)
  apply(simp add: decode_quinb_def)
  apply(simp add: decode_quinb_def)
  apply(simp add: decode_quinb_def)
  apply(simp add: decode_quinb_def)
  apply(simp add: decode_quinb_def)
  apply(simp add: decode_quinb_def)
  apply(simp add: decode_quinb_def)
  apply(simp add: decode_quinb_def)
  apply(simp add: decode_quinb_def)
  apply(simp add: decode_quinb_def)
  apply(simp add: decode_quinb_def)
  apply(simp add: decode_quinb_def)
  apply(simp add: decode_quinb_def)
  apply(simp add: decode_quinb_def)
  apply(simp add: decode_quinb_def)
  apply(simp add: decode_quinb_def)
  apply(simp add: decode_quinb_def)
  apply(simp add: decode_quinb_def)
  apply(simp add: decode_quinb_def)
  apply(simp add: decode_quinb_def)
  apply(simp add: decode_quinb_def)
  apply(simp add: decode_quinb_def)
  apply(simp add: decode_quinb_def)
  apply(simp add: decode_quinb_def)
  apply(simp add: decode_quinb_def)
  apply(simp add: decode_quinb_def)
  apply(simp add: decode_quinb_def)
  apply(simp add: decode_quinb_def)
  apply(simp add: decode_quinb_def)
  apply(simp add: decode_quinb_def)
  apply(simp add: decode_quinb_def)
  apply(simp add: decode_quinb_def)
  apply(simp add: decode_quinb_def)
  apply(simp add: decode_quinb_def)
  apply(simp add: decode_quinb_def)
  apply(simp add: decode_quinb_def)
  apply(simp add: decode_quinb_def)
  apply(simp add: decode_quinb_def)
  apply(simp add: decode_quinb_def)
  by(simp add: decode_quinb_def)

lemma five_bit_encode_decode_general: "q ∈ possible_encode_quinb x ⟹ decode_quinb q = Some x"
  apply(simp add: possible_encode_quinb_def decode_blur)
  by (simp add: five_bit_encode_decode)

lemma encoding_quinb_cons : "y ∈ encoding_quinb_to_char_list (a # x) = 
  (∃ h r. y = h # r ∧ h ∈ possible_encode_quinb a ∧
   r ∈ encoding_quinb_to_char_list x)"
  apply(cases y)
   apply(simp add: encoding_quinb_to_char_list_def set_Cons_def)
  by(auto simp add: encoding_quinb_to_char_list_def set_Cons_def)

lemma decode_char_possible_typical: "y ∈ encoding_quinb_to_char_list x ⟹
    decode_char_list y =
    decode_char_list (typical_encoding_quinb_to_char_list x)"
  apply(induction x arbitrary: y)
   apply(simp add: typical_encoding_quinb_to_char_list_def encoding_quinb_to_char_list_def)
  apply(auto simp add: encoding_quinb_cons decode_char_list_def five_bit_encode_decode_general)
  using decode_char_list_def ql_cl_ql by auto

lemma quinb_to_char_possible_typical :
  "y ∈ encoding_quinb_to_char_list x ⟹
   decoding y =
   decoding (typical_encoding_quinb_to_char_list x)"
  apply(simp add: decoding_def)
  by (simp add: decode_char_possible_typical)

text "All possible encodings decode the same way as the typical encoding."

lemma encoding_possible_typical :
  "y ∈ possible_encoding x ⟹ decoding y = decoding (typical_encoding x)"
  by (simp add: possible_encoding_def quinb_to_char_possible_typical typical_encoding_def)  

section ‹Theorems›

subsection ‹Typical encoding followed by decoding›

text ‹The typical encoding followed by decoding results in the original byte sequence.›

theorem encode_decode : "decoding (typical_encoding x) = Some x"
  by (simp add: decoding_def ql_cl_ql typical_encoding_decoding_quinb typical_encoding_def)

subsection ‹Any possible encoding followed by decoding›

theorem encode_decode_all : "y ∈ possible_encoding x ⟹ decoding y = Some x"
  by (simp add: encode_decode encoding_possible_typical)

text "Advertisement: we prove theorems for you. https://convenience-logician.de"

end

document.pdf

Oops. I still need to combine the two theorems about

1. byte list <--> "5 bits" list, and
2. "5 bits" list <--> string

---

Done.

Suggestion: turn the Advertisement into a Motto or Creed.