31/08/06: seplog for MIPS milestone (ASIAN 2006)

NB: See this page ("cryptoasm" tab) for an updated version.

The whole archive: asian2006.tar.gz

Contents overview:

• From previous work:
  • Various general lemmas and tactics: util.v, util_tactic.v
  • Definition of heaps: heap.v, heap_tactics.v
• Machine integers:
  • Operations on lists of bits: listbit.v
  • Correctness of operations on lists of bits: listbit_correct.v
  • Machine integers: machine_int.v
• Axiomatic semantics:
  • Definition of states: state.v
  • Operational and axiomatic semantics of structured MIPS programs: mips.v
  • Derived Hoare triples: mips_contrib.v
• Custom tactics: mips_tactics.v
• A library for arrays: mapstos.v
• Operational for unstructured MIPS programs and certified translator from structure MIPS programs: mips0.v
• Application to verification of multi-precision arithmetic functions:
  • A library for multi-precision integers: sum.v, ssum.v
  • Multi-precision addition: multiadd.v
  • Multi-precision subtraction: multisub.v
  • Multi-precision multiplication: multimul.v
  • Montgomery multiplication: prelude, verification (informal sketch)
  • Conversion signed/unsigned: ssum_converter.v
• Compilation scripts: build.sh, clean.sh