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 multi_negate_triple

Require Import ssreflect ssrbool.
Require Import Arith_ext ZArith_ext Lists_ext.
Require Import nodup.
Require Import machine_int multi_int.
Import MachineInt.
Require Import mips_bipl mips_seplog mips_contrib mips_tactics.
Import expr_m.
Import assert_m.

Require Import multi_negate_prg.

Local Open Scope mips_expr_scope.
Local Open Scope mips_assert_scope.
Local Open Scope mips_hoare_scope.
Local Open Scope nodup_scope.

Lemma negate_triple : forall a a0 slen ptr A', nodup(a, a0, r0) ->
  {{ var_e a |--> slen :: ptr :: nil ** int_e ptr |--> A' }}
  negate a a0
  {{ var_e a |--> cplt2 slen :: ptr :: nil ** int_e ptr |--> A' }}.
Proof.
move=> a a0 slen ptr A' Hregs; rewrite /negate.

lw a0 zero16 a

apply hoare_lw_back_alt'' with (fun s h =>
  (var_e a |--> slen :: ptr :: nil ** int_e ptr |--> A') s h /\
  [a0]_s = slen)%mips_expr%mips_assert.

rewrite /while.entails => s h Hmem.
exists slen; split.
- rewrite /= !assert_m.con_assoc_equiv in Hmem.
  case: Hmem => h1 [h2 [h1_d_h2 [h1_U_h2 [Hh1 Hh2]]]].
  Compose_sepcon h1 h2; last by done.
  move: Hh1; apply assert_m.mapsto_ext => //=.
  by rewrite sext_0 add_0.
- rewrite /mips_contrib.update_store_lw.
  repeat reg_upd.
  repeat (split=> //).
  move: Hmem; apply assert_m.monotony => //= h'.
  apply assert_m.monotony => // h''.
  apply assert_m.mapsto_ext => //=; by reg_upd.
  apply assert_m.monotony => // h'''; last by reg_upd.
  apply assert_m.mapsto_ext => //=; by reg_upd.
  by apply assert_m.mapstos_ext.

subu a0 r0 a0

apply mips_contrib.hoare_subu with (fun s h =>
  (var_e a |--> slen :: ptr :: nil ** int_e ptr |--> A') s h /\ [a0 ]_ s = cplt2 slen).

rewrite /while.entails => s h [Hmem Ha0].
rewrite /mips_seplog.wp_subu.
repeat reg_upd.
repeat (split=> //).
move: Hmem. apply assert_m.monotony => // h'.
apply assert_m.monotony => // h''.
apply assert_m.mapsto_ext=> //=; by reg_upd.
apply assert_m.monotony => //= h'''; last by reg_upd.
apply assert_m.mapsto_ext => //=; by reg_upd.
by apply assert_m.mapstos_ext.
by rewrite add_com add_0 Ha0.

sw a0 zero16 a

apply mips_contrib.hoare_sw_back'.

rewrite /while.entails => s h [Hmem Ha0].
exists (int_e slen).
rewrite /= in Hmem.
rewrite !assert_m.con_assoc_equiv in Hmem.
case: Hmem => h1 [h2 [h1_d_h2 [h1_U_h2 [Hh1 Hh2]]]].
Compose_sepcon h1 h2.
move: Hh1; apply assert_m.mapsto_ext => //=.
by rewrite sext_0 add_0.

rewrite /assert_m.imp.
move=> h' [h2_d_h' Hh'] h'' Hh''.
rewrite /=.
rewrite !assert_m.con_assoc_equiv.
Compose_sepcon h' h2; last by exact Hh2.
move: Hh'; apply mapsto_ext.
by rewrite /= sext_0 add_0.
by rewrite /= Ha0.
Qed.