Skip to content

Latest commit

 

History

History
334 lines (317 loc) · 12.2 KB

INSTALL.md

File metadata and controls

334 lines (317 loc) · 12.2 KB

Installation

These are instructions on how to install and verify the supplementary material, either locally or using the paper artifact. The artifact is a QEMU virtual machine image with only necessary dependencies installed, and is approximately 2 GB, but may grow up to 12 GB if modified (say, by installing GHC). The virtual machine may use up to 2 GB of memory only following these instructions. The instructions are also labelled with "[Artifact only]" iff using the VM, and "[No artifact]" iff running locally, which requires Coq, Agda, GHC, and other dependencies to be installed.

  1. [Artifact only] Install QEMU
    • On Windows, virtualization needs to be enabled: from the Start menu, search for and open Windows Features, select Hyper-V and Windows Hypervisor Platform, and click OK
  2. [Artifact only] Run the script start.sh or start.bat (Windows), which will run the following command: 
    qemu-system-x86_64 -m 2048 -accel <accel> -cpu max -nic user -hda disk.qcow2
    • Linux: kvm for <accel>
    • Apple: hvf for <accel>
    • Windows: tcg for <accel>
    • Other: tcg for <accel>
  3. [Artifact only] Within QEMU, login as root (blank password); you should already be in the /root/StraTT directory
  4. To check the Coq development:
    1. cd coq from the StraTT directory
    2. make -Bf CoqSrc.mk to force check proof of type safety
    3. Assumptions (in axioms.v) will be printed by above
  5. To check the Agda development:
    1. cd agda from the StraTT directory
    2. rm *.agdai to clean up previously checked files
    3. agda consistency.agda to check proof of consistency
    4. grep "postulate" *.agda to find postulates
  6. To run prototype implementation:
    1. cd impl from the StraTT directory
    2. [No artifact] Build implementation:
      1. ghcup install ghc 9.6.6 to install GHC
      2. stack install to compile implementation
    3. stratt pi/StraTT.pi to check examples listed in paper
    4. stratt pi/README.pi to check all examples provided
  7. [Artifact only] All changes made can be undone by git reset && git restore .

Artifact troubleshooting

The Arch Linux wiki on QEMU has good guidance on using QEMU if problems persist. Flags can be passed directly to the start.sh script.

  • If qemu-system-x86_64 cannot be found, ensure that the path to QEMU binaries is in your PATH environment variable
  • If there is an "invalid accelerator" error, use tcg for <accel>
  • If more memory is required, increase the number of MB in -m 2048
  • If things aren't displaying correctly, add the -nographic flag to see the output directly in the terminal

Dependency and version summary

The below table summarizes the versions of the various required dependencies when running locally. Brief installation details are found in the README.md files of each of the three subdirectories.

Dependency Version
OCaml 4.14.2
Coq 8.19.1
Metalib latest
Ott 0.33
LNgen 0.3.2
GHC 9.6.6
Stack latest
Cabal latest
Agda 2.7.0.1
agda-stdlib 2.1.1
Z3 4.13.0

Expected outputs

The following are the expected outputs from running the commands above in the corresponding directories in the VM.

[/root/StraTT/agda] $ agda consistency.agda
Checking consistency (/root/StraTT/agda/consistency.agda).
 Checking common (/root/StraTT/agda/common.agda).
 Checking accessibility (/root/StraTT/agda/accessibility.agda).
 Checking syntactics (/root/StraTT/agda/syntactics.agda).
 Checking reduction (/root/StraTT/agda/reduction.agda).
 Checking typing (/root/StraTT/agda/typing.agda).
 Checking semantics (/root/StraTT/agda/semantics.agda).
 Checking soundness (/root/StraTT/agda/soundness.agda).

[/root/StraTT/agda] $ grep "postulate" *.agda
accessibility.agda:  private postulate

