NB: This Coq documentation contains a revised version of the Coq implementation of these papers [1], [2], [3], [4], and is also the support for ongoing research. A partial archive (14/01/2001) is available at here. Drop us a line if you are interested in a complete, up-to-date archive.

Library POLAR_library_functions

Require Import ssreflect ssrbool eqtype.
Require Import Bool_ext ZArith_ext Lists_ext String_ext.
Require Import machine_int.
Import MachineInt.
Require Import C_types C_expr C_bipl C_cmd C_seplog.

Local Open Scope minC_expr_scope.
Local Open Scope minC_cmd_scope.

Module PolarSSL.

Axiom ssl_fetch_input : var -> var -> exp -> @while.cmd cmd0 bexp.

Axiom memcpy : var -> exp -> exp -> exp -> @while.cmd cmd0 bexp.
Axiom memset : var -> exp -> exp -> exp -> @while.cmd cmd0 bexp.

Axiom md5_update : exp -> exp -> exp -> @while.cmd cmd0 bexp.
Axiom sha1_update : exp -> exp -> exp -> @while.cmd cmd0 bexp.

End PolarSSL.