Skip to content

Commit 27ec4ff

Browse files
DominicPMDominicPM
committed
proofs/isabelle: wire up split theories, add PDF document generation, remove monolithic files
Update ROOT with PDF output, document sections, and theory ordering. Update Makefile with build/pdf/clean targets. Add document/root.tex with LaTeX preamble. Update imports in MLKEM_Functional_Correctness.thy, MLKEM_Machine_Model.thy, and MLKEM_Poly_Definitions.thy. Remove superseded monolithic Common.thy and MLKEM_Poly_Functional_Correctness.thy.
1 parent 1990ba5 commit 27ec4ff

19 files changed

Lines changed: 1379 additions & 0 deletions

‎proofs/isabelle/.gitignore‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
# Isabelle/jEdit backup files
2+
*~
3+
# Isabelle build output
4+
output/

‎proofs/isabelle/MLKEM_Functional_Correctness.thy‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
theory MLKEM_Functional_Correctness
2+
imports
3+
MLKEM_Machine_Model_Instance
4+
MLKEM_FC_InvNTT
5+
MLKEM_FC_PolyLoop
6+
MLKEM_NTT_Correctness
7+
begin
8+
9+
text \<open>
10+
Top-level entry point for \<^verbatim>\<open>mlkem-native\<close> functional-correctness proofs.
11+
12+
Intentionally empty, barring imports.
13+
\<close>
14+
15+
end

‎proofs/isabelle/MLKEM_Machine_Model.thy‎