[/root/StraTT/coq] $ make -Bf CoqSrc.mk
COQDEP VFILES
COQC StraTT_ott.v
COQC StraTT_inf.v
COQC axioms.v
COQC tactics.v
COQC basics.v
COQC incr.v
COQC ctx.v
COQC restrict.v
COQC subst.v
COQC inversion.v
COQC typesafety.v
Axioms:
ineq_Type_Bottom : forall S : signature, DEquiv S a_Type a_Bottom -> False
ineq_Pi_Type
  : forall (S : signature) (B1 : tm) (j : Datatypes.nat) (B2 : tm),
    DEquiv S (a_Pi B1 j B2) a_Type -> False
ineq_Pi_Bottom
  : forall (S : signature) (B1 : tm) (j : Datatypes.nat) (B2 : tm),
    DEquiv S (a_Pi B1 j B2) a_Bottom -> False
ineq_Arrow_Type
  : forall (S : signature) (A1 A2 : tm),
    DEquiv S (a_Arrow A1 A2) a_Type -> False
ineq_Arrow_Pi
  : forall (S : signature) (A1 B1 A2 : tm) (j : Datatypes.nat) (B2 : tm),
    DEquiv S (a_Arrow A1 A2) (a_Pi B1 j B2) -> False
ineq_Arrow_Bottom
  : forall (S : signature) (A1 A2 : tm),
    DEquiv S (a_Arrow A1 A2) a_Bottom -> False
Eqdep.Eq_rect_eq.eq_rect_eq
  : forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p),
    x = eq_rect p Q x p h
DEquiv_Pi_inj3
  : forall (S : signature) (A1 B1 : tm) (j1 j2 : Datatypes.nat)
      (A2 B2 a : tm),
    lc_tm a ->
    DEquiv S (a_Pi A1 j1 B1) (a_Pi A2 j2 B2) ->
    DEquiv S (open B1 a) (open B2 a)
DEquiv_Pi_inj2
  : forall (S : signature) (A1 B1 : tm) (j1 j2 : Datatypes.nat) (A2 B2 : tm),
    DEquiv S (a_Pi A1 j1 B1) (a_Pi A2 j2 B2) -> j1 = j2
DEquiv_Pi_inj1
  : forall (S : signature) (A1 B1 : tm) (j1 j2 : Datatypes.nat) (A2 B2 : tm),
    DEquiv S (a_Pi A1 j1 B1) (a_Pi A2 j2 B2) -> DEquiv S A1 A2
DEquiv_Arrow_inj2
  : forall (S : signature) (A1 B1 A2 B2 : tm),
    DEquiv S (a_Arrow A1 B1) (a_Arrow A2 B2) -> DEquiv S B1 B2
DEquiv_Arrow_inj1
  : forall (S : signature) (A1 B1 A2 B2 : tm),
    DEquiv S (a_Arrow A1 B1) (a_Arrow A2 B2) -> DEquiv S A1 A2

[/root/StraTT/impl] $ stratt pi/StraTT.pi
processing StraTT.pi...
Parsing File "pi/StraTT.pi"
type checking...
Checking module "StraTT"
module StraTT where
id' : (X : Type 0) -> (x : X 0) -> X @ 1
id' = \X x. x
id : (X : Type 0) -> X -> X @ 1
id = \X x. x
idid1 : ((X : Type 1) -> X -> X) -> (X : Type 0) -> X -> X @ 2
idid1 = \id. id ((X : Type 0) -> X -> X) (\X. id X)
idid2 : ((X : Type 2) -> X -> X) -> (X : Type 0) -> X -> X @ 3
idid2 = \id.
          id (((X : Type 1) -> X -> X) -> (X : Type 0) -> X -> X) idid1 (\X.
                                                                           id X)
idid3 : ((X : Type 3) -> X -> X) -> (X : Type 0) -> X -> X @ 4
idid3 = \id.
          id (((X : Type 2) -> X -> X) -> (X : Type 0) -> X -> X) idid2 (\X.
                                                                           id X)
