Ryan Scott RyanGlScott
RyanGlScott
/ cabal.project.local
Last active
September 30, 2023 13:58
containers-0.7 cabal.project.local
View cabal.project.local
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| constraints: | |
| containers == 0.7.* | |
| allow-newer: | |
| aeson:containers, | |
| Cabal-syntax:containers, | |
| cabal-install-parsers:containers, | |
| cassava:containers, | |
| foldable1-classes-compat:containers, | |
| hashable:containers, |
View crux-mir-test.txt
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| crux-mir | |
| crux concrete | |
| refs | |
| promoted_imm: OK (0.15s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 0 | |
| Crux output: 0 | |
| mut_raw: OK (0.15s) | |
| Compiling and running oracle program (0.15s) |
RyanGlScott
/ Blah.sawcore
Created
January 23, 2023 16:53
Heapster example of how to specify a memcpy-like function
View Blah.sawcore
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| module Blah where |
View cabal.project.local
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| allow-newer: | |
| aeson:deepseq, | |
| aeson:ghc-prim, | |
| aeson:template-haskell, | |
| aeson:th-abstraction, | |
| assoc:base, | |
| async:base, | |
| attoparsec:ghc-prim, | |
| binary-orphans:base, | |
| boring:base, |
RyanGlScott
/ SimplifiedExample.v
Last active
November 22, 2022 20:30
View SimplifiedExample.v
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| From Coq Require Import Program.Basics. | |
| From Coq Require Program.Equality. | |
| From Coq Require Import Vectors.Vector. | |
| From Coq Require Import Logic.Eqdep. | |
| Import VectorNotations. | |
| Require Import Lia. | |
| Require Import ZArith. | |
| Require Import ZifyBool. |
RyanGlScott
/ ZifyTermTakeOne.v
Created
November 21, 2022 14:48
A failing attempt to use https://github.com/coq/coq/pull/16868
View ZifyTermTakeOne.v
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| From Coq Require Import Program.Basics. | |
| From Coq Require Program.Equality. | |
| From Coq Require Import Vectors.Vector. | |
| From Coq Require Import Logic.Eqdep. | |
| Import VectorNotations. | |
| Require Import Lia. | |
| Require Import ZArith. | |
| Require Import ZifyBool. |
View HDList.hs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {-# LANGUAGE DataKinds #-} | |
| {-# LANGUAGE FlexibleInstances #-} | |
| {-# LANGUAGE GADTs #-} | |
| {-# LANGUAGE StandaloneKindSignatures #-} | |
| {-# LANGUAGE TypeOperators #-} | |
| {-# LANGUAGE UndecidableInstances #-} | |
| module HDList where | |
| import qualified Control.Category as Cat (Category(..)) | |
| import Data.Function (on) |
RyanGlScott
/ DList.v
Last active
July 24, 2022 12:33
Proofs of the difference list invariant for various operations
View DList.v
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Require Import Lists.List. | |
| Import ListNotations. | |
| Open Scope list_scope. | |
| Require Import Logic.FunctionalExtensionality. | |
| Require Import Lists.Streams. | |
| Inductive DList (a : Type) : Type := | |
| | MkDList : (list a -> list a) -> DList a. | |
| Arguments MkDList {a} f. |
RyanGlScott
/ FromToVec.hs
Created
August 28, 2021 15:00
Proofs involving conversion from and to length-indexed vectors
View FromToVec.hs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {-# LANGUAGE DataKinds #-} | |
| {-# LANGUAGE GADTs #-} | |
| {-# LANGUAGE PolyKinds #-} | |
| {-# LANGUAGE ScopedTypeVariables #-} | |
| {-# LANGUAGE StandaloneKindSignatures #-} | |
| {-# LANGUAGE TypeApplications #-} | |
| {-# LANGUAGE TypeFamilies #-} | |
| {-# LANGUAGE TypeOperators #-} | |
| module FromToVec where |
View Main.hs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {-# LANGUAGE DataKinds #-} | |
| {-# LANGUAGE GADTs #-} | |
| {-# LANGUAGE KindSignatures #-} | |
| {-# LANGUAGE NoStarIsType #-} | |
| {-# LANGUAGE RankNTypes #-} | |
| {-# LANGUAGE ScopedTypeVariables #-} | |
| {-# LANGUAGE TypeApplications #-} | |
| {-# LANGUAGE TypeOperators #-} | |
| {-# OPTIONS_GHC -Wall #-} | |
| module Main (main) where |
NewerOlder