text:
(** File generated by coq-of-ocaml *)
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Src.List.
Require Src.Option.

Module Graph.
  Definition edge (v : Set) : Set := v * v.

  Module t.
    Record record {v : Set} : Set := Build {
      vertices : list v;
      edges : list (edge v) }.
    Arguments record : clear implicits.
    Definition with_vertices {t_v} vertices (r : record t_v) :=
      Build t_v vertices r.(edges).
    Definition with_edges {t_v} edges (r : record t_v) :=
      Build t_v r.(vertices) edges.
  End t.
  Definition t := t.record.
End Graph.

Module Color.
  Inductive t : Set :=
  | R : t
  | G : t
  | B : t.

  Definition coloring : Set := list t.
End Color.

Module CNF.
  Inductive var (v : Set) : Set :=
  | Var : v -> Color.t -> var v.

  Arguments Var {_}.

  Inductive literal (v : Set) : Set :=
  | Lit : var v -> literal v
  | NLit : var v -> literal v.

  Arguments Lit {_}.
  Arguments NLit {_}.

  Definition clause (v : Set) : Set := list (literal v).

  Definition t (v : Set) : Set := list (clause v).

  Definition solution (v : Set) : Set := list (literal v).

  Definition solver (v : Set) : Set :=
    (v -> v -> bool) -> t v -> option (solution v).

  Definition lit {A : Set} (v_value : A) (c_value : Color.t) : literal A :=
    Lit (Var v_value c_value).

  Definition nlit {A : Set} (v_value : A) (c_value : Color.t) : literal A :=
    NLit (Var v_value c_value).
End CNF.

Definition vertex_has_color {v : Set} (g_value : Graph.t v) : CNF.t v :=
  let f_value {B : Set} (v_value : B) : list (CNF.literal B) :=
    let lit (c_value : Color.t) : CNF.literal B :=
      CNF.Lit (CNF.Var v_value c_value) in
    [ lit Color.R; lit Color.G; lit Color.B ] in
  List.map f_value g_value.(Graph.t.vertices).

Definition vertices_color_uniqueness {v : Set} (g_value : Graph.t v)
  : CNF.t v :=
  let f_value (v_value : v) : list (list (CNF.literal v)) :=
    let diff_cols (c1 : Color.t) (c2 : Color.t) : list (CNF.literal v) :=
      [ CNF.nlit v_value c1; CNF.nlit v_value c2 ] in
    [
      diff_cols Color.R Color.B;
      diff_cols Color.B Color.G;
      diff_cols Color.R Color.G
    ] in
  List.flatten (List.map f_value g_value.(Graph.t.vertices)).

Definition adj_vertices_have_diff_colors {v : Set} (g_value : Graph.t v)
  : CNF.t v :=
  let f_value (function_parameter : Graph.edge v)
    : list (list (CNF.literal v)) :=
    let '(u_value, v_value) := function_parameter in
    let diff_cols (c1 : Color.t) (c2 : Color.t) : list (CNF.literal v) :=
      [ CNF.nlit u_value c1; CNF.nlit v_value c2 ] in
    [
      diff_cols Color.R Color.G;
      diff_cols Color.B Color.G;
      diff_cols Color.R Color.B
    ] in
  List.flatten (List.map f_value g_value.(Graph.t.edges)).

Definition op_at {A : Set} : list A -> list A -> list A := List.append.

Definition generate_cnf {v : Set} (g_value : Graph.t v) : CNF.t v :=
  op_at (op_at (vertex_has_color g_value) (vertices_color_uniqueness g_value))
    (adj_vertices_have_diff_colors g_value).

Module List.
  Include List.

  Definition map_opt {a b : Set} (f_value : a -> option b) (l_value : list a)
    : option (list b) :=
    let h_value (e_value : a) (xs : list b) : Option.t (list b) :=
      Option.map (fun (x_value : b) => cons_value x_value xs) (f_value e_value)
      in
    let g_value (r_value : Option.t (list b)) (e_value : a)
      : Option.t (list b) :=
      Option.bind r_value (h_value e_value) in
    List.fold_left g_value (Some nil) l_value.
End List.

