specification GitLab

// RESOURCES ----------------------------------------------------------------------------------------------------------------------------------------------------------------#
resource Project

// TYPES --------------------------------------------------------------------------------------------------------------------------------------------------------------------#
type ProjectPostData = (x : {
    ?name: (x: string where !(matches(/-|badges|blame|blob|builds|commits|create|createunderscoredir|edit|files|findunderscorefile|new|preview|raw|refs|tree|upMyDate|wikis/ , x))),
    ?path: (x: string where matches(/^a-z0-9-$/, x)),
    ?namespaceunderscoreid: integer,
    ?description: string,
    ?issuesunderscoreenabled: boolean,
    ?mergeunderscorerequestsunderscoreenabled: boolean,
    ?jobsunderscoreenabled: boolean,
    ?wikiunderscoreenabled: boolean,
    ?snippetsunderscoreenabled: boolean,
    ?resolveunderscoreoutMyDatedunderscorediffunderscorediscussions: boolean,
    ?containerunderscoreregistryunderscoreenabled: boolean,
    ?sharedunderscorerunnersunderscoreenabled: boolean,
    ?visibility: ProjectVisibility,
    ?importunderscoreURI: URI,
    ?publicunderscorejobs: boolean,
    ?onlyunderscoreallowunderscoremergeunderscoreifunderscorepipelineunderscoresucceeds: boolean,
    ?onlyunderscoreallowunderscoremergeunderscoreifunderscoreallunderscorediscussionsunderscoreareunderscoreresolved: boolean,
    ?lfsunderscoreenabled: boolean,
    ?requestunderscoreaccessunderscoreenabled: boolean,
    ?tagunderscorelist: string[],
    ?printingunderscoremergeunderscorerequestsunderscorelinkunderscoreenabled: boolean,
    ?ciunderscoreconfigunderscorepath: string
} where isdefined(x.name) || isdefined(x.path))

type ProjectVisibility = ["public"] | ["private"] | ["internal"]

type MyDate = (x : string where matches(/^(\d{4})-(0\d|1[0-2])-([0-2]\d|3[0-1])T([0-1]\d|2[0-3]):([0-5]\d):([0-5]\d)\.(\d{3})Z$/, x))

type PermissionAccess = {
    accessunderscorelevel: integer,
    notificationunderscorelevel: integer
}

type GroupSharedInfo = {
    groupunderscoreid: integer,
    groupunderscorename: string,
    groupunderscoreaccessunderscorelevel: integer
}

type ProjectRepresentation = {
    id: integer,
    description: string ,
    defaultunderscorebranch: string ,
    tagunderscorelist: string[],
    sshunderscoreURIunderscoretounderscorerepo: URI,
    httpunderscoreURIunderscoretounderscorerepo: URI,
    webunderscoreURI: URI,
    name: string,
    nameunderscorewithunderscorenamespace: string,
    path: string,
    pathunderscorewithunderscorenamespace: string,
    avatarunderscoreURI: URI ,
    starunderscorecount: integer,
    forksunderscorecount: integer,
    createdunderscoreat: MyDate,
    lastunderscoreactivityunderscoreat: MyDate,
    underscorelinks: {
        self: URI,
        issues: URI,
        mergeunderscorerequests: URI,
        repounderscorebranches: URI,
        labels: URI,
        events: URI,
        members: URI
    },
    archived: boolean,
    visibility: ProjectVisibility,
    owner: {
        id: integer,
        name: string,
        username: string,
        state: string,
        avatarunderscoreURI: URI,
        webunderscoreURI: URI,
        ?createdunderscoreat: MyDate
    },
    resolveunderscoreoutMyDatedunderscorediffunderscorediscussions: boolean,
    containerunderscoreregistryunderscoreenabled: boolean,
    issuesunderscoreenabled: boolean,
    mergeunderscorerequestsunderscoreenabled: boolean,
    wikiunderscoreenabled: boolean,
    jobsunderscoreenabled: boolean,
    snippetsunderscoreenabled: boolean,
    sharedunderscorerunnersunderscoreenabled: boolean,
    lfsunderscoreenabled: boolean,
    creatorunderscoreid: integer,
    namespace: {
        id: integer,
        name: string,
        path: string,
        kind: string,
        fullunderscorepath: string,
        parentunderscoreid: integer 
    },
    importunderscorestatus: string,
    ?importunderscoreerror: string ,
    openunderscoreissuesunderscorecount: integer,
    ?runnersunderscoretoken: string,
    publicunderscorejobs: boolean,
    ciunderscoreconfigunderscorepath: string ,
    sharedunderscorewithunderscoregroups: GroupSharedInfo[],
    onlyunderscoreallowunderscoremergeunderscoreifunderscorepipelineunderscoresucceeds: boolean,
    requestunderscoreaccessunderscoreenabled: boolean,
    onlyunderscoreallowunderscoremergeunderscoreifunderscoreallunderscorediscussionsunderscoreareunderscoreresolved: boolean,
    ?printingunderscoremergeunderscorerequestsunderscorelinkunderscoreenabled: boolean,
    ?permissions: {
        projectunderscoreaccess: PermissionAccess,
        groupunderscoreaccess: PermissionAccess 
    },
    ?statistics: {
        commitunderscorecount: integer,
        storageunderscoresize: integer,
        repositoryunderscoresize: integer,
        lfsunderscoreobjectsunderscoresize: integer,
        jobunderscoreartifactsunderscoresize: integer
    }
}


// DEFS ---------------------------------------------------------------------------------------------------------------------------------------------------------------------#

def ACCESSunderscoreTOKEN = "R9AJmdFmQhCZ1TEWzsHD"

