1	import Base
2	import ../json.bend as Json
3	import ../act.bend as Act
4	import ./base.bend as SBase
5	import ./seq.bend as SSeq
6	
7	# ---- the identity oracle (GET /api/oauth/profile) ------------------------------------
8	
9	# What the oracle answered: nothing usable, or an account uuid with an
10	# optional address and organization.
11	type Prof is Data:
12	  ProfNone{}
13	  Prof{uuid: String, email: Maybe<&2, String>, org: Maybe<&2, String>}
14	
15	def opt_str(+rec: Json.Json, +key: String) -> Maybe<&2, String>:
16	  Maybe.bind(&2, Json.Json, String, Json.get(key, rec), s => Json.as_string(s))
17	
18	def org_uuid_of(+o: Maybe<&2, Json.Json>) -> Maybe<&2, String>:
19	  match o:
20	    case None{}:
21	      None{}
22	    case Some{rec}:
23	      opt_str(rec, "uuid")
24	
25	def prof3b(+empty: Bool, +uuid: String, +email: Maybe<&2, String>, +org: Maybe<&2, String>) -> Prof:
26	  match empty:
27	    case True{}:
28	      ProfNone{}
29	    case False{}:
30	      Prof{uuid, email, org}
31	
32	def prof3(+uuid: String, +email: Maybe<&2, String>, +org: Maybe<&2, String>) -> Prof:
33	  prof3b(String.is_empty(uuid), uuid, email, org)
34	
35	def prof2(+acct: Maybe<&2, Json.Json>, +org: Maybe<&2, String>) -> Prof:
36	  match acct:
37	    case None{}:
38	      ProfNone{}
39	    case Some{a}:
40	      prof3(String.trim(SSeq.field_str(a, "uuid")), opt_str(a, "email"), org)
41	
42	# oauth.fetch_oauth_profile's reading of the response body.
43	def profile_of(+j: Json.Json) -> Prof:
44	  prof2(Json.get("account", j), org_uuid_of(Json.get("organization", j)))
45	
46	def profile_of_res(r: Result<&2, &2, String, Json.Json>) -> Prof:
47	  match r:
48	    case Fail{e}:
49	      ProfNone{}
50	    case Done{j}:
51	      profile_of(j)
52	
53	def profile_of_text(+body: String) -> Prof:
54	  profile_of_res(Json.parse(body))
55	
56	# Should the stored credential's owner be looked up, and with which token?
57	type Plan is Data:
58	  PSkip{why: String}
59	  PFetch{token: String}
60	
61	# The access token's expiry in whole seconds (`expiresAt` is epoch ms).
62	def expires_s(+ms: String) -> Maybe<&2, U32>:
63	  U32.read(String.take(ms, Nat.sub(String.length(ms), 3n)))
64	
65	def token_of(+creds: Json.Json) -> String:
66	  SSeq.field_str(SSeq.get_or("claudeAiOauth", creds, Json.JNull{}), "accessToken")
67	
68	def expiry_text(+m: Maybe<&2, Json.Json>) -> Maybe<&2, U32>:
69	  match m:
70	    case Some{Json.JNum{t}}:
71	      expires_s(t)
72	    case _:
73	      None{}
74	
75	def expiry_of(+creds: Json.Json) -> Maybe<&2, U32>:
76	  expiry_text(Json.get("expiresAt", SSeq.get_or("claudeAiOauth", creds, Json.JNull{})))
77	
78	def plan5(+expired: Bool, +token: String) -> Plan:
79	  match expired:
80	    case True{}:
81	      PSkip{"the access token is expired"}
82	    case False{}:
83	      PFetch{token}
84	
85	def plan4(+token: String, +expiry: Maybe<&2, U32>, +now: U32) -> Plan:
86	  match expiry:
87	    case Some{e}:
88	      plan5(U32.is_le(e, now), token)
89	    case None{}:
90	      PFetch{token}
91	
92	def plan3b(+empty: Bool, +token: String, +expiry: Maybe<&2, U32>, +now: U32) -> Plan:
93	  match empty:
94	    case True{}:
95	      PSkip{"no access token to resolve"}
96	    case False{}:
97	      plan4(token, expiry, now)
98	
99	def plan3(+token: String, +expiry: Maybe<&2, U32>, +now: U32) -> Plan:
100	  plan3b(String.is_empty(token), token, expiry, now)
101	
102	def plan_res(r: Result<&2, &2, String, Json.Json>, +now: U32) -> Plan:
103	  match r:
104	    case Fail{e}:
105	      PSkip{"no access token to resolve"}
106	    case Done{+j}:
107	      plan3(token_of(j), expiry_of(j), now)
108	
109	def plan_for(+creds: String, +now: U32) -> Plan:
110	  plan_res(Json.parse(creds), now)
111	
112	type Verdict is Data:
113	  VOk{}
114	  VUnverified{why: String}
115	  VBad{msg: String}
116	
117	def bad_uuid(+email: String, +seen: String, +want: String) -> String:
118	  "The stored credential does not belong to " ++ email ++ ": the token resolves to account " ++ seen ++ ", not " ++ want
119	    ++ ". Nothing was changed. This happens when the config names one account while the credential store still holds another's token (e.g. a renamed .claude.json over a live keychain item). Log in as "
120	    ++ email ++ " in THIS environment, then re-run."
121	
122	def bad_email(+email: String, +seen: String) -> String:
123	  "The stored credential does not belong to " ++ email ++ ": the token resolves to " ++ seen
124	    ++ ". Nothing was changed. This happens when the config names one account while the credential store still holds another's token (e.g. a renamed .claude.json over a live keychain item). Log in as "
125	    ++ email ++ " in THIS environment, then re-run."
126	
127	def bad_org(+email: String, +seen: String, +want: String) -> String:
128	  "The stored credential for " ++ email ++ " belongs to organization " ++ SBase.sel.s(String.is_empty(seen), "personal", seen)
129	    ++ ", not " ++ SBase.sel.s(String.is_empty(want), "personal", want) ++ ". Nothing was changed. Two accounts can share an email across organizations. Log in as "
130	    ++ email ++ " in the " ++ SBase.sel.s(String.is_empty(want), "personal", want) ++ " organization in THIS environment, then re-run."
131	
132	def org_verdict2(+same: Bool, +email: String, +seen: String, +want: String) -> Verdict:
133	  match same:
134	    case True{}:
135	      VOk{}
136	    case False{}:
137	      VBad{bad_org(email, seen, want)}
138	
139	def org_verdict(+email: String, +want: String, +org: Maybe<&2, String>) -> Verdict:
140	  match org:
141	    case None{}:
142	      VOk{}
143	    case Some{o}:
144	      org_verdict2(String.eq(String.trim(o), want), email, String.trim(o), want)
145	
146	# Only a clean identity match goes on to the organization check.
147	def then_org(+v: Verdict, +email: String, +want: String, +org: Maybe<&2, String>) -> Verdict:
148	  match v:
149	    case VOk{}:
150	      org_verdict(email, want, org)
151	    case _:
152	      v
153	
154	def sel.v(+c: Bool, +x: Verdict, +y: Verdict) -> Verdict:
155	  match c:
156	    case True{}:
157	      x
158	    case False{}:
159	      y
160	
161	def ident_by_email2(+empty: Bool, +email: String, +seen: String) -> Verdict:
162	  match empty:
163	    case True{}:
164	      VUnverified{"the resolved identity carries no address"}
165	    case False{}:
166	      sel.v(String.eq(String.to_lower(seen), String.to_lower(email)), VOk{}, VBad{bad_email(email, seen)})
167	
168	def ident_by_email(+email: String, +seen: String) -> Verdict:
169	  ident_by_email2(String.is_empty(seen), email, seen)
170	
171	def ident_verdict2(+no_uuid: Bool, +email: String, +acct_uuid: String, +uuid: String, +pemail: Maybe<&2, String>) -> Verdict:
172	  match no_uuid:
173	    case True{}:
174	      ident_by_email(email, String.trim(SSeq.str_or(pemail, "")))
175	    case False{}:
176	      sel.v(String.eq(uuid, acct_uuid), VOk{}, VBad{bad_uuid(email, uuid, acct_uuid)})
177	
178	def ident_verdict(+email: String, +acct_uuid: String, +uuid: String, +pemail: Maybe<&2, String>) -> Verdict:
179	  ident_verdict2(String.is_empty(acct_uuid), email, acct_uuid, uuid, pemail)
180	
181	# Does the credential's owner match (email, org, accountUuid)? Uuid first,
182	# then the address only when no uuid is on file; the org is checked either way.
183	# None from the oracle is "unresolvable", never "wrong".
184	def judge(+email: String, +org: String, +acct_uuid: String, +p: Prof) -> Verdict:
185	  match p:
186	    case ProfNone{}:
187	      VUnverified{"the identity lookup did not resolve"}
188	    case Prof{uuid, pemail, porg}:
189	      then_org(ident_verdict(email, acct_uuid, uuid, pemail), email, org, porg)
190	
191	# ---- choosing a slot (pure) ---------------------------------------------------------------
192	
193	# Where a new identity goes: its slot, the slot of another account to displace
194	# (archived, never deleted) and the old slot of the same account when it moves.
195	type SlotPlan is Data:
196	  SPOk{num: String, displace: Maybe<&2, String>, migrate: Maybe<&2, String>}
197	  SPErr{code: U32, msg: String}
198	
199	def sel.m(+c: Bool, +x: Maybe<&2, String>, +y: Maybe<&2, String>) -> Maybe<&2, String>:
200	  match c:
201	    case True{}:
202	      x
203	    case False{}:
204	      y
205	
206	def differs(+m: Maybe<&2, String>, +num: String) -> Maybe<&2, String>:
207	  match m:
208	    case Some{old}:
209	      sel.m(String.eq(old, num), None{}, Some{old})
210	    case None{}:
211	      None{}
212	
213	def occupied2(+same: Bool, +assume_yes: Bool, +num: String, +other: String) -> SlotPlan:
214	  match same assume_yes:
215	    case True{} _:
216	      SPOk{num, None{}, None{}}
217	    case False{} True{}:
218	      SPOk{num, Some{num}, None{}}
219	    case False{} False{}:
220	      SPErr{10, "Slot " ++ num ++ " already occupied by " ++ other}
221	
222	def occupied(+rec: Maybe<&2, Json.Json>, +email: String, +org: String, +assume_yes: Bool, +num: String) -> SlotPlan:
223	  match rec:
224	    case None{}:
225	      SPOk{num, None{}, None{}}
226	    case Some{r}:
227	      occupied2(SSeq.rec_is(r, email, org), assume_yes, num, SSeq.field_str(r, "email"))
228	
229	def with_migrate(+p: SlotPlan, +m: Maybe<&2, String>) -> SlotPlan:
230	  match p:
231	    case SPOk{num, d, old}:
232	      SPOk{num, d, m}
233	    case _:
234	      p
235	
236	def plan_slot2(+n: U32, +seq: Json.Json, +email: String, +org: String, +assume_yes: Bool) -> SlotPlan:
237	  with_migrate(occupied(SSeq.slot_record(seq, U32.show(n)), email, org, assume_yes, U32.show(n)),
238	    differs(SSeq.find_slot(seq, email, org), U32.show(n)))
239	
240	def plan_slot1(+low: Bool, +n: U32, +seq: Json.Json, +email: String, +org: String, +assume_yes: Bool) -> SlotPlan:
241	  match low:
242	    case True{}:
243	      SPErr{1, "Slot number must be >= 1"}
244	    case False{}:
245	      plan_slot2(n, seq, email, org, assume_yes)
246	
247	def plan_slot(+slot: Maybe<&2, U32>, +seq: Json.Json, +email: String, +org: String, +assume_yes: Bool) -> SlotPlan:
248	  match slot:
249	    case None{}:
250	      SPOk{U32.show(SSeq.next_slot(seq)), None{}, None{}}
251	    case Some{n}:
252	      plan_slot1(U32.is_lt(n, 1), n, seq, email, org, assume_yes)
253	
254	# ---- records and credential payloads ------------------------------------------------------
255	
256	def with_kind(+api_key: Bool, +rec: Json.Json) -> Json.Json:
257	  match api_key:
258	    case True{}:
259	      Json.set("kind", SSeq.jstr("api_key"), rec)
260	    case False{}:
261	      rec
262	
263	def token_record(+email: String, +ts: String, +api_key: Bool) -> Json.Json:
264	  with_kind(api_key, Json.JObj{Json.JField{"email", SSeq.jstr(email), Json.JField{"uuid", SSeq.jstr(""),
265	    Json.JField{"organizationUuid", SSeq.jstr(""), Json.JField{"organizationName", SSeq.jstr(""), Json.JField{"added", SSeq.jstr(ts), Json.JNil{}}}}}}})
266	
267	def with_alias2(+empty: Bool, +alias: String, +rec: Json.Json) -> Json.Json:
268	  match empty:
269	    case True{}:
270	      rec
271	    case False{}:
272	      Json.set("alias", SSeq.jstr(alias), rec)
273	
274	def with_alias(+alias: String, +rec: Json.Json) -> Json.Json:
275	  with_alias2(String.is_empty(alias), alias, rec)
276	
277	# {"claudeAiOauth": {"accessToken": T, "scopes": ["user:inference"]}}, as json.dumps writes it.
278	def setup_token_creds(+token: String) -> String:
279	  Json.emit_py(SSeq.obj1("claudeAiOauth", Json.JObj{Json.JField{"accessToken", SSeq.jstr(token),
280	    Json.JField{"scopes", Json.arr([SSeq.jstr("user:inference")]), Json.JNil{}}}}))
281	
282	# The config backup add-token synthesizes.
283	def token_config(+email: String) -> String:
284	  Json.emit_py(SSeq.obj1("oauthAccount", Json.JObj{Json.JField{"emailAddress", SSeq.jstr(email), Json.JField{"accountUuid", SSeq.jstr(""),
285	    Json.JField{"organizationUuid", Json.JNull{}, Json.JField{"organizationName", Json.JNull{}, Json.JNil{}}}}}}))
286	
287	def default_email(+api_key: Bool, +slot: U32) -> String:
288	  SBase.sel.s(api_key, "api-key", "setup-token") ++ "-" ++ U32.show(slot) ++ "@token.local"
289	
290	def kind_label(+api_key: Bool) -> String:
291	  SBase.sel.s(api_key, "API key", "token")
292	
293	def kind_name(+api_key: Bool) -> String:
294	  SBase.sel.s(api_key, "api_key", "oauth")
295	
296	def kind_title(+api_key: Bool) -> String:
297	  SBase.sel.s(api_key, "API-key", "OAuth")
298	
299	# `do ActM<A>:` blocks (the do-notation needs the monad's name defined here).
300	def ActM(-A: Type) -> Type:
301	  Act.of(A)
302	
303	def ActM.pure(-A: Type, x: A) -> Act.of(A):
304	  Act.pure(A, x)
305	
306	def ActM.bind(-A: Type, -B: Type, m: Act.of(A), f: A -> Act.of(B)) -> Act.of(B):
307	  Act.bind(A, B, m, f)