Commits on Nov 5, 2024

1. Make symbolic simulation for equiv checking infer output of loads …

   This patch updates symbolic simulation tactics for equivalence checking
   to infer the output of loads from assumptions if there is no directly
   matching equality.
   
   For example, if there is an assumption `read (memory :> bytes (ptr,8*n)) = a`
   but nothing about `read (memory :> bytes64 (word_add (ptr,8*k)))`, it
   tries to construct its output as `bigdigit a k` using `SIMPLE_ARITH_TAC`.
   This helps remove boilerplate codes in proofs that manually construct
   all equalities between 64-bit and 128-bit memory reads at known
   locations.
   This also reduces the sizes of assumptions, which may affect
   positive results to proof checking times, but in fact caused slowdown to
   larger equivalence checking tactics such as p256/p384's point
   operations. For these ops, a separate flag disabling this feature is
   set.
   
   The main tactics are `MK_MEMORY_READ_EQ_BIGDIGIT_RULE` and
   `DIGITIZE_MEMORY_READS`.
   They construct equations involving the unseen memory reads and
   `bigdigit`. They are passed to `ARM_N_STEP_TAC` (the `ARM_STEP'_TAC` in the
   past; this renaming will be explained below), which are called 'auxiliary
   memory read equations, and they are either `ASSUME_TAC`ed or passed to
   the caller separately from other normal equations describing the actual
   outputs of a simulated instruction.
   
   On top of these updates, I also
   
   - Renamed the tactics that are related to equivalence checking so that
     it does not have a punctuation mark but instead `_N` as a
     differentiating string from its original version. For example, the
     equivlaence checking version of `ARM_STEP_TAC` was `ARM_STEP'_TAC`,
     but now it is `ARM_N_STEP_TAC`. `_N` came from `ensures_n`. Some
     tactics are exception from this pattern, however.
   - Added `approximate_input_output_regs` which gets the input and output register
     from a basic block. Input registers are registers that are read
     without written, and output registers are those written but not read
     later. This does not consider memory reads and writes. This will be used in my future patches.
   - Extended `ENSURES2_WHILE_PAUP_TAC` so that its step counter needed to
     simulate the backedge is not just '1', but parameterically given in
     general.
   - And many other minor changes and updates..!

   

   aqjune-aws committed Nov 5, 2024
   Configuration menu

   • View commit details
   • Copy full SHA for 383ef0c
   • Browse repository at this point

   Copy the full SHA

   383ef0c View commit details

   Browse the repository at this point in the history

2. Try to use older HOL Light to avoid timeouts

   

   aqjune-aws committed Nov 5, 2024
   Configuration menu

   • View commit details
   • Copy full SHA for 5e275eb
   • Browse repository at this point

   Copy the full SHA

   5e275eb View commit details

   Browse the repository at this point in the history