1use std::collections::{BTreeSet, HashMap, HashSet};
11
12use serde::{Deserialize, Serialize};
13
14use super::diagnostics::{Result, unsupported};
15use super::ir::{Decl, Effect, Expr, Node, Pattern, Plan, Program, Prop};
16use super::types::Type;
17use super::{Language, Span};
18
19#[derive(Clone, Copy, Debug)]
21pub struct AssumptionText {
22 pub id: &'static str,
23 pub statement: &'static str,
24}
25
26pub const IN_BOUNDS_READS: AssumptionText = AssumptionText {
27 id: "in-bounds-array-reads",
28 statement: "the translation agrees with the source on executions whose array reads are in bounds; JavaScript reads undefined at an index outside an array, where the target aborts",
29};
30
31#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
33#[serde(rename_all = "camelCase")]
34pub struct Mapping {
35 pub kind: String,
36 pub source: String,
37 pub target: String,
38 pub source_span: Option<Span>,
39}
40
41#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
43pub struct Assumption {
44 pub id: String,
45 pub statement: String,
46 pub details: Vec<String>,
47}
48
49#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
51pub struct Encoding {
52 pub id: String,
53 pub statement: String,
54}
55
56#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
58#[serde(rename_all = "camelCase")]
59pub struct TheoremRecord {
60 pub source: String,
61 pub target: String,
62 pub kind: String,
63 pub closed_goal: bool,
64 #[serde(default, skip_serializing_if = "Option::is_none")]
65 pub discharge: Option<String>,
66 #[serde(default, skip_serializing_if = "Option::is_none")]
67 pub check: Option<String>,
68}
69
70#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
72pub struct Emitted {
73 pub language: Language,
74 pub text: String,
75 #[serde(skip)]
78 pub preludes: Vec<String>,
79 #[serde(skip)]
83 pub definitions: Vec<String>,
84 pub mappings: Vec<Mapping>,
85 pub assumptions: Vec<Assumption>,
86 pub encodings: Vec<Encoding>,
87 pub theorems: Vec<TheoremRecord>,
88 pub entry: Option<String>,
89}
90
91#[derive(Clone, Copy, Debug, Default, PartialEq, Eq)]
93pub enum CtorStyle {
94 Module,
95 #[default]
96 Data,
97}
98
99#[derive(Clone, Copy, Default)]
101#[allow(clippy::struct_excessive_bools)] pub struct EmitOptions {
103 pub ctor_style: CtorStyle,
104 pub type_name: Option<fn(&str) -> String>,
105 pub value_name: Option<fn(&str) -> String>,
106 pub ctor_name: Option<fn(&str) -> String>,
107 pub module_segment: Option<fn(&str) -> String>,
108 pub generated: Option<fn(&str) -> Vec<String>>,
110 pub type_space: bool,
111 pub modules_share_term_space: bool,
112 pub modules_share_type_space: bool,
113 pub root_reserved: &'static [&'static str],
115}
116
117struct Target {
118 local: String,
119 path: Vec<String>,
120}
121
122pub struct EmitState<'p> {
123 pub program: &'p Program,
124 pub language: Language,
125 pub ident: fn(&str) -> String,
126 reserved: BTreeSet<String>,
127 options: EmitOptions,
128 names: HashMap<String, Target>,
129 ctor_names: HashMap<String, String>,
130 module_names: HashMap<String, String>,
131 taken: HashMap<String, HashSet<String>>,
132 claimed: BTreeSet<String>,
133 pub mappings: Vec<Mapping>,
134 assumptions: Vec<Assumption>,
135 encodings: Vec<Encoding>,
136 pub theorems: Vec<TheoremRecord>,
137}
138
139impl<'p> EmitState<'p> {
140 #[must_use]
141 pub fn new(
142 program: &'p Program,
143 language: Language,
144 ident: fn(&str) -> String,
145 reserved: &[&str],
146 options: EmitOptions,
147 ) -> Self {
148 let mut state = Self {
149 program,
150 language,
151 ident,
152 reserved: reserved.iter().map(|name| (*name).to_owned()).collect(),
153 options,
154 names: HashMap::new(),
155 ctor_names: HashMap::new(),
156 module_names: HashMap::new(),
157 taken: HashMap::new(),
158 claimed: BTreeSet::new(),
159 mappings: Vec::new(),
160 assumptions: Vec::new(),
161 encodings: Vec::new(),
162 theorems: Vec::new(),
163 };
164 state.assign();
165 state
166 }
167
168 fn assign(&mut self) {
170 let module_name = self.options.module_segment.unwrap_or(self.ident);
171 let module_space = if self.options.modules_share_term_space {
173 "term"
174 } else if self.options.modules_share_type_space {
175 "type"
176 } else {
177 "module"
178 };
179 let program = self.program;
180 for entry in &program.declarations {
181 let module_path = entry.module_path();
182 let mut segments = Vec::new();
183 for (index, segment) in module_path.iter().enumerate() {
184 let key = module_path[..=index].join(".");
185 if !self.module_names.contains_key(&key) {
186 let parent = module_path[..index].join(".");
187 let name =
188 self.claim(&format!("{module_space}:{parent}"), &module_name(segment));
189 self.module_names.insert(key.clone(), name);
190 }
191 segments.push(self.module_names[&key].clone());
192 }
193 let space = format!("term:{}", module_path.join("."));
194 let base = match entry {
195 Decl::Data(_) => self.options.type_name.unwrap_or(self.ident)(entry.name()),
196 _ => self.options.value_name.unwrap_or(self.ident)(entry.name()),
197 };
198 let local_space = if matches!(entry, Decl::Data(_)) && self.options.type_space {
199 format!("type:{}", module_path.join("."))
200 } else {
201 space.clone()
202 };
203 let local = self.claim(&local_space, &base);
204 self.names.insert(
205 entry.full_name().to_owned(),
206 Target {
207 local,
208 path: segments,
209 },
210 );
211 if let Decl::Data(data) = entry {
212 for ctor in &data.ctors {
213 let ctor_base = self.options.ctor_name.unwrap_or(self.ident)(&ctor.name);
214 let ctor_space = if self.options.ctor_style == CtorStyle::Module {
215 space.clone()
216 } else {
217 format!("ctor:{}", data.full_name)
218 };
219 let name = self.claim(&ctor_space, &ctor_base);
220 self.ctor_names
221 .insert(format!("{}#{}", data.full_name, ctor.name), name);
222 }
223 }
224 }
225 }
226
227 fn claim(&mut self, space: &str, name: &str) -> String {
228 if !self.taken.contains_key(space) {
229 let mut used: HashSet<String> = self.reserved.iter().cloned().collect();
231 if space.ends_with(':') {
232 used.extend(
233 self.options
234 .root_reserved
235 .iter()
236 .map(|name| (*name).to_owned()),
237 );
238 }
239 self.taken.insert(space.to_owned(), used);
240 }
241 let generated = self.options.generated;
242 let used = self
243 .taken
244 .get_mut(space)
245 .expect("namespace was just created");
246 let is_generated = |candidate: &str, used: &HashSet<String>| {
247 generated.is_some_and(|generated| {
248 generated(candidate).iter().any(|name| used.contains(name))
249 })
250 };
251 let mut candidate = name.to_owned();
252 let mut index = 2;
253 while used.contains(&candidate) || is_generated(&candidate, used) {
254 candidate = format!("{name}_{index}");
255 index += 1;
256 }
257 let mut names = vec![candidate.clone()];
258 if let Some(generated) = generated {
259 names.extend(generated(&candidate));
260 }
261 for name in names {
262 used.insert(name.clone());
263 self.claimed.insert(name);
264 }
265 candidate
266 }
267
268 #[must_use]
271 pub fn local_reserved(&self) -> BTreeSet<String> {
272 self.reserved.union(&self.claimed).cloned().collect()
273 }
274
275 #[must_use]
280 pub fn local_name(&self, full_name: &str) -> &str {
281 &self.names[full_name].local
282 }
283
284 #[must_use]
289 pub fn module_path(&self, full_name: &str) -> &[String] {
290 &self.names[full_name].path
291 }
292
293 #[must_use]
295 pub fn module_name(&self, source_path: &[String]) -> Option<&str> {
296 self.module_names
297 .get(&source_path.join("."))
298 .map(String::as_str)
299 }
300
301 #[must_use]
303 pub fn reference(&self, full_name: &str, separator: &str) -> String {
304 let target = &self.names[full_name];
305 let mut parts = target.path.clone();
306 parts.push(target.local.clone());
307 parts.join(separator)
308 }
309
310 #[must_use]
315 pub fn ctor_local(&self, data_name: &str, ctor: &str) -> &str {
316 &self.ctor_names[&format!("{data_name}#{ctor}")]
317 }
318
319 #[must_use]
321 pub fn ctor_ref(&self, data_name: &str, ctor: &str, separator: &str) -> String {
322 let local = self.ctor_local(data_name, ctor);
323 if self.options.ctor_style == CtorStyle::Module {
324 let mut parts = self.module_path(data_name).to_vec();
325 parts.push(local.to_owned());
326 return parts.join(separator);
327 }
328 format!("{}{separator}{local}", self.reference(data_name, separator))
329 }
330
331 pub fn map(&mut self, entry: &Decl, target: &str) {
333 if matches!(entry, Decl::Data(data) if data.output) {
335 return;
336 }
337 let source_span = entry.span();
338 let mut path = self.module_path(entry.full_name()).to_vec();
339 path.push(target.to_owned());
340 self.mappings.push(Mapping {
341 kind: match entry {
342 Decl::Fn(_) => "function",
343 other => other.kind(),
344 }
345 .to_owned(),
346 source: entry.full_name().to_owned(),
347 target: path.join("."),
348 source_span,
349 });
350 if let Decl::Data(data) = entry {
351 for ctor in &data.ctors {
352 self.mappings.push(Mapping {
353 kind: "constructor".to_owned(),
354 source: format!("{}.{}", data.full_name, ctor.name),
355 target: self.ctor_ref(&data.full_name, &ctor.name, "."),
356 source_span,
357 });
358 }
359 }
360 }
361
362 pub fn assume(&mut self, assumption: AssumptionText, detail: Option<&str>) {
363 let index = if let Some(index) = self
364 .assumptions
365 .iter()
366 .position(|record| record.id == assumption.id)
367 {
368 index
369 } else {
370 self.assumptions.push(Assumption {
371 id: assumption.id.to_owned(),
372 statement: assumption.statement.to_owned(),
373 details: Vec::new(),
374 });
375 self.assumptions.len() - 1
376 };
377 let record = &mut self.assumptions[index];
378 if let Some(detail) = detail
379 && !record.details.iter().any(|known| known == detail)
380 {
381 record.details.push(detail.to_owned());
382 }
383 }
384
385 pub fn machine_integer(&mut self, ty: &Type, representation: &str) {
387 let key = ty.key();
388 self.encode(
389 &format!("machine-integer:{key}"),
390 &format!("{key} values are {representation} values; every {key} operation tests where Rust panics, overflow or a zero divisor, and aborts there with Rust's panic message, and otherwise computes the in-range result exactly"),
391 );
392 }
393
394 pub fn array_read(&mut self) {
396 self.assume(IN_BOUNDS_READS, None);
397 }
398
399 pub fn encode(&mut self, id: &str, statement: &str) {
400 if !self.encodings.iter().any(|encoding| encoding.id == id) {
401 self.encodings.push(Encoding {
402 id: id.to_owned(),
403 statement: statement.to_owned(),
404 });
405 }
406 }
407
408 pub fn theorem(&mut self, full_name: &str, name: &str, closed_goal: bool, bounded: bool) {
411 let mut path = self.module_path(full_name).to_vec();
412 path.push(name.to_owned());
413 self.theorems.push(TheoremRecord {
414 source: full_name.to_owned(),
415 target: path.join("."),
416 kind: "theorem".to_owned(),
417 closed_goal,
418 discharge: bounded.then(|| "source-kernel".to_owned()),
419 check: bounded.then(|| "bounded".to_owned()),
420 });
421 }
422
423 pub fn assertion_theorem(&mut self, name: &str, effect: &Effect) {
424 self.assertion_theorem_with(name, effect, None);
425 }
426
427 pub fn assertion_theorem_with(&mut self, name: &str, effect: &Effect, discharge: Option<&str>) {
429 let span = match effect {
430 Effect::Print { span, .. }
431 | Effect::Let { span, .. }
432 | Effect::Assert { span, .. }
433 | Effect::Output { span, .. }
434 | Effect::Unwrap { span, .. } => *span,
435 };
436 self.theorems.push(TheoremRecord {
437 source: format!(
438 "main:assert@{}",
439 span.map_or_else(|| "?".to_owned(), |span| span.start.to_string())
440 ),
441 target: name.to_owned(),
442 kind: "assertion".to_owned(),
443 closed_goal: true,
444 discharge: discharge.map(str::to_owned),
445 check: None,
446 });
447 }
448
449 #[must_use]
450 pub fn assumption_list(&self) -> Vec<Assumption> {
451 self.assumptions.clone()
452 }
453
454 #[must_use]
455 pub fn encoding_list(&self) -> Vec<Encoding> {
456 self.encodings.clone()
457 }
458
459 #[must_use]
461 pub fn finish(&self, text: String, entry: Option<String>) -> Emitted {
462 Emitted {
463 language: self.language,
464 text,
465 preludes: Vec::new(),
466 definitions: Vec::new(),
467 mappings: self.mappings.clone(),
468 assumptions: self.assumption_list(),
469 encodings: self.encoding_list(),
470 theorems: self.theorems.clone(),
471 entry,
472 }
473 }
474}
475
476fn type_dependencies(ty: &Type, found: &mut HashSet<String>) {
477 match ty {
478 Type::Data { name } => {
479 found.insert(name.clone());
480 }
481 Type::Array { element } => type_dependencies(element, found),
482 _ => {}
483 }
484}
485
486fn expr_dependencies(expr: &Expr, found: &mut HashSet<String>) {
487 type_dependencies(&expr.ty, found);
488 match &expr.node {
489 Node::Call { func, .. } => {
490 found.insert(func.clone());
491 }
492 Node::Ctor { data, .. } => {
493 found.insert(data.clone());
494 }
495 Node::Binary {
496 domain: Some(domain),
497 ..
498 } => type_dependencies(domain, found),
499 Node::Cast { from, to, .. } => {
500 type_dependencies(from, found);
501 type_dependencies(to, found);
502 }
503 Node::Match { cases, .. } => {
504 for kase in cases {
505 if let Pattern::Ctor { data, .. } = &kase.pattern {
506 found.insert(data.clone());
507 }
508 }
509 }
510 _ => {}
511 }
512 for child in expr.children() {
513 expr_dependencies(child, found);
514 }
515}
516
517fn prop_dependencies(prop: &Prop, found: &mut HashSet<String>) {
518 match prop {
519 Prop::Forall { binders, body } => {
520 for binder in binders {
521 type_dependencies(&binder.ty, found);
522 }
523 prop_dependencies(body, found);
524 }
525 Prop::And { left, right } | Prop::Or { left, right } | Prop::Implies { left, right } => {
526 prop_dependencies(left, found);
527 prop_dependencies(right, found);
528 }
529 Prop::Not { arg } => prop_dependencies(arg, found),
530 Prop::Bool { expr } => expr_dependencies(expr, found),
531 other => {
532 if let Some((_, comparison)) = other.comparison() {
533 expr_dependencies(&comparison.left, found);
534 expr_dependencies(&comparison.right, found);
535 type_dependencies(&comparison.domain, found);
536 }
537 }
538 }
539}
540
541pub fn unthreaded(what: &str) -> ! {
546 panic!("{what} reaches a pure target's emitter without its abort threaded")
547}
548
549#[must_use]
551pub fn dependencies(entry: &Decl) -> HashSet<String> {
552 fn lemmas(plan: &Plan, found: &mut HashSet<String>) {
553 match plan {
554 Plan::Close { hints } => {
555 found.extend(hints.lemmas.iter().cloned());
556 found.extend(hints.unfold.iter().cloned());
557 }
558 Plan::Induction(split) | Plan::Cases(split) => {
559 for kase in &split.cases {
560 lemmas(&kase.plan, found);
561 }
562 }
563 }
564 }
565 let mut found = HashSet::new();
566 match entry {
567 Decl::Data(data) => {
568 for ctor in &data.ctors {
569 for field in &ctor.fields {
570 type_dependencies(&field.ty, &mut found);
571 }
572 }
573 }
574 Decl::Fn(function) => {
575 for param in &function.params {
576 type_dependencies(¶m.ty, &mut found);
577 }
578 type_dependencies(&function.ret, &mut found);
579 expr_dependencies(&function.body, &mut found);
580 }
581 Decl::Theorem(theorem) => {
582 for binder in &theorem.binders {
583 type_dependencies(&binder.ty, &mut found);
584 }
585 prop_dependencies(&theorem.prop, &mut found);
586 lemmas(&theorem.proof.plan, &mut found);
587 }
588 }
589 found.remove(entry.full_name());
590 found
591}
592
593pub struct Dependence {
595 marked: HashSet<String>,
596 floats: bool,
598}
599
600impl Dependence {
601 #[must_use]
604 pub fn numbers(program: &Program) -> Self {
605 let marked = program
606 .declarations
607 .iter()
608 .filter(|entry| !matches!(entry, Decl::Theorem(_)) && mentions_float(entry))
609 .map(|entry| entry.full_name().to_owned())
610 .collect();
611 Self::closed(program, marked, true)
612 }
613
614 #[must_use]
618 pub fn partial(program: &Program) -> Self {
619 let marked = program
620 .declarations
621 .iter()
622 .filter(|entry| {
623 matches!(entry, Decl::Fn(function)
624 if function.mutual || (function.recursive && function.decreasing.is_none()))
625 })
626 .map(|entry| entry.full_name().to_owned())
627 .collect();
628 Self::closed(program, marked, false)
629 }
630
631 fn closed(program: &Program, mut numeric: HashSet<String>, floats: bool) -> Self {
632 let uses: Vec<(String, HashSet<String>)> = program
633 .declarations
634 .iter()
635 .map(|entry| (entry.full_name().to_owned(), dependencies(entry)))
636 .collect();
637 let mut grew = true;
638 while grew {
639 grew = false;
640 for (name, used) in &uses {
641 if !numeric.contains(name) && used.iter().any(|name| numeric.contains(name)) {
642 numeric.insert(name.clone());
643 grew = true;
644 }
645 }
646 }
647 Self {
648 marked: numeric,
649 floats,
650 }
651 }
652
653 #[must_use]
654 pub fn prop(&self, prop: &Prop) -> bool {
655 let mut found = HashSet::new();
656 prop_dependencies(prop, &mut found);
657 (self.floats && mentions_float(prop)) || found.iter().any(|name| self.marked.contains(name))
658 }
659
660 #[must_use]
661 pub fn expr(&self, expr: &Expr) -> bool {
662 let mut found = HashSet::new();
663 expr_dependencies(expr, &mut found);
664 (self.floats && mentions_float(expr)) || found.iter().any(|name| self.marked.contains(name))
665 }
666}
667
668fn mentions_float(node: &impl Serialize) -> bool {
670 fn visit(value: &serde_json::Value) -> bool {
671 match value {
672 serde_json::Value::Array(items) => items.iter().any(visit),
673 serde_json::Value::Object(fields) => {
674 fields.get("kind").and_then(serde_json::Value::as_str) == Some("float")
675 || fields.values().any(visit)
676 }
677 _ => false,
678 }
679 }
680 serde_json::to_value(node).is_ok_and(|value| visit(&value))
681}
682
683#[must_use]
689pub fn mutual_groups(program: &Program) -> HashMap<String, Vec<&Decl>> {
690 let members: Vec<&Decl> = program
691 .declarations
692 .iter()
693 .filter(|entry| matches!(entry, Decl::Fn(function) if function.mutual))
694 .collect();
695 let calls: HashMap<&str, HashSet<String>> = members
696 .iter()
697 .map(|entry| (entry.full_name(), dependencies(entry)))
698 .collect();
699 let reached = |from: &str| {
700 let mut seen: HashSet<String> = HashSet::from([from.to_owned()]);
701 let mut stack = vec![from.to_owned()];
702 while let Some(name) = stack.pop() {
703 for next in calls.get(name.as_str()).into_iter().flatten() {
704 if calls.contains_key(next.as_str()) && seen.insert(next.clone()) {
705 stack.push(next.clone());
706 }
707 }
708 }
709 seen
710 };
711 let reach: HashMap<&str, HashSet<String>> = members
712 .iter()
713 .map(|entry| (entry.full_name(), reached(entry.full_name())))
714 .collect();
715 members
716 .iter()
717 .map(|entry| {
718 let group = members
719 .iter()
720 .copied()
721 .filter(|other| {
722 reach[entry.full_name()].contains(other.full_name())
723 && reach[other.full_name()].contains(entry.full_name())
724 })
725 .collect();
726 (entry.full_name().to_owned(), group)
727 })
728 .collect()
729}
730
731pub fn order_declarations(
740 program: &Program,
741 require_contiguous_modules: bool,
742) -> Result<Vec<&Decl>> {
743 let entries = &program.declarations;
744 let position: HashMap<&str, usize> = entries
745 .iter()
746 .enumerate()
747 .map(|(index, entry)| (entry.full_name(), index))
748 .collect();
749 let pending: Vec<HashSet<String>> = entries.iter().map(dependencies).collect();
750 let groups = mutual_groups(program);
752 let unit = |index: usize| -> Vec<&Decl> {
753 groups
754 .get(entries[index].full_name())
755 .cloned()
756 .unwrap_or_else(|| vec![&entries[index]])
757 };
758 let mut done: HashSet<&str> = HashSet::new();
759 let mut order: Vec<&Decl> = Vec::new();
760 let mut current: &[String] = &[];
761 while order.len() < entries.len() {
762 let mut ready: Vec<usize> = (0..entries.len())
763 .filter(|&index| {
764 let members = unit(index);
765 !done.contains(entries[index].full_name())
766 && members.iter().all(|member| {
767 pending[position[member.full_name()]].iter().all(|name| {
768 done.contains(name.as_str())
769 || !position.contains_key(name.as_str())
770 || members.iter().any(|other| other.full_name() == name)
771 })
772 })
773 })
774 .collect();
775 if ready.is_empty() {
776 let stuck = entries
777 .iter()
778 .find(|entry| !done.contains(entry.full_name()))
779 .expect("some declaration is pending");
780 return Err(unsupported(
781 "cyclic declarations",
782 &format!(
783 "{} depends on declarations that depend on it, which needs mutual definitions",
784 stuck.full_name()
785 ),
786 stuck.span(),
787 ));
788 }
789 let shared = |index: usize| {
790 let path = entries[index].module_path();
791 current
792 .iter()
793 .zip(path)
794 .take_while(|(left, right)| left == right)
795 .count()
796 };
797 ready.sort_by(|&left, &right| shared(right).cmp(&shared(left)).then(left.cmp(&right)));
798 let next = &entries[ready[0]];
799 for member in unit(ready[0]) {
800 if member.module_path() != next.module_path() {
801 return Err(unsupported(
802 "mutual recursion across modules",
803 &format!(
804 "{} and {} are mutually recursive in different modules; the target defines them together in one module",
805 next.full_name(),
806 member.full_name()
807 ),
808 member.span(),
809 ));
810 }
811 order.push(member);
812 done.insert(member.full_name());
813 }
814 current = next.module_path();
815 }
816 if require_contiguous_modules {
817 let mut closed: HashSet<String> = HashSet::new();
818 let mut open: &[String] = &[];
819 for entry in &order {
820 let path = entry.module_path();
821 for depth in 0..open.len() {
822 if path.get(depth) != Some(&open[depth]) {
823 for index in depth..open.len() {
824 closed.insert(open[..=index].join("."));
825 }
826 break;
827 }
828 }
829 for depth in 1..=path.len() {
830 let key = path[..depth].join(".");
831 if closed.contains(&key) {
832 return Err(unsupported(
833 "interleaved modules",
834 &format!(
835 "module {key} would have to be reopened after its declarations depend on later ones; the target cannot reopen a module"
836 ),
837 entry.span(),
838 ));
839 }
840 }
841 open = path;
842 }
843 }
844 Ok(order)
845}