Vale basic support for PowerPC architecture

This patch adds Vale support for PowerPC architecture, The patch implements 64-bit little-endian specification of PPC arch in addition to use Power ISA v.3.0 for the instruction set hence the supported processors are POWER9+.
The patch also tries to have a relative interface with x64simple implementation by using the same naming convention and common functions to make the code more maintainable.
The following features are implemented:
- General-purpose registers.
- Vector registers (with the compatibility to use in VSR-specific instructions).
- Condition Register (CR) and Fixed-Point Exception Register (XER) to update the comparison status and to handle carry and overflow occurrences.
- Validation, evaluation and update functions for registers.
- Procedure conditional statements (If, Else, While) that support register-register and register-immediate comparisons. Unlike x64, using those statements update the flags accordingly at run-time rather than havoc them to get refreshed values of Condition Register (CR).
- Basic and vector instruction support for which have use-cases.
- Print functions for the supported instructions with bare register names, GCC has -mregnames option to assemble named registers for PowerPC but it's GCC-specific option and disabled by default.
- GCC assembly printer support.
- Lemmas functions for high-level functions in addition to ensure the results of basic and vector instructions.
- Negative constant support in assembly in addition to ensure the bounds of instruction operands and memory offsets.
- Memory interface to deal with memory addresses and operands.
- Implement Copy16 function in PPC64LE.Test.Memcpy module.

fstar/code/arch/ppc64le/PPC64LE.Vale.Decls.fst

@@ -0,0 +1,79 @@
+module PPC64LE.Vale.Decls
+open PPC64LE.Machine_s
+open PPC64LE.Vale
+open PPC64LE.Vale.State
+open PPC64LE.Vale.StateLemmas
+module S = PPC64LE.Semantics_s
+module P = PPC64LE.Print_s
+
+let xer_ov = Lemmas.xer_ov
+let xer_ca = Lemmas.xer_ca
+let update_xer_ov = Lemmas.update_xer_ov
+let update_xer_ca = Lemmas.update_xer_ca
+let ins = S.ins
+type ocmp = S.ocmp
+type va_fuel = nat
+
+type va_pbool = Vale.Def.PossiblyMonad.pbool
+let va_ttrue () = Vale.Def.PossiblyMonad.ttrue
+let va_ffalse = Vale.Def.PossiblyMonad.ffalse
+let va_pbool_and x y = Vale.Def.PossiblyMonad.((&&.)) x y
+
+let mul_nat_helper x y =
+ FStar.Math.Lemmas.nat_times_nat_is_nat x y
+
+let va_fuel_default () = 0
+
+let va_lemma_upd_update sM =
+ ()
+
+let va_cmp_eq o1 o2 = S.OEq o1 o2
+let va_cmp_ne o1 o2 = S.ONe o1 o2
+let va_cmp_le o1 o2 = S.OLe o1 o2
+let va_cmp_ge o1 o2 = S.OGe o1 o2
+let va_cmp_lt o1 o2 = S.OLt o1 o2
+let va_cmp_gt o1 o2 = S.OGt o1 o2
+
+let eval_code = Lemmas.eval_code
+let eval_while_inv = Lemmas.eval_while_inv
+
+let mem_inv m = True
+let va_ins_lemma c0 s0 = ()
+
+let eval_ocmp = Lemmas.eval_ocmp
+let valid_ocmp = Lemmas.valid_ocmp
+let eval_cmp_cr0 = S.eval_cmp_cr0
+
+unfold let va_eval_ins = Lemmas.eval_ins
+
+let lemma_cmp_eq s o1 o2 = ()
+let lemma_cmp_ne s o1 o2 = ()
+let lemma_cmp_le s o1 o2 = ()
+let lemma_cmp_ge s o1 o2 = ()
+let lemma_cmp_lt s o1 o2 = ()
+let lemma_cmp_gt s o1 o2 = ()
+
+let lemma_valid_cmp_eq s o1 o2 = ()
+let lemma_valid_cmp_ne s o1 o2 = ()
+let lemma_valid_cmp_le s o1 o2 = ()
+let lemma_valid_cmp_ge s o1 o2 = ()
+let lemma_valid_cmp_lt s o1 o2 = ()
+let lemma_valid_cmp_gt s o1 o2 = ()
+
+let va_compute_merge_total = Lemmas.compute_merge_total
+let va_lemma_merge_total b0 s0 f0 sM fM sN = Lemmas.lemma_merge_total b0 s0 f0 sM fM sN; Lemmas.compute_merge_total f0 fM
+let va_lemma_empty_total = Lemmas.lemma_empty_total
+let va_lemma_ifElse_total = Lemmas.lemma_ifElse_total
+let va_lemma_ifElseTrue_total = Lemmas.lemma_ifElseTrue_total
+let va_lemma_ifElseFalse_total = Lemmas.lemma_ifElseFalse_total
+let va_lemma_while_total = Lemmas.lemma_while_total
+let va_lemma_whileTrue_total = Lemmas.lemma_whileTrue_total
+let va_lemma_whileFalse_total = Lemmas.lemma_whileFalse_total
+let va_lemma_whileMerge_total = Lemmas.lemma_whileMerge_total
+
+let printer = P.printer
+let print_string = FStar.IO.print_string
+let print_header = P.print_header
+let print_proc = P.print_proc
+let print_footer = P.print_footer
+let gcc = P.gcc