commit 6a05fa545dcb3c29201ec53ab2c741c049446534
author Jade Philipoom <jadep@google.com> Thu May 19 16:42:46 2022 +0100
committer Alphan Ulusoy <alphan@google.com> Mon May 23 09:54:54 2022 -0400
tree a5968e4bc6ba16ef5b16589abb3eae0f06294fbe
parent cd78b23c9595977b14152487586784a10c76a176

Update veri-titan to secure-foundations/veri-titan@a5b18fa

Update code from upstream repository https://github.com/secure-
foundations/veri-titan.git to revision
a5b18fa0bea5d943c9267d3561cbd2704764a868

* Make a separate procedure for throwing deliberate errors. (Jade
  Philipoom)
* Make the loop iteration counter count write_to_dmem loops in
  addition to modexp (Jade Philipoom)
* Add loop iteration counter for fault injection hardening. (Jade
  Philipoom)
* Add comments to generated OTBN modexp (Jade Philipoom)
* Add back auto-generated files with a new .gitignore pattern (Jade
  Philipoom)
* Make Z3 target more platform-independent (Bryan Parno)
* progress on the polymul (yizhou7)
* poly mul and poly scale (yizhou7)
* rv bit rev (yizhou7)
* somewhat messy but almost done with bit_rev in riscv (yizhou7)
* removed assumes in bit rev proofs (yizhou7)
* removed one assume (yizhou7)
* bit rev model somewhat working (yizhou7)
* some progress (yizhou7)
* add b as part of the datatype (yizhou7)
* some progress (yizhou7)
* bit rev shuffle proof more complicated than expected (yizhou7)
* inverse ntt (yizhou7)
* rename invs to avoid conflicts (yizhou7)
* directory reorg (yizhou7)
* updated the riscv impl (yizhou7)
* remove large amount of duplications in ntt and intt (yizhou7)
* intt dafny model and proof (yizhou7)
* Update names of OTBN build scripts (Jade Philipoom)
* rename inner mq sub add (yizhou7)
* use mq_add mq_sub with fixed regs (yizhou7)
* forward ntt seems to work (yizhou7)
* add post lemma for t_inv (yizhou7)
* fixed unsound requires (yizhou7)
* inner most loop seems done (yizhou7)
* annoying bound proofs (yizhou7)
* wip on s_loop (yizhou7)
* wip for s_loop (yizhou7)
* update dafny impl (yizhou7)
* wip (yizhou7)
* reorg innt model (yizhou7)
* fix up the rsa code (yizhou7)
* worked around werid dafny asbtract module bug (yizhou7)
* add support for b16 iter wirte (yizhou7)
* add some support for b16_iter (yizhou7)
* Update README.md to include Singular requirement (Sydney Gibson)
* Add subm ins to OTBN and clean up files (Sydney Gibson)
* Fix mq_add to not use hardcoded modulus (Sydney Gibson)
* mq_add done with assumed Q=12289 in wmod (Sydney Gibson)
* remove assume about Q - x_e (yizhou7)
* addm fully implemented plus correctness lemma (Sydney Gibson)
* Get otbn mq_arith test-ready (Sydney Gibson)
* intt (with maybe one assume) (yizhou7)
* revamp forward ntt so that things are pretty much all parameterized
  (yizhou7)
* structurally very similar invs for innt (yizhou7)
* include the command ran (yizhou7)
* some basic comparsion (yizhou7)
* remove the need to pass in psi (yizhou7)
* much cleaner python references (yizhou7)
* Add otbn addm instruction (Sydney Gibson)
* our alternative version seems to work (yizhou7)
* mostly got the alternative version working (yizhou7)
* update the dafny impl to use the table (yizhou7)
* separate table (yizhou7)
* update mulntt_ct to use montmul and adjusted twiddle factors
  (yizhou7)
* update python script to use twiddle factors in montgomery form
  (yizhou7)
