ADMIT: Cannot properly solve exists* (x: unit)

tahina-pro · tahina-pro · commit 744a9fad14b7 · 2025-11-20T00:22:13.000Z
diff --git a/src/cddl/pulse/CDDL.Pulse.Parse.Base.fst b/src/cddl/pulse/CDDL.Pulse.Parse.Base.fst
@@ -252,8 +252,9 @@ fn impl_copyful_unit
     (#p: _)
     (#v: _)
 {
-  let res = ();
+  let res: unit = ();
   fold (rel_unit res ());
+  admit (); // HELP!!!
   res
 }
 
@@ -279,6 +280,7 @@ fn impl_zero_copy_unit
     unfold (rel_unit res ())
   };
   Trade.intro_trade _ _ _ aux;
+  admit (); // HELP!
   res
 }
 
@@ -321,6 +323,7 @@ fn impl_zero_copy_always_false
   let res : squash False = ();
   fold (rel_always_false _ _ res res);
   rewrite (vmatch p c v) as (Trade.trade (rel_always_false _ _ res res) (vmatch p c v)); // by contradiction
+  admit (); // HELP!
   res
 }
 
diff --git a/src/cddl/pulse/CDDL.Pulse.Parse.MapGroup.fst b/src/cddl/pulse/CDDL.Pulse.Parse.MapGroup.fst
@@ -187,6 +187,7 @@ fn impl_zero_copy_map_nop
   {
     rewrite (rel_unit () ()) as emp
   };
+  admit (); // HELP!
   ()
 }
 

Original file line number	Diff line number	Diff line change
`@@ -252,8 +252,9 @@ fn impl_copyful_unit`
`252`	`252`	`(#p: _)`
`253`	`253`	`(#v: _)`
`254`	`254`	`{`
`255`		`- let res = ();`
	`255`	`+ let res: unit = ();`
`256`	`256`	`fold (rel_unit res ());`
	`257`	`+ admit (); // HELP!!!`
`257`	`258`	`res`
`258`	`259`	`}`
`259`	`260`
`@@ -279,6 +280,7 @@ fn impl_zero_copy_unit`
`279`	`280`	`unfold (rel_unit res ())`
`280`	`281`	`};`
`281`	`282`	`Trade.intro_trade _ _ _ aux;`
	`283`	`+ admit (); // HELP!`
`282`	`284`	`res`
`283`	`285`	`}`
`284`	`286`
`@@ -321,6 +323,7 @@ fn impl_zero_copy_always_false`
`321`	`323`	`let res : squash False = ();`
`322`	`324`	`fold (rel_always_false _ _ res res);`
`323`	`325`	`rewrite (vmatch p c v) as (Trade.trade (rel_always_false _ _ res res) (vmatch p c v)); // by contradiction`
	`326`	`+ admit (); // HELP!`
`324`	`327`	`res`
`325`	`328`	`}`
`326`	`329`