From 83ce316944156a7f283e1204d8aa756399172ac1 Mon Sep 17 00:00:00 2001 From: Lasse Letager Hansen Date: Mon, 18 Mar 2024 20:26:31 +0100 Subject: [PATCH] Working example --- .../backends/coq/ssprove/ssprove_backend.ml | 1 + proof-libs/coq/ssprove/src/ChoiceEquality.v | 22 ++++++++++--------- proof-libs/coq/ssprove/src/Hacspec_Lib_Ltac.v | 2 -- .../proofs/ssprove/extraction/Enum_repr.v | 19 +--------------- 4 files changed, 14 insertions(+), 30 deletions(-) diff --git a/engine/backends/coq/ssprove/ssprove_backend.ml b/engine/backends/coq/ssprove/ssprove_backend.ml index 7d60082b8..7edcd5502 100644 --- a/engine/backends/coq/ssprove/ssprove_backend.ml +++ b/engine/backends/coq/ssprove/ssprove_backend.ml @@ -2378,6 +2378,7 @@ let hardcoded_coq_headers = Open Scope list_scope.\n\ Open Scope Z_scope.\n\ Open Scope bool_scope.\n\n\ + From Crypt Require Import jasmin_word.\n\n\ From Hacspec Require Import ChoiceEquality.\n\ From Hacspec Require Import LocationUtility.\n\ From Hacspec Require Import Hacspec_Lib_Comparable.\n\ diff --git a/proof-libs/coq/ssprove/src/ChoiceEquality.v b/proof-libs/coq/ssprove/src/ChoiceEquality.v index a702d8fef..a1c218b0a 100644 --- a/proof-libs/coq/ssprove/src/ChoiceEquality.v +++ b/proof-libs/coq/ssprove/src/ChoiceEquality.v @@ -204,16 +204,18 @@ Ltac normalize_fset := Ltac solve_match := try set (fset _) ; - (lazymatch (* match *) goal with - | |- context [ fsubset ?a (?a :|: _) ] => apply fsubsetUl - | |- context [ fsubset ?a (_ :|: ?a) ] => apply fsubsetUr - | |- context [ fsubset fset0 _ ] => apply fsub0set - | |- context [ fsubset ?a ?a ] => apply fsubsetxx - (* | |- context [ fsubset ?a (?b :|: _) ] => assert (a = b) by reflexivity ; apply fsubsetUl *) - (* | |- context [ fsubset ?a (_ :|: ?b) ] => assert (a = b) by reflexivity ; apply fsubsetUr *) - (* | |- context [ fsubset ?a _ ] => assert (a = fset0) by reflexivity ; apply fsub0set *) - (* | |- context [fsubset ?a ?b ] => assert (a = b) by reflexivity ; apply fsubsetxx *) - end). + (apply fsub0set + || apply fsubsetxx + || (lazymatch (* match *) goal with + | |- context [ fsubset ?a (?a :|: _) ] => apply fsubsetUl + | |- context [ fsubset ?a (_ :|: ?a) ] => apply fsubsetUr + | |- context [ fsubset fset0 _ ] => apply fsub0set + | |- context [ fsubset ?a ?a ] => apply fsubsetxx + (* | |- context [ fsubset ?a (?b :|: _) ] => assert (a = b) by reflexivity ; apply fsubsetUl *) + (* | |- context [ fsubset ?a (_ :|: ?b) ] => assert (a = b) by reflexivity ; apply fsubsetUr *) + (* | |- context [ fsubset ?a _ ] => assert (a = fset0) by reflexivity ; apply fsub0set *) + (* | |- context [fsubset ?a ?b ] => assert (a = b) by reflexivity ; apply fsubsetxx *) + end)). Ltac split_fsubset_lhs := repeat (rewrite !is_true_split_and || rewrite !fsubUset) ; diff --git a/proof-libs/coq/ssprove/src/Hacspec_Lib_Ltac.v b/proof-libs/coq/ssprove/src/Hacspec_Lib_Ltac.v index f9dbeeba5..0e05a9d1f 100644 --- a/proof-libs/coq/ssprove/src/Hacspec_Lib_Ltac.v +++ b/proof-libs/coq/ssprove/src/Hacspec_Lib_Ltac.v @@ -254,8 +254,6 @@ Ltac solve_ssprove_obligations := || fset_equality (* TODO: add match goal *) || solve_in_fset (* TODO: add match goal *) || ssprove_valid'_2 - || now apply fsubsetUl - || now apply fsubsetUr || (Tactics.program_simpl; fail))). Ltac solve_fsubset_trans := diff --git a/tests/enum-repr/proofs/ssprove/extraction/Enum_repr.v b/tests/enum-repr/proofs/ssprove/extraction/Enum_repr.v index c53f955ee..851780036 100644 --- a/tests/enum-repr/proofs/ssprove/extraction/Enum_repr.v +++ b/tests/enum-repr/proofs/ssprove/extraction/Enum_repr.v @@ -57,22 +57,8 @@ Equations EnumWithRepr_ImplicitDiscrEmptyStruct {L : {fset Location}} {I : Inter solve_lift (ret_both (inr (tt : 'unit) : t_EnumWithRepr)) : both L I t_EnumWithRepr. Fail Next Obligation. -Ltac solve_ssprove_obligations := - repeat ( - intros ; autounfold ; normalize_fset ; - now (solve_match || now (apply fsubsetxx || apply fsub0set) - || solve_in_mem (* TODO: add match goal *) - || fset_equality (* TODO: add match goal *) - || solve_in_fset (* TODO: add match goal *) - || ssprove_valid'_2 - || now apply fsubsetUl - || now apply fsubsetUr - || (Tactics.program_simpl; fail))). - -Obligation Tactic := (* try timeout 8 *) solve_ssprove_obligations. - Equations t_EnumWithRepr_cast_to_repr {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 t_EnumWithRepr) : both L1 I1 int16 := - t_EnumWithRepr_cast_to_repr x := + t_EnumWithRepr_cast_to_repr x := matchb x with | EnumWithRepr_ExplicitDiscr1_case => solve_lift discriminant_EnumWithRepr_ExplicitDiscr1 @@ -85,13 +71,10 @@ Equations t_EnumWithRepr_cast_to_repr {L1 : {fset Location}} {I1 : Interface} (x end : both L1 I1 int16. Fail Next Obligation. -(*Not implemented yet? todo(item)*) - Equations f {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 int32 := f _ := letb v__x := cast_int (WS2 := U32) (discriminant_EnumWithRepr_ExplicitDiscr2 .+ (ret_both (0 : int16))) in solve_lift ((cast_int (WS2 := U32) (t_EnumWithRepr_cast_to_repr EnumWithRepr_ImplicitDiscrEmptyTuple)) .+ (cast_int (WS2 := U32) (t_EnumWithRepr_cast_to_repr EnumWithRepr_ImplicitDiscrEmptyStruct))) : both L1 I1 int32. -Next Obligation. Fail Next Obligation. Equations ff__CONST {L : {fset Location}} {I : Interface} : both L I int16 :=