Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 4 additions & 4 deletions dag/gunbc/auth/profile_projection.dag
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ import extdeps.filesystem.filesystem_io {
FilesystemReadOutcome, FilesystemReadRefused, FilesystemReadSucceeded,
}
import extdeps.languages.json.emit {
serialize_json, json_object, json_kv, json_string, JsonValue,
serialize_json, json_object, json_kv, json_string, JsonValue, JsonKeyValue,
}
import extdeps.languages.json.parse {
parse_json_document, json_field_string, json_document_gap_text,
Expand Down Expand Up @@ -87,21 +87,21 @@ fn principal_profile_json(profile: PrincipalProfile) -> String {
], profile_name_members(name: profile.name)), concat(profile_email_members(email: profile.email), profile_picture_members(picture: profile.picture)))))
}

fn profile_name_members(name: String?) -> List<JsonValue> {
fn profile_name_members(name: String?) -> List<JsonKeyValue> {
match name {
Present { value: n } => [ json_kv(key: "name", value: json_string(s: n)) ]
Absent => []
}
}

fn profile_email_members(email: Email?) -> List<JsonValue> {
fn profile_email_members(email: Email?) -> List<JsonKeyValue> {
match email {
Present { value: e } => [ json_kv(key: "email", value: json_string(s: e as String)) ]
Absent => []
}
}

fn profile_picture_members(picture: Uri?) -> List<JsonValue> {
fn profile_picture_members(picture: Uri?) -> List<JsonKeyValue> {
match picture {
Present { value: u } => [ json_kv(key: "picture", value: json_string(s: uri_wire(uri: u) as String)) ]
Absent => []
Expand Down
8 changes: 4 additions & 4 deletions dag/gunbc/auth/session_store.dag
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,7 @@ import extdeps.filesystem.filesystem_io {
filesystem_entry_presence,
}
import extdeps.languages.json.emit {
serialize_json, json_object, json_kv, json_string, JsonValue,
serialize_json, json_object, json_kv, json_string, JsonValue, JsonKeyValue,
}
import extdeps.languages.json.parse {
parse_json_document, json_field_string, json_document_gap_text,
Expand Down Expand Up @@ -104,7 +104,7 @@ fn authenticated_session_json(session: AuthenticatedSession) -> String {
// THE OPTIONAL PICTURE MEMBER, emitted only when the login projected one: absence is the
// member's ABSENCE on the wire, never an empty string standing in for none. The spelling is
// the Uri wire form (https://… or http://…), the same claim the ID-token reader admitted.
fn session_profile_picture_members(picture: Uri?) -> List<JsonValue> {
fn session_profile_picture_members(picture: Uri?) -> List<JsonKeyValue> {
match picture {
Present { value: u } => [ json_kv(key: "picture", value: json_string(s: uri_wire(uri: u) as String)) ]
Absent => []
Expand All @@ -113,15 +113,15 @@ fn session_profile_picture_members(picture: Uri?) -> List<JsonValue> {

// THE OPTIONAL NAME MEMBER, the same law as the picture: absence is the member's ABSENCE,
// never an empty string standing in for none.
fn session_profile_name_members(name: String?) -> List<JsonValue> {
fn session_profile_name_members(name: String?) -> List<JsonKeyValue> {
match name {
Present { value: n } => [ json_kv(key: "name", value: json_string(s: n)) ]
Absent => []
}
}

// THE OPTIONAL EMAIL MEMBER, the same law again.
fn session_profile_email_members(email: Email?) -> List<JsonValue> {
fn session_profile_email_members(email: Email?) -> List<JsonKeyValue> {
match email {
Present { value: e } => [ json_kv(key: "email", value: json_string(s: e as String)) ]
Absent => []
Expand Down
7 changes: 4 additions & 3 deletions dag/gunbc/bmc_dry_realization.dag
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
module gunbc.bmc_dry_realization

import std.types { Bool, Int, List, NonEmptyStr, String }
import std.algebra { list_snoc_item }
import std.measure { Second, second }
import v2.std.operation_argv { OperationRef }
import v2.std.operation_realization {
Expand Down Expand Up @@ -161,9 +162,9 @@ fn bmc_dry_realization(identity: NonEmptyStr, initial: BmcWorld, epoch: Second)
identity: identity,
initial: initial,
epoch: epoch,
bindings: list_append(
bmc_bindings(get: fn(w) { w }, put: fn(w, next) { next }),
virtual_delay_binding(at: sleep_delay_seconds_operation, seconds_input: "seconds"),
bindings: list_snoc_item(
xs: bmc_bindings(get: fn(w) { w }, put: fn(w, next) { next }),
item: virtual_delay_binding(at: sleep_delay_seconds_operation, seconds_input: "seconds"),
),
advance: bmc_advance,
}
Expand Down
13 changes: 7 additions & 6 deletions dag/gunbc/bmc_model.dag
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@ module gunbc.bmc_model
import std.types { Bool, Int, List, NonEmptyStr }
import std.measure { Second, second, second_count }
import std.optional { Present, Absent }
import std.algebra { list_snoc_item }
import v2.std.algebra { any, filter }
import extdeps.bmc.ipmi_channel { IpmiChannelNumber, IpmiUserId, IpmiUserChannelAccess, IpmiChannelPrivilegeLimit }
import extdeps.bmc.redfish_telemetry { RedfishLogEntry, RedfishLogService, RedfishTelemetryPoint }
Expand Down Expand Up @@ -229,7 +230,7 @@ fn bmc_web_login(world: BmcWorld, username: String, password: String) -> BmcWebL
if username == account.username && password == account.password {
let session = BmcWebSession { id: web.next_session_id, csrf_token: concat("csrf-", to_string(web.next_session_id)), privilege: account.privilege }
BmcWebLoginStep {
world: bmc_with_web(world: world, web: bmc_web_with(web: web, sessions: list_append(web.sessions, session), next_session_id: web.next_session_id + 1, kvm: web.kvm)),
world: bmc_with_web(world: world, web: bmc_web_with(web: web, sessions: list_snoc_item(xs: web.sessions, item: session), next_session_id: web.next_session_id + 1, kvm: web.kvm)),
reply: BmcWebLoginAccepted { session: session },
}
} else {
Expand Down Expand Up @@ -337,7 +338,7 @@ fn bmc_host_boots(world: BmcWorld, now: Second) -> BmcWorld {
let via = match world.boot_override { BootOverrideCdromEfiNextBoot => true BootOverrideNone => false }
let pending = match world.sol_drop_after_boot {
Absent => world.pending
Present { value: after } => list_append(world.pending, BmcScheduledEvent { at: second(count: second_count(s: now) + second_count(s: after)), event: BmcSolSessionDropped {} })
Present { value: after } => list_snoc_item(xs: world.pending, item: BmcScheduledEvent { at: second(count: second_count(s: now) + second_count(s: after)), event: BmcSolSessionDropped {} })
}
BmcWorld {
power: BmcPowerOn, pending: pending, fired: world.fired, boot_override: BootOverrideNone, sel: world.sel,
Expand All @@ -357,7 +358,7 @@ fn bmc_chassis_control(world: BmcWorld, action: IpmiChassisControlAction, now: S
if bmc_power_is_on(world: world) {
let off = bmc_with_power(world: world, power: BmcPowerOff)
let restore = BmcScheduledEvent { at: second(count: second_count(s: now) + second_count(s: world.cycle_off_interval)), event: BmcPowerRestored {} }
BmcChassisControlStep { world: bmc_with_pending(world: off, pending: list_append(off.pending, restore), fired: off.fired), effect_taken: true }
BmcChassisControlStep { world: bmc_with_pending(world: off, pending: list_snoc_item(xs: off.pending, item: restore), fired: off.fired), effect_taken: true }
} else { BmcChassisControlStep { world: world, effect_taken: false } }
IpmiChassisHardReset =>
if bmc_power_is_on(world: world) { BmcChassisControlStep { world: bmc_host_boots(world: world, now: now), effect_taken: true } }
Expand Down Expand Up @@ -393,7 +394,7 @@ fn bmc_advance(world: BmcWorld, now: Second) -> BmcWorld {
Present { value: e } => {
let remaining = bmc_without_first(pending: world.pending, event: e)
let applied = bmc_apply_event(world: bmc_with_pending(world: world, pending: remaining, fired: world.fired), event: e.event, at: e.at)
bmc_advance(world: bmc_with_pending(world: applied, pending: applied.pending, fired: list_append(applied.fired, e)), now: now)
bmc_advance(world: bmc_with_pending(world: applied, pending: applied.pending, fired: list_snoc_item(xs: applied.fired, item: e)), now: now)
}
}
}
Expand Down Expand Up @@ -425,7 +426,7 @@ fn bmc_without_first(pending: List<BmcScheduledEvent>, event: BmcScheduledEvent)
if !acc.removed && second_count(s: e.at) == second_count(s: event.at) && bmc_event_eq(a: e.event, b: event.event) {
BmcPendingRemoval { kept: acc.kept, removed: true }
} else {
BmcPendingRemoval { kept: list_append(acc.kept, e), removed: acc.removed }
BmcPendingRemoval { kept: list_snoc_item(xs: acc.kept, item: e), removed: acc.removed }
}
}).kept
}
Expand Down Expand Up @@ -524,7 +525,7 @@ fn bmc_with_ipmi_user_access(world: BmcWorld, rows: List<IpmiUserChannelAccess>)
fn bmc_ipmi_set_user_access(world: BmcWorld, access: IpmiUserChannelAccess) -> BmcIpmiSetUserAccessStep {
if any(world.ipmi_users, u => (u.id as Int) == (access.user as Int)) {
let others = filter(world.ipmi_user_access, r => !((r.user as Int) == (access.user as Int) && (r.channel as Int) == (access.channel as Int)))
BmcIpmiSetUserAccessStep { world: bmc_with_ipmi_user_access(world: world, rows: list_append(others, access)), completed: true }
BmcIpmiSetUserAccessStep { world: bmc_with_ipmi_user_access(world: world, rows: list_snoc_item(xs: others, item: access)), completed: true }
} else {
BmcIpmiSetUserAccessStep { world: world, completed: false }
}
Expand Down
3 changes: 2 additions & 1 deletion dag/gunbc/filesystem_model.dag
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
module gunbc.filesystem_model

import std.types { Bool, List, String }
import std.algebra { list_snoc_item }
import std.measure { second, ByteSize, byte_size }
import std.bytes { bytes_octets, utf8_encode_bytes }
import v2.std.operation_argv { OperationRef, BoundOperationInvocation }
Expand Down Expand Up @@ -128,7 +129,7 @@ fn fs_write(fs: ModeledFilesystem, path: String, content: String, create_new: Bo
fn fs_with_file(fs: ModeledFilesystem, path: String, content: String) -> ModeledFilesystem {
ModeledFilesystem {
directories: fs.directories,
files: list_append(filter(fs.files, f => f.path != path), ModeledFile { path: path, content: content }),
files: list_snoc_item(xs: filter(fs.files, f => f.path != path), item: ModeledFile { path: path, content: content }),
refused_reads: fs.refused_reads,
}
}
Expand Down
8 changes: 4 additions & 4 deletions dag/gunbc/machine_intake/mtcollins1_boot_dry_realization.dag
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ module gunbc.machine_intake_mtcollins1_boot_dry_realization
import extdeps.tools.gnu_coreutils { readlink_command }
import std.types { Bool, Int, List, NonEmptyStr, String }
import std.measure { Second, second, second_count }
import std.algebra { trim }
import std.algebra { trim, list_snoc_item }
import v2.std.operation_argv { OperationRef }
import v2.std.operation_realization {
OperationRealization, OperationBinding, OperationCall, OperationStep,
Expand Down Expand Up @@ -236,7 +236,7 @@ fn live_collectors(w: MtCollins1BootWorld) -> List<ModeledProcess> {
}

fn started(w: MtCollins1BootWorld, p: ModeledProcess, fs: ModeledFilesystem) -> MtCollins1BootWorld {
with_worker(w: with_fs(w: w, fs: if p.alive { process_visible(fs: fs, p: p) } else { fs }), worker: ModeledWorker { next_pid: p.pid + 1, processes: list_append(w.worker.processes, p), uptime_at_origin: w.worker.uptime_at_origin })
with_worker(w: with_fs(w: w, fs: if p.alive { process_visible(fs: fs, p: p) } else { fs }), worker: ModeledWorker { next_pid: p.pid + 1, processes: list_snoc_item(xs: w.worker.processes, item: p), uptime_at_origin: w.worker.uptime_at_origin })
}

// THE NOTICE WATCHER the boot step starts before the entry (gunbc.ci_spec): its token in the
Expand All @@ -246,7 +246,7 @@ fn started(w: MtCollins1BootWorld, p: ModeledProcess, fs: ModeledFilesystem) ->
fn with_notice_watcher(w: MtCollins1BootWorld, capture_path: String, token: String) -> MtCollins1BootWorld {
let p = ModeledProcess { pid: w.worker.next_pid, start_time: start_ticks(w: w, now: second(count: 0)), comm: "bash", cmdline: "bash -c gunbc-sol-notice-watch", capture_path: capture_path, diagnostic_path: "", alive: true }
let fs = fs_with_file(fs: fs_with_file(fs: w.fs, path: concat(capture_path, mtcollins1_sol_notice_ready_suffix), content: concat(token, "\n")), path: mtcollins1_sol_notice_watcher_path(capture_path: capture_path), content: process_identity(p: p))
let env = list_append(w.environment, ModeledVariable { name: mtcollins1_sol_notice_token_env as String, value: token })
let env = list_snoc_item(xs: w.environment, item: ModeledVariable { name: mtcollins1_sol_notice_token_env as String, value: token })
started(w: MtCollins1BootWorld { bmc: w.bmc, fs: w.fs, environment: env, agent: w.agent, remote_hosts: w.remote_hosts, clock: w.clock, worker: w.worker, console: w.console, media: w.media, screen: w.screen }, p: p, fs: fs)
}

Expand Down Expand Up @@ -533,7 +533,7 @@ fn owned_launch_handler(w: MtCollins1BootWorld, call: OperationCall) -> Operatio
KvmModeledRefused { event_word: word, would_write: line } => OperationHarnessFault { reason: concat("kvm_journal_line refused the modeled ", concat(word, concat(" line: ", line))) as NonEmptyStr }
KvmModeledRendered { text: t } => {
let fs = appended(fs: fs_write(fs: w.fs, path: pid_path, content: process_identity(p: p), create_new: false).fs, path: concat(dir, "/journal"), text: t)
let screen = ModeledKvmViewer { session: w.screen.session, still_bytes: w.screen.still_bytes, still_sha256: w.screen.still_sha256, observers: list_append(w.screen.observers, ModeledKvmObserver { pid: p.pid, dir: dir, seq: 0, seen_files: 0 }) }
let screen = ModeledKvmViewer { session: w.screen.session, still_bytes: w.screen.still_bytes, still_sha256: w.screen.still_sha256, observers: list_snoc_item(xs: w.screen.observers, item: ModeledKvmObserver { pid: p.pid, dir: dir, seq: 0, seen_files: 0 }) }
exited_step(state: with_screen(w: started(w: w, p: p, fs: fs), screen: screen), stdout: "", exit_code: 0)
}
}
Expand Down
3 changes: 2 additions & 1 deletion dag/gunbc/megarac_media_model.dag
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@ module gunbc.megarac_media_model

import std.types { Bool, Int, List, String }
import std.measure { Second, second, second_count }
import std.algebra { list_snoc_item }

// THE BMC's VIRTUAL-MEDIA SUBSYSTEM (AMI MegaRAC SP-X, firmware 0.32): the same controller as
// gunbc.bmc_model, held as its own record because its state -- web sessions, the NFS share binding,
Expand Down Expand Up @@ -88,7 +89,7 @@ fn megarac_open_session(world: MegaRacMediaWorld, cookie_jar: String) -> MegaRac
let id = world.next_session
let token = concat("modeled-csrf-", to_string(id))
MegaRacOpened {
world: megarac_with_sessions(world: world, sessions: list_append(world.sessions, MegaRacSession { cookie_jar: cookie_jar, csrf_token: token, open: true }), next_session: id + 1),
world: megarac_with_sessions(world: world, sessions: list_snoc_item(xs: world.sessions, item: MegaRacSession { cookie_jar: cookie_jar, csrf_token: token, open: true }), next_session: id + 1),
racsession_id: id,
csrf_token: token,
}
Expand Down
Loading