Skip to content

Commit 6244539

Browse files
denisecasedenisecase
committed
folders
1 parent 0197af2 commit 6244539

45 files changed

Lines changed: 377 additions & 291 deletions

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎EvolutionProtocol.lean‎

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
import EvolutionProtocol.Conformance
2+
import EvolutionProtocol.Core
3+
import EvolutionProtocol.Graph
4+
import EvolutionProtocol.Spec
5+
6+
/-!
7+
REQ.PUBLIC.SURFACE:
8+
Canonical public import surface for this package.
9+
Do not add any declarations here.
10+
Do not add empty namespaces.
11+
12+
WHY:
13+
Downstream projects should have exactly one stable import path for this repo.
14+
15+
OBS:
16+
- This module re-exports the intended public modules by importing them.
17+
- It must not define placeholder namespaces.
18+
- All exported declarations live in imported modules.
19+
-/

StructuralExplainability/EvolutionProtocol/Spec/Conformance.lean renamed to EvolutionProtocol/Conformance.lean

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
import StructuralExplainability.EvolutionProtocol.Spec.IdentifierMap
1+
import EvolutionProtocol.Spec.IdentifierMap
22

3-
namespace StructuralExplainability.EvolutionProtocol.Spec
3+
namespace EvolutionProtocol.Conformance
44

55
/-!
66
# EP Conformance Predicate (v1)
@@ -77,4 +77,4 @@ theorem conforms_of_mem (e : ConformanceEvidence) (p : Prop) :
7777
unfold Conforms at hconf
7878
exact andList_of_mem (ps := requirements e) (p := p) hmem hconf
7979

80-
end StructuralExplainability.EvolutionProtocol.Spec
80+
end EvolutionProtocol.Conformance

‎EvolutionProtocol/Core.lean‎

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
import EvolutionProtocol.Core.Base
2+
import EvolutionProtocol.Core.Model
3+
import EvolutionProtocol.Core.Record
4+
import EvolutionProtocol.Core.Shared
5+
6+
/-!
7+
REQ.PUBLIC.SURFACE:
8+
Canonical public import surface for this layer.
9+
Do not add any declarations here.
10+
Do not add empty namespaces.
11+
12+
WHY:
13+
Downstream layers should have exactly one stable import path for this layer.
14+
15+
OBS:
16+
- This module re-exports the intended public modules by importing them.
17+
- It must not define placeholder namespaces.
18+
- All exported declarations live in imported modules.
19+
-/

‎EvolutionProtocol/Core/Base.lean‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
import EvolutionProtocol.Core.Base.Ids
2+
import EvolutionProtocol.Core.Base.Primitives
3+
4+
/-!
5+
REQ.PUBLIC.SURFACE:
6+
Canonical public import surface for this layer.
7+
Do not add any declarations here.
8+
Do not add empty namespaces.
9+
10+
WHY:
11+
Downstream layers should have exactly one stable import path for this layer.
12+
13+
OBS:
14+
- This module re-exports the intended public modules by importing them.
15+
- It must not define placeholder namespaces.
16+
- All exported declarations live in imported modules.
17+
-/

StructuralExplainability/EvolutionProtocol/Core/Base/Ids.lean renamed to EvolutionProtocol/Core/Base/Ids.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
namespace StructuralExplainability.EvolutionProtocol.Core.Base
1+
namespace EvolutionProtocol.Core.Base
22

33
/-!
44
REQ:
@@ -14,4 +14,4 @@ abbrev RelationshipId := String
1414
abbrev EvolutionId := String
1515
abbrev ConsentId := String
1616

17-
end StructuralExplainability.EvolutionProtocol.Core.Base
17+
end EvolutionProtocol.Core.Base

StructuralExplainability/EvolutionProtocol/Core/Base/Primitives.lean renamed to EvolutionProtocol/Core/Base/Primitives.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
namespace StructuralExplainability.EvolutionProtocol.Core.Base
1+
namespace EvolutionProtocol.Core.Base
22

33
/-!
44
REQ:
@@ -13,4 +13,4 @@ abbrev Uri := String
1313
abbrev DateTime := String
1414
abbrev Sha256 := String
1515

16-
end StructuralExplainability.EvolutionProtocol.Core.Base
16+
end EvolutionProtocol.Core.Base