Definition recover_answer {v : Set}
  (equal : v -> v -> bool) (g_value : Graph.t v) (sol : option (CNF.solution v))
  : option Color.coloring :=
  let get_coloring (sol : CNF.solution v) : option (list Color.t) :=
    let f_value (v_value : v) : option Color.t :=
      let true_var (function_parameter : CNF.literal v) : option Color.t :=
        match function_parameter with
        | CNF.Lit (CNF.Var v' c_value) =>
          if equal v_value v' then
            Some c_value
          else
            None
        | _ => None
        end in
      List.find_map true_var sol in
    let map_opt :=
      (List.map_opt : (v -> option Color.t) -> list v -> option (list Color.t))
      in
    (map_opt : (v -> option Color.t) -> list v -> option (list Color.t))
      (f_value : v -> option Color.t) (g_value.(Graph.t.vertices) : list v) in
  Option.bind sol get_coloring.

Definition solve {v : Set}
  (equal : v -> v -> bool) (sat_sol : CNF.solver v) (g_value : Graph.t v)
  : option Color.coloring :=
  recover_answer equal g_value (sat_sol equal (generate_cnf g_value)).

author: bot-mne-v-rot


text:
(***
 * Oqarina
 * Copyright 2021 Carnegie Mellon University.
 *
 * NO WARRANTY. THIS CARNEGIE MELLON UNIVERSITY AND SOFTWARE ENGINEERING
 * INSTITUTE MATERIAL IS FURNISHED ON AN "AS-IS" BASIS. CARNEGIE MELLON
 * UNIVERSITY MAKES NO WARRANTIES OF ANY KIND, EITHER EXPRESSED OR
 * IMPLIED, AS TO ANY MATTER INCLUDING, BUT NOT LIMITED TO, WARRANTY OF
 * FITNESS FOR PURPOSE OR MERCHANTABILITY, EXCLUSIVITY, OR RESULTS
 * OBTAINED FROM USE OF THE MATERIAL. CARNEGIE MELLON UNIVERSITY DOES NOT
 * MAKE ANY WARRANTY OF ANY KIND WITH RESPECT TO FREEDOM FROM PATENT,
 * TRADEMARK, OR COPYRIGHT INFRINGEMENT.
 *
 * Released under a BSD (SEI)-style license, please see license.txt or
 * contact permission@sei.cmu.edu for full terms.
 *
 * [DISTRIBUTION STATEMENT A] This material has been approved for public
 * release and unlimited distribution.  Please see Copyright notice for
 * non-US Government use and distribution.
 *
 * This Software includes and/or makes use of the following Third-Party
 * Software subject to its own license:
 *
 * 1. Coq theorem prover (https://github.com/coq/coq/blob/master/LICENSE)
 * Copyright 2021 INRIA.
 *
 * 2. Coq JSON (https://github.com/liyishuai/coq-json/blob/comrade/LICENSE)
 * Copyright 2021 Yishuai Li.
 *
 * DM21-0762
***)
(** %\section{\texttt{Communication\_Properties}} %*)

(* begin hide *)
(** Coq Library *)
Require Import List.
Import ListNotations. (* from List *)
Require Import Coq.Lists.ListDec.
Require Import Coq.ZArith.ZArith.

(** Oqarina library *)
Require Import Oqarina.core.all.
Require Import Oqarina.coq_utils.all.
Require Import Oqarina.AADL.Kernel.all.
Require Import Oqarina.AADL.property_sets.aadl_project.
(* end hide *)

(** %\N \texttt{communication\_properties}% as Coq/AADL property_types. *)

Definition Communication_Properties_PS :=
    PropertySet (Id "Communication_Properties") [

    (* Overflow_Handling_Protocol: enumeration (DropOldest, DropNewest, Error)
       => DropOldest applies to (event port, event data port,
                                 subprogram access); *)

    "Overflow_Handling_Protocol" :prop PT_Enumeration [
        Id "DropOldest"; Id "DropNewest"; Id "Error" ]
        => (Some (PV_Enum (Id "DropOldest"))) applies [];

    (* Queue_Size: aadlinteger 0 .. Max_Queue_Size => 1
          applies to (event port, event data port, subprogram access); *)

    "Queue_Size" :prop aadlinteger
          => (Some (PV_Int 1%Z)) applies [] ;

    (* IO_Reference_Time: type enumeration
        (Dispatch, Start, Completion, Deadline, NoIO, Dynamic); *)

    "IO_Reference_Time" :type PT_Enumeration [
      Id "Dispatch" ; Id "Start" ;  Id "Completion" ; Id "Deadline" ;
      Id "NoIO" ; Id "Dynamic" ];

    (* IO_Time_Spec: type record (
        Offset: Time_Range;
        Time: IO_Reference_Time; ); *)

    "IO_Time_Spec" :type PT_Record [
      FieldDecl (Id "Offset") (PT_TypeRef (PSQN "AADL_Project" "Time_Range")) ;
      FieldDecl (Id "Time")
        (PT_TypeRef (PSQN "Communication_Properties" "IO_Reference_Time")) ];

    (* Input_Time: list of IO_Time_Spec =>
        ([Time => Dispatch; Offset => 0 ns .. 0 ns;])
		    applies to (feature); *)

    "Input_Time" :prop PT_List
                  (PT_TypeRef (PSQN "Communication_Properties" "IO_Time_Spec"))
      => (Some (PV_List
                [ PV_Record [
                  FieldVal (Id "Time") (PV_Enum (Id "Dispatch")) ;
                  FieldVal (Id "Offset")
                      (PV_IntRange (PV_IntU 0 (PV_Unit (Id "ns")))
                                   (PV_IntU 0 (PV_Unit (Id "ns"))))
                     ]]))
        applies []

  ].

  Lemma Communication_Properties_PS_Valid :
    typecheck_property_sets [AADL_Project_PS ; Communication_Properties_PS] = true.
  Proof.
      trivial.
  Qed.

(** %
  \begin{definition}[Queue\_Size (AADLv2.2 \S XXX]
 TBD
  \end{definition}
% *)

Definition Queue_Size_Name := PSQN "Communication_Properties" "Queue_Size".

Definition Is_Queue_Size (pa : property_association) :=
  Is_Property_Name Queue_Size_Name pa.

Definition Map_Queue_Size (pa : list property_association) : Z :=
    let pv := resolve_default_value [Communication_Properties_PS] Queue_Size_Name in
      match pv with
      | None => -1%Z (* should never be executed *)
      | Some pv_ => Map_PV_Int_List pa pv_ Is_Queue_Size
      end.

(** %
  \begin{definition}[Overflow\_Handling\_Protocol (AADLv2.2 \S XXX]
 TBD
  \end{definition}
% *)

Definition Overflow_Handling_Protocol_Name := PSQN "Communication_Properties" "Overflow_Handling_Protocol".

Definition Is_Overflow_Handling_Protocol(pa : property_association) :=
  Is_Property_Name Overflow_Handling_Protocol_Name pa.

Inductive Overflow_Handling_Protocol :=
Unspecified_Overflow_Handling_Protocol | DropOldest | DropNewest | Error.
Scheme Equality for Overflow_Handling_Protocol.

Definition Map_Overflow_Handling_Protocol_pv
  (pv : property_value) : Overflow_Handling_Protocol :=
  match pv with
    | (PV_Enum (Id "DropOldest")) => DropOldest
    | (PV_Enum (Id "DropnNewest")) => DropNewest
    | (PV_Enum (Id "Error")) => Error
    | _ => Unspecified_Overflow_Handling_Protocol
  end.

Definition Map_Overflow_Handling_Protocol (pa : list property_association) :=
  match filter Is_Overflow_Handling_Protocol pa with
  | nil =>
    let pv := resolve_default_value [
      Communication_Properties_PS] Overflow_Handling_Protocol_Name in
      match pv with
      | None => Unspecified_Overflow_Handling_Protocol
      | Some pv => Map_Overflow_Handling_Protocol_pv pv
      end
  | v :: _ => Map_Overflow_Handling_Protocol_pv v.(PV)
  end.

(** %\define{Queue\_Processing\_Protocol (Coq)}{}{TBD} %
*)

Inductive Queue_Processing_Protocol :=
| FIFO.

(** %\define{IO\_Time\_Spec (Coq)}{}{TBD} % *)

Inductive IO_Time_Spec :=
| Dispatch
| Start : Time_Range -> IO_Time_Spec
| Completion : Time_Range -> IO_Time_Spec
| NoIo
| Unspecified_IO_Time_Spec.

Lemma IO_Time_Spec_eq_dec : forall x y : IO_Time_Spec, {x=y}+{x<>y}.
Proof.
  repeat decide equality.
Qed.

Definition Map_IO_Time_Spec (pv : property_value) :=
  match pv with
  | PV_Record l =>
    let time := Get_Record_Member l (Id "Time") in
    match time with
    | None => Unspecified_IO_Time_Spec
    | Some (FieldVal (Id "Time") (PV_Enum (Id "Dispatch"))) => Dispatch
    | Some (FieldVal (Id "Time") (PV_Enum (Id "NoIo"))) => NoIo
    | Some (FieldVal (Id "Time") (PV_Enum (Id "Start"))) =>
    let offset := Get_Record_Member l (Id "Offset") in
    match offset with
      | None => Unspecified_IO_Time_Spec
      | Some (FieldVal _ pv) =>  Start (Map_Time_Range pv)
    end
    | _ => Unspecified_IO_Time_Spec
    end
  | _ => Unspecified_IO_Time_Spec
  end.

Fixpoint Map_IO_Time_Spec_list (pv : list property_value) :=
  match pv with
  | nil => nil
  | h :: t => Map_IO_Time_Spec h :: Map_IO_Time_Spec_list t
  end.

Inductive input_time :=
| Input_Time : list IO_Time_Spec -> input_time.

Lemma input_time_eq_dec : eq_dec input_time.
Proof.
  unfold eq_dec.
  decide equality.
  apply list_eq_dec; apply IO_Time_Spec_eq_dec.
Defined.

Definition projectionIO_Time_Spec (i : input_time) :=
  match i with
  | Input_Time t => t
  end.

(** %\define{Input\_Time (Coq)}{}{TBD} % *)

Definition Input_Time_Name := PSQN "Communication_Properties" "Input_Time".

Definition Is_Input_Time (pa : property_association) :=
  Is_Property_Name Input_Time_Name pa.

Definition Unspecified_Input_Time := Input_Time [ ] .

Definition Map_Input_Time_pv (pv : property_value) :=
  match pv with
  | PV_List l => Input_Time (Map_IO_Time_Spec_list l)
  | _ => Unspecified_Input_Time
  end.

Definition Map_Input_Time (pa : list property_association) : input_time :=
  match filter Is_Input_Time pa with
  | nil =>
    let pv := resolve_default_value [Communication_Properties_PS] Input_Time_Name in
    match pv with
    | None => Unspecified_Input_Time (* should never be executed *)
    | Some pv_ => Map_Input_Time_pv pv_
    end
  | v :: _ => Map_Input_Time_pv v.(PV)
  end.

(** %\define{IO\_Time\_Spec Well-formedness rule (Coq)}{}
  {An input time is well-formed iff. there is no duplicate in the list of IO\_Time\_Spec.} %
*)

Definition input_time_wf  (i : input_time) :=
  NoDup (projectionIO_Time_Spec i).

Definition input_time_wf_dec : forall i : input_time, dec_sumbool (input_time_wf i).
Proof.
  unfold dec_sumbool.
  intros.
  unfold input_time_wf.
  apply NoDup_dec'.
  apply IO_Time_Spec_eq_dec.
Defined.

author: Oqarina

repo: oqarina

save_path: github-repos/coq/Oqarina-oqarina


text:
(**************************************************************************)
(*  This file is part of CertrBPF,                                        *)
(*  a formally verified rBPF verifier + interpreter + JIT in Coq.         *)
(*                                                                        *)
(*  Copyright (C) 2022 Inria                                              *)
(*                                                                        *)
(*  This program is free software; you can redistribute it and/or modify  *)
(*  it under the terms of the GNU General Public License as published by  *)
(*  the Free Software Foundation; either version 2 of the License, or     *)
(*  (at your option) any later version.                                   *)
(*                                                                        *)
(*  This program is distributed in the hope that it will be useful,       *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU General Public License for more details.                          *)
(*                                                                        *)
(**************************************************************************)

From bpf.comm Require Import Flag Regs State Monad LemmaNat rBPFMonadOp.
From bpf.monadicmodel Require Import Opcode rBPFInterpreter.
From Coq Require Import List Lia ZArith.
From compcert Require Import Integers Values Clight Memory.
Import ListNotations.

From bpf.clightlogic Require Import Clightlogic CorrectRel CommonLemma.

From bpf.clight Require Import interpreter.

From bpf.simulation Require Import correct_get_opcode_mem_ld_reg correct_check_mem correct_cmp_ptr32_nullM correct_upd_flag correct_load_mem correct_upd_reg.

From bpf.simulation Require Import MatchState InterpreterRel.

(**
Check step_opcode_mem_ld_reg.

step_opcode_mem_ld_reg
     : val -> int -> reg -> nat -> M unit

*)
Open Scope Z_scope.

Section Step_opcode_mem_ld_reg.
  Context {S: special_blocks}.
  (** The program contains our function of interest [fn] *)
  Definition p : Clight.program := prog.

  (* [Args,Res] provides the mapping between the Coq and the C types *)
  (* Definition Args : list CompilableType := [stateCompilableType].*)
  Definition args : list Type := [(val:Type); (reg:Type); (nat:Type)].
  Definition res : Type := unit.

  (* [f] is a Coq Monadic function with the right type *)
  Definition f : arrow_type args (M State.state res) := step_opcode_mem_ld_reg.

  (* [fn] is the Cligth function which has the same behaviour as [f] *)
  Definition fn: Clight.function := f_step_opcode_mem_ld_reg.

  (* [match_arg] relates the Coq arguments and the C arguments *)
  Definition match_arg_list : DList.t (fun x => x -> Inv _) ((unit:Type) ::args) :=
  (dcons (fun _ => StateLess _ is_state_handle)
    (dcons (stateless val32_correct)
      (dcons (stateless reg_correct)
        (dcons (stateless opcode_correct)
              (DList.DNil _))))).

  (* [match_res] relates the Coq result and the C result *)
  Definition match_res : res -> Inv State.state:= fun _ => StateLess _ (eq Vundef).

  Instance correct_function_step_opcode_mem_ld_reg : forall a, correct_function _ p args res f fn modifies false match_state match_arg_list match_res a.
  Proof.
    correct_function_from_body args.
    correct_body.
    (** how to use correct_* *)
    unfold INV.
    unfold f, app, step_opcode_mem_ld_reg.
    simpl.
    correct_forward.

    get_invariant _op.
    exists (v::nil).
    split.
    unfold map_opt, exec_expr. rewrite p0; reflexivity.
    intros; simpl.
    tauto.

    intros.
    destruct x eqn: HLD.
    - (**r op_BPF_LDXW *)
      eapply correct_statement_switch with (n:= 97%Z).
      + simpl.

        eapply correct_statement_seq_body_drop.
        intros.
        correct_forward.

        get_invariant _st.
        get_invariant _addr.
        exists (v::Vint (Int.repr 1)::Vint (Int.repr 4)::v0::nil).
        split.
        unfold map_opt, exec_expr. rewrite p0, p1.
        reflexivity.
        intros; simpl.
        unfold stateless, perm_correct, match_chunk, rBPFAST.memory_chunk_to_valu32, rBPFAST.well_chunk_Z.
        unfold eval_inv, is_state_handle in c2; unfold stateless in c3.
        eauto.

        intros.
        correct_forward.

        get_invariant _st.
        get_invariant _addr_ptr.
        exists (v0::nil).
        split.
        unfold map_opt, exec_expr. rewrite p1.
        reflexivity.
        intros; simpl.
        unfold val_ptr_correct.
        unfold correct_check_mem.match_res, val_ptr_correct in c3.
        intuition eauto.

        intros.
        correct_forward.

        change (upd_flag Flag.BPF_ILLEGAL_MEM) with
          (bindM (upd_flag Flag.BPF_ILLEGAL_MEM) (fun _ : unit => returnM tt)).
        correct_forward.

        get_invariant _st.
        exists (v::Vint (Int.neg (Int.repr 2))::nil). (**r star here *)
        unfold map_opt, exec_expr.
        rewrite p0.
        unfold Cop.sem_unary_operation, typeof; simpl.
        split; [reflexivity |].
        intros; simpl.
        unfold eval_inv, stateless, flag_correct, int_of_flag, Z_of_flag.
        unfold eval_inv, is_state_handle in c2.
        rewrite Int.neg_repr.
        tauto.

        intros.
        correct_forward.
        unfold match_res.
        reflexivity.

        correct_forward.

        get_invariant _st.
        get_invariant _addr_ptr.
        get_invariant _is_null.
        exists (v::Vint (Int.repr 4)::v0::nil).
        split.
        unfold map_opt, exec_expr. rewrite p0, p1.
        reflexivity.
        intros; simpl.
        unfold stateless, match_chunk, rBPFAST.memory_chunk_to_valu32, rBPFAST.well_chunk_Z, val_ptr_correct.
        unfold eval_inv, is_state_handle in c2; unfold correct_check_mem.match_res, val_ptr_correct in c3.
        split; [intuition|].
        split; [reflexivity|].
        tauto.

        intros.
        correct_forward.

        get_invariant _st.
        get_invariant _dst.
        get_invariant _v.
        exists (v::v0::v1::nil). (**r star here *)
        unfold map_opt, exec_expr.
        rewrite p0, p1, p2.
        split; [reflexivity |].
        intros; simpl.
        tauto.

        intros.
        correct_forward.
        unfold match_res.
        reflexivity.

        get_invariant _is_null.
        unfold eval_inv,correct_cmp_ptr32_nullM.match_res, match_bool in c2.
        unfold exec_expr. rewrite p0.
        subst.
        unfold Val.of_bool, Vtrue, Vfalse.
        destruct x1; reflexivity.
      + reflexivity.
      + intros.
        get_invariant _opcode_ld.
        unfold eval_inv, correct_get_opcode_mem_ld_reg.match_res, opcode_mem_ld_reg_correct in c2.
        subst.
        unfold exec_expr.
        rewrite p0.
        reflexivity.
      + change Int.modulus with 4294967296.
        lia.

    - (**r op_BPF_LDXH *)
      eapply correct_statement_switch with (n:= 105%Z).
      + simpl.

        eapply correct_statement_seq_body_drop.
        intros.
        correct_forward.

        get_invariant _st.
        get_invariant _addr.
        exists (v::Vint (Int.repr 1)::Vint (Int.repr 2)::v0::nil).
        split.
        unfold map_opt, exec_expr. rewrite p0, p1.
        reflexivity.
        intros; simpl.
        unfold eval_inv, stateless, perm_correct, match_chunk, rBPFAST.memory_chunk_to_valu32, rBPFAST.well_chunk_Z.
        unfold eval_inv, is_state_handle in c2; unfold stateless in c3.
        eauto.

        intros.
        correct_forward.

        get_invariant _st.
        get_invariant _addr_ptr.
        exists (v0::nil).
        split.
        unfold map_opt, exec_expr. rewrite p1.
        reflexivity.
        intros; simpl.
        unfold val_ptr_correct.
        unfold eval_inv, is_state_handle in c2.
        unfold correct_check_mem.match_res, val_ptr_correct in c3.
        intuition eauto.

        intros.
        correct_forward.

        change (upd_flag Flag.BPF_ILLEGAL_MEM) with
          (bindM (upd_flag Flag.BPF_ILLEGAL_MEM) (fun _ : unit => returnM tt)).
        correct_forward.

        get_invariant _st.
        exists (v::Vint (Int.neg (Int.repr 2))::nil). (**r star here *)
        unfold map_opt, exec_expr.
        rewrite p0.
        unfold Cop.sem_unary_operation, typeof; simpl.
        split; [reflexivity |].
        intros; simpl.
        unfold eval_inv, stateless, flag_correct, int_of_flag, Z_of_flag.
        unfold eval_inv, is_state_handle in c2.
        rewrite Int.neg_repr.
        tauto.

        intros.
        correct_forward.
        unfold match_res.
        reflexivity.

        correct_forward.

        get_invariant _st.
        get_invariant _addr_ptr.
        get_invariant _is_null.
        exists (v::Vint (Int.repr 2)::v0::nil).
        split.
        unfold map_opt, exec_expr. rewrite p0, p1.
        reflexivity.
        intros; simpl.
        unfold eval_inv, stateless, match_chunk, rBPFAST.memory_chunk_to_valu32, rBPFAST.well_chunk_Z, val_ptr_correct.
        unfold eval_inv, is_state_handle in c2; unfold correct_check_mem.match_res, val_ptr_correct in c3.
        split; [intuition|].
        split; [reflexivity|].
        intuition congruence.

        intros.
        correct_forward.

        get_invariant _st.
        get_invariant _dst.
        get_invariant _v.
        exists (v::v0::v1::nil). (**r star here *)
        unfold map_opt, exec_expr.
        rewrite p0, p1, p2.
        split; [reflexivity |].
        intros; simpl.
        unfold eval_inv, is_state_handle in c2.
        unfold correct_load_mem.match_res in c4.
        intuition eauto.

        intros.
        correct_forward.
        unfold match_res.
        reflexivity.

        get_invariant _is_null.
        unfold eval_inv,correct_cmp_ptr32_nullM.match_res, match_bool in c2.
        unfold exec_expr. rewrite p0.
        subst.
        unfold Val.of_bool, Vtrue, Vfalse.
        destruct x1; reflexivity.
      + reflexivity.
      + intros.
        get_invariant _opcode_ld.
        unfold eval_inv,correct_get_opcode_mem_ld_reg.match_res, opcode_mem_ld_reg_correct in c2.
        subst.
        unfold exec_expr.
        rewrite p0.
        reflexivity.
      + change Int.modulus with 4294967296.
        lia.

    - (**r op_BPF_LDXB *)
      eapply correct_statement_switch with (n:= 113%Z).
      + simpl.

        eapply correct_statement_seq_body_drop.
        intros.
        correct_forward.

        get_invariant _st.
        get_invariant _addr.
        exists (v::Vint (Int.repr 1)::Vint (Int.repr 1)::v0::nil).
        split.
        unfold map_opt, exec_expr. rewrite p0, p1.
        reflexivity.
        intros; simpl.
        unfold eval_inv, stateless, perm_correct, match_chunk, rBPFAST.memory_chunk_to_valu32, rBPFAST.well_chunk_Z.
        unfold eval_inv, is_state_handle in c2; unfold stateless in c3.
        eauto.

        intros.
        correct_forward.

        get_invariant _st.
        get_invariant _addr_ptr.
        exists (v0::nil).
        split.
        unfold map_opt, exec_expr. rewrite p1.
        reflexivity.
        intros; simpl.
        unfold val_ptr_correct.
        unfold eval_inv, is_state_handle in c2.
        unfold correct_check_mem.match_res, val_ptr_correct in c3.
        intuition eauto.

        intros.
        correct_forward.

        change (upd_flag Flag.BPF_ILLEGAL_MEM) with
          (bindM (upd_flag Flag.BPF_ILLEGAL_MEM) (fun _ : unit => returnM tt)).
        correct_forward.

        get_invariant _st.
        exists (v::Vint (Int.neg (Int.repr 2))::nil). (**r star here *)
        unfold map_opt, exec_expr.
        rewrite p0.
        unfold Cop.sem_unary_operation, typeof; simpl.
        split; [reflexivity |].
        intros; simpl.
        unfold eval_inv, stateless, flag_correct, int_of_flag, Z_of_flag.
        unfold eval_inv, is_state_handle in c2.
        rewrite Int.neg_repr.
        tauto.

        intros.
        correct_forward.
        unfold match_res.
        reflexivity.

        correct_forward.

        get_invariant _st.
        get_invariant _addr_ptr.
        get_invariant _is_null.
        exists (v::Vint (Int.repr 1)::v0::nil).
        split.
        unfold map_opt, exec_expr. rewrite p0, p1.
        reflexivity.
        intros; simpl.
        unfold eval_inv, stateless, match_chunk, rBPFAST.memory_chunk_to_valu32, rBPFAST.well_chunk_Z, val_ptr_correct.
        unfold eval_inv, is_state_handle in c2; unfold correct_check_mem.match_res, val_ptr_correct in c3.
        split; [intuition|].
        split; [reflexivity|].
        unfold correct_cmp_ptr32_nullM.match_res in c4.
        intuition congruence.

        intros.
        correct_forward.

        get_invariant _st.
        get_invariant _dst.
        get_invariant _v.
        exists (v::v0::v1::nil). (**r star here *)
        unfold map_opt, exec_expr.
        rewrite p0, p1, p2.
        split; [reflexivity |].
        intros; simpl.
        unfold eval_inv, is_state_handle in c2.
        unfold correct_load_mem.match_res in c4.
        intuition eauto.

        intros.
        correct_forward.
        unfold match_res.
        intros.
        unfold eval_inv.
        reflexivity.

        get_invariant _is_null.
        unfold eval_inv,correct_cmp_ptr32_nullM.match_res, match_bool in c2.
        unfold exec_expr. rewrite p0.
        subst.
        unfold Val.of_bool, Vtrue, Vfalse.
        destruct x1; reflexivity.
      + reflexivity.
      + intros.
        get_invariant _opcode_ld.
        unfold eval_inv,correct_get_opcode_mem_ld_reg.match_res, opcode_mem_ld_reg_correct in c2.
        subst.
        unfold exec_expr.
        rewrite p0.
        reflexivity.
      + change Int.modulus with 4294967296.
        lia.

    - (**r op_BPF_LDXDW *)
      eapply correct_statement_switch with (n:= 121%Z).
      + simpl.

        eapply correct_statement_seq_body_drop.
        intros.
        correct_forward.

        get_invariant _st.
        get_invariant _addr.
        exists (v::Vint (Int.repr 1)::Vint (Int.repr 8)::v0::nil).
        split.
        unfold map_opt, exec_expr. rewrite p0, p1.
        reflexivity.
        intros; simpl.
        unfold eval_inv, stateless, perm_correct, match_chunk, rBPFAST.memory_chunk_to_valu32, rBPFAST.well_chunk_Z.
        unfold eval_inv, is_state_handle in c2; unfold stateless in c3.
        eauto.

        intros.
        correct_forward.

        get_invariant _st.
        get_invariant _addr_ptr.
        exists (v0::nil).
        split.
        unfold map_opt, exec_expr. rewrite p1.
        reflexivity.
        intros; simpl.
        unfold val_ptr_correct.
        unfold eval_inv, is_state_handle in c2.
        unfold correct_check_mem.match_res, val_ptr_correct in c3.
        intuition eauto.

        intros.
        correct_forward.

        change (upd_flag Flag.BPF_ILLEGAL_MEM) with
          (bindM (upd_flag Flag.BPF_ILLEGAL_MEM) (fun _ : unit => returnM tt)).
        correct_forward.

        get_invariant _st.
        exists (v::Vint (Int.neg (Int.repr 2))::nil). (**r star here *)
        unfold map_opt, exec_expr.
        rewrite p0.
        unfold Cop.sem_unary_operation, typeof; simpl.
        split; [reflexivity |].
        intros; simpl.
        unfold eval_inv, stateless, flag_correct, int_of_flag, Z_of_flag.
        unfold eval_inv, is_state_handle in c2.
        rewrite Int.neg_repr.
        tauto.

        intros.
        correct_forward.
        unfold match_res.
        reflexivity.

        correct_forward.

        get_invariant _st.
        get_invariant _addr_ptr.
        get_invariant _is_null.
        exists (v::Vint (Int.repr 8)::v0::nil).
        split.
        unfold map_opt, exec_expr. rewrite p0, p1.
        reflexivity.
        intros; simpl.
        unfold eval_inv, stateless, match_chunk, rBPFAST.memory_chunk_to_valu32, rBPFAST.well_chunk_Z, val_ptr_correct.
        unfold eval_inv, is_state_handle in c2; unfold eval_inv,correct_check_mem.match_res, val_ptr_correct,stateless in c3.
        intuition congruence.

        intros.
        correct_forward.

        get_invariant _st.
        get_invariant _dst.
        get_invariant _v.
        exists (v::v0::v1::nil). (**r star here *)
        unfold map_opt, exec_expr.
        rewrite p0, p1, p2.
        split; [reflexivity |].
        intros; simpl.
        unfold eval_inv, is_state_handle in c2.
        unfold correct_load_mem.match_res in c4.
        intuition eauto.

        intros.
        correct_forward.
        unfold match_res.
        reflexivity.

        get_invariant _is_null.
        unfold eval_inv,correct_cmp_ptr32_nullM.match_res, match_bool in c2.
        unfold exec_expr. rewrite p0.
        subst.
        unfold Val.of_bool, Vtrue, Vfalse.
        destruct x1; reflexivity.
      + reflexivity.
      + intros.
        get_invariant _opcode_ld.
        unfold eval_inv,correct_get_opcode_mem_ld_reg.match_res, opcode_mem_ld_reg_correct in c2.
        subst.
        unfold exec_expr.
        rewrite p0.
        reflexivity.
      + change Int.modulus with 4294967296.
        lia.
    - (**r op_BPF_LDX_REG_ILLEGAL_INS *)
      eapply correct_statement_switch_ex.
      + reflexivity.
      + intros.
        assert (Hillegal_ins: exists n i,
          eval_inv (correct_get_opcode_mem_ld_reg.match_res op_BPF_LDX_REG_ILLEGAL_INS) n st0 m0 /\
          n = Vint (Int.repr (Z.of_nat i)) /\
          (i <> 0x61 /\ i <> 0x69 /\ i <> 0x71 /\ i <> 0x79)%nat /\
          (i <= 255)%nat /\
          exec_expr (Smallstep.globalenv (semantics2 p)) empty_env le0 m0
            (Etempvar _opcode_ld Ctypesdefs.tuchar) =
              Some (Vint (Int.repr (Z.of_nat i)))).
        {
          get_invariant _opcode_ld.
          unfold correct_get_opcode_mem_ld_reg.match_res in c2.
          exists v.
          assert (c3':=c2).
          unfold opcode_mem_ld_reg_correct in c3'.
          destruct c3' as (i & V & ILL & RANGE).
          exists i.
          split ; auto.
          split ; auto.
          split ; auto.
          split ; auto.
          unfold exec_expr. congruence.
        }
        destruct Hillegal_ins as (n & i & Hprop & Hn_eq & Hill & Hrange & EX).
        exists (Z.of_nat i).
        split; auto.
        split.

        change Int.modulus with 4294967296.
        lia.

        unfold select_switch.
        unfold select_switch_case.
        repeat destruct Coqlib.zeq; try lia.
        (* default *)
        simpl.
        (**r s1 -> (Ssequence s1 s2) *)
        eapply correct_statement_seq_body_drop.
        intros.

        change (upd_flag Flag.BPF_ILLEGAL_INSTRUCTION) with
          (bindM (upd_flag Flag.BPF_ILLEGAL_INSTRUCTION) (fun _ : unit => returnM tt)).
        correct_forward.

        get_invariant _st.
        exists (v ::
                (Vint (Int.neg (Int.repr 1))) :: nil). (**r star here *)
        unfold map_opt, exec_expr.
        rewrite p0.
        unfold Cop.sem_unary_operation; simpl.
        split.
        reflexivity.
        intros.
        unfold eval_inv, stateless, flag_correct, int_of_flag; simpl.
        split; auto.
        intros.

        (**r goal: correct_body p unit (returnM tt) fn (Sreturn None) modifies *)
        correct_forward.
        reflexivity.
  Qed.

End Step_opcode_mem_ld_reg.

Close Scope Z_scope.

Existing Instance correct_function_step_opcode_mem_ld_reg.

author: future-proof-iot

repo: CertFC


text:
Require Import Coq.Classes.Morphisms Crypto.Util.Relations Crypto.Util.Tactics.
Require Import Crypto.Algebra Crypto.Algebra.Monoid Crypto.Algebra.ScalarMult.

Section BasicProperties.
  Context {T eq op id inv} `{@group T eq op id inv}.
  Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
  Local Infix "*" := op.
  Local Infix "=" := eq : eq_scope.
  Local Open Scope eq_scope.

  Lemma cancel_left : forall z x y, z*x = z*y <-> x = y.
  Proof. eauto using Monoid.cancel_left, left_inverse. Qed.
  Lemma cancel_right : forall z x y, x*z = y*z <-> x = y.
  Proof. eauto using Monoid.cancel_right, right_inverse. Qed.
  Lemma inv_inv x : inv(inv(x)) = x.
  Proof. eauto using Monoid.inv_inv, left_inverse. Qed.
  Lemma inv_op_ext x y : (inv y*inv x)*(x*y) =id.
  Proof. eauto using Monoid.inv_op, left_inverse. Qed.

  Lemma inv_unique x ix : ix * x = id -> ix = inv x.
  Proof.
    intro Hix.
    cut (ix*x*inv x = inv x).
    - rewrite <-associative, right_inverse, right_identity; trivial.
    - rewrite Hix, left_identity; reflexivity.
  Qed.

  Lemma inv_bijective x y : inv x = inv y <-> x = y.
  Proof.
    split; intro Hi; rewrite ?Hi; try reflexivity.
    assert (Hii:inv (inv x) = inv (inv y)) by (rewrite Hi; reflexivity).
    rewrite 2inv_inv in Hii; exact Hii.
  Qed.

  Lemma inv_op x y : inv (x*y) = inv y*inv x.
  Proof.
    symmetry. etransitivity.
    2:eapply inv_unique.
    2:eapply inv_op_ext.
    reflexivity.
  Qed.

  Lemma inv_id : inv id = id.
  Proof. symmetry. eapply inv_unique, left_identity. Qed.

  Lemma inv_id_iff x : inv x = id <-> x = id.
  Proof.
    split; intro Hi; rewrite ?Hi, ?inv_id; try reflexivity.
    rewrite <-inv_id, inv_bijective in Hi; exact Hi.
  Qed.

  Lemma inv_nonzero_nonzero x : x <> id <-> inv x <> id.
  Proof. setoid_rewrite inv_id_iff; reflexivity. Qed.

  Lemma eq_r_opp_r_inv a b c : a = op c (inv b) <-> op a b = c.
  Proof.
    split; intro Hx; rewrite Hx || rewrite <-Hx;
      rewrite <-!associative, ?left_inverse, ?right_inverse, right_identity;
      reflexivity.
  Qed.

  Section ZeroNeqOne.
    Context {one} `{is_zero_neq_one T eq id one}.
    Lemma opp_one_neq_zero : inv one <> id.
    Proof. setoid_rewrite inv_id_iff. exact one_neq_zero. Qed.
    Lemma zero_neq_opp_one : id <> inv one.
    Proof. intro Hx. symmetry in Hx. eauto using opp_one_neq_zero. Qed.
  End ZeroNeqOne.
End BasicProperties.

Section Homomorphism.
  Context {G EQ OP ID INV} {groupG:@group G EQ OP ID INV}.
  Context {H eq op id inv} {groupH:@group H eq op id inv}.
  Context {phi:G->H}`{homom:@Monoid.is_homomorphism G EQ OP H eq op phi}.
  Local Infix "=" := eq. Local Infix "=" := eq : type_scope.

  Lemma homomorphism_id : phi ID = id.
  Proof.
    assert (Hii: op (phi ID) (phi ID) = op (phi ID) id) by
        (rewrite <- Monoid.homomorphism, left_identity, right_identity; reflexivity).
    rewrite cancel_left in Hii; exact Hii.
  Qed.

  Lemma homomorphism_inv x : phi (INV x) = inv (phi x).
  Proof.
    apply inv_unique.
    rewrite <- Monoid.homomorphism, left_inverse, homomorphism_id; reflexivity.
  Qed.

  Section ScalarMultHomomorphism.
    Context {MUL} {MUL_is_scalarmult:@ScalarMult.is_scalarmult G EQ OP ID MUL }.
    Context {mul} {mul_is_scalarmult:@ScalarMult.is_scalarmult H eq op id mul }.
    Lemma homomorphism_scalarmult n P : phi (MUL n P) = mul n (phi P).
    Proof. eapply ScalarMult.homomorphism_scalarmult, homomorphism_id. Qed.

    Import ScalarMult.
    Lemma opp_mul : forall n P, inv (mul n P) = mul n (inv P).
    Proof.
      induction n; intros.
      { rewrite !scalarmult_0_l, inv_id; reflexivity. }
      { rewrite <-NPeano.Nat.add_1_l, Plus.plus_comm at 1.
        rewrite scalarmult_add_l, scalarmult_1_l, inv_op, scalarmult_S_l, cancel_left; eauto. }
    Qed.
  End ScalarMultHomomorphism.
End Homomorphism.

Section Homomorphism_rev.
  Context {G EQ OP ID INV} {groupG:@group G EQ OP ID INV}.
  Context {H} {eq : H -> H -> Prop} {op : H -> H -> H} {id : H} {inv : H -> H}.
  Context {phi:G->H} {phi':H->G}.
  Local Infix "=" := EQ. Local Infix "=" := EQ : type_scope.
  Context (phi'_phi_id : forall A, phi' (phi A) = A)
          (phi'_eq : forall a b, EQ (phi' a) (phi' b) <-> eq a b)
          (phi'_op : forall a b, phi' (op a b) = OP (phi' a) (phi' b))
          {phi'_inv : forall a, phi' (inv a) = INV (phi' a)}
          {phi'_id : phi' id = ID}.

  Lemma group_from_redundant_representation
    : @group H eq op id inv /\ @Monoid.is_homomorphism G EQ OP H eq op phi /\ @Monoid.is_homomorphism H eq op G EQ OP phi'.
  Proof.
    repeat match goal with
           | [ H : _/\_ |- _ ] => destruct H; try clear H
           | [ H : group |- _ ] => destruct H; try clear H
           | [ H : monoid |- _ ] => destruct H; try clear H
           | [ H : is_associative |- _ ] => destruct H; try clear H
           | [ H : is_left_identity |- _ ] => destruct H; try clear H
           | [ H : is_right_identity |- _ ] => destruct H; try clear H
           | [ H : Equivalence _ |- _ ] => destruct H; try clear H
           | [ H : is_left_inverse |- _ ] => destruct H; try clear H
           | [ H : is_right_inverse |- _ ] => destruct H; try clear H
           | _ => intro
           | _ => split
           | [ H : eq _ _ |- _ ] => apply phi'_eq in H
           | [ |- eq _ _ ] => apply phi'_eq
           | [ H : EQ _ _ |- _ ] => rewrite H
           | _ => progress erewrite ?phi'_op, ?phi'_inv, ?phi'_id, ?phi'_phi_id by reflexivity
           | [ H : _ |- _ ] => progress erewrite ?phi'_op, ?phi'_inv, ?phi'_id in H by reflexivity
           | _ => solve [ eauto ]
           end.
  Qed.

  Definition homomorphism_from_redundant_representation
    : @Monoid.is_homomorphism G EQ OP H eq op phi.
  Proof.
    split; repeat intro; apply phi'_eq; rewrite ?phi'_op, ?phi'_phi_id; easy.
  Qed.
End Homomorphism_rev.

Section GroupByHomomorphism.
  Lemma surjective_homomorphism_from_group
        {G EQ OP ID INV} {groupG:@group G EQ OP ID INV}
        {H eq op id inv}
        {Equivalence_eq: @Equivalence H eq} {eq_dec: forall x y, {eq x y} + {~ eq x y} }
        {Proper_op:Proper(eq==>eq==>eq)op}
        {Proper_inv:Proper(eq==>eq)inv}
        {phi iph} {Proper_phi:Proper(EQ==>eq)phi} {Proper_iph:Proper(eq==>EQ)iph}
        {surj:forall h, eq (phi (iph h)) h}
        {phi_op : forall a b, eq (phi (OP a b)) (op (phi a) (phi b))}
        {phi_inv : forall a, eq (phi (INV a)) (inv (phi a))}
        {phi_id : eq (phi ID) id}
  : @group H eq op id inv.
  Proof.
    repeat split; eauto with core typeclass_instances; intros;
      repeat match goal with
               |- context[?x] =>
               match goal with
               | |- context[iph x] => fail 1
               | _ => unify x id; fail 1
               | _ => is_var x; rewrite <- (surj x)
               end
             end;
      repeat rewrite <-?phi_op, <-?phi_inv, <-?phi_id;
      f_equiv; auto using associative, left_identity, right_identity, left_inverse, right_inverse.
  Qed.

  Lemma isomorphism_to_subgroup_group
        {G EQ OP ID INV}
        {Equivalence_EQ: @Equivalence G EQ} {eq_dec: forall x y, {EQ x y} + {~ EQ x y} }
        {Proper_OP:Proper(EQ==>EQ==>EQ)OP}
        {Proper_INV:Proper(EQ==>EQ)INV}
        {H eq op id inv} {groupG:@group H eq op id inv}
        {phi}
        {eq_phi_EQ: forall x y, eq (phi x) (phi y) -> EQ x y}
        {phi_op : forall a b, eq (phi (OP a b)) (op (phi a) (phi b))}
        {phi_inv : forall a, eq (phi (INV a)) (inv (phi a))}
        {phi_id : eq (phi ID) id}
    : @group G EQ OP ID INV.
  Proof.
    repeat split; eauto with core typeclass_instances; intros;
      eapply eq_phi_EQ;
      repeat rewrite ?phi_op, ?phi_inv, ?phi_id;
      auto using associative, left_identity, right_identity, left_inverse, right_inverse.
  Qed.
End GroupByHomomorphism.

Section HomomorphismComposition.
  Context {G EQ OP ID INV} {groupG:@group G EQ OP ID INV}.
  Context {H eq op id inv} {groupH:@group H eq op id inv}.
  Context {K eqK opK idK invK} {groupK:@group K eqK opK idK invK}.
  Context {phi:G->H} {phi':H->K}
          {Hphi:@Monoid.is_homomorphism G EQ OP H eq op phi}
          {Hphi':@Monoid.is_homomorphism H eq op K eqK opK phi'}.
  Lemma is_homomorphism_compose
        {phi'':G->K}
        (Hphi'' : forall x, eqK (phi' (phi x)) (phi'' x))
    : @Monoid.is_homomorphism G EQ OP K eqK opK phi''.
  Proof.
    split; repeat intro; rewrite <- !Hphi''.
    { rewrite !Monoid.homomorphism; reflexivity. }
    { apply Hphi', Hphi; assumption. }
  Qed.

  Global Instance is_homomorphism_compose_refl
    : @Monoid.is_homomorphism G EQ OP K eqK opK (fun x => phi' (phi x))
    := is_homomorphism_compose (fun x => reflexivity _).
End HomomorphismComposition.

author: JasonGross

repo: slow-coq-examples


text:
Require Import JMeq ProofIrrelevance.
Require Export Notations.
Require Import Common StructureEquality FEqualDep.

Set Implicit Arguments.

Generalizable All Variables.

Set Asymmetric Patterns.

Set Universe Polymorphism.

Local Infix "==" := JMeq.

Record SpecializedCategory (obj : Type) :=
  Build_SpecializedCategory' {
      Object :> _ := obj;
      Morphism : obj -> obj -> Type;

      Identity : forall x, Morphism x x;
      Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d';

      Associativity : forall o1 o2 o3 o4
                             (m1 : Morphism o1 o2)
                             (m2 : Morphism o2 o3)
                             (m3 : Morphism o3 o4),
                        Compose (Compose m3 m2) m1 = Compose m3 (Compose m2 m1);
      (* ask for [eq_sym (Associativity ...)], so that C^{op}^{op} is convertible with C *)
      Associativity_sym : forall o1 o2 o3 o4
                                 (m1 : Morphism o1 o2)
                                 (m2 : Morphism o2 o3)
                                 (m3 : Morphism o3 o4),
                            Compose m3 (Compose m2 m1) = Compose (Compose m3 m2) m1;
      LeftIdentity : forall a b (f : Morphism a b), Compose (Identity b) f = f;
      RightIdentity : forall a b (f : Morphism a b), Compose f (Identity a) = f
    }.

Bind Scope category_scope with SpecializedCategory.
Bind Scope object_scope with Object.
Bind Scope morphism_scope with Morphism.

Arguments Object {obj%type} C%category / : rename.
Arguments Morphism {obj%type} !C%category s d : rename. (* , simpl nomatch. *)
Arguments Identity {obj%type} [!C%category] x%object : rename.
Arguments Compose {obj%type} [!C%category s%object d%object d'%object] m1%morphism m2%morphism : rename.

Section SpecializedCategoryInterface.
  Definition Build_SpecializedCategory (obj : Type)
             (Morphism : obj -> obj -> Type)
             (Identity' : forall o : obj, Morphism o o)
             (Compose' : forall s d d' : obj, Morphism d d' -> Morphism s d -> Morphism s d')
             (Associativity' : forall (o1 o2 o3 o4 : obj) (m1 : Morphism o1 o2) (m2 : Morphism o2 o3) (m3 : Morphism o3 o4),
                                 Compose' o1 o2 o4 (Compose' o2 o3 o4 m3 m2) m1 = Compose' o1 o3 o4 m3 (Compose' o1 o2 o3 m2 m1))
             (LeftIdentity' : forall (a b : obj) (f : Morphism a b), Compose' a b b (Identity' b) f = f)
             (RightIdentity' : forall (a b : obj) (f : Morphism a b), Compose' a a b f (Identity' a) = f)
  : @SpecializedCategory obj
    := @Build_SpecializedCategory' obj
                                   Morphism
                                   Identity'
                                   Compose'
                                   Associativity'
                                   (fun _ _ _ _ _ _ _ => eq_sym (Associativity' _ _ _ _ _ _ _))
                                   LeftIdentity'
                                   RightIdentity'.
End SpecializedCategoryInterface.

(* create a hint db for all category theory things *)
Create HintDb category discriminated.
(* create a hint db for morphisms in categories *)
Create HintDb morphism discriminated.

Hint Extern 1 => symmetry : category morphism. (* TODO(jgross): Why do I need this? *)

Ltac spcategory_hideProofs :=
  repeat match goal with
             | [ |- context[{|
                               Associativity := ?pf0;
                               Associativity_sym := ?pf1;
                               LeftIdentity := ?pf2;
                               RightIdentity := ?pf3
                             |}] ] =>
               hideProofs pf0 pf1 pf2 pf3
         end.

Hint Resolve @LeftIdentity @RightIdentity @Associativity : category morphism.
Hint Rewrite @LeftIdentity @RightIdentity : category.
Hint Rewrite @LeftIdentity @RightIdentity : morphism.

(* eh, I'm not terribly happy.  meh. *)
Definition LocallySmallSpecializedCategory (obj : Type) (*mor : obj -> obj -> Set*) := SpecializedCategory obj.
Definition SmallSpecializedCategory (obj : Set) (*mor : obj -> obj -> Set*) := SpecializedCategory obj.
Identity Coercion LocallySmallSpecializedCategory_SpecializedCategory_Id : LocallySmallSpecializedCategory >-> SpecializedCategory.
Identity Coercion SmallSpecializedCategory_LocallySmallSpecializedCategory_Id : SmallSpecializedCategory >-> SpecializedCategory.

Section Categories_Equal.
  Lemma SpecializedCategory_contr_eq' `(C : @SpecializedCategory objC) `(D : @SpecializedCategory objC)
        (C_morphism_proof_irrelevance
         : forall s d (m1 m2 : Morphism C s d) (pf1 pf2 : m1 = m2),
             pf1 = pf2)
  : forall (HM : @Morphism _ C = @Morphism _ D),
      match HM in (_ = y) return (forall x : objC, y x x) with
        | eq_refl => Identity (C := C)
      end = Identity (C := D)
      -> match
        HM in (_ = y) return (forall s d d' : objC, y d d' -> y s d -> y s d')
      with
        | eq_refl => Compose (C := C)
      end = Compose (C := D)
      -> C = D.
    intros.
    destruct C, D;
      subst_body;
      intros;
      simpl in *.
    subst.
    repeat f_equal;
      repeat (apply functional_extensionality_dep; intro);
      trivial.
  Qed.

  Lemma SpecializedCategory_contr_eq `(C : @SpecializedCategory objC) `(D : @SpecializedCategory objC)
        (C_morphism_proof_irrelevance
         : forall s d (m1 m2 : Morphism C s d) (pf1 pf2 : m1 = m2),
             pf1 = pf2)
        (C_morphism_type_contr
         : forall s d (pf1 pf2 : Morphism C s d = Morphism C s d),
             pf1 = pf2)
  : forall (HM : forall s d, @Morphism _ C s d = @Morphism _ D s d),
      (forall x,
         match HM x x in (_ = y) return y with
           | eq_refl => Identity (C := C) x
         end = Identity (C := D) x)
      -> (forall s d d' (m : Morphism D d d') (m' : Morphism D s d),
            match HM s d' in (_ = y) return y with
              | eq_refl =>
                match HM s d in (_ = y) return (y -> Morphism C s d') with
                  | eq_refl =>
                    match
                      HM d d' in (_ = y) return (y -> Morphism C s d -> Morphism C s d')
                    with
                      | eq_refl => Compose (d':=d')
                    end m
                end m'
            end = Compose m m')
      -> C = D.
    intros HM HI HC.
    assert (HM' : @Morphism _ C = @Morphism _ D)
      by (repeat (apply functional_extensionality_dep; intro); trivial).
    apply (SpecializedCategory_contr_eq' _ _ C_morphism_proof_irrelevance HM');
      revert HI HC C_morphism_proof_irrelevance C_morphism_type_contr;
      destruct C, D; simpl in *; clear;
      intros;
      subst_body;
      simpl in *;
      repeat (subst || intro || apply functional_extensionality_dep);
      rewrite_rev_hyp;
      generalize_eq_match;
      subst_eq_refl_dec;
      trivial.
  Qed.

  Lemma SpecializedCategory_eq `(C : @SpecializedCategory objC) `(D : @SpecializedCategory objC) :
    @Morphism _ C = @Morphism _ D
    -> @Identity _ C == @Identity _ D
    -> @Compose _ C == @Compose _ D
    -> C = D.
    intros.
    destruct_head @SpecializedCategory;
    simpl in *; repeat subst;
    f_equal; apply proof_irrelevance.
  Qed.

  Lemma SpecializedCategory_JMeq `(C : @SpecializedCategory objC) `(D : @SpecializedCategory objD) :
    objC = objD
    -> @Morphism _ C == @Morphism _ D
    -> @Identity _ C == @Identity _ D
    -> @Compose _ C == @Compose _ D
    -> C == D.
    intros; destruct_head @SpecializedCategory;
    simpl in *; repeat subst; JMeq_eq;
    f_equal; apply proof_irrelevance.
  Qed.
End Categories_Equal.

Ltac spcat_eq_step_with tac :=
  structures_eq_step_with_tac ltac:(apply SpecializedCategory_eq || apply SpecializedCategory_JMeq) tac.

Ltac spcat_eq_with tac := repeat spcat_eq_step_with tac.

Ltac spcat_eq_step := spcat_eq_step_with idtac.
Ltac spcat_eq := spcategory_hideProofs; spcat_eq_with idtac.

Ltac solve_for_identity :=
  match goal with
    | [ |- @Compose _ ?C ?s ?s ?d ?a ?b = ?b ]
      => cut (a = @Identity _ C s);
        [ try solve [ let H := fresh in intro H; rewrite H; apply LeftIdentity ] | ]
    | [ |- @Compose _ ?C ?s ?d ?d ?a ?b = ?a ]
      => cut (b = @Identity _ C d );
        [ try solve [ let H := fresh in intro H; rewrite H; apply RightIdentity ] | ]
  end.

(** * Version of [Associativity] that avoids going off into the weeds in the presence of unification variables *)

Definition NoEvar T (_ : T) := True.

Lemma AssociativityNoEvar `(C : @SpecializedCategory obj) : forall (o1 o2 o3 o4 : C) (m1 : C.(Morphism) o1 o2)
  (m2 : C.(Morphism) o2 o3) (m3 : C.(Morphism) o3 o4),
  NoEvar (m1, m2) \/ NoEvar (m2, m3) \/ NoEvar (m1, m3)
  -> Compose (Compose m3 m2) m1 = Compose m3 (Compose m2 m1).
  intros; apply Associativity.
Qed.

Ltac noEvar := match goal with
                 | [ |- context[NoEvar ?X] ] => (has_evar X; fail 1)
                                                  || cut (NoEvar X); [ intro; tauto | constructor ]
               end.

Hint Rewrite @AssociativityNoEvar using noEvar : category.
Hint Rewrite @AssociativityNoEvar using noEvar : morphism.

Ltac try_associativity_quick tac := try_rewrite Associativity tac.
Ltac try_associativity tac := try_rewrite_by AssociativityNoEvar ltac:(idtac; noEvar) tac.

Ltac find_composition_to_identity :=
  match goal with
    | [ H : @Compose _ _ _ _ _ ?a ?b = @Identity _ _ _ |- context[@Compose ?A ?B ?C ?D ?E ?c ?d] ]
      => let H' := fresh in
        assert (H' : b = d /\ a = c) by (split; reflexivity); clear H';
          assert (H' : @Compose A B C D E c d = @Identity _ _ _) by (
            exact H ||
              (unfold Object; simpl in H |- *; exact H || (rewrite H; reflexivity))
          );
          first [
            rewrite H'
            | simpl in H' |- *; rewrite H'
            | let H'T := type of H' in fail 2 "error in rewriting a found identity" H "[" H'T "]"
          ]; clear H'
  end.

(** * Back to the main content.... *)

Section Category.
  Context `(C : @SpecializedCategory objC).

  (* Quoting Wikipedia,
    In category theory, an epimorphism (also called an epic
    morphism or, colloquially, an epi) is a morphism [f : X → Y]
    which is right-cancellative in the sense that, for all
    morphisms [g, g' : Y → Z],
    [g ○ f = g' ○ f -> g = g']

    Epimorphisms are analogues of surjective functions, but they
    are not exactly the same. The dual of an epimorphism is a
    monomorphism (i.e. an epimorphism in a category [C] is a
    monomorphism in the dual category [OppositeCategory C]).
    *)
  Definition IsEpimorphism x y (m : C.(Morphism) x y) : Prop :=
    forall z (m1 m2 : C.(Morphism) y z), Compose m1 m = Compose m2 m ->
      m1 = m2.
  Definition IsMonomorphism x y (m : C.(Morphism) x y) : Prop :=
    forall z (m1 m2 : C.(Morphism) z x), Compose m m1 = Compose m m2 ->
      m1 = m2.

  Section properties.
    Lemma IdentityIsEpimorphism x : IsEpimorphism _ _ (Identity x).
      repeat intro; autorewrite with category in *; trivial.
    Qed.

    Lemma IdentityIsMonomorphism x : IsMonomorphism _ _ (Identity x).
      repeat intro; autorewrite with category in *; trivial.
    Qed.

    Lemma EpimorphismComposition s d d' m0 m1 :
      IsEpimorphism _ _ m0
      -> IsEpimorphism _ _ m1
      -> IsEpimorphism _ _ (Compose (C := C) (s := s) (d := d) (d' := d') m0 m1).
      repeat intro.
      repeat match goal with | [ H : _ |- _ ] => rewrite <- Associativity in H end.
      intuition.
    Qed.

    Lemma MonomorphismComposition s d d' m0 m1 :
      IsMonomorphism _ _ m0
      -> IsMonomorphism _ _ m1
      -> IsMonomorphism _ _ (Compose (C := C) (s := s) (d := d) (d' := d') m0 m1).
      repeat intro.
      repeat match goal with | [ H : _ |- _ ] => rewrite Associativity in H end.
      intuition.
    Qed.
  End properties.
End Category.

Hint Immediate @IdentityIsEpimorphism @IdentityIsMonomorphism @MonomorphismComposition @EpimorphismComposition : category morphism.

Arguments IsEpimorphism {objC} [C x y] m.
Arguments IsMonomorphism {objC} [C x y] m.

Section AssociativityComposition.
  Context `(C : @SpecializedCategory obj).
  Variables o0 o1 o2 o3 o4 : C.

  Lemma compose4associativity_helper
    (a : Morphism C o3 o4) (b : Morphism C o2 o3)
    (c : Morphism C o1 o2) (d : Morphism C o0 o1) :
    Compose (Compose a b) (Compose c d) = (Compose a (Compose (Compose b c) d)).
    repeat rewrite Associativity; reflexivity.
  Qed.
End AssociativityComposition.

Ltac compose4associativity' a b c d := transitivity (Compose a (Compose (Compose b c) d)); try solve [ apply compose4associativity_helper ].
Ltac compose4associativity :=
  match goal with
    | [ |- Compose (Compose ?a ?b) (Compose ?c ?d) = _ ] => compose4associativity' a b c d
    | [ |- _ = Compose (Compose ?a ?b) (Compose ?c ?d) ] => compose4associativity' a b c d
  end.

author: CategoricalData

repo: catdb

save_path: github-repos/coq/CategoricalData-catdb


text:
From Test Require Import tactic.

Section FOFProblem.

Variable Universe : Set.
Variable UniverseElement : Universe.

Variable wd_ : Universe -> Universe -> Prop.
Variable col_ : Universe -> Universe -> Universe -> Prop.

Variable col_swap1_1 : (forall A B C : Universe, (col_ A B C -> col_ B A C)).
Variable col_swap2_2 : (forall A B C : Universe, (col_ A B C -> col_ B C A)).
Variable col_triv_3 : (forall A B : Universe, col_ A B B).
Variable wd_swap_4 : (forall A B : Universe, (wd_ A B -> wd_ B A)).
Variable col_trans_5 : (forall P Q A B C : Universe, ((wd_ P Q /\ (col_ P Q A /\ (col_ P Q B /\ col_ P Q C))) -> col_ A B C)).

Theorem pipo_6 : (forall O E Eprime A B C D X Bprimeprime Dprime : Universe, ((wd_ C O /\ (wd_ A O /\ (wd_ B O /\ (wd_ D O /\ (wd_ O E /\ (wd_ O Eprime /\ (wd_ E Eprime /\ (wd_ Eprime C /\ (wd_ X O /\ (wd_ E Bprimeprime /\ (wd_ C X /\ (wd_ B Bprimeprime /\ (col_ O E A /\ (col_ O E B /\ (col_ O E C /\ (col_ O E D /\ (col_ O E X /\ (col_ O Eprime Bprimeprime /\ (col_ O Eprime X /\ col_ O Eprime Dprime))))))))))))))))))) -> col_ O E Eprime)).
Proof.
  time tac.
Qed.

End FOFProblem.

author: janicicpredrag

repo: Larus

save_path: github-repos/coq/janicicpredrag-Larus


text:
Set Default Goal Selector "!".

From Undecidability.MinskyMachines Require Import MM_computable MM_sss mm_utils.
From Undecidability.StackMachines Require Import BSM_computable.

From Undecidability.Shared.Libs.DLW Require Import vec pos sss subcode.

Require Import Lia Vector Nat Arith List.

From Undecidability.MinskyMachines.MM
  Require Import mm_defs mm_utils mm_comp_strong.

Definition MM_cast {n} (P : list (mm_instr (Fin.t n))) {m} (E : n = m) : list (mm_instr (Fin.t m)).
subst m. exact P. Defined.

Lemma MM_cast_length {n} (P : list (mm_instr (Fin.t n))) {m} (E : n = m) :
  length (MM_cast P E) = length P.
Proof.
  destruct E. cbn. reflexivity.
Qed.

Lemma cast_eq_refl {X n} (v : Vector.t X n) E : cast v E = v.
Proof.
  induction v; cbn; congruence.
Qed.

Lemma fin_cast_eq_refl {n} (v : pos n) E : Fin.cast v E = v.
Proof.
  induction v; cbn; congruence.
Qed.

Lemma MM_cast_spec {n m} i (P : list (mm_instr (pos n))) (E : n = m) j v k w :
   sss.sss_output (@mm_sss _) (i, P) (j, v) (k, w) <-> sss.sss_output (@mm_sss _) (i, MM_cast P E) (j, Vector.cast v E) (k, Vector.cast w E).
Proof.
  destruct E. cbn. now rewrite !cast_eq_refl.
Qed.

Lemma MM_cast_terminates {n m} i (P : list (mm_instr (pos n))) (E : n = m) j v :
   sss.sss_terminates (@mm_sss _) (i, P) (j, v) <-> sss.sss_terminates (@mm_sss _) (i, MM_cast P E) (j, Vector.cast v E).
Proof.
  destruct E. cbn. now rewrite !cast_eq_refl.
Qed.

Local Notation "P '/MM/' s '~~>' t" := (sss.sss_output (@mm_sss _) P s t) (at level 70, no associativity).
Local Notation "P '/MM/' s '~~>' t" := (sss.sss_output (@mm_sss _) P s t) (at level 70, no associativity).

Local Notation "e #> x" := (vec_pos e x).
Local Notation "e [ v / x ]" := (vec_change e x v).

Lemma vec_app_spec {X n m} (v : Vector.t X n) (w : Vector.t X m) :
  vec_app v w = Vector.append v w.
Proof.
  induction v.
  - cbn. eapply vec_pos_ext. intros. now rewrite vec_pos_set.
  - rewrite vec_app_cons. cbn. congruence.
Qed.

Lemma vec_map_spec {X Y n} (v : Vector.t X n) (f : X -> Y) :
  vec_map f v = Vector.map f v.
Proof.
  induction v; cbn; congruence.
Qed.

Lemma vec_change_swap [X] [n] (v : vec X n) (p : pos n) (q : pos n) x y :
p <> q ->
v[x / p][y / q] = v [y / q][x / p].
Proof.
  intros Hnew. eapply vec_pos_ext. intros r.
  destruct (pos_eq_dec q r).
  - subst. rewrite vec_change_eq, vec_change_neq, vec_change_eq; congruence.
  - destruct (pos_eq_dec p r).
    + subst. rewrite vec_change_neq, vec_change_eq, vec_change_eq; congruence.
    + rewrite !vec_change_neq; congruence.
Qed.

Lemma pos_left_inj {n m} p q :
  @pos_left n m p = @pos_left n m q -> p = q.
Proof.
  induction p in q |- *; cbn in *.
  - eapply (Fin.caseS' q).
    + reflexivity.
    + clear q. cbn. congruence.
  - eapply (Fin.caseS' q).
    + cbn. congruence.
    + clear q. cbn. intros. f_equal. eapply IHp.
      now eapply pos_nxt_inj.
Qed.

Lemma pos_right_inj {n m} p q :
  @pos_right n m p = @pos_right n m q -> p = q.
Proof.
  induction n in p, q |- *; cbn in *.
  - eauto.
  - intros. eapply IHn, pos_nxt_inj, H.
Qed.

Lemma pos_right_left {n m} p q :
  @pos_left n m p <> @pos_right n m q.
Proof.
  induction n; cbn.
  - inversion p.
  - eapply (Fin.caseS' p).
    + cbn. congruence.
    + cbn. intros ? ? % pos_nxt_inj. firstorder.
Qed.

Lemma cast_vec_pos { X n m} (v : Vector.t X n) (E : n = m) p :
  cast v E #> p = v #> Fin.cast p (eq_sym E).
Proof.
  destruct E. cbn. now rewrite cast_eq_refl, fin_cast_eq_refl.
Qed.

Lemma cast_ext { X n m} (v1 v2 : Vector.t X n) (E1 E2 : n = m) :
  v1 = v2 ->
  cast v1 E1 = cast v2 E2.
Proof.
  intros ->.
  destruct E1. cbn. now rewrite !cast_eq_refl.
Qed.

Lemma nth_error_vec_list {X n} (v : Vector.t X n) m (H : m < n) x :
  nth_error (vec_list v) m = Some x ->
  v #> Fin.of_nat_lt H = x.
Proof.
  induction v in m , H |- *; cbn.
  - lia.
  - destruct m; cbn.
    + congruence.
    + eapply IHv.
Qed.

Lemma vec_list_inj {X n} (v w : Vector.t X n) :
  vec_list v = vec_list w -> v = w.
Proof.
  induction v in w |- *.
  - pattern w. revert w. eapply Vector.case0. reflexivity.
  - eapply (Vector.caseS' w). clear w. intros y w. cbn.
    intros [= ->]. f_equal. eauto.
Qed.

Lemma vec_list_vec_app {X n m} (v : Vector.t X n) (w : Vector.t X m) :
  vec_list (vec_app v w) = vec_list v ++ vec_list w.
Proof.
  rewrite ! vec_app_spec.
  induction v in w |- *.
  - cbn. reflexivity.
  - cbn. f_equal. eauto.
Qed.

Fixpoint update {X} (n : nat) (l : list X) y :=
  match l, n with
  | nil, _ => nil
  | x :: l, 0 => y :: l
  | x :: l, S n => x :: update n l y
  end.

Lemma vec_list_vec_change {X n} (v : Vector.t X n) (x : X) (p : pos n) :
  vec_list (vec_change v p x) = update (proj1_sig (Fin.to_nat p)) (vec_list v) x.
Proof.
  induction v; cbn.
  - inversion p.
  - eapply (Fin.caseS' p); cbn.
    + cbn. reflexivity.
    + intros. specialize (IHv p0). destruct (Fin.to_nat p0) eqn:E. cbn in *. now f_equal.
Qed.

Lemma vec_list_cast {X n} (v :Vector.t X n) m (E : n = m) :
 vec_list (cast v E) = vec_list v.
Proof.
  destruct E. now rewrite cast_eq_refl.
Qed.

Lemma vector_inv_back {X n} (v : Vector.t X (S n)) E :
  { '(x, v') : X * Vector.t X n | v = Vector.cast (append v' (x ## vec_nil)) E }.
Proof.
  destruct E.
  destruct (splitat n v) eqn:E.
  eexists (vec_head t0, t).
  erewrite <- append_splitat. 1: now rewrite cast_eq_refl.
  rewrite E. f_equal. eapply (Vector.caseS' t0). cbn.
  intros h. eapply Vector.case0. reflexivity.
Qed.

Lemma pos_left_spec {m n} p :
  @pos_left m n p = Fin.L n p.
Proof.
  induction p; cbn; congruence.
Qed.

Lemma pos_right_spec {m n} p :
  @pos_right m n p = Fin.R m p.
Proof.
  induction m; cbn; congruence.
Qed.

Lemma update_app_right {X} (x : X) l1 l2 i :
  i >= length l1 ->
  update i (l1 ++ l2) x = l1 ++ update (i - length l1) l2 x.
Proof.
  induction l1 in i |- *; cbn.
  - now rewrite Nat.sub_0_r.
  - intros Hi. destruct i. 1: lia.
    cbn. rewrite IHl1. 1: reflexivity. lia.
Qed.

Lemma update_app_left {X} (x : X) l1 l2 i :
  i < length l1 ->
  update i (l1 ++ l2) x = update i l1 x ++ l2.
Proof.
  induction l1 in i |- *; cbn.
  - lia.
  - intros Hi. destruct i; cbn.
    + reflexivity.
    + rewrite IHl1. 1: reflexivity. lia.
Qed.

Lemma vec_list_const {X x n} : vec_list (@const X x n) = List.repeat x n.
Proof. induction n; cbn; congruence. Qed.

Section preprocess.

  Variables k n : nat.

  Notation reg p := (@pos_left (1 + k + n) 3 (pos_left n (pos_right 1 p))).
  Notation tmp p := (@pos_right (1 + k + n) 3 p).

  Lemma tmp0_tmp1 : tmp pos0 <> tmp pos1. Proof. intros H % pos_right_inj. congruence. Qed.
  Lemma tmp0_tmp2 : tmp pos0 <> tmp pos2. Proof. intros H % pos_right_inj. congruence. Qed.
  Lemma tmp2_tmp0 : tmp pos2 <> tmp pos0. Proof. intros H % pos_right_inj. congruence. Qed.
  Lemma tmp1_tmp2 : tmp pos1 <> tmp pos2. Proof. intros H % pos_right_inj % pos_nxt_inj. congruence.  Qed.

  Lemma tmp_tgt p : tmp p <> pos0. Proof. cbn. congruence. Qed.

  Lemma tmp_reg p q : tmp p <> reg q. Proof. cbn. intros H % pos_nxt_inj. eapply pos_right_left. now rewrite H. Qed.

  Lemma tgt_reg p : reg p <> pos0. Proof. cbn. congruence. Qed.

  Lemma reg_inj p q : reg p = reg q -> p = q. Proof. cbn. now intros ? % pos_nxt_inj % pos_left_inj % pos_left_inj. Qed.

  Hint Resolve tmp0_tmp1 tmp0_tmp1 tmp2_tmp0 tmp1_tmp2 tmp_tgt tmp_reg tgt_reg reg_inj : core.

  Section prep.

  Import ListNotations.

  Definition prep (p : pos k) (i : nat) : list (mm_instr (pos (1 + k + n + 3))) :=
  (* i: *)    mm_transfert (reg p) pos0 (tmp pos0) i ++
  (* i+3: *) [INC (reg p)] ++
  (* i+4: *) [DEC Fin.F1 (14 + i)] ++
  (* i+5 *)   mm_push_One (reg p) (tmp pos0) (tmp pos1) (5+i) ++
  (* i+13: *)[DEC (tmp pos0) (4 + i) ].

  End prep.

  Lemma prep_length p i : length (prep p i) = 14. Proof. reflexivity. Qed.

  Lemma prep_spec (p : pos k) v i np :
    v #> pos0 = 0 ->
    v #> tmp pos0 = 0 ->
    v #> tmp pos1 = 0 ->
    v #> reg p = np ->
    (i, prep p i) /MM/ (i, v) ~~> (14 + i, v [ (stack_enc (List.repeat true (v #> reg p))) / reg p]).
  Proof.
    intros Htgt Htmp1 Htmp2 Hnp. unfold prep.
    split. 2:{ cbn. lia. }
    eapply sss_compute_trans.
    { eapply subcode_sss_compute with (P := (i,mm_transfert (reg p) (pos0) (pos_right (1 + k + n) Fin.F1) i)). 1: auto.
      eapply sss_progress_compute. eapply mm_transfert_progress; auto. }
    mm sss INC with (pos_left 3 (pos_left n (pos_right 1 p))). 1: replace (3 + i) with (i + 3) by lia. 1: auto.
    rew vec. replace (1 + (3 + i)) with (4 + i) by lia.
    rewrite vec_change_swap.
    1: rewrite vec_change_idem.
    1: pose (npm := 0).
    1: match goal with [ |- context [vec_change ?v ?x 1]] => change (vec_change v x 1) with (vec_change v x (stack_enc (repeat true npm))) end.
    1: assert (np = np + npm) by lia.
    1: rewrite Hnp. 1: revert Hnp. 1: revert H. 2:auto.
    generalize np at 2 4. generalize npm. intros npr npl Heq Hnp.
    induction npl in npr, np, Heq, Hnp |- *.
    - eapply sss_compute_trans.
      { eapply subcode_sss_compute with (P := (i+4, DEC Fin.F1 (14 + i) :: List.nil)). 1: auto.
        mm sss DEC zero with pos0 (14 + i). 1: replace (4 + i) with (i + 4) by lia. 1: eapply subcode_refl. 1: rew vec. fold plus.
        mm sss stop. }
      mm sss stop. f_equal. cbn.
      rewrite vec_change_swap. 2:congruence.
      match goal with [ |- context [@vec_change ?X ?n ?vv ?x 0]] => replace (@vec_change X n vv x 0) with (vec_change vv x (v#>pos0)) end.
      2: now rewrite Htgt. rewrite vec_change_same. subst. reflexivity.
    - eapply sss_compute_trans.
      { eapply subcode_sss_compute with (P := (i+4, DEC Fin.F1 (14 + i) :: List.nil)). 1: auto.
        mm sss DEC S with pos0 (14 + i) npl. 1:  replace (4 + i) with (i + 4) by lia. 1: eapply subcode_refl. 1:  rew vec. fold plus.
        mm sss stop. }
      rew vec.
      eapply sss_compute_trans.
      { eapply subcode_sss_compute with (P := (5 + i, mm_push_One (pos_left 3 (pos_left n (pos_right 1 p))) (pos_right (1 + k + n) pos0) (pos_right (1 + k + n) pos1) (5+i))).
        1: replace (5 + i) with (i + 5) at 1 by lia; auto.
        eapply sss_progress_compute. eapply mm_push_One_progress; rew vec.
        - rewrite vec_change_neq; eauto.
        - rewrite vec_change_neq; eauto. }
      mm sss DEC zero with (pos_right (1 + k + n) Fin.F1) (4 + i).
      1: replace (8 + (1 + (4 + i))) with (i + 13) by lia.  1: auto.
      1: rewrite vec_change_neq. 2:auto. 1:  rewrite vec_change_neq. 2:auto.
      1: rewrite vec_change_neq. 2:auto. 1:  eauto.
      rewrite vec_change_swap. 2:auto. rewrite vec_change_idem.
      change (true :: repeat true npr) with (repeat true (S npr)). eapply IHnpl.
      1: lia. assumption.
  Qed.

  Fixpoint PREP' (k' : nat) (H : k' <= k) (i : nat) : list (mm_instr (pos (1 + k + n + 3))).
  Proof.
    destruct k'.
    - exact List.nil.
    - refine (List.app (PREP' k' _ i) _).  1: abstract lia.
      assert (Hn : k' < k) by abstract lia.
      refine (prep (Fin.of_nat_lt Hn) (14 * k' + i)).
  Defined.

  Lemma PREP'_length k' H i : length (@PREP' k' H i) = k' * 14.
  Proof.
    induction k' in i, H |- *; cbn.
    - reflexivity.
    - autorewrite with list. rewrite IHk'. cbn. lia.
  Qed.

  Definition PREP (i : nat) : list (mm_instr (pos (1 + k + n + 3))). refine (@PREP' k _ i). abstract lia. Defined.

  Lemma PREP_length i : length (PREP i) = k * 14. Proof. eapply PREP'_length. Qed.
  Hint Resolve PREP_length : core.

  Lemma PREP_spec_strong i x w k'' k' v1 v2 v :
    forall E : k'' + k' = k,
    v = (Vector.cast (Vector.append v1 v2) E) ->
    x = 0 ->
    forall H,
    (i, PREP' k'' H i) /MM/ (i, Vector.append (Vector.append (x ## v) w) (0 ## 0 ## 0 ## vec_nil)) ~~>
    (i + (k'' * 14), Vector.append (Vector.append (x ## (Vector.cast (Vector.append (Vector.map (fun n => stack_enc (List.repeat true n)) v1) v2) E)) w) (0 ## 0 ## 0 ## vec_nil)).
  Proof.
    intros E -> -> Hle.
    split. 2:{ cbn. rewrite PREP'_length. right. lia. }
    revert i v1 k' Hle E v2.
    induction k'' as [ | k'' ]; intros i v1 k' Hle E v2.
    - cbn. mm sss stop. f_equal. 1:  lia. revert v1. eapply Vector.case0. cbn. reflexivity.
    - cbn [PREP'].
      edestruct (vector_inv_back v1) as [(x, v1l) Hv1].
      assert (H1 : k'' <= k) by lia.
      assert (H2 : k'' + S k' = k) by lia.
      specialize (IHk'' i v1l (S k') (PREP'_subproof k'' Hle) H2 (x ## v2)).
      eapply subcode_sss_compute_trans with (P := (i, PREP' k'' (PREP'_subproof k'' Hle) i)).  1: auto.
      1: match type of IHk'' with sss_compute _ _ (_, ?st) _ => evar (Vector.t nat (1 + k + n + 3)); enough (Eq : st = t) end; subst t.
      1: rewrite Eq in IHk''. 1:  eapply IHk''.
      { rewrite Hv1. repeat f_equal.
        eapply vec_list_inj. rewrite !vec_list_cast, <- !vec_app_spec, !vec_list_vec_app.
        rewrite vec_list_cast. rewrite vec_list_vec_app. cbn. now rewrite <- app_assoc.
      }
      replace (14 * k'' + i) with (i + k'' * 14) by lia.
      eapply subcode_sss_compute_trans with (P := (i + k'' * 14, prep (Fin.of_nat_lt (PREP'_subproof0 k'' Hle)) (i + k'' * 14))).
      { eexists. eexists. split.  1: reflexivity. rewrite PREP'_length. lia. }
      1: eapply prep_spec.
      + reflexivity.
      + cbn. rewrite <- !vec_app_spec. rewrite vec_pos_app_right. reflexivity.
      + cbn. rewrite <- !vec_app_spec. rewrite vec_pos_app_right. reflexivity.
      + cbn. rewrite <- !vec_app_spec. rewrite !vec_pos_app_left. reflexivity.
      + mm sss stop. f_equal. 1:lia.
        rewrite <- !vec_app_spec.
        eapply vec_list_inj.

        rewrite vec_list_vec_change.
        rewrite !(@vec_list_vec_app nat (1 + k + n) 3).
        rewrite !vec_list_vec_app. cbn [vec_list].
        rewrite !vec_list_cast.
        rewrite !vec_list_vec_app. cbn [vec_list].
        rewrite !vec_list_vec_map. rewrite Hv1. rewrite vec_list_cast.
        rewrite <- !vec_app_spec.
        rewrite !vec_list_vec_app. cbn [vec_list].
        clear. fold plus.
        rewrite pos_left_spec. pose proof (@Fin.L_sanity (S (k + n)) 3). cbn in H. rewrite H. clear H.
        rewrite pos_left_spec. pose proof (@Fin.L_sanity (S (k)) n). cbn in H. rewrite H. clear H.
        rewrite pos_right_spec. pose proof (@Fin.R_sanity k 1 ). cbn [plus] in H. rewrite H. clear H.
        rewrite Fin.to_nat_of_nat. cbn [proj1_sig update app]. f_equal.
        rewrite map_app. cbn [map].
        rewrite <- !pos_left_spec.
        rewrite update_app_left. 2:{ simpl_list. rewrite vec_list_length. cbn. lia. }
        rewrite update_app_left. 2:{ simpl_list. rewrite vec_list_length. cbn. lia. }
        rewrite update_app_right. 2:{ simpl_list. rewrite vec_list_length. cbn. lia. }
        simpl_list. rewrite vec_list_length. rewrite Nat.sub_diag. cbn [update].
        f_equal. f_equal.
        rewrite <- !app_assoc. f_equal.
        cbn [app]. f_equal. f_equal. f_equal.
        rewrite (@vec_pos_app_left nat (add (S k) n) 3).
        rewrite <- pos_left_spec.
        rewrite (@vec_pos_app_left nat (S k) n).
        rewrite <- pos_right_spec.
        cbn [pos_right]. cbn.
        eapply nth_error_vec_list.
        rewrite vec_list_cast, !vec_list_vec_app.
        rewrite nth_error_app2; rewrite vec_list_length. 2: lia.
        rewrite Nat.sub_diag. reflexivity.
        Unshelve. lia.
  Qed.

  Lemma myeq m : m + 0 = m.
  Proof.
    induction m.
    - reflexivity.
    - cbn. rewrite IHm. reflexivity.
  Defined.

  Lemma PREP_spec i v w :
      (i, PREP i) /MM/ (i, Vector.append (Vector.append (0 ## v) w) (0 ## 0 ## 0 ## vec_nil)) ~~> (i + (k * 14), Vector.append (Vector.append (0 ## Vector.map (fun n => stack_enc (List.repeat true n)) v) w) (0 ## 0 ## 0 ## vec_nil)).
  Proof.
    unfold PREP.
    pose proof (@PREP_spec_strong i 0 w k 0 v vec_nil v (myeq k)).
    match goal with [ |- sss_output _ _ (_, ?st) _ ] => evar (Vector.t nat (1 + k + n + 3)); enough (st = t) as ->; subst t end.
    1: match goal with [ |- sss_output _ _ _ (_, ?st) ] => evar (Vector.t nat (1 + k + n + 3)); enough (st = t) as ->; subst t end.
    1: apply H; try reflexivity. 3: reflexivity.
    2:{ repeat f_equal. clear. induction k; cbn.
        - rewrite cast_eq_refl.
          pattern v. revert v. eapply Vector.case0. reflexivity.
        - eapply (Vector.caseS' v). clear v. intros x v. cbn.
        f_equal. rewrite IHn. eapply cast_ext. f_equal. eapply IHn.
    }
    clear. generalize (myeq k).
    induction v; intros E.
    - cbn. reflexivity.
    - cbn. f_equal. eapply IHv.
  Qed.

  Fixpoint PREPMORE' (n' : nat) (H : n' <= n) : list (mm_instr (pos (1 + k + n + 3))).
  Proof.
    destruct n'.
    - exact List.nil.
    - refine (List.app (PREPMORE' n' _) _).  1: abstract lia.
      assert (Hn : n' < n) by abstract lia.
      refine (INC (pos_left 3 (pos_right (1 + k) (Fin.of_nat_lt Hn))) :: List.nil).
  Defined.

  Lemma PREPMORE'_length (n' : nat) (H : n' <= n) : length (PREPMORE' n' H) = n'.
  Proof.
    induction n' in H |- *; cbn.
    - reflexivity.
    - simpl_list. rewrite IHn'. cbn. lia.
  Qed.

  Definition PREPMORE : list (mm_instr (pos (1 + k + n + 3))). refine (@PREPMORE' n _). abstract lia. Defined.

  Lemma PREPMORE'_spec i x (w : Vector.t nat k) n'' n' :
    forall E : n'' + n' = n,
    forall H,
    (i, PREPMORE' n'' H) /MM/ (i, Vector.append (Vector.append (x ## w) (Vector.const 0 n)) (0 ## 0 ## 0 ## vec_nil)) ~~>
    (i + n'', Vector.append (Vector.append (x ## w) (Vector.cast (Vector.append (Vector.const 1 n'') (Vector.const 0 n')) E)) (0 ## 0 ## 0 ## vec_nil)).
  Proof.
    intros E Hle.
    split. 2:{ cbn. rewrite PREPMORE'_length. lia. }
    revert n' E Hle.
    induction n''; intros n' E Hle.
    - cbn [PREPMORE']. mm sss stop. f_equal.  1: lia.  1: repeat f_equal. cbn. destruct E. now rewrite cast_eq_refl.
    - cbn [PREPMORE'].
      eapply subcode_sss_compute_trans with (P := (i, PREPMORE' n'' (PREPMORE'_subproof n'' Hle))).  1: auto.
      { eapply IHn''. }
      mm sss INC with (pos_left 3 (pos_right (1 + k) (Fin.of_nat_lt (PREPMORE'_subproof0 n'' Hle)))).
      { eexists. eexists. split.  1: reflexivity. now rewrite PREPMORE'_length. }
      mm sss stop. f_equal. 1: lia.
      rewrite <- !vec_app_spec.
      rewrite !vec_pos_app_left.
      rewrite !vec_pos_app_right.
      eapply vec_list_inj.
      rewrite vec_list_vec_change.
      rewrite !vec_list_vec_app.
      rewrite pos_left_spec.
      rewrite Fin.L_sanity.
      rewrite pos_right_spec.
      rewrite Fin.R_sanity.
      rewrite Fin.to_nat_of_nat. cbn [proj1_sig plus].
      rewrite update_app_left. 2:{ rewrite !app_length, !vec_list_length. lia. }
      f_equal.
      rewrite update_app_right. 2:{ cbn. rewrite !vec_list_length. lia. }
      f_equal. rewrite vec_list_length. replace (S (k + n'') - S k) with n'' by lia.
      rewrite !vec_list_cast.
      rewrite !vec_list_vec_app.
      rewrite update_app_right. 2:{ cbn. rewrite !vec_list_length. lia. }
      rewrite (@vec_list_vec_app nat (S n'') n').
      replace (S n'') with (n'' + 1) by lia.
      rewrite vec_list_length. rewrite Nat.sub_diag. instantiate (2 := 1 + n'). cbn.
      rewrite !vec_list_const. rewrite repeat_app. cbn. rewrite <- !app_assoc.
      f_equal. cbn. f_equal.
      f_equal.
      eapply nth_error_vec_list.
      rewrite vec_list_cast, !vec_list_vec_app; cbn.
      rewrite nth_error_app2. 2: rewrite vec_list_length; lia.
      now rewrite vec_list_length, Nat.sub_diag.
      Unshelve. lia.
  Qed.

  Lemma PREPMORE_spec i x (w : Vector.t nat k) :
    (i, PREPMORE) /MM/ (i, Vector.append (Vector.append (x ## w) (Vector.const 0 n)) (0 ## 0 ## 0 ## vec_nil)) ~~>
    (i + n, Vector.append (Vector.append (x ## w) (Vector.const 1 n)) (0 ## 0 ## 0 ## vec_nil)).
  Proof.
    pose proof (PREPMORE'_spec i x w n 0). cbn in H. cbn.
    match goal with [ |- sss_output _ _ _ (_, ?st) ] => evar (Vector.t nat (1 + k + n + 3)); enough (st = t) as ->; subst t end.
    1: eapply H. repeat f_equal.
    eapply vec_list_inj. rewrite vec_list_cast, vec_list_const, <- vec_app_spec, vec_list_vec_app, vec_list_const.
    now simpl_list.
    Unshelve. lia.
  Qed.

  Section POSTP.
  Import ListNotations.

  Definition POSTP (i : nat) : list (mm_instr (pos (1 + k + n + 3))) :=
(*     (*    i *) mm_transfert pos0 (tmp pos2) (tmp pos0) i ++
 *) (*    i *) mm_pop (tmp pos2) (tmp pos0) (tmp pos1) (i) (i+16) (i+16) (i+18) ++
    (* 16+i *)[INC pos0] ++
    (* 17+i *)[DEC (tmp pos0) (i)].

  End POSTP.

  Lemma POSTP_length i : length (POSTP i) = 18. Proof. reflexivity. Qed.
  Hint Resolve POSTP_length : core.
  Hint Rewrite POSTP_length : list.

  Lemma POSTP_spec_strong i v out out' :
     v #> pos0 = out' ->
     v #> tmp pos0 = 0 ->
     v #> tmp pos1 = 0 ->
     v #> tmp pos2 = stack_enc (List.repeat true out) ->
     (i, POSTP i) /MM/ (i, v) ~~> (i + 18, v [ (out + out') / Fin.F1 ] [ (stack_enc nil) / tmp pos2] ).
  Proof.
    intros Htgt Htmp0 Htmp1 Htmp2.
    split. 2:{ cbn. lia. }
    induction out in v, Htgt, Htmp0, Htmp1, Htmp2, out', Htgt, Htmp2 |- *.
    - cbn [repeat] in Htmp2.
      eapply subcode_sss_compute_trans with (P := (i,mm_pop (tmp pos2) (tmp pos0) (tmp pos1) (i) (i+16) (i+16) (i+18))). 1: unfold POSTP; auto.
      { eapply sss_progress_compute. eapply mm_pop_void_progress; eauto. }
      mm sss stop. f_equal. eapply vec_pos_ext. fold plus. intros p.
      eapply (Fin.caseS' p).
      + rewrite vec_change_neq; eauto. rewrite vec_change_eq; eauto.
      + clear p. apply pos_left_right_rect.
        * intros p. rewrite !vec_change_neq; try congruence. intros ? % pos_nxt_inj. fold pos_right in H. eapply pos_right_left. now rewrite H.
        * intros p. eapply (Fin.caseS' p); clear p.
          -- rewrite !vec_change_neq; try congruence. eapply tmp2_tmp0.
          -- intros p. eapply (Fin.caseS' p); clear p.
             ++ rewrite !vec_change_neq; try congruence. intros H. eapply tmp1_tmp2. cbn. rewrite <- H. reflexivity.
             ++ intros p. eapply (Fin.caseS' p); clear p.
               ** rewrite vec_change_eq. 2: reflexivity. eauto.
               ** eapply Fin.case0.
    - cbn [repeat] in Htmp2.
      eapply subcode_sss_compute_trans with (P := (i,mm_pop (tmp pos2) (tmp pos0) (tmp pos1) (i) (i+16) (i+16) (i+18))). 1: unfold POSTP; auto.
      { eapply sss_progress_compute. eapply mm_pop_One_progress; eauto. }
      mm sss INC with pos0.  1: unfold POSTP.  1: auto. fold plus in *.
      mm sss DEC zero with (tmp pos0) i.  1: unfold POSTP.  1: auto.
      {rew vec. rewrite vec_change_neq; eauto. }
      rew vec. specialize IHout with (out' := S out').
      replace (out + S out') with (S (out + out')) in IHout by lia.
      match goal with [ |- sss_compute _ _ _ (_, ?st) ] => evar (Vector.t nat (1 + k + n + 3)); enough (st = t) as ->; subst t end.
      1: eapply IHout; rew vec.
      + rewrite vec_change_neq; eauto.
      + rewrite vec_change_neq; eauto.
      + rew vec. symmetry. rewrite vec_change_swap. 2: eauto. rewrite vec_change_idem, vec_change_swap; eauto.
  Qed.

  Lemma POSTP_spec i v out :
     v #> pos0 = 0 ->
     v #> tmp pos0 = 0 ->
     v #> tmp pos1 = 0 ->
     v #> tmp pos2 = stack_enc (List.repeat true out) ->
     (i, POSTP i) /MM/ (i, v) ~~> (i + 18, v [ out / pos0] [ (stack_enc nil) / tmp pos2 ]).
  Proof.
    intros Htgt Htmp0 Htmp1 Htmp2.
    pose proof (POSTP_spec_strong i v out 0 Htgt Htmp0 Htmp1 Htmp2). rewrite NPeano.Nat.add_0_r in H.
    eapply H.
  Qed.

  Definition PREPALL i := PREP i ++ PREPMORE ++ INC pos0 :: List.nil.

  Lemma PREPALL_length i : length (PREPALL i) = k * 14 + n + 1.
  Proof. unfold PREPALL, PREPMORE; rewrite !app_length, PREP_length, PREPMORE'_length; cbn; lia. Qed.

  Lemma PREPALL_spec i v :
    (i, PREPALL i) /MM/ (i, Vector.append (Vector.append (0 ## v) (Vector.const 0 n)) (0 ## 0 ## 0 ## vec_nil)) ~~>
          (i + k * 14 + n + 1, Vector.append (Vector.append (stack_enc nil ## Vector.map (fun n => stack_enc (List.repeat true n)) v) (Vector.const (stack_enc nil) n)) (0 ## 0 ## 0 ## vec_nil)).
  Proof.
    split. 2: cbn; rewrite PREPALL_length; lia.
    eapply subcode_sss_compute_trans. 2: eapply PREP_spec. 1: unfold PREPALL; auto.
    eapply subcode_sss_compute_trans. 2: eapply PREPMORE_spec. 1: unfold PREPALL; auto.
    mm sss INC with pos0.
    { unfold PREPALL. eexists. eexists nil. cbn. split.  1: now rewrite app_assoc.
      rewrite app_length, PREP_length; unfold PREPMORE; rewrite PREPMORE'_length. lia. }
    fold plus. mm sss stop.
    f_equal. lia.
  Qed.

End preprocess.

Lemma cast_cast {n m} {E : n = m} {X} (v : Vector.t X n) (E2 : m = n) :
  cast (cast v E) E2 = v.
Proof.
  destruct E. now rewrite !cast_eq_refl.
Qed.

Definition cases {k i} : (forall p : pos (1 + k + i + 3),
{p = pos_right (1 + k + i) pos0} + {p = pos_right (1 + k + i) pos1} + {p = pos_right (1 + k + i) pos2} +
{q : pos (1 + k + i) | p = pos_left 3 q}).
Proof.
  apply pos_left_right_rect; [ eauto | ].
  intros p. eapply (Fin.caseS' p); [ eauto | ].
  intros p'. eapply (Fin.caseS' p'); [ eauto | ].
  intros p''. eapply (Fin.caseS' p''); [ eauto | ].
  eapply Fin.case0.
Defined.

Lemma vec_pos_const {k} {X x} (p : pos k) : @const X x k #> p = x.
Proof.
  induction p; cbn; eauto.
Qed.

Lemma BSM_computable_to_MM_computable {k} (R : Vector.t nat k -> nat -> Prop) :
  BSM_computable R -> MM_computable R.
Proof.
  intros (i & n & P & HP1 & HP2) % BSM_computable_iff. eapply MM_computable_iff.
  unshelve epose proof (@bsm_mm_compiler_strong (1 + k + i) n P (pos_right _ Fin.F1) (pos_right _ (Fin.FS Fin.F1)) (pos_right _ (pos2)) (pos_left _) (1 + length (PREPALL k i 1)) _ _ _ _ ) as [Q HQ].
  - eapply tmp0_tmp1.
  - intros p. intros H. eapply  pos_right_left. now rewrite H.
  - intros.  intros H. eapply  pos_right_left. now rewrite H.
  - now intros ? ? ? % pos_left_inj.
  - exact cases.
  - intros ? % pos_right_inj; congruence.
  - intros ? % pos_right_inj % pos_nxt_inj. congruence.
  - intros p. intros H. eapply  pos_right_left. now rewrite H.
  - exists (i + 3).   assert (E : 1 + k + i + 3 = (1 + k) + (i + 3)) by lia.
    pose (q' := PREPALL k i 1 ++ Q ++ mm_transfert pos0 (pos_right (1 + k + i) pos2) (pos_right (1 + k + i) pos0) (1 + length (PREPALL k i 1) + length Q) ++ POSTP k i (4 + length (PREPALL k i 1) + length Q)).
    assert (Eq1 : forall v, cast (append (append (0 ## v) (const 0 i)) (const 0 3)) E = append (0 ## v) (const 0 (i + 3))).
      { intros v. clear. cbn.
        f_equal. match goal with [ |- context [@f_equal ?A ?B ?f ?x ?y ?e]] => generalize (@f_equal A B f x y e) end. clear.
        induction v; cbn; intros E.
        - induction i in E |- *; cbn.
          + reflexivity.
          + now rewrite IHi.
        - f_equal. now rewrite IHv.
      }
    exists (MM_cast q' E). fold plus. split.
    + intros v m. intros ? % HP1.
      setoid_rewrite eval_iff.
      destruct H as (c & v' & H % BSM_sss.eval_iff). fold plus in *.
      eapply HQ in H.
      eexists. eexists ?[v']. rewrite <- Eq1.
      unshelve eassert (Eq2 : forall v' : Vector.t nat (k + (i + 3)), m ## v' = cast (m ## _) E).
      { fold plus. refine (Vector.cast v' _). abstract lia. }
      { clear. intros v. cbn. f_equal.
        match goal with [ |- context [@f_equal ?A ?B ?f ?x ?y ?e]] => generalize (@f_equal A B f x y e) end. fold plus.
        intros E2. generalize (BSM_computable_to_MM_computable_subproof k i E).
        clear. intros E1. cbn in *. revert v E1 E2. generalize (k + i + 2).  generalize (k + (i + 2)). clear. intros.
        destruct E1. now rewrite !cast_eq_refl.
      }
      rewrite Eq2.
      instantiate (v' := (cast _ _)).
      rewrite <- @MM_cast_spec. subst q'.
      split.
      1: { eapply subcode_sss_compute_trans. 2: eapply PREPALL_spec. 1: auto.
      match goal with [H : sss_output _  _ ?st1 _ |- sss_compute _ _ ?st2 _ ] => enough (st1 = st2) end.
      1: rewrite H0 in H.
      1: eapply subcode_sss_compute_trans. 2: eapply H.  1: auto.
      2:{ f_equal.  1: rewrite PREPALL_length.  1: lia. clear.
          eapply vec_pos_ext. intros p.
          unfold vec_enc. rewrite vec_pos_set. destruct (cases p) as [ [[-> | ->] | ->] | [q ->]].
          - cbn. rewrite <- !vec_app_spec. now rewrite vec_pos_app_right.
          - cbn. rewrite <- !vec_app_spec. now rewrite vec_pos_app_right.
          - cbn. rewrite <- !vec_app_spec. now rewrite vec_pos_app_right.
          - rewrite <- !vec_app_spec. rewrite vec_pos_app_left.
            revert q. eapply pos_left_right_rect.
            + intros p. rewrite !vec_pos_app_left.
              rewrite <- !vec_map_spec. eapply (Fin.caseS' p).
              * cbn. reflexivity.
              * cbn. intros. rewrite !vec_pos_map. reflexivity.
            + intros p. rewrite !vec_pos_app_right.
              now rewrite !vec_pos_const.
      }
      eapply subcode_sss_compute_trans with (P := (1 + length (PREPALL k i 1) + length Q, mm_transfert pos0 (pos_right (1 + k + i) pos2) (pos_right (1 + k + i) pos0) (1 + length (PREPALL k i 1) + length Q))).
      { eexists (PREPALL k i 1 ++ Q). eexists (POSTP _ _ _). split. 1:  now rewrite <- app_assoc. rewrite !app_length, PREPALL_length. lia. }
      1: eapply sss_progress_compute.  1: eapply mm_transfert_progress.
      1-5: clear.
      { cbn. congruence. }
      { cbn. congruence. }
      { cbn. intros ? % pos_nxt_inj % pos_right_inj. congruence. }
      { unfold vec_enc. rewrite vec_pos_set.
        destruct cases as [ [ [| ] | ] | [q Hq]]; rew vec.
        exfalso. eapply pos_right_left. now rewrite Hq. }
      { unfold vec_enc. rewrite vec_pos_set.
        destruct cases as [ [ [| ] | ] | [q Hq]]; rew vec.
        exfalso. eapply pos_right_left. now rewrite Hq. }
      { reflexivity. }
      eapply subcode_sss_compute_trans with (P := (4 + length (PREPALL k i 1) + length Q, POSTP k i (4 + length (PREPALL k i 1) + length Q))).
      { eexists _. eexists List.nil. split.  1: rewrite app_nil_r.  1: now rewrite !app_assoc. rewrite !app_length, PREPALL_length. cbn. lia. }
      1: eapply POSTP_spec.
      { unfold vec_enc. rewrite vec_pos_set. destruct cases as [ [ | ] | [q Hq]]; rew vec. }
      { unfold vec_enc. rewrite !vec_pos_set.
        destruct cases as [ [ [| ] | ] | [q Hq]]; rew vec.
        all: try now (cbn in e; congruence).
        revert Hq. eapply (Fin.caseS' q).
        all: try now (cbn; congruence).
        intros _. rewrite vec_change_neq. 2: intros ? % pos_right_inj; congruence.
        rewrite vec_change_neq. 2: cbn; congruence.
        rewrite vec_pos_set.
        destruct cases as [ [ [| ] | ] | [q' Hq']]; rew vec.
        exfalso. eapply pos_right_left. now rewrite Hq'. }
      {  unfold vec_enc. rewrite !vec_pos_set.
         destruct cases as [ [ [| ] | ] | [q Hq]]; rew vec.
         { rewrite vec_pos_set. destruct cases as [ [ [| ] | ] | [q' Hq']]; rew vec.
         exfalso. eapply pos_right_left. now rewrite Hq'. }
         { rewrite vec_pos_set. destruct cases as [ [ [| ] | ] | [q' Hq']]; rew vec.
         exfalso. eapply pos_right_left. now rewrite Hq'. }
         { rewrite vec_change_neq. 2: intros ? % pos_right_inj % pos_nxt_inj; congruence.
           rewrite vec_change_neq. 2: cbn; congruence.
           rewrite vec_pos_set.
           destruct cases as [ [ [| ] | ] | [q' Hq']]; rew vec.
           exfalso. eapply pos_right_left. now rewrite Hq'. }
      }
      2:{  fold plus.
      mm sss stop. cbn. f_equal.
      rewrite cast_cast.
      reflexivity.
      }
      {  unfold vec_enc. rewrite !vec_pos_set. destruct cases as [ [ [| ] | ] | [q' Hq']]; rew vec.
         all: try now (cbn in e; congruence).
         revert Hq'. eapply (Fin.caseS' q').
         all: try now (cbn; congruence). }
      Unshelve. lia.
      }
      cbn. autorewrite with list. cbn. setoid_rewrite PREPALL_length. right. lia.
    + intros v H2.
      eapply HP2. eapply HQ. eapply MM_cast_terminates with (E := E).
      eapply subcode_sss_terminates.
      2:{ eapply subcode_sss_terminates_inv.  1: eapply mm_sss_fun.
      1: eapply H2.
          2:{rewrite <- Eq1. rewrite <- MM_cast_spec.
             rewrite PREPALL_length. cbn [plus].
             match goal with [ |- sss_output _ _ _ (_, ?st) ] => evar (t : Vector.t nat (1 + k + i + 3)); enough (Eq : st = t) end; subst t.
             1: rewrite Eq.  1: eapply PREPALL_spec.

             clear.
          eapply vec_pos_ext. intros p.
          unfold vec_enc. rewrite vec_pos_set. destruct (cases p) as [ [[-> | ->] | ->] | [q ->]].
          - cbn. rewrite <- !vec_app_spec. now rewrite vec_pos_app_right.
          - cbn. rewrite <- !vec_app_spec. now rewrite vec_pos_app_right.
          - cbn. rewrite <- !vec_app_spec. now rewrite vec_pos_app_right.
          - rewrite <- !vec_app_spec. rewrite vec_pos_app_left.
            revert q. eapply pos_left_right_rect.
            + intros p. repeat setoid_rewrite vec_pos_app_left.
              repeat setoid_rewrite <- vec_map_spec. eapply (Fin.caseS' p).
              * cbn. reflexivity.
              * intros. repeat setoid_rewrite vec_pos_map.
                f_equal. rewrite (@vec_pos_app_left (list bool) (1 + k) i).
                cbn. rewrite vec_pos_map. reflexivity.
            + intros p. rewrite !vec_pos_app_right.
              rewrite (@vec_pos_app_right (list bool) (S k) i).
              now rewrite !vec_pos_const.
          }

      clear. subst q'. generalize (PREPALL k i 1).
      intros l.
      generalize (mm_transfert pos0 (pos_right (1 + k + i) pos2) (pos_right (1 + k + i) pos0) (1 + length l + length Q) ++ POSTP k i (4 + length l + length Q)).
      fold plus. revert l. destruct E. cbn. intros. exists nil. cbn. eauto.
      }

      clear. subst q'.
      generalize (PREPALL k i 1).
      intros l.
      generalize (mm_transfert pos0 (pos_right (1 + k + i) pos2) (pos_right (1 + k + i) pos0) (1 + length l + length Q) ++ POSTP k i (4 + length l + length Q)).
      fold plus. revert l. destruct E. cbn. intros. exists l. cbn. eauto.
Qed.

author: uds-psl

repo: coq-library-undecidability


text:
Require Import Coq.Arith.EqNat.
Require Import Coq.Bool.Bool.
Require Import FunctionalExtensionality.
Require Import List.
Require Import FJ_tactics.
Require Import Functors.
Require Import MonadLib.
Require Import Names.
Require Import PNames.
Require Import EffPure.

Section EffReader.

  Variable D : Set -> Set.
  Context {Fun_D : Functor D}.
  Let DType := DType D.

  Context {eq_DType_DT : forall T, FAlgebra eq_DTypeName T (eq_DTypeR D) D}.

  Variable F : Set -> Set -> Set.
  Context {Fun_F : forall A, Functor (F A)}.
  Let Exp (A : Set) := Exp (F A).

  Variable MT : Set -> Set.
  Context {Fun_MT : Functor MT}.
  Context {Mon_MT : Monad MT}.
  Context {Fail_MT : FailMonad MT}.
  Context {Inj_MT : InjMonad MT}.
  Context {Reasonable_MT : Reasonable_Monad MT}.
  Context {MT_eq_dec : forall (A : Set) (mta : MT A),
    {exists a, mta = return_ a} + {mta = fail}}.

  Variable V : Set -> Set.
  Context {Fun_V : Functor V}.
  Let Value := Value V.

  Variable (ME : Set -> Set). (* Evaluation Monad. *)
  Context {Fun_ME : Functor ME}.
  Context {Mon_ME : Monad ME}.
  Context {Fail_ME : FailMonad ME}.
  Context {Environment_ME : Environment ME (Env Value)}.

  Context {eval_F : FAlgebra EvalName (Exp nat) (evalR V) (F nat)}.
  Context {evalM_F : FAlgebra EvalName (Exp nat) (evalMR V ME) (F nat)}.

  Variable EQV_E : forall A B, (eqv_i F A B -> Prop) -> eqv_i F A B -> Prop.
  Let E_eqv A B := iFix (EQV_E A B).
  Let E_eqvC {A B : Set} gamma gamma' e e' :=
    E_eqv _ _ (mk_eqv_i _ A B gamma gamma' e e').
  Context {funEQV_E : forall A B, iFunctor (EQV_E A B)}.
  Context {Typeof_F : forall T, FAlgebra TypeofName T (typeofR D MT) (F DType)}.

  Section WFValue_Sec.

    Variable TypContext : Set.
    Context {TypContextCE : ConsExtensionC TypContext}.
    Context {GammaTypContext : GammaTypContextC D TypContext}.
    Context {TypContext_GCE : GammaConsExtensionC D TypContext _ _}.

    Variable WFV : (WFValue_i D V TypContext -> Prop) -> WFValue_i D V TypContext -> Prop.
    Context {funWFV : iFunctor WFV}.

    (* ============================================== *)
    (* WELL-FORMED MONADIC STATE VALUES               *)
    (* ============================================== *)

    Variable WFVM : (WFValueM_i D V MT ME TypContext -> Prop) -> WFValueM_i D V MT ME TypContext -> Prop.
    Let WFValueM := iFix WFVM.
    Let WFValueMC Sigma v T:= WFValueM (mk_WFValueM_i D V MT ME _ Sigma v T).

    Inductive WFValueM_Environment (A : WFValueM_i D V MT ME TypContext -> Prop) : WFValueM_i D V MT ME TypContext -> Prop :=
    | WFVM_Ask : forall Sigma (k : list Value -> ME Value) T,
      (forall env, WF_EnvG _ _ _ WFV env Sigma ->
        A (mk_WFValueM_i D V MT ME _ Sigma (k env) T)) ->
      WFValueM_Environment A (mk_WFValueM_i D V MT ME _ Sigma (do env <- ask; k env) T)
    | WFVM_Local : forall Sigma Gamma' f m k T' T,
      (* Local Changes are keep the environment well-formed in some Gamma'. *)
      (*ConsExtension (ConsExtensionC := TypContextCE') Sigma' Sigma -> *)
      (forall env, WF_EnvG _ V _ WFV env Sigma -> WF_EnvG _ V _ WFV (f env) (GammaSet _ Sigma Gamma')) ->
      (* The body of the local update is well-formed in the new environment *)
      (A (mk_WFValueM_i _ _ _ _ _ (GammaSet _ Sigma Gamma') m (return_ T'))) ->
      (* In any conservative extension of Sigma, the body of the bind
         is well-formed. *)
      (forall Sigma' v,
        ConsExtension Sigma' Sigma ->
        WFValueC _ _ _ WFV Sigma' v T' ->
        A (mk_WFValueM_i D V MT ME _ Sigma' (k v) T)) ->
      WFValueM_Environment A (mk_WFValueM_i _ _ _ _ _ Sigma (local f m >>= k) T).

    Definition ind_alg_WFVM_Environment (P : WFValueM_i D V MT ME TypContext -> Prop)
      (H_Ask : forall Sigma (k : list Value -> ME Value) T,
      (forall env, WF_EnvG _ _ _ _  env Sigma ->
        P (mk_WFValueM_i D V MT ME _ Sigma (k env) T)) ->
      P (mk_WFValueM_i D V MT ME _ Sigma (do env <- ask; k env) T))
      (H_Local : forall Sigma Gamma' f m k T' T,
        (* ConsExtension (ConsExtensionC := TypContextCE') Sigma' Sigma ->*)
      (forall env, WF_EnvG _ _ _ WFV env Sigma -> WF_EnvG _ _ _ WFV (f env) (GammaSet _ Sigma Gamma')) ->
      (P (mk_WFValueM_i _ _ _ _ _ (GammaSet _ Sigma Gamma') m (return_ T'))) ->
      (forall Sigma' v,
        ConsExtension Sigma' Sigma ->
        WFValueC _ _ _ WFV Sigma' v T' ->
        P (mk_WFValueM_i D V MT ME _ Sigma' (k v) T)) ->
      P (mk_WFValueM_i _ _ _ _ _ Sigma (local f m >>= k) T))
      (i : WFValueM_i D V MT ME _)
      (e : WFValueM_Environment P i)
      :
      P i :=
      match e in WFValueM_Environment _ i return P i with
        | WFVM_Ask Sigma k T WF_k =>
          H_Ask Sigma k T WF_k
        | WFVM_Local Sigma Gamma' f m k T' T (*Sub_Sig'_Sig *) WF_env WF_m WF_k =>
          H_Local Sigma Gamma' f m k T' T (*Sub_Sig'_Sig *) WF_env WF_m WF_k
      end.

    Definition WFVM_Environment_ifmap
      (A B : WFValueM_i D V MT ME _ -> Prop)
      (i : WFValueM_i D V MT ME _)
      (f : forall i, A i -> B i)
      (WFVM_a : WFValueM_Environment A i)
      :
      WFValueM_Environment B i :=
      match WFVM_a in WFValueM_Environment _ i return WFValueM_Environment B i with
        | WFVM_Ask Sigma k T WF_k =>
          WFVM_Ask _ Sigma k T (fun env WF_env => f _ (WF_k env WF_env))
        | WFVM_Local Sigma Gamma' f' m k T' T (*Sub_Sig'_Sig *) WF_env WF_m WF_k =>
          WFVM_Local _ Sigma Gamma' f' m k T' T (*Sub_Sig'_Sig *) WF_env (f _ WF_m)
          (fun Sigma'' v Sub_Sig''_Sig' WF_v_T' => (f _ (WF_k Sigma'' v Sub_Sig''_Sig' WF_v_T')))
      end.

    Global Instance iFun_wfvm_Environment : iFunctor WFValueM_Environment.
      constructor 1 with (ifmap := WFVM_Environment_ifmap).
      (* ifmap_fusion *)
      destruct a; simpl; intros; reflexivity.
      (* ifmap_id *)
      destruct a; simpl; intros; auto;
        apply f_equal; repeat (apply functional_extensionality_dep; intros); auto.
    Defined.

    Context {Sub_WFVM_Base_WFVM : Sub_iFunctor (WFValueM_base D V MT ME _ WFV) WFVM}.
    Context {Sub_WFVM_Environment_WFVM : Sub_iFunctor WFValueM_Environment WFVM}.

    Global Instance wfvm_bind_Environment :
      iPAlgebra wfvm_bind_Name (wfvm_bind_P D V MT ME TypContext WFV WFVM) WFValueM_Environment.
    Proof.
      constructor; unfold iAlgebra; intros.
      apply ind_alg_WFVM_Environment; try eassumption;
        unfold wfvm_bind_P; simpl; intros.
      (* ask *)
      rewrite <- associativity.
      apply (inject_i (subGF := Sub_WFVM_Environment_WFVM)).
      constructor.
      intros.
      apply H0; auto.
      (* local *)
      repeat rewrite <- associativity.
      apply (inject_i (subGF := Sub_WFVM_Environment_WFVM)).
      constructor 2 with (Gamma' := Gamma') (T' := T'); simpl in *; auto.
      generalize (H1 return_ return_); rewrite <- right_unit; rewrite <- left_unit; intro WF_m_T; apply WF_m_T.
      simpl; intros; repeat rewrite fmap_return; apply inj_return; congruence.
      intros; apply (inject_i (subGF := Sub_WFVM_Base_WFVM)); econstructor; eauto.
      apply return_orn; auto.
      intros; apply H2; eauto.
      intros; eapply WFVM_ke_kt; eauto; eapply ConsExtension_trans; eauto.
    Defined.

    Context {WFV_Weaken_WFV : iPAlgebra WFValue_Weaken_Name (WFValue_Weaken_P D V _ WFV) WFV}.

    Context {TypContextCE' : ConsExtensionC TypContext}.
    Context {WFV_Weaken_WFV' : iPAlgebra WFValue_Weaken_Name (WFValue_Weaken_P (TypContextCE := TypContextCE') D V _ WFV) WFV}.

    Lemma WF_Environment_Weaken : forall Sigma env gamma,
      WF_Environment D V _ WFV Sigma env gamma ->
      forall Sigma',
        ConsExtension Sigma' Sigma ->
        WF_Environment D V _ WFV Sigma' env gamma.
    Proof.
      intros; eapply P2_Env_P_P'; try eassumption.
      intros; eapply (WFV_Weaken D V _ WFV _ _ H1); eauto.
    Qed.

    Definition WFValue_Weaken'_P (i : WFValue_i D V TypContext) :=
      forall env,
        WFValueC _ _ _ WFV (GammaSet _ (wfv_S _ _ _ i) env) (wfv_v _ _ _ i) (wfv_T _ _ _ i).

    Inductive WFValue_Weaken'_Name := wfvalue_weaken'_name.

    Context {WFV_Weaken'_WFV : iPAlgebra WFValue_Weaken'_Name WFValue_Weaken'_P WFV}.

    Definition WFV_Weaken' := ifold_ WFV _ (ip_algebra (iPAlgebra := WFV_Weaken'_WFV)).

  (* ============================================== *)
  (* TYPE SOUNDNESS                                 *)
  (* ============================================== *)

    Context {wfvm_bind_alg :
      iPAlgebra wfvm_bind_Name (wfvm_bind_P D V MT ME _ WFV WFVM (TypContextCE := TypContextCE)) WFVM}.
    Context {EQV_proj1_alg :
      forall A B, iPAlgebra EQV_proj1_Name (EQV_proj1_P F EQV_E A B) (EQV_E _ _)}.
    Context {WFV_proj1_a_WFV :
      iPAlgebra WFV_proj1_a_Name (WFV_proj1_a_P D V _ WFV) WFV}.
     Context {WFV_proj1_b_WFV :
       iPAlgebra WFV_proj1_b_Name (WFV_proj1_b_P D V _ WFV) WFV}.
     Context {eq_DType_eq_DT : PAlgebra eq_DType_eqName D D (UP'_P (eq_DType_eq_P D))}.
     Context {eq_DType_neq_D : PAlgebra eq_DType_neqName D D (UP'_P (eq_DType_neq_P D))}.

    Class GammaConsExtension'C (TypContext : Set)
      (ConsExt : ConsExtensionC TypContext)
      (GammaTyp : GammaTypContextC D TypContext) : Type :=
      {
        ConsExtension_GammaInsert : forall Sigma T,
          ConsExtension (ConsExtensionC := ConsExt) (GammaInsert _ T Sigma) Sigma}.

    Context {TypContextGCE' : GammaConsExtension'C TypContext TypContextCE' GammaTypContext}.

  End WFValue_Sec.

End EffReader.

(*
*** Local Variables: ***
*** coq-prog-args: ("-emacs-U" "-impredicative-set") ***
*** End: ***
*)

author: skeuchel