* cleanup python scripts (yizhou7)
* prove mq_rshift1 procedure and lemma (Sydney Gibson)
* test out intt using the same ct code (yizhou7)
* removed most assumes (yizhou7)
* removed assume in x_value_odd_square_lemma (yizhou7)
* remove assume in x_value_even_square_lemma (yizhou7)
* reorg bit_rev_int (yizhou7)
* removed some assumes (yizhou7)
* a version with many assumes (yizhou7)
* done proving j_loop_inv_pre_lemma/j_loop_inv_post_lemma (yizhou7)
* next_t_loop_view (yizhou7)
* proved build_higher_inverse_lemma (yizhou7)
* s_loop_inv pre/post lemma (yizhou7)
* stronger s_loop_perserves_lower_inv_lemma (yizhou7)
* s_loop_perserves_inv_lemma (yizhou7)
* proved s_loop_perserves_higher_inv_lemma (yizhou7)
* proved the core butterfly ops (with some assumes) (yizhou7)
* replaced assume about x_square (yizhou7)
* remove two assumes about bitrev (yizhou7)
* proved lower_points_view_value_lemma (yizhou7)
* points_view_index_lemmas (yizhou7)
* cleanups on level_polys & level_points_view (yizhou7)
* even more completed invs (yizhou7)
* start porting invs to dafny (yizhou7)
* more complete invs (yizhou7)
* some progress on the polysplit (yizhou7)
* starting the dafny loop version (yizhou7)
* some more inv figured out (yizhou7)
* got some inv figured out (yizhou7)
* inv guess seems to hold for the last level at least (yizhou7)
* testing out invs on python code (yizhou7)
* redo nth root lemma (yizhou7)
* sanity checking python (yizhou7)
* progress on mq_rshift1 proof (Sydney Gibson)
* add neg instruction to risc-v model (Sydney Gibson)
* add mq_sub and proof (Sydney Gibson)
* mq_add proof without assert false (Sydney Gibson)
* Working proof for mq_add (Sydney Gibson)
* remove assume in ntt_rec (yizhou7)
* remove assumes in ntt (yizhou7)
* import fix (yizhou7)
* file renames (yizhou7)
* a cleaner version of ntt_rec (yizhou7)
* uncomment post condition (yizhou7)
* remove one assume (yizhou7)
* fix error in ntt_rec (yizhou7)
* almost done with loop version (yizhou7)
* almost getting ntt working (yizhou7)
* first version of ntt_chunk_loop (yizhou7)
* ntt_chunk_loop seems to work (yizhou7)
* making progress on proving ntt_chunk_loop_inv (yizhou7)
* remove additional even/odd args (yizhou7)
* proved that ntt_level_implies_chunk_inv (yizhou7)
* restructure indicies computations (yizhou7)
* seems to have worked around the timeout issue (yizhou7)
* encounter timeout in loop ntt (yizhou7)
* cleaner version of ntt_rec3 (yizhou7)
* Partial progress on mq_add proof (Sydney Gibson)
* add chunk view functions (yizhou7)
* use ntt_rec3 as a reference (yizhou7)
* reduce the number of arguments passed around (yizhou7)
* ntt_rec2_chunk_rec seems to work (yizhou7)
* getting close to a level recursive version (yizhou7)
* convert ntt_rec2 into using ghost a (yizhou7)
* better post conditions for ntt_indicies_inv_consequence (yizhou7)
* incoperate indicies into rec2 (yizhou7)
* incoperate ntt_indicies_inv_consequence into ntt_rec2 (yizhou7)
* Clean up helpers (Bryan Parno)
* Helper goes through, modulo a few small helpers (Bryan Parno)
* a functional and recursive ntt_rec (yizhou7)
* add level chunk functions (yizhou7)
* Progress on the base case. (Bryan Parno)
* Induction step goes through for poly_eval_split_helper (Bryan Parno)
* More progress (Bryan Parno)
* ntt_chunk_base_case (yizhou7)
* rename chunk index into ki to better match the loop version
  (yizhou7)
