Skip to content

Instantly share code, notes, and snippets.

View RyanGlScott's full-sized avatar

Ryan Scott RyanGlScott

View GitHub Profile
@RyanGlScott
RyanGlScott / cabal.project.local
Last active October 23, 2024 12:09
GHC 9.12 cabal.project.local
allow-newer:
assoc:base,
async:base,
binary-orphans:base,
-- TODO
blank-canvas:base,
-- TODO
blank-canvas-examples:base,
boring:base,
-- TODO
@RyanGlScott
RyanGlScott / A.hs
Created September 26, 2024 18:09
An unsuccessful attempt at distilling a GHC infinite loop during compilation
{-# LANGUAGE Haskell2010 #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE NoImplicitPrelude #-}
module Main (main) where
import Language.Copilot
import Copilot.Compile.C99
import Data.Type.Equality as DE
import Data.Proxy (Proxy(..))
@RyanGlScott
RyanGlScott / copilot-theorem-struct-updates.diff
Created July 5, 2024 20:18
A patch allowing copilot-theorem to support the UpdateField operation
diff --git a/copilot-theorem/src/Copilot/Theorem/What4/Translate.hs b/copilot-theorem/src/Copilot/Theorem/What4/Translate.hs
index f55e3884..428b6ac3 100644
--- a/copilot-theorem/src/Copilot/Theorem/What4/Translate.hs
+++ b/copilot-theorem/src/Copilot/Theorem/What4/Translate.hs
@@ -799,6 +799,8 @@ translateOp2 sym origExpr op xe1 xe2 = case (op, xe1, xe2) of
(CE.BwShiftL _ _, xe1, xe2) -> translateBwShiftL xe1 xe2
(CE.BwShiftR _ _, xe1, xe2) -> translateBwShiftR xe1 xe2
(CE.Index _, xe1, xe2) -> translateIndex xe1 xe2
+ (CE.UpdateField atp _ftp extractor, structXe, fieldXe) ->
+ translateUpdateField atp extractor structXe fieldXe
@RyanGlScott
RyanGlScott / StructsOfArrays.hs
Created July 5, 2024 19:44
A Copilot specification involving an update to a struct containing arrays
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE NoImplicitPrelude #-}
module Main (main) where
import Language.Copilot
import Copilot.Compile.C99
data SoA = SoA
{ arr :: Field "arr" (Array 2 Word32)
}
@RyanGlScott
RyanGlScott / FloatingPoint.cry
Last active May 19, 2024 12:17
FloatingPoint in Cryptol
module FloatingPoint where
import Float
type FloatingPoint e m =
{ sign : Bit
, exp : [e]
, sfd : [m]
}
@RyanGlScott
RyanGlScott / cabal.project.local
Last active May 4, 2024 12:38
GHC 9.10 cabal.project.local
allow-newer:
aeson:containers,
aeson:template-haskell,
-- Ugh.
aeson:th-abstraction,
assoc:base,
async:base,
-- TODO
bifunctors:template-haskell,
binary-orphans:base,
@RyanGlScott
RyanGlScott / cabal.project.local
Last active September 30, 2023 13:58
containers-0.7 cabal.project.local
constraints:
containers == 0.7.*
allow-newer:
aeson:containers,
Cabal-syntax:containers,
cabal-install-parsers:containers,
cassava:containers,
foldable1-classes-compat:containers,
hashable:containers,
@RyanGlScott
RyanGlScott / crux-mir-test.txt
Created March 21, 2023 14:40
crux-mir test suite progress
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
RyanGlScott / Blah.sawcore
Created January 23, 2023 16:53
Heapster example of how to specify a memcpy-like function
module Blah where