diff --git a/dag/extdeps/network/arista_7050s_52.dag b/dag/extdeps/network/arista_7050s_52.dag new file mode 100644 index 00000000000..a5e65f24211 --- /dev/null +++ b/dag/extdeps/network/arista_7050s_52.dag @@ -0,0 +1,278 @@ +module extdeps.network.arista_7050s_52 + +import std.types { Bool, Int, List, NonEmptyStr } +import std.measure { + Bandwidth, bandwidth, + ByteSize, byte_size, byte_size_count, + PacketRate, packet_rate, packet_rate_count, + Percent, percent, percent_count, + Watt, watt, + Milliwatt, milliwatt, + Volt, volt, + Millimeter, millimeter, + Celsius, celsius, + Gigabyte, gigabyte, + Mebibyte, mebibyte, + Nanosecond, nanosecond, +} +import std.decl_ref { DeclarationRef, WholeDeclaration } +import extdeps.network.switch_types { NetworkSwitchCatalogRow, SwitchPortGroup, TrackedGap } +import extdeps.vendor.arista { arista } +import extdeps.vendor { Vendor } +import extdeps.hardware { Hardware } +import extdeps.external_authority { ExternalAuthority, ExternalModelScope, ExternalSubjectRef } +import extdeps.uri { Uri, Https } +import v2.std.optional { Present } + +// THE DCS-7050S-52, ARISTA'S 52-PORT 1/10GBE SFP+ SWITCH IN THE 7050 SERIES. Modelled from the +// Arista 7050S datasheet read 2026-09-03. The canonical authority is the datasheet at +// arista.com; its bytes were fetched via a third-party mirror (spectra.com hosts the same +// document) because arista.com served a JavaScript challenge to this session's client -- the +// citation is the route to the publisher's document, and the document's identity is carried in +// arista7050s_datasheet below. +// +// THE -52 AND THE -64 ARE TWO SUBJECTS ON ONE DATASHEET, AND THE CONFUSION IS COMMON ENOUGH TO +// STATE. The datasheet's overview reads: "The 7050S-64 switch offers 48 SFP+ and 4 QSFP+ +// interfaces while the 7050S-52 switch offers 52 SFP+ interfaces." The DCS-7050S-52 therefore +// carries FIFTY-TWO 1/10GbE SFP+ ports and NO QSFP+ ports; several reseller listings describe a +// "48 SFP+ + 4 QSFP+" 7050S-52, which is the -64's port map read onto the wrong model number. +// This module models the datasheet's -52 row, and the seller's listing for the operator's +// purchase is cited nowhere because it adds no product fact the datasheet does not carry. +// +// PROCUREMENT IS NOT A VENDOR FACT. The operator purchased this switch on eBay (order +// 15-15103-52948, 2026-09-01); that purchase is a workflow/ops fact whose home is the fleet and +// procurement layer, not extdeps. The listing's "240V 60Hz" is inside the datasheet's 100-240 V +// 50/60 Hz envelope and adds nothing to model. + +data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https + locator: "www.arista.com/assets/data/pdf/Datasheets/7050S_Datasheet.pdf" + } +} + +// The datasheet covers both 7050S-64 and 7050S-52; the row below is the -52 and says so at every +// field. Document identity is carried here so a later reader can resolve the citation without +// repeating the fetch. +data arista7050s_datasheet: NonEmptyStr = "7050S Datasheet, Arista 7050 Series 10/40G Data Center Switches, covering the 7050S-64 (48 SFP+ + 4 QSFP+) and the 7050S-52 (52 SFP+)" + +// ================= THE SHARED CATALOG ROW ================= + +data arista_7050s_52_catalog: NetworkSwitchCatalogRow = NetworkSwitchCatalogRow { + model: "DCS-7050S-52", + manufacturer: arista, + port_inventory: [ + SwitchPortGroup { + connector: "SFP+", + port_count: 52, + data_rates: [ + bandwidth(1000000000), + bandwidth(10000000000), + ], + }, + ], + fanless: false, + switching_capacity: Present { value: bandwidth(1040000000000) }, + max_power_draw: milliwatt(185000), +} + +// ================= THROUGHPUT AND LATENCY ================= + +// The datasheet's model-comparison table states the -52's throughput as 1.04 Terabits/second and +// 780 million packets per second, and the latency section states 800 to 1150 ns through the SFP+ +type Arista7050s52ThroughputFacts { + switching_capacity: Bandwidth + packet_rate: PacketRate + latency_min_ns: Nanosecond + latency_max_ns: Nanosecond +} + +data arista_7050s_52_throughput: Arista7050s52ThroughputFacts = Arista7050s52ThroughputFacts { + switching_capacity: bandwidth(1040000000000), + packet_rate: packet_rate(780000000), + latency_min_ns: nanosecond(800), + latency_max_ns: nanosecond(1150), +} + +// ================= PLATFORM ================= + +// The datasheet's "Resilient Control Plane" and model-comparison table carry the compute facts: +// dual-core x86 CPU, 4 GB DRAM, 2 GB flash, 9 MB dynamic packet buffer, and a factory-optional +// 50 GB SSD. The SSD is an OPTION, not a shipped default -- the field carries Present only +// because the option is factory-available, and the distinction is stated in the comment. +type Arista7050s52PlatformFacts { + cpu: NonEmptyStr + system_memory: Gigabyte + flash_storage: Gigabyte + packet_buffer: Mebibyte + optional_ssd: Gigabyte + operating_system: NonEmptyStr +} + +data arista_7050s_52_platform: Arista7050s52PlatformFacts = Arista7050s52PlatformFacts { + cpu: "Dual-Core x86", + system_memory: gigabyte(4), + flash_storage: gigabyte(2), + packet_buffer: mebibyte(9), + optional_ssd: gigabyte(50), + operating_system: "Arista EOS", +} + +// ================= MANAGEMENT PORTS ================= + +// One 100/1000 management port, one RS-232 (RJ-45) console port and one USB port are the +// datasheet's model-comparison rows for the -52. +type Arista7050s52ManagementFacts { + management_port: NonEmptyStr + console_port: NonEmptyStr + usb_ports: Int +} + +data arista_7050s_52_management: Arista7050s52ManagementFacts = Arista7050s52ManagementFacts { + management_port: "100/1000", + console_port: "RS-232 RJ-45", + usb_ports: 1, +} + +// ================= POWER AND COOLING ================= + +// The model-comparison table gives typical/max draw as 103/185 W for the -52, and the power +// supply table gives the AC envelope: 100-240 V, 2.2-5.3 A, 50/60 Hz, IEC 320-C13 input +// connector. High-availability rows: 2 hot-swap PSUs (1+1 redundant), 4 N+1 hot-swap fans, +// reversible airflow. +// The datasheet states "Input Current 2.2-5.3A"; no fractional Ampere measure exists in +// std.measure, so the vendor's own string is carried with the unit named, rather than a +// fabricated integer. +type Arista7050s52PowerFacts { + psu_count: Int + psu_hot_swap: Bool + psu_redundancy: NonEmptyStr + ac_input_range_min: Volt + ac_input_range_max: Volt + ac_input_current: NonEmptyStr + input_frequency: NonEmptyStr + input_connector: NonEmptyStr + typical_power_draw: Watt + max_power_draw: Watt +} + +data arista_7050s_52_power: Arista7050s52PowerFacts = Arista7050s52PowerFacts { + psu_count: 2, + psu_hot_swap: true, + psu_redundancy: "1+1 redundant", + ac_input_range_min: volt(100), + ac_input_range_max: volt(240), + ac_input_current: "2.2-5.3 A", + input_frequency: "50/60 Hz", + input_connector: "IEC 320-C13", + typical_power_draw: watt(103), + max_power_draw: watt(185), +} + +type Arista7050s52CoolingFacts { + fan_count: Int + fan_redundancy: NonEmptyStr + fan_hot_swap: Bool + reversible_airflow: Bool +} + +data arista_7050s_52_cooling: Arista7050s52CoolingFacts = Arista7050s52CoolingFacts { + fan_count: 4, + fan_redundancy: "N+1 redundant", + fan_hot_swap: true, + reversible_airflow: true, +} + +// ================= CHASSIS AND ENVIRONMENT ================= + +type Arista7050s52ChassisFacts { + length_mm: Millimeter + height_mm: Millimeter + depth_mm: Millimeter + operating_temp_min: Celsius + operating_temp_max: Celsius + storage_temp_min: Celsius + storage_temp_max: Celsius + relative_humidity_min: Percent + relative_humidity_max: Percent + operating_altitude_ft: Int +} + +data arista_7050s_52_chassis: Arista7050s52ChassisFacts = Arista7050s52ChassisFacts { + length_mm: millimeter(445), + height_mm: millimeter(44), + depth_mm: millimeter(406), + operating_temp_min: celsius(0), + operating_temp_max: celsius(40), + storage_temp_min: celsius(-40), + storage_temp_max: celsius(70), + relative_humidity_min: percent(5), + relative_humidity_max: percent(95), + operating_altitude_ft: 10000, +} + +// ================= SCALE ================= + +// The "Table Sizes" section of the datasheet. Carried as typed rows because these are the +// numbers a consumer would join a workload against. +type Arista7050s52ScaleFacts { + mac_addresses: Int + ipv4_routes_unicast: Int + ipv4_host_routes: Int + ipv6_routes_unicast: Int + ecmp_ways: Int + vlans: Int + jumbo_frame_size: ByteSize +} + +data arista_7050s_52_scale: Arista7050s52ScaleFacts = Arista7050s52ScaleFacts { + mac_addresses: 128000, + ipv4_routes_unicast: 16000, + ipv4_host_routes: 32000, + ipv6_routes_unicast: 8000, + ecmp_ways: 32, + vlans: 4096, + jumbo_frame_size: byte_size(9216), +} + +// ================= CROSS-CHECK AND OPEN GAPS ================= + +// The datasheet's own model-comparison table is the cross-check: the -52 row states "52xSFP+" +// ports, 1.04 Tbps throughput, 780 Mpps, 4 GB memory, 103/185 W draw -- and this module's rows +// carry exactly those figures. The one number that is carried as a plain Int (780,000,000) is +// the datasheet's own "780 Mpps", stated at the same precision. +data arista_7050s_52_open_gaps: List = [ + "The datasheet gives throughput in the model-comparison table only; no separate switching-capacity figure is published, so the two are the same number and that is stated, not derived.", + "Weight (17 lb / 7.71 kg) is published in the datasheet's physical-characteristics section but no Weight measure exists in std.measure; the figure is deliberately not modelled as a bare Int to avoid an untyped number, and a consumer that needs it should extend std.measure first.", + "The 7050S-52-F (front-to-rear) and 7050S-52-R (rear-to-front) airflow variants share this chassis row; the operator's order is for the base DCS-7050S-52 and the variant suffix, if any, will be read off the delivered unit.", +] + +data arista_7050s_52_tracked_gaps: List = [ + TrackedGap { + feature_tag: "extdeps-foot-length-scale", + dissolves_on: "std.measure adds a Scale arm for the international foot on the Length axis (a non-decimal, non-SI scale analogous to Minute's Sixty on Time)", + note: "operating_altitude_ft as bare Int with unit in field name. Same gate class as extdeps-hour-scale in extdeps.network.mikrotik_crs812.", + }, +] + +fn arista_7050s_52_gap_count() -> Int { + count(arista_7050s_52_open_gaps) +} + +fn arista_7050s_52_tracked_gap_count() -> Int { + count(arista_7050s_52_tracked_gaps) +} + +// ================= MODEL SCOPE ================= + +data extdeps_model_scope: ExternalModelScope = ExternalModelScope { + subject: ExternalSubjectRef { + declaration: DeclarationRef { + module_path: "extdeps.network.arista_7050s_52", + decl_name: "arista_7050s_52_catalog", + field: WholeDeclaration + } + }, + first_citation: extdeps_external_authority_anchor, + further_citations: [] +} diff --git a/dag/extdeps/network/mikrotik_crs812.dag b/dag/extdeps/network/mikrotik_crs812.dag new file mode 100644 index 00000000000..78cc18dd7e4 --- /dev/null +++ b/dag/extdeps/network/mikrotik_crs812.dag @@ -0,0 +1,362 @@ +module extdeps.network.mikrotik_crs812 + +import std.types { Bool, Int, List, NonEmptyStr, String } +import std.measure { + HardwareThreadCount, hardware_thread_count, hardware_thread_count_value, + CpuCoreCount, cpu_core_count, cpu_core_count_value, + PowerCordCount, power_cord_count, power_cord_count_value, + UsdWholeDollars, usd_whole_dollars, usd_whole_dollars_count, + Bandwidth, bandwidth, bandwidth_count, + BitWidth, bit_width, + Watt, watt, + Milliwatt, milliwatt, + Hertz, hertz, + Volt, volt, + Millimeter, millimeter, + Celsius, celsius, + Gigabyte, gigabyte, + Mebibyte, mebibyte, +} +import std.decl_ref { DeclarationRef, WholeDeclaration } +import extdeps.network.switch_types { NetworkSwitchCatalogRow, SwitchPortGroup, TrackedGap } +import extdeps.vendor.mikrotik { mikrotik } +import extdeps.vendor { Vendor } +import extdeps.hardware { Hardware } +import extdeps.external_authority { ExternalAuthority, ExternalModelScope, ExternalSubjectRef } +import extdeps.uri { Uri, Https } +import v2.std.optional { Absent } + +// THE CRS812-8DS-2DQ-2DDQ-RM, MIKROTIK'S 400G TOP-OF-RACK / LEAF SWITCH. This is the orderable +// rack-mount product code (the "RM" suffix); MikroTik markets the family as "CRS812 DDQ". +// Modelled from three first-party MikroTik documents read 2026-09-03: the product page +// (crs812_ddq), the RouterOS hardware manual page, and the product datasheet PDF. Every field +// below is a reading of one of those three, and where two of them disagree the disagreement is +// carried as two rows rather than smoothed over. +// +// WHY THIS MODULE IS ONE SUBJECT, NOT TWO: the port inventory and the platform are properties of +// one orderable part. A separate orderable accessory (400G DAC, optical transceiver) is a +// different subject with its own module when it is modelled. +// +// PROCUREMENT IS NOT A VENDOR FACT. The operator purchased this switch on eBay (order +// 22-15092-90152, 2026-09-02); that purchase is a workflow/ops fact whose home is the fleet and +// procurement layer (product.inventory), not extdeps -- the pattern fleet_physical_inventory +// states ("Amazon order IDs/URLs are procurement provenance, never asset identity"). The eBay +// listing is cited nowhere below because it adds no product fact the three first-party documents +// do not already carry. + +data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https + locator: "mikrotik.com/product/crs812_ddq" + } +} + +data crs812_manual_authority: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https + locator: "manual.mikrotik.com/hardware/crs812-8ds-2dq-2ddq-rm/" + } +} + +data crs812_datasheet_authority: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https + locator: "cdn.mikrotik.com/web-assets/product_files/CRS812-8DS-2DQ-2DDQ-RM_251055.pdf" + } +} + +// ================= THE SHARED CATALOG ROW ================= +// +// The port rates below are the vendor's own callouts, and the two Ethernet ports carry a +// subtlety worth stating: the product-page heading calls them "1G/2.5G/5G/10G" ports but the +// parenthetical -- echoed by the manual and the datasheet -- says supported rates are +// 10M/100M/1G/10G. The supported set is modelled, and the heading's 2.5G/5G is recorded as a +// vendor-side inconsistency (the heading calls 2.5G/5G rates the port does not support, +// recorded in crs812_open_gaps). The QSFP56-DD and QSFP56 port +// rates are the datasheet's "40G/50G/100G/200G/400G" and "40G/50G/100G/200G" callouts. +data crs812_catalog: NetworkSwitchCatalogRow = NetworkSwitchCatalogRow { + model: "CRS812-8DS-2DQ-2DDQ-RM", + manufacturer: mikrotik, + port_inventory: [ + SwitchPortGroup { + connector: "RJ45", + port_count: 2, + data_rates: [ + bandwidth(10000000), + bandwidth(100000000), + bandwidth(1000000000), + bandwidth(10000000000), + ], + }, + SwitchPortGroup { + connector: "SFP56", + port_count: 8, + data_rates: [ + bandwidth(1000000000), + bandwidth(2500000000), + bandwidth(5000000000), + bandwidth(10000000000), + bandwidth(25000000000), + bandwidth(50000000000), + ], + }, + SwitchPortGroup { + connector: "QSFP56", + port_count: 2, + data_rates: [ + bandwidth(40000000000), + bandwidth(50000000000), + bandwidth(100000000000), + bandwidth(200000000000), + ], + }, + SwitchPortGroup { + connector: "QSFP56-DD", + port_count: 2, + data_rates: [ + bandwidth(40000000000), + bandwidth(50000000000), + bandwidth(100000000000), + bandwidth(200000000000), + bandwidth(400000000000), + ], + }, + ], + fanless: false, + switching_capacity: Absent, + max_power_draw: milliwatt(134000), +} + +// MIKROTIK DOES NOT PUBLISH A SWITCHING CAPACITY for this model, on the product page or the +// datasheet. `Absent` is the honest row; a derived figure would be a fabricated fact, and the +// witness asserts the absence. + +// ================= PLATFORM ================= + +type Crs812PlatformFacts { + cpu_model: NonEmptyStr + cpu_architecture: NonEmptyStr + cpu_core_count: CpuCoreCount + cpu_thread_count: HardwareThreadCount + cpu_nominal_frequency: Hertz + switch_chip_model: NonEmptyStr + ram: Gigabyte + ram_type: NonEmptyStr + storage: Mebibyte + storage_type: NonEmptyStr + operating_system: NonEmptyStr + routeros_license_level: Int +} + +data crs812_platform: Crs812PlatformFacts = Crs812PlatformFacts { + cpu_model: "AL52400", + cpu_architecture: "ARM 64bit", + cpu_core_count: cpu_core_count(4), + cpu_thread_count: hardware_thread_count(4), + cpu_nominal_frequency: hertz(2000000000), + switch_chip_model: "98DX7335", + ram: gigabyte(4), + ram_type: "DDR4", + storage: mebibyte(512), + storage_type: "NAND", + operating_system: "RouterOS v7", + routeros_license_level: 6, +} + +// ================= POWER ================= + +// The product page and the manual agree on the powering envelope: two AC input slots, 100-240 V, +// 50-60 Hz, dual-redundant hot-swap PSUs. The manual states the PSU rating (250 W) and the input +// current (7 A max) that the product page leaves out. "Without attachments" is the product page's +// own figure -- the manual restates it as "maximum power consumption without attachments is 81 W". +type Crs812PowerFacts { + ac_input_count: Int + ac_input_range_min: Volt + ac_input_range_max: Volt + input_frequency: NonEmptyStr + psu_slot_count: Int + psu_rating: Watt + psu_hot_swap: Bool + max_power_draw: Watt + max_power_draw_without_attachments: Watt +} + +data crs812_power: Crs812PowerFacts = Crs812PowerFacts { + ac_input_count: 2, + ac_input_range_min: volt(100), + ac_input_range_max: volt(240), + input_frequency: "50-60 Hz", + psu_slot_count: 2, + psu_rating: watt(250), + psu_hot_swap: true, + max_power_draw: watt(134), + max_power_draw_without_attachments: watt(81), +} + +// ================= COOLING ================= + +type Crs812CoolingFacts { + fan_count: Int + fan_hot_swap: Bool +} + +data crs812_cooling: Crs812CoolingFacts = Crs812CoolingFacts { + fan_count: 4, + fan_hot_swap: true, +} + +// ================= CHASSIS ================= + +// THE DEPTH IS WHERE THE TWO FIRST-PARTY DOCUMENTS DISAGREE, AND THE DISAGREEMENT IS CARRIED +// RATHER THAN RESOLVED. The RouterOS hardware manual reads "443 x 156 x 44 mm"; the product +// datasheet PDF reads "443 x 268 x 44 mm". 156 mm is a plausible bare-chassis depth and 268 mm +// a plausible rack-mount depth with ears and PSUs, but neither document says which it measured, +// so neither figure is promoted to the canonical row and a reader sees both readings with their +// sources. The length and height agree across both documents. +type Crs812Dimensions { + length_mm: Millimeter + depth_mm: Millimeter + height_mm: Millimeter + source: ExternalAuthority +} + +data crs812_dimensions_manual: Crs812Dimensions = Crs812Dimensions { + length_mm: millimeter(443), + depth_mm: millimeter(156), + height_mm: millimeter(44), + source: crs812_manual_authority, +} + +data crs812_dimensions_datasheet: Crs812Dimensions = Crs812Dimensions { + length_mm: millimeter(443), + depth_mm: millimeter(268), + height_mm: millimeter(44), + source: crs812_datasheet_authority, +} + +// MTBF is a duration measured in hours. No Hour type exists at the Scale level (Minute uses the +// Sixty prefix; Hour would need Sixty*Sixty = 3600, which no existing Scale arm provides). +// A correct Hour type requires adding a new Scale arm, which is a load-bearing std change and +// its own PR. The figure is therefore carried as a bare Int with the unit in the field name +// (mtbf_hours). Same class as feature:extdeps-foot-length-scale in extdeps.network.arista_7050s_52. +// See crs812_tracked_gaps below for the dissolution condition. +type Crs812EnvironmentalFacts { + operating_temp_min: Celsius + operating_temp_max: Celsius + mtbf_hours: Int + certification: List + ip_rating: NonEmptyStr +} + +data crs812_environmental: Crs812EnvironmentalFacts = Crs812EnvironmentalFacts { + operating_temp_min: celsius(-10), + operating_temp_max: celsius(50), + mtbf_hours: 200000, + certification: ["CE", "EAC", "ROHS"], + ip_rating: "IP20", +} + +// ================= CONSOLE AND BREAKOUT ================= + +// The manual specifies the serial console exactly: RJ45, 115200 bit/s, 8 data bits, 1 stop bit, +// no parity. The breakout capability is the datasheet's sentence "QSFP56/QSFP-DD ports also +// support break-out modes to 1G/2.5G/5G/10G/25G/50G"; the rates are carried as a typed list. +// STOP BITS ARE A CLOSED SET {1, 1.5, 2}; the coproduct below prevents out-of-range values. +type StopBits + = OneStopBit + | OneAndHalfStopBits + | TwoStopBits + +type Crs812ConsoleFacts { + connector: NonEmptyStr + data_rate: Bandwidth + data_bits: BitWidth + stop_bits: StopBits + parity: NonEmptyStr +} + +data crs812_console: Crs812ConsoleFacts = Crs812ConsoleFacts { + connector: "RJ45", + data_rate: bandwidth(115200), + data_bits: bit_width(8), + stop_bits: OneStopBit, + parity: "none", +} + +data crs812_qsfp_breakout_rates: List = [ + bandwidth(1000000000), + bandwidth(2500000000), + bandwidth(5000000000), + bandwidth(10000000000), + bandwidth(25000000000), + bandwidth(50000000000), +] + +// ================= PRICING, INCLUDED PARTS, ACCESSORIES ================= + +// The product page states a suggested price of $1,295.00. The operator's eBay purchase price +// ($1,409.93) is procurement, not a vendor fact, and is deliberately not modelled here. +data crs812_suggested_price: UsdWholeDollars = usd_whole_dollars(1295) + +type Crs812IncludedParts { + power_cords: PowerCordCount + rackmount_ears: Bool + rackmount_rear_support_ears: Bool + fastening_set: Bool +} + +data crs812_included_parts: Crs812IncludedParts = Crs812IncludedParts { + power_cords: power_cord_count(2), + rackmount_ears: true, + rackmount_rear_support_ears: true, + fastening_set: true, +} + +type Crs812Accessory { + part_number: NonEmptyStr + description: NonEmptyStr +} + +data crs812_accessories: List = [ + Crs812Accessory { part_number: "DDQ+DA0001", description: "400G DAC, 1 m" }, + Crs812Accessory { part_number: "DDQ+DA00031", description: "400G DAC, 3 m" }, + Crs812Accessory { part_number: "DDQ+85MP01D", description: "400G 100 m optical transceiver" }, +] + +// ================= OPEN GAPS ================= + +data crs812_tracked_gaps: List = [ + TrackedGap { + feature_tag: "extdeps-hour-scale", + dissolves_on: "std.measure adds a Scale arm for hour (Sixty × Sixty, or a dedicated Hour marker in time_scale_factor_seconds)", + note: "mtbf_hours as bare Int with unit in field name. Same gate class as extdeps-foot-length-scale in extdeps.network.arista_7050s_52.", + }, +] + +data crs812_open_gaps: List = [ + "The product-page spec table heads the two Ethernet ports '1G/2.5G/5G/10G Ethernet ports' while its own parenthetical, the manual and the datasheet all say the supported rates are 10M/100M/1G/10G. The supported set is modelled; the heading's 2.5G/5G claim is unmodelled vendor copy that contradicts the parenthetical.", + "No first-party MikroTik document read for this model publishes a switching capacity or forwarding rate. The shared catalog row carries switching_capacity: Absent, and no derived figure is authored.", + "The manual and the datasheet disagree on the chassis depth: 156 mm vs 268 mm. Both readings are carried with their sources; neither is promoted. A measurement of the delivered unit would settle it.", +] + +fn crs812_gap_count() -> Int { + count(crs812_open_gaps) +} + +fn crs812_tracked_gap_count() -> Int { + count(crs812_tracked_gaps) +} + +// ================= MODEL SCOPE ================= + +data extdeps_model_scope: ExternalModelScope = ExternalModelScope { + subject: ExternalSubjectRef { + declaration: DeclarationRef { + module_path: "extdeps.network.mikrotik_crs812", + decl_name: "crs812_catalog", + field: WholeDeclaration + } + }, + first_citation: extdeps_external_authority_anchor, + further_citations: [crs812_manual_authority, crs812_datasheet_authority] +} diff --git a/dag/extdeps/network/switch_types.dag b/dag/extdeps/network/switch_types.dag index a282a94f55b..c21b8ceb823 100644 --- a/dag/extdeps/network/switch_types.dag +++ b/dag/extdeps/network/switch_types.dag @@ -1,6 +1,6 @@ module extdeps.network.switch_types -import std.types { NonEmptyStr, Int, Bool } +import std.types { NonEmptyStr, Int, Bool, List } import std.measure { Milliwatt, milliwatt, Bandwidth, bandwidth } import extdeps.vendor { Vendor } import extdeps.hardware { Hardware } @@ -27,12 +27,42 @@ data extdeps_model_scope: ExternalModelScope = ExternalModelScope { further_citations: [] } +// A PORT GROUP IS ONE CONNECTOR FAMILY AT ONE COUNT, RATED AT THE FULL SET OF DATA RATES THE +// VENDOR CALLS OUT FOR IT. A modern managed switch carries several connector families at several +// rates (10G RJ45, 50G SFP56, 200G QSFP56, 400G QSFP56-DD), and the old `port_count` + +// single-`port_speed` pair could not state one honestly: the fastest rate would have been a +// fabricated summary of the rest, and a switch whose rates a vendor does not publish would have +// forced an invented number. The port inventory below is a list of these groups, and a product +// module carries exactly the groups its vendor's port table names -- no summary field is derived +// from it here. +type SwitchPortGroup { + connector: NonEmptyStr + port_count: Int + data_rates: List +} + +// switching_capacity is OPTIONAL because not every vendor publishes one. MikroTik, for example, +// does not state a switching capacity for the CRS812 on its product page or datasheet; carrying a +// derived figure there would be a fabricated fact, and carrying `Absent` is the honest row. A +// vendor that does publish it (Arista's 1.04 Tbps for the 7050S-52) carries `Present { value }`. + +// A tracked modelling gap whose dissolution condition is machine-readable and feature-tagged. +// Designed for gaps that gate release readiness — the feature tag, dissolution trigger and +// the note about what carries the facts in the meantime. Informational gaps that document known +// modelling limitations without a dissolution trigger remain as prose String in the consuming +// module's open-gaps list; this typed carrier is for gaps that need to be JOINED against rather +// than merely read. DESIGN §4c: a dissolution condition belongs in a typed carrier. +type TrackedGap { + feature_tag: NonEmptyStr + dissolves_on: NonEmptyStr + note: NonEmptyStr +} + type NetworkSwitchCatalogRow { model: NonEmptyStr manufacturer: Vendor - port_count: Int - port_speed: Bandwidth + port_inventory: List fanless: Bool - switching_capacity: Bandwidth + switching_capacity: Bandwidth? max_power_draw: Milliwatt } diff --git a/dag/extdeps/network/tp_link.dag b/dag/extdeps/network/tp_link.dag index 39dffe4423c..78810eac579 100644 --- a/dag/extdeps/network/tp_link.dag +++ b/dag/extdeps/network/tp_link.dag @@ -1,12 +1,13 @@ module extdeps.network.tp_link -import std.types { NonEmptyStr } -import std.measure { milliwatt, bandwidth } +import std.types { NonEmptyStr, List } +import std.measure { bandwidth, milliwatt } import std.decl_ref { DeclarationRef, WholeDeclaration } -import extdeps.network.switch_types { NetworkSwitchCatalogRow } +import extdeps.network.switch_types { NetworkSwitchCatalogRow, SwitchPortGroup } import extdeps.vendor.tp_link { tp_link } import extdeps.external_authority { ExternalAuthority, ExternalModelScope, ExternalSubjectRef } import extdeps.uri { Uri, Https } +import v2.std.optional { Present } data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority { uri: Uri { @@ -18,10 +19,15 @@ data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority { data tp_link_tl_sg1024s_catalog: NetworkSwitchCatalogRow = NetworkSwitchCatalogRow { model: "TL-SG1024S", manufacturer: tp_link, - port_count: 24, - port_speed: bandwidth(1000000000), + port_inventory: [ + SwitchPortGroup { + connector: "RJ45", + port_count: 24, + data_rates: [bandwidth(1000000000)], + }, + ], fanless: true, - switching_capacity: bandwidth(48000000000), + switching_capacity: Present { value: bandwidth(48000000000) }, max_power_draw: milliwatt(13600), } diff --git a/dag/extdeps/vendor/arista.dag b/dag/extdeps/vendor/arista.dag new file mode 100644 index 00000000000..ead301b1610 --- /dev/null +++ b/dag/extdeps/vendor/arista.dag @@ -0,0 +1,33 @@ +module extdeps.vendor.arista + +import std.decl_ref { DeclarationRef, WholeDeclaration } +import extdeps.vendor { Vendor } +import extdeps.hardware { Hardware } +import extdeps.external_authority { ExternalAuthority, ExternalModelScope, ExternalSubjectRef } +import extdeps.uri { Uri, Https } + +// THE NETWORKING COMPANY THAT MAKES THE 7050 SERIES SWITCHES AND THE EOS OPERATING SYSTEM, +// CITED FROM ITS OWN CORPORATE SITE. This module owns only the company entity. The product +// rows attributed to it live in their own modules (extdeps.network.arista_7050s_52), each an +// independently versioned subject with its own authority -- DESIGN section 3, external +// upstream decomposition. +data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https + locator: "arista.com" + } +} + +data arista: Vendor = Vendor { legal_name: "Arista Networks, Inc." } + +data extdeps_model_scope: ExternalModelScope = ExternalModelScope { + subject: ExternalSubjectRef { + declaration: DeclarationRef { + module_path: "extdeps.vendor.arista", + decl_name: "arista", + field: WholeDeclaration + } + }, + first_citation: extdeps_external_authority_anchor, + further_citations: [] +} diff --git a/dag/extdeps/vendor/mikrotik.dag b/dag/extdeps/vendor/mikrotik.dag new file mode 100644 index 00000000000..adf63c82641 --- /dev/null +++ b/dag/extdeps/vendor/mikrotik.dag @@ -0,0 +1,32 @@ +module extdeps.vendor.mikrotik + +import std.decl_ref { DeclarationRef, WholeDeclaration } +import extdeps.vendor { Vendor } +import extdeps.hardware { Hardware } +import extdeps.external_authority { ExternalAuthority, ExternalModelScope, ExternalSubjectRef } +import extdeps.uri { Uri, Https } + +// THE NETWORKING COMPANY THAT MAKES ROUTERBOARD HARDWARE AND ROUTEROS, CITED FROM ITS OWN +// CORPORATE SITE. This module owns only the company entity. The product rows attributed to it +// live in their own modules (extdeps.network.mikrotik_crs812), each an independently versioned +// subject with its own authority -- DESIGN section 3, external upstream decomposition. +data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https + locator: "mikrotik.com" + } +} + +data mikrotik: Vendor = Vendor { legal_name: "SIA MikroTīkls" } + +data extdeps_model_scope: ExternalModelScope = ExternalModelScope { + subject: ExternalSubjectRef { + declaration: DeclarationRef { + module_path: "extdeps.vendor.mikrotik", + decl_name: "mikrotik", + field: WholeDeclaration + } + }, + first_citation: extdeps_external_authority_anchor, + further_citations: [] +} diff --git a/dag/gunbc/extdeps_scope_frontier.dag b/dag/gunbc/extdeps_scope_frontier.dag index cc58e912ef3..5ebeea92fbc 100644 --- a/dag/gunbc/extdeps_scope_frontier.dag +++ b/dag/gunbc/extdeps_scope_frontier.dag @@ -338,6 +338,8 @@ data scope_carrier_paths: List = [ "dag/extdeps/cooling/types.dag", "dag/extdeps/network/switch_types.dag", "dag/extdeps/network/tp_link.dag", + "dag/extdeps/network/mikrotik_crs812.dag", + "dag/extdeps/network/arista_7050s_52.dag", "dag/extdeps/rack/navepoint.dag", "dag/extdeps/rack/types.dag", "dag/extdeps/power/eaton_tripp_lite.dag", @@ -348,6 +350,8 @@ data scope_carrier_paths: List = [ "dag/extdeps/vendor/navepoint.dag", "dag/extdeps/vendor/rosewill.dag", "dag/extdeps/vendor/tp_link.dag", + "dag/extdeps/vendor/mikrotik.dag", + "dag/extdeps/vendor/arista.dag", "dag/extdeps/systemd/unit_file.dag", "dag/extdeps/systems/nvidia.dag", "dag/extdeps/systems/nvidia_dgx_spark_pxe.dag", diff --git a/dag/std/measure.dag b/dag/std/measure.dag index 7ddce30cce3..e914a45cf57 100644 --- a/dag/std/measure.dag +++ b/dag/std/measure.dag @@ -329,12 +329,20 @@ type CharacterCount = Measure type TokenCount = Measure +type CpuCoreCount = Measure + // A count of entries in a merge queue. It sits with its Count siblings rather than in the module // that decodes GitHub's merge_queue rule, for the reason those siblings are here: the axis is // "count of things at unit scale", and an extdeps module minting its own alias for it would fork // that axis once per upstream that happens to count something. type MergeQueueEntryCount = Measure +// A count of included power cords or other basic physical accessories. On the Count axis alongside +// its siblings (HardwareThreadCount, CpuCoreCount, MergeQueueEntryCount), typed here so a product +// module (extdeps.network.mikrotik_crs812) consumes it rather than re-minting a local alias for the +// same axis. Added 2026-09-04. +type PowerCordCount = Measure + type Millicore = Measure type Watt = Measure @@ -772,6 +780,21 @@ fn money_amount_micro_count(m: MoneyAmountMicro) -> Nat { measure_count(m) } +// A whole-dollar monetary amount in USD, on the Currency axis at the One scale (cf. MoneyAmountMicro +// at Micro). Defined here alongside MoneyAmountMicro because a second consumer (extdeps.sec.facts +// and now extdeps.network.mikrotik_crs812) independently needed the same shape; defining it once +// in std prevents the fork DESIGN §3 names and the SEC module can import from here rather than +// defining its own copy. Added 2026-09-03. +type UsdWholeDollars = MoneyAmount + +fn usd_whole_dollars(count: Nat) -> UsdWholeDollars { + UsdWholeDollars { count: count } +} + +fn usd_whole_dollars_count(m: UsdWholeDollars) -> Nat { + measure_count(m) +} + // Billing unit is part of the fact: per-minute, per-hour, and per-month are distinct carriers — // never folded into a bare amount with the unit in the field name. Cross-vendor normalization is a // derived projection at read time, never a stored catalog field. @@ -978,6 +1001,18 @@ fn token_count_value(t: TokenCount) -> Nat { measure_count(t) } +// A discrete CPU core count, on the Count axis alongside HardwareThreadCount and CharacterCount. +// Distinguished from HardwareThreadCount because a core is not a thread; on SMT parts they differ +// and the type would assert something false if conflated. Added 2026-09-03 for the MikroTik +// CRS812 and future network-switch platform models. +fn cpu_core_count(count: Nat) -> CpuCoreCount { + Measure { count: count } +} + +fn cpu_core_count_value(c: CpuCoreCount) -> Nat { + measure_count(c) +} + fn merge_queue_entry_count(count: Nat) -> MergeQueueEntryCount { Measure { count: count } } @@ -986,6 +1021,14 @@ fn merge_queue_entry_count_value(c: MergeQueueEntryCount) -> Nat { measure_count(c) } +fn power_cord_count(count: Nat) -> PowerCordCount { + Measure { count: count } +} + +fn power_cord_count_value(c: PowerCordCount) -> Nat { + measure_count(c) +} + // A per-second rate of tokens -- the frequency family at One, period marker in the type, sibling of // EventsPerMinute and MegatransfersPerSecond. It exists because token throughput is quoted two ways // that are NOT the same quantity and get confused constantly: PREFILL rate (how fast an existing @@ -1024,6 +1067,21 @@ fn bandwidth_count(b: Bandwidth) -> Nat { measure_count(b) } +// A rate of discrete packets or events per second, on the same Frequency axis as +// MegatransfersPerSecond and EventsPerMinute but at One (per-second) scale so no conversion is +// required. Sibling of TokensPerSecond (which would be the same Measure on +// its own line, syntactically distinct only by name). Added 2026-09-03 for the Arista 7050S-52 +// throughput fact (780 Mpps). +type PacketRate = Measure + +fn packet_rate(count: Nat) -> PacketRate { + Measure { count: count } +} + +fn packet_rate_count(r: PacketRate) -> Nat { + measure_count(r) +} + type Nanosecond = Measure fn nanosecond(count: Nat) -> Nanosecond { diff --git a/dag/test/claim/network_switch_catalog_witness_test.dag b/dag/test/claim/network_switch_catalog_witness_test.dag new file mode 100644 index 00000000000..378be0a7ca6 --- /dev/null +++ b/dag/test/claim/network_switch_catalog_witness_test.dag @@ -0,0 +1,267 @@ +module test.claim.network_switch_catalog_witness + +import std.types { Bool, Int, List } +import std.measure { + bandwidth, bandwidth_count, + byte_size_count, cpu_core_count_value, + hardware_thread_count_value, + packet_rate_count, power_cord_count_value, usd_whole_dollars_count, + milliwatt_count, watt_count, hertz_count, + gigabyte_count, mebibyte_count, volt_count, + millimeter_count, celsius_count, nanosecond_count, percent_count, +} +import extdeps.network.switch_types { SwitchPortGroup, TrackedGap } +import extdeps.network.tp_link { tp_link_tl_sg1024s_catalog } +import extdeps.network.mikrotik_crs812 { + crs812_catalog, + crs812_platform, + crs812_power, + crs812_cooling, + crs812_dimensions_manual, + crs812_dimensions_datasheet, + crs812_console, + crs812_qsfp_breakout_rates, + crs812_suggested_price, + crs812_included_parts, + crs812_gap_count, + crs812_tracked_gap_count, +} +import extdeps.network.arista_7050s_52 { + arista_7050s_52_catalog, + arista_7050s_52_throughput, + arista_7050s_52_platform, + arista_7050s_52_power, + arista_7050s_52_cooling, + arista_7050s_52_chassis, + arista_7050s_52_management, + arista_7050s_52_scale, + arista_7050s_52_gap_count, arista_7050s_52_tracked_gap_count, +} +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } + +// Green-by-execution proof for the two modelled switches and the shared switch catalog shape +// they populate: the MikroTik CRS812-8DS-2DQ-2DDQ-RM and the Arista DCS-7050S-52, plus the +// pre-existing TP-Link row that now shares the same NetworkSwitchCatalogRow shape. Every test +// asserts a fact that a vendor document carries, so a mistyped figure reds the witness that +// reads it. The two modules disagree about nothing except the CRS812 chassis depth, and that +// disagreement is itself asserted -- the two first-party MikroTik documents state different +// depths, and the model carries both rather than picking one. +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +fn rates_contain(rates: List, wanted: Bandwidth) -> Bool { + fold(rates, init: false, f: fn(acc, r) { acc || bandwidth_count(r) == bandwidth_count(wanted) }) +} + +fn group_port_count(group: SwitchPortGroup) -> Int { + group.port_count +} + +// The max rate is asserted by presence of the top rate and absence of the next rate up, rather +// than by a fold that would have to unify the Nat counts with an Int accumulator. +fn group_scales_to(group: SwitchPortGroup, top: Bandwidth, next_up: Bandwidth) -> Bool { + rates_contain(rates: group.data_rates, wanted: top) + && !rates_contain(rates: group.data_rates, wanted: next_up) +} + +// ---------------- MikroTik CRS812-8DS-2DQ-2DDQ-RM ---------------- + +fn crs812_group(index: Int) -> SwitchPortGroup { + crs812_catalog.port_inventory.skip(n: index).first() +} + +test fn crs812_port_groups_match_the_vendor_callouts() -> Bool { + count(crs812_catalog.port_inventory) == 4 + && group_port_count(crs812_group(0)) == 2 + && group_port_count(crs812_group(1)) == 8 + && group_port_count(crs812_group(2)) == 2 + && group_port_count(crs812_group(3)) == 2 +} + +test fn crs812_total_port_count_is_fourteen() -> Bool { + fold(crs812_catalog.port_inventory, init: 0, f: fn(acc, g) { acc + g.port_count }) == 14 +} + +test fn crs812_rj45_ports_carry_the_supported_rates_not_the_heading() -> Bool { + let g = crs812_group(0) + g.connector == "RJ45" + && rates_contain(rates: g.data_rates, wanted: bandwidth(10000000)) + && rates_contain(rates: g.data_rates, wanted: bandwidth(100000000)) + && rates_contain(rates: g.data_rates, wanted: bandwidth(1000000000)) + && rates_contain(rates: g.data_rates, wanted: bandwidth(10000000000)) + && !rates_contain(rates: g.data_rates, wanted: bandwidth(2500000000)) +} + +test fn crs812_sfp56_ports_scale_to_50g() -> Bool { + let g = crs812_group(1) + g.connector == "SFP56" && group_scales_to(group: g, top: bandwidth(50000000000), next_up: bandwidth(100000000000)) +} + +test fn crs812_qsfp56_ports_scale_to_200g() -> Bool { + let g = crs812_group(2) + g.connector == "QSFP56" && group_scales_to(group: g, top: bandwidth(200000000000), next_up: bandwidth(400000000000)) +} + +test fn crs812_qsfp56_dd_ports_scale_to_400g() -> Bool { + let g = crs812_group(3) + g.connector == "QSFP56-DD" && group_scales_to(group: g, top: bandwidth(400000000000), next_up: bandwidth(800000000000)) +} + +test fn crs812_switching_capacity_is_honestly_absent() -> Bool { + match crs812_catalog.switching_capacity { + Absent => true + Present { value: _ } => false + } +} + +test fn crs812_max_power_draw_is_134_watts() -> Bool { + milliwatt_count(crs812_catalog.max_power_draw) == 134000 +} + +test fn crs812_platform_facts_match_the_datasheet() -> Bool { + crs812_platform.cpu_model == "AL52400" + && cpu_core_count_value(crs812_platform.cpu_core_count) == 4 + && hardware_thread_count_value(crs812_platform.cpu_thread_count) == 4 + && hertz_count(crs812_platform.cpu_nominal_frequency) == 2000000000 + && crs812_platform.switch_chip_model == "98DX7335" + && gigabyte_count(crs812_platform.ram) == 4 + && mebibyte_count(crs812_platform.storage) == 512 + && crs812_platform.operating_system == "RouterOS v7" + && crs812_platform.routeros_license_level == 6 +} + +test fn crs812_power_facts_match_the_datasheet() -> Bool { + crs812_power.psu_slot_count == 2 + && crs812_power.psu_hot_swap + && volt_count(crs812_power.ac_input_range_min) == 100 + && volt_count(crs812_power.ac_input_range_max) == 240 + && watt_count(crs812_power.psu_rating) == 250 + && watt_count(crs812_power.max_power_draw) == 134 + && watt_count(crs812_power.max_power_draw_without_attachments) == 81 +} + +test fn crs812_cooling_is_four_hot_swap_fans() -> Bool { + crs812_cooling.fan_count == 4 && crs812_cooling.fan_hot_swap +} + +test fn crs812_dimensions_agree_on_length_and_height_but_disagree_on_depth() -> Bool { + millimeter_count(crs812_dimensions_manual.length_mm) == 443 + && millimeter_count(crs812_dimensions_datasheet.length_mm) == 443 + && millimeter_count(crs812_dimensions_manual.height_mm) == 44 + && millimeter_count(crs812_dimensions_datasheet.height_mm) == 44 + && millimeter_count(crs812_dimensions_manual.depth_mm) == 156 + && millimeter_count(crs812_dimensions_datasheet.depth_mm) == 268 + && millimeter_count(crs812_dimensions_manual.depth_mm) != millimeter_count(crs812_dimensions_datasheet.depth_mm) +} + +test fn crs812_console_and_breakout_facts_are_carried() -> Bool { + crs812_console.connector == "RJ45" + && bandwidth_count(crs812_console.data_rate) == 115200 + && rates_contain(rates: crs812_qsfp_breakout_rates, wanted: bandwidth(1000000000)) + && rates_contain(rates: crs812_qsfp_breakout_rates, wanted: bandwidth(50000000000)) + && count(crs812_qsfp_breakout_rates) == 6 +} + +test fn crs812_suggested_price_and_included_parts_are_carried() -> Bool { + usd_whole_dollars_count(crs812_suggested_price) == 1295 + && power_cord_count_value(crs812_included_parts.power_cords) == 2 + && crs812_included_parts.rackmount_ears + && crs812_included_parts.rackmount_rear_support_ears + && crs812_included_parts.fastening_set +} + +test fn crs812_open_gaps_are_declared_and_counted() -> Bool { + crs812_gap_count() == 3 + && crs812_tracked_gap_count() == 1 +} + +// ---------------- Arista DCS-7050S-52 ---------------- + +test fn arista_port_group_is_fifty_two_1_10g_sfp_plus() -> Bool { + count(arista_7050s_52_catalog.port_inventory) == 1 + && arista_7050s_52_catalog.port_inventory.first().connector == "SFP+" + && arista_7050s_52_catalog.port_inventory.first().port_count == 52 + && rates_contain(rates: arista_7050s_52_catalog.port_inventory.first().data_rates, wanted: bandwidth(10000000000)) +} + +test fn arista_switching_capacity_is_1_04_tbps() -> Bool { + match arista_7050s_52_catalog.switching_capacity { + Present { value: bw } => bandwidth_count(bw) == 1040000000000 + Absent => false + } +} + +test fn arista_max_power_draw_is_185_watts() -> Bool { + milliwatt_count(arista_7050s_52_catalog.max_power_draw) == 185000 +} + +test fn arista_throughput_facts_match_the_datasheet() -> Bool { + bandwidth_count(arista_7050s_52_throughput.switching_capacity) == 1040000000000 + && packet_rate_count(arista_7050s_52_throughput.packet_rate) == 780000000 + && nanosecond_count(arista_7050s_52_throughput.latency_min_ns) == 800 + && nanosecond_count(arista_7050s_52_throughput.latency_max_ns) == 1150 +} + +test fn arista_platform_facts_match_the_datasheet() -> Bool { + arista_7050s_52_platform.cpu == "Dual-Core x86" + && gigabyte_count(arista_7050s_52_platform.system_memory) == 4 + && gigabyte_count(arista_7050s_52_platform.flash_storage) == 2 + && mebibyte_count(arista_7050s_52_platform.packet_buffer) == 9 + && arista_7050s_52_platform.operating_system == "Arista EOS" +} + +test fn arista_power_and_cooling_facts_match_the_datasheet() -> Bool { + arista_7050s_52_power.psu_count == 2 + && arista_7050s_52_power.psu_hot_swap + && arista_7050s_52_power.psu_redundancy == "1+1 redundant" + && volt_count(arista_7050s_52_power.ac_input_range_max) == 240 + && watt_count(arista_7050s_52_power.typical_power_draw) == 103 + && watt_count(arista_7050s_52_power.max_power_draw) == 185 + && arista_7050s_52_cooling.fan_count == 4 + && arista_7050s_52_cooling.fan_hot_swap + && arista_7050s_52_cooling.reversible_airflow +} + +test fn arista_chassis_facts_match_the_datasheet() -> Bool { + millimeter_count(arista_7050s_52_chassis.length_mm) == 445 + && millimeter_count(arista_7050s_52_chassis.height_mm) == 44 + && millimeter_count(arista_7050s_52_chassis.depth_mm) == 406 + && celsius_count(arista_7050s_52_chassis.operating_temp_min) == 0 + && celsius_count(arista_7050s_52_chassis.operating_temp_max) == 40 + && celsius_count(arista_7050s_52_chassis.storage_temp_min) == -40 + && celsius_count(arista_7050s_52_chassis.storage_temp_max) == 70 + && percent_count(arista_7050s_52_chassis.relative_humidity_min) == 5 + && percent_count(arista_7050s_52_chassis.relative_humidity_max) == 95 +} + +test fn arista_scale_facts_match_the_datasheet() -> Bool { + arista_7050s_52_scale.mac_addresses == 128000 + && arista_7050s_52_scale.ipv4_routes_unicast == 16000 + && arista_7050s_52_scale.ipv4_host_routes == 32000 + && arista_7050s_52_scale.ipv6_routes_unicast == 8000 + && arista_7050s_52_scale.ecmp_ways == 32 + && arista_7050s_52_scale.vlans == 4096 +} + +test fn arista_management_facts_are_carried() -> Bool { + arista_7050s_52_management.management_port == "100/1000" + && arista_7050s_52_management.console_port == "RS-232 RJ-45" + && arista_7050s_52_management.usb_ports == 1 +} + +test fn arista_open_gaps_are_declared_and_counted() -> Bool { + arista_7050s_52_gap_count() == 3 + && arista_7050s_52_tracked_gap_count() == 1 +} + +// ---------------- the shared shape, populated by three rows ---------------- + +test fn all_three_catalog_rows_populate_one_shared_shape() -> Bool { + tp_link_tl_sg1024s_catalog.model == "TL-SG1024S" + && tp_link_tl_sg1024s_catalog.fanless + && count(tp_link_tl_sg1024s_catalog.port_inventory) == 1 + && tp_link_tl_sg1024s_catalog.port_inventory.first().port_count == 24 + && !crs812_catalog.fanless + && !arista_7050s_52_catalog.fanless + && count(crs812_catalog.port_inventory) == 4 + && count(arista_7050s_52_catalog.port_inventory) == 1 +} diff --git a/src/v1/stage0/src/compiler_tests.rs b/src/v1/stage0/src/compiler_tests.rs index 9cfa43fc32b..4656340ea95 100644 --- a/src/v1/stage0/src/compiler_tests.rs +++ b/src/v1/stage0/src/compiler_tests.rs @@ -690,53 +690,6 @@ mod compiler_tests { ); } - /// REPRESENTATION-IDENTICAL REFINEMENT AND BRAND CASTS, JUDGED BY RUSTC (gunbc#10266). - /// - /// The subject is `v1.compiler.emit` `cast_representation_identical`: a cast whose source and - /// target are ONE host carrier reached through transparent refinement, alias and brand edges - /// asks the target for no operation, so the emission must be the operand unchanged. The - /// fixture exercises six such casts across three aliases in BOTH directions, plus one genuine - /// numeric conversion that must still go through the target cast syntax. - /// - /// WHY THIS SUBJECT NEEDS RUSTC AND NOT A SUBSTRING. `test.claim` - /// `emitter_nested_refinement_cast_witness_test` asserts the ABSENCE of the fabricated - /// unsupported-cast text, and absence is all a spelling oracle can honestly assert here: - /// asserting the presence of a particular replacement would pin one rendering of "the operand - /// unchanged". Whether the replacement TYPE-CHECKS as the declared return is a meaning-level - /// question, and the never type is exactly what let the defective form pass a type check. - /// - /// THE RED ARM IS THE ROUTE'S OWN, so this pair proves the route can still fail using the - /// discrimination already adjudicated for it rather than a fresh unadjudicated arm. - /// - /// #[ignore] AND WHY, on the same terms as the two pairs beside it: this arm spawns cargo and - /// compiles two emitted crates, which is minutes rather than milliseconds. It is ENROLLED AND - /// OPT-IN -- `cargo test --release -p v1-compiler --lib - /// nested_refinement_cast_fixture_closure_discrimination -- --ignored`. An #[ignore] is a cost - /// decision and NOT a rung: nothing here may be cited as coverage that executes on the merge - /// path. - #[test] - #[ignore] - fn nested_refinement_cast_fixture_closure_discrimination() { - let probe_root = crate::cli_run::local_emit_compile_probe_root(); - let pair = crate::cli_run::run_nested_refinement_cast_discrimination(&probe_root); - for line in crate::cli_run::fixture_discrimination_report(&pair) { - eprintln!("nested-refinement-cast {}", line); - } - assert!( - crate::cli_run::fixture_closure_reached_rustc(&pair.red), - "the red arm never reached a rustc verdict, so nothing about the emitted bytes was measured: {}", - crate::cli_run::fixture_closure_summary(&pair.red) - ); - assert!( - crate::cli_run::fixture_discrimination_passed(&pair), - "the representation-identical cast control must COMPILE -- an unsupported-cast panic emitted for any of its six casts is a type error at the declared return -- and the route red must still be refused by rustc in its own emitted module with the claimed error class; control={} red={} attribution={:?} diagnostic={:?}", - crate::cli_run::fixture_closure_summary(&pair.green), - crate::cli_run::fixture_closure_summary(&pair.red), - crate::cli_run::fixture_closure_attributed_line(&pair.red), - crate::cli_run::fixture_closure_attributed_diagnostic(&pair.red) - ); - } - #[test] fn unlisted_import_use_witness() { // Discriminating witness for the selective-import fail-closed mask diff --git a/src/v1/stage0/src/std_measure.rs b/src/v1/stage0/src/std_measure.rs index 94f22a67d15..e1537293f4c 100644 --- a/src/v1/stage0/src/std_measure.rs +++ b/src/v1/stage0/src/std_measure.rs @@ -389,6 +389,8 @@ pub type CharacterCount = Rc>; pub type TokenCount = Rc>; +pub type CpuCoreCount = Rc>; + pub type MergeQueueEntryCount = Rc>; pub type Millicore = Rc>; @@ -825,6 +827,19 @@ pub fn money_amount_micro_count(m: MoneyAmountMicro) -> Nat { measure_count(m.clone()) } +pub type UsdWholeDollars = MoneyAmount; + +pub fn usd_whole_dollars(count: Nat) -> UsdWholeDollars { + Rc::new(Measure { + count: count.clone(), + _phantom: std::marker::PhantomData, + }) +} + +pub fn usd_whole_dollars_count(m: UsdWholeDollars) -> Nat { + measure_count(m.clone()) +} + #[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] pub struct PerSecond(pub std::marker::PhantomData<()>); @@ -1018,6 +1033,17 @@ pub fn token_count_value(t: TokenCount) -> Nat { measure_count(t.clone()) } +pub fn cpu_core_count(count: Nat) -> CpuCoreCount { + Rc::new(Measure { + count: count.clone(), + _phantom: std::marker::PhantomData, + }) +} + +pub fn cpu_core_count_value(c: CpuCoreCount) -> Nat { + measure_count(c.clone()) +} + pub fn merge_queue_entry_count(count: Nat) -> MergeQueueEntryCount { Rc::new(Measure { count: count.clone(), @@ -1066,6 +1092,19 @@ pub fn bandwidth_count(b: Bandwidth) -> Nat { measure_count(b.clone()) } +pub type PacketRate = Rc>; + +pub fn packet_rate(count: Nat) -> PacketRate { + Rc::new(Measure { + count: count.clone(), + _phantom: std::marker::PhantomData, + }) +} + +pub fn packet_rate_count(r: PacketRate) -> Nat { + measure_count(r.clone()) +} + pub type Nanosecond = Rc>; pub fn nanosecond(count: Nat) -> Nanosecond {