idid1id : ((idid1 (\X x. x)) = (\X x. x)) @ 2
idid1id = Refl
idid2id : ((idid2 (\X x. x)) = (\X x. x)) @ 3
idid2id = Refl
idid3id : ((idid3 (\X x. x)) = (\X x. x)) @ 4
idid3id = Refl
OptionC : Type -> Type @ 1
OptionC = \X. (Y : Type 0) -> Y -> (X -> Y) -> Y
NoneC : (X : Type 0) -> OptionC X @ 1
NoneC = \X Y y f. y
SomeC : (X : Type 0) -> X -> OptionC X @ 1
SomeC = \X x Y y f. f x
joinC : (X : Type 0) -> OptionC (OptionC X) -> OptionC X @ 1
joinC = \X oopt Y y f. oopt Y y (\opt. opt Y y f)
Option' : (X : Type 0) -> Type @ 2
Option' = \X.
            (Y : Type 0) -> (_ : Y 0) -> (_1 : (_2 : X 0) -> Y 1) -> Y
None' : (X : Type 0) -> Option' X @ 2
None' = \X Y y f. y
Some' : (X : Type 0) -> (_ : X 0) -> Option' X @ 2
Some' = \X x Y y f. f x
join' : (X : Type 0) -> (_ : Option'^2 (Option' X) 4) -> Option' X @ 5
join' = \X oopt Y y f. oopt Y y (\opt. opt Y y f)
neg : Type -> Type @ 0
neg = \X. X -> Void
DecC : Type -> Type @ 1
DecC = \X. (Z : Type 0) -> (X -> Z) -> (neg X -> Z) -> Z
yes : (X : Type 0) -> X -> DecC X @ 1
yes = \X x Z f g. f x
no : (X : Type 0) -> neg X -> DecC X @ 1
no = \X nx Z f g. g nx
neg' : (_ : Type 0) -> Type @ 1
neg' = \X. X -> Void
DecC' : (_ : Type 0) -> Type @ 3
DecC' = \X.
          (Z : Type 0) -> (yz : (x : X 0) -> Z 2) -> (nz : (nx : neg' X 1) -> Z 2) -> Z
yes' : (X : Type 0) -> (x : X 0) -> DecC' X @ 3
yes' = \X x Z f g. f x
no' : (X : Type 0) -> (nx : neg' X 1) -> DecC' X @ 3
no' = \X nx Z f g. g nx
eq : (X : Type 0) -> X -> X -> Type @ 1
eq = \X x y. (P : X -> Type 0) -> P x -> P y
refl : (X : Type 0) -> (x : X 0) -> eq X x x @ 1
refl = \X x P px. px
isProp : (X : Type 0) -> Type @ 1
isProp = \X. (x : X 0) -> (y : X 0) -> eq X x y
isSet : (X : Type 0) -> Type @ 2
isSet = \X. (x : X 0) -> (y : X 0) -> isProp^1 (eq X x y)
data Dec (X : Type) : Type 0 where
  Yes of (_689 : X) @ 0
  No of (_691 : neg X) @ 0
decDNE : (X : Type 0) -> Dec X -> neg (neg X) -> X @ 1
decDNE = \X dec nnx.
           case dec of
             Yes x -> x
             No nx -> absurd nnx nx
data Eq (X : Type @ 0) (x : X) (y : X) : Type 1 where
  refl of (z : X @ 0) (z = x) (z = y) @ 1
isProp' : (X : Type 0) -> Type @ 1
isProp' = \X. (x : X 0) -> (y : X 0) -> Eq X x y
isSet' : (X : Type 0) -> Type @ 2
isSet' = \X. (x : X 0) -> (y : X 0) -> isProp'^1 (Eq X x y)
UIP : (X : Type 0) -> (x : X 0) -> (p : Eq X x x 1) -> Eq^1 (Eq X x x) p (refl x) @ 2
UIP = \X x p.
        case p of
          refl z -> refl^1 (refl z)
data NPair (X : Type @ 0) (P : X -> Type) : Type 1 where
  MkPair of (x : X @ 0) (_814 : P x) @ 1
nfst : (X : Type 0) -> (P : X -> Type 0) -> NPair X P -> X @ 1
nfst = \X P p.
         case p of
           MkPair x y -> x
nsnd : (X : Type 0) -> (P : X -> Type 0) -> (p : NPair X P 1) -> P (nfst X P p) @ 2
nsnd = \X P p.
         case p of
           MkPair x y -> y
data DPair (X : Type @ 0) (P : (_ : X 0) -> Type) : Type 1 where
  MkPair of (x : X @ 0) (_865 : P x) @ 1
dfst : (X : Type 0) -> (P : (_ : X 0) -> Type 1) -> DPair X P -> X @ 2
dfst = \X P p.
         case p of
           MkPair x y -> x
dsnd : (X : Type 0) -> (P : (_ : X 0) -> Type 1) -> (p : DPair X P 1) -> case p of
                                                                           MkPair x y -> P x @ 2
dsnd = \X P p.
         case p of
           MkPair x y -> y
data U : Type 1 where MkU of (X : Type @ 0) (_923 : X -> U) @ 1
data WF (u : U) : Type 2 where
  MkWF of (X : Type @ 0)
          (f : X -> U @ 1)
          (_933 : (x : X 1) -> WF (f x))
          (u = MkU X f) @ 2
wf : (u : U 1) -> WF u @ 2
wf = \u.
       case u of
         MkU X f -> MkWF X f (\x. wf (f x))
loop : U @ 1
loop = TRUSTME
nwfLoop : WF loop -> Void @ 2
nwfLoop = \wfLoop. TRUSTME
falseLoop : Void @ 2
falseLoop = nwfLoop (wf loop)
regular : U -> Type @ 1
regular = \u.
            case u of
              MkU X f -> (x : X 0) -> ((f x) = (MkU X f)) -> Void
R : U^2 @ 3
R = MkU^2 (NPair^1 U regular) (\ureg. TRUSTME)
R_nonreg : regular^2 R -> Void @ 3
R_nonreg = TRUSTME
R_reg : regular^2 R @ 3
R_reg = \ureg p.
          case ureg of
            MkPair u reg -> TRUSTME
falseR : Void @ 3
falseR = R_nonreg R_reg
P : Type -> Type @ 0
P = \X. X -> Type
UU : Type @ 1
UU = (X : Type 0) -> (P (P X) -> X) -> P (P X)
tau : P (P UU) -> UU @ 1
tau = \t X f p. t (\s. p (f (s X f)))
sig : UU^1 -> P (P UU) @ 2
sig = \s. s UU tau
Delta : P UU^1 @ 2
Delta = \y. ((p : P UU 1) -> sig y p -> p (tau (sig y))) -> Void
Omega : UU @ 3
Omega = tau (\p. (x : UU^1 2) -> sig x p -> p (\X. x X))
M : (x : UU^2 3) -> sig^1 x Delta -> Delta^1 x @ 4
M = \x s d. d Delta s (\p. d (\y. p (tau (sig y))))
D : Type @ 3
D = (p : P UU 1) -> ((x : UU 1) -> sig TRUSTME p -> p x) -> p Omega

Artifact creation

This section is not for artifact reviewers; it contains notes on how the artifact itself was created.

  1. Create 12 GB dynamic disk image: qemu-img create -f qcow2 disk.qcow2 12G
  2. Boot disk with Alpine Linux (virtual) 3.20.3 for installation: 
    qemu-system-x86_64 -m 2048 -accel kvm -cpu host -nic user -nographic \
   -hda disk.qcow2 -cdrom "alpine-virt-3.20.3-x86_64" -boot order=d
  3. Boot image using start script and install prerequisite software: 
    apk add binutils-gold coq curl gcc g++ git gmp-dev libc-dev libffi-dev make musl-dev ncurses-dev opam perl tar xz z3 zlib-dev
    then install GHCup, Cabal, Stack, GHC, Agda, and Metalib as required
  4. If any partition modifications need to be done: 
    modprobe nbd max_part=4
qemu-nbd -c /dev/nbd0 disk.qcow2
# inspect/mount/modify/etc. device
qemu-nbd -d /dev/nbd0
  5. Shrink disk to occupied space only: 
    virt-sparsify --in-p lace disk.qcow2
mv disk.qcow2 disk-old.qcow2
qemu-img convert -O qcow2 disk-old.qcow2 disk.qcow2
rm disk-old.qcow2