# Theory Round

theory Round
imports RMD_Specification

theory Round
imports RMD_Specification
begin

spark_open

abbreviation from_chain ::  where

abbreviation from_chain_pair ::  where

abbreviation to_chain ::  where

abbreviation to_chain_pair ::  where

abbreviation steps' ::  where

abbreviation round_spec ::  where

spark_proof_functions
steps = steps'
round_spec = round_spec

lemma uint_word_of_int_id:
assumes
assumes
shows
unfolding int_word_uint
using assms

lemma steps_step:
unfolding steps_def
by (induct i) simp_all

lemma from_to_id:
proof (cases CC)
fix a::RMD.chain
fix b c d e f::word32
assume
thus ?thesis by (cases a) simp
qed

lemma steps_to_steps':

unfolding from_to_id ..

lemma steps'_step:
assumes
shows

proof -
have  using assms by simp
show ?thesis
unfolding  steps_step steps_to_steps'
..
qed

lemma step_from_hyp:
assumes
step_hyp:

assumes  (is )
assumes                 and  and  and
assumes  and  and  and  and
assumes  and  and  and  and
assumes  and  and  and  and
assumes  and
assumes  and
assumes  and
shows

using step_hyp
proof -
let ?MM = 4294967296
have AL:
by (rule uint_word_of_int_id[OF  ])
have CL:
by (rule uint_word_of_int_id[OF  ])
have DL:  ..
have EL:
by (rule uint_word_of_int_id[OF  ])
have AR:
by (rule uint_word_of_int_id[OF  ])
have CR:
by (rule uint_word_of_int_id[OF  ])
have DR:  ..
have ER:
by (rule uint_word_of_int_id[OF  ])
have BL:

(is )
proof -
have  using
have  using
have  using
have  by simp
show ?thesis
unfolding
uint_word_of_int_id[OF  ]
uint_word_of_int_id[OF  ]
int_word_uint
unfolding
unfolding word_uint.Abs_norm

)
qed

have BR:

(is )
proof -
have  using
have  using
have  using
have  by simp
have nat_transfer:
using nat_diff_distrib
by simp
show ?thesis
unfolding
uint_word_of_int_id[OF  ]
uint_word_of_int_id[OF  ]
int_word_uint
nat_transfer
unfolding
unfolding word_uint.Abs_norm

)
qed

show ?thesis
unfolding steps'_step[OF ] step_hyp[symmetric]
step_both_def step_r_def step_l_def
by (simp add: AL BL CL DL EL AR BR CR DR ER)
qed

spark_vc procedure_round_61
proof -
let ?M =
have step_hyp:

unfolding steps_def
uint_word_of_int_id[OF  ]
uint_word_of_int_id[OF  ]
uint_word_of_int_id[OF  ]
uint_word_of_int_id[OF  ]
uint_word_of_int_id[OF  ])
let ?rotate_arg_l =

let ?rotate_arg_r =

note returns =

note x_borders =

from   x_borders
have  by blast
hence x_lower:  unfolding returns .

from   x_borders
have  by blast
hence x_upper:  unfolding returns .

from   x_borders
have  by blast
hence x_lower':  unfolding returns .

from   x_borders
have  by blast
hence x_upper':  unfolding returns .

have  by simp
have  by simp
note step_from_hyp [OF
step_hyp
H2 H4 H6 H8 H10 H2 H4 H6 H8 H10 ― ‹upper bounds›
H1 H3 H5 H7 H9  H1 H3 H5 H7 H9  ― ‹lower bounds›
]
from this[OF x_lower x_upper x_lower' x_upper'  ]
x_lower x_lower'
show ?thesis unfolding returns(1) returns(2) unfolding returns
by (simp del: mod_pos_pos_trivial mod_neg_neg_trivial)
qed

spark_vc procedure_round_62
proof -
let ?M =
let ?rotate_arg_l =

let ?rotate_arg_r =

have s:  by simp
note returns =

[simplified s]

note x_borders =

from   x_borders
have  by blast
hence x_lower:  unfolding returns .

from   x_borders
have  by blast
hence x_upper:  unfolding returns .

from   x_borders
have  by blast
hence x_lower':  unfolding returns .

from   x_borders
have  by blast
hence x_upper':  unfolding returns .

from  have  by simp
from  have  by simp

have  by simp

note step_from_hyp[OF H1

]
from this[OF
x_lower x_upper x_lower' x_upper'
]
x_lower x_lower'
show ?thesis unfolding
unfolding returns(1) returns(2) unfolding returns
by (simp del: mod_pos_pos_trivial mod_neg_neg_trivial)

qed

spark_vc procedure_round_76
proof -
let ?M =
let ?INIT_CHAIN =

have steps_to_steps':

unfolding from_to_id by simp
from

show ?thesis
unfolding round_def
unfolding steps_to_steps'
unfolding H1[symmetric]