Blaisorblade

##########################################################################
##* crouton.conf defaults are:                                          ##
# DELAY=10            # delay desired number of seconds before starting ##
# CHROOT=xenial       # enter desired chroot to start                   ##
# START_DE=startxfce4 # enter desired Desktop Envirnoment to use        ##
# CHROOT_APP=none     # enter desired chroot application to run         ##
# XMETHOD=default     # enter the desired XMETHOD (xorg,xephyr,xiwi)    ##
# RUN_STATE=y         # change to 'n' to disable running $CHROOT        ##
##########################################################################

Blaisorblade

# Copyright (c) 2016 The crouton Authors. All rights reserved.
# Use of this source code is governed by a BSD-style license that can be
# found in the LICENSE file.

## Filename: /etc/init/crouton.conf
## NOTE: 'rootfs' verification needs to be removed.

## crouton chroot - Start session
##
## This will start a (crouton) chroot Desktop Environment session

Blaisorblade

#!/bin/sh -e 
##!! PLEASE USE THIS SCRIPT WITH CAUTION - AND AT YOUR OWN RISK          !!##
##!! IT HAS BEEN KNOWN TO CAUSE RESETS AND WIPE DATA ON SOME CHROMEBOXES !!##

APPLICATION="${0##*/}"
ANSWER=''
SUDO=''

USAGE="
$APPLICATION [no options]

Blaisorblade

% Ensure that bussproofs and mathpartir rules have the same thickness.
%
% bussproofs uses hrule, defaulting to 0.4pt. Instead, testing and docs show
% that mathpartir uses \over, both by default and here.
% Horizontal rule thickness for \over depends on font parameters.
%%
% Read the thickness of fraction rule.
%%
% 1. We use https://tex.stackexchange.com/a/96063/1340 to read font parameters.
% 2. The parameter in question is \fontdimen8\textfont3,

Blaisorblade

1: looking for (Equiv (hoD Σ n)) without backtracking
1.1: (*external*) (eapply (ofe_equiv _)) on (Equiv (hoD Σ n)), 0 subgoal(s)
1: looking for (Equiv (hoLtyO Σ n)) without backtracking
1.1: (*external*) (eapply (ofe_equiv _)) on
(Equiv (hoLtyO Σ n)), 0 subgoal(s)
1: looking for (Proper (equiv ==> equiv) packHoLtyO) without backtracking
1: looking for (Params (@packHoLtyO) ?H0) with backtracking
1.1: exact Params_instance_1 on (Params (@packHoLtyO) ?H0), 0 subgoal(s)
1.1: (*external*) proper_reflexive on
(Proper (equiv ==> equiv) packHoLtyO), 1 subgoal(s)

Blaisorblade

From iris.si_logic Require Import siprop bi.

(** Taken from [base_logic.bi]. *)
(** New unseal tactic that also unfolds the BI layer.
    TODO: Can we get rid of this? *)
Ltac unseal := (* Coq unfold used to circumvent bug #5699 in rewrite /foo *)
  unfold bi_emp; simpl; unfold sbi_emp; simpl;
  unfold siProp_emp, bupd, bi_bupd_bupd, bi_pure,
  bi_and, bi_or, bi_impl, bi_forall, bi_exist,
  bi_sep, bi_wand, bi_persistently, sbi_internal_eq, sbi_later; simpl;

Blaisorblade

        (*external*) (simple apply @label_pair_iapprox_persistent)(level 1, pattern 
        @Persistent (uPredI (iResUR ?Σ))
          (@iapprox ?Σ ?Hdlang (prod label ?A)
             (@label_pair_iapprox ?Σ ?Hdlang ?A ?B) 
             ?x ?y), id 0)

        simple apply @label_pair_iapprox_persistent(level 1, pattern 
        @Persistent (uPredI (iResUR ?META11068))
          (@iapprox ?META11068 ?META11069 (prod label ?META11070)
             (@label_pair_iapprox ?META11068 ?META11069 ?META11070 ?META11071)

Blaisorblade

From iris.base_logic Require Import invariants.
(* From iris.bi Require Import ascii. *)
From iris.algebra Require Import ofe cmra frac agree gmap.

Definition fractionalR (o : ofeT) : cmraT := prodR fracR (agreeR (leibnizO o)).
Lemma fractional_op A p q (rv : agreeR (leibnizO A)) :
  (p, rv) ⋅ (q, rv) ≡ ((p + q)%Qp, rv).
Proof. by rewrite -pair_op agree_idemp. Qed.

Section sec.

Blaisorblade

From iris.algebra Require Import ofe.

Instance equiv_ext_discrete_fun {A B} :
  subrelation (≡@{A -d> B}) (pointwise_relation A (≡)).
Proof. done. Qed.

Instance dist_ext_discrete_fun {A B n} :
  subrelation (dist n (A := A -d> B)) (pointwise_relation A (dist n)).
Proof. done. Qed.

Blaisorblade

module Semwap.NatSem where

open import Prelude hiding (force)
open import Prelude.Extras.Eq
open import Prelude.Extras.Delay

import Level

open import Semwap.Expr