* Experiment (Bryan Parno)
* fix up errors in pow2 (yizhou7)
* remove indicies in ntt_rec (yizhou7)
* ntt_indicies_inv_consequence seems done (yizhou7)
* Progress on poly_eval_split_lemma_helper (Bryan Parno)
* odd_indexed_indices_reorder symmetric (yizhou7)
* fix up index.py after Pow2 removal (yizhou7)
* a stronger inv for the bit reverse (yizhou7)
* Restore ntt_cancellation_lemma proof (Bryan Parno)
* Tediously prove nth_root_lemma() (Bryan Parno)
* making some progress on even index sorting (yizhou7)
* making some progress on bit rev (yizhou7)
* split files (yizhou7)
* at leat prove that the indicies are in bound (yizhou7)
* leave poly_eval_split_lemma as axiom (yizhou7)
* cleanup the odd even defs (yizhou7)
* make ntt_base_case assumption more explicit (yizhou7)
* cleanup the axioms a bit (yizhou7)
* Some proofs for the axioms (Bryan Parno)
* oops more typos (yizhou7)
* fix the N constant error (yizhou7)
* remove some assumes (yizhou7)
* naive forward ntt (yizhou7)
* some progress on y_k_value (yizhou7)
* ntt_base_case (yizhou7)
* start of naive ntt (yizhou7)
* Add stand-alone falcon sigverify routine + riscv asm (Sydney Gibson)
* mod_exp seems done (yizhou7)
* progress on mp post (yizhou7)
* more progress on mod_exp (yizhou7)
* progress on mp_loop (yizhou7)
* forgot to add vad file (yizhou7)
* mont_mul seems done (yizhou7)
* mont_mul_add seems done (yizhou7)
* progress on mma_post (yizhou7)
* mma inner loop (yizhou7)
* main mma_loop body seems done (yizhou7)
* progress on the main loop body (yizhou7)
* example usage of stack frame var in mma_pre (yizhou7)
* partial progress on mma (yizhou7)
* make stack push more opaque (yizhou7)
* update sub_mod to load symbolic n (yizhou7)
* update source to use n and d0inv as externs (yizhou7)
* add load symbol (yizhou7)
* mark consts_inv as opaque (yizhou7)
* add contants for heap (yizhou7)
* sub_mod seems to be okay (yizhou7)
* bug fix in subc (order of args wrong) (yizhou7)
* use modfies anyways (yizhou7)
* bug fix on state equal (yizhou7)
* use frame false for mula and mulaa (yizhou7)
* mul example (yizhou7)
* fix typo in mul name (yizhou7)
* moved examples (yizhou7)
* most of the instructions (yizhou7)
* add semantics for popm_w (yizhou7)
* reduce the number of post conditions in sw_stack (yizhou7)
* sw/lw with iters (yizhou7)
* add flags to msp state (yizhou7)
* add 16 bits based source file for msp modexp (yizhou7)
* add pushm_w semantics (yizhou7)
* add vale.i.dfy for msp (yizhou7)
* move reference (yizhou7)
* add starting defs for msp430 (yizhou7)
* add source for msp430 (yizhou7)
* cleanup build, mark stack_init as extern (yizhou7)
* fix up otbn ptr issue (yizhou7)
* add lw_prev (yizhou7)
* mostly fixed up mp (yizhou7)
* mm seems to work (yizhou7)
* revamped mma (yizhou7)
* mma seems to work (yizhou7)
* basic use case of save registers in mma (yizhou7)
* mostly fixed up the decls in rv (yizhou7)
* Update dependencies to include those needed for Vale, check those
  dependencies, and link to Vale install instructions (Jade Philipoom)
* update riscv vale.i.dfy (yizhou7)
* cleanup some duplicated defs (yizhou7)
* patch up a version using generated memory models (yizhou7)
* rename some files (yizhou7)
* template files (yizhou7)
* mem_t imem_t refinement (yizhou7)
* slightly change the inv proof interface (yizhou7)
* verify manual written files (yizhou7)
* most part of write_preserves_inv (yizhou7)
* stack model with frames (yizhou7)
* an untemplated version (yizhou7)
* 2/3 equiv invs (yizhou7)
* attempting to prove stack inv (yizhou7)
* commit a hand written version for stack modeling first (yizhou7)
* small write preserves inv (yizhou7)
* mostly done with 2 width (yizhou7)
* fix some typos (yizhou7)
* use of jinja macro (yizhou7)
* move script dir (yizhou7)
* remove rr lemma that is no longer needed (yizhou7)
* update build system (yizhou7)
* bug fix in montmul_inv_lemma (yizhou7)
* update mul256_correct_lemma (yizhou7)
* mostly done with simplification using gbassert (yizhou7)
* converted most gbasserts (yizhou7)
* remove unused and redundant code (Sydney Gibson)
* update the mont_loop_divisible_lemma proof to use gbassert (yizhou7)
* use a mod version of dafny (yizhou7)
* emit comment in modexp_printer (yizhou7)
* Finish NOP test suite and new printer config (Sydney Gibson)
* Add test cases for empty constructs and function calls (Sydney
  Gibson)
* Fix IfElse test cases(?) (Sydney Gibson)
* Working test set up + a few working NOP tests (Sydney Gibson)
* An alternate approach to overlap detection (Bryan Parno)
* simplify for testing purposes, fix printer call (Sydney Gibson)
* Another attempt at nop detection (Sydney Gibson)
* update the build slightly, add riscv printer output (yizhou7)
* Working nop checker (Sydney Gibson)
* update the dafny lib hash (yizhou7)
* add nop eval (Sydney Gibson)
* Get rid of warnings in make file (Sydney Gibson)
* remove duplicated files (yizhou7)
* seem be have located and fixed the printer branch bug (yizhou7)
* fix the skipping in ifelse (yizhou7)
* Add runnable riscv-rsa test assembly + harness (Sydney Gibson)
* Start NOP removal (Sydney Gibson)
* update printer (yizhou7)
* remove constants addresses from riscv impl (yizhou7)
* separate mod_pow and main (yizhou7)

Signed-off-by: Jade Philipoom <jadep@google.com>