riscv: use `uint8_t` for `register_t`

`register_t` only needs to be able to index into the TCB user context
array, which has 35 entries on RISC-V. Therefore `uint8_t` is
sufficient.

Using the smallest possible type for `register_t` helps with binary
verification. This shrinks static read-only data, which in turn reduces
the complexity of binary verification proof search.

This commit verifies the corresponding C kernel patch.

Co-authored-by: Zoltan Kocsis <Zoltan.Kocsis@data61.csiro.au>
Signed-off-by: Mitchell Buckley <Mitchell.Buckley@data61.csiro.au>
Signed-off-by: Zoltan Kocsis <Zoltan.Kocsis@data61.csiro.au>

lib/Word_Lib/Word_Lemmas_Internal.thy

@@ -623,4 +623,26 @@ lemma word_le_1:
   shows "w \<le> 1 \<longleftrightarrow> w = 0 \<or> w = 1"
   using dual_order.antisym lt1_neq0 word_zero_le by blast
 
+lemma less_ucast_ucast_less':
+  "x < UCAST('b \<rightarrow> 'a) y \<Longrightarrow> UCAST('a \<rightarrow> 'b) x < y"
+  for x :: "'a::len word" and y :: "'b::len word"
+  by (clarsimp simp: order.strict_iff_order dual_order.antisym le_ucast_ucast_le)
+
+lemma ucast_up_less_bounded_implies_less_ucast_down':
+  assumes len: "LENGTH('a::len) < LENGTH('b::len)"
+  assumes bound: "y < 2 ^ LENGTH('a)"
+  assumes less: "UCAST('a \<rightarrow> 'b) x < y"
+  shows "x < UCAST('b \<rightarrow> 'a) y"
+  apply (rule le_less_trans[OF _ ucast_mono[OF less bound]])
+  using len by (simp add: is_down ucast_down_ucast_id)
+
+lemma ucast_up_less_bounded_iff_less_ucast_down':
+  assumes len: "LENGTH('a::len) < LENGTH('b::len)"
+  assumes bound: "y < 2 ^ LENGTH('a)"
+  shows "UCAST('a \<rightarrow> 'b) x < y \<longleftrightarrow> x < UCAST('b \<rightarrow> 'a) y"
+  apply (rule iffI)
+   prefer 2
+   apply (simp add: less_ucast_ucast_less')
+  using assms by (rule ucast_up_less_bounded_implies_less_ucast_down')
+
 end

proof/crefine/RISCV64/StateRelation_C.thy

@@ -207,7 +207,7 @@ definition
   \<and> tcb_queue_relation getNext getPrev hp queue NULL qhead"
 
 fun
-  register_from_H :: "register \<Rightarrow> machine_word"
+  register_from_H :: "register \<Rightarrow> register_idx"
   where
     "register_from_H RISCV64.LR = scast Kernel_C.LR"
 |   "register_from_H RISCV64.SP = scast Kernel_C.SP"

proof/crefine/RISCV64/SyscallArgs_C.thy

@@ -602,11 +602,6 @@ lemma nat_less_4_cases:
   "(x::nat) < 4 \<Longrightarrow> x=0 \<or> x=1 \<or> x=2 \<or> x=3"
   by clarsimp
 
-lemma msgRegisters_scast:
-  "n < unat (scast n_msgRegisters :: machine_word) \<Longrightarrow>
-  unat (scast (index msgRegistersC n)::machine_word) = unat (index msgRegistersC n)"
-  by (simp add: kernel_all_global_addresses.msgRegisters_def fupdate_def update_def n_msgRegisters_def)
-
 lemma asUser_cur_obj_at':
   assumes f: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>"
   shows "\<lbrace>\<lambda>s. obj_at' (\<lambda>tcb. P (atcbContextGet (tcbArch tcb))) (ksCurThread s) s \<and> t = ksCurThread s\<rbrace>
@@ -1058,7 +1053,6 @@ lemma index_msgRegisters_less':
 
 lemma index_msgRegisters_less:
   "n < 4 \<Longrightarrow> index msgRegistersC n <s 35"
-  "n < 4 \<Longrightarrow> index msgRegistersC n < 35"
   using index_msgRegisters_less'
   by (simp_all add: word_sless_msb_less)
 
@@ -1131,15 +1125,15 @@ lemma getSyscallArg_ccorres_foo:
        apply (rule conseqPre, vcg)
        apply (clarsimp simp: rf_sr_ksCurThread)
        apply (drule (1) obj_at_cslift_tcb)
-       apply (clarsimp simp: typ_heap_simps' msgRegisters_scast)
+       apply (clarsimp simp: typ_heap_simps')
        apply (clarsimp simp: ctcb_relation_def ccontext_relation_def
                              msgRegisters_ccorres atcbContextGet_def
                              carch_tcb_relation_def cregs_relation_def)
        apply (subst (asm) msgRegisters_ccorres)
         apply (clarsimp simp: n_msgRegisters_def)
-       apply (simp add: n_msgRegisters_def word_less_nat_alt)
-       apply (simp add: index_msgRegisters_less unat_less_helper)
-      apply wp[1]
+        apply (clarsimp simp: n_msgRegisters_def word_less_nat_alt word_upcast_0_sle)
+       apply (clarsimp simp: index_msgRegisters_less' ucast_up_less_bounded_iff_less_ucast_down')
+       apply wp[1]
      apply (wp getMRs_tcbContext)
     apply simp
    apply (rule ccorres_seq_skip [THEN iffD2])

proof/crefine/RISCV64/TcbAcc_C.thy

@@ -120,13 +120,12 @@ lemma register_from_H_less:
   by (cases hr, simp_all add: "StrictC'_register_defs")
 
 lemma register_from_H_sless:
-  "register_from_H hr <s 35"
+  "UCAST(register_idx_len \<rightarrow> int_literal_len) (register_from_H hr) <s 0x23"
   by (cases hr, simp_all add: "StrictC'_register_defs" word_sless_def word_sle_def)
 
-lemma register_from_H_0_sle[simp]:
-  "0 <=s register_from_H hr"
-  using word_0_sle_from_less[OF order_less_le_trans] register_from_H_less
-  by fastforce
+lemma register_from_H_0_sle'[simp]:
+  "0 <=s UCAST(register_idx_len \<rightarrow> int_literal_len) (register_from_H hr)"
+  by (cases hr, simp_all add: "StrictC'_register_defs" word_sless_def word_sle_def)
 
 lemma getRegister_ccorres [corres]:
   "ccorres (=) ret__unsigned_long_' \<top>

proof/crefine/RISCV64/Wellformed_C.thy

@@ -42,6 +42,10 @@ type_synonym tcb_cnode_array = "cte_C[5]"
 type_synonym registers_count = 35
 type_synonym registers_array = "machine_word[registers_count]"
 
+type_synonym register_idx_len = 8
+type_synonym register_idx = "register_idx_len word"
+type_synonym int_literal_len = "32 signed"
+
 abbreviation "user_context_Ptr \<equiv> Ptr :: addr \<Rightarrow> user_context_C ptr"
 abbreviation "machine_word_Ptr \<equiv> Ptr :: addr \<Rightarrow> machine_word ptr"
 abbreviation "tcb_cnode_Ptr \<equiv> Ptr :: addr \<Rightarrow> tcb_cnode_array ptr"