Verified SAR-BP: A verified C implementation of SAR backprojection
with a certified absolute error bound.

Version 1.0 (2015-12-04)

Copyright (C) 2015 Reservoir Labs Inc.
All rights reserved.

This library and all of its files are distributed under the GNU
General Public License, version 3.0, or (at your option) any later
version. See LICENSE for more legal information on use and
distribution of Verified SAR-BP.


Verified SAR-BP is based on Section 5 of its authors' paper published
at CPP 2016 (5th ACM/SIGPLAN international conference on Certified
Programs and Proofs):

Tahina Ramananandro, Paul Mountcastle, Benoit Meister and Richard
Lethin
A Unified Coq Framework for Verifying C Programs with Floating-Point
Computations

However, the C implementation of SAR backprojection certified in
Verified SAR-BP, which can be found in sar/backprojection.c, is only
based on sin, cos and sqrt all assumed to be correctly rounded in
double-precision floating-point numbers, and does not use any of the
patent-pending and/or otherwise patent-protected approximations of
square root, norm and sine described in Sections 5.1 and 5.3 of the
abovementioned CPP 2016 paper.


Summary of directories:

  sar (corresponding to logical path sar): SAR backprojection, C
  implementation and proof

  sar_sizes: bounds on SAR image and input data. This directory is not
  in the building path; instead, relevant files are copied from there
  to sar at the ./configure step (see below).


Most interesting files:

  sar/SARBackProj.v: mathematical specification of SAR backprojection
  in real numbers

  sar/backprojection.c: C implementation (see the comment above about
  its relationship with the authors' CPP 2016 paper)

  sar/SARBackProjSource.v: the Clight abstract syntax tree that was
  obtained from sar/backprojection.c through CompCert Clightgen.

  sar/SARBackProjSourceSpec.v: the hypotheses and correctness
  statement

  sar/Main.v: main theorem about SAR backprojection.


Verified SAR-BP requires Coq 8.5beta2, Reservoir Labs Inc. R-CoqLib
version 1.0, and Reservoir Labs Inc. VCFloat, version 1.0, which are
assumed to be already installed on your system.
R-CoqLib and VCFloat can be retrieved from Reservoir's GitHub at
https://github.com/reservoirlabs

See ACKS for copyright information about those external libraries, as
well as copyright and licensing information about the prior works from
which Verified SAR-BP is derived.


Usage: assuming that you already have a standard installation of Coq
8.5beta2, VCFloat 1.0, GNU make.

  1. Choose an image size, by:

     ./configure --image-size <imagesize> --vcfloat <path>

     where <imagesize> is one of: small  medium  large

     and <path> is the absolute path to VCFloat's root directory (NOT
     its vcfloat/ subdirectory!)

  2. Build, by:

     make

  Then, the theorem statement about the correctness of the C
  implementation of SAR backprojection included in
  sar/backprojection.c, along with the error bound and the list of
  axioms, should display on screen, corresponding to the "Norm:
  Double; Interpol.: Single; Sine/cosine: Double then Single; Final
  sum: Double then Single" (2nd line of data) of the table in Figure
  12 of the abovementioned CPP 2016 paper.

  After building, you do not need to move the files anywhere else
  (and, by the way, `make install' does not work). The build system
  automatically generates a ./run-coqide.sh script to edit the sources
  with CoqIDE (if installed on your system), as well as local load
  path configuration files for Emacs+ProofGeneral (if installed on
  your system). If you want to compile code against Verified SAR-BP,
  you can have a look at the autogenerated `coqopts' file, to grab the
  load path options to pass to Coq and its relevant tools (coqc,
  coq_makefile, etc.)