spectrum.paws.getSpectrum

valid {
    input.Body.antenna.height == NUMBER
    input.Body.antenna.heightType == STRING
    input.Body.antenna.heightUncertainty == NUMBER
    input.Body.capabilities.frequencyRanges[_].channelId == STRING
    input.Body.capabilities.frequencyRanges[_].maxPowerDBm == NUMBER
    input.Body.capabilities.frequencyRanges[_].startHz == NUMBER
    input.Body.capabilities.frequencyRanges[_].stopHz == NUMBER
    input.Body.deviceDesc.etsiEnDeviceCategory == STRING
    input.Body.deviceDesc.etsiEnDeviceEmissionsClass == STRING
    input.Body.deviceDesc.etsiEnDeviceType == STRING
    input.Body.deviceDesc.etsiEnTechnologyId == STRING
    input.Body.deviceDesc.fccId == STRING
    input.Body.deviceDesc.fccTvbdDeviceType == STRING
    input.Body.deviceDesc.manufacturerId == STRING
    input.Body.deviceDesc.modelId == STRING
    input.Body.deviceDesc.rulesetIds[_] == STRING
    input.Body.deviceDesc.serialNumber == STRING
    input.Body.location.confidence == INTEGER
    input.Body.location.point.center.latitude == NUMBER
    input.Body.location.point.center.longitude == NUMBER
    input.Body.location.point.orientation == NUMBER
    input.Body.location.point.semiMajorAxis == NUMBER
    input.Body.location.point.semiMinorAxis == NUMBER
    input.Body.location.region.exterior[_].latitude == NUMBER
    input.Body.location.region.exterior[_].longitude == NUMBER
    input.Body.masterDeviceDesc.etsiEnDeviceCategory == STRING
    input.Body.masterDeviceDesc.etsiEnDeviceEmissionsClass == STRING
    input.Body.masterDeviceDesc.etsiEnDeviceType == STRING
    input.Body.masterDeviceDesc.etsiEnTechnologyId == STRING
    input.Body.masterDeviceDesc.fccId == STRING
    input.Body.masterDeviceDesc.fccTvbdDeviceType == STRING
    input.Body.masterDeviceDesc.manufacturerId == STRING
    input.Body.masterDeviceDesc.modelId == STRING
    input.Body.masterDeviceDesc.rulesetIds[_] == STRING
    input.Body.masterDeviceDesc.serialNumber == STRING
    input.Body.owner.operator.adr.code == STRING
    input.Body.owner.operator.adr.country == STRING
    input.Body.owner.operator.adr.locality == STRING
    input.Body.owner.operator.adr.pobox == STRING
    input.Body.owner.operator.adr.region == STRING
    input.Body.owner.operator.adr.street == STRING
    input.Body.owner.operator.email.text == STRING
    input.Body.owner.operator.fn == STRING
    input.Body.owner.operator.org.text == STRING
    input.Body.owner.operator.tel.uri == STRING
    input.Body.owner.owner.adr.code == STRING
    input.Body.owner.owner.adr.country == STRING
    input.Body.owner.owner.adr.locality == STRING
    input.Body.owner.owner.adr.pobox == STRING
    input.Body.owner.owner.adr.region == STRING
    input.Body.owner.owner.adr.street == STRING
    input.Body.owner.owner.email.text == STRING
    input.Body.owner.owner.fn == STRING
    input.Body.owner.owner.org.text == STRING
    input.Body.owner.owner.tel.uri == STRING
    input.Body.requestType == STRING
    input.Body.type == STRING
    input.Body.version == STRING
    input.ProviderMetadata.Region == STRING
}

spectrum.paws.getSpectrumBatch