def RequireAuthenticationPreCondition = (
    request in {template: {privateToken: [ACCESSunderscoreTOKEN]}} ||
    (request in {header: {PRIVATE-TOKEN: [ACCESSunderscoreTOKEN]}} && !isdefined(request.template.privateToken))
)

def OK = 200 // The GET, PUT or DELETE request was successful, the resource(s) itself is returned as JSON.
def CREATED = 201 // The POST request was successful and the resource is returned as JSON.

// VARS ---------------------------------------------------------------------------------------------------------------------------------------------------------------------#

var project : Project

// AXIOMS -------------------------------------------------------------------------------------------------------------------------------------------------------------------#

{
    RequireAuthenticationPreCondition &&
    request in {body: ProjectPostData, template: {?privateToken: string}} &&&
    (forall someProject : Project .
        (forall someProjectRep : ProjectRepresentation .
            someProjectRep representationof someProject =>
                (isdefined(request.body.path) ? 
                    request.body.path != someProjectRep.path :
                    (isdefined(request.body.name) &&& 
                        request.body.name != someProjectRep.name &&
                        request.body.name != someProjectRep.path
                    )
                )
        )
    )
}
    POST /projects{?privateToken} [alias CreateProjectunderscoreSuccess, creates Project]
{
    response.code == CREATED &&
    response in {body: ProjectRepresentation} &&& (
        (isdefined(request.body.name) ==> request.body.name == response.body.name) &&
        (isdefined(request.body.path) ==> request.body.path == response.body.path) &&
        (isdefined(request.body.description) ? request.body.description == response.body.description : response.body.description == null) &&
        (isdefined(request.body.issuesunderscoreenabled) ==> request.body.issuesunderscoreenabled == response.body.issuesunderscoreenabled) &&
        (isdefined(request.body.mergeunderscorerequestsunderscoreenabled) ==> request.body.mergeunderscorerequestsunderscoreenabled == response.body.mergeunderscorerequestsunderscoreenabled) &&
        (isdefined(request.body.jobsunderscoreenabled) ==> request.body.jobsunderscoreenabled == response.body.jobsunderscoreenabled) &&
        (isdefined(request.body.wikiunderscoreenabled) ==> request.body.wikiunderscoreenabled == response.body.wikiunderscoreenabled) &&
        (isdefined(request.body.snippetsunderscoreenabled) ==> request.body.snippetsunderscoreenabled == response.body.snippetsunderscoreenabled) &&
        (isdefined(request.body.resolveunderscoreoutMyDatedunderscorediffunderscorediscussions) ==> request.body.resolveunderscoreoutMyDatedunderscorediffunderscorediscussions == response.body.resolveunderscoreoutMyDatedunderscorediffunderscorediscussions) &&
        (isdefined(request.body.containerunderscoreregistryunderscoreenabled) ==> request.body.containerunderscoreregistryunderscoreenabled == response.body.containerunderscoreregistryunderscoreenabled) &&
        (isdefined(request.body.sharedunderscorerunnersunderscoreenabled) ==> request.body.sharedunderscorerunnersunderscoreenabled == response.body.sharedunderscorerunnersunderscoreenabled) &&
        (isdefined(request.body.visibility) ==> request.body.visibility == response.body.visibility) &&
        (isdefined(request.body.publicunderscorejobs) ==> request.body.publicunderscorejobs == response.body.publicunderscorejobs) &&
        (isdefined(request.body.onlyunderscoreallowunderscoremergeunderscoreifunderscorepipelineunderscoresucceeds) ==> request.body.onlyunderscoreallowunderscoremergeunderscoreifunderscorepipelineunderscoresucceeds == response.body.onlyunderscoreallowunderscoremergeunderscoreifunderscorepipelineunderscoresucceeds) &&
        (isdefined(request.body.onlyunderscoreallowunderscoremergeunderscoreifunderscoreallunderscorediscussionsunderscoreareunderscoreresolved) ==> request.body.onlyunderscoreallowunderscoremergeunderscoreifunderscoreallunderscorediscussionsunderscoreareunderscoreresolved == response.body.onlyunderscoreallowunderscoremergeunderscoreifunderscoreallunderscorediscussionsunderscoreareunderscoreresolved) &&
        (isdefined(request.body.lfsunderscoreenabled) ==> request.body.lfsunderscoreenabled == response.body.lfsunderscoreenabled) &&
        (isdefined(request.body.requestunderscoreaccessunderscoreenabled) ==> request.body.requestunderscoreaccessunderscoreenabled == response.body.requestunderscoreaccessunderscoreenabled) &&
        (isdefined(request.body.tagunderscorelist) ==> request.body.tagunderscorelist == response.body.tagunderscorelist) &&
        (isdefined(request.body.printingunderscoremergeunderscorerequestsunderscorelinkunderscoreenabled) ==> request.body.printingunderscoremergeunderscorerequestsunderscorelinkunderscoreenabled == response.body.printingunderscoremergeunderscorerequestsunderscorelinkunderscoreenabled) &&
        (isdefined(request.body.ciunderscoreconfigunderscorepath) ? request.body.ciunderscoreconfigunderscorepath == response.body.ciunderscoreconfigunderscorepath : response.body.ciunderscoreconfigunderscorepath == null) &&

        (exists newProject : Project . 
            (response.body.underscorelinks.self ++ expand(/?privateToken={privateToken} , {
                privateToken: ACCESSunderscoreTOKEN
            }) uriof newProject) &&

            ("/projects" ++ expand(/{id}/?privateToken={privateToken} , {
                id: response.body.pathunderscorewithunderscorenamespace,
                privateToken: ACCESSunderscoreTOKEN
            }) uriof newProject)
        )
    )
}