‎EvolutionProtocol/Core/Model.lean‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
import EvolutionProtocol.Core.Model.Consent
2+
import EvolutionProtocol.Core.Model.IdentifierScheme
3+
import EvolutionProtocol.Core.Model.Retention
4+
5+
/-!
6+
REQ.PUBLIC.SURFACE:
7+
Canonical public import surface for this layer.
8+
Do not add any declarations here.
9+
Do not add empty namespaces.
10+
11+
WHY:
12+
Downstream layers should have exactly one stable import path for this layer.
13+
14+
OBS:
15+
- This module re-exports the intended public modules by importing them.
16+
- It must not define placeholder namespaces.
17+
- All exported declarations live in imported modules.
18+
-/

StructuralExplainability/EvolutionProtocol/Core/Model/Consent.lean renamed to EvolutionProtocol/Core/Model/Consent.lean

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
import StructuralExplainability.EvolutionProtocol.Core.Base.Ids
1+
import EvolutionProtocol.Core.Base.Ids
22

3-
namespace StructuralExplainability.EvolutionProtocol.Core.Model
3+
namespace EvolutionProtocol.Core.Model
44

55
/-!
66
REQ:
@@ -21,8 +21,8 @@ inductive ConsentState where
2121

2222
/-- Consent record (scaffold). -/
2323
structure Consent where
24-
id : StructuralExplainability.EvolutionProtocol.Core.Base.ConsentId
24+
id : EvolutionProtocol.Core.Base.ConsentId
2525
state : ConsentState
2626
deriving Repr, BEq, DecidableEq
2727

28-
end StructuralExplainability.EvolutionProtocol.Core.Model
28+
end EvolutionProtocol.Core.Model

StructuralExplainability/EvolutionProtocol/Core/Model/IdentifierScheme.lean renamed to EvolutionProtocol/Core/Model/IdentifierScheme.lean

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
import StructuralExplainability.EvolutionProtocol.Core.Base.Primitives
1+
import EvolutionProtocol.Core.Base.Primitives
22

3-
namespace StructuralExplainability.EvolutionProtocol.Core.Model
3+
namespace EvolutionProtocol.Core.Model
44

55
/-!
66
REQ:
@@ -29,4 +29,4 @@ structure Identifier where
2929
def Identifier.toString (i : Identifier) : String :=
3030
s!"{repr i.scheme}:{i.value}"
3131

32-
end StructuralExplainability.EvolutionProtocol.Core.Model
32+
end EvolutionProtocol.Core.Model

StructuralExplainability/EvolutionProtocol/Core/Model/Retention.lean renamed to EvolutionProtocol/Core/Model/Retention.lean

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
import StructuralExplainability.EvolutionProtocol.Core.Base.Ids
1+
import EvolutionProtocol.Core.Base.Ids
22

3-
namespace StructuralExplainability.EvolutionProtocol.Core.Model
3+
namespace EvolutionProtocol.Core.Model
44

55
/-!
66
REQ:
@@ -39,7 +39,7 @@ structure RetentionPolicy (TimePoint : Type) where
3939
period : Option (TimeInterval TimePoint) := none
4040
reviewBy : Option TimePoint := none
4141
consentId :
42-
Option StructuralExplainability.EvolutionProtocol.Core.Base.ConsentId := none
42+
Option EvolutionProtocol.Core.Base.ConsentId := none
4343
deriving Repr, BEq, DecidableEq
4444

4545

@@ -58,7 +58,7 @@ def RetentionExpired
5858
(policy : RetentionPolicy TimePoint)
5959
(_now : TimePoint)
6060
(consentWithdrawn :
61-
StructuralExplainability.EvolutionProtocol.Core.Base.ConsentId -> Prop)
61+
EvolutionProtocol.Core.Base.ConsentId -> Prop)
6262
(legalEnded : Prop := False)
6363
(contractEnded : Prop := False)
6464
(interestEnded : Prop := False)
@@ -83,8 +83,8 @@ theorem retention_expired_of_consent_withdrawn
8383
(policy : RetentionPolicy TimePoint)
8484
(now : TimePoint)
8585
(consentWithdrawn :
86-
StructuralExplainability.EvolutionProtocol.Core.Base.ConsentId -> Prop)
87-
(c : StructuralExplainability.EvolutionProtocol.Core.Base.ConsentId)
86+
EvolutionProtocol.Core.Base.ConsentId -> Prop)
87+
(c : EvolutionProtocol.Core.Base.ConsentId)
8888
(hbasis : policy.basis = RetentionBasis.consentBased)
8989
(hcid : policy.consentId = some c)
9090
(hwd : consentWithdrawn c)
@@ -93,4 +93,4 @@ theorem retention_expired_of_consent_withdrawn
9393
unfold RetentionExpired
9494
simp [hbasis, hcid, hwd]
9595

96-
end StructuralExplainability.EvolutionProtocol.Core.Model
96+
end EvolutionProtocol.Core.Model

0 commit comments

Comments
 (0)