Theory Babai_Algorithm_Updated
theory Babai_Algorithm_Updated
imports
LLL_Basis_Reduction.LLL_Impl
"HOL.Archimedean_Field"
"HOL-Analysis.Inner_Product"
begin
fun calculate_c:: "rat vec ⇒ rat vec list ⇒ nat => int" where
"calculate_c s L1 n = round ((s ∙ (L1!((dim_vec s) - n))) / (sq_norm_vec (L1!((dim_vec s) - n))))"
fun update_s:: "rat vec ⇒ rat vec list ⇒ rat vec list ⇒ nat ⇒ rat vec" where
"update_s sn M Mt n = ((rat_of_int (calculate_c sn Mt n)) ⋅⇩v M!((dim_vec sn) - n)) "
fun babai_help:: "rat vec ⇒ rat vec list ⇒ rat vec list ⇒ nat ⇒ rat vec" where
"babai_help s M Mt 0 = s" |
"babai_help s M Mt (Suc n) = (let B = (babai_help s M Mt n) in B - (update_s B M Mt (Suc n)))"
text ‹This assumes an LLL-reduced input and outputs a short vector of the form $v+t$, with $v \in L$ ›
fun babai_of_LLL :: "rat vec ⇒ rat vec list ⇒ rat vec" where
"babai_of_LLL s M = babai_help s M (gram_schmidt (dim_vec s) M) (dim_vec s)"
text ‹This begins with a non-reduced basis and outputs a vector $v$ in $L$ which is close to $t$›
fun full_babai :: "int vec list ⇒ rat vec ⇒ rat ⇒ int vec"
where "full_babai fs target α =
map_vec int_of_rat
(babai_of_LLL
(uminus target)
(LLL.RAT (LLL_Impl.reduce_basis α fs))
+ target)"
end