Discussion:
am I doing something fundamentally impredicative in this code? or is there a better approach
(too old to reply)
Carter Schonwald
2018-02-01 22:13:58 UTC
Permalink
Raw Message
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)
-}
Carter Schonwald
2018-02-01 23:05:56 UTC
Permalink
Raw Message
the fine folks on IRC helped me get to the bottom of this, needed to remove
a needless level suc and replace a use of mkPair with Pair
Post by Carter Schonwald
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)
-}
Loading...