valid {
    input.Body.antenna.height == NUMBER
    input.Body.antenna.heightType == STRING
    input.Body.antenna.heightUncertainty == NUMBER
    input.Body.capabilities.frequencyRanges[_].channelId == STRING
    input.Body.capabilities.frequencyRanges[_].maxPowerDBm == NUMBER
    input.Body.capabilities.frequencyRanges[_].startHz == NUMBER
    input.Body.capabilities.frequencyRanges[_].stopHz == NUMBER
    input.Body.deviceDesc.etsiEnDeviceCategory == STRING
    input.Body.deviceDesc.etsiEnDeviceEmissionsClass == STRING
    input.Body.deviceDesc.etsiEnDeviceType == STRING
    input.Body.deviceDesc.etsiEnTechnologyId == STRING
    input.Body.deviceDesc.fccId == STRING
    input.Body.deviceDesc.fccTvbdDeviceType == STRING
    input.Body.deviceDesc.manufacturerId == STRING
    input.Body.deviceDesc.modelId == STRING
    input.Body.deviceDesc.rulesetIds[_] == STRING
    input.Body.deviceDesc.serialNumber == STRING
    input.Body.locations[_].confidence == INTEGER
    input.Body.locations[_].point.center.latitude == NUMBER
    input.Body.locations[_].point.center.longitude == NUMBER
    input.Body.locations[_].point.orientation == NUMBER
    input.Body.locations[_].point.semiMajorAxis == NUMBER
    input.Body.locations[_].point.semiMinorAxis == NUMBER
    input.Body.locations[_].region.exterior[_].latitude == NUMBER
    input.Body.locations[_].region.exterior[_].longitude == NUMBER
    input.Body.masterDeviceDesc.etsiEnDeviceCategory == STRING
    input.Body.masterDeviceDesc.etsiEnDeviceEmissionsClass == STRING
    input.Body.masterDeviceDesc.etsiEnDeviceType == STRING
    input.Body.masterDeviceDesc.etsiEnTechnologyId == STRING
    input.Body.masterDeviceDesc.fccId == STRING
    input.Body.masterDeviceDesc.fccTvbdDeviceType == STRING
    input.Body.masterDeviceDesc.manufacturerId == STRING
    input.Body.masterDeviceDesc.modelId == STRING
    input.Body.masterDeviceDesc.rulesetIds[_] == STRING
    input.Body.masterDeviceDesc.serialNumber == STRING
    input.Body.owner.operator.adr.code == STRING
    input.Body.owner.operator.adr.country == STRING
    input.Body.owner.operator.adr.locality == STRING
    input.Body.owner.operator.adr.pobox == STRING
    input.Body.owner.operator.adr.region == STRING
    input.Body.owner.operator.adr.street == STRING
    input.Body.owner.operator.email.text == STRING
    input.Body.owner.operator.fn == STRING
    input.Body.owner.operator.org.text == STRING
    input.Body.owner.operator.tel.uri == STRING
    input.Body.owner.owner.adr.code == STRING
    input.Body.owner.owner.adr.country == STRING
    input.Body.owner.owner.adr.locality == STRING
    input.Body.owner.owner.adr.pobox == STRING
    input.Body.owner.owner.adr.region == STRING
    input.Body.owner.owner.adr.street == STRING
    input.Body.owner.owner.email.text == STRING
    input.Body.owner.owner.fn == STRING
    input.Body.owner.owner.org.text == STRING
    input.Body.owner.owner.tel.uri == STRING
    input.Body.requestType == STRING
    input.Body.type == STRING
    input.Body.version == STRING
    input.ProviderMetadata.Region == STRING
}

spectrum.paws.init

valid {
    input.Body.deviceDesc.etsiEnDeviceCategory == STRING
    input.Body.deviceDesc.etsiEnDeviceEmissionsClass == STRING
    input.Body.deviceDesc.etsiEnDeviceType == STRING
    input.Body.deviceDesc.etsiEnTechnologyId == STRING
    input.Body.deviceDesc.fccId == STRING
    input.Body.deviceDesc.fccTvbdDeviceType == STRING
    input.Body.deviceDesc.manufacturerId == STRING
    input.Body.deviceDesc.modelId == STRING
    input.Body.deviceDesc.rulesetIds[_] == STRING
    input.Body.deviceDesc.serialNumber == STRING
    input.Body.location.confidence == INTEGER
    input.Body.location.point.center.latitude == NUMBER
    input.Body.location.point.center.longitude == NUMBER
    input.Body.location.point.orientation == NUMBER
    input.Body.location.point.semiMajorAxis == NUMBER
    input.Body.location.point.semiMinorAxis == NUMBER
    input.Body.location.region.exterior[_].latitude == NUMBER
    input.Body.location.region.exterior[_].longitude == NUMBER
    input.Body.type == STRING
    input.Body.version == STRING
    input.ProviderMetadata.Region == STRING
}

spectrum.paws.notifySpectrumUse

