Prove the RISCV implementation of the compiler

[clebreto]

• [x] Create the skeleton for proofs (prove with Admitted).
• [x] Divide and plan the parallelization of Lemma to prove ( 1 file per person), do not forget to indicate whether the proofs are duplicates of ARM proofs
• [x] Prove the Lemma

[clebreto]

Will be solved by #781 .