Lines changed: 58 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,58 @@
1+
theory MLKEM_Machine_Model
2+
imports "Micro_C_Examples.Simple_C_Functions"
3+
begin
4+
5+
(*<*)
6+
text \<open>
7+
Machine-model assumptions used by generated \<^verbatim>\<open>mlkem-native\<close> C definitions.
8+
Types are extracted first so locale assumptions can depend on the generated
9+
C record/datatype names.
10+
\<close>
11+
12+
micro_c_file manifest: "generated/manifests/poly.types.manifest" "generated/c/poly.pre.c"
13+
14+
locale c_mlk_machine_model =
15+
c_pointer_model c_ptr_add c_ptr_shift_signed c_ptr_diff
16+
c_ptr_less c_ptr_le c_ptr_greater c_ptr_ge
17+
c_ptr_to_uintptr c_uintptr_to_ptr +
18+
reference reference_types +
19+
ref_c_mlk_poly: reference_allocatable reference_types _ _ _ _ _ _ _ c_mlk_poly_prism +
20+
ref_c_mlk_poly_mulcache: reference_allocatable reference_types _ _ _ _ _ _ _ c_mlk_poly_mulcache_prism +
21+
ref_c_uint: reference_allocatable reference_types _ _ _ _ _ _ _ c_uint_prism +
22+
ref_c_int: reference_allocatable reference_types _ _ _ _ _ _ _ c_int_prism +
23+
ref_c_short: reference_allocatable reference_types _ _ _ _ _ _ _ c_short_prism +
24+
ref_c_ushort: reference_allocatable reference_types _ _ _ _ _ _ _ c_ushort_prism +
25+
ref_c_short_list: reference_allocatable reference_types _ _ _ _ _ _ _ c_short_list_prism
26+
for c_ptr_add :: \<open>('addr, 8 word list) gref \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> ('addr, 8 word list) gref\<close>
27+
and c_ptr_shift_signed :: \<open>('addr, 8 word list) gref \<Rightarrow> int \<Rightarrow> nat \<Rightarrow> ('addr, 8 word list) gref\<close>
28+
and c_ptr_diff :: \<open>('addr, 8 word list) gref \<Rightarrow> ('addr, 8 word list) gref \<Rightarrow> nat \<Rightarrow> int\<close>
29+
and c_ptr_less :: \<open>('addr, 8 word list) gref \<Rightarrow> ('addr, 8 word list) gref \<Rightarrow> bool\<close>
30+
and c_ptr_le :: \<open>('addr, 8 word list) gref \<Rightarrow> ('addr, 8 word list) gref \<Rightarrow> bool\<close>
31+
and c_ptr_greater :: \<open>('addr, 8 word list) gref \<Rightarrow> ('addr, 8 word list) gref \<Rightarrow> bool\<close>
32+
and c_ptr_ge :: \<open>('addr, 8 word list) gref \<Rightarrow> ('addr, 8 word list) gref \<Rightarrow> bool\<close>
33+
and c_ptr_to_uintptr :: \<open>('addr, 8 word list) gref \<Rightarrow> int\<close>
34+
and c_uintptr_to_ptr :: \<open>int \<Rightarrow> ('addr, 8 word list) gref\<close>
35+
and reference_types :: \<open>'s::{sepalg} \<Rightarrow> 'addr \<Rightarrow> 8 word list \<Rightarrow> c_abort \<Rightarrow> 'i prompt \<Rightarrow>
36+
'o prompt_output \<Rightarrow> unit\<close>
37+
and c_mlk_poly_prism :: \<open>(8 word list, c_mlk_poly) prism\<close>
38+
and c_mlk_poly_mulcache_prism :: \<open>(8 word list, c_mlk_poly_mulcache) prism\<close>
39+
and c_uint_prism :: \<open>(8 word list, c_uint) prism\<close>
40+
and c_int_prism :: \<open>(8 word list, c_int) prism\<close>
41+
and c_short_prism :: \<open>(8 word list, c_short) prism\<close>
42+
and c_ushort_prism :: \<open>(8 word list, c_ushort) prism\<close>
43+
and c_short_list_prism :: \<open>(8 word list, c_short list) prism\<close>
44+
begin
45+
46+
adhoc_overloading store_reference_const \<rightleftharpoons> ref_c_mlk_poly.new
47+
adhoc_overloading store_reference_const \<rightleftharpoons> ref_c_mlk_poly_mulcache.new
48+
adhoc_overloading store_reference_const \<rightleftharpoons> ref_c_uint.new
49+
adhoc_overloading store_reference_const \<rightleftharpoons> ref_c_int.new
50+
adhoc_overloading store_reference_const \<rightleftharpoons> ref_c_short.new
51+
adhoc_overloading store_reference_const \<rightleftharpoons> ref_c_ushort.new
52+
adhoc_overloading store_reference_const \<rightleftharpoons> ref_c_short_list.new
53+
adhoc_overloading store_update_const \<rightleftharpoons> update_fun
54+
55+
end
56+
(*>*)
57+
58+
end

‎proofs/isabelle/MLKEM_Machine_Model_Instance.thy‎

Lines changed: 230 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,230 @@
1+
theory MLKEM_Machine_Model_Instance
2+
imports
3+
MLKEM_Machine_Model
4+
"Micro_Rust_Runtime.Runtime_Heap"
5+
"Shallow_Micro_C.C_Byte_Encoding"
6+
begin
7+
8+
section \<open>Consistency model for @{locale c_mlk_machine_model}\<close>
9+
10+
subsection \<open>Default instance for byte lists\<close>
11+
12+
text \<open>
13+
The heap model @{type mem} requires @{class default} on the stored value type.
14+
We instantiate it for lists with the empty list as default value.
15+
\<close>
16+
17+
instantiation list :: (type) default
18+
begin
19+
20+
definition default_list :: \<open>'a list\<close> where
21+
\<open>default_list = []\<close>
22+
23+
instance ..
24+
25+
end
26+
27+
text \<open>
28+
We provide a concrete interpretation of the @{locale c_mlk_machine_model} locale
29+
using the AutoCorrode heap model from @{theory Micro_Rust_Runtime.Runtime_Heap},
30+
together with byte-level prisms for all C types.
31+
The successful processing of this theory proves that the locale assumptions
32+
are consistent (satisfiable).
33+
\<close>
34+
35+
subsection \<open>Byte prism for @{type c_short} lists\<close>
36+
37+
fun decode_c_short_list :: \<open>8 word list \<Rightarrow> c_short list option\<close> where
38+
\<open>decode_c_short_list [] = Some []\<close>
39+
| \<open>decode_c_short_list [_] = None\<close>
40+
| \<open>decode_c_short_list (a # b # rest) =
41+
Option.bind (prism_project c_short_byte_prism [a, b])
42+
(\<lambda>c. map_option ((#) c) (decode_c_short_list rest))\<close>
43+
44+
definition c_short_list_byte_prism :: \<open>(8 word list, c_short list) prism\<close> where
45+
\<open>c_short_list_byte_prism \<equiv> make_prism
46+
(\<lambda>cs. concat (List.map (prism_embed c_short_byte_prism) cs))
47+
decode_c_short_list\<close>
48+
49+
text \<open>
50+
Validity of @{const c_short_list_byte_prism}: Each @{type c_short} is encoded as exactly
51+
2 bytes via @{const c_short_byte_prism}. Decoding splits the byte list into 2-byte chunks
52+
and decodes each chunk.
53+
\<close>
54+
55+
lemma c_short_byte_prism_embed_length:
56+
shows \<open>length (prism_embed c_short_byte_prism c) = 2\<close>
57+
unfolding c_short_byte_prism_def prism_compose_def word_sword_iso_prism_def iso_prism_def
58+
word16_byte_list_prism_le_def list_fixlen_prism_def by (simp add: list_fixlen_embed_def)
59+
60+
lemma decode_encode_c_short_list:
61+
shows \<open>decode_c_short_list (concat (List.map (prism_embed c_short_byte_prism) cs)) = Some cs\<close>
62+
proof (induction cs)
63+
case Nil
64+
then show ?case by simp
65+
next
66+
case (Cons c cs)
67+
obtain a b where ab: \<open>prism_embed c_short_byte_prism c = [a, b]\<close>
68+
using c_short_byte_prism_embed_length[of c] by (metis (no_types, opaque_lifting) length_0_conv
69+
length_Cons length_tl list.sel(3) numeral_2_eq_2 Suc_length_conv)
70+
have proj: \<open>prism_project c_short_byte_prism [a, b] = Some c\<close>
71+
using is_valid_prism_def[of c_short_byte_prism] c_byte_prism_valid(4) ab by metis
72+
show ?case
73+
using Cons.IH by (simp add: ab proj)
74+
qed
75+
76+
lemma encode_decode_c_short_list:
77+
shows \<open>decode_c_short_list bs = Some cs \<Longrightarrow>
78+
bs = concat (List.map (prism_embed c_short_byte_prism) cs)\<close>
79+
proof (induction bs arbitrary: cs rule: decode_c_short_list.induct)
80+
case 1
81+
then show ?case by simp
82+
next
83+
case (2 v)
84+
then show ?case by simp
85+
next
86+
case (3 a b rest)
87+
from 3(2) obtain c where proj: \<open>prism_project c_short_byte_prism [a, b] = Some c\<close> and
88+
mc: \<open>map_option ((#) c) (decode_c_short_list rest) = Some cs\<close>
89+
by (cases \<open>prism_project c_short_byte_prism [a, b]\<close>) auto
90+
from mc obtain cs' where rest_decode: \<open>decode_c_short_list rest = Some cs'\<close> and
91+
cs_eq: \<open>cs = c # cs'\<close>
92+
by (cases \<open>decode_c_short_list rest\<close>) auto
93+
have embed: \<open>[a, b] = prism_embed c_short_byte_prism c\<close>
94+
using is_valid_prism_def[of c_short_byte_prism] c_byte_prism_valid(4) proj by metis
95+
have \<open>rest = concat (List.map (prism_embed c_short_byte_prism) cs')\<close>
96+
using 3(1)[OF proj rest_decode] .
97+
then show ?case
98+
by (simp add: cs_eq embed)
99+
qed
100+
101+
lemma c_short_list_byte_prism_valid:
102+
shows \<open>is_valid_prism c_short_list_byte_prism\<close>
103+
unfolding is_valid_prism_def c_short_list_byte_prism_def by (auto simp: decode_encode_c_short_list
104+
dest: encode_decode_c_short_list)
105+
106+
subsection \<open>Struct iso prisms\<close>
107+
108+
definition c_mlk_poly_struct_prism :: \<open>(c_short list, c_mlk_poly) prism\<close> where
109+
\<open>c_mlk_poly_struct_prism \<equiv> iso_prism make_c_mlk_poly c_mlk_poly_coeffs\<close>
110+
111+
definition c_mlk_poly_mulcache_struct_prism :: \<open>(c_short list, c_mlk_poly_mulcache) prism\<close> where
112+
\<open>c_mlk_poly_mulcache_struct_prism \<equiv> iso_prism make_c_mlk_poly_mulcache c_mlk_poly_mulcache_coeffs\<close>
113+
114+
lemma c_mlk_poly_struct_prism_valid:
115+
shows \<open>is_valid_prism c_mlk_poly_struct_prism\<close>
116+
unfolding c_mlk_poly_struct_prism_def by (rule iso_prism_valid) auto
117+
118+
lemma c_mlk_poly_mulcache_struct_prism_valid:
119+
shows \<open>is_valid_prism c_mlk_poly_mulcache_struct_prism\<close>
120+
unfolding c_mlk_poly_mulcache_struct_prism_def by (rule iso_prism_valid) auto
121+
122+
subsection \<open>Composed byte prisms for struct types\<close>
123+
124+
definition c_mlk_poly_byte_prism :: \<open>(8 word list, c_mlk_poly) prism\<close> where
125+
\<open>c_mlk_poly_byte_prism \<equiv> prism_compose c_short_list_byte_prism c_mlk_poly_struct_prism\<close>
126+
127+
definition c_mlk_poly_mulcache_byte_prism :: \<open>(8 word list, c_mlk_poly_mulcache) prism\<close> where
128+
\<open>c_mlk_poly_mulcache_byte_prism \<equiv>
129+
prism_compose c_short_list_byte_prism c_mlk_poly_mulcache_struct_prism\<close>
130+
131+
lemma c_mlk_poly_byte_prism_valid:
132+
shows \<open>is_valid_prism c_mlk_poly_byte_prism\<close>
133+
unfolding c_mlk_poly_byte_prism_def by (intro prism_compose_valid c_short_list_byte_prism_valid
134+
c_mlk_poly_struct_prism_valid)
135+
136+
lemma c_mlk_poly_mulcache_byte_prism_valid:
137+
shows \<open>is_valid_prism c_mlk_poly_mulcache_byte_prism\<close>
138+
unfolding c_mlk_poly_mulcache_byte_prism_def by (intro prism_compose_valid
139+
c_short_list_byte_prism_valid c_mlk_poly_mulcache_struct_prism_valid)
140+
141+
subsection \<open>Global interpretation of @{locale c_mlk_machine_model}\<close>
142+
143+
text \<open>
144+
The parameter order follows Isabelle's locale convention: implicit parameters
145+
from parent locales (here: @{locale reference}) come first, then the explicit
146+
parameters from the \<open>for\<close> clause.
147+
We provide trivial dummy implementations for @{locale c_pointer_model} parameters.
148+
\<close>
149+
150+
global_interpretation mlk_instance: c_mlk_machine_model
151+
\<comment> \<open>Implicit @{locale reference} parameters\<close>
152+
urust_heap_update_raw_fun
153+
urust_heap_dereference_raw_fun
154+
urust_heap_reference_raw_fun
155+
urust_heap_points_to_raw'
156+
\<open>\<lambda>_. UNIV\<close> UNIV
157+
urust_heap_can_alloc_reference
158+
\<comment> \<open>@{locale c_pointer_model} for-clause parameters (dummy implementations)\<close>
159+
\<open>\<lambda>p _ _. p\<close>
160+
\<open>\<lambda>p _ _. p\<close>
161+
\<open>\<lambda>_ _ _. (0::int)\<close>
162+
\<open>\<lambda>_ _. False\<close>
163+
\<open>\<lambda>_ _. True\<close>
164+
\<open>\<lambda>_ _. True\<close>
165+
\<open>\<lambda>_ _. True\<close>
166+
\<open>\<lambda>_. (0::int)\<close>
167+
\<open>\<lambda>_. undefined\<close>
168+
\<comment> \<open>@{locale reference} type-constraining parameter\<close>
169+
\<open>\<lambda>_ _ _ _ _ _. ()\<close>
170+
\<comment> \<open>Prism parameters for @{locale reference_allocatable} instances\<close>
171+
c_mlk_poly_byte_prism
172+
c_mlk_poly_mulcache_byte_prism
173+
c_uint_byte_prism
174+
c_int_byte_prism
175+
c_short_byte_prism
176+
c_ushort_byte_prism
177+
c_short_list_byte_prism
178+
rewrites \<open>reference_defs.dereference_fun urust_heap_dereference_raw_fun =
179+
urust_heap_dereference_fun\<close>
180+
and \<open>reference_defs.update_fun urust_heap_update_raw_fun urust_heap_dereference_raw_fun =
181+
urust_heap_update_fun\<close>
182+
and \<open>reference_defs.reference_fun urust_heap_reference_raw_fun =
183+
urust_heap_reference_fun\<close>
184+
proof -
185+
show \<open>c_mlk_machine_model
186+
urust_heap_update_raw_fun urust_heap_dereference_raw_fun
187+
urust_heap_reference_raw_fun urust_heap_points_to_raw'
188+
(\<lambda>_. UNIV) UNIV urust_heap_can_alloc_reference
189+
(\<lambda>p _ _. p) (\<lambda>_ _ _. (0::int)) (\<lambda>_ _. False) (\<lambda>_ _. True) (\<lambda>_ _. True)
190+
c_mlk_poly_byte_prism c_mlk_poly_mulcache_byte_prism
191+
c_uint_byte_prism c_int_byte_prism c_short_byte_prism
192+
c_ushort_byte_prism c_short_list_byte_prism\<close>
193+
proof
194+
\<comment> \<open>Prism validity for each @{locale reference_allocatable} instance\<close>
195+
show \<open>is_valid_prism c_mlk_poly_byte_prism\<close>
196+
by (rule c_mlk_poly_byte_prism_valid)
197+
show \<open>is_valid_prism c_mlk_poly_mulcache_byte_prism\<close>
198+
by (rule c_mlk_poly_mulcache_byte_prism_valid)
199+
show \<open>is_valid_prism c_uint_byte_prism\<close>
200+
by (rule c_byte_prism_valid(5))
201+
show \<open>is_valid_prism c_int_byte_prism\<close>
202+
by (rule c_byte_prism_valid(6))
203+
show \<open>is_valid_prism c_short_byte_prism\<close>
204+
by (rule c_byte_prism_valid(4))
205+
show \<open>is_valid_prism c_ushort_byte_prism\<close>
206+
by (rule c_byte_prism_valid(3))
207+
show \<open>is_valid_prism c_short_list_byte_prism\<close>
208+
by (rule c_short_list_byte_prism_valid)
209+
\<comment> \<open>Allocatability: @{term \<open>prism_dom p \<subseteq> UNIV\<close>} is trivially true for each prism\<close>
210+
show \<open>References.can_create_gref_for_prism c_mlk_poly_byte_prism\<close>
211+
by (simp add: References.can_create_gref_for_prism_def)
212+
show \<open>References.can_create_gref_for_prism c_mlk_poly_mulcache_byte_prism\<close>
213+
by (simp add: References.can_create_gref_for_prism_def)
214+
show \<open>References.can_create_gref_for_prism c_uint_byte_prism\<close>
215+
by (simp add: References.can_create_gref_for_prism_def)
216+
show \<open>References.can_create_gref_for_prism c_int_byte_prism\<close>
217+
by (simp add: References.can_create_gref_for_prism_def)
218+
show \<open>References.can_create_gref_for_prism c_short_byte_prism\<close>
219+
by (simp add: References.can_create_gref_for_prism_def)
220+
show \<open>References.can_create_gref_for_prism c_ushort_byte_prism\<close>
221+
by (simp add: References.can_create_gref_for_prism_def)
222+
show \<open>References.can_create_gref_for_prism c_short_list_byte_prism\<close>
223+
by (simp add: References.can_create_gref_for_prism_def)
224+
\<comment> \<open>@{locale c_pointer_model} axioms: trivially satisfied by dummy implementations\<close>
225+
qed auto
226+
qed (auto simp: urust_heap_dereference_fun_def urust_heap_update_fun_def
227+
urust_heap_reference_fun_def)
228+
229+
end
230+

‎proofs/isabelle/MLKEM_Poly_Definitions.thy‎

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
theory MLKEM_Poly_Definitions
2+
imports
3+
MLKEM_Machine_Model
4+
begin
5+
6+
(*<*)
7+
text \<open>
8+
Auto-generated by @{file "pipeline/generate.py"} from preprocessed C.
9+
Source unit: @{file "../../mlkem/src/poly.c"}
10+
Preprocessed unit: @{file "generated/c/poly.pre.c"}
11+
\<close>
12+
13+
context c_mlk_machine_model
14+
begin
15+
16+
micro_c_file addr: 'addr gv: "8 word list" manifest: "generated/manifests/poly.functions.manifest" "generated/c/poly.pre.c"
17+
18+
end
19+
(*>*)
20+
21+
22+
end

‎proofs/isabelle/MLKEM_Verify_Definitions.thy‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
theory MLKEM_Verify_Definitions
2+
imports
3+
MLKEM_Machine_Model
4+
begin
5+
6+
text \<open>
7+
Auto-generated by @{file "pipeline/generate.py"} from preprocessed C.
8+
Source unit: @{file "../../mlkem/src/verify.c"}
9+
Preprocessed unit: @{file "generated/c/verify.pre.c"}
10+
\<close>
11+
12+
micro_c_file "generated/c/verify.pre.c"
13+
14+
15+
16+
end

0 commit comments

Comments
 (0)