valid {
    input.Body.deviceDesc.etsiEnDeviceCategory == STRING
    input.Body.deviceDesc.etsiEnDeviceEmissionsClass == STRING
    input.Body.deviceDesc.etsiEnDeviceType == STRING
    input.Body.deviceDesc.etsiEnTechnologyId == STRING
    input.Body.deviceDesc.fccId == STRING
    input.Body.deviceDesc.fccTvbdDeviceType == STRING
    input.Body.deviceDesc.manufacturerId == STRING
    input.Body.deviceDesc.modelId == STRING
    input.Body.deviceDesc.rulesetIds[_] == STRING
    input.Body.deviceDesc.serialNumber == STRING
    input.Body.location.confidence == INTEGER
    input.Body.location.point.center.latitude == NUMBER
    input.Body.location.point.center.longitude == NUMBER
    input.Body.location.point.orientation == NUMBER
    input.Body.location.point.semiMajorAxis == NUMBER
    input.Body.location.point.semiMinorAxis == NUMBER
    input.Body.location.region.exterior[_].latitude == NUMBER
    input.Body.location.region.exterior[_].longitude == NUMBER
    input.Body.spectra[_].bandwidth == NUMBER
    input.Body.spectra[_].frequencyRanges[_].channelId == STRING
    input.Body.spectra[_].frequencyRanges[_].maxPowerDBm == NUMBER
    input.Body.spectra[_].frequencyRanges[_].startHz == NUMBER
    input.Body.spectra[_].frequencyRanges[_].stopHz == NUMBER
    input.Body.type == STRING
    input.Body.version == STRING
    input.ProviderMetadata.Region == STRING
}

spectrum.paws.register

valid {
    input.Body.antenna.height == NUMBER
    input.Body.antenna.heightType == STRING
    input.Body.antenna.heightUncertainty == NUMBER
    input.Body.deviceDesc.etsiEnDeviceCategory == STRING
    input.Body.deviceDesc.etsiEnDeviceEmissionsClass == STRING
    input.Body.deviceDesc.etsiEnDeviceType == STRING
    input.Body.deviceDesc.etsiEnTechnologyId == STRING
    input.Body.deviceDesc.fccId == STRING
    input.Body.deviceDesc.fccTvbdDeviceType == STRING
    input.Body.deviceDesc.manufacturerId == STRING
    input.Body.deviceDesc.modelId == STRING
    input.Body.deviceDesc.rulesetIds[_] == STRING
    input.Body.deviceDesc.serialNumber == STRING
    input.Body.deviceOwner.operator.adr.code == STRING
    input.Body.deviceOwner.operator.adr.country == STRING
    input.Body.deviceOwner.operator.adr.locality == STRING
    input.Body.deviceOwner.operator.adr.pobox == STRING
    input.Body.deviceOwner.operator.adr.region == STRING
    input.Body.deviceOwner.operator.adr.street == STRING
    input.Body.deviceOwner.operator.email.text == STRING
    input.Body.deviceOwner.operator.fn == STRING
    input.Body.deviceOwner.operator.org.text == STRING
    input.Body.deviceOwner.operator.tel.uri == STRING
    input.Body.deviceOwner.owner.adr.code == STRING
    input.Body.deviceOwner.owner.adr.country == STRING
    input.Body.deviceOwner.owner.adr.locality == STRING
    input.Body.deviceOwner.owner.adr.pobox == STRING
    input.Body.deviceOwner.owner.adr.region == STRING
    input.Body.deviceOwner.owner.adr.street == STRING
    input.Body.deviceOwner.owner.email.text == STRING
    input.Body.deviceOwner.owner.fn == STRING
    input.Body.deviceOwner.owner.org.text == STRING
    input.Body.deviceOwner.owner.tel.uri == STRING
    input.Body.location.confidence == INTEGER
    input.Body.location.point.center.latitude == NUMBER
    input.Body.location.point.center.longitude == NUMBER
    input.Body.location.point.orientation == NUMBER
    input.Body.location.point.semiMajorAxis == NUMBER
    input.Body.location.point.semiMinorAxis == NUMBER
    input.Body.location.region.exterior[_].latitude == NUMBER
    input.Body.location.region.exterior[_].longitude == NUMBER
    input.Body.type == STRING
    input.Body.version == STRING
    input.ProviderMetadata.Region == STRING
}

spectrum.paws.verifyDevice

valid {
    input.Body.deviceDescs[_].etsiEnDeviceCategory == STRING
    input.Body.deviceDescs[_].etsiEnDeviceEmissionsClass == STRING
    input.Body.deviceDescs[_].etsiEnDeviceType == STRING
    input.Body.deviceDescs[_].etsiEnTechnologyId == STRING
    input.Body.deviceDescs[_].fccId == STRING
    input.Body.deviceDescs[_].fccTvbdDeviceType == STRING
    input.Body.deviceDescs[_].manufacturerId == STRING
    input.Body.deviceDescs[_].modelId == STRING
    input.Body.deviceDescs[_].rulesetIds[_] == STRING
    input.Body.deviceDescs[_].serialNumber == STRING
    input.Body.type == STRING
    input.Body.version == STRING
    input.ProviderMetadata.Region == STRING
}