Carter Schonwald

2018-02-01 22:13:58 UTC

Hello everyone! i'm messing around with trying to mock / model out first

class "signed values", and with a toy development i'm getting some type

universe issues which makes me suspect i'm modelling it wrong,

feedback would be appreciated,

https://gist.github.com/cartazio/373eaa1ab726b2f6e651777a44b3f2b1

is the current version of the code

many thanks!

-Carter

also including it inline below

module auth where

open import Data.String

open import Data.Nat

open import Level

open import Data.Product

open import Relation.Binary.PropositionalEquality

open import Relation.Binary.HeterogeneousEquality as Het

-- SignedBy will be a magic built in type that requires type checker support

-- seems likely in practice that i'll need to have some singleton structures

record SignedBy {â } (t : Set â ) ( identity : String ) : Set â where

field

val : t

uniqueCounter : â --- unique natural number th

hashOfVal : â --- nat number thats a Cryptographically Strong Hash of

the canonical serialization of val

signature : String --- signature of concatenation of

---(hashfOfVal , uniqueCounter), using the public

key denotated by identity

data AsDelegate : Set where

IsDelegate : AsDelegate

IsLeaf : AsDelegate

open AsDelegate

record TypeSing {â : Level} ( tau : Set â ) (v : tau) : Set â where

field

singVal : tau

singIsSing : singVal â¡ v

record Pair {tx ty : Level} ( x : Set tx ) (y : Set ty ) : Set ( Level.suc

(tx Level.â ty )) where

constructor mkPair

field

one : x

two : y

data OnBehalfOf : String -> String -> AsDelegate -> Set where

Self : { x : String } -> OnBehalfOf x x IsDelegate

DelegatedTo : {root mid : String} -> (end : String)->

SignedBy ( mkPair (OnBehalfOf mid root IsDelegate) (

TypeSing String end)) mid ->

---- not sure how to hack around this type universe issue...

am I getting impredicative or wishing i was?

OnBehalfOf end root IsDelegate

LeafAuth : {root mid : String} -> (end : String) -> OnBehalfOf mid root

IsDelegate -> OnBehalfOf end root IsLeaf

{-

equivalent datalog would be (roughly)

onBehalfOf(me,me,Delegate).

onBehalfOf(agent,originalPerson,Delegate) :-

onBehalfOf(mid,originalPerson,Delegate),AddsDelegateFor(mid,originalperson,agent)

onBhealfOf(leafAgent,originalPerson,LEAF) :-

onBehalfOf(mid,originalPerson,Delegate),AddsLeafFor(mid,originalperson,leafAgent)

-}

class "signed values", and with a toy development i'm getting some type

universe issues which makes me suspect i'm modelling it wrong,

feedback would be appreciated,

https://gist.github.com/cartazio/373eaa1ab726b2f6e651777a44b3f2b1

is the current version of the code

many thanks!

-Carter

also including it inline below

module auth where

open import Data.String

open import Data.Nat

open import Level

open import Data.Product

open import Relation.Binary.PropositionalEquality

open import Relation.Binary.HeterogeneousEquality as Het

-- SignedBy will be a magic built in type that requires type checker support

-- seems likely in practice that i'll need to have some singleton structures

record SignedBy {â } (t : Set â ) ( identity : String ) : Set â where

field

val : t

uniqueCounter : â --- unique natural number th

hashOfVal : â --- nat number thats a Cryptographically Strong Hash of

the canonical serialization of val

signature : String --- signature of concatenation of

---(hashfOfVal , uniqueCounter), using the public

key denotated by identity

data AsDelegate : Set where

IsDelegate : AsDelegate

IsLeaf : AsDelegate

open AsDelegate

record TypeSing {â : Level} ( tau : Set â ) (v : tau) : Set â where

field

singVal : tau

singIsSing : singVal â¡ v

record Pair {tx ty : Level} ( x : Set tx ) (y : Set ty ) : Set ( Level.suc

(tx Level.â ty )) where

constructor mkPair

field

one : x

two : y

data OnBehalfOf : String -> String -> AsDelegate -> Set where

Self : { x : String } -> OnBehalfOf x x IsDelegate

DelegatedTo : {root mid : String} -> (end : String)->

SignedBy ( mkPair (OnBehalfOf mid root IsDelegate) (

TypeSing String end)) mid ->

---- not sure how to hack around this type universe issue...

am I getting impredicative or wishing i was?

OnBehalfOf end root IsDelegate

LeafAuth : {root mid : String} -> (end : String) -> OnBehalfOf mid root

IsDelegate -> OnBehalfOf end root IsLeaf

{-

equivalent datalog would be (roughly)

onBehalfOf(me,me,Delegate).

onBehalfOf(agent,originalPerson,Delegate) :-

onBehalfOf(mid,originalPerson,Delegate),AddsDelegateFor(mid,originalperson,agent)

onBhealfOf(leafAgent,originalPerson,LEAF) :-

onBehalfOf(mid,originalPerson,Delegate),AddsLeafFor(mid,originalperson,leafAgent)

-}