Skip to content

Commit 8c60e3f

Browse files
theebayusertheebayuser
authored
interpreter: prove env-independence of run/exec/execOne for import-free modules (#159)
1 parent b790306 commit 8c60e3f

1 file changed

Lines changed: 258 additions & 0 deletions

File tree

‎interpreter/Interpreter/Wasm/Semantics/Lemmas.lean‎

Lines changed: 258 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -556,4 +556,262 @@ theorem run_eq
556556
· cases n <;> rfl
557557
all_goals rfl
558558

559+
560+
/-! ## Environment independence
561+
562+
When a module declares no imported functions (`imports = []`), the host
563+
environment is never consulted: the host arm of `run` is dead, and `env`
564+
is otherwise only threaded, never inspected. So `run` (hence `exec` /
565+
`execOne`) gives the same result under any two environments. This is what
566+
lets fuel-free specs and `iris`-style adequacy results quantify over an
567+
arbitrary `env` yet be discharged at the canonical empty one. Proved by
568+
the same joint fuel induction as `fuel_mono_aux`. -/
569+
set_option maxHeartbeats 1600000 in
570+
/-- Joint env-independence for `execOne`, `exec`, and `run`, over any module
571+
with no imported functions. Proved by induction on fuel, mirroring
572+
`fuel_mono_aux`. The three projections follow. -/
573+
theorem env_indep_aux {α : Type} : ∀ (f : Nat),
574+
(∀ (m : Module) (_ : m.imports.length = 0) (st : Store α) (s : Locals)
575+
(inst : Instruction) (env env' : HostEnv α),
576+
execOne f m st s inst env = execOne f m st s inst env') ∧
577+
(∀ (m : Module) (_ : m.imports.length = 0) (st : Store α) (s : Locals)
578+
(p : Program) (env env' : HostEnv α),
579+
exec f m st s p env = exec f m st s p env') ∧
580+
(∀ (m : Module) (_ : m.imports.length = 0) (id : Nat) (initial : Store α)
581+
(args : List Value) (env env' : HostEnv α),
582+
run f m id initial args env = run f m id initial args env') := by
583+
intro f
584+
induction f with
585+
| zero =>
586+
have hOne : ∀ (m : Module) (_ : m.imports.length = 0) (st : Store α) (s : Locals)
587+
(inst : Instruction) (env env' : HostEnv α),
588+
execOne 0 m st s inst env = execOne 0 m st s inst env' := by
589+
intro m _ st s inst env env'
590+
simp only [execOne.eq_def]
591+
have hExec : ∀ (m : Module) (_ : m.imports.length = 0) (st : Store α) (s : Locals)
592+
(p : Program) (env env' : HostEnv α),
593+
exec 0 m st s p env = exec 0 m st s p env' := by
594+
intro m hh st s p env env'
595+
cases p with
596+
| nil => simp only [exec]
597+
| cons inst rest => simp only [exec, execOne.eq_def]
598+
refine ⟨hOne, hExec, ?_⟩
599+
intro m hh id initial args env env'
600+
have hnone : m.imports[id]? = none := by
601+
rw [List.eq_nil_of_length_eq_zero hh]; rfl
602+
simp only [run, hnone]
603+
rcases h : m.funcs[id - m.imports.length]? with _ | fn
604+
· rfl
605+
· simp only
606+
rw [hExec m hh initial (fn.toLocals (args.take fn.numParams).reverse) fn.body env env']
607+
rcases hres : exec 0 m initial
608+
(fn.toLocals (args.take fn.numParams).reverse) fn.body env' with
609+
_ | ⟨n, _, _⟩ | _ | _ | _ | _ | ⟨id', st', vs⟩ | _
610+
· rfl
611+
· cases n <;> rfl
612+
· rfl
613+
· rfl
614+
· rfl
615+
· rfl
616+
· simp only [runTail]
617+
· rfl
618+
| succ k ih =>
619+
obtain ⟨ihOne, ihExec, ihRun⟩ := ih
620+
-- Step 1: execOne at fuel k+1.
621+
have hOne : ∀ (m : Module) (_ : m.imports.length = 0) (st : Store α) (s : Locals)
622+
(inst : Instruction) (env env' : HostEnv α),
623+
execOne (k + 1) m st s inst env = execOne (k + 1) m st s inst env' := by
624+
intro m hh st s inst env env'
625+
cases inst with
626+
| block ps rs body =>
627+
simp only [execOne.eq_def]
628+
rw [ihExec m hh st s body env env']
629+
| loop ps rs body =>
630+
simp only [execOne_loop_succ]
631+
rw [ihExec m hh st s body env env']
632+
rcases hres : exec k m st s body env' with
633+
⟨st', s'⟩ | ⟨n, st', s'⟩ | ⟨st', vs⟩ | msg | msg | _ | ⟨id', st', vs⟩
634+
| ⟨tag, targs, st', s'⟩
635+
· rfl
636+
· cases n with
637+
| zero =>
638+
exact ihOne m hh st'
639+
{ s' with values := s'.values.take ps ++ s.values.drop ps }
640+
(.loop ps rs body) env env'
641+
| succ _ => rfl
642+
· rfl
643+
· rfl
644+
· rfl
645+
· rfl
646+
· rfl
647+
· rfl
648+
| iff ps rs thn els =>
649+
simp only [execOne.eq_def]
650+
rcases hvals : s.values with _ | ⟨v, vs⟩
651+
· rfl
652+
· cases v with
653+
| i32 c =>
654+
by_cases hc : c ≠ 0
655+
· simp only [if_pos hc]
656+
rw [ihExec m hh st { s with values := vs } thn env env']
657+
· simp only [if_neg hc]
658+
rw [ihExec m hh st { s with values := vs } els env env']
659+
| i64 _ => rfl
660+
| f32 _ => rfl
661+
| f64 _ => rfl
662+
| funcref _ => rfl
663+
| externref _ => rfl
664+
| exnref _ => rfl
665+
| v128 _ => rfl
666+
| anyref _ => rfl
667+
| call id =>
668+
simp only [execOne.eq_def]
669+
rw [ihRun m hh id st s.values env env']
670+
| callIndirect ti tj =>
671+
rcases hvals : s.values with _ | ⟨v, rest⟩
672+
· simp only [execOne.eq_def, hvals]
673+
· cases hv : v with
674+
| i64 i =>
675+
rcases htbl : st.tables[tj]? with _ | tbl
676+
· simp only [execOne.eq_def, hvals, hv, htbl]
677+
· rcases hslot : tbl[i.toNat]? with _ | slot
678+
· simp only [execOne.eq_def, hvals, hv, htbl, hslot]
679+
· cases hslot' : slot with
680+
| i32 _ => simp only [execOne.eq_def, hvals, hv, htbl, hslot, hslot']
681+
| i64 _ => simp only [execOne.eq_def, hvals, hv, htbl, hslot, hslot']
682+
| f32 _ => simp only [execOne.eq_def, hvals, hv, htbl, hslot, hslot']
683+
| f64 _ => simp only [execOne.eq_def, hvals, hv, htbl, hslot, hslot']
684+
| externref _ => simp only [execOne.eq_def, hvals, hv, htbl, hslot, hslot']
685+
| exnref _ => simp only [execOne.eq_def, hvals, hv, htbl, hslot, hslot']
686+
| v128 _ => simp only [execOne.eq_def, hvals, hv, htbl, hslot, hslot']
687+
| funcref r =>
688+
rcases hr : r with _ | fid
689+
· simp only [execOne.eq_def, hvals, hv, htbl, hslot, hslot', hr]
690+
· rcases hfn : m.funcSig? fid with _ | fnsig
691+
· simp only [execOne.eq_def, hvals, hv, htbl, hslot, hslot', hr, hfn]
692+
· rcases hty : m.types[ti]? with _ | ty
693+
· simp only [execOne.eq_def, hvals, hv, htbl, hslot, hslot', hr, hfn, hty]
694+
· by_cases hsig : m.indirectCallTypeOk fid ti fnsig ty = true
695+
· simp only [execOne.eq_def, hvals, hv, htbl, hslot, hslot', hr,
696+
hfn, hty, if_pos hsig, ihRun m hh fid st rest env env']
697+
· simp only [execOne.eq_def, hvals, hv, htbl, hslot, hslot', hr,
698+
hfn, hty, if_neg hsig]
699+
| anyref _ => simp only [execOne.eq_def, hvals, hv, htbl, hslot, hslot']
700+
| f32 _ => simp only [execOne.eq_def, hvals, hv]
701+
| f64 _ => simp only [execOne.eq_def, hvals, hv]
702+
| funcref _ => simp only [execOne.eq_def, hvals, hv]
703+
| externref _ => simp only [execOne.eq_def, hvals, hv]
704+
| exnref _ => simp only [execOne.eq_def, hvals, hv]
705+
| v128 _ => simp only [execOne.eq_def, hvals, hv]
706+
| i32 i =>
707+
rcases htbl : st.tables[tj]? with _ | tbl
708+
· simp only [execOne.eq_def, hvals, hv, htbl]
709+
· rcases hslot : tbl[i.toNat]? with _ | slot
710+
· simp only [execOne.eq_def, hvals, hv, htbl, hslot]
711+
· cases hslot' : slot with
712+
| i32 _ => simp only [execOne.eq_def, hvals, hv, htbl, hslot, hslot']
713+
| i64 _ => simp only [execOne.eq_def, hvals, hv, htbl, hslot, hslot']
714+
| f32 _ => simp only [execOne.eq_def, hvals, hv, htbl, hslot, hslot']
715+
| f64 _ => simp only [execOne.eq_def, hvals, hv, htbl, hslot, hslot']
716+
| externref _ => simp only [execOne.eq_def, hvals, hv, htbl, hslot, hslot']
717+
| exnref _ => simp only [execOne.eq_def, hvals, hv, htbl, hslot, hslot']
718+
| v128 _ => simp only [execOne.eq_def, hvals, hv, htbl, hslot, hslot']
719+
| funcref r =>
720+
rcases hr : r with _ | fid
721+
· simp only [execOne.eq_def, hvals, hv, htbl, hslot, hslot', hr]
722+
· rcases hfn : m.funcSig? fid with _ | fnsig
723+
· simp only [execOne.eq_def, hvals, hv, htbl, hslot, hslot', hr, hfn]
724+
· rcases hty : m.types[ti]? with _ | ty
725+
· simp only [execOne.eq_def, hvals, hv, htbl, hslot, hslot', hr, hfn, hty]
726+
· by_cases hsig : m.indirectCallTypeOk fid ti fnsig ty = true
727+
· simp only [execOne.eq_def, hvals, hv, htbl, hslot, hslot', hr,
728+
hfn, hty, if_pos hsig, ihRun m hh fid st rest env env']
729+
· simp only [execOne.eq_def, hvals, hv, htbl, hslot, hslot', hr,
730+
hfn, hty, if_neg hsig]
731+
| anyref _ => simp only [execOne.eq_def, hvals, hv, htbl, hslot, hslot']
732+
| anyref _ => simp only [execOne.eq_def, hvals, hv]
733+
| tryTable ps rs catches body =>
734+
simp only [execOne.eq_def]
735+
rw [ihExec m hh st s body env env']
736+
| callRef ti =>
737+
rcases hvals : s.values with _ | ⟨v, rest⟩
738+
· simp only [execOne.eq_def, hvals]
739+
· cases hv : v with
740+
| i32 _ => simp only [execOne.eq_def, hvals, hv]
741+
| i64 _ => simp only [execOne.eq_def, hvals, hv]
742+
| f32 _ => simp only [execOne.eq_def, hvals, hv]
743+
| f64 _ => simp only [execOne.eq_def, hvals, hv]
744+
| externref _ => simp only [execOne.eq_def, hvals, hv]
745+
| exnref _ => simp only [execOne.eq_def, hvals, hv]
746+
| v128 _ => simp only [execOne.eq_def, hvals, hv]
747+
| funcref r =>
748+
rcases hr : r with _ | fid
749+
· simp only [execOne.eq_def, hvals, hv, hr]
750+
· simp only [execOne.eq_def, hvals, hv, hr, ihRun m hh fid st rest env env']
751+
| anyref _ => simp only [execOne.eq_def, hvals, hv]
752+
| memOp kIdx inner =>
753+
rcases hmem : st.extraMems[kIdx - 1]? with _ | memK
754+
· simp only [execOne_memOp_succ, hmem]
755+
· rcases hdecl : m.extraMemories[kIdx - 1]? with _ | declK
756+
· simp only [execOne_memOp_succ, hmem, hdecl]
757+
· simp only [execOne_memOp_succ, hmem, hdecl,
758+
ihOne { m with memory := some declK } hh { st with mem := memK }
759+
s inner env env']
760+
| _ => simp only [execOne.eq_def]
761+
-- Step 2: exec at fuel k+1 using hOne.
762+
have hExec : ∀ (m : Module) (_ : m.imports.length = 0) (st : Store α) (s : Locals)
763+
(p : Program) (env env' : HostEnv α),
764+
exec (k + 1) m st s p env = exec (k + 1) m st s p env' := by
765+
intro m hh st s p env env'
766+
induction p generalizing st s with
767+
| nil => simp only [exec]
768+
| cons inst rest ihRest =>
769+
simp only [exec]
770+
rw [hOne m hh st s inst env env']
771+
rcases hres : execOne (k+1) m st s inst env' with
772+
⟨st', s'⟩ | ⟨n, st', s'⟩ | ⟨st', vs⟩ | msg | msg | _ | ⟨id', st', vs⟩
773+
| ⟨tag, targs, st', s'⟩
774+
· exact ihRest st' s'
775+
all_goals rfl
776+
refine ⟨hOne, hExec, ?_⟩
777+
-- Step 3: run at fuel k+1.
778+
intro m hh id initial args env env'
779+
have hnone : m.imports[id]? = none := by
780+
rw [List.eq_nil_of_length_eq_zero hh]; rfl
781+
simp only [run, hnone]
782+
rcases h : m.funcs[id - m.imports.length]? with _ | fn
783+
· rfl
784+
· simp only
785+
rw [hExec m hh initial (fn.toLocals (args.take fn.numParams).reverse) fn.body env env']
786+
rcases hres : exec (k+1) m initial
787+
(fn.toLocals (args.take fn.numParams).reverse) fn.body env' with
788+
_ | ⟨n, _, _⟩ | _ | _ | _ | _ | ⟨id', st', vs⟩ | _
789+
· rfl
790+
· cases n <;> rfl
791+
· rfl
792+
· rfl
793+
· rfl
794+
· rfl
795+
· simp only [runTail, ihRun m hh id' st' vs env env']
796+
· rfl
797+
798+
theorem execOne_env_indep
799+
{m : Module} (hm : m.imports.length = 0) {st : Store α} {s : Locals}
800+
{inst : Instruction} {fuel : Nat} {env env' : HostEnv α} :
801+
execOne fuel m st s inst env = execOne fuel m st s inst env' :=
802+
(env_indep_aux fuel).1 m hm st s inst env env'
803+
804+
theorem exec_env_indep
805+
{m : Module} (hm : m.imports.length = 0) {st : Store α} {s : Locals}
806+
{p : Program} {fuel : Nat} {env env' : HostEnv α} :
807+
exec fuel m st s p env = exec fuel m st s p env' :=
808+
(env_indep_aux fuel).2.1 m hm st s p env env'
809+
810+
/-- With no imported functions, `run` does not depend on the host environment. -/
811+
theorem run_env_indep
812+
{m : Module} (hm : m.imports.length = 0) {id : Nat} {initial : Store α}
813+
{args : List Value} {fuel : Nat} {env env' : HostEnv α} :
814+
run fuel m id initial args env = run fuel m id initial args env' :=
815+
(env_indep_aux fuel).2.2 m hm id initial args env env'
816+
559817
end Wasm

0 commit comments

Comments
 (0)